(Z3 ocaml) 检查整数理论中方程的所有解

问题描述

在 Z3ML 中，如果整数理论中的方程有多个解，我如何像 Z3Py 中的 here 一样得到所有解？

open Z3
open Z3.Arithmetic
open Z3.solver
open Z3.Expr
open Z3.Boolean
open Printf

let assertions (ctx : Z3.context) = 
    let zero : Expr.expr = Arithmetic.Integer.mk_numeral_i ctx 0 in
    let three : Expr.expr = Arithmetic.Integer.mk_numeral_i ctx 3 in
    let x : Expr.expr = Arithmetic.Integer.mk_const_s ctx "x" in
    let y : Expr.expr = Arithmetic.Integer.mk_const_s ctx "y" in
    [Arithmetic.mk_ge ctx x zero; Arithmetic.mk_le ctx x three; Arithmetic.mk_ge ctx x y; Arithmetic.mk_le ctx x y]

(** get_all_models *)
let models () =
    let ctx = Z3.mk_context [("model","true"); ("proof","false")] in
    let slvr = Solver.mk_solver ctx None in
    let get_all_models (c : Z3.context) (s : Solver.solver) = 
        Solver.add s (assertions c); 
        Printf.printf "%s\n" (Solver.string_of_status (Solver.check s []));
        match Solver.get_model s with
        | Some m -> Printf.printf "%s\n" (Model.to_string m)
        | None ->  Printf.printf "no model\n"       
    in  
    get_all_models ctx slvr

就像上面的代码示例，我怎样才能得到所有的模型/解决方案，它们是 {(x=0,y=0),(x=1,y=1),(x=2,y= 2),(x=3,y=3)}

解决方法

暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！

如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。

小编邮箱:dio#foxmail.com (将#修改为@）

ocaml ocaml z3