我有一个文件包含:

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Real)
(declare-const e Real)
(assert (> a (+ b 2)))
(assert (= a (+ (* 2 c) 10)))
(assert (<= (+ c b) 1000))
(assert (>= d e))
(check-sat)
(get-model)

并且,根据在线教程,在此文件上运行z3应该返回:

sat
(model
    (define-fun c () Int
        (- 5))
    (define-fun a () Int
        0)
    (define-fun b () Int
        (- 3))
    (define-fun d ()
        Real 0.0)
    (define-fun e ()
        Real 0.0)
)

所以我知道这是合法的Z3输入.但是,每当我运行"z3 [option]"时,无论选择何种选项,我得到的都是错误消息 - 包括无.有人能告诉我如何在输入文件上正确调用Z3吗？

问候.

给定一个使用 Z3 实数编码的问题，Z3 /smt2 /st产生的哪些统计数据可能有助于判断实数引擎是否“有问题/做了很多工作”？

就我而言，我有两个几乎等效的问题编码，都使用实数。然而，编码中的“小”差异在运行时产生了很大差异，即编码 A 需要 2:30 分钟，编码 B 需要 13 分钟。Z3的统计数据显示，conflicts和quant-instantiations大多是等价的，但其他人都没有，例如grobner，pivots和nonlinear-horner。

两种不同的统计数据可作为gist 使用。

编辑（以解决 Leo 的评论）：

两个版本生成的 SMT2 编码约为 30k 行，并且使用实数的断言散布在整个代码中。的主要区别在于编码乙使用大量尚未得以实时类型的常量从范围0.0到1.0由不等式，例如有界0.0 < r1 < 1.0或0.0 < r3 < 0.75 - r1 - r2，而在编码许多这些尚未得以常数已经从相同的范围置换为固定真实值，例如，0.1或0.75 - 0.01。两种编码都使用非线性实数算术，例如r1 * (1.0 - r2).

来自两种编码的一些随机示例可作为要点。如上所述，所有出现的变量都是未指定的实数。

PS：是否为固定实数值引入别名，例如，

