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

remove deprecated functions from ML API. #1393

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-12-07 18:43:29 +05:30
parent 39d1ad3edb
commit 8e1ab23c3d
2 changed files with 0 additions and 87 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1975,56 +1975,6 @@ struct
(List.length assumptions) assumptions (List.length assumptions) assumptions
formula formula
let parse_smtlib_string (ctx:context) (str:string) (sort_names:Symbol.symbol list) (sorts:Sort.sort list) (decl_names:Symbol.symbol list) (decls:func_decl list) =
let csn = List.length sort_names in
let cs = List.length sorts in
let cdn = List.length decl_names in
let cd = List.length decls in
if (csn <> cs || cdn <> cd) then
raise (Error "Argument size mismatch")
else
Z3native.parse_smtlib_string ctx str
cs sort_names sorts cd decl_names decls
let parse_smtlib_file (ctx:context) (file_name:string) (sort_names:Symbol.symbol list) (sorts:Sort.sort list) (decl_names:Symbol.symbol list) (decls:func_decl list) =
let csn = (List.length sort_names) in
let cs = (List.length sorts) in
let cdn = (List.length decl_names) in
let cd = (List.length decls) in
if (csn <> cs || cdn <> cd) then
raise (Error "Argument size mismatch")
else
Z3native.parse_smtlib_file ctx file_name
cs sort_names sorts cd decl_names decls
let get_num_smtlib_formulas (ctx:context) = Z3native.get_smtlib_num_formulas ctx
let get_smtlib_formulas (ctx:context) =
let n = get_num_smtlib_formulas ctx in
let f i = Z3native.get_smtlib_formula ctx i in
mk_list f n
let get_num_smtlib_assumptions (ctx:context) = Z3native.get_smtlib_num_assumptions ctx
let get_smtlib_assumptions (ctx:context) =
let n = get_num_smtlib_assumptions ctx in
let f i = Z3native.get_smtlib_assumption ctx i in
mk_list f n
let get_num_smtlib_decls (ctx:context) = Z3native.get_smtlib_num_decls ctx
let get_smtlib_decls (ctx:context) =
let n = get_num_smtlib_decls ctx in
let f i = Z3native.get_smtlib_decl ctx i in
mk_list f n
let get_num_smtlib_sorts (ctx:context) = Z3native.get_smtlib_num_sorts ctx
let get_smtlib_sorts (ctx:context) =
let n = get_num_smtlib_sorts ctx in
let f i = Z3native.get_smtlib_sort ctx i in
mk_list f n
let parse_smtlib2_string (ctx:context) (str:string) (sort_names:Symbol.symbol list) (sorts:Sort.sort list) (decl_names:Symbol.symbol list) (decls:func_decl list) = let parse_smtlib2_string (ctx:context) (str:string) (sort_names:Symbol.symbol list) (sorts:Sort.sort list) (decl_names:Symbol.symbol list) (decls:func_decl list) =
let csn = List.length sort_names in let csn = List.length sort_names in
let cs = List.length sorts in let cs = List.length sorts in

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

@ -3441,43 +3441,6 @@ sig
@return A string representation of the benchmark. *) @return A string representation of the benchmark. *)
val benchmark_to_smtstring : context -> string -> string -> string -> string -> Expr.expr list -> Expr.expr -> string val benchmark_to_smtstring : context -> string -> string -> string -> string -> Expr.expr list -> Expr.expr -> string
(** Parse the given string using the SMT-LIB parser.
The symbol table of the parser can be initialized using the given sorts and declarations.
The symbols in the arrays in the third and fifth argument
don't need to match the names of the sorts and declarations in the arrays in the fourth
and sixth argument. This is a useful feature since we can use arbitrary names to
reference sorts and declarations. *)
val parse_smtlib_string : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> unit
(** Parse the given file using the SMT-LIB parser.
{!parse_smtlib_string} *)
val parse_smtlib_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> unit
(** The number of SMTLIB formulas parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
val get_num_smtlib_formulas : context -> int
(** The formulas parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
val get_smtlib_formulas : context -> Expr.expr list
(** The number of SMTLIB assumptions parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
val get_num_smtlib_assumptions : context -> int
(** The assumptions parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
val get_smtlib_assumptions : context -> Expr.expr list
(** The number of SMTLIB declarations parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
val get_num_smtlib_decls : context -> int
(** The declarations parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
val get_smtlib_decls : context -> FuncDecl.func_decl list
(** The number of SMTLIB sorts parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
val get_num_smtlib_sorts : context -> int
(** The sort declarations parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
val get_smtlib_sorts : context -> Sort.sort list
(** Parse the given string using the SMT-LIB2 parser. (** Parse the given string using the SMT-LIB2 parser.
{!parse_smtlib_string} {!parse_smtlib_string}