当Z3中的公式不饱和并且(防止出现)时,有一个输出,我找不到任何关于它是什么的信息.我在哪里可以找到有关它的任何文件？
在我看来相当难以理解,是否有可能将此作为输入的工具？
干杯,马特
从当前版本开始,"ctx-solver-simplified"中存在一些问题,例如http://rise4fun.com/Z3/CqRv中的 z3给出了错误的答案.我将"ctx-solver-simplified"替换为"简化",如http://rise4fun.com/Z3/x9X4 我想知道,这两种策略"简化"和"ctx-solver-simplified"之间有什么区别？
我正在浏览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"
我有两个不同大小的'a'和'b'变量,见下文.我有几个问题:
(1)如何将'a'的值复制为'b'？(即延长操作)
(2)如何将'b'的值复制为'a'？(即截断操作)
谢谢.
a = BitVec('a', 1)
b = BitVec('b', 32)
给定Z3py中的表达式,我可以将其转换为SMT-LIB2语言吗？(所以我可以将这个SMT-LIB2表达式提供给支持SMT-LIB2的其他SMT求解器)
如果可以,请举一个例子.
非常感谢.
今天我也想看看在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中的预期行为吗？
假设我有两个约束(c1,c2),我想检查它们是否语法相同:
c1: f(x)>1 && g(y)=2
c2: f(x)>1 && g(y)=2
选项1:我们可以把这变成一个可满足性问题,就像这篇文章: 两个boolexpr是否相等
选项2:我们也可以将它们变成字符串并比较相等:
if(c1.toString().equals(c2.toString()))
///do somthing
但随着约束的大小增加,这两个选项都有很大的开销.例如,在Expr中调用toString()方法对于大型约束非常昂贵.
两个问题:
如何在Z3(Java版本)中检查两个约束在语法上是否完全相同？
如果我们没有1的好解决方案,我正在考虑为Expr对象编写一个包装器并使用工厂方法来避免从Z3生成重复(语法)对象.然后我必须设计自己的equal()和hashCode()函数.但到目前为止,我仍然无法找到一种有效的方法.
对于我正在开始的项目,我将需要使用SAT求解器.我之前使用过其中一些但主要用于实验,而这里项目的主要约束是良好的性能.我正在尝试寻找替代方案,并尝试了解每种方案如何根据我的具体要求定位.特别是:
我需要提取令人满意的任务,不仅要检查是否满足,而且解算器应该允许我重复求解相同的公式,寻找不同的可能令人满意的任务,最终以有效的方式迭代所有这些,(例如,没有我)必须添加一个条款并重新开始).
该项目应该仍然是积极维护和相当的生产质量,而不是自出版以来放弃的一些竞争获胜的研究项目(见picosat).
此外,由于我使用的是C++,解算器应该提供一个高效且(可能)良好的编写C++接口.
我考虑的第一个候选人是Z3,但我对文档感到困惑,如果上面的第1点得到支持则无法理解,如果我只需要SAT而不是SMT就可能有点过分.C++界面似乎也很容易使用,但我无法忍受这样一个事实:我必须使用普通字符串命名变量(这与我周围的算法配对非常糟糕.这是不是可以避免？).
那么你能否给我一些关于哪个SAT求解器使用的建议,或者对Z3的怀疑有所启发？
如何while循环（C-代码）一个简单SMT2语言或Z3转换？例如：
int x,a;
while(x > 10 && x < 100){
a = x + a;
x++;
}