这与我之前在Z3 SMT 2.0 与 Z3 py 实现中提出的问题有关, 我实现了具有无穷大的正实数的完整代数,并且求解器行为不端。当注释的约束为约束提供实际解决方案时,我在这个简单的实例上变得未知。
# Data type declaration
MyR = Datatype('MyR')
MyR.declare('inf');
MyR.declare('num',('re',RealSort()))
MyR = MyR.create()
inf = MyR.inf
num = MyR.num
re = MyR.re
# Functions declaration
#sum
def msum(a, b):
return If(a == inf, a, If(b == inf, b, num(re(a) + re(b))))
#greater or equal
def mgeq(a, b):
return If(a == inf, True, If(b == inf, False, re(a) >= re(b)))
#greater than
def mgt(a, b):
return If(a == inf, b!=inf, If(b == inf, False, re(a) > re(b)))
#multiplication inf*0=0 inf*inf=inf num*num normal
def mmul(a, b):
return If(a == inf, If(b==num(0),b,a), If(b == inf, If(a==num(0),a,b), num(re(a)*re(b))))
s0,s1,s2 = Consts('s0 s1 s2', MyR)
# Constraints add to solver
constraints =[
s2==mmul(s0,s1),
s0!=inf,
s1!=inf
]
#constraints =[s2==mmul(s0,s1),s0==num(1),s1==num(2)]
sol1= Solver()
sol1.add(constraints)
set_option(rational_to_decimal=True)
if sol1.check()==sat:
m = sol1.model()
print m
else:
print sol1.check()
我不知道这是令人惊讶还是意料之中。有没有办法让它工作?