我已尝试实现以下链接中定义的楼层和天花板功能
但是Z3查询返回了反例。
地板功能
_X=Real('_X')
_Y=Int('_Y')
_W=Int('_W')
_n=Int('_n')
_Floor=Function('_Floor',RealSort(),IntSort())
..
_s.add(_X>=0)
_s.add(_Y>=0)
_s.add(Implies(_Floor(_X)==_Y,And(Or(_Y==_X,_Y<_X),ForAll(_W,Implies(And(_W>=0,_W<_X),And(_W ==_Y,_W<_Y))))))
_s.add(Implies(And(Or(_Y==_X,_Y<_X),ForAll(_W,Implies(And(_W>=0,_W<_X),And(_W==_Y,_W<_Y))),_Floor(_X)==_Y))
_s.add(Not(_Floor(0.5)==0))
预期结果-未完成
实际结果-星期六
天花板功能
_X=Real('_X')
_Y=Int('_Y')
_W=Int('_W')
_Ceiling=Function('_Ceiling',RealSort(),IntSort())
..
..
_s.add(_X>=0)
_s.add(_Y>=0)
_s.add(Implies(_Ceiling(_X)==_Y,And(Or(_Y==_X,_Y<_X),ForAll(_W,Implies(And(_W>=0,_W<_X),And(_W ==_Y,_Y<_W))))))
_s.add(Implies(And(Or(_Y==_X,_Y<_X),ForAll(_W,Implies(And(_W>=0,_W<_X),And(_W==_Y,_Y<_W)))),_Ceiling(_X)==_Y))
_s.add(Not(_Ceilng(0.5)==1))
预期结果-未完成
实际结果-星期六
[您的编码不会加载到z3，即使在消除了'..'之后，它也会产生语法错误，因为您对Implies的调用需要一个额外的参数。但我会忽略所有这些。]
简短的答案是，您实际上无法在SMT求解器中执行这种操作。如果可以，则可以求解任意Diophantine方程。只需按照Reals对其进行转换，求解即可（存在Reals的决策过程），然后通过说Floor(solution) = solution添加额外约束，即结果为整数。因此，通过此参数，您可以看到对此类函数进行建模将超出SMT求解器的功能。
请参阅此答案以获取详细信息：Get fractional part of real in QF_UFNRA
话虽如此，但not表示您无法在Z3中进行编码。它只是意味着它将或多或少地无用。这是我的处理方式：
from z3 import *
s = Solver()
Floor = Function('Floor',RealSort(),IntSort())
r = Real('R')
f = Int('f')
s.add(ForAll([r, f], Implies(And(f <= r, r < f+1), Floor(r) == f)))
现在，如果我这样做：
s.add(Not(Floor(0.5) == 0))
print(s.check())
您将获得unsat，这是正确的。如果您改为这样做：
s.add(Not(Floor(0.5) == 1))
print(s.check())
您会看到z3永远循环下去。为了使此功能有用，您希望以下内容也能起作用：
test = Real('test')
s.add(test == 2.4)
result = Int('result')
s.add(Floor(test) == result)
print(s.check())
但是再次，您会看到z3永远循环。
因此，最重要的是：是的，您可以对此类构造进行建模，并且z3将正确回答最简单的查询。但是，如果有任何有趣的事情，它将永远循环下去。 （基本上，只要您期望sat和大多数unsat场景，除非它们可以被固定折叠即可，我希望z3会简单地循环。）这有一个很好的理由，正如我提到的：这样的理论只是不可决定的，远远超出了SMT求解器的功能范围。
如果您对这些函数建模感兴趣，最好的选择是使用更传统的定理证明器，例如Isabelle，Coq，ACL2，HOL，HOL-Light等。它们更适合解决此类问题。另外，请阅读Get fractional part of real in QF_UFNRA，其中涉及如何使用非线性实数算法对此类函数进行建模的其他一些细节。