z3py 相关问题

Z3 Theorem Prover的Python接口

如何为从IndexOf表达式获得的值添加偏移量？也就是说，我该怎么做？ > import z3> s ='hello'> t ='e'> z3.simplify（z3.IndexOf（s，t，0）+ z3.IntVal（1））z3 ....

z3 z3py

回答 1 投票 2

Z3 bitvecs到Int和back

我有以下代码：从z3 import * a0 = Int（'a0'）a1 = Int（'a1'）a2 = Int（'a2'）v1 = BitVec（'v1'，32）s.add（v1 = =（（a0 + a1）>> 31）>> 30）s.add（（（v1 + a2）＆3） - v1 == 1）...

python z3 z3py

回答 1 投票 0

在z3中如何获取字符串的上部？

我想断言我的字符串变量的上限等于字符串值。 E.g> v = z3.String（'var'）> v.upper（）== z3.StringVal（'HELLO'）但是，我没有看到从z3获得上层的方法......

z3 z3py

回答 1 投票 0

Z3是否会添加添加剂？

我知道Z3具有基于堆栈的缓存，可以添加和缓存其他公式。是否有内置的方式或扩展，允许组合两个Z3缓存？来自z3的例子（Z3 py）......

caching z3 z3py

回答 1 投票 0

在Bools列表上创建一个or-constraint

我正在使用Python中的Z3来生成解散难题的解决方案。我以前没有SAT / SMT求解器或Z3的经验，甚至我的Python仍处于pidgin级别。所以请温柔。 ...

python z3 z3py

回答 1 投票 1

保存并重新加载z3py解算器约束

我可以保存为z3解算器创建的约束，然后重新加载它们以继续寻找更多解决方案吗？我已经知道有这样的东西的SMT-LIB2格式和z3和z3py ......

z3 z3py

回答 1 投票 2

如何通过Z3或SMT-Lib添加新逻辑？

我有一个理论部分，我在其中描述新的逻辑，我想实现它。但我不想从头开始做所有事情。我看到SMT-Lib / Z3有很大的潜力，所以我怎样才能实现我的......

z3 smt z3py lib

回答 1 投票 0

将Z3与Google Colaboratory一起使用

我试图从谷歌Colaboratory运行Z3（https://github.com/Z3Prover/z3）到目前为止没有运气。我可以使用！apt-get install z3正确安装它。但Python绑定似乎不是......

google-colaboratory z3py

回答 2 投票 0

使用Optimize.minimize（）时，我可以使用“超时”获得解决方案吗？

我正在尝试最小化变量，但z3需要很长时间才能给我一个解决方案。我想知道是否有可能在超时被触发时获得解决方案。如果是的话我该怎么办...

z3 z3py

回答 1 投票 1

如何在Z3py中激活部分模式？

我正在使用Z3的Python绑定，我很好奇，部分模式会加速我的模型。但是在Python中似乎没有办法做到这一点。（set_param（...）似乎没有......

python z3 z3py

回答 1 投票 0

（get-unsat-core）Z3：不可用核心

这是我的程序，当图中存在一个循环时返回SAT，而当没有循环时返回UNSAT :( set-option：fixedpoint.engine datalog）（define-sort s（）Int）（declare-rel edge（ss））...

z3 proof z3py sat sat-solvers

回答 2 投票 1

使用Z3Py设置相同约束的不同运行时间

我正在使用z3py API编写Z3求解器的调度问题。除了解算器的运行时间在每个时间（有时是因子10/100）不同的事实之外，它的效果非常好。

python z3 z3py

回答 1 投票 1

Z3和策略：使用哪种策略？

所以我试图用z3解决调度问题。我有一组需要完成的工作和一组能够完成这些工作的资源。订购工作（总订单）和...

z3 smt z3py

回答 1 投票 1

如何按顺序打印z3求解器结果print（s.model（））？

假设我有一个10个变量的列表v = [Real（'v_％s'％（i + 1））for i in range（10）]我想为i添加一个简单的约束，如s = Solver（）在范围（10）中：s.add（v [i] == i）如果s.check（）...

python python-3.x z3 z3py

回答 1 投票 1

在Z3中获取战术应用的结果作为表达式

在C ++中是否有类似Z3py接口的as_expr（）。我试图得到将战术应用为z3表达式exp的结果，而不是类型apply_result。例如，在下面......

c++ z3 z3py

回答 1 投票 2

z3：解决八皇后拼图

我正在使用Z3解决八皇后拼图。我知道在这个问题上每个女王可以用一个整数表示。但是，当我通过以下两个整数代表女王时：从z3 ...

python z3 smt z3py

回答 1 投票 4

如何将算术表达式转换为Python算术函数？

假设我在Z3中进行了算术比较。遵循Z3py的语法，这是：e = z3.Int（'x'）<= 3是否有一种简单的方法（而不是繁琐的，逐案解析过程）来转换...

python z3 z3py

回答 2 投票 1

计算Z3量化公式中的变量数量

我正在尝试收集公式中的所有变量（Z3py中的量化公式）。一个小例子w，x，y，z = Bools（'wxy z'）fml = And（ForAll（x，ForAll（y，And（x，y））），ForAll（z，ForAll（w，And（z） ...

z3 z3py quantifiers

回答 1 投票 2

最大化z3中的最小值

我想在整数空间中找到满足某些属性的n维点（x1 ... xn），同时最大化x与m集合中任何元素之间的最小距离（预定义/ ...

z3 z3py

回答 1 投票 1

Z3：我应该使用Arrays，IntVectors还是别的什么？

我想知道我应该为我的z3应用程序使用什么数据类型。我的理解是，类整数数组结构的唯一选择是Array（IntSort（），IntSort（））和IntVector（）。 ...

z3 smt z3py

回答 1 投票 1

z3py 相关问题

最新问题