Z3 实数算术和数据类型理论整合得不太好

这与我之前问过的问题有关Z3 SMT 2.0 与 Z3 py 实现 https://stackoverflow.com/questions/13826217/z3-smt-2-0-vs-z3-py-implementation我实现了无穷大正实数的完整代数，但求解器行为不当。 当注释的约束给出约束的实际解决方案时，我对这个简单的实例一无所知。

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

我不知道这是令人惊讶还是预料之中。有办法让它发挥作用吗？

你的问题是非线性的。新的（完整的）非线性算术求解器（nlsat）在 Z3 中没有与其他理论（例如代数数据类型）集成。请参阅帖子：

• 使用 Z3_solver_get_unsat_core 获取 unsat 核心 https://stackoverflow.com/questions/13590129/getting-unsat-core-using-z3-solver-get-unsat-core
• 非线性算术和未解释的函数 https://stackoverflow.com/questions/10669503/non-linear-arithmetic-and-uninterpreted-functions

这是当前版本的限制。未来的版本将解决这个问题。

同时，您可以通过使用不同的编码来解决该问题。如果仅使用实数算术和布尔值，问题将在以下范围内nlsat。一种可能性是编码MyR作为 Python 对：Z3 布尔表达式和 Z3 实数表达式。

这是部分编码。我没有对所有运算符进行编码。该示例也可在线获取，网址为http://rise4fun.com/Z3Py/EJLq 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()