CODEWITHSUNDEEP
pythonz3
i'm ashamed with what i asked
i'm ashamed with what i asked

Reputation: 576

Use another solver() as input

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

Answers (1)

alias
alias

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

Related Questions