The Z3 command line tool does not have this option. Moreover, Z3 contains several solvers and preprocessing steps. It is not clear which step will be useful to you. The Z3 source code is available at https://github.com/Z3Prover/z3 . When Z3 compiles in debug mode, it provides an additional command line option -tr:<tag> . This option can be used to selectively transmit information. For example, the nlsat_solver.cpp source file contains the following command:
TRACE("nlsat", tout << "starting search...\n"; display(tout); tout << "\nvar order:\n"; display_vars(tout););
The command line -tr:nlsat will instruct Z3 to follow the instructions above. tout - trace output stream. It will be saved in a .z3-trace file. The Z3 source is populated with these TRACE commands. Since the code is available, we can also add our own trace commands to the code.
If you publish your example, I can tell you which components of Z3 are used for preprocessing and solving the problem. Then we can choose which “tags” we should include for tracking.
EDIT (after constraints were published): Your example is in mixed integer and real nonlinear arithmetic. The new non-linear arithmetic solver ( nlsat ) in Z3 does not support to_int . Thus, the general purpose solver Z3 is used to solve your problem. Although this solver accepts almost everything, it is not even complete for nonlinear real arithmetic. Nonlinear support for this solver is based on: interval analysis and Grobner's basic calculations. This solver is implemented in the src/smt (in an unstable branch ). The arithmetic module is implemented in the theory_arith* files. A good trace command line option is -tr:after_reduce . It will display a set of constraints after preprocessing. The bottleneck is the arithmetic module ( theory_arith* ).
Additional notes:
The problem is an unsolvable fragment: mixed integer and real nonlinear arithmetic. That is, it is impossible to record sound and a complete solver for this fragment. Of course, we can write a solver that solves the examples that we find in practice. I believe you can extend nlsat to handle to_int .
If you avoid to_int , you can use nlsat . The problem will be in a nonlinear real arithmetic fragment. I understand that this can be difficult, since to_int seems to be the key in your encoding.
The code in the "unstable" branch on z3.codeplex.com is much better organized than the official version in the "leading" branch. I will soon combine it with the "master." You can get an "unstable" branch if you want to play with the source code.
The "unstable" branch uses a new build system. You can create a release version with trace support. You just need to use the -t option when creating the Makefile.
python / mk_make.py -t scripts
- When Z3 is compiled in debug mode, the option
AUTO_CONFIG=false by default. Thus, to reproduce the behavior of the release mode, you must specify the command line option AUTO_CONFIG=true .