mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

fix ml build breakd #1659, #1660

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-05-29 07:37:27 -07:00
parent da0239d200
commit 6dc9c3a587
2 changed files with 1 additions and 98 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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

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

@ -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.