(define-sort $Perms () Real)
(declare-const …

有人可以帮我指出使用一阶公式的下列方程的最佳编码,以便将其作为SMT求解器的输入吗？

x`=Ax+b

先前问题中指出的安装问题仍然存在.我曾尝试在Windows XP SP3 32位和Windows 7 64位下安装Z3 4.3.0和4.1.这些组合都不起作用!我能够做" from z3 import *",但是init()Z3 dll的失败.我的Python版本是2.7.3.Z3独立和Python独立工作,但没有很多抱怨它们不能一起工作.

这将有助于获得最新的安装配方,回答以下问题:

应该使用哪个Z3下载(源版本,预编译版本)？

应该使用哪个Python版本？

在init()调用中应该引用哪个或哪些Z3 DLL？一个例子会有所帮助(包括带空格的路径的原始字符串用法).

应该使用哪些Z3 Python源文件(Z3的某些下载有*.py文件,其他有*.pyc文件)？编译的Python文件是否与多个Python版本兼容？

如何设置PATH和PYTHONPATH？

如何以自动提供Z3初始化的方式调用Python的IDLE shell？

对不起,如果这听起来像是一个新手问题,但......

我有几个 SMTLIB2 示例，z3 通常在 10 毫秒内发现 unsat，但是，当我添加请求以生成 unsat 核心时，check-sat 会持续运行几分钟而不返回。这种行为是预期的吗？请求 unsat 核心是否不仅仅是打开仪器记录依赖项，并更改 z3 运行的程序和选项？是否可以设置更多选项，以便在使用 unsat 核心生成时看到的行为与不使用时看到的行为相同？

我在 Scientific Linux 6.3 上使用 Z3 4.3.1（稳定分支）。

这些例子在 AUFNIRA 中，尽管有几个不涉及实数并且可能不是非线性的。

谢谢，

保罗。

我的例子:方程组

  a = b+c
? e = a*c

? a = +2     ; some replaceable concrete values
? c = +18

  b = -16
? e = -32

我想要的信息

在一个方程组中,我希望得到以下知识:

我可以用来从给定值(在约束基础中)计算变量值(解决方案)的抽象公式.

(就像在高中,老师不仅希望看到结果,而且还有这样一个转化的抽象公式.)

  b = a-c     ; is an equivalent transformation from `a = b+c`
? e = (a-c)*c ; is an term replacement `b ? a-c` of `e = a*c`

我的问题

如何使用Z3Py从Z3约束方程组中检索此信息？

谢谢. - 如果有什么不清楚的地方,请评论一下是什么问题.

我想将RatNum表达式转换为Dot Net小数.RatNum有一个ToDecimalString方法,但不是ToDecimal方法.这有什么理由吗？除了Decimal.Parse(ratnum.ToDecimalString(2))之外还有其他方法可以将RatNum转换为小数吗？谢谢.

我正在尝试使用Visual Studio 2010编译器在Windows 7 64 Professional 64位上构建Z3定理证明器.我按照README说明进行操作,直到进入"build"目录并点击nmake.过了一会儿,我得到以下内容:

    cl /Fez3.exe /nologo /MD shell/datalog_frontend.obj shell/dimacs_frontend.obj shell/install_tactic.obj shell/main.obj shell/smtlib_frontend.ob
j shell/z3_log_frontend.obj api/api.lib parsers/smt/smtparser.lib tactic/portfolio/portfolio.lib tactic/ufbv/ufbv_tactic.lib tactic/smtlogics/smtlogic
_tactics.lib muz_qe/muz_qe.lib tactic/sls/sls_tactic.lib smt/tactic/smt_tactic.lib tactic/fpa/fpa.lib tactic/bv/bv_tactics.lib smt/user_plugin/user_pl
ugin.lib smt/smt.lib smt/proto_model/proto_model.lib ast/rewriter/bit_blaster/bit_blaster.lib ast/proof_checker/proof_checker.lib ast/macros/macros.li
b ast/pattern/pattern.lib parsers/smt2/smt2parser.lib cmd_context/extra_cmds/extra_cmds.lib cmd_context/cmd_context.lib solver/solver.lib tactic/aig/a
ig_tactic.lib math/subpaving/tactic/subpaving_tactic.lib nlsat/tactic/nlsat_tactic.lib tactic/arith/arith_tactics.lib sat/tactic/sat_tactic.lib tactic
/core/core_tactics.lib ast/normal_forms/normal_forms.lib ast/simplifier/simplifier.lib front_end_params/front_end_params.lib math/euclid/euclid.lib ma
th/grobner/grobner.lib parsers/util/parser_util.lib ast/substitution/substitution.lib tactic/tactic.lib model/model.lib ast/rewriter/rewriter.lib ast/
ast.lib math/subpaving/subpaving.lib math/interval/interval.lib nlsat/nlsat.lib sat/sat.lib math/polynomial/polynomial.lib util/util.lib /link /DEBUG
/MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 …

我在Z3中得到以下统计信息.

(:added-eqs            24529
 :binary-propagations  43837
 :bv-bit2core          7115
 :bv-conflicts         156
 :bv-diseqs            10395
 :bv-dynamic-diseqs    10028
 :bv->core-eq          10401
 :conflicts            409
 :decisions            4840
 :del-clause           84926
 :final-checks         2
 :max-generation       4
 :memory               5.69
 :minimized-lits       467
 :mk-clause            88358
 :propagations         90195
 :quant-instantiations 3388
 :restarts             3
 :time                 0.83)

我想知道每个结果行使用的指标.

你能帮助我吗？

我想证明一种简化方法，其中涉及计算以2为底的对数。z3 / cvc4中是否有任何函数可用于计算它？