+- Python Forum (https://python-forum.io)
+-- Forum: Python Coding (https://python-forum.io/forum-7.html)
+--- Forum: Data Science (https://python-forum.io/forum-44.html)
+--- Thread: model interpretation for automated theorem proving with Z3 (/thread-28309.html)
model interpretation for automated theorem proving with Z3 - vdbrueck - Jul-13-2020
Hi, does someone know how the model output of Z3 automated theorem prover from Microsoft is interpreted?
The model output (s.model()) contains the following cryptical function description. It is not clear to me what this means. Thanks a lot for any help.
connected = [else ->
Or(And(If(Var(0) == Type!val!2,
Type!val!2,
If(Var(0) == Type!val!0,
Type!val!0,
Type!val!1)) ==
Type!val!0,
If(Var(1) == Type!val!2,
Type!val!2,
If(Var(1) == Type!val!0,
Type!val!0,
Type!val!1)) ==
Type!val!0),
And(If(Var(0) == Type!val!2,
Type!val!2,
If(Var(0) == Type!val!0,
Type!val!0,
Type!val!1)) ==
Type!val!1,
If(Var(1) == Type!val!2,
Type!val!2,
If(Var(1) == Type!val!0,
Type!val!0,
Type!val!1)) ==
Type!val!1),
And(If(Var(0) == Type!val!2,
Type!val!2,
If(Var(0) == Type!val!0,
Type!val!0,
Type!val!1)) ==
Type!val!1,
If(Var(1) == Type!val!2,
Type!val!2,
If(Var(1) == Type!val!0,
Type!val!0,
Type!val!1)) ==
Type!val!2),
And(If(Var(0) == Type!val!2,
Type!val!2,
If(Var(0) == Type!val!0,
Type!val!0,
Type!val!1)) ==
Type!val!2,
If(Var(1) == Type!val!2,
Type!val!2,
If(Var(1) == Type!val!0,
Type!val!0,
Type!val!1)) ==
Type!val!2),
And(If(Var(0) == Type!val!2,
Type!val!2,
If(Var(0) == Type!val!0,
Type!val!0,
Type!val!1)) ==
Type!val!2,
If(Var(1) == Type!val!2,
Type!val!2,
If(Var(1) == Type!val!0,
Type!val!0,
Type!val!1)) ==
Type!val!1))],The associated code is given here: from z3 import *
s=Solver()
Type=DeclareSort("Type")
connected=Function("connected",Type,Type,BoolSort())
r1=Const("r1",Type)
r2=Const("r2",Type)
r3=Const("r3",Type)
r4=Const("r4",Type)
x=Const("x",Type)
y=Const("y",Type)
w=Function("w",Type,BoolSort())
o=Function("o",Type,BoolSort())
axioms2=w(r1),o(r2),o(r3),ForAll([x,y],
Implies(And(w(x),w(y)),connected(x,y))),
ForAll([x,y],Implies(And(o(x),o(y)),connected(x,y)))]
s2=Solver()
s2.add(axioms2)
s2.check()
print ("MODEL")<br>
print (s2.model())<br>