mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

ML API bugfixes for FPA numeral accessors

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-10-24 13:32:37 +01:00
parent abcb6040d4 df2a569d25
commit 7517cf485e
3 changed files with 49 additions and 56 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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

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

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

34
src/cmd_context/check_logic.cpp
View file

@ -24,7 +24,7 @@ Revision History:
#include"datatype_decl_plugin.h"
#include"ast_pp.h"
#include"for_each_expr.h"
#include<strstream>
#include<sstream>
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);