DIMACS internal representation

[alipourm]

How can I dump internal dimacs representation when I'm running z3 on SMT2 formatted files? Is there option to enable when I'm building z3?

[NikolajBjorner]

SMT2 format is much more general than DIMACS, so not all formulas can correspond to an equi-satisfiable DIMACS representation of a SAT problem. So assuming that SMT2 maps to DIMACS is in general false. For example, SMT2 allows you to write formulas over linear (and non-linear) arithmetic. There is no such direct representation in DIMACS for propositional logic. At best you can invoke some theorems that map ILP to a polynomial size representation in propositional logic and try your luck. Of course SMT solvers want to be less naïve and apply native procedures for theories, such as arithmetic.

For QF_FD (finite domain problems, that include bit-vectors and finite data-types) formulas can be converted to DIMACS. A future version of Z3 will have an option from the binary API to print goals to DIMACS. For formulas that go beyond QF_FD, the formulas will be abstractions. This can easily lead to confusion among use scenarios so I even wonder about the usefulness of this feature.

Note that you can use the binary API already to walk formulas that have been clausified and simplified, and bit-blasted and write your own pretty printer to DIMACS.

[alipourm]

Thank you, Nikolaj.

My main goal is to (1) translate a verified program to the corresponding SMT, (2) find an unsat-core of the formula, (3) and finally map the core to the corresponding statement.

I'm using CBMC to translate a program to SMT2 for the first phase. My current problem is that it uses uninterpreted functions for abstracting functions, for example a block in a function can be represented as (define-fun |B89| () Bool (and |goto_symex::&92;guard#4| (not |goto_symex::&92;guard#5|) |goto_symex::&92;guard#6|)).

This causes a problem: When I extract the unsat-core, z3 only return named asserts in cores, but I need finer grain cores to find the corresponding statements in the functions. Is there any way to get a finer-grain core in z3?

[NikolajBjorner]

Not sure how to answer directly. Exporting to DIMACS seems like a diversion from the purpose you are stating. The general statement is that you can extract cores for the set of assertions you track. You decide which assertions are tracked and Z3 will report cores over tracked assertions. Alternatively you can use indicator variables with clauses and check satisfiability with the indicator variables as assumptions. The SMT-LIB2.6 format describes the format for using such indicator variables. A SAT solver doesn't really give you anything more: the use of indicator variables is based on an approach developed by MiniSAT and adapted widely. With clausal proofs you may dispense with these variables and scale better, but in terms of basic capabilities they are the same with Z3.

Note that |B89| is a macro for a conjunction using three literals. These are not really functions. They are propositional identifiers. "define-fun" acts as a macro definition. "declare-fun" can be used for 0-ary functions, in other words as placeholder for "declare-const", which are treated as uninterpreted identifiers (I tend to call them uninterpreted constants).

[NikolajBjorner]

I am not sure what is actionable here. You can get cores by using assumption literals, similar to minisat etc. and also as described in the SMT-LIB2 format for check-sat with assumptions.