如何解决(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 举报,一经查实,本站将立刻删除。