Z3 OCaml API: mk_solver_s、mk_solver和mk_simple_solver的区别

Question

下午好,

我使用Z3 OCaml绑定来验证rational值上的属性。当我使用mk_solver_s ctx "QF_NRA"和mk_simple_solver初始化求解器时，我注意到了巨大的差异(这里的上下文是let ctx = mk_context [("model","true");("unsat_core","true")])。

或什么可以是卫星/非卫星。假设您没有得到“未知符号”这类问题，一般来说，sat/unsat的答案应该没有差别，但是性能可能会根据逻辑选择而有所不同。

更具体地说，我对神经网络的可能激活进行分支和界限的探索。这里的激活被理解为某个函数的输入是正的还是负的，这个函数的结果给出了神经网络的不同行为，并给出了对输入的一些线性约束。

神经网络线性部分用SMT公式表示。然后，每次我遇到一个可能的激活，我可以检查它是否有可能，根据以前已满足的激活。如果一次激活是可能的，则相关约束将添加到求解器堆栈中并继续进行。如果两种激活是可能的，则克隆求解器，并且我继续使用两个求解器，每一个都有一个附加的约束。

通过使用mk_solver_s ctx QF_NRA，我比使用mk_simple_solver ctx (实际上，n是神经元的数量)有更多的可能激活；第一个模型没有考虑到我添加的一些约束。例如，我有

(> |CELL_actual_input_0_0_0_1| (/ 1.0 2.0))
(< |CELL_actual_input_0_0_0_1| 2.0)
(> |CELL_actual_input_0_0_0_0| (/ 1.0 2.0))
(< |CELL_actual_input_0_0_0_0| 2.0)

在我的解决方案堆中，但是我的一个模型显示

(define-fun |CELL_actual_input_0_0_0_0| () Real
  0.0)
(define-fun |CELL_actual_input_0_0_0_1| () Real
  0.0)

仅更改求解器初始化函数将删除此行为。

文档(在这里：https://z3prover.github.io/api/html/ml/Z3.Solver.html)缺乏对此的任何解释；也许我不是在寻找好地方。我想知道以下功能之间有什么区别：

• mk_simple_solver
• mk_solver_s (它似乎只接受理论字符串，但对于这个https://github.com/Z3Prover/z3/issues/1035#issuecomment-303160975，它实际上接受了很多策略，我不知道如何使用use)
• mk_solver

)。

mk_simple_solver设置和mk_solver_s不做的“默认”是什么？

我很想做一个增强OCaml API的请求，我不太确定该从哪里开始。

(预先谢谢:)

Answer 1

您可以通过查看这些问题的实现来回答其中的一些问题：

let mk_solver ctx logic =
    match logic with
    | None -> Z3native.mk_solver ctx
    | Some x -> Z3native.mk_solver_for_logic ctx x

let mk_solver_s ctx logic = mk_solver ctx (Some (Symbol.mk_string ctx logic))
let mk_simple_solver = Z3native.mk_simple_solver

因此，mk_solver_s中的字符串允许您选择想要的逻辑。(不是不同的“理论”)。逻辑可以看作是理论的组合，详见SMTLib站点：http://smtlib.cs.uiowa.edu/theories.shtml vs http://smtlib.cs.uiowa.edu/logics.shtml)

因此，mk_solver_s与mk_solver完全相同，只不过它允许您从给定的逻辑开始。(逻辑选择主要取决于在求解器中有哪些符号可用，因为某些术语在某些逻辑中才有意义。例如，你不能在任何宣称自己是无量词的逻辑中使用量词，等等。)

你说你注意到“巨大的差异”使用这些，但没有详细说明这些差异是什么？你是说表演？或者什么可以是sat/unsat。假设您没有得到“未知符号”这类问题，一般来说，sat/unsat答案应该没有区别，但是性能可能会根据逻辑选择而有所不同。(例如，选择一个不同的逻辑可以对不需要其他任何东西的约束产生巨大的影响。)但如果没有细节，很难对此发表看法。

希望这能让你开始。有时候，最好的方法就是查看源代码本身！