diff --git a/scripts/update_api.py b/scripts/update_api.py index febbf3eb2..fc0f1c939 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1079,7 +1079,7 @@ def def_API(name, result, params): def mk_bindings(): exe_c.write("void register_z3_replayer_cmds(z3_replayer & in) {\n") for key, val in API2Id.items(): - exe_c.write(" in.register_cmd(%s, exec_%s);\n" % (key, val)) + exe_c.write(" in.register_cmd(%s, exec_%s, \"%s\");\n" % (key, val, val)) exe_c.write("}\n") def ml_method_name(name): diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 9f0ddbaa8..944e447c6 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -776,6 +776,8 @@ extern "C" { SET_ERROR_CODE(Z3_SORT_ERROR); RETURN_Z3(of_expr(0)); } + SASSERT(from[i]->get_ref_count() > 0); + SASSERT(to[i]->get_ref_count() > 0); } expr_safe_replace subst(m); for (unsigned i = 0; i < num_exprs; i++) { diff --git a/src/api/api_ast_vector.cpp b/src/api/api_ast_vector.cpp index e1d4d78ff..d6ff1bbb3 100644 --- a/src/api/api_ast_vector.cpp +++ b/src/api/api_ast_vector.cpp @@ -26,6 +26,7 @@ Revision History: extern "C" { Z3_ast_vector Z3_API Z3_mk_ast_vector(Z3_context c) { + std::cout << "ast-vector\n"; Z3_TRY; LOG_Z3_mk_ast_vector(c); RESET_ERROR_CODE(); diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 4d8484ced..8d2bc5b50 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -3822,6 +3822,7 @@ public class Context extends IDisposable m_Params_DRQ.clear(this); m_Probe_DRQ.clear(this); m_Solver_DRQ.clear(this); + m_Optimize_DRQ.clear(this); m_Statistics_DRQ.clear(this); m_Tactic_DRQ.clear(this); m_Fixedpoint_DRQ.clear(this); diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 84c70001e..8fdc795fb 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -60,7 +60,7 @@ struct o.inc_ref (context_gno ctx) no ; ( if not (is_null o.m_n_obj) then - o.dec_ref (context_gno ctx) o.m_n_obj ; + o.dec_ref (context_gno ctx) o.m_n_obj ; (context_sub1 ctx) ) ; o.m_n_obj <- no @@ -68,8 +68,8 @@ struct let z3obj_dispose o = if not (is_null o.m_n_obj) then ( - o.dec_ref (z3obj_gnc o) o.m_n_obj ; - (context_sub1 (z3obj_gc o)) + o.dec_ref (z3obj_gnc o) o.m_n_obj ; + (context_sub1 (z3obj_gc o)) ) ; o.m_n_obj <- null @@ -81,12 +81,12 @@ struct let z3_native_object_of_ast_ptr : context -> Z3native.ptr -> z3_native_object = fun ctx no -> let res : z3_native_object = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.inc_ref ; - dec_ref = Z3native.dec_ref } in + m_n_obj = null ; + inc_ref = Z3native.inc_ref ; + dec_ref = Z3native.dec_ref } in (z3obj_sno res ctx no) ; (z3obj_create res) ; - res + res end open Internal @@ -137,18 +137,18 @@ struct let create_i ( ctx : context ) ( no : Z3native.ptr ) = let res : symbol = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = z3obj_nil_ref ; - dec_ref = z3obj_nil_ref } in + m_n_obj = null ; + inc_ref = z3obj_nil_ref ; + dec_ref = z3obj_nil_ref } in (z3obj_sno res ctx no) ; (z3obj_create res) ; res let create_s ( ctx : context ) ( no : Z3native.ptr ) = let res : symbol = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = z3obj_nil_ref ; - dec_ref = z3obj_nil_ref } in + m_n_obj = null ; + inc_ref = z3obj_nil_ref ; + dec_ref = z3obj_nil_ref } in (z3obj_sno res ctx no) ; (z3obj_create res) ; res @@ -156,7 +156,7 @@ struct let create ( ctx : context ) ( no : Z3native.ptr ) = match (symbol_kind_of_int (Z3native.get_symbol_kind (context_gno ctx) no)) with | INT_SYMBOL -> (create_i ctx no) - | STRING_SYMBOL -> (create_s ctx no) + | STRING_SYMBOL -> (create_s ctx no) let gc ( x : symbol ) = (z3obj_gc x) let gnc ( x : symbol ) = (z3obj_gnc x) @@ -264,16 +264,16 @@ end = struct module ASTVector = struct type ast_vector = z3_native_object - + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : ast_vector = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.ast_vector_inc_ref ; - dec_ref = Z3native.ast_vector_dec_ref } in + m_n_obj = null ; + inc_ref = Z3native.ast_vector_inc_ref ; + dec_ref = Z3native.ast_vector_dec_ref } in (z3obj_sno res ctx no) ; (z3obj_create res) ; res - + let mk_ast_vector ( ctx : context ) = (create ctx (Z3native.mk_ast_vector (context_gno ctx))) let get_size ( x : ast_vector ) = @@ -287,69 +287,69 @@ end = struct let resize ( x : ast_vector ) ( new_size : int ) = Z3native.ast_vector_resize (z3obj_gnc x) (z3obj_gno x) new_size - + let push ( x : ast_vector ) ( a : ast ) = Z3native.ast_vector_push (z3obj_gnc x) (z3obj_gno x) (z3obj_gno a) - + let translate ( x : ast_vector ) ( to_ctx : context ) = create to_ctx (Z3native.ast_vector_translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx)) let to_list ( x : ast_vector ) = - let xs = (get_size x) in + let xs = (get_size x) in let f i = (get x i) in mk_list f xs let to_expr_list ( x : ast_vector ) = - let xs = (get_size x) in + let xs = (get_size x) in let f i = (Expr.expr_of_ptr (z3obj_gc x) (z3obj_gno (get x i))) in mk_list f xs - + let to_string ( x : ast_vector ) = Z3native.ast_vector_to_string (z3obj_gnc x) (z3obj_gno x) end module ASTMap = - struct + struct type ast_map = z3_native_object - + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : ast_map = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.ast_map_inc_ref ; - dec_ref = Z3native.ast_map_dec_ref } in + m_n_obj = null ; + inc_ref = Z3native.ast_map_inc_ref ; + dec_ref = Z3native.ast_map_dec_ref } in (z3obj_sno res ctx no) ; (z3obj_create res) ; - res - + res + let mk_ast_map ( ctx : context ) = (create ctx (Z3native.mk_ast_map (context_gno ctx))) let astmap_of_ptr ( ctx : context ) ( no : Z3native.ptr ) = let res : ast_map = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.ast_map_inc_ref ; - dec_ref = Z3native.ast_map_dec_ref } in + m_n_obj = null ; + inc_ref = Z3native.ast_map_inc_ref ; + dec_ref = Z3native.ast_map_dec_ref } in (z3obj_sno res ctx no) ; (z3obj_create res) ; res - + let contains ( x : ast_map ) ( key : ast ) = Z3native.ast_map_contains (z3obj_gnc x) (z3obj_gno x) (z3obj_gno key) - + let find ( x : ast_map ) ( key : ast ) = ast_of_ptr (z3obj_gc x) (Z3native.ast_map_find (z3obj_gnc x) (z3obj_gno x) (z3obj_gno key)) - + let insert ( x : ast_map ) ( key : ast ) ( value : ast ) = Z3native.ast_map_insert (z3obj_gnc x) (z3obj_gno x) (z3obj_gno key) (z3obj_gno value) let erase ( x : ast_map ) ( key : ast ) = Z3native.ast_map_erase (z3obj_gnc x) (z3obj_gno x) (z3obj_gno key) - + let reset ( x : ast_map ) = Z3native.ast_map_reset (z3obj_gnc x) (z3obj_gno x) let get_size ( x : ast_map ) = Z3native.ast_map_size (z3obj_gnc x) (z3obj_gno x) - + let get_keys ( x : ast_map ) = let av = ASTVector.create (z3obj_gc x) (Z3native.ast_map_keys (z3obj_gnc x) (z3obj_gno x)) in (ASTVector.to_list av) @@ -369,7 +369,7 @@ end = struct | QUANTIFIER_AST | VAR_AST -> true | _ -> false - + let is_app ( x : ast ) = (get_ast_kind x) == APP_AST let is_var ( x : ast ) = (get_ast_kind x) == VAR_AST let is_quantifier ( x : ast ) = (get_ast_kind x) == QUANTIFIER_AST @@ -385,12 +385,12 @@ end = struct false else Z3native.is_eq_ast (z3obj_gnc a) (z3obj_gno a) (z3obj_gno b) - + let compare a b = if (get_id a) < (get_id b) then -1 else if (get_id a) > (get_id b) then 1 else - 0 - + 0 + let translate ( x : ast ) ( to_ctx : context ) = if (z3obj_gnc x) == (context_gno to_ctx) then x @@ -456,11 +456,11 @@ end = struct let equal : sort -> sort -> bool = fun a b -> (a == b) || if (gnc a) != (gnc b) then - false + false else - (Z3native.is_eq_sort (gnc a) (gno a) (gno b)) + (Z3native.is_eq_sort (gnc a) (gno a) (gno b)) - + let get_id ( x : sort ) = Z3native.get_sort_id (gnc x) (gno x) let get_sort_kind ( x : sort ) = (sort_kind_of_int (Z3native.get_sort_kind (gnc x) (gno x))) let get_name ( x : sort ) = (Symbol.create (gc x) (Z3native.get_sort_name (gnc x) (gno x))) @@ -468,9 +468,9 @@ end = struct let mk_uninterpreted ( ctx : context ) ( s : Symbol.symbol ) = let res = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.inc_ref ; - dec_ref = Z3native.dec_ref } in + m_n_obj = null ; + inc_ref = Z3native.inc_ref ; + dec_ref = Z3native.dec_ref } in (z3obj_sno res ctx (Z3native.mk_uninterpreted_sort (context_gno ctx) (Symbol.gno s))) ; (z3obj_create res) ; Sort(res) @@ -490,14 +490,14 @@ sig module Parameter : sig type parameter = - P_Int of int + P_Int of int | P_Dbl of float | P_Sym of Symbol.symbol | P_Srt of Sort.sort | P_Ast of AST.ast | P_Fdl of func_decl | P_Rat of string - + val get_kind : parameter -> Z3enums.parameter_kind val get_int : parameter -> int val get_float : parameter -> float @@ -538,18 +538,18 @@ end = struct let create_ndr ( ctx : context ) ( name : Symbol.symbol ) ( domain : Sort.sort list ) ( range : Sort.sort ) = let res = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.inc_ref ; - dec_ref = Z3native.dec_ref } in + m_n_obj = null ; + inc_ref = Z3native.inc_ref ; + dec_ref = Z3native.dec_ref } in (z3obj_sno res ctx (Z3native.mk_func_decl (context_gno ctx) (Symbol.gno name) (List.length domain) (Sort.sort_lton domain) (Sort.gno range))) ; (z3obj_create res) ; FuncDecl(res) let create_pdr ( ctx : context) ( prefix : string ) ( domain : Sort.sort list ) ( range : Sort.sort ) = let res = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.inc_ref ; - dec_ref = Z3native.dec_ref } in + m_n_obj = null ; + inc_ref = Z3native.inc_ref ; + dec_ref = Z3native.dec_ref } in (z3obj_sno res ctx (Z3native.mk_fresh_func_decl (context_gno ctx) prefix (List.length domain) (Sort.sort_lton domain) (Sort.gno range))) ; (z3obj_create res) ; FuncDecl(res) @@ -568,51 +568,51 @@ end = struct | P_Ast of AST.ast | P_Fdl of func_decl | P_Rat of string - + let get_kind ( x : parameter ) = (match x with - | P_Int(_) -> PARAMETER_INT - | P_Dbl(_) -> PARAMETER_DOUBLE - | P_Sym(_) -> PARAMETER_SYMBOL - | P_Srt(_) -> PARAMETER_SORT - | P_Ast(_) -> PARAMETER_AST - | P_Fdl(_) -> PARAMETER_FUNC_DECL - | P_Rat(_) -> PARAMETER_RATIONAL) - + | P_Int(_) -> PARAMETER_INT + | P_Dbl(_) -> PARAMETER_DOUBLE + | P_Sym(_) -> PARAMETER_SYMBOL + | P_Srt(_) -> PARAMETER_SORT + | P_Ast(_) -> PARAMETER_AST + | P_Fdl(_) -> PARAMETER_FUNC_DECL + | P_Rat(_) -> PARAMETER_RATIONAL) + let get_int ( x : parameter ) = match x with - | P_Int(x) -> x - | _ -> raise (Z3native.Exception "parameter is not an int") - + | P_Int(x) -> x + | _ -> raise (Z3native.Exception "parameter is not an int") + let get_float ( x : parameter ) = match x with - | P_Dbl(x) -> x - | _ -> raise (Z3native.Exception "parameter is not a float") + | P_Dbl(x) -> x + | _ -> raise (Z3native.Exception "parameter is not a float") let get_symbol ( x : parameter ) = match x with - | P_Sym(x) -> x - | _ -> raise (Z3native.Exception "parameter is not a symbol") - + | P_Sym(x) -> x + | _ -> raise (Z3native.Exception "parameter is not a symbol") + let get_sort ( x : parameter ) = match x with - | P_Srt(x) -> x - | _ -> raise (Z3native.Exception "parameter is not a sort") + | P_Srt(x) -> x + | _ -> raise (Z3native.Exception "parameter is not a sort") let get_ast ( x : parameter ) = match x with - | P_Ast(x) -> x - | _ -> raise (Z3native.Exception "parameter is not an ast") + | P_Ast(x) -> x + | _ -> raise (Z3native.Exception "parameter is not an ast") let get_func_decl ( x : parameter ) = match x with - | P_Fdl(x) -> x - | _ -> raise (Z3native.Exception "parameter is not a func_decl") + | P_Fdl(x) -> x + | _ -> raise (Z3native.Exception "parameter is not a func_decl") let get_rational ( x : parameter ) = match x with - | P_Rat(x) -> x - | _ -> raise (Z3native.Exception "parameter is not a rational string") + | P_Rat(x) -> x + | _ -> raise (Z3native.Exception "parameter is not a rational string") end let mk_func_decl ( ctx : context ) ( name : Symbol.symbol ) ( domain : Sort.sort list ) ( range : Sort.sort ) = @@ -710,19 +710,19 @@ end = struct let param_descrs_of_ptr ( ctx : context ) ( no : Z3native.ptr ) = let res : param_descrs = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.param_descrs_inc_ref ; - dec_ref = Z3native.param_descrs_dec_ref } in + m_n_obj = null ; + inc_ref = Z3native.param_descrs_inc_ref ; + dec_ref = Z3native.param_descrs_dec_ref } in (z3obj_sno res ctx no) ; (z3obj_create res) ; res - + let validate ( x : param_descrs ) ( p : params ) = Z3native.params_validate (z3obj_gnc x) (z3obj_gno p) (z3obj_gno x) - + let get_kind ( x : param_descrs ) ( name : Symbol.symbol ) = (param_kind_of_int (Z3native.param_descrs_get_kind (z3obj_gnc x) (z3obj_gno x) (Symbol.gno name))) - + let get_names ( x : param_descrs ) = let n = Z3native.param_descrs_size (z3obj_gnc x) (z3obj_gno x) in let f i = Symbol.create (z3obj_gc x) (Z3native.param_descrs_get_name (z3obj_gnc x) (z3obj_gno x) i) in @@ -746,9 +746,9 @@ end = struct let mk_params ( ctx : context ) = let res : params = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.params_inc_ref ; - dec_ref = Z3native.params_dec_ref } in + m_n_obj = null ; + inc_ref = Z3native.params_inc_ref ; + dec_ref = Z3native.params_dec_ref } in (z3obj_sno res ctx (Z3native.mk_params (context_gno ctx))) ; (z3obj_create res) ; res @@ -807,32 +807,30 @@ end = struct let gno e = match e with Expr(a) -> (z3obj_gno a) let expr_of_ptr : context -> Z3native.ptr -> expr = fun ctx no -> + let e = z3_native_object_of_ast_ptr ctx no in if ast_kind_of_int (Z3native.get_ast_kind (context_gno ctx) no) == QUANTIFIER_AST then - Expr(z3_native_object_of_ast_ptr ctx no) + Expr(e) else let s = Z3native.get_sort (context_gno ctx) no in let sk = (sort_kind_of_int (Z3native.get_sort_kind (context_gno ctx) s)) in if (Z3native.is_algebraic_number (context_gno ctx) no) then - Expr(z3_native_object_of_ast_ptr ctx no) - else - if (Z3native.is_numeral_ast (context_gno ctx) no) then - match sk with - | REAL_SORT - | BOOL_SORT - | ARRAY_SORT - | BV_SORT - | ROUNDING_MODE_SORT - | RELATION_SORT - | UNINTERPRETED_SORT - | FLOATING_POINT_SORT - | INT_SORT - | DATATYPE_SORT - | FINITE_DOMAIN_SORT -> - Expr(z3_native_object_of_ast_ptr ctx no) - | _ -> - raise (Z3native.Exception "Unsupported numeral object") - else - Expr(z3_native_object_of_ast_ptr ctx no) + Expr(e) + else if (Z3native.is_numeral_ast (context_gno ctx) no) then + match sk with + | REAL_SORT + | BOOL_SORT + | ARRAY_SORT + | BV_SORT + | ROUNDING_MODE_SORT + | RELATION_SORT + | UNINTERPRETED_SORT + | FLOATING_POINT_SORT + | INT_SORT + | DATATYPE_SORT + | FINITE_DOMAIN_SORT -> Expr(e) + | _ -> raise (Z3native.Exception "Unsupported numeral object") + else + Expr(e) let expr_of_ast a = let q = (Z3enums.ast_kind_of_int (Z3native.get_ast_kind (z3obj_gnc a) (z3obj_gno a))) in @@ -866,9 +864,9 @@ end = struct let get_num_args ( x : expr ) = Z3native.get_app_num_args (gnc x) (gno x) let get_args ( x : expr ) = let n = (get_num_args x) in - let f i = expr_of_ptr (Expr.gc x) (Z3native.get_app_arg (gnc x) (gno x) i) in - mk_list f n - + let f i = expr_of_ptr (Expr.gc x) (Z3native.get_app_arg (gnc x) (gno x) i) in + mk_list f n + let update ( x : expr ) ( args : expr list ) = if ((AST.is_app (ast_of_expr x)) && (List.length args <> (get_num_args x))) then raise (Z3native.Exception "Number of arguments does not match") @@ -880,7 +878,7 @@ end = struct raise (Z3native.Exception "Argument sizes do not match") else expr_of_ptr (Expr.gc x) (Z3native.substitute (gnc x) (gno x) (List.length from) (expr_lton from) (expr_lton to_)) - + let substitute_one ( x : expr ) from to_ = substitute ( x : expr ) [ from ] [ to_ ] @@ -1012,10 +1010,10 @@ struct match e with Expr.Expr(a) -> let q = (Z3enums.ast_kind_of_int (Z3native.get_ast_kind (z3obj_gnc a) (z3obj_gno a))) in if (q != Z3enums.QUANTIFIER_AST) then - raise (Z3native.Exception "Invalid coercion") + raise (Z3native.Exception "Invalid coercion") else - Quantifier(e) - + Quantifier(e) + let gc ( x : quantifier ) = match (x) with Quantifier(e) -> (Expr.gc e) let gnc ( x : quantifier ) = match (x) with Quantifier(e) -> (Expr.gnc e) let gno ( x : quantifier ) = match (x) with Quantifier(e) -> (Expr.gno e) @@ -1023,25 +1021,25 @@ struct module Pattern = struct type pattern = Pattern of AST.ast - + let ast_of_pattern e = match e with Pattern(x) -> x let pattern_of_ast a = (* CMW: Unchecked ok? *) Pattern(a) - + let gc ( x : pattern ) = match (x) with Pattern(a) -> (z3obj_gc a) let gnc ( x : pattern ) = match (x) with Pattern(a) -> (z3obj_gnc a) let gno ( x : pattern ) = match (x) with Pattern(a) -> (z3obj_gno a) let get_num_terms ( x : pattern ) = - Z3native.get_pattern_num_terms (gnc x) (gno x) + Z3native.get_pattern_num_terms (gnc x) (gno x) let get_terms ( x : pattern ) = let n = (get_num_terms x) in let f i = (expr_of_ptr (gc x) (Z3native.get_pattern (gnc x) (gno x) i)) in mk_list f n - + let to_string ( x : pattern ) = Z3native.pattern_to_string (gnc x) (gno x) end @@ -1101,76 +1099,76 @@ struct raise (Z3native.Exception "Number of sorts does not match number of names") else if ((List.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then Quantifier(expr_of_ptr ctx (Z3native.mk_quantifier (context_gno ctx) true - (match weight with | None -> 1 | Some(x) -> x) - (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns))) - (List.length sorts) (Sort.sort_lton sorts) - (Symbol.symbol_lton names) - (Expr.gno body))) + (match weight with | None -> 1 | Some(x) -> x) + (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns))) + (List.length sorts) (Sort.sort_lton sorts) + (Symbol.symbol_lton names) + (Expr.gno body))) else Quantifier(expr_of_ptr ctx (Z3native.mk_quantifier_ex (context_gno ctx) true - (match weight with | None -> 1 | Some(x) -> x) - (match quantifier_id with | None -> null | Some(x) -> (Symbol.gno x)) - (match skolem_id with | None -> null | Some(x) -> (Symbol.gno x)) - (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns))) - (List.length nopatterns) (expr_lton nopatterns) - (List.length sorts) (Sort.sort_lton sorts) - (Symbol.symbol_lton names) - (Expr.gno body))) - + (match weight with | None -> 1 | Some(x) -> x) + (match quantifier_id with | None -> null | Some(x) -> (Symbol.gno x)) + (match skolem_id with | None -> null | Some(x) -> (Symbol.gno x)) + (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns))) + (List.length nopatterns) (expr_lton nopatterns) + (List.length sorts) (Sort.sort_lton sorts) + (Symbol.symbol_lton names) + (Expr.gno body))) + let mk_forall_const ( ctx : context ) ( bound_constants : expr list ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern list ) ( nopatterns : expr list ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = if ((List.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then Quantifier(expr_of_ptr ctx (Z3native.mk_quantifier_const (context_gno ctx) true - (match weight with | None -> 1 | Some(x) -> x) - (List.length bound_constants) (expr_lton bound_constants) - (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns))) - (Expr.gno body))) + (match weight with | None -> 1 | Some(x) -> x) + (List.length bound_constants) (expr_lton bound_constants) + (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns))) + (Expr.gno body))) else Quantifier(expr_of_ptr ctx (Z3native.mk_quantifier_const_ex (context_gno ctx) true - (match weight with | None -> 1 | Some(x) -> x) - (match quantifier_id with | None -> null | Some(x) -> (Symbol.gno x)) - (match skolem_id with | None -> null | Some(x) -> (Symbol.gno x)) - (List.length bound_constants) (expr_lton bound_constants) - (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns))) - (List.length nopatterns) (expr_lton nopatterns) - (Expr.gno body))) + (match weight with | None -> 1 | Some(x) -> x) + (match quantifier_id with | None -> null | Some(x) -> (Symbol.gno x)) + (match skolem_id with | None -> null | Some(x) -> (Symbol.gno x)) + (List.length bound_constants) (expr_lton bound_constants) + (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns))) + (List.length nopatterns) (expr_lton nopatterns) + (Expr.gno body))) let mk_exists ( ctx : context ) ( 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 (List.length sorts) != (List.length names) then raise (Z3native.Exception "Number of sorts does not match number of names") else if ((List.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then Quantifier(expr_of_ptr ctx (Z3native.mk_quantifier (context_gno ctx) false - (match weight with | None -> 1 | Some(x) -> x) - (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns))) - (List.length sorts) (Sort.sort_lton sorts) - (Symbol.symbol_lton names) - (Expr.gno body))) + (match weight with | None -> 1 | Some(x) -> x) + (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns))) + (List.length sorts) (Sort.sort_lton sorts) + (Symbol.symbol_lton names) + (Expr.gno body))) else Quantifier(expr_of_ptr ctx (Z3native.mk_quantifier_ex (context_gno ctx) false - (match weight with | None -> 1 | Some(x) -> x) - (match quantifier_id with | None -> null | Some(x) -> (Symbol.gno x)) - (match skolem_id with | None -> null | Some(x) -> (Symbol.gno x)) - (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns))) - (List.length nopatterns) (expr_lton nopatterns) - (List.length sorts) (Sort.sort_lton sorts) - (Symbol.symbol_lton names) - (Expr.gno body))) - + (match weight with | None -> 1 | Some(x) -> x) + (match quantifier_id with | None -> null | Some(x) -> (Symbol.gno x)) + (match skolem_id with | None -> null | Some(x) -> (Symbol.gno x)) + (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns))) + (List.length nopatterns) (expr_lton nopatterns) + (List.length sorts) (Sort.sort_lton sorts) + (Symbol.symbol_lton names) + (Expr.gno body))) + let mk_exists_const ( ctx : context ) ( bound_constants : expr list ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern list ) ( nopatterns : expr list ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = if ((List.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then Quantifier(expr_of_ptr ctx (Z3native.mk_quantifier_const (context_gno ctx) false - (match weight with | None -> 1 | Some(x) -> x) - (List.length bound_constants) (expr_lton bound_constants) - (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns))) - (Expr.gno body))) + (match weight with | None -> 1 | Some(x) -> x) + (List.length bound_constants) (expr_lton bound_constants) + (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns))) + (Expr.gno body))) else Quantifier(expr_of_ptr ctx (Z3native.mk_quantifier_const_ex (context_gno ctx) false - (match weight with | None -> 1 | Some(x) -> x) - (match quantifier_id with | None -> null | Some(x) -> (Symbol.gno x)) - (match skolem_id with | None -> null | Some(x) -> (Symbol.gno x)) - (List.length bound_constants) (expr_lton bound_constants) - (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns))) - (List.length nopatterns) (expr_lton nopatterns) - (Expr.gno body))) + (match weight with | None -> 1 | Some(x) -> x) + (match quantifier_id with | None -> null | Some(x) -> (Symbol.gno x)) + (match skolem_id with | None -> null | Some(x) -> (Symbol.gno x)) + (List.length bound_constants) (expr_lton bound_constants) + (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns))) + (List.length nopatterns) (expr_lton nopatterns) + (Expr.gno 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 @@ -1209,7 +1207,7 @@ struct let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( domain : Sort.sort ) ( range : Sort.sort ) = (Expr.mk_const ctx name (mk_sort ctx domain range)) - let mk_const_s ( ctx : context ) ( name : string ) ( domain : Sort.sort ) ( range : Sort.sort ) = + let mk_const_s ( ctx : context ) ( name : string ) ( domain : Sort.sort ) ( range : Sort.sort ) = mk_const ctx (Symbol.mk_string ctx name) domain range let mk_select ( ctx : context ) ( a : expr ) ( i : expr ) = @@ -1229,7 +1227,7 @@ struct expr_of_ptr ctx (Z3native.mk_array_default (context_gno ctx) (Expr.gno arg)) let mk_array_ext ( ctx : context) ( arg1 : expr ) ( arg2 : expr ) = - expr_of_ptr ctx (Z3native.mk_array_ext (context_gno ctx) (Expr.gno arg1) (Expr.gno arg2)) + expr_of_ptr ctx (Z3native.mk_array_ext (context_gno ctx) (Expr.gno arg1) (Expr.gno arg2)) end @@ -1305,7 +1303,7 @@ struct let is_relation ( x : expr ) = let nc = (Expr.gnc x) in ((Z3native.is_app (Expr.gnc x) (Expr.gno x)) && - (sort_kind_of_int (Z3native.get_sort_kind nc (Z3native.get_sort nc (Expr.gno x))) == RELATION_SORT)) + (sort_kind_of_int (Z3native.get_sort_kind nc (Z3native.get_sort nc (Expr.gno x))) == RELATION_SORT)) let is_store ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_STORE) let is_empty ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_EMPTY) @@ -1335,7 +1333,7 @@ struct module Constructor = struct type constructor = z3_native_object - + module FieldNumTable = Hashtbl.Make(struct type t = AST.ast let equal x y = AST.compare x y = 0 @@ -1347,28 +1345,28 @@ struct let create ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : Sort.sort option list ) ( sort_refs : int list ) = let n = (List.length field_names) in if n != (List.length sorts) then - raise (Z3native.Exception "Number of field names does not match number of sorts") + raise (Z3native.Exception "Number of field names does not match number of sorts") else - if n != (List.length sort_refs) then - raise (Z3native.Exception "Number of field names does not match number of sort refs") - else + if n != (List.length sort_refs) then + raise (Z3native.Exception "Number of field names does not match number of sort refs") + else let ptr = (Z3native.mk_constructor (context_gno ctx) (Symbol.gno name) - (Symbol.gno recognizer) - n - (Symbol.symbol_lton field_names) - (Sort.sort_option_lton sorts) - (Array.of_list sort_refs)) in - let no : constructor = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = z3obj_nil_ref ; - dec_ref = z3obj_nil_ref} in - (z3obj_sno no ctx ptr) ; - (z3obj_create no) ; - let f = fun o -> Z3native.del_constructor (z3obj_gnc o) (z3obj_gno o) in - Gc.finalise f no ; - FieldNumTable.add _field_nums no n ; - no - + (Symbol.gno recognizer) + n + (Symbol.symbol_lton field_names) + (Sort.sort_option_lton sorts) + (Array.of_list sort_refs)) in + let no : constructor = { m_ctx = ctx ; + m_n_obj = null ; + inc_ref = z3obj_nil_ref ; + dec_ref = z3obj_nil_ref} in + (z3obj_sno no ctx ptr) ; + (z3obj_create no) ; + let f = fun o -> Z3native.del_constructor (z3obj_gnc o) (z3obj_gno o) in + Gc.finalise f no ; + FieldNumTable.add _field_nums no n ; + no + let get_num_fields ( x : constructor ) = FieldNumTable.find _field_nums x let get_constructor_decl ( x : constructor ) = @@ -1377,13 +1375,13 @@ struct let get_tester_decl ( x : constructor ) = let (_, b, _) = (Z3native.query_constructor (z3obj_gnc x) (z3obj_gno x) (get_num_fields x)) in - func_decl_of_ptr (z3obj_gc x) b + func_decl_of_ptr (z3obj_gc x) b let get_accessor_decls ( x : constructor ) = let (_, _, c) = (Z3native.query_constructor (z3obj_gnc x) (z3obj_gno x) (get_num_fields x)) in let f i = func_decl_of_ptr (z3obj_gc x) (Array.get c i) in mk_list f (Array.length c) - + end module ConstructorList = @@ -1392,9 +1390,9 @@ struct let create ( ctx : context ) ( c : Constructor.constructor list ) = let res : constructor_list = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = z3obj_nil_ref ; - dec_ref = z3obj_nil_ref} in + m_n_obj = null ; + inc_ref = z3obj_nil_ref ; + dec_ref = z3obj_nil_ref} in let f x =(z3obj_gno x) in (z3obj_sno res ctx (Z3native.mk_constructor_list (context_gno ctx) (List.length c) (Array.of_list (List.map f c)))) ; (z3obj_create res) ; @@ -1429,8 +1427,8 @@ struct let mk_sorts_s ( ctx : context ) ( names : string list ) ( c : Constructor.constructor list list ) = mk_sorts ctx ( - let f e = (Symbol.mk_string ctx e) in - List.map f names + let f e = (Symbol.mk_string ctx e) in + List.map f names ) c @@ -1600,27 +1598,27 @@ struct let get_big_int ( x : expr ) = if (is_int_numeral x) then - let s = (Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)) in - (Big_int.big_int_of_string s) + let s = (Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)) in + (Big_int.big_int_of_string s) else raise (Z3native.Exception "Conversion failed.") - + let numeral_to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x) let mk_const ( ctx : context ) ( name : Symbol.symbol ) = Expr.mk_const ctx name (mk_sort ctx) - + let mk_const_s ( ctx : context ) ( name : string ) = mk_const ctx (Symbol.mk_string ctx name) - + let mk_mod ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = expr_of_ptr ctx (Z3native.mk_mod (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - + let mk_rem ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = expr_of_ptr ctx (Z3native.mk_rem (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) let mk_numeral_s ( ctx : context ) ( v : string ) = expr_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (Sort.gno (mk_sort ctx))) - + let mk_numeral_i ( ctx : context ) ( v : int ) = expr_of_ptr ctx (Z3native.mk_int (context_gno ctx) v (Sort.gno (mk_sort ctx))) @@ -1634,60 +1632,60 @@ struct module Real = struct let mk_sort ( ctx : context ) = - Sort.sort_of_ptr ctx (Z3native.mk_real_sort (context_gno ctx)) + Sort.sort_of_ptr ctx (Z3native.mk_real_sort (context_gno ctx)) let get_numerator ( x : expr ) = expr_of_ptr (Expr.gc x) (Z3native.get_numerator (Expr.gnc x) (Expr.gno x)) - + let get_denominator ( x : expr ) = expr_of_ptr (Expr.gc x) (Z3native.get_denominator (Expr.gnc x) (Expr.gno x)) - + let get_ratio ( x : expr ) = if (is_rat_numeral x) then - let s = (Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)) in - (Ratio.ratio_of_string s) + let s = (Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)) in + (Ratio.ratio_of_string s) else raise (Z3native.Exception "Conversion failed.") let to_decimal_string ( x : expr ) ( precision : int ) = Z3native.get_numeral_decimal_string (Expr.gnc x) (Expr.gno x) precision - + let numeral_to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x) let mk_const ( ctx : context ) ( name : Symbol.symbol ) = Expr.mk_const ctx name (mk_sort ctx) - + let mk_const_s ( ctx : context ) ( name : string ) = mk_const ctx (Symbol.mk_string ctx name) let mk_numeral_nd ( ctx : context ) ( num : int ) ( den : int ) = if (den == 0) then - raise (Z3native.Exception "Denominator is zero") + raise (Z3native.Exception "Denominator is zero") else - expr_of_ptr ctx (Z3native.mk_real (context_gno ctx) num den) - + expr_of_ptr ctx (Z3native.mk_real (context_gno ctx) num den) + let mk_numeral_s ( ctx : context ) ( v : string ) = expr_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (Sort.gno (mk_sort ctx))) - + let mk_numeral_i ( ctx : context ) ( v : int ) = expr_of_ptr ctx (Z3native.mk_int (context_gno ctx) v (Sort.gno (mk_sort ctx))) - + let mk_is_integer ( ctx : context ) ( t : expr ) = (expr_of_ptr ctx (Z3native.mk_is_int (context_gno ctx) (Expr.gno t))) - + let mk_real2int ( ctx : context ) ( t : expr ) = (expr_of_ptr ctx (Z3native.mk_real2int (context_gno ctx) (Expr.gno t))) module AlgebraicNumber = struct let to_upper ( x : expr ) ( precision : int ) = - expr_of_ptr (Expr.gc x) (Z3native.get_algebraic_number_upper (Expr.gnc x) (Expr.gno x) precision) - + expr_of_ptr (Expr.gc x) (Z3native.get_algebraic_number_upper (Expr.gnc x) (Expr.gno x) precision) + let to_lower ( x : expr ) precision = - expr_of_ptr (Expr.gc x) (Z3native.get_algebraic_number_lower (Expr.gnc x) (Expr.gno x) precision) - + expr_of_ptr (Expr.gc x) (Z3native.get_algebraic_number_lower (Expr.gnc x) (Expr.gno x) precision) + let to_decimal_string ( x : expr ) ( precision : int ) = - Z3native.get_numeral_decimal_string (Expr.gnc x) (Expr.gno x) precision - + Z3native.get_numeral_decimal_string (Expr.gnc x) (Expr.gno x) precision + let numeral_to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x) end end @@ -1843,9 +1841,9 @@ struct let mk_sge ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = (expr_of_ptr ctx (Z3native.mk_bvsge (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) let mk_ugt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvugt (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) + (expr_of_ptr ctx (Z3native.mk_bvugt (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) let mk_sgt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvsgt (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) + (expr_of_ptr ctx (Z3native.mk_bvsgt (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) let mk_concat ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = expr_of_ptr ctx (Z3native.mk_concat (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) let mk_extract ( ctx : context ) ( high : int ) ( low : int ) ( t : expr ) = @@ -1857,7 +1855,7 @@ struct let mk_repeat ( ctx : context ) ( i : int ) ( t : expr ) = expr_of_ptr ctx (Z3native.mk_repeat (context_gno ctx) i (Expr.gno t)) let mk_shl ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvshl (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) + expr_of_ptr ctx (Z3native.mk_bvshl (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) let mk_lshr ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = expr_of_ptr ctx (Z3native.mk_bvlshr (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) let mk_ashr ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = @@ -1869,15 +1867,15 @@ struct let mk_ext_rotate_left ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = expr_of_ptr ctx (Z3native.mk_ext_rotate_left (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) let mk_ext_rotate_right ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_ext_rotate_right (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) + expr_of_ptr ctx (Z3native.mk_ext_rotate_right (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) let mk_bv2int ( ctx : context ) ( t : expr ) ( signed : bool ) = expr_of_ptr ctx (Z3native.mk_bv2int (context_gno ctx) (Expr.gno t) signed) let mk_add_no_overflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) ( signed : bool) = (expr_of_ptr ctx (Z3native.mk_bvadd_no_overflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2) signed)) let mk_add_no_underflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvadd_no_underflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) + (expr_of_ptr ctx (Z3native.mk_bvadd_no_underflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) let mk_sub_no_overflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvsub_no_overflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) + (expr_of_ptr ctx (Z3native.mk_bvsub_no_overflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) let mk_sub_no_underflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) ( signed : bool) = (expr_of_ptr ctx (Z3native.mk_bvsub_no_underflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2) signed)) let mk_sdiv_no_overflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = @@ -1887,7 +1885,7 @@ struct let mk_mul_no_overflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) ( signed : bool) = (expr_of_ptr ctx (Z3native.mk_bvmul_no_overflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2) signed)) let mk_mul_no_underflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvmul_no_underflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) + (expr_of_ptr ctx (Z3native.mk_bvmul_no_underflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) let mk_numeral ( ctx : context ) ( v : string ) ( size : int ) = expr_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (Sort.gno (mk_sort ctx size))) end @@ -1897,66 +1895,66 @@ module FloatingPoint = struct module RoundingMode = struct - let mk_sort ( ctx : context ) = - (Sort.sort_of_ptr ctx (Z3native.mk_fpa_rounding_mode_sort (context_gno ctx))) - let is_fprm ( x : expr ) = - (Sort.get_sort_kind (Expr.get_sort(x))) == ROUNDING_MODE_SORT - let mk_round_nearest_ties_to_even ( ctx : context ) = - (expr_of_ptr ctx (Z3native.mk_fpa_round_nearest_ties_to_even (context_gno ctx))) - let mk_rne ( ctx : context ) = - (expr_of_ptr ctx (Z3native.mk_fpa_rne (context_gno ctx))) - let mk_round_nearest_ties_to_away ( ctx : context ) = - (expr_of_ptr ctx (Z3native.mk_fpa_round_nearest_ties_to_away (context_gno ctx))) - let mk_rna ( ctx : context ) = - (expr_of_ptr ctx (Z3native.mk_fpa_rna (context_gno ctx))) - let mk_round_toward_positive ( ctx : context ) = - (expr_of_ptr ctx (Z3native.mk_fpa_round_toward_positive (context_gno ctx))) - let mk_rtp ( ctx : context ) = - (expr_of_ptr ctx (Z3native.mk_fpa_rtp (context_gno ctx))) - let mk_round_toward_negative ( ctx : context ) = - (expr_of_ptr ctx (Z3native.mk_fpa_round_toward_negative (context_gno ctx))) - let mk_rtn ( ctx : context ) = - (expr_of_ptr ctx (Z3native.mk_fpa_rtn (context_gno ctx))) - let mk_round_toward_zero ( ctx : context ) = - (expr_of_ptr ctx (Z3native.mk_fpa_round_toward_zero (context_gno ctx))) - let mk_rtz ( ctx : context ) = - (expr_of_ptr ctx (Z3native.mk_fpa_rtz (context_gno ctx))) + let mk_sort ( ctx : context ) = + (Sort.sort_of_ptr ctx (Z3native.mk_fpa_rounding_mode_sort (context_gno ctx))) + let is_fprm ( x : expr ) = + (Sort.get_sort_kind (Expr.get_sort(x))) == ROUNDING_MODE_SORT + let mk_round_nearest_ties_to_even ( ctx : context ) = + (expr_of_ptr ctx (Z3native.mk_fpa_round_nearest_ties_to_even (context_gno ctx))) + let mk_rne ( ctx : context ) = + (expr_of_ptr ctx (Z3native.mk_fpa_rne (context_gno ctx))) + let mk_round_nearest_ties_to_away ( ctx : context ) = + (expr_of_ptr ctx (Z3native.mk_fpa_round_nearest_ties_to_away (context_gno ctx))) + let mk_rna ( ctx : context ) = + (expr_of_ptr ctx (Z3native.mk_fpa_rna (context_gno ctx))) + let mk_round_toward_positive ( ctx : context ) = + (expr_of_ptr ctx (Z3native.mk_fpa_round_toward_positive (context_gno ctx))) + let mk_rtp ( ctx : context ) = + (expr_of_ptr ctx (Z3native.mk_fpa_rtp (context_gno ctx))) + let mk_round_toward_negative ( ctx : context ) = + (expr_of_ptr ctx (Z3native.mk_fpa_round_toward_negative (context_gno ctx))) + let mk_rtn ( ctx : context ) = + (expr_of_ptr ctx (Z3native.mk_fpa_rtn (context_gno ctx))) + let mk_round_toward_zero ( ctx : context ) = + (expr_of_ptr ctx (Z3native.mk_fpa_round_toward_zero (context_gno ctx))) + let mk_rtz ( ctx : context ) = + (expr_of_ptr ctx (Z3native.mk_fpa_rtz (context_gno ctx))) end - + let mk_sort ( ctx : context ) ( ebits : int ) ( sbits : int ) = - (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort (context_gno ctx) ebits sbits)) + (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort (context_gno ctx) ebits sbits)) let mk_sort_half ( ctx : context ) = - (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_half (context_gno ctx))) + (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_half (context_gno ctx))) let mk_sort_16 ( ctx : context ) = - (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_16 (context_gno ctx))) + (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_16 (context_gno ctx))) let mk_sort_single ( ctx : context ) = - (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_single (context_gno ctx))) + (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_single (context_gno ctx))) let mk_sort_32 ( ctx : context ) = - (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_32 (context_gno ctx))) + (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_32 (context_gno ctx))) let mk_sort_double ( ctx : context ) = - (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_double (context_gno ctx))) + (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_double (context_gno ctx))) let mk_sort_64 ( ctx : context ) = - (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_64 (context_gno ctx))) + (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_64 (context_gno ctx))) let mk_sort_quadruple ( ctx : context ) = - (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_quadruple (context_gno ctx))) + (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_quadruple (context_gno ctx))) let mk_sort_128 ( ctx : context ) = - (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_128 (context_gno ctx))) + (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_128 (context_gno ctx))) let mk_nan ( ctx : context ) ( s : Sort.sort ) = - (expr_of_ptr ctx (Z3native.mk_fpa_nan (context_gno ctx) (Sort.gno s))) + (expr_of_ptr ctx (Z3native.mk_fpa_nan (context_gno ctx) (Sort.gno s))) let mk_inf ( ctx : context ) ( s : Sort.sort ) ( negative : bool ) = - (expr_of_ptr ctx (Z3native.mk_fpa_inf (context_gno ctx) (Sort.gno s) negative)) + (expr_of_ptr ctx (Z3native.mk_fpa_inf (context_gno ctx) (Sort.gno s) negative)) let mk_zero ( ctx : context ) ( s : Sort.sort ) ( negative : bool ) = - (expr_of_ptr ctx (Z3native.mk_fpa_zero (context_gno ctx) (Sort.gno s) negative)) + (expr_of_ptr ctx (Z3native.mk_fpa_zero (context_gno ctx) (Sort.gno s) negative)) let mk_fp ( ctx : context ) ( sign : expr ) ( exponent : expr ) ( significand : expr ) = - (expr_of_ptr ctx (Z3native.mk_fpa_fp (context_gno ctx) (Expr.gno sign) (Expr.gno exponent) (Expr.gno significand))) + (expr_of_ptr ctx (Z3native.mk_fpa_fp (context_gno ctx) (Expr.gno sign) (Expr.gno exponent) (Expr.gno significand))) let mk_numeral_f ( ctx : context ) ( value : float ) ( s : Sort.sort ) = - (expr_of_ptr ctx (Z3native.mk_fpa_numeral_double (context_gno ctx) value (Sort.gno s))) + (expr_of_ptr ctx (Z3native.mk_fpa_numeral_double (context_gno ctx) value (Sort.gno s))) let mk_numeral_i ( ctx : context ) ( value : int ) ( s : Sort.sort ) = - (expr_of_ptr ctx (Z3native.mk_fpa_numeral_int (context_gno ctx) value (Sort.gno s))) + (expr_of_ptr ctx (Z3native.mk_fpa_numeral_int (context_gno ctx) value (Sort.gno s))) let mk_numeral_i_u ( ctx : context ) ( sign : bool ) ( exponent : int ) ( significand : int ) ( s : Sort.sort ) = - (expr_of_ptr ctx (Z3native.mk_fpa_numeral_int64_uint64 (context_gno ctx) sign exponent significand (Sort.gno s))) + (expr_of_ptr ctx (Z3native.mk_fpa_numeral_int64_uint64 (context_gno ctx) sign exponent significand (Sort.gno s))) let mk_numeral_s ( ctx : context ) ( v : string ) ( s : Sort.sort ) = (expr_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (Sort.gno s))) @@ -1991,7 +1989,7 @@ struct let is_to_sbv ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_TO_SBV) let is_to_real ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_TO_REAL) let is_to_ieee_bv ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_TO_IEEE_BV) - + let numeral_to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x) let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( s : Sort.sort ) = Expr.mk_const ctx name s @@ -2064,24 +2062,24 @@ struct expr_of_ptr ctx (Z3native.mk_fpa_to_real (context_gno ctx) (Expr.gno t)) let get_ebits ( ctx : context ) ( s : Sort.sort ) = - (Z3native.fpa_get_ebits (context_gno ctx) (Sort.gno s)) + (Z3native.fpa_get_ebits (context_gno ctx) (Sort.gno s)) let get_sbits ( ctx : context ) ( s : Sort.sort ) = - (Z3native.fpa_get_sbits (context_gno ctx) (Sort.gno s)) + (Z3native.fpa_get_sbits (context_gno ctx) (Sort.gno s)) let get_numeral_sign ( ctx : context ) ( t : expr ) = - (Z3native.fpa_get_numeral_sign (context_gno ctx) (Expr.gno t)) + (Z3native.fpa_get_numeral_sign (context_gno ctx) (Expr.gno t)) let get_numeral_significand_string ( ctx : context ) ( t : expr ) = - (Z3native.fpa_get_numeral_significand_string (context_gno ctx) (Expr.gno t)) + (Z3native.fpa_get_numeral_significand_string (context_gno ctx) (Expr.gno t)) let get_numeral_significand_uint ( ctx : context ) ( t : expr ) = - (Z3native.fpa_get_numeral_significand_uint64 (context_gno ctx) (Expr.gno t)) + (Z3native.fpa_get_numeral_significand_uint64 (context_gno ctx) (Expr.gno t)) let get_numeral_exponent_string ( ctx : context ) ( t : expr ) = - (Z3native.fpa_get_numeral_exponent_string (context_gno ctx) (Expr.gno t)) + (Z3native.fpa_get_numeral_exponent_string (context_gno ctx) (Expr.gno t)) let get_numeral_exponent_int ( ctx : context ) ( t : expr ) = - (Z3native.fpa_get_numeral_exponent_int64 (context_gno ctx) (Expr.gno t)) + (Z3native.fpa_get_numeral_exponent_int64 (context_gno ctx) (Expr.gno t)) let mk_to_ieee_bv ( ctx : context ) ( t : expr ) = - (expr_of_ptr ctx (Z3native.mk_fpa_to_ieee_bv (context_gno ctx) (Expr.gno t))) + (expr_of_ptr ctx (Z3native.mk_fpa_to_ieee_bv (context_gno ctx) (Expr.gno t))) let mk_to_fp_int_real ( ctx : context ) ( rm : expr ) ( exponent : expr ) ( significand : expr ) ( s : Sort.sort ) = - (expr_of_ptr ctx (Z3native.mk_fpa_to_fp_int_real (context_gno ctx) (Expr.gno rm) (Expr.gno exponent) (Expr.gno significand) (Sort.gno s))) + (expr_of_ptr ctx (Z3native.mk_fpa_to_fp_int_real (context_gno ctx) (Expr.gno rm) (Expr.gno exponent) (Expr.gno significand) (Sort.gno s))) let numeral_to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x) end @@ -2137,9 +2135,9 @@ struct let create ( ctx : context ) ( no : Z3native.ptr ) = let res : goal = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.goal_inc_ref ; - dec_ref = Z3native.goal_dec_ref } in + m_n_obj = null ; + inc_ref = Z3native.goal_inc_ref ; + dec_ref = Z3native.goal_dec_ref } in (z3obj_sno res ctx no) ; (z3obj_create res) ; res @@ -2176,7 +2174,7 @@ struct let get_formulas ( x : goal ) = let n = get_size x in let f i = ((expr_of_ptr (z3obj_gc x) - (Z3native.goal_formula (z3obj_gnc x) (z3obj_gno x) i))) in + (Z3native.goal_formula (z3obj_gnc x) (z3obj_gno x) i))) in mk_list f n let get_num_exprs ( x : goal ) = Z3native.goal_num_exprs (z3obj_gnc x) (z3obj_gno x) @@ -2200,9 +2198,9 @@ struct Z3native.apply_result_inc_ref (z3obj_gnc x) arn ; let sg = Z3native.apply_result_get_num_subgoals (z3obj_gnc x) arn in let res = if sg == 0 then - raise (Z3native.Exception "No subgoals") + raise (Z3native.Exception "No subgoals") else - Z3native.apply_result_get_subgoal (z3obj_gnc x) arn 0 in + Z3native.apply_result_get_subgoal (z3obj_gnc x) arn 0 in Z3native.apply_result_dec_ref (z3obj_gnc x) arn ; Z3native.tactic_dec_ref (z3obj_gnc x) tn ; create (z3obj_gc x) res @@ -2213,13 +2211,13 @@ struct let to_string ( x : goal ) = Z3native.goal_to_string (z3obj_gnc x) (z3obj_gno x) let as_expr ( x : goal ) = - let n = get_size x in - if n = 0 then - (Boolean.mk_true (z3obj_gc x)) - else if n = 1 then - (List.hd (get_formulas x)) - else - (Boolean.mk_and (z3obj_gc x) (get_formulas x)) + let n = get_size x in + if n = 0 then + (Boolean.mk_true (z3obj_gc x)) + else if n = 1 then + (List.hd (get_formulas x)) + else + (Boolean.mk_and (z3obj_gc x) (get_formulas x)) end @@ -2229,9 +2227,9 @@ struct let create ( ctx : context ) ( no : Z3native.ptr ) = let res : model = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.model_inc_ref ; - dec_ref = Z3native.model_dec_ref } in + m_n_obj = null ; + inc_ref = Z3native.model_inc_ref ; + dec_ref = Z3native.model_dec_ref } in (z3obj_sno res ctx no) ; (z3obj_create res) ; res @@ -2242,40 +2240,40 @@ struct let create ( ctx : context ) ( no : Z3native.ptr ) = let res : func_interp = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.func_interp_inc_ref ; - dec_ref = Z3native.func_interp_dec_ref } in + m_n_obj = null ; + inc_ref = Z3native.func_interp_inc_ref ; + dec_ref = Z3native.func_interp_dec_ref } in (z3obj_sno res ctx no) ; (z3obj_create res) ; res - + module FuncEntry = - struct + struct type func_entry = z3_native_object - + let create ( ctx : context ) ( no : Z3native.ptr ) = - let res : func_entry = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.func_entry_inc_ref ; - dec_ref = Z3native.func_entry_dec_ref } in - (z3obj_sno res ctx no) ; - (z3obj_create res) ; - res - + let res : func_entry = { m_ctx = ctx ; + m_n_obj = null ; + inc_ref = Z3native.func_entry_inc_ref ; + dec_ref = Z3native.func_entry_dec_ref } in + (z3obj_sno res ctx no) ; + (z3obj_create res) ; + res + let get_value ( x : func_entry ) = - expr_of_ptr (z3obj_gc x) (Z3native.func_entry_get_value (z3obj_gnc x) (z3obj_gno x)) + expr_of_ptr (z3obj_gc x) (Z3native.func_entry_get_value (z3obj_gnc x) (z3obj_gno x)) let get_num_args ( x : func_entry ) = Z3native.func_entry_get_num_args (z3obj_gnc x) (z3obj_gno x) - + let get_args ( x : func_entry ) = - let n = (get_num_args x) in - let f i = (expr_of_ptr (z3obj_gc x) (Z3native.func_entry_get_arg (z3obj_gnc x) (z3obj_gno x) i)) in - mk_list f n - + let n = (get_num_args x) in + let f i = (expr_of_ptr (z3obj_gc x) (Z3native.func_entry_get_arg (z3obj_gnc x) (z3obj_gno x) i)) in + mk_list f n + let to_string ( x : func_entry ) = - let a = (get_args x) in - let f c p = (p ^ (Expr.to_string c) ^ ", ") in - "[" ^ List.fold_right f a ((Expr.to_string (get_value x)) ^ "]") + let a = (get_args x) in + let f c p = (p ^ (Expr.to_string c) ^ ", ") in + "[" ^ List.fold_right f a ((Expr.to_string (get_value x)) ^ "]") end let get_num_entries ( x: func_interp ) = Z3native.func_interp_get_num_entries (z3obj_gnc x) (z3obj_gno x) @@ -2291,14 +2289,14 @@ struct let to_string ( x : func_interp ) = let f c p = ( - let n = (FuncEntry.get_num_args c) in - p ^ - let g c p = (p ^ (Expr.to_string c) ^ ", ") in - (if n > 1 then "[" else "") ^ - (List.fold_right - g - (FuncEntry.get_args c) - ((if n > 1 then "]" else "") ^ " -> " ^ (Expr.to_string (FuncEntry.get_value c)) ^ ", ")) + let n = (FuncEntry.get_num_args c) in + p ^ + let g c p = (p ^ (Expr.to_string c) ^ ", ") in + (if n > 1 then "[" else "") ^ + (List.fold_right + g + (FuncEntry.get_args c) + ((if n > 1 then "]" else "") ^ " -> " ^ (Expr.to_string (FuncEntry.get_value c)) ^ ", ")) ) in List.fold_right f (get_entries x) ("else -> " ^ (Expr.to_string (get_else x)) ^ "]") end @@ -2310,9 +2308,9 @@ struct else let np = Z3native.model_get_const_interp (z3obj_gnc x) (z3obj_gno x) (FuncDecl.gno f) in if (Z3native.is_null np) then - None + None else - Some (expr_of_ptr (z3obj_gc x) np) + Some (expr_of_ptr (z3obj_gc x) np) let get_const_interp_e ( x : model ) ( a : expr ) = get_const_interp x (Expr.get_func_decl a) @@ -2322,20 +2320,20 @@ struct if (FuncDecl.get_arity f) == 0 then let n = Z3native.model_get_const_interp (z3obj_gnc x) (z3obj_gno x) (FuncDecl.gno f) in if (Z3native.is_null n) then - None + None else - match sk with - | ARRAY_SORT -> - if not (Z3native.is_as_array (z3obj_gnc x) n) then - raise (Z3native.Exception "Argument was not an array constant") - else - let fd = Z3native.get_as_array_func_decl (z3obj_gnc x) n in + match sk with + | ARRAY_SORT -> + if not (Z3native.is_as_array (z3obj_gnc x) n) then + raise (Z3native.Exception "Argument was not an array constant") + else + let fd = Z3native.get_as_array_func_decl (z3obj_gnc x) n in get_func_interp x (func_decl_of_ptr (z3obj_gc x) fd) - | _ -> raise (Z3native.Exception "Constant functions do not have a function interpretation; use ConstInterp"); + | _ -> raise (Z3native.Exception "Constant functions do not have a function interpretation; use ConstInterp"); else let n = (Z3native.model_get_func_interp (z3obj_gnc x) (z3obj_gno x) (FuncDecl.gno f)) in if (Z3native.is_null n) then None else Some (FuncInterp.create (z3obj_gc x) n) - + (** The number of constants that have an interpretation in the model. *) let get_num_consts ( x : model ) = Z3native.model_get_num_consts (z3obj_gnc x) (z3obj_gno x) @@ -2389,9 +2387,9 @@ struct let create ( ctx : context ) ( no : Z3native.ptr ) = let res : probe = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.probe_inc_ref ; - dec_ref = Z3native.probe_dec_ref } in + m_n_obj = null ; + inc_ref = Z3native.probe_inc_ref ; + dec_ref = Z3native.probe_dec_ref } in (z3obj_sno res ctx no) ; (z3obj_create res) ; res @@ -2449,9 +2447,9 @@ struct let create ( ctx : context ) ( no : Z3native.ptr ) = let res : tactic = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.tactic_inc_ref ; - dec_ref = Z3native.tactic_dec_ref } in + m_n_obj = null ; + inc_ref = Z3native.tactic_inc_ref ; + dec_ref = Z3native.tactic_dec_ref } in (z3obj_sno res ctx no) ; (z3obj_create res) ; res @@ -2459,30 +2457,30 @@ struct module ApplyResult = struct type apply_result = z3_native_object - + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : apply_result = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.apply_result_inc_ref ; - dec_ref = Z3native.apply_result_dec_ref } in + m_n_obj = null ; + inc_ref = Z3native.apply_result_inc_ref ; + dec_ref = Z3native.apply_result_dec_ref } in (z3obj_sno res ctx no) ; (z3obj_create res) ; res - + let get_num_subgoals ( x : apply_result ) = Z3native.apply_result_get_num_subgoals (z3obj_gnc x) (z3obj_gno x) - + let get_subgoals ( x : apply_result ) = let n = (get_num_subgoals x) in let f i = Goal.create (z3obj_gc x) (Z3native.apply_result_get_subgoal (z3obj_gnc x) (z3obj_gno x) i) in mk_list f n - + let get_subgoal ( x : apply_result ) ( i : int ) = Goal.create (z3obj_gc x) (Z3native.apply_result_get_subgoal (z3obj_gnc x) (z3obj_gno x) i) - + let convert_model ( x : apply_result ) ( i : int ) ( m : Model.model ) = Model.create (z3obj_gc x) (Z3native.apply_result_convert_model (z3obj_gnc x) (z3obj_gno x) i (z3obj_gno m)) - + let to_string ( x : apply_result ) = Z3native.apply_result_to_string (z3obj_gnc x) (z3obj_gno x) end @@ -2515,10 +2513,10 @@ struct | Some(x) -> (Some (Z3native.tactic_and_then (context_gno ctx) (z3obj_gno c) x))) in match (List.fold_left f None ts) with | None -> - create ctx (Z3native.tactic_and_then (context_gno ctx) (z3obj_gno t1) (z3obj_gno t2)) + create ctx (Z3native.tactic_and_then (context_gno ctx) (z3obj_gno t1) (z3obj_gno t2)) | Some(x) -> - let o = (Z3native.tactic_and_then (context_gno ctx) (z3obj_gno t2) x) in - create ctx (Z3native.tactic_and_then (context_gno ctx) (z3obj_gno t1) o) + let o = (Z3native.tactic_and_then (context_gno ctx) (z3obj_gno t2) x) in + create ctx (Z3native.tactic_and_then (context_gno ctx) (z3obj_gno t1) o) let or_else ( ctx : context ) ( t1 : tactic ) ( t2 : tactic ) = create ctx (Z3native.tactic_or_else (context_gno ctx) (z3obj_gno t1) (z3obj_gno t2)) @@ -2566,14 +2564,14 @@ end module Statistics = -struct +struct type statistics = z3_native_object let create ( ctx : context ) ( no : Z3native.ptr ) = let res : statistics = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.stats_inc_ref ; - dec_ref = Z3native.stats_dec_ref } in + m_n_obj = null ; + inc_ref = Z3native.stats_inc_ref ; + dec_ref = Z3native.stats_dec_ref } in (z3obj_sno res ctx no) ; (z3obj_create res) ; res @@ -2582,44 +2580,44 @@ struct module Entry = struct type statistics_entry = { - mutable m_key : string; - mutable m_is_int : bool ; - mutable m_is_float : bool ; - mutable m_int : int ; - mutable m_float : float } - + mutable m_key : string; + mutable m_is_int : bool ; + mutable m_is_float : bool ; + mutable m_int : int ; + mutable m_float : float } + let create_si k v = - let res : statistics_entry = { - m_key = k ; - m_is_int = true ; - m_is_float = false ; - m_int = v ; - m_float = 0.0 - } in - res + let res : statistics_entry = { + m_key = k ; + m_is_int = true ; + m_is_float = false ; + m_int = v ; + m_float = 0.0 + } in + res let create_sd k v = - let res : statistics_entry = { - m_key = k ; - m_is_int = false ; - m_is_float = true ; - m_int = 0 ; - m_float = v - } in - res - + let res : statistics_entry = { + m_key = k ; + m_is_int = false ; + m_is_float = true ; + m_int = 0 ; + m_float = v + } in + res + let get_key (x : statistics_entry) = x.m_key - let get_int (x : statistics_entry) = x.m_int + let get_int (x : statistics_entry) = x.m_int let get_float (x : statistics_entry) = x.m_float let is_int (x : statistics_entry) = x.m_is_int let is_float (x : statistics_entry) = x.m_is_float let to_string_value (x : statistics_entry) = - if (is_int x) then - string_of_int (get_int x) - else if (is_float x) then - string_of_float (get_float x) - else + if (is_int x) then + string_of_int (get_int x) + else if (is_float x) then + string_of_float (get_float x) + else raise (Z3native.Exception "Unknown statistical entry type") let to_string ( x : statistics_entry ) = (get_key x) ^ ": " ^ (to_string_value x) end @@ -2631,11 +2629,11 @@ struct let get_entries ( x : statistics ) = let n = (get_size x ) in let f i = ( - let k = Z3native.stats_get_key (z3obj_gnc x) (z3obj_gno x) i in - if (Z3native.stats_is_uint (z3obj_gnc x) (z3obj_gno x) i) then - (Entry.create_si k (Z3native.stats_get_uint_value (z3obj_gnc x) (z3obj_gno x) i)) - else - (Entry.create_sd k (Z3native.stats_get_double_value (z3obj_gnc x) (z3obj_gno x) i)) + let k = Z3native.stats_get_key (z3obj_gnc x) (z3obj_gno x) i in + if (Z3native.stats_is_uint (z3obj_gnc x) (z3obj_gno x) i) then + (Entry.create_si k (Z3native.stats_get_uint_value (z3obj_gnc x) (z3obj_gno x) i)) + else + (Entry.create_sd k (Z3native.stats_get_double_value (z3obj_gnc x) (z3obj_gno x) i)) ) in mk_list f n @@ -2643,7 +2641,7 @@ struct let n = (get_size x) in let f i = (Z3native.stats_get_key (z3obj_gnc x) (z3obj_gno x) i) in mk_list f n - + let get ( x : statistics ) ( key : string ) = let f p c = (if ((Entry.get_key c) == key) then (Some c) else p) in List.fold_left f None (get_entries x) @@ -2657,9 +2655,9 @@ struct let create ( ctx : context ) ( no : Z3native.ptr ) = let res : solver = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.solver_inc_ref ; - dec_ref = Z3native.solver_dec_ref } in + m_n_obj = null ; + inc_ref = Z3native.solver_inc_ref ; + dec_ref = Z3native.solver_dec_ref } in (z3obj_sno res ctx no) ; (z3obj_create res) ; res @@ -2695,7 +2693,7 @@ struct else let f a b = (Z3native.solver_assert_and_track (z3obj_gnc x) (z3obj_gno x) (Expr.gno a) (Expr.gno b)) in ignore (List.iter2 f cs ps) - + let assert_and_track ( x : solver ) ( c : expr ) ( p : expr ) = Z3native.solver_assert_and_track (z3obj_gnc x) (z3obj_gno x) (Expr.gno c) (Expr.gno p) @@ -2710,30 +2708,30 @@ struct let check ( x : solver ) ( assumptions : expr list ) = let r = if ((List.length assumptions) == 0) then - lbool_of_int (Z3native.solver_check (z3obj_gnc x) (z3obj_gno x)) + lbool_of_int (Z3native.solver_check (z3obj_gnc x) (z3obj_gno x)) else - let f x = (Expr.gno x) in - lbool_of_int (Z3native.solver_check_assumptions (z3obj_gnc x) (z3obj_gno x) (List.length assumptions) (Array.of_list (List.map f assumptions))) + let f x = (Expr.gno x) in + lbool_of_int (Z3native.solver_check_assumptions (z3obj_gnc x) (z3obj_gno x) (List.length assumptions) (Array.of_list (List.map f assumptions))) in match r with | L_TRUE -> SATISFIABLE | L_FALSE -> UNSATISFIABLE | _ -> UNKNOWN - + let get_model ( x : solver ) = let q = Z3native.solver_get_model (z3obj_gnc x) (z3obj_gno x) in if (Z3native.is_null q) then None else Some (Model.create (z3obj_gc x) q) - + let get_proof ( x : solver ) = let q = Z3native.solver_get_proof (z3obj_gnc x) (z3obj_gno x) in if (Z3native.is_null q) then None else Some (expr_of_ptr (z3obj_gc x) q) - + let get_unsat_core ( x : solver ) = let av = AST.ASTVector.create (z3obj_gc x) (Z3native.solver_get_unsat_core (z3obj_gnc x) (z3obj_gno x)) in (AST.ASTVector.to_expr_list av) @@ -2758,7 +2756,7 @@ struct create ctx (Z3native.mk_solver_from_tactic (context_gno ctx) (z3obj_gno t)) let translate ( x : solver ) ( to_ctx : context ) = - create to_ctx (Z3native.solver_translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx)) + create to_ctx (Z3native.solver_translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx)) let to_string ( x : solver ) = Z3native.solver_to_string (z3obj_gnc x) (z3obj_gno x) end @@ -2770,9 +2768,9 @@ struct let create ( ctx : context ) = let res : fixedpoint = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.fixedpoint_inc_ref ; - dec_ref = Z3native.fixedpoint_dec_ref } in + m_n_obj = null ; + inc_ref = Z3native.fixedpoint_inc_ref ; + dec_ref = Z3native.fixedpoint_dec_ref } in (z3obj_sno res ctx (Z3native.mk_fixedpoint (context_gno ctx))) ; (z3obj_create res) ; res @@ -2815,7 +2813,7 @@ struct | L_TRUE -> Solver.SATISFIABLE | L_FALSE -> Solver.UNSATISFIABLE | _ -> Solver.UNKNOWN - + let push ( x : fixedpoint ) = Z3native.fixedpoint_push (z3obj_gnc x) (z3obj_gno x) @@ -2844,7 +2842,7 @@ struct None else Some (expr_of_ptr (z3obj_gc x) q) - + let add_cover ( x : fixedpoint ) ( level : int ) ( predicate : func_decl ) ( property : expr ) = Z3native.fixedpoint_add_cover (z3obj_gnc x) (z3obj_gno x) level (FuncDecl.gno predicate) (Expr.gno property) @@ -2980,13 +2978,13 @@ struct raise (Z3native.Exception "Argument size mismatch") else Z3native.parse_smtlib_string (context_gno ctx) str - cs - (Symbol.symbol_lton sort_names) - (Sort.sort_lton sorts) - cd - (Symbol.symbol_lton decl_names) - (let f x = FuncDecl.gno x in (Array.of_list (List.map f decls))) - + cs + (Symbol.symbol_lton sort_names) + (Sort.sort_lton sorts) + cd + (Symbol.symbol_lton decl_names) + (let f x = FuncDecl.gno x in (Array.of_list (List.map f 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 @@ -2996,12 +2994,12 @@ struct raise (Z3native.Exception "Argument size mismatch") else Z3native.parse_smtlib_file (context_gno ctx) file_name - cs - (Symbol.symbol_lton sort_names) - (Sort.sort_lton sorts) - cd - (Symbol.symbol_lton decl_names) - (let f x = FuncDecl.gno x in (Array.of_list (List.map f decls))) + cs + (Symbol.symbol_lton sort_names) + (Sort.sort_lton sorts) + cd + (Symbol.symbol_lton decl_names) + (let f x = FuncDecl.gno x in (Array.of_list (List.map f decls))) let get_num_smtlib_formulas ( ctx : context ) = Z3native.get_smtlib_num_formulas (context_gno ctx) @@ -3040,13 +3038,13 @@ struct raise (Z3native.Exception "Argument size mismatch") else (expr_of_ptr ctx (Z3native.parse_smtlib2_string (context_gno ctx) str - cs - (Symbol.symbol_lton sort_names) - (Sort.sort_lton sorts) - cd - (Symbol.symbol_lton decl_names) - (let f x = FuncDecl.gno x in (Array.of_list (List.map f decls))))) - + cs + (Symbol.symbol_lton sort_names) + (Sort.sort_lton sorts) + cd + (Symbol.symbol_lton decl_names) + (let f x = FuncDecl.gno x in (Array.of_list (List.map f decls))))) + let parse_smtlib2_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 @@ -3056,12 +3054,12 @@ struct raise (Z3native.Exception "Argument size mismatch") else (expr_of_ptr ctx (Z3native.parse_smtlib2_string (context_gno ctx) file_name - cs - (Symbol.symbol_lton sort_names) - (Sort.sort_lton sorts) - cd - (Symbol.symbol_lton decl_names) - (let f x = FuncDecl.gno x in (Array.of_list (List.map f decls))))) + cs + (Symbol.symbol_lton sort_names) + (Sort.sort_lton sorts) + cd + (Symbol.symbol_lton decl_names) + (let f x = FuncDecl.gno x in (Array.of_list (List.map f decls))))) end module Interpolation = @@ -3102,21 +3100,21 @@ struct match r with | 0 -> raise (Z3native.Exception "Interpolation problem could not be read.") | _ -> - let f1 i = (expr_of_ptr ctx (Array.get cnsts i)) in - let f2 i = (Array.get parents i) in - let f3 i = (expr_of_ptr ctx (Array.get theory i)) in - ((mk_list f1 num), - (mk_list f2 num), - (mk_list f3 num_theory)) + let f1 i = (expr_of_ptr ctx (Array.get cnsts i)) in + let f2 i = (Array.get parents i) in + let f3 i = (expr_of_ptr ctx (Array.get theory i)) in + ((mk_list f1 num), + (mk_list f2 num), + (mk_list f3 num_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 (context_gno ctx) - num - (let f x = Expr.gno x in (Array.of_list (List.map f cnsts))) - (Array.of_list parents) - (let f x = Expr.gno x in (Array.of_list (List.map f interps))) - num_theory - (let f x = Expr.gno x in (Array.of_list (List.map f theory)))) in + num + (let f x = Expr.gno x in (Array.of_list (List.map f cnsts))) + (Array.of_list parents) + (let f x = Expr.gno x in (Array.of_list (List.map f interps))) + num_theory + (let f x = Expr.gno x in (Array.of_list (List.map f theory)))) in match (lbool_of_int r) with | L_UNDEF -> raise (Z3native.Exception "Interpolant could not be verified.") | L_FALSE -> raise (Z3native.Exception "Interpolant could not be verified.") diff --git a/src/api/z3_replayer.cpp b/src/api/z3_replayer.cpp index 927521b65..8ce81ec31 100644 --- a/src/api/z3_replayer.cpp +++ b/src/api/z3_replayer.cpp @@ -46,6 +46,7 @@ struct z3_replayer::imp { size_t m_ptr; size_t_map m_heap; svector m_cmds; + vector m_cmds_names; enum value_kind { INT64, UINT64, DOUBLE, STRING, SYMBOL, OBJECT, UINT_ARRAY, INT_ARRAY, SYMBOL_ARRAY, OBJECT_ARRAY, FLOAT }; @@ -509,6 +510,7 @@ struct z3_replayer::imp { if (idx >= m_cmds.size()) throw z3_replayer_exception("invalid command"); try { + TRACE("z3_replayer_cmd", tout << m_cmds_names[idx] << "\n";); m_cmds[idx](m_owner); } catch (z3_error & ex) { @@ -672,9 +674,11 @@ struct z3_replayer::imp { m_result = obj; } - void register_cmd(unsigned id, z3_replayer_cmd cmd) { + void register_cmd(unsigned id, z3_replayer_cmd cmd, char const* name) { m_cmds.reserve(id+1, 0); + m_cmds_names.reserve(id+1, ""); m_cmds[id] = cmd; + m_cmds_names[id] = name; } void reset() { @@ -786,8 +790,8 @@ void z3_replayer::store_result(void * obj) { return m_imp->store_result(obj); } -void z3_replayer::register_cmd(unsigned id, z3_replayer_cmd cmd) { - return m_imp->register_cmd(id, cmd); +void z3_replayer::register_cmd(unsigned id, z3_replayer_cmd cmd, char const* name) { + return m_imp->register_cmd(id, cmd, name); } void z3_replayer::parse() { diff --git a/src/api/z3_replayer.h b/src/api/z3_replayer.h index 6c566d553..88654363d 100644 --- a/src/api/z3_replayer.h +++ b/src/api/z3_replayer.h @@ -62,7 +62,7 @@ public: void ** get_obj_addr(unsigned pos); void store_result(void * obj); - void register_cmd(unsigned id, z3_replayer_cmd cmd); + void register_cmd(unsigned id, z3_replayer_cmd cmd, char const* name); }; #endif diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 2ee6c7556..ab1a5a5af 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1656,6 +1656,7 @@ ast * ast_manager::register_node_core(ast * n) { n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk(); + TRACE("ast", tout << "Object " << n->m_id << " was created.\n";); TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";); // increment reference counters diff --git a/src/ast/rewriter/expr_safe_replace.cpp b/src/ast/rewriter/expr_safe_replace.cpp index b43577960..8ce40e49a 100644 --- a/src/ast/rewriter/expr_safe_replace.cpp +++ b/src/ast/rewriter/expr_safe_replace.cpp @@ -20,9 +20,11 @@ Revision History: #include "expr_safe_replace.h" #include "rewriter.h" +#include "ast_pp.h" void expr_safe_replace::insert(expr* src, expr* dst) { + SASSERT(m.get_sort(src) == m.get_sort(dst)); m_src.push_back(src); m_dst.push_back(dst); m_subst.insert(src, dst); @@ -30,7 +32,7 @@ void expr_safe_replace::insert(expr* src, expr* dst) { void expr_safe_replace::operator()(expr* e, expr_ref& res) { m_todo.push_back(e); - expr* a, *b, *d; + expr* a, *b; while (!m_todo.empty()) { a = m_todo.back(); @@ -39,7 +41,7 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) { } else if (m_subst.find(a, b)) { m_cache.insert(a, b); - m_todo.pop_back(); + m_todo.pop_back(); } else if (is_var(a)) { m_cache.insert(a, a); @@ -51,18 +53,21 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) { m_args.reset(); bool arg_differs = false; for (unsigned i = 0; i < n; ++i) { - if (m_cache.find(c->get_arg(i), d)) { + expr* d = 0, *arg = c->get_arg(i); + if (m_cache.find(arg, d)) { m_args.push_back(d); - arg_differs |= c->get_arg(i) != d; + arg_differs |= arg != d; + SASSERT(m.get_sort(arg) == m.get_sort(d)); } else { - m_todo.push_back(c->get_arg(i)); + m_todo.push_back(arg); } } if (m_args.size() == n) { if (arg_differs) { b = m.mk_app(c->get_decl(), m_args.size(), m_args.c_ptr()); m_refs.push_back(b); + SASSERT(m.get_sort(a) == m.get_sort(b)); } else { b = a; } @@ -71,6 +76,7 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) { } } else { + (std::cout << "q\n").flush(); SASSERT(is_quantifier(a)); quantifier* q = to_quantifier(a); expr_safe_replace replace(m); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 75e27c081..ea5bec231 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -163,6 +163,7 @@ std::ostream& zstring::operator<<(std::ostream& out) const { seq_decl_plugin::seq_decl_plugin(): m_init(false), m_stringc_sym("String"), + m_charc_sym("Char"), m_string(0), m_char(0) {} @@ -369,7 +370,8 @@ void seq_decl_plugin::init() { void seq_decl_plugin::set_manager(ast_manager* m, family_id id) { decl_plugin::set_manager(m, id); - m_char = m->mk_sort(symbol("Char"), sort_info(m_family_id, _CHAR_SORT, 0, (parameter const*)0)); + bv_util bv(*m); + m_char = bv.mk_sort(8); m->inc_ref(m_char); parameter param(m_char); m_string = m->mk_sort(symbol("String"), sort_info(m_family_id, SEQ_SORT, 1, ¶m)); @@ -401,8 +403,6 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter return m.mk_sort(symbol("RegEx"), sort_info(m_family_id, RE_SORT, num_parameters, parameters)); case _STRING_SORT: return m_string; - case _CHAR_SORT: - return m_char; default: UNREACHABLE(); return 0; @@ -470,6 +470,8 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, } return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k, num_parameters, parameters)); + + case OP_STRING_CONST: if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) { m.raise_exception("invalid string declaration"); @@ -583,7 +585,7 @@ void seq_decl_plugin::get_sort_names(svector & sort_names, symbol app* seq_decl_plugin::mk_string(symbol const& s) { parameter param(s); func_decl* f = m_manager->mk_const_decl(m_stringc_sym, m_string, - func_decl_info(m_family_id, OP_STRING_CONST, 1, ¶m)); + func_decl_info(m_family_id, OP_STRING_CONST, 1, ¶m)); return m_manager->mk_const(f); } @@ -591,10 +593,11 @@ app* seq_decl_plugin::mk_string(zstring const& s) { symbol sym(s.encode().c_str()); parameter param(sym); func_decl* f = m_manager->mk_const_decl(m_stringc_sym, m_string, - func_decl_info(m_family_id, OP_STRING_CONST, 1, ¶m)); + func_decl_info(m_family_id, OP_STRING_CONST, 1, ¶m)); return m_manager->mk_const(f); } + bool seq_decl_plugin::is_value(app* e) const { return is_app_of(e, m_family_id, OP_STRING_CONST); } @@ -609,11 +612,21 @@ app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort app* seq_util::str::mk_string(zstring const& s) { return u.seq.mk_string(s); } + app* seq_util::str::mk_char(zstring const& s, unsigned idx) { bv_util bvu(m); return bvu.mk_numeral(s[idx], s.num_bits()); } +bool seq_util::str::is_char(expr* n, zstring& c) const { + if (u.is_char(n)) { + c = zstring(to_app(n)->get_decl()->get_parameter(0).get_symbol().bare_str()); + return true; + } + else { + return false; + } +} bool seq_util::str::is_string(expr const* n, zstring& s) const { if (is_string(n)) { diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 33d4de378..9a5f65d05 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -22,13 +22,13 @@ Revision History: #define SEQ_DECL_PLUGIN_H_ #include "ast.h" +#include "bv_decl_plugin.h" enum seq_sort_kind { SEQ_SORT, RE_SORT, - _STRING_SORT, // internal only - _CHAR_SORT // internal only + _STRING_SORT // internal only }; enum seq_op_kind { @@ -131,6 +131,7 @@ class seq_decl_plugin : public decl_plugin { ptr_vector m_sigs; bool m_init; symbol m_stringc_sym; + symbol m_charc_sym; sort* m_string; sort* m_char; @@ -187,6 +188,7 @@ public: ast_manager& get_manager() const { return m; } + bool is_char(sort* s) const { return seq.is_char(s); } bool is_string(sort* s) const { return is_seq(s) && seq.is_char(s->get_parameter(0).get_ast()); } bool is_seq(sort* s) const { return is_sort_of(s, m_fid, SEQ_SORT); } bool is_re(sort* s) const { return is_sort_of(s, m_fid, RE_SORT); } @@ -195,6 +197,7 @@ public: bool is_seq(sort* s, sort*& seq) { return is_seq(s) && (seq = to_sort(s->get_parameter(0).get_ast()), true); } bool is_re(expr* e) const { return is_re(m.get_sort(e)); } bool is_re(expr* e, sort*& seq) const { return is_re(m.get_sort(e), seq); } + bool is_char(expr* e) const { return is_char(m.get_sort(e)); } app* mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range); bool is_skolem(expr const* e) const { return is_app_of(e, m_fid, _OP_SEQ_SKOLEM); } @@ -215,6 +218,7 @@ public: app* mk_empty(sort* s) { return m.mk_const(m.mk_func_decl(m_fid, OP_SEQ_EMPTY, 0, 0, 0, (expr*const*)0, s)); } app* mk_string(zstring const& s); app* mk_string(symbol const& s) { return u.seq.mk_string(s); } + app* mk_char(char ch); app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); } app* mk_concat(expr* a, expr* b, expr* c) { return mk_concat(mk_concat(a, b), c); @@ -238,6 +242,7 @@ public: } bool is_string(expr const* n, zstring& s) const; + bool is_char(expr* n, zstring& s) const; bool is_empty(expr const* n) const { symbol s; return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && *s.bare_str() == 0); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index db96f3d0c..62e4f4338 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -331,7 +331,7 @@ bool theory_seq::check_length_coherence_tbd() { if (is_var(f) && f == e) { expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m); TRACE("seq", tout << "Unsolved " << mk_pp(e, m) << "\n";); -#if 0 +#if 1 if (!assume_equality(e, emp)) { // e = emp \/ e = unit(head.elem(e))*tail(e) sort* char_sort = 0; @@ -341,9 +341,11 @@ bool theory_seq::check_length_coherence_tbd() { expr_ref head(m_util.str.mk_unit(v), m); expr_ref conc(m_util.str.mk_concat(head, tail), m); add_axiom(mk_eq(e, emp, false), mk_eq(e, conc, false)); + assume_equality(tail, emp); } #endif - coherent = false; + m_branch_variable_head = j + 1; + return false; } } return coherent; diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h index 04f38020c..5065c733d 100644 --- a/src/smt/theory_seq_empty.h +++ b/src/smt/theory_seq_empty.h @@ -30,6 +30,7 @@ namespace smt { seq_util u; symbol_set m_strings; unsigned m_next; + char m_char; std::string m_unique_prefix; obj_map m_unique_sequences; expr_ref_vector m_trail; @@ -41,6 +42,7 @@ namespace smt { m_model(md), u(m), m_next(0), + m_char(0), m_unique_prefix("#B"), m_trail(m) { @@ -99,6 +101,11 @@ namespace smt { expr* v0 = get_fresh_value(seq); return u.re.mk_to_re(v0); } + if (u.is_char(s)) { + //char s[2] = { ++m_char, 0 }; + //return u.str.mk_char(zstring(s), 0); + return u.str.mk_char(zstring("a"), 0); + } NOT_IMPLEMENTED_YET(); return 0; } diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 06a82b0d5..a22275043 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -239,16 +239,26 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode else { scoped_mpq sig(m_mpq_manager); scoped_mpz exp(m_mpq_manager); + scoped_mpq pow(m_mpq_manager); m_mpq_manager.set(sig, significand); m_mpq_manager.abs(sig); m_mpz_manager.set(exp, exponent); - + m_mpq_manager.set(pow, mpq(2)); + // Normalize - while (m_mpq_manager.ge(sig, 2)) { - m_mpq_manager.div(sig, mpq(2), sig); + unsigned loop = 0; + while (m_mpq_manager.ge(sig, pow)) { + m_mpq_manager.mul(pow, 2, pow); m_mpz_manager.inc(exp); + ++loop; + if (loop % 1000 == 0) std::cout << loop << "\n"; } + std::cout << loop << "\n"; + if (loop > 0) { + m_mpq_manager.div(sig, pow, sig); + } + std::cout << loop << "\n"; while (m_mpq_manager.lt(sig, 1)) { m_mpq_manager.mul(sig, 2, sig);