标签: z3

我有兴趣和寻找SMT Z3使用的实际例子(如DbC)以及该工具的代码和开源替代品.所以,事实上,我对类似的Z3正式求解工具很感兴趣,但是:

• 它必须是开源的
• 提供低级(API)和高级(文本脚本)交互
• 支持SMT-LIB
• 适合(可用)在工具中/用于编写/用于Java,python,ruby,Vala等语言,而不是 Haskell
• 具有基于它的稳定(可在实践中使用)工具,如合同设计(DbC),静态类型验证等.

根据SMT-LIB主页(详见bit.ly软件包),2010年SMT解决方案列表为:"Alt-Ergo,Barcelogic,Beaver,Boolector,CVC3,DPT,MathSAT,OpenSMT,SatEEn,Spear,STP,SWORD, UCLID,veriT,Yices,Z3."

请提供有关在实践中使用其中任何一个的任何反馈(代码示例是最好的)？

最后,任何有关它与GHC可能性进行比较的信息都是有用的,但仅限于存在实施示例(不是语言"特征")的情况.

有关Z3的更快速信息,请访问http://bit.ly/bundles/ewiger/1

我用z3分析了QF_AUFLIA中的公式.结果是sat.返回的模型(get-model)包含以下行:

  (define-fun PCsc5_ () Int
    (ite (= 2 false) 23 33)

根据我对SMTLIBv2语言的理解,这个陈述是错误的.=应该只应用于相同类型的参数.但是,2有排序Int和false排序Bool.

当我将这两行反馈给z3时,它同意我的意见:

invalid function application, sort mismatch on argument at position 2

这是一个错误吗？

如果没有,我该怎么解释(= 2 false)？

基本上,我想让Z3给我一个任意整数,其值大于10.所以我写下面的语句:

(declare-const x (Int))
(assert (forall ((i Int)) (> i 10)))
(check-sat)
(get-value(x))

如何将此量词应用于我的模型？我知道你可以写(assert(> x 10))来实现这一点.但我的意思是我想在我的模型量词所以每次我宣布一个整型常量,其值是保证时间将超过10所以我不必为每一个整型常量,我insert语句(主张(>×10))声明.

说我有

t1<x and x<t2

是否可以隐藏变量x以便 t1<t2 在Z3中？

我使用的是Z3的.NET API.当我通过调用实例化解算器时:

Solver s = ctx.MkSolver(ctx.TryFor(ctx.MkTactic("qflia"), TimeLimit));

对于某些型号的声明,给它一个60秒(60000毫秒)的TimeLimit

s.Check()

60秒后不返回.对于某些型号,它会在几秒钟后返回,在我的情况下不会出现问题,但对于某些型号它根本不会返回(我在3天后取消了该过程).

如何在给定的时间限制后强制Z3停止检查？

由于这个问题有点难以描述,我将用一个小例子来描述我的问题.假设有一个命题公式集,其元素是布尔变量a,b和c.当使用z3获得该公式集的真值分配时,是否存在某种设置变量优先级的方法？我的意思是如果优先级是a> b> c,那么在搜索过程中,z3首先假定a为真,如果a不可能为真,则假定b为真,依此类推.换句话说,如果z3给出真值赋值:在上述优先级下不是a,b,c,则意味着a不可能为真,因为a与b相比具有高优先级.希望我能清楚地描述这个问题.

链接：具有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), …

Z3的算术求解器是基于DPLL(T)和Simplex(本文所述)开发的.我不明白Z3在生成冲突解释时如何执行回溯.我举个例子:

线性算术公式为:

(2x1+x2?200 OR 3x1+x2?250) AND (2x1+x2+x3?200 OR 4x1+2x2+x3?400) AND x1?50 AND x2?50 AND x3?60

断言后2x1+x2?200,2x1+x2+x3?200,x1?50,x2?50和x3?60先后,它产生冲突的解释集{2x1+x2+x3?200, x1?50, x2?50, x3?60}.

我的问题是,当生成此冲突集时,如何执行回溯？

在Microsoft Z3中,当我们尝试求解公式时,Z3始终以相同的顺序返回结果,此时有两个或更多可满足的解决方案.

是否有可能从Z3获得随机结果,以便对于相同的输入,它将在不同的执行中生成不同的输出序列.

请注意,我使用的是C或C#API.我没有使用smt2lib使用Z3.因此,如果您可以给我一个可以添加随机化的C或C#API函数示例,它将更有用.

我在使用LiquidHaskell证明以下法律时遇到了麻烦:

它被称为DeMorgan定律(之一),并简单地指出,or对两个值的否定必须and与每个值的否定相同.它已经被证明了很长时间,并且是LiquidHaskell 教程中的一个例子.我正在学习本教程,但未能通过以下代码:

-- Test.hs
module Main where

main :: IO ()
main = return ()

(==>) :: Bool -> Bool -> Bool
False ==> False = True
False ==> True  = True
True  ==> True  = True
True  ==> False = False

(<=>)  :: Bool -> Bool -> Bool
False <=> False = True
False <=> True  = False
True  <=> True  = True
True  <=> False = False

{-@ type TRUE  = {v:Bool …