列表中的项目-理解，在z3模型中部分求值

、、、

但我不明白为什么x_17会出现在列表中。另一个结果是：[var = 0]from z3 import * data = [BitVec("x_{}".format(i), 8) for i in r

浏览 19提问于2020-06-04得票数 1

回答已采纳

1回答

是否可以通过C++接口检查变量是否具有确定性值

、

我注意到Z3可以从一些纸上做所有的事情。在我的项目中，我必须在SMT公式中搜索确定性变量。我所说的确定性，是指变量只能取一个int值才能使公式可满足。到目前为止，我能做的最好的事情就是多次调用solver.check()函数，以求取我感兴趣的每个变量的值。有没有更快的方法通过使用API来做到这一点？基本上，我想做所有的and和谓词抽象/投影。

浏览 0提问于2013-07-26得票数 0

1回答

Z3PY将整数转换为Python整数

、、

当我的公式被模型解出时，我可以通过调用Z3 ()-function把它打印出来。但是如何将模型输出保存为变量中的普通int呢？这样我就可以用它们了。我可以将它们转换成普通的int类型，这样我就可以在我的程序中的其他Python代码中使用它们了吗？我使用求解器的全部目的是将结果作为另一个Python程序的输入。所以我需要它能够处理它。

浏览 21提问于2021-01-27得票数 2

回答已采纳

1回答

Z3能检查包含递归函数的公式的可满足性吗？

、

我正在尝试一些涉及递归函数的示例。我已经尝试了下面的例子。 Z3可以检查包含递归函数的公式的可满足性，还是不能处理任何归纳事实？

浏览 0提问于2011-08-02得票数 4

回答已采纳

1回答

理解z3模型

、

6(ζ5(ν0), ζ5(ν1))],问题：我正在尝试理解Z3生成的模型。我有以下疑问。谢谢。

浏览 1提问于2012-10-15得票数 3

回答已采纳

1回答

R多部分公式在数学术语中意味着什么？

、、

在R公式包中，引入了像y ~ x1 + x2|I(x1^2)这样的多部分公式的概念。这个公式在数学上是什么意思？这与y ~ x1 + x2 + I(x1^2)或两个独立的y ~ x1 + x2和y ~ I(x1^2)有什么不同？

浏览 2提问于2010-12-08得票数 8

1回答

对于空模型，处理量化公式的正确方法是什么？

、、

我在玩未解释的排序和函数，无法完全理解量化的公式是如何与空模型交互的。这里(也是这里的)有一些简单的例子，有些让我感到困惑：一些看似等同于[∃v : v = v]的公式在某种程度

浏览 2提问于2013-03-01得票数 1

回答已采纳

1回答

添加z3约束，以便z3变量的值等于某个函数的返回值

、、

