mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

add arguments to optimize_check fix #1866

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-14 20:39:54 -07:00
parent 5b51e69137
commit 0457b5a73f
2 changed files with 11 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/api/ml/z3.ml
View file

@ -705,6 +705,10 @@ struct
let mk_forall_const = _internal_mk_quantifier_const ~universal:true
let mk_exists = _internal_mk_quantifier ~universal:false
let mk_exists_const = _internal_mk_quantifier_const ~universal:false
let mk_lambda_const ctx bound body = Z3native.mk_lambda_const ctx (List.length bound) bound body
let mk_lambda ctx bound body =
let (names, sorts) = List.unzip bound in
Z3native.mk_lambda ctx (List.length bound) sorts names body
let mk_quantifier (ctx:context) (universal:bool) (sorts:Sort.sort list) (names:Symbol.symbol list) (body:expr) (weight:int option) (patterns:Pattern.pattern list) (nopatterns:expr list) (quantifier_id:Symbol.symbol option) (skolem_id:Symbol.symbol option) =
if universal then
@ -1947,7 +1951,7 @@ struct
let minimize (x:optimize) (e:Expr.expr) = mk_handle x (Z3native.optimize_minimize (gc x) x e)
let check (x:optimize) =
let r = lbool_of_int (Z3native.optimize_check (gc x) x) 0 [] in
let r = lbool_of_int (Z3native.optimize_check (gc x) x 0 []) 0 in
match r with
| L_TRUE -> Solver.SATISFIABLE
| L_FALSE -> Solver.UNSATISFIABLE

6
src/api/ml/z3.mli
View file

@ -736,6 +736,12 @@ sig
(** Create an existential Quantifier. *)
val mk_exists_const : context -> Expr.expr list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier
(** Create a lambda binding. *)
val mk_lambda_const : context -> Expr.expr list -> Expr.expr -> quantifier
(** Create a lambda binding where bound variables are given by symbols and sorts *)
val mk_lambda : context -> (Symbol.symbol * Sort.sort) list -> Expr.expr -> quantifier
(** Create a Quantifier. *)
val mk_quantifier : context -> Sort.sort list -> Symbol.symbol list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier