diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 613db591e..dbf36c6a4 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1324,14 +1324,14 @@ struct let mk_to_real = Z3native.mk_fpa_to_real let get_ebits = Z3native.fpa_get_ebits let get_sbits = Z3native.fpa_get_sbits - let get_numeral_sign_bv = Z3native.fpa_get_numeral_sign_bv - let get_numeral_exponent_bv = Z3native.fpa_get_numeral_exponent_bv - let get_numeral_significand_bv = Z3native.fpa_get_numeral_significand_bv let get_numeral_sign = Z3native.fpa_get_numeral_sign - let get_numeral_significand_string = Z3native.fpa_get_numeral_significand_string - let get_numeral_significand_uint = Z3native.fpa_get_numeral_significand_uint64 + let get_numeral_sign_bv = Z3native.fpa_get_numeral_sign_bv let get_numeral_exponent_string = Z3native.fpa_get_numeral_exponent_string let get_numeral_exponent_int = Z3native.fpa_get_numeral_exponent_int64 + let get_numeral_exponent_bv = Z3native.fpa_get_numeral_exponent_bv + let get_numeral_significand_string = Z3native.fpa_get_numeral_significand_string + let get_numeral_significand_uint = Z3native.fpa_get_numeral_significand_uint64 + let get_numeral_significand_bv = Z3native.fpa_get_numeral_significand_bv let mk_to_ieee_bv = Z3native.mk_fpa_to_ieee_bv let mk_to_fp_int_real = Z3native.mk_fpa_to_fp_int_real let numeral_to_string x = Z3native.get_numeral_string (Expr.gc x) x diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index e08028c61..2a73c08fb 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -2138,36 +2138,36 @@ sig (** Retrieves the number of bits reserved for the significand in a FloatingPoint sort. *) val get_sbits : context -> Sort.sort -> int + (** Retrieves the sign of a floating-point literal. *) + val get_numeral_sign : context -> Expr.expr -> bool * int + (** Return the sign of a floating-point numeral as a bit-vector expression. Remark: NaN's do not have a bit-vector sign, so they are invalid arguments. *) val get_numeral_sign_bv : context -> Expr.expr -> Expr.expr + (** Return the exponent value of a floating-point numeral as a string *) + val get_numeral_exponent_string : context -> Expr.expr -> bool -> string + + (** Return the exponent value of a floating-point numeral as a signed integer *) + val get_numeral_exponent_int : context -> Expr.expr -> bool -> bool * int + (** Return the exponent of a floating-point numeral as a bit-vector expression. - Remark: +oo, -oo and NaN's do not have a bit-vector exponent, so they are invalid arguments. *) - val get_numeral_exponent_bv : context -> Expr.expr -> Expr.expr + Remark: NaN's do not have a bit-vector exponent, so they are invalid arguments. *) + val get_numeral_exponent_bv : context -> Expr.expr -> bool -> Expr.expr (** Return the significand value of a floating-point numeral as a bit-vector expression. - Remark: +oo, -oo and NaN's do not have a bit-vector significand, so they are invalid arguments. *) + Remark: NaN's do not have a bit-vector significand, so they are invalid arguments. *) val get_numeral_significand_bv : context -> Expr.expr -> Expr.expr - (** Retrieves the sign of a floating-point literal. *) - val get_numeral_sign : context -> Expr.expr -> bool * int - (** Return the significand value of a floating-point numeral as a string. *) val get_numeral_significand_string : context -> Expr.expr -> string (** Return the significand value of a floating-point numeral as a uint64. Remark: This function extracts the significand bits, without the hidden bit or normalization. Throws an exception if the - significand does not fit into a uint64. *) + significand does not fit into an int. *) val get_numeral_significand_uint : context -> Expr.expr -> bool * int - (** Return the exponent value of a floating-point numeral as a string *) - val get_numeral_exponent_string : context -> Expr.expr -> string - - (** Return the exponent value of a floating-point numeral as a signed integer *) - val get_numeral_exponent_int : context -> Expr.expr -> bool * int - (** Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. *) val mk_to_ieee_bv : context -> Expr.expr -> Expr.expr @@ -3035,29 +3035,22 @@ sig (** Assert a constraint (or multiple) into the solver. *) val add : solver -> Expr.expr list -> unit - (** * Assert multiple constraints (cs) into the solver, and track them (in the - * unsat) core - * using the Boolean constants in ps. - * - * This API is an alternative to {!check} with assumptions for - * extracting unsat cores. - * Both APIs can be used in the same solver. The unsat core will contain a - * combination - * of the Boolean variables provided using {!assert_and_track} - * and the Boolean literals - * provided using {!check} with assumptions. *) + (** Assert multiple constraints (cs) into the solver, and track them (in the + unsat) core using the Boolean constants in ps. + + This API is an alternative to {!check} with assumptions for extracting unsat cores. + Both APIs can be used in the same solver. The unsat core will contain a combination + of the Boolean variables provided using {!assert_and_track} and the Boolean literals + provided using {!check} with assumptions. *) val assert_and_track_l : solver -> Expr.expr list -> Expr.expr list -> unit - (** * Assert a constraint (c) into the solver, and track it (in the unsat) core - * using the Boolean constant p. - * - * This API is an alternative to {!check} with assumptions for - * extracting unsat cores. - * Both APIs can be used in the same solver. The unsat core will contain a - * combination - * of the Boolean variables provided using {!assert_and_track} - * and the Boolean literals - * provided using {!check} with assumptions. *) + (** Assert a constraint (c) into the solver, and track it (in the unsat) core + using the Boolean constant p. + + This API is an alternative to {!check} with assumptions for extracting unsat cores. + Both APIs can be used in the same solver. The unsat core will contain a combination + of the Boolean variables provided using {!assert_and_track} and the Boolean literals + provided using {!check} with assumptions. *) val assert_and_track : solver -> Expr.expr -> Expr.expr -> unit (** The number of assertions in the solver. *) diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp index d9fe9ab72..d598dfa39 100644 --- a/src/cmd_context/check_logic.cpp +++ b/src/cmd_context/check_logic.cpp @@ -24,7 +24,7 @@ Revision History: #include"datatype_decl_plugin.h" #include"ast_pp.h" #include"for_each_expr.h" -#include +#include struct check_logic::imp { ast_manager & m; @@ -189,7 +189,7 @@ struct check_logic::imp { else { m_unknown_logic = true; } - + m_logic = logic; } @@ -237,7 +237,7 @@ struct check_logic::imp { } } - void operator()(var * n) { + void operator()(var * n) { if (!m_quantifiers) fail("logic does not support quantifiers"); check_sort(m.get_sort(n)); @@ -279,7 +279,7 @@ struct check_logic::imp { } } } - + // check if the divisor is a numeral void check_div(app * n) { SASSERT(n->get_num_args() == 2); @@ -328,8 +328,8 @@ struct check_logic::imp { return false; non_numeral = arg; } - if (non_numeral == 0) - return true; + if (non_numeral == 0) + return true; if (is_diff_var(non_numeral)) return true; if (!m_a_util.is_add(non_numeral) && !m_a_util.is_sub(non_numeral)) @@ -338,10 +338,10 @@ struct check_logic::imp { } return true; } - + bool is_diff_arg(expr * t) { if (is_diff_var(t)) - return true; + return true; if (is_numeral(t)) return true; if (m_a_util.is_add(t) || m_a_util.is_sub(t)) @@ -366,7 +366,7 @@ struct check_logic::imp { expr * t1 = to_app(lhs)->get_arg(0); expr * t2 = to_app(lhs)->get_arg(1); if (is_diff_var(t1) && is_diff_var(t2)) - return; + return; if (m_a_util.is_add(t1) && m_a_util.is_add(t2)) { // QF_RDL supports (<= (- (+ x ... x) (+ y ... y)) c) if (to_app(t1)->get_num_args() != to_app(t2)->get_num_args()) @@ -391,7 +391,7 @@ struct check_logic::imp { check_diff_arg(n); } } - + void operator()(app * n) { sort * s = m.get_sort(n); check_sort(s); @@ -415,18 +415,18 @@ struct check_logic::imp { if (!m_ints || !m_reals) { if (m_a_util.is_to_real(n) || m_a_util.is_to_int(n)) fail("logic does not support casting operators"); - } + } } else if (fid == m_bv_util.get_family_id()) { - // nothing to check... + // nothing to check... } else if (fid == m_ar_util.get_family_id()) { - // nothing to check... + // nothing to check... if (m_diff) check_diff_args(n); } else if (fid == m.get_basic_family_id()) { - // nothing to check... + // nothing to check... if (m_diff) { if (m.is_eq(n)) check_diff_predicate(n); @@ -449,8 +449,8 @@ struct check_logic::imp { fail(strm.str().c_str()); } } - - void operator()(quantifier * n) { + + void operator()(quantifier * n) { if (!m_quantifiers) fail("logic does not support quantifiers"); } @@ -490,7 +490,7 @@ struct check_logic::imp { check_logic::check_logic() { m_imp = 0; } - + check_logic::~check_logic() { if (m_imp) dealloc(m_imp);