Reputation: 576
I want to use existing solver()
as input. For example , i have three solver:
Tie, Shirt = Bools('Tie Shirt')
s_one = Solver()
s_one.add(Or(Tie, Shirt))
s_two = Solver()
s_two.add(Or(Not(Tie), Shirt))
s_three = Solver()
s_three.add(Or(Not(Tie), Not(Shirt)))
Now i want to combine all the solver to something like this : (this script doesn't work, just to show what i meant)
s_four = Solver()
s_four.add(s_one, Or(s_two, s_three))
How do i do something like that ?
Upvotes: 1
Views: 60
Reputation: 30525
This is a bit of an odd thing to do, since you already know what the assertions you're adding are. But I can imagine scenarios where you have solvers coming from different parts of the program, or if you are building a library on top of z3 itself.
To achieve what you want, use the assertions
method:
from z3 import *
Tie, Shirt = Bools('Tie Shirt')
s_one = Solver()
s_one.add(Or(Tie, Shirt))
s_two = Solver()
s_two.add(Or(Not(Tie), Shirt))
s_three = Solver()
s_three.add(Or(Not(Tie), Not(Shirt)))
s_four = Solver()
s_four.add(s_one.assertions(), Or(list(s_two.assertions()) + list(s_three.assertions())))
print(s_four.sexpr())
This prints:
(declare-fun Shirt () Bool)
(declare-fun Tie () Bool)
(assert (or Tie Shirt))
(assert (or (not Tie) Shirt (not Tie) (not Shirt)))
Upvotes: 2