From 0457b5a73f2326202fb2cd35bc37e508d85e1d31 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 14 Oct 2018 20:39:54 -0700 Subject: [PATCH] add arguments to optimize_check fix #1866 Signed-off-by: Nikolaj Bjorner --- src/api/ml/z3.ml | 6 +++++- src/api/ml/z3.mli | 6 ++++++ 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 2ad07aee4..3c583eaef 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -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 diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 18ade29bf..ddc9f2a41 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -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