[QUESTION] How to log all SAT literals

[cvick32]

I'm working on a tool that profiles SAT solvers. I'd like to have a map from variables in a goto program to their corresponding SAT literals so that I can log which areas of a goto program the SAT solver is spending the most time. When I print out the DIMACS for a given C file, there is a variable to literal mapping, but it doesn't seem to map all of the literals in the SAT problem. Is there a way that I can log the rest of the literals and the constructs that they represent? I figure that the unused literals are used for scaffolding the problem in CBMC, but I'm not sure.

To take a concrete example, the following C file:

#define SIZE 20
char buffer[SIZE];

char read_buffer(int i)  {
  if (0 <= i && i < SIZE) return buffer[i];
  return '\0';
}
char read_pointer(int i) {
  if (0 <= i && i < SIZE) return *(buffer + i);
  return '\0';
}

int main() {
  int index;
  read_buffer(index);
  read_pointer(index);
}

Produces the below variable to literal mapping in the DIMACS. This is very close to what I'm after and includes all of the goto variables that were generated. But it raises a few questions.

First, what does it mean for a variable to be full of FALSE or TRUE? I've seen in solvers/flattening/bv_dimacs.cpp that this means that the variable is constant, but does that mean it is not represented in the SAT problem at all?

Second, what does it mean for variables to share regions of literals? read_pointer::i!0@1#1, read_buffer::i!0@1#1, and main::1::index!0@1#1 all share the same literal representation.

Finally, how do I interpret the "missing" literals in the range 35-166 and 231-553? It seems these literals are important as they appear in the generated clauses, but they don't map to any goto variables.

Thanks for your help!

p cnf 553 1230
...
c goto_symex::\guard#1 1
c goto_symex::\guard#2 2
c prop_conv::context$0 553
c symex::args::1 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230
c symex::args::0 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198
c read_pointer::i!0@1#1 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
c read_buffer::i!0@1#1 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
c main::1::index!0@1#1 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
c buffer#1[[13]] FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c __CPROVER_deallocated#1 FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c buffer#1[[F]] FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c buffer#1[[C]] FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c buffer#1[[B]] FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c buffer#1[[A]] FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c buffer#1[[9]] FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c buffer#1[[8]] FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c buffer#1[[7]] FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c buffer#1[[6]] FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c buffer#1[[5]] FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c buffer#1[[2]] FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c buffer#1 FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c buffer#1[[4]] FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c buffer#1[[12]] FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c __CPROVER_memory_leak#1 FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c buffer#1[[3]] FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c buffer#1[[10]] FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c buffer#1[[11]] FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c __CPROVER_max_malloc_size!0#1 FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE TRUE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c __CPROVER_rounding_mode!0#1 FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c buffer#1[[1]] FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c __CPROVER_dead_object#1 FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c buffer#1[[E]] FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c buffer#1[[0]] FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE
c buffer#1[[D]] FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE