Z3 实数算法和数据类型理论整合得不是很好 [英] Z3 real arithmetics and data types theories integrating not that well
问题描述
这与我之前在 Z3 SMT 2.0 提出的问题有关vs Z3 py 实现我为无穷大的正实数实现了完整的代数，但求解器行为不端.当注释约束给出约束的实际解决方案时，我对这个简单实例一无所知.
This is related to the question I asked before at Z3 SMT 2.0 vs Z3 py implementation I implemented the full algebra for positive reals with infinity and the solver is misbehaving. I get unknown on this simple instance, when the commented constraint gives an actual solution for the constraint.
# 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()
我不知道这是令人惊讶的还是意料之中的.有没有办法让它工作?
I don't know whether this is surprising or expected. Is there a way to make it work?
推荐答案
您的问题是非线性的.Z3 中新的(完整的)非线性算术求解器 (nlsat) 未与其他理论(如代数数据类型)集成.查看帖子:
Your problem is nonlinear. The new (and complete) nonlinear arithmetic solver (nlsat) in Z3 is not integrated with other theories such as algebraic datatypes. See the posts:
这是当前版本的限制.未来的版本将解决这个问题.
This is a limitation in the current version. Future versions will address this issue.
同时，您可以通过使用不同的编码来解决该问题.如果只使用实数和布尔值，问题将在 nlsat 的范围内.一种可能性是将 MyR 编码为 Python 对:Z3 布尔表达式和 Z3 实数表达式.
In the meantime, you can workaround the problem by using a different encoding. If you use only real arithmetic and Booleans, the problem will be in the scope of nlsat. One possibility is to encode MyR as a Python pair: Z3 Boolean expression and Z3 Real expression.
这里是部分编码.我没有对所有运算符进行编码.该示例也可在 http://rise4fun.com/Z3Py/EJLq
Here is a partial encoding. I did not encode all operators. The example is also available online at http://rise4fun.com/Z3Py/EJLq
from z3 import *
# Encoding MyR as pair (Z3 Boolean expression, Z3 Real expression)
# We use a class to be able to overload +, *, <, ==
class MyRClass:
def __init__(self, inf, val):
self.inf = inf
self.val = val
def __add__(self, other):
other = _to_MyR(other)
return MyRClass(Or(self.inf, other.inf), self.val + other.val)
def __radd__(self, other):
return self.__add__(other)
def __mul__(self, other):
other = _to_MyR(other)
return MyRClass(Or(self.inf, other.inf), self.val * other.val)
def __rmul(self, other):
return self.__mul__(other)
def __eq__(self, other):
other = _to_MyR(other)
return Or(And(self.inf, other.inf),
And(Not(self.inf), Not(other.inf), self.val == other.val))
def __ne__(self, other):
return Not(self.__eq__(other))
def __lt__(self, other):
other = _to_MyR(other)
return And(Not(self.inf),
Or(other.inf, self.val < other.val))
def MyR(name):
# A MyR variable is encoded as a pair of variables name.inf and name.var
return MyRClass(Bool('%s.inf' % name), Real('%s.val' % name))
def MyRVal(v):
return MyRClass(BoolVal(False), RealVal(v))
def Inf():
return MyRClass(BoolVal(True), RealVal(0))
def _to_MyR(v):
if isinstance(v, MyRClass):
return v
elif isinstance(v, ArithRef):
return MyRClass(BoolVal(False), v)
else:
return MyRVal(v)
s0 = MyR('s0')
s1 = MyR('s1')
s2 = MyR('s2')
sol = Solver()
sol.add( s2 == s0*s1,
s0 != Inf(),
s1 != Inf(),
s0 == s1,
s2 == 2,
)
print sol
print sol.check()
print sol.model()
这篇关于Z3 实数算法和数据类型理论整合得不是很好的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
