7

The theorem proving tool z3 is taking a lot of time to solve a formula, which I believe it should be able to handle easily. To understand this better and possibly optimize my input to z3, I wanted to see the internal constraints that z3 generates as part of its solving process. How do I print the formula that z3 produces for its back-end solvers, when using z3 from the command line?

user1779685
  • 283
  • 2
  • 8

1 Answers1

12

Z3 command line tool does not have such option. Moreover, Z3 contains several solvers and pre-processing steps. It is unclear which step would be useful for you. The Z3 source code is available at https://github.com/Z3Prover/z3. When Z3 is compiled in debug mode, it provides an extra command line option -tr:<tag>. This option can be used to selectively dump information. For example, the source file nlsat_solver.cpp contains the following instruction:

TRACE("nlsat", tout << "starting search...\n"; display(tout); 
               tout << "\nvar order:\n"; 
               display_vars(tout););

The command line option -tr:nlsat will instruct Z3 to execute the instruction above. tout is the trace output stream. It will be stored in the file .z3-trace. The Z3 source is full of these TRACE commands. Since the code is available, we can also add our own trace commands in the code.

If you post your example, I can tell you which Z3 components are used to preprocess and solve it. Then, we can select which "tags" we should enable for tracing.

EDIT (after the constraints were posted): Your example is in the mixed integer & real nonlinear arithmetic. The new nonlinear arithmetic solver (nlsat) in Z3 does not support to_int. Thus, the Z3 general purpose solver is used to solve your problem. Although this solver accepts almost everything, it is not even complete for nonlinear real arithmetic. The nonlinear support on this solver is based on: interval analysis and Grobner basis computations. This solver is implemented in the folder src/smt (in the unstable branch). The arithmetic module is implemented in the files theory_arith*. A good tracing command line option is -tr:after_reduce. It will display the set of constraints after pre-processing. The bottleneck is the arithmetic module (theory_arith*).

Additional Remarks:

  • The problem is in a undecidable fragment: mixed integer & real nonlinear arithmetic. That is, it is impossible to write a sound and complete solver for this fragment. Of course, we can write a solver that solves instances we find in practice. I believe it is possible to extend nlsat to handle the to_int.

  • If you avoid to_int, you will be able to use nlsat. The problem will be in the nonlinear real arithmetic fragment. I understand that this may be hard, since the to_int seems to be a key thing in your encoding.

  • The code in the "unstable" branch at z3.codeplex.com is much better organized than the official version in the "master" branch. I will merge it with the "master" branch soon. You can retrieve the "unstable" branch if you want to play with the source code.

  • The "unstable" branch uses a new build system. You can build the release version with tracing support. You just have to use the option -t when generating the Makefile.

python scripts/mk_make.py -t

  • When Z3 is compiled in debug mode, the option AUTO_CONFIG=false by default. Thus, to reproduce the behavior of "release" mode, you must provide the command line option AUTO_CONFIG=true.
OrenIshShalom
  • 5,974
  • 9
  • 37
  • 87
Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53
  • Thanks for your prompt responses. – user1779685 Oct 30 '12 at 19:08
  • Thanks also for the link to the source code: I had not known it had been released. As you suggest, I'll try using tags and trace to dump selective information. If you could give hints as to what modules may be involved, that would be very helpful - it would also help me tune the constraints - I believe I might not be using z3 in the best possible way for this problem. stackoverflow is not allowing me to paste that code: probably exceeds their line limit for a post. I'll try posting that again as a new post or distill parts of the constraints and post portions while also being comprehensible. – user1779685 Oct 30 '12 at 19:26
  • (assert (>= a b)) (assert (and (< a 128.0) (>= a 1.0))) (assert (and (< b 128.0) (>= b 0.5))) (assert (and (< c 128.0) (>= c 0.5))) (assert (= two-to-p (to_real (^ 2 23)))) ;Computing exponent of a (assert (= two-to-exp-a (ite (and (>= a 0.5) (< a 1.0)) 0.5 (ite (and (>= a 1.0) (< a 2.0)) 1.0 (ite (and (>= a 2.0) (< a 4.0)) 2.0 (ite (and (>= a 4.0) (< a 8.0)) 4.0 (ite (and (>= a 8.0) (< a 16.0)) 8.0 (ite (and (>= a 16.0) (< a 32.0)) 16.0 (ite (and (>= a 32.0) (< a 64.0)) 32.0 (ite (and (>= a 64.0) (< a 128.0)) 64.0 (ite (and (>= a 128.0) (< a 256.0)) 128.0 256.0))))))))))) – user1779685 Oct 30 '12 at 19:37
  • (assert (= a-plus-b-real (+ a b))) (assert (= overflow (>= a-plus-b-real (+ two-to-exp-a two-to-exp-a)))) (assert (or (and (not overflow) (= two-to-exp-a-plus-b two-to-exp-a) (= a-plus-b (* (/ (to_real (to_int (* (/ a-plus-b-real two-to-exp-a-plus-b) two-to-p))) two-to-p) two-to-exp-a-plus-b))) (and overflow (= two-to-exp-a-plus-b (+ two-to-exp-a two-to-exp-a)) (= a-plus-b (* (/ (to_real(to_int (* (/ a-plus-b-real two-to-exp-a-plus-b) two-to-p))) two-to-p) two-to-exp-a-plus-b))))); – user1779685 Oct 30 '12 at 19:40
  • Parts of constraints are above, Constraint Summary: It involves mainly real arithmetic. All declarations are for Real type. There are Real operations like +,*,/ on variables. It also uses to_real and to_int. I get a counterexample (as expected) quickly when I use lesser values for two-to-p, like (to_real (^ 2 10)), but z3 seems to choke when I give larger values , eg., (to_real (^ 2 23)) which is what I really need to do (In the end, I assert inequality between two real values). Sorry - the formatting seems to have got messed up when posting from formatted file. – user1779685 Oct 30 '12 at 19:44
  • UPDATE: Here's a link to the [z3 constraints file](http://www.ccs.neu.edu/home/jaideep/z3-constraints). Thanks in advance. – user1779685 Oct 30 '12 at 20:32