我想知道有什么方法可以在不获取模型的情况下为求解器中现有的声明变量添加一些新的约束。(declare-fun k!647 () (_ BitVec 8))我怎么才能得到他们一般声明的名字呢？
情况是，我想为现有的“变量？”添加更多的约束</
浏览 18提问于2019-07-08得票数 0
不幸的是，我没有足够的声誉来评论其他问题的答案。所以我必须开始一个新的问题。
从本质上讲，我遇到了与所描述的相同的问题。我想使用Z3进行增量求解。为了将约束放入Z3，我使用了smtlib2字符串。对于第一组约束，一切都很正常，我可以将变量的声明等直接放入smtlib2字符串中。当以增量方式添加
浏览 2提问于2013-05-20得票数 1
回答已采纳
我使用z3作为我的应用程序中的底层约束解决程序，通过它的C++接口。我声明一个z3上下文为一个类的成员，这个类用于解决许多独立的约束集。事情是这样的:在求解一个约束集时，我声明z3‘解’器‘，但是在解决许多独立问题时，z3 'context’是同一
浏览 3提问于2014-04-12得票数 4
回答已采纳
1回答
与类似(但有点相反)，我do希望在可能的情况下公开随机性。也就是说，我希望连续两个查询提供不同的结果。这有可能吗？这是我的代码：{ context ctx; }
solver.pop()
浏览 0提问于2020-06-01得票数 0
回答已采纳
我对MAX-SAT很感兴趣，并希望Z3能将其作为内置功能。在不久的将来有没有这样做的计划？最后，maxsat示例中<em
浏览 5提问于2012-05-22得票数 3
由于该算法需要多次求解原约束集的子集，所以我决定在z3 c++接口中使用push/pop函数(在nlsat解算器中检查(假设)不工作)。选择器变量用于暗示添加/删除约束。但当我解决约束集时，我遇到了一个问题。z3能够告诉我，整个约束集在不到1分钟的时间内是unsat。但是，当检查原始约束集的子集时，它不会给出
浏览 3提问于2014-04-30得票数 1
回答已采纳
如何使用Z3 python编写与此代码相当的代码？a Int) (b Int)) Int(get-model)(我可以声明mym
浏览 1提问于2021-08-06得票数 0
回答已采纳
1回答
我是Z3的新手，在这里和谷歌上都在搜索我的问题的答案。不幸的是，我没有成功。现在，我想提取模型定义的函数d的某些值，例如d(0,0)。下面的语句工作
浏览 0提问于2012-07-25得票数 10
回答已采纳
2回答
假设我有约束：[x > 2, y > 1, x < 10]，并且我想在y==1时添加条件x%4 == 0，并获得所有结果，我该如何在Z3中做到这一点呢？我为已求解的结果添加了阻塞约束，并对其进行迭代以获得所有可能的y == 1结果，但我发现它只是忽略了值y == 1。 下面是我用来测试的代码，它没有产生任何解决方案。
浏览 23提问于2020-09-13得票数 0
回答已采纳
在C++中，z3::context context生成一个新context.Through这个具有新上下文的Z3表达式可以被创建为context.bv_const(variable_name, 16)如何使用z3 python api实现相同的行为呢？
浏览 38提问于2021-01-03得票数 0
回答已采纳
1回答
回到过去的日子(即。去年)，我们曾经能够使用理论插件作为一种实现自定义简化器的方法。Z3文档甚至包含了。
我的问题很简单:有没有办法用Z3 4.x实现同样的目标？特别是，我感兴趣的是一种为Z3提供基本术语的外部计算评估的方法。
浏览 2提问于2012-12-10得票数 2
回答已采纳
1回答
distinct函数的Z3(declare-const b S)允许约束变量集(此处为a和b)，以便集合中的所有变量必须采用不同的值，我的问题是：是否也可以强迫变量获得唯一值，而不显式地引用它应该与之不同的变量集？有点像(declare-unique-const b S)
浏览 4提问于2013-02-19得票数 0
回答已采纳
我遇到了一个问题，即嵌入在更大系统中的z3代码尽管超时时间较长，但无法找到解决特定约束集(通过C++接口添加)的解决方案。当我将约束转储到文件(在求解器上使用to_smt2()方法，在调用check()之前)，并通过独立的z3可执行文件运行该文件时，它将在大约4秒内解决系统问题(返回sat)。是否有一种方法可以使用C++接口将该文件读入嵌入式解决程序，替换现<em
浏览 2提问于2017-01-27得票数 1
回答已采纳
1回答
虽然我对SystemVerilog约束语言的简单性和灵活性有任何怀疑，但我已经决定使用Z3或Gecode来完成我正在做的工作，主要是因为它们都处于麻省理工学院的许可之下。然而，它的编程模型似乎有点简单，它确实为创建自己类型的变量提供了一种方法。因此，我也许可以在C++位集上创建某种包装器，类似于IntVar如何包装32位整数。然而，这将缺乏执行基于乘法的约束的能力
浏览 5提问于2020-01-27得票数 0
回答已采纳
1回答
我实际上使用Z3py来调度解决问题，我试图表示一个2处理器系统，其中必须完成4个不同执行时间的进程。但是现在我不知道如何表示我的处理器来添加我需要的3个规则:单一性(每个子进程必须完成1次，并且只有1个处理器完成1次)检查到达(进程的第一部分在到达之前不能被处理)和顺序(进程的每个部分必须在先例之后处理)，所以我想用数组来表示我的2个处理器，并使用这种声明：
P = Array('P&#x
浏览 0提问于2013-05-16得票数 1
回答已采纳
我想用C++应用程序接口在Z3中进行增量求解。
char *decl = "(declare-const p0 Bool)";so
浏览 2提问于2016-10-06得票数 2
我试着用Cygwin和JDK 1.7.0在Win XP上编译Scala^Z3，但是它没有像预期的那样工作。我做了以下工作：-使用SBT 0.7.4 -使用github的当前Scala^Z3版本-使用Cygwin及其gcc -使用JDK 1.7.0 (javac)\psuter-ScalaZ3-35cb691\src\c/z3_Z3Wrap
浏览 2提问于2011-09-12得票数 3
回答已采纳
2回答
让我们看一下以下问题：f(a, b, c, x, y, z)是一个布尔函数，其中a、b、c、x、y和z是布尔值，f的输出是布尔值。F的定义由许多and/或/nor运算符组成。我希望找到一组包含三个布尔值x0、y0和z0的值，以便： f(0, 0, 0, x0, y0, z0) = 0 ANDf(0, 1, 0,一种简单的方法是定义3个布尔变量x，y，z，然后重复定义函数f 8次。但是，f由复杂的<
浏览 39提问于2020-12-16得票数 0
我想在SMT v2.6中对通用数据类型的行为进行建模。我使用Z3作为约束求解器。我根据以下列方式将一个泛型列表建模为参数化数据类型：我希望列表在数据类型方面是通用的稍后，我想以下列方式声明常量：(declare-const y (MyList Real))
浏览 2提问于2017-12-03得票数 3
回答已采纳
1回答
我正在使用Python中的Z3来生成解决溶解难题的解决方案。我之前没有使用SAT/SMT解决程序或Z3的经验，甚至我的Python也还处于pidgin级别。所以请温柔点。在我的方法中，我有两个列表xs和ys。我从其他约束中了解到，在这两个列表中，最多有一个条目是True，其他所有条目都是假的。每个列表要么为零，要么<e
浏览 1提问于2019-03-09得票数 1
回答已采纳
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
云直播活动推荐
腾讯云开发者
