Z3 中的地板和天花板功能实现 [英] Floor and Ceiling Function implementation in Z3
问题描述
我尝试实现以下链接中定义的地板和天花板功能
I have tried to implement Floor and Ceiling Function as defined in the following link
但 Z3 查询返回反例.
But Z3 query returning counterexample.
地板功能
_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<的调用/code> 需要一个额外的参数.但我会忽略所有这些.]
[Your encoding doesn't load to z3, it gives a syntax error even after eliminating the '..', as your call to Implies needs an extra argument. But I'll ignore all that.]
简短的回答是，您无法在 SMT-Solver 中真正执行此类操作.如果可以，那么您可以求解任意丢番图方程.简单地将其转换为 Reals，解决它(Reals 有一个决策过程)，然后通过说 Floor(solution) = solution 添加结果为整数的额外约束.因此，通过这个论点，您可以看到对此类函数进行建模将超出 SMT 求解器的能力.
The short answer is, you can't really do this sort of thing in an SMT-Solver. If you could, then you can solve arbitrary Diophantine equations. Simply cast it in terms of Reals, solve it (there is a decision procedure for Reals), and then add the extra constraint that the result is an integer by saying Floor(solution) = solution. So, by this argument, you can see that modeling such functions will be beyond the capabilities of an SMT solver.
详情请参阅此答案:获取小数部分QF_UFNRA 中的实数
话虽如此，这并不不意味着您无法在 Z3 中对此进行编码.这只是意味着它或多或少是无用的.以下是我将如何去做:
Having said that, this does not mean you cannot code this up in Z3. It just means that it will be more or less useless. Here's how I would go about it:
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，这是正确的.如果你这样做:
you'll get unsat, which is correct. If you do this instead:
s.add(Not(Floor(0.5) == 1))
print(s.check())
你会看到 z3 只是永远循环.为了使其有用，您还需要以下内容:
you'll see that z3 simply loops forever. To make this usefull, you'd want the following to work as well:
test = Real('test')
s.add(test == 2.4)
result = Int('result')
s.add(Floor(test) == result)
print(s.check())
但同样，您会看到 z3 只是永远循环.
but again, you'll see that z3 simply loops forever.
所以，底线:是的，您可以对此类构造进行建模，z3 将正确回答最简单的查询.但是对于任何有趣的事情，它都会永远循环下去.(基本上，只要你期望 sat 和大多数 unsat 场景，除非它们可以被不断折叠起来，我希望 z3 简单地循环.)而且有一个正如我所提到的，这是一个很好的理由:这些理论是不可判定的，并且远远超出了 SMT 求解器的能力范围.
So, bottom line: Yes, you can model such constructs, and z3 will correctly answer the simplest of queries. But with anything interesting, it'll simply loop forever. (Essentially whenever you'd expect sat and most of the unsat scenarios unless they can be constant-folded away, I'd expect z3 to simply loop.) And there's a very good reason for that, as I mentioned: Such theories are just not decidable and fall well out of the range of what an SMT solver can do.
如果您对建模此类函数感兴趣，最好的办法是使用更传统的定理证明器，例如 Isabelle、Coq、ACL2、HOL、HOL-Light 等.他们更适合处理这类问题.此外，请阅读获取实数的小数部分在 QF_UFNRA 中，因为它介绍了如何使用非线性实数算法对此类函数进行建模的其他一些细节.
If you are interested in modeling such functions, your best bet is to use a more traditional theorem prover, like Isabelle, Coq, ACL2, HOL, HOL-Light, amongst others. They are much more suited for working on these sorts of problems. And also, give a read to Get fractional part of real in QF_UFNRA as it goes into some of the other details of how you can go about modeling such functions using non-linear real arithmetic.
这篇关于Z3 中的地板和天花板功能实现的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
