Z3 and DIMACS output

Question

Z3 currently supports the DIMACS format for input. Is there any way to output the DIMACS format for the problem before solution? I mean converting the problem to a system CNFs and output it in a DIMACS format. If not, any ideas towards this direction would be more than helpful.

Accepted Answer

The DIMACS format is very primitive, it supports only Boolean variables. Z3 does not reduce every problem into SAT. Some problems are solved using a propositional SAT solver, but this is not the rule. This usually only happens if the input contains only Boolean and/or Bit-vector variables. Moreover, even if the input problem contains only Boolean and Bit-vector variables, there is no guarantee that Z3 will use a pure SAT solver to solve it.

That being said, you can use the tactic framework to control Z3. For example, for Bit-vector problems, the following tactic will convert it into a propositional formula in CNF format. It should be straightforward to convert it into DIMACS. Here is the example. You can try it online at: http://rise4fun.com/Z3Py/E1s

```
x, y, z = BitVecs('x y z', 16)
g = Goal()
g.add(x == y, z > If(x < 0, x, -x))
print g
# t is a tactic that reduces a Bit-vector problem into propositional CNF
t = Then('simplify', 'bit-blast', 'tseitin-cnf')
subgoal = t(g)
assert len(subgoal) == 1
# Traverse each clause of the first subgoal
for c in subgoal[0]:
  print c
```

Z3 and DIMACS output

Solution

Problem