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]