diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 5766c79f9..a676f8c43 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1654,7 +1654,6 @@ struct mk_list f n let get_subgoal (x:apply_result) (i:int) = Z3native.apply_result_get_subgoal (gc x) x i - let convert_model (x:apply_result) (i:int) (m:Model.model) = Z3native.apply_result_convert_model (gc x) x i m let to_string (x:apply_result) = Z3native.apply_result_to_string (gc x) x end @@ -1995,52 +1994,6 @@ struct cs sort_names sorts cd decl_names decls end -module Interpolation = -struct - let mk_interpolant = Z3native.mk_interpolant - - let mk_interpolation_context (settings:(string * string) list) = - let cfg = Z3native.mk_config () in - let f e = Z3native.set_param_value cfg (fst e) (snd e) in - List.iter f settings; - let res = Z3native.mk_interpolation_context cfg in - Z3native.del_config cfg; - Z3native.set_ast_print_mode res (int_of_ast_print_mode PRINT_SMTLIB2_COMPLIANT); - Z3native.set_internal_error_handler res; - res - - let get_interpolant (ctx:context) (pf:expr) (pat:expr) (p:Params.params) = - let av = Z3native.get_interpolant ctx pf pat p in - AST.ASTVector.to_expr_list av - - let compute_interpolant (ctx:context) (pat:expr) (p:Params.params) = - let (r, interp, model) = Z3native.compute_interpolant ctx pat p in - let res = lbool_of_int r in - match res with - | L_TRUE -> (res, None, Some model) - | L_FALSE -> (res, Some (AST.ASTVector.to_expr_list interp), None) - | _ -> (res, None, None) - - let get_interpolation_profile = Z3native.interpolation_profile - - let read_interpolation_problem (ctx:context) (filename:string) = - let (r, num, cnsts, parents, error, num_theory, theory) = - Z3native.read_interpolation_problem ctx filename - in - match r with - | 0 -> raise (Error "Interpolation problem could not be read.") - | _ -> (cnsts, parents, theory) - - let check_interpolant (ctx:context) (num:int) (cnsts:Expr.expr list) (parents:int list) (interps:Expr.expr list) (num_theory:int) (theory:Expr.expr list) = - let (r, str) = Z3native.check_interpolant ctx num cnsts parents interps num_theory theory in - match (lbool_of_int r) with - | L_UNDEF -> raise (Error "Interpolant could not be verified.") - | L_FALSE -> raise (Error "Interpolant could not be verified.") - | _ -> () - - let write_interpolation_problem (ctx:context) (num:int) (cnsts:Expr.expr list) (parents:int list) (filename:string) (num_theory:int) (theory:Expr.expr list) = - Z3native.write_interpolation_problem ctx num cnsts parents filename num_theory theory -end let set_global_param = Z3native.global_param_set diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 0fd1242ee..9b424b508 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -2447,7 +2447,7 @@ sig The antecedents are proofs for equalities used as substitution rules. The object is also used in a few cases. The cases are: - When applying contextual simplification (CONTEXT_SIMPLIFIER=true) - - When converting bit-vectors to Booleans (BIT2BOOL=true) + - When converting bit-vectors to Booleans (BIT2BOOL=true) *) val is_rewrite_star : Expr.expr -> bool (** Indicates whether the term is a proof for pulling quantifiers out. @@ -2964,11 +2964,6 @@ sig (** Retrieves a subgoal from the apply_result. *) val get_subgoal : apply_result -> int -> Goal.goal - (** Convert a model for a subgoal into a model for the original - goal [g], that the ApplyResult was obtained from. - #return A model for [g] *) - val convert_model : apply_result -> int -> Model.model -> Model.model - (** A string representation of the ApplyResult. *) val to_string : apply_result -> string end @@ -3424,51 +3419,6 @@ sig val parse_smtlib2_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> Expr.expr end -(** Interpolation *) -module Interpolation : -sig - - (** Create an AST node marking a formula position for interpolation. - The expression must have Boolean sort. *) - val mk_interpolant : context -> Expr.expr -> Expr.expr - - (** The interpolation context is suitable for generation of interpolants. - For more information on interpolation please refer - too the C/C++ API, which is well documented. *) - val mk_interpolation_context : (string * string) list -> context - - (** Gets an interpolant. - For more information on interpolation please refer - too the C/C++ API, which is well documented. *) - val get_interpolant : context -> Expr.expr -> Expr.expr -> Params.params -> Expr.expr list - - (** Computes an interpolant. - For more information on interpolation please refer - too the C/C++ API, which is well documented. *) - val compute_interpolant : context -> Expr.expr -> Params.params -> (Z3enums.lbool * Expr.expr list option * Model.model option) - - (** Retrieves an interpolation profile. - For more information on interpolation please refer - too the C/C++ API, which is well documented. *) - val get_interpolation_profile : context -> string - - (** Read an interpolation problem from file. - For more information on interpolation please refer - too the C/C++ API, which is well documented. *) - val read_interpolation_problem : context -> string -> (Expr.expr list * int list * Expr.expr list) - - (** Check the correctness of an interpolant. - For more information on interpolation please refer - too the C/C++ API, which is well documented. *) - val check_interpolant : context -> int -> Expr.expr list -> int list -> Expr.expr list -> int -> Expr.expr list -> unit - - (** Write an interpolation problem to file suitable for reading with - Z3_read_interpolation_problem. - For more information on interpolation please refer - too the C/C++ API, which is well documented. *) - val write_interpolation_problem : context -> int -> Expr.expr list -> int list -> string -> int -> Expr.expr list -> unit - -end (** Set a global (or module) parameter, which is shared by all Z3 contexts.