Jul-13-2020, 05:10 PM
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.
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>