Z3實數運算和數據類型理論綜合不如

這與我之前詢問的問題有關Z3 SMT 2.0 vs Z3 py implementation 我實現了具有無窮大的正實數的完整代數，解算器行爲異常。在這個簡單的實例中，當註釋約束給出約束的實際解決方案時，我就不知道了。Z3實數運算和數據類型理論綜合不如

# 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()

我不知道這是否令人驚訝或預期。有沒有辦法讓它工作？

來源

2012-12-13 user1895575

你的問題是非線性的。 Z3中新的（和完整的）非線性算術求解器（nlsat）未與其他理論（如代數數據類型）集成。看到帖子：

這是在當前版本的限制。未來的版本將解決這個問題。

與此同時，您可以通過使用不同的編碼來解決問題。如果您僅使用真正的算術和布爾值，則問題將在nlsat的範圍內。一種可能性是將MyR編碼爲Python對：Z3布爾表達式和Z3實數表達式。

這是一個部分編碼。我沒有編碼所有的操作員。該示例還可在線獲得，網址爲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()

來源

2012-12-13 21:37:09

Z3實數運算和數據類型理論綜合不如

回答

相關問題