According to simplification in Z3, there are two ways to simplify an expression in Z3: simplify and ctx-solver-simplify When using the Java api, I am only able to find the method simplify() on the com.microsoft.z3.Expr class. How can I use the ctx-solver-simplify method? It does not seem to exist in the Solver class.
0
votes
1 Answers
0
votes
You need to use a tactic, see this for an overview: http://rise4fun.com/z3/tutorialcontent/strategies
See this answer for an example in Java, as well as a comparison between using tactics or the main solver:
How to call Z3 properly from Java program?
To use the ctx-solver-simplify tactic from Java, create the object with:
Tactic css = ctx.MkTactic("ctx-solver-simplify")
where ctx is a Z3 Context object.
