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

如何解决Z3 OCaml API：mk_solver_s、mk_solver 和 mk_simple_solver 的区别

下午好，

我正在使用 Z3 OCaml 绑定来验证有理值的属性。当我使用 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 有更多可能的激活（实际上，2^n 其中 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 它实际上接受了很多策略，我不知道如何使用）
• mk_solver

mk_simple_solver 设置而 mk_solver_s 没有设置的“默认值”是什么？

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

先谢谢你:)

解决方法

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

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 答案应该没有区别，但性能可能会因逻辑选择而异。 （例如，选择差异逻辑可以对不需要其他任何东西的约束产生巨大影响。）但没有细节就很难判断。

希望这可以帮助您入门。有时最好的办法是查看源代码本身！