如何创建包含一组其他对象的数据类型.基本上,我正在做以下代码:
(define-sort Set(T) (Array Int T))
(declare-datatypes () ((A f1 (cons (value Int) (b (Set B))))
(B f2 (cons (id Int) (a (Set A))))
))
但是Z3告诉我对A和B的未知排序.如果我删除"Set",它就像指南所说的一样.我试图使用List,但它不起作用.谁知道如何让它工作？
我正在尝试用zt的smt-lib 2语法编码QBF.运行z3会产生警告
警告:未能找到量词的模式(量词id:k!14)
并且可满足性结果是"未知的".
代码如下:
(declare-fun R (Bool Bool Bool Bool) Bool)
(assert
(forall ((x2 Bool) (x3 Bool))
(exists ((y Bool))
(forall ((x1 Bool))
(R x1 x2 x3 y)
)
)
)
)
(check-sat)
我通过重写代码来摆脱警告
(set-option :auto-config false)
(set-option :mbqi false)
(declare-fun R (Bool Bool Bool Bool) Bool)
(declare-fun x1 () Bool)
(declare-fun x2 () Bool)
(declare-fun x3 () Bool)
(declare-fun y () Bool)
(assert
(forall ((x2 Bool) (x3 Bool))
(!
(exists ((y Bool))
(!
(forall ((x1 Bool))
(!
(R …定理证明工具z3花了很多时间来解决一个公式,我相信它应该能够轻松处理.为了更好地理解这一点并可能优化我对z3的输入,我想看到z3生成的内部约束作为其求解过程的一部分.当从命令行使用z3时,如何打印z3为其后端解算器生成的公式？
对于下面的代码,我观察到非常快速的结果,似乎是由三个不寻常的方面引起/影响:
(set-option :produce-proof true),最终的UNSAT非常快.如果没有此选项,最终的check-sat不会终止.有人可以解释这些情况下的行为吗？只是选项的组合导致保留正确的事实来快速回答最终的SAT吗？未使用的构造函数的字段名称如何影响求解器的性能？
与此问题相关的代码如下.嵌入在代码中的是具有额外上下文和重复问题的注释.
;;;;;;;;;;;;;;;;;;;;;;;;;;;; Configuration ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; E-matching won't terminate on our queries, so turn it off
(set-option :smt.ematching false)
(set-option :smt.mbqi true)
;; In lieu of an initial test, produce-proofs true is a huge benefit to
;; the performance of the final check-sat
(set-option :produce-proofs true)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; Raw data ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Our syntactic representation of 'Bits'
;; Removing 'Raw2345', or renaming it to 'Raw2', causes ~30x more computation time.
(declare-datatypes …我尝试了下面的代码 http://rise4fun.com/z3/tutorial
(declare-const a Int)
(assert (> a 100))
(check-sat)
(get-model)
结果总是如此a=101.我在答案中需要一些随机性,它会产生一个范围内的随机数[101,MAXINT).例如得到一个seed=1000并提供a=12344.对于seed=2323报价a=9088765和....
我应该在这个简单的代码中添加什么？
我正在研究一个Python项目,我正在尝试以一些可怕的方式加快速度:我设置了Z3求解器,然后我分叉了这个过程,让Z3在子进程中执行求解并传递一个将模型的可挑剔表示返回到父级.
这很好用,代表了我正在尝试做的第一阶段:父进程现在不再受CPU约束.下一步是多线程父线程,以便我们可以并行解决多个Z3求解器.
我很确定在设置阶段我已经互斥了Z3的任何并发访问,并且任何时候只有一个线程应该触摸Z3.然而,尽管如此,我在libz3.so中得到随机段错误.在这一点上,重要的是要注意,它并不总是触及Z3 的相同线程 - 同一个对象(不是解算器本身,而是表达式)可能在不同的时间由不同的线程处理.
我的问题是,是否有可能多线程Z3？这里有一个简短的说明(http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html)说"从多个线程访问Z3对象是不安全的".我想我会回答我的问题,但我希望这意味着说不应该同时从多个线程访问Z3 .另一个资源(再次:在Windows上安装Z3 + Python)从莱昂纳多自己说,"Z3使用线程本地存储",我猜,这将沉没整个事业,但是a)答案是从2012年开始,所以也许是事情已经改变了,并且b)也许它使用线程本地存储来处理一些不相关的东西？
无论如何,多线程Z3是否可能(来自Python)？我不想将设置阶段推进子进程......
我已经使用 Anaconda Prompt ( pip install z3-solver ) 在我的 Python3 环境中从 PyPi 安装了 z3-solver 包，仅此而已。
该包出现在site-packages/目录中（该包具有 _init__.py 和所有必需文件，包括 z3.py ）。但是，当我尝试从 Jupyter Notebook 运行此示例时，它返回以下消息：NameError：名称“Int”未定义。
我只使用 Anaconda 很短时间，所以我不确定安装是如何进行的。这真的很奇怪，因为“pip install”命令在大多数情况下都可以正常工作。我做错了什么或者这个包需要更多配置吗？
我们知道,我们可以通过以下方式证明一个定理的有效性:
let Demorgan(x, y) = formula1(x,y) iff formula2(x,y)
assert ( forall (x,y) . Demorgan(x,y) )
或者,我们可以通过以下方式消除forall量词:
let Demorgan(x, y) = formula1(x,y) iff formula2(x,y)
( assert (not Demorgan(x,y) ) )
因此,如果它返回不饱和,那么我们可以说上面的公式是有效的.
现在我想用这个想法从以下断言中消除forall量词:
assert ( exists x1,x2,x3 st .( forall y . formula1(x1,y) iff
formula2(x2,y) iff
formula3(x3,y) ) )
那么在Z3(使用C++ API或SMT-LIB2.0)中有什么办法可以断言如下:
assert (exists x1,x2,x3 st. ( and ((not ( formula1(x1,y) iff formula2(x2,y) )) == unsat)
((not ( formula2(x2,y) iff formula3(x3,y) )) == unsat)))
我是Z3的新手,我正在查看在线python教程.
然后我想我可以检查BitVecs中的溢出行为.
我写了这段代码:
x = BitVec('x', 3)
y = Int('y')
solve(BV2Int(x) == y, Not(BV2Int(x + 1) == (y + 1)))
我期待[y = 7,x = 7](即当值相等但后继不是因为x + 1将为0而y + 1将为8)
但Z3回答[y = 0,x = 0].
我究竟做错了什么？
任何或多或少的实用编程语言和编译器都必须处理约束.最常见的约束是类型.通常,类型推导和统一是通过简单的算法(例如Hindley-Milner)完成的,其中最终程序中的所有项都被赋予唯一类型.如果没有发生,则会出现错误指示.
在编译器中可能存在更复杂的约束,其中完全统一是不可能的,并且解决方案仅在某些限制下存在.可能的例子是
数据流分析.仿射相等约束的解可以用于循环矢量化.
内存管理.如果我们对引用和数据访问模式有一些约束,编译器可以从优化引用计数和垃圾收集中受益.
从另一点来看,约束求解器(如Z3或Yices)在为不同类型的约束寻找可满足的模型方面非常强大.
我正在寻找有关编译器如何从SMT求解器的强大功能以及他们正在解决的任务类型中受益的成功案例.我列出了一些区域,但我没有找到任何具体的例子.你能建议吗？
compiler-construction programming-languages constraint-programming smt z3