我似乎无法在Max OS X Mountain Lion上安装Z3（4.3.1）（正确安装了Xcode/命令行工具）。问题是autconf没有随Xcode及其命令行工具一起安装/提供 我需要从源代码下载并安装autoconf/automake等吗 是的，我们需要autoconf来安装Z3 v4.3.1。 下一版本将不具有此依赖项。 同时，我们可以在不使用autoconf的情况下构建不稳定的（正在进行的工作）分支。 是编译不稳定分支的指令。 同样的指令也可用于编译contrib分支。该分支本质上是

我正在使用Codeplex最新的z3主代码，标记为v4.3.1 我想要一个像prove这样的函数，它有一个有用的返回值并且不打印。所以，我写下了似乎显而易见的东西： def prove2(claim): s = Solver() s.add(Not(claim)) if s.check() == unsat: return True, [] return False, s.model() 但是，此代码的运行速度明显低于默认的prove函数 src

ve2的作用是什么？向后推（mk_和（ve））；do？删除它。此外，您需要将s.add（mk_或（ve2））；更改为s.add（mk_或（ve）） 不确定要在那里构建什么类型的表达式。您需要类似于x0！=1 | | x1！=7 | |……的内容

我有一个对变量进行排序的程序，我试图用Z3检查它的有效性，但我有一个代码段，其中变量被交换，我不知道如何用SMT语法建模。以下是原始代码段： if (x > y) { temp = x; x = y; y = temp; } 关于SMT，我已经写了一个断言，但我想这并不完全正确： (declare-fun x () Int) (declare-fun y () Int) (declare-fun temp () Int) (assert (=> (> s1 s2

在阅读Z3的快速LCF样式校对重构时，我了解到Z3的语言中有像+或forall这样的解释函数。我想也有一些未被理解的函数。这两者之间有什么区别？它们是有名称和签名但没有定义的函数，请参见。它们是有名称和签名但没有定义的函数，请参见

我想用Z3解决以下示例： input = 0 if input < 5: var v1 = 5 input += v1 input *= v1 if input > 5: return True else: return False 如何将5添加到输入和多个输入中，以便稍后检查其是否大于5？建模此类命令式程序的标准技术是将其转换为SSA（静态单赋值）形式，基本上是通过在每个位置复制每个赋值变量。有关详细信息，请参阅： 基于这一想法，我将为您

是否有Z3的INI选项的详细文档。我必须做一个尝试和错误的方法来找出我的QF_BV问题的最佳选择。我仍然不确定是否有更多的选项可以让我的z3跑得更快。如果有人能指出INI选项的任何现有详细解释，那就太好了 谢谢。我们目前正在重新构造Z3，并且正在远离这种方法：一个具有“千”个参数的解算器。 我们正在将Z3转变为一种更加模块化和灵活的方法，用于组合求解器和指定策略。 您可以在以下内容中找到有关此新方法的更多信息 关于INI选项，其中一些选项已被弃用，之所以存在，是因为我们尚未完成到新方法的转换。

我正在尝试使用函数Z3_benchmark_to_smtlib_string（）。以下是我使用的参数： Z3_benchmark_to_smtlib_string( ctx, /* this one is valid */ "test", /* this one is random, I don't understand it */ "QF_UFBV",

我有一些简单的约束，涉及z3中实数的乘法，它们产生unknown。问题似乎是它们被包装在一个数据类型中，因为未包装的版本会产生sat 以下是一个简化的案例： (declare-datatypes () ((T (NUM (n Real))))) (declare-const a T) (declare-const b T) (declare-const c T) (assert (is-NUM a)) (assert (is-NUM b)) (assert (is-NUM c)) (ass

我正在使用量化的位向量公式和位向量算法进行基准测试。基准测试使用Z34.3.0在Linux 64位中生成一个分段错误。我认为问题的出现是因为对平等的过渡使用 ... (assert (= (bvadd (capacity this) (_ bv1 5)) (EAO.length (elements this)) )) (assert (= (EAO.length (elements this)) (IKAO.length (heap this)) )) 有关完整的基准可在此处找到： 感谢您报

有没有办法将简化应用于z3中定义的未解释的函数，而不是目标和子目标 我有以下z3代码： 我得到以下输出： 事实证明，通过对f的定义应用重写规则，我们可以得到 通过以下推导，f等于第二个参数（x！2）： (f!8 (k!7 x!1) (k!6 x!2)) = (f!8 false (k!6 x!2)) = (f!8 false x!2) =(x!2) 有没有办法让z3自动生成以下定义 谢谢你的帮助。 当做 Oswaldo.一个选项是要求Z3计算表达式（f x y），其中x和y是新的

我试图理解如何使用解eq，我希望Z3能解决这个问题 (declare-const mem (Array Int Int)) (declare-const adr_a Int) (declare-const a Int) (assert (= (select mem adr_a) a)) (assert (<= 0 (select mem adr_a))) (apply solve-eqs) （声明常量mem（数组Int）） （声明常数adr_为整数） （声明常量为Int） （断言（（选择

我想创建一个表达式，它选择给定表达式集中的一个。给定一个表达式数组 Expr[] availableExprs = ...; 对于静态已知长度，我希望Z3选择其中任何一个（如switch语句）。如果问题是SAT，我需要一种方法来找出在模型中选择了哪一个（它在数组中的索引） 最快的编码方式是什么 到目前为止，我考虑了以下方法： 将整数限制为[0，arrayLength），并使用ITE选择其中一个表达式。模型允许我提取此整数。不幸的是，这将整数理论引入了模型（以前根本不使用整数） 为每个可能的选择

我在试用Z3中的PDR引擎，我不确定使用哪个版本的Z3 git的“官方”主分支似乎有效，但日期为2012年11月。我相信从那以后情况有所改善。另一方面，不稳定分支“可能包含不稳定和/或未测试的代码”，这似乎是正确的 发动机的最新“稳定”版本是什么 比如说 (declare-rel R (Real Real)) (declare-var x Real) (declare-var y Real) (rule (=> (and (= x 0) (= y 0)) (R x y)) )

我正在为Z3使用Python绑定，并尝试创建一个属性为函数的Z3数据类型。例如，我可能会执行以下操作： Foo = Datatype('Foo') Foo.declare('foo', [('my_function', Function('f', IntSort(), BoolSort()))]) Foo.create() 这是一种尝试，创建一个带有属性my_function的数据类型Foo，在这里我可以调用my_function x（如果x是Foo类型的变量），以便将一些函数从int导出到b

我很困惑，很难理解Z3 fixedpoint引擎的两种不同输入格式是如何关联的。简短的例子：假设我想证明负数的存在。我声明了一个函数，对于非负数返回1，对于负数返回0，然后如果存在函数返回0的参数，则要求解算器失败。但有一个限制：当至少存在一个负数时，我希望解算器响应sat，如果所有数字都是非负数，则响应unsat 使用declare rel和query格式非常简单： (declare-rel f (Int Int)) (declare-rel fail ()) (declare-var n I

如何在使用Z3_parse_smtlib2_文件API读取基准时使用（push）和（pop）。如何使用Z3_parse_smtlib2_文件API获得（assert（not（=o2_s o2_I））和（assert（not（=o1_s o1_I））约束的结果。我仅在使用C中的Z3_parse_smtlib2_文件API读取基准测试时才获得（assert（not（=o1_s o1_I））的结果 (declare-fun i_s () Int) (declare-fun t_s () Int) (d

一阶逻辑的有效命题（EPR）片段通常定义为∃十,。∀Y.Φ（X，Y），其中X和Y是（可能是空的）变量序列。量化顺序是否正确，即∃*∀*，与EPR的可判定性有关？如果量化顺序被切换，我们会失去可判定性吗 特别是，我感兴趣的是在可判定逻辑中捕获集合一元绑定操作的语义。给定类型为T1的元素的集S1（即S1具有类型T1集），以及类型为T1->T2集的函数f，set monad的绑定操作通过在S1的每个元素上应用f，构造类型为T2集的新集S2，以及合并结果集。此行为可在以下SMT-LIB代码/公式中捕获：

在unix上，我尝试使用一个prove，它使用Z3。我下载并构建了源代码（4.1.2；尽管z3-version显示了4.2）。AProVE将z3与-m选项一起使用，但4.2不支持-m。根据AProVE developers-m在Z34.0中可用 如何获取支持-m的z3源文件？或者，我的问题有简单的解决方法吗？默认情况下启用模型生成。我们不再需要提供选项-m。 如果您不能更改一个prove，那么可以为Z3创建一个包装器，在调用Z3之前删除选项-m。另一个选项是破解Z3源代码中的文件shell\ma

我有以下计划： ;;; Sets (declare-fun lock_0 (Int) Bool) (declare-fun lock_1 (Int) Bool) (declare-fun lock_2 (Int) Bool) (declare-fun lock_3 (Int) Bool) ;;; verify if sets lock_0 and lock_1 haven't elements in common (assert (exists ((x Int)) (=> (lock_0

这是我的简单编码。我想得到表示所有这些约束的最终布尔CNF。Z3解算器中是否有任何选项可以获得最终的布尔CNF x = Int('x') y = Int('y') c1 = And(x >= 1, x <= 10) c2 = And(y >= 1, y <= 10) c3 = Distinct(x,y) s = Solver() s.add(c1 , c2 , c3) # I need the final Boolean CNF formula from Z3 sol

我正在使用Z3（2012-12-21 git版本，最新的“主”版本）检查工具的可移植性，因此尝试在Sparc64上编译Z3。我不得不摆弄src/util/hwf.cpp，这样它就可以将Sparc64而不仅仅是IA64视为缺少SIMD内部函数和emmintrin.h。汇编成功了 不幸的是，由于prime\u generator:：prime\u generator（）。我不知道为什么 Program received signal SIGBUS, Bus error. 0x009b1dac in

当对不同的变量和公式调用Z3py的Exists函数时，我得到了完全相同的结果。这是某种Python问题还是Z3在这里被破坏了？如何修复？以下示例说明了该问题： from z3 import * a, a0, a1, b, b0, b1 = Ints('a a0 a1 b b0 b1') x, y = Bools('x y') s = Solver() formula = Implies(x, And(a>0,b1<0)) substitution1 = substitute(form

我试图在我的上下文中使用“FiniteDomainSort”，但当我将其交给解算器时，它会抛出一些异常 备注： *我按照建议使用mknumeric *使用z3-4.3.0 x64（win）和z3-4.3.2 x64（ubuntu）进行测试 *在同一示例中使用IntSort时运行良好 例如： using System; using System.Collections.Generic; using Microsoft.Z3; namespace NS { class CL { public sta

我尝试使用位向量在模型值中获得随机结果，如de Moura建议的，但随后使用Z3Py而不是SMTLIB。我把他的例子翻译成： from z3 import * s = Solver() x = BitVec('x', 16) set_option('auto_config', False) set_option('smt.phase_selection',5) s.add(ULT(x,100)) s.check() s.model() s.check() s.model() 然而，结果似乎总是

我试图用两个整数来表示一个实数，用它们作为实数的分子和分母。我编写了以下程序： (declare-const a Int) (declare-const b Int) (declare-const f Real) (assert (= f (/ a b))) (assert (= f 0.5)) (assert (> b 2)) (assert (> b a)) (check-sat) (get-model) 程序返回SAT结果如下： sat (model (define

有一种用于调试Z3跟踪的工具，称为“Z3 Axiom Profiler”。我发现，这似乎是axiom剖析器，已经三年了。从这些VCC源构建是获取探查器的正确方法，还是有更新的版本？这是最新的版本。您可以在二进制VCC发行版中找到一个可执行文件。我指导了一名学生（Frederik Rothenberger），他对以前的axiom profiler进行了各种改进。您可能希望尝试新版本，其中包括许多错误修复和实例化图的新可视化 较新版本可在以下位置获得： 弗雷德里克的项目报告在这里，以防万一： 如

我正在努力改进我的Z3代码的计时。我观察到，无论我的机器有多少个内核，Z3总是只使用一个内核。有没有一种方法可以让Z3使用所有的内核，因为它肯定会提高性能？可能重复的请参见

我们可以在z3中以增量方式使用MaxSMT解算器（优化）的先前解决方案吗？此外，是否有任何方法可以在优化器上打印出软断言？如果您询问是否在技术上可以使用MaxSMT问题增量运行z3或OptiMathSAT，则答案是是。（使用API） 在执行检查sat时，具有相同id的所有软子句都被视为同一MaxSMT目标的一部分。本质上，OMT解算器惰性地评估MaxSMT目标的相关软子句集。这适用于z3和OptiMathSAT 在迭代过程的早期阶段找到的最优解可能与后期阶段的最优解相差很远 在处理MaxSMT问

我正在尝试验证003-23-80.cnf是否可以使用Z3Prover。我已经用Minisat验证过它是可以满足的，但是它花费了大约2小时和500 MB的内存 在bash中，我写道： z3-wcnf-st-T:9000-内存：500003-23-80.cnf 我相信这会将时间延长到9000秒，将内存延长到500兆字节，但我的输出是不安全的： 我做错了什么？不考虑内存/时间等。；如果miniat说这个基准是sat，而z3说它是unsat，那么其中一个就有一个bug！根据实际需要的是哪一个，您应该将

我知道带乘法的整数理论一般是不可判定的。然而，在某些情况下，Z3确实返回一个模型。我很想知道这是怎么做到的。它是否与实数上非线性算术的新决策过程有关？Z3返回乘法查询模型的具体实例（如：有限模下的整数等）有哪些？非常感谢您的帮助。是的，非线性整数算法的决策问题是不可判定的。 我们可以用非线性整数算法对图灵机的停止问题进行编码。 我强烈推荐这本漂亮的书给任何对这个问题感兴趣的人 请注意，如果公式有解，我们总是可以用蛮力找到它。也就是说，我们不断枚举所有可能的赋值，并测试它们是否满足公式。这与试图通

我想知道是否可以使用命名表达式来实现软约束，而不显式地使用手动“跟踪”变量 在消息中，莱昂纳多解释了如何使用辅助布尔以手动方式实现软约束 在以下信息中： 莱昂纳多说，命名表达式本质上被视为模型查找的含义 如上面第一条消息所述，使用手动跟踪相当麻烦，因为它需要对解算器进行多次调用（事实上，在最坏的情况下可能需要调用2^n，以便在我们有n软约束时获得尽可能多的软约束满足）。 有没有可能将这两种思想结合起来，让Z3以更简单的方式实现软约束？基于这两条消息中的想法，我天真地尝试了以下方法： (set

我想通过给z3一个断言来比较两种不同宽度的浮点数。 例如，我想比较IEEE 32位和IEEE 64位浮点数 我的尝试如下所示： (set-logic QF_FPA) (set-option :produce-models true) (declare-fun x_64 () (_ FP 11 53)) (declare-fun x_32 () (_ FP 8 24)) (assert (== ((_ asFloat 11 53) roundNearestTiesToEven x_64 ) x_6

我正试图使用Why3的Z3后端来检索模型，然后这些模型可以用来派生出程序中出现错误的测试用例。然而，Z3版本4.3.2似乎无法回答sat的任何Why3目标。看起来Why3使用的一些公理化定义不知何故混淆了Z3。例如，下面的例子是Why3生成的一小部分 (declare-fun abs1 (Int) Int) ;; abs_def (assert (forall ((x Int)) (ite (<= 0 x) (= (abs1 x) x) (= (abs1 x) (- x)))))

在对多项式不等式进行推理时，Z3似乎必须首先将多项式转换为单项式形式。我想知道解算器中是否有一个设置，可以让我定义多项式要转换成的单项式阶数 我使用的是z3py界面，我无法通过在线搜索找到它 否，Z3没有此设置

我在Z3中尝试了上述代码，但Z3无法回答。您能告诉我哪里出错了吗？作为一般模式，不要期望MBQI生产模型 涉及 只有无限范围的不同值。 如果确实需要，那么可以使用define-fun-rec构造来定义 递归函数。Z3目前相信该定义 格式良好（例如，与函数对应的方程 定义是令人满意的） Z3在搜索期间被动地使用递归定义的函数：无论何时 约束的地面部分有一个候选模型，它 检查候选模型的值是否充分定义了函数图。如果不是，则函数定义将在所选值上实例化，直到在相关值上定义好为止 到地面的约束 (set-o

我想知道SMT-LIB 2.0脚本中是否有可能访问解算器的最后一个可满足性决策（sat、unsat等）。例如，以下代码： (set-option :produce-unsat-cores true) (set-option :produce-models true) (set-logic QF_UF) (declare-fun p () Bool) (declare-fun q () Bool) (declare-fun r () Bool) (assert (! (=> p q) :n

使用smtlib，我想使用QF_UFNRA制作一些类似模的东西。这使我无法使用mod，to_int，to_real这样的东西 最后，我想在下面的代码中得到z的分数部分： (set-logic QF_UFNRA) (declare-fun z () Real) (declare-fun z1 () Real) (define-fun zval_1 ((x Real)) Real x ) (declare-fun zval (Real) Real) (assert (= z 1

在渴望SMT解算器中，SMT公式被编码为可等满足的布尔公式，该布尔公式被馈送给SAT解算器。通常，对于QF_-UF公式，未解释的函数通过Ackermann约化或Bryant约化进行约化，然后通过等式图方法构造一个等式可满足的布尔公式 因此，我想知道，在给定QF_UF公式的情况下，是否可以调用现有SMT解算器来获得可等式满足的布尔公式，而无需破解解算器的低级实现。例如，Z3有一些转换输入问题的策略（例如tseitin cnf和elim term ite），并且有这样的转换策略吗？在Z3中，您可以使

我试图在z3中的位向量中的特定索引处设置一个位 目前，我使用bit-wise或来实现这一点。我使用的是大位向量（超过1000位），我相信这会导致解算器花费大量时间。我希望他们的方法能够更快地在位向量中设置任意位（类似于数组使用的存储） 有没有更好的方法来实现这一点，或者我只是在使用逐位或？我不确定它是否会更快，但您始终可以这样执行断言： (assert (= ((_ extract i i) bv) #b1)) 告诉解算器ibv的第th位高。当然，这在您的特定应用程序中是否可用取决于这些新表达

我正在使用Z3定理证明器（使用Z3Py:Python中的Z3API）创建QBF（量化布尔公式） Z3中有没有办法直接将qbf公式转换成Prenex？我认为没有转换成Prenex的策略，但你肯定可以应用量词消除策略并进一步处理你的公式。请注意，转换后的公式与原始公式不太一样，因为它们是机械生成的 下面是一个例子： from z3 import * f = Function('f', IntSort(), IntSort(), IntSort()) x, y = Ints('x y') p = F

我在SMT-LIB中使用Int定义时间步长，这迫使我断言一些事情，以确保负片中没有发生任何事情： (declare-sort Pkg) ; A package (define-sort Time () Int) ; The installation step ; ... (assert (forall ((t Time) (p Pkg)) (=> (< t 0) (not (installed p t))))) （声明排序包）；包裹 （定义排序时间（）Int）；安装步骤 ; ...

在Z3中，是否有一种使用SMT 2输入格式计算BitVec中设置为1的位数的紧凑方法 这个问题的公认答案是： 展示了一种使用Python实现的方法。目前在SMTLib中直接实现这一点并不容易。最好的方法是针对每个位向量大小滚动自己的值；相当难看，但很容易生成代码： (set-logic QF_BV) (set-option :produce-models true) (define-fun popCount8 ((x (_ BitVec 8))) (_ BitVec 8)

我想检查a，b，c的值，如果值'a'等于1，'x'加一。我们继续处理值“b”和“c”。 所以如果a=1，b=1，c=1，x的结果应该是3。 如果a=1，b=1，c=0，那么x的结果应该是2。 z3中有什么要实现的方法吗？ 源代码如下所示： 从z3进口* a、 b，c=Ints'abc' x、 y=整数x y s=解算器 s、 addIfa==1，x=x+1，y=y-1 s、 addIfb==1，x=x+1，y=y-1 s、 加法=1，x=x+1，y=y-1 s、 检查 打印s.model 关于我

我见过一些例子，它们在解决方案中设法返回“不在乎”。我认为这利用了Z3的相关性传播。（见，） 这允许： (set-option :smt.auto-config false) (declare-const x Bool) (declare-const y Bool) (assert (or x y)) (assert x) (check-sat) (echo "Expect x is true") (eval x) ; returns true (echo "Expect y is don

我试图实现本文中的一些代码：证明关于一台简单机器的事实。我使用Python Z3 API编写了以下代码，与论文中描述的代码类似：为了更好地显示问题，特意简化了代码和问题： from z3 import * MachineIntSort = BitVecSort(16) MachineInt = lambda x: BitVec(x, 16) def DeclareLinkedList(sort): LinkedList = Datatype(f'{sort.name()}_Linke

F（x1）>a F（x2）=0（导数） F（x）=∑ ci*x^i；(一)∈[0，n]；c是一个常数）您的问题非常模糊，如果您显示您尝试了什么以及遇到了什么问题，堆栈溢出效果最好 然而，下面是如何使用Python接口为z3编写特定函数的代码F=2x^3+3x+4： 从z3导入* #将F表示为一个函数。这里有2x^3+3x+4 def F（x）： 返回2*x*x*x+3*x+4 #类似地，F的导数为：6x^2+3 def dF（x）： 返回6*x*x+3 x1，x2，a，b=整数（'x1-x2-a

例如： from z3 import * p1,p2, p3 = Reals('p1 p2 p3') s = Optimize() s.add(And(Or(p1>=0, p2>0),Or(p1<=10,p3>0))) print(s.check()) print(s.model()) 没错。但是，在设置较少变量的情况下，获得预期结果（满足约束和（或（p1>=0，p2>0）或（p10））是很有价值的 例如，仅设置p1=0（或范围内的任何值（[0,10]），则满足约束。只

我试图理解如何定义一个断言，以证明已经定义的函数的某些数学性质。正如在SMT中所讨论的，解算器不太适合于归纳，而归纳通常需要证明数学性质 在我的例子中，我有一个递归函数定义，用于标识函数f（x）=x（作为一个简单的示例）： 这表明，这些特征无法在开箱即用的情况下得到证明。然而，我想知道一般的数学性质是如何在z3中得到证明的。我尝试用所有量词证明函数的对合，但z3没有终止： (assert (forall ((a String)) (= a (indenti

在一次测试中，我发现了以下等价性，它基于混合布尔算术逻辑，我似乎无法在合理的时间内（几秒或几分钟）用Z3证明。我遵循一种反例驱动的方法（CEGIS），将原始表达式和合成候选项提供给一个不同的查询：如果没有找到反例，则合成是正确的 (set-logic QF_BV) (declare-fun y () (_ BitVec 64)) (declare-fun x () (_ BitVec 64)) (assert (let ((a!1 (bvsub (bvsub (bvsub x #x0000000