2回答
我正在通过它的.Net Api使用Z3。我构建的模型有相当多的约束条件。到目前为止，我一直在使用各自的Z3命令(在.Net Api中)逐行构建我的模型。但现在模型的大小增加了，创建模型所需的时间非常可观。我在想，有没有一种方法可以将模型构建为文本文件，并一次性将完成的模型输入到Z3求解器中？
浏览 22提问于2020-09-22得票数 0
1回答
我正在使用Z3来生成一个优化的时间表。在检查可满足性之后，生成模型并将其存储到文本文件中。但是，我注意到Z3并没有按任何顺序排列模型中的值。是否有办法使Z3按升序排列它们？
浏览 0提问于2018-12-27得票数 1
回答已采纳
使用Yices使用归纳数据类型进行计算的一个简单示例是： c2define x1::T)(assert (/= x1 x2))相应的输出是：(= x1 c1)此示例使用以下代码使用sat (define-fun x2 () T (c3 false))
(define-fun x1 () T c1)
浏览 1提问于2013-12-01得票数 1
回答已采纳
1回答
我使用Z3检查数组属性片段中公式的可满足性。Z3返回的数组变量的模型通常使用其他if表达式、if-then-else案例分析等来表示。我想以某种方式解析Z3输出的模型并创建数组，它显式地满足输入的SMT-LIB公式。例如，我希望能够以某种方式始终将Z3输出的模型简化为以下形式： 1 -> 3 else -> 6是否有一些简单的方法来遍历模型
浏览 1提问于2013-07-03得票数 1
我在玩未解释的排序和函数，无法完全理解量化的公式是如何与空模型交互的。这里(也是这里的)有一些简单的例子，有些让我感到困惑：
一些看似等同于[∃v : v = v]的公式在某种程度上阻止了z3生成空模型。例如，如果我们将这样的公式添加到一个求解器中，然后尝试创建类似于allsat过程的东西(添加越来越多的约束以排除越来越多的模型</
浏览 2提问于2013-03-01得票数 1
回答已采纳
1回答
Z3可以输出模型，当输入满足时，我们可以提取值。另一种看待这个问题的方法是:当z3证明方程返回false时，我们可以打印一个组合，从而得到unsat (false)值吗？
浏览 1提问于2017-05-19得票数 0
1回答
我正在尝试优化从我的模型中生成的z3 python输入。我能够在15k约束的模型上运行它(200个状态)，然后z3停止在合理的时间内完成(<10分钟)。是否有一种方法来优化从我的模型生成的约束？
浏览 3提问于2013-01-08得票数 3
我正在使用SMTLIB2语言，通过SMTLIB求解器来解决我在逻辑QF_BV中表达的问题。我希望在非饱和核心生成时考虑的断言已经使用(assert (! (EXPR) :named NAME))构造指定了。不出所料，Z3给了我一个unsat。然而，Z3似乎总是丢弃由所有命名断言组成的“微不足道的”unsat core。
我知道存在我命名的
浏览 3提问于2012-02-28得票数 6
回答已采纳
克莱因集团的产品表如下：使用以下Z3 SMT-LIB代码可以获得Klein的表示：(declare-sort S) )(eval (f a b))(eval (f (f (f a
浏览 4提问于2013-11-21得票数 0
回答已采纳
2回答
我在JAVA中使用Z3已经有两年了。出于某种原因，我总是以字符串的形式生成SMTLib2代码，然后使用parseSMTLib2String构建相应的Z3 Expr。据我所知，每次用这个方法输入相同的输入两次，我总是得到相同的模型。现在发生
浏览 2提问于2017-12-15得票数 2
回答已采纳
1回答
上下文:我使用z3对有界java程序验证进行了研究。我想得到一个线性化问题的优化模型。一种标准的方法是递增地搜索模型，直到找到未满足条件的情况。但是性能似乎是个问题，而且引入JNI破坏了代码的可移植性，JNI将z3 c/c++ api集成到我的工具中。
现在我想在java方法的所有输入上添加约束。我使用数量数组(我使用数组理论对堆进行建模)。然而，对于可满足的问题，z3总是立即返回“未知”。似乎生成模型是不
浏览 5提问于2012-07-13得票数 2
回答已采纳
1回答
在中，我给出了一个函数公理化，并要求Z3提供一个模型。但是，因为解决带有量词的问题在一般情况下是无法确定的，所以Z3会超时。ABC) (y ABC)) (=> (and (= x int) (= y int)) (= (f x y) int))))(get-model) in
浏览 1提问于2016-05-29得票数 0
1回答
在Z3教程的13.2.3节中，有一个很好的例子，说明了如何在处理注入性公理化时减少必须实例化的模式数量。在这个例子中，必须声明为内射的函数f接受类型A的对象作为输入，并返回类型B的对象。我有一个SMT问题(FOL+EUF)，在这个问题上Z3似乎没有终止，我正在尝试找出原因。我有一个函数f:A->A，我断言它是内射的。问题会不会是f的domain和codomain重合？
浏览 1提问于2012-12-14得票数 3
回答已采纳
我使用Z3 .Net API开发了一个模型。该程序运行良好。但当我增加输入大小(即模型大小)时，程序会运行很长时间，然后结束，并给出以下消息：
"Unhandled Exception: OutOfMemoryException."
浏览 3提问于2012-03-29得票数 2
回答已采纳
在使用SMTLIBv2输入格式和Z3模式时，我遇到了一个问题:我一直使用以下输入获得“未知”的结果：(declare-fun path整个想法可以追溯到Milicevic和Kugler的一篇文章，在文章中，他们使用Z3 2.0和.net API以这种方式表示模型检查问题。：我在Z3 X (10.8.3)上使用了MacOS版本4.3.2，上面提到的
浏览 4提问于2013-04-04得票数 4
在使用z3优化求解器时，需要模型的边界，特别是约束条件复杂。我可以在Z3 python api中找到函数upper和lower，但不能用于Java api。您能举一些例子来说明如何在Z3 java api中获取模型边界吗？
浏览 26提问于2020-08-16得票数 0
回答已采纳
z3 -smt2 <filename>只输出'sat‘或'unsat’。如果满足约束，我希望Z3输出模型，如果不满足，则输出unsat核心。我应该使用哪些Z3选项？
浏览 8提问于2015-12-18得票数 0
回答已采纳
云服务器
ICP备案
云直播
对象存储
实时音视频
腾讯云开发者
