0

In Z3ML, If an equation in integer theory has more than one solution, how can I get all the solutions just like here in Z3Py?

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

just like the code sample above, how can I get all the models/solutions, which are {(x=0, y=0), (x=1, y=1), (x=2,y=2), (x=3, y=3)}

howareyouimfinethanks
  • 11
  • 2
  • There's no out-of-the-box function to do this, just like in any other API. You'll have to code it yourself. It'd be a translation of the Python code you linked to, as I believe all the API calls made there are available in the O'Caml interface. You'll get better help here on stack-overflow if you start with some code and post what difficulties (if any) you run into. – alias Mar 20 '21 at 17:42
  • yeah, just like the code I post, I want to get all the models of a linear integer equation through the function `get_all_models`(maybe have the form of list or else). That seems tough enough for me... – howareyouimfinethanks Mar 23 '21 at 09:11
  • You could be interested by [Frama-C](http://frama-c.com/) and by [RefPerSys](http://refpersys.org/) – Basile Starynkevitch Apr 09 '21 at 06:09

0 Answers0