Z3: Is it possible to simplify a part of the assertions only?

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, but I don't think Java is a necessity to answer this question.

Right now I am using the following Java code to simplify a subset of my assertions in Z3:

Tactic simplifyTactic = ctx.mkTactic("ctx-solver-simplify");
Goal goal = ctx.mkGoal(true, false, false);
goal.add(bel.toArray(new BoolExpr[0])); // bel is List<BoolExpr>
ApplyResult applyResult = simplifyTactic.apply(goal);

Up to now I have filtered the assertions to be simplified before simplifying them using the above code, which works as expected.

After some testing I came to the conclusion that I need to also insert the filtered assertions (which contained some meta information like cardinalities) of the model.

Is it possible to simplify some set A of assertions, while another set B of assertions is still regarded but not changed?

The following example may clarify this question a little bit:

(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)
(declare-const d Bool)

(assert (=> a c)); member of set A
(assert (=> b d)); member of set A
(assert a); member of set A

; member of set B
(assert 
    (<= 
        (+ (ite (= c true) 1 0) (ite (= d true) 1 0))
        1
    )
)

; member of set B
(assert 
    (>= 
        (+ (ite (= c true) 1 0) (ite (= d true) 1 0))
        1
    )
)

(apply ctx-solver-simplify)

If this SMT-LIB V2 code is executed by Z3 the result is:

(goals 
    (goal 
        c 
        (not b) 
        a 
        (<= (+ (ite (= c true) 1 0) (ite (= d true) 1 0)) 1) 
        :precision precise :depth 1
    ) 
)

For this simple example the result is quite ok. The constraints (the first three assertions (my set A)) have been simplified as expected. The following two assertion (with my cardinalities information (set B)) has been simplified as well. Now, what I want Z3 to do is do the simplifications but without mixing results of set A and B. Given more complex assertions this will happen (and happened in my case).

How is this done?

Answer 1

You'll need to add both A and B for the simplification. The following script uses the idea of checking if each assertion e in the simplified result is equal to any assertion edel in the set B, and if so, not including e in the simplified result, all done after the initial simplification using both A and B. You could of course also just remove all the assertions in B from the simplified result by their pointers, but this may fail if the assertions in B are transformed (as is the case when I ran your example in z3py instead of Z3's SMT interface), so this motivates proving if the assertions are equal or not as the script does.

It additionally checks the conjunction of all assertions in B. In general, you might have to consider permutations thereof (e.g., the conjunctions of pairs, triples, etc., of assertions in B), which may make it impractical, but maybe it will work for your purposes. It works for the example provided. Here's the script in z3py (link to rise4fun: http://rise4fun.com/Z3Py/slY6 ):

a,b,c,d = Bools('a b c d')
g = Goal()

A = []
A.append(Implies(a, c))
A.append(Implies(b, d))
A.append(a)

B = []
B.append((If(c == True, 1, 0) +  (If(d == True, 1, 0))) <=  1 )
B.append((If(c == True, 1, 0) +  (If(d == True, 1, 0))) >=  1 )

g.add(A)
g.add(B)

#t = Tactic('simplify')
#print t(g) # note difference

t = Tactic('ctx-solver-simplify')
ar = t(g)
print ar # [[c, Not(b), a, If(d, 1, 0) <= 0]]

s = Solver()
s.add(A)
result = []
for e in ar[0]: # iterate over expressions in result
  # try to prove equal
  s.push()
  s.add(Not(e == And(B))) # conunction of all assertions in B
  satres = s.check()
  s.pop()
  if satres == unsat:
    continue

  # check each in B individually
  for edel in B:
    # try to prove equal
    s.push()
    s.add(Not(e == edel))
    satres = s.check()
    s.pop()
    if satres != unsat:
      result.append(e)
      break

print result # [c, Not(b), a]