在z3中定义有界整数

在Z3中有明确的方法来定义有界整数吗？在z3中定义有界整数

例如，假设我想定义一个整数变量“x”，它可以从[1,4]中取值。我可以做以下操作（我正在使用Java API）

IntExpr x = ctx.mkIntConst("x"); 
solver.add(ctx.mkGT(x, ctx.mkInt(0))); // (assert (> x 0)) 
solver.add(ctx.mkLT(x, ctx.mkInt(5))); // (assert (< x 5))

但是，我不知道是否有更聪明的方法来做到这一点？一些可以在声明时自动放置变量的上下限的东西。我列举了一些枚举，但我不确定这是否是最佳选择。

谢谢

来源

2017-06-29 Mohammed

如果他们是两个幂，只是使用位向量。否则，没有简单的方法来做到这一点（即你做对了）。

来源

2017-06-29 22:23:14

不幸的是，没有一种“好”的方式来模拟这种约束。比特向量走得太远了，假设你可以使用机器算术（即模块化），并且你的范围很好地适应，如前所述。以下是以前的相关讨论：Is there an UnsignedIntSort in Z3?。

要正确支持你想要的，你需要谓词子类型。定理证明者，如PVS和Yices的老版本（1.X系列中的SMTLib变体之前的版本）支持这样的花式类型，具有不同程度的自动化。如果你需要坚持现代化的SMT解决方案，不幸的是，你别无选择，只能用很多束缚约束来束缚你的代码。当然，它会非常快速地变得非常难看，因为在每次操作之后你都必须检查边界并定义上溢/下溢的含义。如果尊重边界是必不可少的，那么适当的定理证明可能是更好的选择。

来源

2017-06-30 05:42:09

谢谢Levent，我唯一担心的就是搜索空间。添加约束约束条件将有助于Z3修剪大量不相关的解决方案，但这些解决方案仍然存在，并且Z3在某一时刻考虑了这些解决方案。我可能弄错了，它可能是相同的，但是如果Z3中存在有界整数，那么可能是这种不相关的解决方案从一开始就不存在。无论如何，我现在会坚持约束约束。 – Mohammed

@Mohammed给变量或它们的组合增加了冗余*上下限，可以加快搜索速度，即使这些*约束可以从现有的约束条件推断出来（例如参见[如何计算WCET .... ]（http://dl.acm.org/citation.cfm?id=2597817&dl=ACM&coll=DL&CFID=780316479&CFTOKEN=19429447））。说到这一点，在这种情况下预测* smt *求解器的运行时间就像抛硬币一样，有几个因素起作用，包括正在考虑的问题的结构，布尔部分如何与LAR约束*进行交互。 –

在z3中定义有界整数

回答

相关问题