As a tactic, the smt
one will not result in any transformation or simplification of the assertions that you're trying to achieve, it's the satisfiability tactic, so for some assertions, it will return sat, unsat, unknown, or may timeout.
The use of the simplify tactic is more in line with what you want, but you may need to apply different tactics to achieve your desired transformation. However, when I encoded your problem in the SMT-LIB format and use the ctx-solver-simplify
tactic as you're trying, it returned I think what you're looking for (rise4fun link: http://rise4fun.com/Z3/r2id ):
(declare-fun A () Bool)
(declare-fun B () Bool)
(declare-fun C () Bool)
(declare-fun D () Bool)
(declare-fun E () Bool)
(declare-fun F () Bool)
(declare-fun G () Bool)
(declare-fun H () Bool)
(declare-fun I () Bool)
(assert (and (=> A B)
(=> (not B) C)
(=> A B)
(=> B A)
(=> D E)
(=> B F)
(=> G D)
(=> H I)
(=> I (not D))
(=> (not D) I)
(=> C (not B))
C))
(apply ctx-solver-simplify)
; result:
; (goals
; (goal
; (=> A B)
; (or (not D) E)
; (or (not G) D)
; (or (not H) I)
; (or (not I) (not D))
; (or D I)
; (not B)
; C
; :precision precise :depth 1)
;)
For your experimentation, you may want to go review the tactics ( http://rise4fun.com/z3/tutorialcontent/strategies#h21 ) and try some out in the SMT-LIB interface before using the API as it will probably be faster for you to experiment. Also, as you can see, this returns a goal. In the Java API, try changing to the following and looking at the ApplyResult
object's Subgoals
field (which is a collection of Goal
objects) to see if it has what you want:
Tactic simplifyTactic = ctx.mkTactic("ctx-solver-simplify");
Goal g = ctx.mkGoal();
g.Assert(bel2.toArray(new BoolExpr[0]));
ApplyResult a = simplifyTactic.Apply(g);
// look at a.Subgoals
This is based on my experience with the .NET API, which may differ slightly from the Java one, but you can check out the Goal
Java documentation here:
https://z3.codeplex.com/SourceControl/changeset/view/8bfbdf1e680d#src/api/java/Goal.java