标签: z3

从当前版本开始,"ctx-solver-simplified"中存在一些问题,例如http://rise4fun.com/Z3/CqRv中的 z3给出了错误的答案.我将"ctx-solver-simplified"替换为"简化",如http://rise4fun.com/Z3/x9X4 我想知道,这两种策略"简化"和"ctx-solver-simplified"之间有什么区别？

我想从z3获得的解决方案没有简化使用let语句.

例如,如果我给出以下内容:

(declare-const x Int)
  (elim-quantifiers (exists ((x.1 Int)) 
    (and (or (and (= (- x.1 2) 0) (<= (- x.1 9) 0)) 
             (and (or (= (- x.1 2) 0) (and (<= (- x.1 4) 0) 
                                      (and (<= (- 4 x.1) 0) 
                                           (<= (- x.1 11) 0)))) (<= (- x.1 9) 0))) (= (- (+ x.1 2) x) 0))))

我得到的解决方案是:

(let ((a!1 (and (or (and (<= x 4) (>= x 4)) (and (<= x 6) (>= x 6) (<= …

我正在浏览Z3py,并在一些特定情况下对如何使用API​​提出疑问.下面的代码是我最终想要使用Z3的简化版本.我的一些问题是:1.有没有办法创建一个任意长的值数组,如下面的变量'a'？2.你能通过Z3py在循环中访问数组的每个元素吗？3.是否可以将结果分配回原始变量或是否需要新变量？转换为CNF会自动添加唯一ID吗？(即a + = b)

总的来说,我迷失了如何将Z3py API应用于以下算法,其中解决方案依赖于'b'.任何帮助或提示都表示赞赏,谢谢.

import sys
import struct

a = "\xff\x33\x01\x88\x02\x11\x03\x55"
b = sys.stdin.read(1) #a byte of user input - value 'a' is good
c = ''
d = ''

for x in range(len(a)):
    c +=  struct.pack( 'B', int(a[x].encode('hex'), 16)^int(b.encode('hex'), 16) )

print c.encode('hex')

second = '\x23\x23'
x = 0
while x < len(c):
    d += struct.pack( 'h', int(c[x:x+1].encode('hex'), 16)^int(second.encode('hex'), 16) )
    x += 2

print d.encode('hex')

if d == '\xbd\x23\x43\x23\x40\x23\x41\x23':
    print "Good"
else:
    print "Bad"

如何检索枚举变量的值v ？例如，

vTyp, (val1,val2,val3) = EnumSort('vTyp',['val1','val2','val3'])
v = Const('my variable',vTyp)

现在，由于只是上面的变量v，我将如何检索值的列表 [val1,val2,val3]中v（这里val1,val3,val3是表达如上）？

我试过了，[v.sort().constructor(0), ...(1), ...(2)] 但是构造方法没有返回表达式。

我有两个不同大小的'a'和'b'变量,见下文.我有几个问题:

(1)如何将'a'的值复制为'b'？(即延长操作)

(2)如何将'b'的值复制为'a'？(即截断操作)

谢谢.

a = BitVec('a', 1)
b = BitVec('b', 32)

链接：具有Pyhton绑定的
Z3定理证明者
picosat

我已经使用Z3作为SAT求解器。对于较大的公式，似乎存在性能问题，这就是为什么我想查看picosat来查看它是否是更快的替代方案。我现有的python代码使用z3语法生成一个命题公式：

from z3 import *

import pycosat
from pycosat import solve, itersolve

#
#1 2  3  4  5  6  7   8  (variable names in picosat are numbers!)
#
C, G, M, P, R, S, SN, B = Bools('C G M P R S SN B')
C = (And(*(S,Or(Not(S),P),Or(Not(P),S),Or(Not(P),B),Or(Not(C),P),Or(Not(G),P),Or(Not(M),P),Or(Not(R),P),Or(Not(SN),P),Or(Not(B),P),True,Not(False),Or(R,SN,B,G,M,C,True))))

# formula in Z3:
f = simplify(C)

print f 

输出/结果

And(S,
    Or(Not(S), P),
    Or(Not(P), S),
    Or(Not(P), B),

    Or(Not(C), P),
    Or(Not(G), P),
    Or(Not(M), P),
    Or(Not(R), P),
    Or(Not(SN), P),
    Or(Not(B), …

今天我也想看看在haskell中解决SAT的选项.首先,我想把自己的接口写入picosat求解器.

然后我发现有SBV库.它是Z3,Yices,CVC4和Boolector的接口.

此外,我在github上进行了谷歌搜索,它甚至可以使用Picosat绑定.

考虑到快速/高性能的限制,是否有任何其他针对SAT求解器的haskell绑定值得关注.Carification:适用于高性能SAT解决(例如,运行数天的问题,以及需要在检查2 ^ 20或更多SAT问题时尽快完成的问题).例如,我在hackage上特别缺少的是绑定到像Plingeling这样的快速并行 SAT求解器.(另外,我在github上发现了当前更新的picosat绑定更多的意外,我很可能会错过其他选项)

SBV库的默认选项是Z3 SMT解算器.在我受过良好教育的猜测中,我是否正确,对于简单的SAT解决而言,picosat比Z3更快？

在使用.smt2文件时,我注意到Z3 4.3.1有一些奇怪的行为.

如果我这样做(assert (= 0 0.5))将是令人满意的.但是,如果我切换订单并且(assert (= 0.5 0))不满意.

我对正在发生的事情的猜测是,如果第一个参数是一个整数,它将它们都转换为整数(将0.5舍入为0),然后进行比较.如果我将"0"更改为"0.0",它将按预期工作.这与我使用的大多数编程语言形成对比,如果其中一个参数是浮点数,它们都被转换为浮点数并进行比较.这真的是Z3中的预期行为吗？

我正在修改一个使用Z3(特别是Python API)来解决bitvector约束的工具.我需要使用一个特定的外部SAT求解器而不是内部的Z3求解器,所以我首先使用这个策略进行爆破

Then('simplify', 'bit-blast', 'tseitin-cnf')

之后我可以相对容易地将子句转储到DIMACS文件中.问题是将得到的命题模型映射回原始约束的模型:据我所知,Python API没有提供访问对应于策略的模型转换器的方法.这是真的？如果是这样,是否可以使用不同的API完成,或者是否有更简单的方法？基本上我只需要知道最终CNF子句中的命题变量如何与原始的bitvector变量相对应.

对于我正在开始的项目,我将需要使用SAT求解器.我之前使用过其中一些但主要用于实验,而这里项目的主要约束是良好的性能.我正在尝试寻找替代方案,并尝试了解每种方案如何根据我的具体要求定位.特别是:

1. 我需要提取令人满意的任务,不仅要检查是否满足,而且解算器应该允许我重复求解相同的公式,寻找不同的可能令人满意的任务,最终以有效的方式迭代所有这些,(例如,没有我)必须添加一个条款并重新开始).

2. 该项目应该仍然是积极维护和相当的生产质量,而不是自出版以来放弃的一些竞争获胜的研究项目(见picosat).

3. 此外,由于我使用的是C++,解算器应该提供一个高效且(可能)良好的编写C++接口.

我考虑的第一个候选人是Z3,但我对文档感到困惑,如果上面的第1点得到支持则无法理解,如果我只需要SAT而不是SMT就可能有点过分.C++界面似乎也很容易使用,但我无法忍受这样一个事实:我必须使用普通字符串命名变量(这与我周围的算法配对非常糟糕.这是不是可以避免？).

那么你能否给我一些关于哪个SAT求解器使用的建议,或者对Z3的怀疑有所启发？