def fun(x): return "Hello" return "Bye"fromz3 import * s = Solver() 如果是r = Real('r

浏览 15提问于2021-12-12得票数 2

回答已采纳

1回答

列表理论是可决定的吗？

我想知道列表的z3理论是否是可决定的？似乎我们只能使用该理论来证明未被证实但未被证实的事实，所以我很好奇它是否真的是可判定的。谢谢你的帮助。

浏览 0提问于2012-06-07得票数 3

回答已采纳

1回答

对Z3 Python对象进行酸洗

、、

是否考虑在将来的版本中支持酸洗(或序列化) Z3对象？我目前正在尝试将Z3 Python API生成的模型打包到一个文件中，我得到了错误消息ctypes objects containing pointers cannot be pickled，我认为这意味着Python API仅仅是Z3 DLL的包装器。或者，有没有更好的方法将Z3 Python API生成的对象保存到文件<em

浏览 1提问于2013-01-30得票数 3

1回答

对清单理论的支持

我很好奇Z3是否有内置的列表类型？从C看来是这样的，但是我对输入SMTLIB / SMTLIB-2格式感兴趣，而不是使用C，所以我想知道Z3是否提供了这样的支持。谢谢。

浏览 4提问于2012-05-05得票数 2

1回答

在某些Z3绑定中是否有不支持声明排序的变通方法？

、

我不太熟悉Z3，但我必须用它来做一些项目。我正在使用，它有像SMT-LIB v2这样的文本接口，能够消除通用量词，但它还不支持declare-sort，而我的模型需要某种自定义的类型定义(我还不能想到如何在我的模型中只使用Int。)在这种情况下，如果我想使用绑定，我如何才能在我的模型中获得declare-sort的特性？在Z3<

浏览 3提问于2012-11-12得票数 4

回答已采纳

1回答

我在python中有一个整数列表，如下所示： myList = [97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110,, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57] 我想让Z3输出各种集合或数字列表，它们都是myList的成员……本质上，我想使用Z3来获取附加<em

浏览 11提问于2019-05-23得票数 0

1回答

如何有效地解决Z3中的理论组合

、

我试图解决一个涉及命题可满足性(带有量词)和线性算法的问题。下面是一个高度简化的问题，它抓住了我想要解决的问题的本质。有人能给我建议吗？我试着读一些像纳尔逊·奥本方法之类的东西，但是有很多不熟悉的符号，学习起来需要很长时间。另外，Z3允许用户调整这些配置吗？最后，我

浏览 2提问于2013-12-06得票数 2

回答已采纳

1回答

支持AUFBV？

Z3会支持AUFBV吗？16))(assert (= (select t #x0000) #x0000))不

浏览 0提问于2011-09-14得票数 2

回答已采纳

1回答

用于smt2文件的Java API推送和弹出

我已经生成了一个smt2文件，它已经被Z3 (4.3)通过Z3 Java成功读取(解析)。现在我想知道如何让Z3开始解决多个作用域(推送和弹出)的公式。smt2文件包含推送和弹出命令的列表。我知道您可以使用solver.push()和solver.pop()来实现这一点，但是这里的问题是作用域已经在文件中生成了，而我没有使用Z3内部API来创建这些公式和作用域。我只需要将整个smt2文件提供给Z3并执行多次求解(只有

浏览 2提问于2015-07-18得票数 1

1回答

Z3中的可判定sqrt函数

由于，Z3现在将在这个涉及平方根的简单模型上失败：(declare-fun y () Real)(assert (= y (sqrt x)))这将返回sat和Z3 4.4.1，而unknown返回主。如果我将问题定义更改为使用由Nikolaj在中定义的，那么Z3母版将返回sat。使用is_s

浏览 5提问于2016-06-23得票数 1

回答已采纳

2回答

在非线性求解器中，什么会影响求解器时间与NLP函数求值？

、、、、

我在理解非线性优化中的性能如何受到求解器引擎接口的特定方式的影响方面有一些困难。我们有一个优化模型，它的第一个版本是用GAMS编写的。IPOPT (一种常见的FOOS非线性求解器引擎)在IPOPT (w/o函数求值)中返回1.4 CPU秒的每次优化的执行时间，在函数求值中返回0.2

浏览 61提问于2016-11-25得票数 0

1回答

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

、、、

我正在使用Z3的Python绑定，我很好奇局部模式是否会加速我的模型。然而，在Python中似乎没有这样做的方法。(set_param(...)似乎没有它的参数)额外的问题:局部模式真的对我有什么好处吗？我正在模拟数组中的计算机内存，并希望Z3忽略从未引用过

浏览 1提问于2018-09-13得票数 0

回答已采纳

2回答

如何使z3 (Python) SAT解偏向于一个标准，例如“更愿意”有更多否定的文字。

、、、、

在Z3 (Python)中，有什么方法可以使SAT搜索偏向于“标准”吗？一个例子:我希望Z3获得一个模型，但不是任何模型:如果可能的话，，，给我一个有大量否定文字的模型。因此，例如，如果我们必须搜索A or B，可能的模型是[A = True, B = True]，但是我宁愿收到模型[A = True, B = False]或模型[A = False, B = True]，因为它

浏览 13提问于2022-01-19得票数 2

回答已采纳

点击加载更多