标签: z3

我正在使用Python绑定Z3定理证明器(Z3Py).我有N个布尔变量,x1,..,xN.我想表达一个约束条件,即N中的N个应该是真的.我怎么能在Z3Py中做到这一点？有没有内置的支持？我检查了在线文档,但Z3Py文档没有提及任何API.

对于N个中的一个约束,我知道我可以单独表达至少一个是真的(断言Or(x1,..,xN))并且最多只有一个为真(断言Not(And(xi,xj) ))所有i,j).我也知道其他方法来手动表达N-out和N-K-out-of-N约束.但是我的印象是,当解算器内置支持此约束时,它有时比手动表达它更有效.

有没有人尝试用Z3本身证明Z3？

甚至可以使用Z3证明Z3是正确的吗？

更理论化,是否有可能使用X本身来证明工具X是正确的？

我在Haskell中使用SBV(带有Z3后端)来创建一些理论证明.我想检查forall x和y给定的约束(比如x + y = y + x,哪里+是"加上运算符",而不是添加)其他一些术语是有效的.我想定义关于+表达式的公理(比如关联性,身份等),然后检查是否有进一步的等式,比如检查是否a + (b + c) == (a + c) + b有效正式a,b和c.

我试图通过以下方式实现它:

main = do
    let x = forall "x"
    let y = forall "y"
    out <- prove $ (x .== x)
    print "end"

但似乎我们不能.==在符号值上使用运算符.这是缺少的功能还是错误的用法？我们能够以某种方式使用SBV吗？

我试图使用Z3来推理子串,并且遇到了一些非直观的行为.当被要求确定'xy'是否出现在'xy'内时,Z3返回'sat',但当被询问'x'是否在'x'中时,它返回'unknown',或'x'在'xy'中.

我已经评论了以下代码来说明这种行为:

(set-logic AUFLIA)
(declare-sort Char 0)

;characters to build strings are _x_ and _y_
(declare-fun _x_ () Char)
(declare-fun _y_ () Char)
(assert (distinct _x_ _y_))

;string literals
(declare-fun findMeX () (Array Int Char))  
(declare-fun findMeXY () (Array Int Char))  
(declare-fun x () (Array Int Char))
(declare-fun xy () (Array Int Char))
(declare-fun length ( (Array Int Char) ) Int )

;set findMeX = 'x'
(assert (= (select findMeX 0) _x_))
(assert (= (length findMeX) 1))

;set findMeXY = …

使用Z3和文本格式,我可以define-fun用来定义函数以便以后重用.例如:

(define-fun mydiv ((x Real) (y Real)) Real
  (if (not (= y 0.0))
      (/ x y)
      0.0))

我想知道如何define-fun使用Z3 API 创建(我使用F#)而不是在任何地方重复函数的主体.我想用它来避免重复和调试公式更容易.我尝试过Context.MkFuncDecl,但它似乎只生成未解释的函数.

我将创建一个固定大小的数组,并用一些值初始化它.

例如,以下C++代码:

a[0] = 10;
a[1] = 23;
a[2] = 27;
a[3] = 12;
a[4] = 19;
a[5] = 31;
a[6] = 41;
a[7] = 7;

Z3中是否有一些实用程序可以对其进行建模？

我是Z3的新手,在这里和Google上搜索了我的问题的答案.不幸的是,我没有成功.

我正在使用Z3 4.0 C/C++ API.我声明了一个未定义的函数d:(Int Int)Int,添加了一些断言,并计算了一个模型.到目前为止,这很好.

现在,我想提取模型定义的函数d的某些值,比如d(0,0).以下语句有效,但返回表达式而不是函数值,即d(0,0)的整数.

z3::expr args[] = {c.int_val(0), c.int_val(0)};
z3::expr result = m.eval(d(2, args));

支票

result.is_int();

返回true.

我的(希望不是太愚蠢)问题是如何将返回的表达式转换为C/C++ int？

非常感谢帮助.谢谢!

简而言之,我需要能够遍历Z3_ast树并访问与其节点相关的数据.似乎无法找到有关如何做到这一点的任何文档/示例.任何指针都会有所帮助.

最后,我需要将smt2lib类型的公式解析为Z3,将一些变量变为常量替换,然后在数据结构中重现公式,该数据结构与另一个不相关的SMT sovler兼容(具体来说,我不认为有关misral的详细信息)对于这个问题很重要但有趣的是它没有命令行界面,我可以在其中提供文本公式.它只有一个C API).我已经想过要以mistral的格式生成公式,我需要遍历Z3_ast树并以所需的格式重建公式.我似乎无法找到任何演示如何执行此操作的文档/示例.任何指针都会有所帮助.

我正在研究一个项目,其重点是使用术语重写来解决/简化固定大小的位向量算术问题,这对于某些决策程序(例如基于钻头爆破的程序)的先前步骤是有用的.术语重写可以完全解决问题,或者产生更简单的等效问题,因此两者的组合可以导致相当大的加速.

我知道许多SMT求解器实现了这种策略(例如Boolector,Beaver,Alt-Ergo或Z3),但很难找到详细描述这些重写步骤的论文/技术报告/等.一般来说,我只发现了作者在几段中描述这种简化步骤的论文.我想找一些文件详细解释术语重写的用法:提供规则的例子,讨论AC重写和/或其他等式公理的便利性,重写策略的使用等.

目前,我刚刚找到了技术报告"固定宽度位向量的决策程序",描述了CVC Lite执行的规范化/简化步骤,我想找到更多这样的技术报告!我还发现了一张关于STP术语重写的海报,但这只是一个简短的总结.

我已经访问了那些SMT求解器的网站,我在他们的出版物页面中搜索过......

我将不胜感激任何参考,或任何有关如何在当前版本的知名SMT求解器中使用术语重写的解释.我对Z3特别感兴趣,因为它看起来有一个最聪明的简化阶段.例如,Z3 3.*引入了一个新的位向量决策程序,但遗憾的是,我无法找到任何描述它的论文.

我在以下看似微不足道的基准测试中尝试了几个SMT求解器(CVC3,CVC4和Z3):

(set-logic LIA)
(set-info :smt-lib-version 2.0)
(assert (forall (( x Int)) (forall ((y Int)) (= y x))))
(check-sat)
(exit)

所有的解决方案都归不为人知.我知道这是一个不可判断的片段(非线性),但我期待有一些简单的实例化启发式方法可以解决它.我也尝试用常量添加一些额外的断言,但它没有帮助.

有没有办法解决这些问题？SMT中量化算法的推理极限是什么？