Z3/OCaml 自由常量

Question

出于好奇，我想知道如何通过 OCaml API 向 Z3 求解器添加一个自由常量，即对应于

的东西

(declare-const k!0 (_ BitVec 5))

以下尝试产生了一个 invalid argument 异常。

let cfg = [("model", "true"); ("proof", "false")] in
let ctx = mk_context cfg in
let solver = Solver.mk_solver ctx None in
  Solver.add solver [Expr.mk_const ctx (Symbol.mk_int ctx 0) (BitVector.mk_sort ctx 5)]

有没有办法在不添加包含常量并简化为 true 的约束的情况下执行此操作？

Answer 1

Solver.add 需要一个布尔排序项，即一个断言，但在这个例子中添加了一个位向量类型的常量，这就是它抱怨无效参数的原因。

一般来说，常量（或任何其他函数）不需要通过 API 在单独的步骤中显式声明，它们可以在 expressions/assertions 中构造和使用而无需声明。

默认情况下，这些常量将被假定为存在性的，否则它们将必须被显式量化（参见量词模块）。

Z3/OCaml 自由常量

Z3/OCaml free constants

z3