我有以下程序，它将简单的key = value约束应用于从字符串到字符串的函数： from z3 import *s = Solver()print(s.check())
print(s.model()) 模型<
浏览 21提问于2021-11-10得票数 0
回答已采纳
1回答
我正在使用z3py推断一个函数，如下所示在断言一组约束之后，如：[(a1,b1) -> c1,(a3,b3) -> c3,else -> 2]k = Int(&#
浏览 2提问于2015-06-29得票数 3
回答已采纳
我正在尝试一些涉及递归函数的示例。我已经尝试了下面的例子。
Z3可以检查包含递归函数的公式的可满足性，还是不能处理任何归纳事实？
浏览 0提问于2011-08-02得票数 4
回答已采纳
1回答
我想把一阶理论应用到微软公司开发的一种SMT解决方案Z3中.这个理论包含两个对象( obj1和obj2 )，一个函数移动，它接受一个对象并返回一个动作，一个一个位置的谓词出现，它以一个动作作为参数。为了证明这一点，我将其翻译为Z3，如下所示：(declare-sort Action 0)
问题是，这提供了以下输出：(((
浏览 1提问于2012-10-29得票数 2
回答已采纳
对于第一组约束，一切都很正常，我可以将变量的声明等直接放入smtlib2字符串中。对于smtlib字符串，解析器接口提供了检索此信息的函数，例如"Z3_get_smtlib_num_decls“和"Z3_get_smtlib_decl”。但是，它们不适用于smtlib2字符串。有一种使用模型的变通方法。对于此变通方法，Z3必须返回包含每个已声明变量的模型
浏览 2提问于2013-05-20得票数 1
回答已采纳
2回答
我在JAVA中使用Z3已经有两年了。出于某种原因，我总是以字符串的形式生成SMTLib2代码，然后使用parseSMTLib2String构建相应的Z3 Expr。基本上，我不会生成字符串，然后解析它，但是我让Z3完成构建Z3 Expr的工作。
现在发生的情况是，我得到了不同的模型，而我已经检查了求解器是否确实
浏览 2提问于2017-12-15得票数 2
回答已采纳
我想知道有什么方法可以在不获取模型的情况下为求解器中现有的声明变量添加一些新的约束。(declare-fun k!647 () (_ BitVec 8))我怎么才能得到他们一般声明的名字呢？
情况是，我想为现有的“变量？”添加更多的约束。在约束中，并一起求解它们。然后形成新的约束，这对于求解器也是正确的</em
浏览 18提问于2019-07-08得票数 0
继续从我的中继续，如果您按照以下方式定义一个集合：s = Solver()s.add(string_set(StringVal('foo')))s.add(string_set(
浏览 1提问于2021-12-07得票数 0
回答已采纳
1回答
我试图使用Z3来推断子字符串，但遇到了一些非直观的行为。当被要求确定'xy‘是否出现在'xy’中时，Z3返回'sat‘，但当询问'x’在'x‘中还是'x’在'xy‘中时，它返回'unknown’。strings are _x_ and _y_(declare-fun _y_ () Char)
(asse
浏览 0提问于2011-08-20得票数 9
回答已采纳
1回答
在Z3教程的13.2.3节中，有一个很好的例子，说明了如何在处理注入性公理化时减少必须实例化的模式数量。在这个例子中，必须声明为内射的函数f接受类型A的对象作为输入，并返回类型B的对象。据我所知，排序A和B是分离的。
我有一个SMT问题(FOL+EUF)，在这个问题上Z3似乎没有终止，我正在尝试找出原因。我有一个函数f:A-&g
浏览 1提问于2012-12-14得票数 3
回答已采纳
我的模型的大部分可以用标准的SMTLIB表示，但其中的一部分需要用通用编程语言来实现，这些语言具有字符串处理、关联数组等结构。--为澄清而编辑--
我希望提供约束的实现(作为函数指针或等效函数)，以
浏览 4提问于2016-07-09得票数 1
1回答
我想知道列表的z3理论是否是可决定的？似乎我们只能使用该理论来证明未被证实但未被证实的事实，所以我很好奇它是否真的是可判定的。谢谢你的帮助。
浏览 0提问于2012-06-07得票数 3
回答已采纳
带有量词的公式包含trans函数的声明。Z3成功找到模型并将其打印出来。但它也会打印trans!1!4464、trans!7!4463等函数的模型。它们不会在模型中的任何地方使用。那是什么？下面是查询：，下面是Z3的输出-
浏览 0提问于2012-03-09得票数 1
回答已采纳
1回答
在中，我给出了一个函数公理化，并要求Z3提供一个模型。但是，因为解决带有量词的问题在一般情况下是无法确定的，所以Z3会超时。这里是一个修改的版本，其中"int“的情况被建模为单个值：(declare-fun f (ABC ABC)，所以Z3很快就给出了答案：(model
(defin
浏览 1提问于2016-05-29得票数 0
1回答
我正在使用Z3来生成一个优化的时间表。在检查可满足性之后，生成模型并将其存储到文本文件中。但是，我注意到Z3并没有按任何顺序排列模型中的值。是否有办法使Z3按升序排列它们？这是它生成的变量值之一。有什么办法让这个提升吗？
浏览 0提问于2018-12-27得票数 1
回答已采纳
我正在编写一些代码，使用Z3字符串计算ACL中的权限。到目前为止，对于SMT2，这是相对容易的。一个例子。z3 c++绑定时，我还不知道如何将Z3：：函数插入到这个绑定中。} acl_eval();}
在C++绑定中，wrt函数就是这样完成的吗？虽然由smt2绑定生成的
浏览 7提问于2020-02-13得票数 1
回答已采纳
如何通过java在z3中生成string？对于整数，有ctx.mkInt(int a)生成值为a的IntExpr，ctx.mkIntConst("a")生成名称为"a“的IntExpr。但是，对于字符串，我只能找到ctx.mkString("a")，它只是一个值为"a“的SeqExpr，类似于ctx.mkInt。所以我想要的</em
浏览 4提问于2020-07-29得票数 0
回答已采纳
(以及函数)的信息。是否还有更有效的方法来解决这个问题，并使z3保存数据类型和函数以供将来的断言和声明使用？编辑：
例如，在我的实际案例中，文件"func.smt“在函数和数据类型之间总共有54个声明(有些非常复杂)。"spec.smt“文件几乎没有声明和断言。最后，我有一个文件，其中有许多断言，我必须一点一点地阅读，并生成一
浏览 4提问于2019-11-30得票数 0
回答已采纳
1回答
下面是简单的代码：a, b, c, d = Ints('a b c d')s.add(a>0)s.add(c>04, b = 8, mod0 = [else -> 0]]
这在4.8.12版中。div0和mod0线意味着什么？
浏览 1提问于2021-09-23得票数 3
回答已采纳
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
云直播活动推荐
腾讯云开发者
