代码之家 › 专栏 › 技术社区 › Mohammed

在z3中定义有界整数

smt bounds z3 integer

Mohammed · 技术社区 · 7 年前

有没有一种聪明的方法来定义Z3中的有界整数?

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

2 回复 | 直到 7 年前

Nuno Lopes 7 年前

alias 7 年前

不幸的是,没有一种“好”的方法来模拟此类约束。如前所述,假设您可以使用机器算法(即模块化),并且您的范围非常适合,则位向量可以走得更远。以下是之前的相关讨论: Is there an UnsignedIntSort in Z3? .

为了正确地支持您想要的内容,需要谓词子类型。定理证明器,如PV和Yices的旧版本(1.X系列中的前SMTLib变体)支持这种奇特的类型,具有不同程度的自动化。不幸的是,如果您需要坚持使用现代SMT求解器,那么您别无选择,只能在代码中添加大量绑定约束。当然,它很快就会变得非常丑陋,因为每次操作后都必须检查边界,并定义其对溢出/下溢的意义。如果必须尊重边界,则适当的定理证明器可能是更好的选择。

推荐文章

AntonioGrissini · 如何在python中将字符串“翻译”为整数?

2 年前

AlexBex · Javascript中的数字在声明为变量后发生更改。即使从字符串解析它,也会返回错误的数字

2 年前

taka · 函数,该函数接受一个int数组并返回一个字符串数组,其中所有元素都转换为字符串

2 年前

Abeezuo · Ruby正则表达式,用于精确包含x个整数的字符串

3 年前

manOnTheMoon · 对于循环-我只能输入1个整数

3 年前

grative · 我怎样才能掩盖Swift中的第一个和最后一个角色?

3 年前

Kaiger Chainer · 将一个元素从list转换为int

3 年前

Mathews lee · 如何将带字母的字符串转换为int c#[重复]

3 年前

MOmo · C++中字符串的最后一个字符使用n后退()和铸造

3 年前

arka · C语言中奇怪的联合行为

3 年前