我已尝试实现以下链接中定义的楼层和天花板功能
但是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的地方），它将永远循环下去。正如我所提到的，这有一个很好的理由：这样的理论只是无法决定的，并且远远超出了SMT求解器的功能范围。
如果您对这些函数建模感兴趣，最好的选择是使用更传统的定理证明器，例如Isabelle，Coq，ACL2，HOL，HOL-Light。它们更适合解决此类问题。