Z3: Use Java API to simplify assertions

Question

I am using the Java-API of Z3 Version 4.3.2 64-bit on Windows 7 as well as Java 7 64-bit.

I'm trying to use simplify in order to gain knowledge about redundant information in my set of assertions.

My first try is to simplify the boolean expression and evaluate the result like this

Expr e = ctx.mkImplies(ctx.mkBoolConst("A"),ctx.mkBoolConst("B")).simplify();

In my example

(=> 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)

this results in a simplified formula

(and 
    (or (not A) B)
    or B C)
    or (not B) A)
    (or (not D) E)
    (or (not B) F)
    (or (not G) D)
    (or (not H) I)
    (or (not I) (not D))
    (or D I)
    (or (not C) (not B))
    C
)

I wrapped the implications in an AND expression before in order to simplify them as one expression.

This result is not yet what I want. The duplicate rule in line three of the original code is taken out (which is fine). But if C is true (last line of the example) then B must be false ((=> C (not B))). If B is false then A must be false ((=> A B)). And so on...

What I expexted was more like the following (I did this by hand so the transformations may have an error)

(and 
    (or (not A) B)       ; transformed to (not A)
    or B C)              ; transformed to C
    or (not B) A)        ; deleted
    (or (not D) E)       ; left unchanged
    (or (not B) F)       ; deleted
    (or (not G) D)       ; left unchanged
    (or (not H) I)       ; left unchanged
    (or (not I) (not D)) ; left unchanged
    (or D I)             ; left unchanged
    (or (not C) (not B)) ; transformed to (not B)
    C                    ; C
)

Next, I tried using tactics like the following

Tactic simplifyTactic = ctx.mkTactic("ctx-solver-simplify");
Tactic smtTactic = ctx.mkTactic("smt");
Tactic then = ctx.then(simplifyTactic, smtTactic, new Tactic[] {});
Solver solver = ctx.mkSolver(then);
solver.add(bel2.toArray(new BoolExpr[0])); // bel2 is List<BoolExpr>
Status status = solver.check();

Doing this leads to a model and not to simplifications. Additionally, it was a little bit difficult for me to get the simplify tactics in line to work at all. Often the result was UNKNOWN with reason "incomplete".

Are the expected results I described above computable with Z3 at all? How can it be done?

I look around in this forum already, but my points are not really answered...

Answer 1

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