About CNF DIMACS formula

[Arnab Ray]

For a given C program file1.c. :

#include <stdbool.h>
bool main()
{

bool x,y,z;
y = !x;
z = y;
assert(!z);
return true;
}

I want to only save the DIMACS CNF formula alongwith the address bits of the program variables in a separate file. How to do that?

--Arnab.

[Daniel Kroening]

Hello Arnab,

do

 cbmc file1.c  --dimacs --outfile cnf

Then you get one file, named "cnf", which has the DIMACS CNF and the mapping from the DIMACS variable indices to the program variable names. If you need that in a separate file, you could use grep, like so

  grep "c " cnf > mapping

The file mapping then contains lines like these:

c main::1::y!0@1#1 10 11 12 13 14 15 16 17
c main::1::y!0@1#2 9 FALSE FALSE FALSE FALSE FALSE FALSE FALSE

c main::1::z!0@1#1 18 19 20 21 22 23 24 25
c main::1::z!0@1#2 9 FALSE FALSE FALSE FALSE FALSE FALSE FALSE

With best regards,

Daniel

[Arnab Ray]

Thanks Daniel!

How do I reduce the CNF formula corresponding to "cnf" using the variable mapping? Like in the above example, variables "10-17" all correspond to the same variable y1. 

I'd like to get the reduced CNF formula. 

[Daniel Kroening]

Hello Arnab,

I suspect that by "reduced" you mean that you were hoping to see one bit for x, y, z only, not eight. To make these variables have one bit only, use __CPROVER_bool instead of "bool". Then you get

c main::1::x!0@1#1 1

c main::1::y!0@1#1 2

c main::1::z!0@1#1 3

With best regards,

Daniel

[Arnab Ray]

Thanks a lot Daniel. I've one more question.

Is there a way in cbmc to provide custom assertions via command line? Like if I want to pass one particular design assertion and check it for multiple programs on the same set of variables. Then I wouldn't need to edit each and every program per se. 

--

---
You received this message because you are subscribed to a topic in the Google Groups "CProver Support" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/cprover-support/1M7cyeRclkk/unsubscribe.
To unsubscribe from this group and all its topics, send an email to cprover-suppo...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/cprover-support/c83ab64c-205c-4a3b-9bfd-00e401caafa8n%40googlegroups.com.

--

Regards,

Arnab.