mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

resolved merge conflicts

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-03-07 14:20:10 +00:00
commit 027331aef2
134 changed files with 4579 additions and 651 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/ackermannization/ackermannize_bv_tactic.cpp
View file

@ -24,8 +24,7 @@ Revision History:
class ackermannize_bv_tactic : public tactic {
public:
ackermannize_bv_tactic(ast_manager& m, params_ref const& p)
: m_m(m)
, m_p(p)
: m(m), m_p(p)
{}
virtual ~ackermannize_bv_tactic() { }
@ -36,7 +35,6 @@ public:
proof_converter_ref & pc,
expr_dependency_ref & core) {
mc = 0;
ast_manager& m(g->m());
tactic_report report("ackermannize", *g);
fail_if_unsat_core_generation("ackermannize", g);
fail_if_proof_generation("ackermannize", g);
@ -44,11 +42,11 @@ public:
expr_ref_vector flas(m);
const unsigned sz = g->size();
for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i));
scoped_ptr<lackr> imp = alloc(lackr, m, m_p, m_st, flas, NULL);
flas.reset();
lackr lackr(m, m_p, m_st, flas, NULL);
// mk result
goal_ref resg(alloc(goal, *g, true));
const bool success = imp->mk_ackermann(resg, m_lemma_limit);
const bool success = lackr.mk_ackermann(resg, m_lemma_limit);
if (!success) { // Just pass on the input unchanged
result.reset();
result.push_back(g.get());
@ -60,12 +58,12 @@ public:
result.push_back(resg.get());
// report model
if (g->models_enabled()) {
mc = mk_ackermannize_bv_model_converter(m, imp->get_info());
mc = mk_ackermannize_bv_model_converter(m, lackr.get_info());
}
resg->inc_depth();
TRACE("ackermannize", resg->display(tout););
SASSERT(resg->is_well_sorted());
resg->inc_depth();
TRACE("ackermannize", resg->display(tout););
SASSERT(resg->is_well_sorted());
}
@ -86,7 +84,7 @@ public:
return alloc(ackermannize_bv_tactic, m, m_p);
}
private:
ast_manager& m_m;
ast_manager& m;
params_ref m_p;
lackr_stats m_st;
double m_lemma_limit;

26
src/api/python/z3.py
View file

@ -8944,7 +8944,31 @@ def fpFP(sgn, exp, sig, ctx=None):
return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx)
def fpToFP(a1, a2=None, a3=None, ctx=None):
"""Create a Z3 floating-point conversion expression from other terms."""
"""Create a Z3 floating-point conversion expression from other term sorts
to floating-point.
From a bit-vector term in IEEE 754-2008 format:
>>> x = FPVal(1.0, Float32())
>>> x_bv = fpToIEEEBV(x)
>>> simplify(fpToFP(x_bv, Float32()))
1
From a floating-point term with different precision:
>>> x = FPVal(1.0, Float32())
>>> x_db = fpToFP(RNE(), x, Float64())
>>> x_db.sort()
FPSort(11, 53)
From a real term:
>>> x_r = RealVal(1.5)
>>> simplify(fpToFP(RNE(), x_r, Float32()))
1.5
From a signed bit-vector term:
>>> x_signed = BitVecVal(-5, BitVecSort(32))
>>> simplify(fpToFP(RNE(), x_signed, Float32()))
-1.25*(2**2)
"""
ctx = _get_ctx(ctx)
if is_bv(a1) and is_fp_sort(a2):
return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), a1.ast, a2.ast), ctx)

31
src/api/z3_api.h
View file

@ -62,7 +62,7 @@ DEFINE_TYPE(Z3_rcf_num);
- \c Z3_constructor: type constructor for a (recursive) datatype.
- \c Z3_constructor_list: list of constructors for a (recursive) datatype.
- \c Z3_params: parameter set used to configure many components such as: simplifiers, tactics, solvers, etc.
- \c Z3_param_descrs: provides a collection of parameter names, their types, default values and documentation strings. Solvers, tactics, and other objects accept different collection of parameters.
- \c Z3_param_descrs: provides a collection of parameter names, their types, default values and documentation strings. Solvers, tactics, and other objects accept different collection of parameters.
- \c Z3_model: model for the constraints asserted into the logical context.
- \c Z3_func_interp: interpretation of a function in a model.
- \c Z3_func_entry: representation of the value of a \c Z3_func_interp at a particular point.
@ -1129,7 +1129,7 @@ typedef enum {
Z3_OP_SEQ_EXTRACT,
Z3_OP_SEQ_REPLACE,
Z3_OP_SEQ_AT,
Z3_OP_SEQ_LENGTH,
Z3_OP_SEQ_LENGTH,
Z3_OP_SEQ_INDEX,
Z3_OP_SEQ_TO_RE,
Z3_OP_SEQ_IN_RE,
@ -1457,7 +1457,7 @@ extern "C" {
/*@{*/
/**
\deprecated
\deprecated
\brief Create a context using the given configuration.
After a context is created, the configuration cannot be changed,
@ -1474,6 +1474,11 @@ extern "C" {
Z3_solver, Z3_func_interp have to be managed by the caller.
Their reference counts are not handled by the context.
Further remarks:
- Z3_sort, Z3_func_decl, Z3_app, Z3_pattern are Z3_ast's.
- Z3 uses hash-consing, i.e., when the same Z3_ast is created twice,
Z3 will return the same pointer twice.
\sa Z3_del_context
def_API('Z3_mk_context', CONTEXT, (_in(CONFIG),))
@ -1492,11 +1497,13 @@ extern "C" {
anymore. This idiom is similar to the one used in
BDD (binary decision diagrams) packages such as CUDD.
Remark: Z3_sort, Z3_func_decl, Z3_app, Z3_pattern are
Z3_ast's.
Remarks:
After a context is created, the configuration cannot be changed.
All main interaction with Z3 happens in the context of a \c Z3_context.
- Z3_sort, Z3_func_decl, Z3_app, Z3_pattern are Z3_ast's.
- After a context is created, the configuration cannot be changed.
- All main interaction with Z3 happens in the context of a \c Z3_context.
- Z3 uses hash-consing, i.e., when the same Z3_ast is created twice,
Z3 will return the same pointer twice.
def_API('Z3_mk_context_rc', CONTEXT, (_in(CONFIG),))
*/
@ -3185,11 +3192,11 @@ extern "C" {
def_API('Z3_is_string', BOOL, (_in(CONTEXT), _in(AST)))
*/
Z3_bool Z3_API Z3_is_string(Z3_context c, Z3_ast s);
Z3_bool Z3_API Z3_is_string(Z3_context c, Z3_ast s);
/**
\brief Retrieve the string constant stored in \c s.
\pre Z3_is_string(c, s)
def_API('Z3_get_string' ,STRING ,(_in(CONTEXT), _in(AST)))
@ -3285,7 +3292,7 @@ extern "C" {
def_API('Z3_mk_seq_index' ,AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset);
/**
\brief Create a regular expression that accepts the sequence \c seq.
@ -4429,8 +4436,8 @@ extern "C" {
Provides an interface to the AST simplifier used by Z3.
It returns an AST object which is equal to the argument.
The returned AST is simplified using algebraic simplificaiton rules,
such as constant propagation (propagating true/false over logical connectives).
The returned AST is simplified using algebraic simplificaiton rules,
such as constant propagation (propagating true/false over logical connectives).
def_API('Z3_simplify', AST, (_in(CONTEXT), _in(AST)))
*/

1
src/ast/ast.cpp
View file

@ -2095,6 +2095,7 @@ inline app * ast_manager::mk_app_core(func_decl * decl, expr * arg1, expr * arg2
}
app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * args) {
bool type_error =
decl->get_arity() != num_args && !decl->is_right_associative() &&
!decl->is_left_associative() && !decl->is_chainable();

2
src/ast/ast.h
View file

@ -972,7 +972,7 @@ public:
*/
virtual bool is_unique_value(app * a) const { return false; }
virtual bool are_equal(app * a, app * b) const { return a == b && is_unique_value(a) && is_unique_value(b); }
virtual bool are_equal(app * a, app * b) const { return a == b; }
virtual bool are_distinct(app * a, app * b) const { return a != b && is_unique_value(a) && is_unique_value(b); }

2
src/ast/ast_smt2_pp.cpp
View file

@ -1075,7 +1075,7 @@ public:
if (strcmp(var_prefix, ALIAS_PREFIX) == 0) {
var_prefix = "_a";
}
unsigned idx = 1;
unsigned idx = 0;
for (unsigned i = 0; i < num; i++) {
symbol name = next_name(var_prefix, idx);
name = ensure_quote_sym(name);

117
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -81,7 +81,7 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_INTERNAL_RM));
TRACE("fpa2bv", tout << "mk_eq_rm a=" << mk_ismt2_pp(a, m) << std::endl;
tout << "mk_eq_rm b=" << mk_ismt2_pp(b, m) << std::endl;);
tout << "mk_eq_rm b=" << mk_ismt2_pp(b, m) << std::endl;);
m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), result);
}
@ -113,9 +113,10 @@ void fpa2bv_converter::mk_distinct(func_decl * f, unsigned num, expr * const * a
result = m.mk_true();
for (unsigned i = 0; i < num; i++) {
for (unsigned j = i+1; j < num; j++) {
expr_ref eq(m);
expr_ref eq(m), neq(m);
mk_eq(args[i], args[j], eq);
m_simp.mk_and(result, m.mk_not(eq), result);
neq = m.mk_not(eq);
m_simp.mk_and(result, neq, result);
}
}
}
@ -422,10 +423,11 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits,
if (log2(sbits + 2) < ebits + 2)
{
// cap the delta
expr_ref cap(m), cap_le_delta(m);
expr_ref cap(m), cap_le_delta(m), exp_delta_ext(m);
cap = m_bv_util.mk_numeral(sbits + 2, ebits + 2);
cap_le_delta = m_bv_util.mk_ule(cap, m_bv_util.mk_zero_extend(2, exp_delta));
m_simp.mk_ite(cap_le_delta, cap, m_bv_util.mk_zero_extend(2, exp_delta), exp_delta);
exp_delta_ext = m_bv_util.mk_zero_extend(2, exp_delta);
m_simp.mk_ite(cap_le_delta, cap, exp_delta_ext, exp_delta);
exp_delta = m_bv_util.mk_extract(ebits - 1, 0, exp_delta);
dbg_decouple("fpa2bv_add_exp_cap", cap);
}
@ -465,7 +467,7 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits,
expr_ref eq_sgn(m);
m_simp.mk_eq(c_sgn, d_sgn, eq_sgn);
// dbg_decouple("fpa2bv_add_eq_sgn", eq_sgn);
dbg_decouple("fpa2bv_add_eq_sgn", eq_sgn);
TRACE("fpa2bv_add_core", tout << "EQ_SGN = " << mk_ismt2_pp(eq_sgn, m) << std::endl; );
// two extra bits for catching the overflow.
@ -478,11 +480,10 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits,
dbg_decouple("fpa2bv_add_c_sig", c_sig);
dbg_decouple("fpa2bv_add_shifted_d_sig", shifted_d_sig);
expr_ref sum(m);
m_simp.mk_ite(eq_sgn,
m_bv_util.mk_bv_add(c_sig, shifted_d_sig),
m_bv_util.mk_bv_sub(c_sig, shifted_d_sig),
sum);
expr_ref sum(m), c_plus_d(m), c_minus_d(m);
c_plus_d = m_bv_util.mk_bv_add(c_sig, shifted_d_sig);
c_minus_d = m_bv_util.mk_bv_sub(c_sig, shifted_d_sig);
m_simp.mk_ite(eq_sgn, c_plus_d, c_minus_d, sum);
SASSERT(is_well_sorted(m, sum));
@ -594,7 +595,7 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args,
c6 = y_is_zero;
v6 = x;
// Actual addition.
//// Actual addition.
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
@ -949,8 +950,11 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args,
dbg_decouple("fpa2bv_div_res_sig_shift_amount", res_sig_shift_amount);
expr_ref shift_cond(m);
shift_cond = m_bv_util.mk_ule(res_sig_lz, m_bv_util.mk_numeral(1, sbits + 4));
m_simp.mk_ite(shift_cond, res_sig, m_bv_util.mk_bv_shl(res_sig, res_sig_shift_amount), res_sig);
m_simp.mk_ite(shift_cond, res_exp, m_bv_util.mk_bv_sub(res_exp, m_bv_util.mk_extract(ebits+1, 0, res_sig_shift_amount)), res_exp);
expr_ref res_sig_shifted(m), res_exp_shifted(m);
res_sig_shifted = m_bv_util.mk_bv_shl(res_sig, res_sig_shift_amount);
res_exp_shifted = m_bv_util.mk_bv_sub(res_exp, m_bv_util.mk_extract(ebits + 1, 0, res_sig_shift_amount));
m_simp.mk_ite(shift_cond, res_sig, res_sig_shifted, res_sig);
m_simp.mk_ite(shift_cond, res_exp, res_exp_shifted, res_exp);
round(f->get_range(), bv_rm, res_sgn, res_sig, res_exp, v8);
@ -1374,8 +1378,9 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
// (x is 0) || (y is 0) -> z
m_simp.mk_or(x_is_zero, y_is_zero, c7);
expr_ref ite_c(m);
m_simp.mk_and(z_is_zero, m.mk_not(rm_is_to_neg), ite_c);
expr_ref ite_c(m), rm_is_not_to_neg(m);
rm_is_not_to_neg = m.mk_not(rm_is_to_neg);
m_simp.mk_and(z_is_zero, rm_is_not_to_neg, ite_c);
mk_ite(ite_c, pzero, z, v7);
// else comes the fused multiplication.
@ -1512,11 +1517,10 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
dbg_decouple("fpa2bv_fma_add_e_sig", e_sig);
dbg_decouple("fpa2bv_fma_add_shifted_f_sig", shifted_f_sig);
expr_ref sum(m);
m_simp.mk_ite(eq_sgn,
m_bv_util.mk_bv_add(e_sig, shifted_f_sig),
m_bv_util.mk_bv_sub(e_sig, shifted_f_sig),
sum);
expr_ref sum(m), e_plus_f(m), e_minus_f(m);
e_plus_f = m_bv_util.mk_bv_add(e_sig, shifted_f_sig);
e_minus_f = m_bv_util.mk_bv_sub(e_sig, shifted_f_sig),
m_simp.mk_ite(eq_sgn, e_plus_f, e_minus_f, sum);
SASSERT(is_well_sorted(m, sum));
@ -1664,10 +1668,10 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args,
dbg_decouple("fpa2bv_sqrt_e_is_odd", e_is_odd);
dbg_decouple("fpa2bv_sqrt_real_exp", real_exp);
expr_ref sig_prime(m);
m_simp.mk_ite(e_is_odd, m_bv_util.mk_concat(a_sig, zero1),
m_bv_util.mk_concat(zero1, a_sig),
sig_prime);
expr_ref sig_prime(m), a_z(m), z_a(m);
a_z = m_bv_util.mk_concat(a_sig, zero1);
z_a = m_bv_util.mk_concat(zero1, a_sig);
m_simp.mk_ite(e_is_odd, a_z, z_a, sig_prime);
SASSERT(m_bv_util.get_bv_size(sig_prime) == sbits+1);
dbg_decouple("fpa2bv_sqrt_sig_prime", sig_prime);
@ -1696,21 +1700,22 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args,
SASSERT(m_bv_util.get_bv_size(S) == sbits + 5);
SASSERT(m_bv_util.get_bv_size(T) == sbits + 6);
expr_ref t_lt_0(m);
m_simp.mk_eq(m_bv_util.mk_extract(sbits+5, sbits+5, T), one1, t_lt_0);
expr_ref t_lt_0(m), T_lsds5(m);
T_lsds5 = m_bv_util.mk_extract(sbits + 5, sbits + 5, T);
m_simp.mk_eq(T_lsds5, one1, t_lt_0);
expr * or_args[2] = { Q, S };
m_simp.mk_ite(t_lt_0, Q,
m_bv_util.mk_bv_or(2, or_args),
Q);
m_simp.mk_ite(t_lt_0, m_bv_util.mk_concat(m_bv_util.mk_extract(sbits+3, 0, R), zero1),
m_bv_util.mk_extract(sbits+4, 0, T),
R);
expr_ref Q_or_S(m), R_shftd(m), T_lsds4(m);
Q_or_S = m_bv_util.mk_bv_or(2, or_args);
m_simp.mk_ite(t_lt_0, Q, Q_or_S, Q);
R_shftd = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits + 3, 0, R), zero1);
T_lsds4 = m_bv_util.mk_extract(sbits + 4, 0, T);
m_simp.mk_ite(t_lt_0, R_shftd, T_lsds4, R);
}
expr_ref is_exact(m);
m_simp.mk_eq(R, m_bv_util.mk_numeral(0, sbits+5), is_exact);
expr_ref is_exact(m), zero_sbits5(m);
zero_sbits5 = m_bv_util.mk_numeral(0, sbits + 5);
m_simp.mk_eq(R, zero_sbits5, is_exact);
dbg_decouple("fpa2bv_sqrt_is_exact", is_exact);
expr_ref rest(m), last(m), q_is_odd(m), rest_ext(m);
@ -1719,10 +1724,10 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args,
dbg_decouple("fpa2bv_sqrt_last", last);
dbg_decouple("fpa2bv_sqrt_rest", rest);
rest_ext = m_bv_util.mk_zero_extend(1, rest);
expr_ref sticky(m);
m_simp.mk_ite(is_exact, m_bv_util.mk_zero_extend(sbits+3, last),
m_bv_util.mk_numeral(1, sbits+4),
sticky);
expr_ref sticky(m), last_ext(m), one_sbits4(m);
last_ext = m_bv_util.mk_zero_extend(sbits + 3, last);
one_sbits4 = m_bv_util.mk_numeral(1, sbits + 4);
m_simp.mk_ite(is_exact, last_ext, one_sbits4, sticky);
expr * or_args[2] = { rest_ext, sticky };
res_sig = m_bv_util.mk_bv_or(2, or_args);
@ -1813,8 +1818,11 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
mk_one(f, one_1, none);
mk_ite(m.mk_eq(a_sgn, one_1), none, pone, xone);
m_simp.mk_eq(a_sig, m_bv_util.mk_numeral(fu().fm().m_powers2(sbits-1), sbits), t1);
m_simp.mk_eq(a_exp, m_bv_util.mk_numeral(-1, ebits), t2);
expr_ref pow_2_sbitsm1(m), m1(m);
pow_2_sbitsm1 = m_bv_util.mk_numeral(fu().fm().m_powers2(sbits - 1), sbits);
m1 = m_bv_util.mk_numeral(-1, ebits);
m_simp.mk_eq(a_sig, pow_2_sbitsm1, t1);
m_simp.mk_eq(a_exp, m1, t2);
m_simp.mk_and(t1, t2, tie);
dbg_decouple("fpa2bv_r2i_c42_tie", tie);
@ -1896,14 +1904,17 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
SASSERT(is_well_sorted(m, tie2_c));
SASSERT(is_well_sorted(m, v51));
expr_ref c521(m), v52(m);
m_simp.mk_not(m.mk_eq(rem, m_bv_util.mk_numeral(0, sbits+1)), c521);
m_simp.mk_and(c521, m.mk_eq(res_sgn, zero_1), c521);
expr_ref c521(m), v52(m), rem_eq_0(m), sgn_eq_zero(m);
rem_eq_0 = m.mk_eq(rem, m_bv_util.mk_numeral(0, sbits + 1));
sgn_eq_zero = m.mk_eq(res_sgn, zero_1);
m_simp.mk_not(rem_eq_0, c521);
m_simp.mk_and(c521, sgn_eq_zero, c521);
m_simp.mk_ite(c521, div_p1, div, v52);
expr_ref c531(m), v53(m);
m_simp.mk_not(m.mk_eq(rem, m_bv_util.mk_numeral(0, sbits+1)), c531);
m_simp.mk_and(c531, m.mk_eq(res_sgn, one_1), c531);
expr_ref c531(m), v53(m), sgn_eq_one(m);
sgn_eq_one = m.mk_eq(res_sgn, one_1);
m_simp.mk_not(rem_eq_0, c531);
m_simp.mk_and(c531, sgn_eq_one, c531);
m_simp.mk_ite(c531, div_p1, div, v53);
expr_ref c51(m), c52(m), c53(m);
@ -3377,9 +3388,10 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref
zero_s = m_bv_util.mk_numeral(0, sbits);
m_simp.mk_eq(zero_s, denormal_sig, is_sig_zero);
expr_ref lz_d(m);
expr_ref lz_d(m), norm_or_zero(m);
mk_leading_zeros(denormal_sig, ebits, lz_d);
m_simp.mk_ite(m.mk_or(is_normal, is_sig_zero), zero_e, lz_d, lz);
norm_or_zero = m.mk_or(is_normal, is_sig_zero);
m_simp.mk_ite(norm_or_zero, zero_e, lz_d, lz);
dbg_decouple("fpa2bv_unpack_lz", lz);
expr_ref shift(m);
@ -3770,8 +3782,9 @@ void fpa2bv_converter::round(sort * s, expr_ref & bv_rm, expr_ref & sgn, expr_re
dbg_decouple("fpa2bv_rnd_rm_is_to_pos", rm_is_to_pos);
expr_ref sgn_is_zero(m);
m_simp.mk_eq(sgn, m_bv_util.mk_numeral(0, 1), sgn_is_zero);
expr_ref sgn_is_zero(m), zero1(m);
zero1 = m_bv_util.mk_numeral(0, 1);
m_simp.mk_eq(sgn, zero1, sgn_is_zero);
dbg_decouple("fpa2bv_rnd_sgn_is_zero", sgn_is_zero);
expr_ref max_sig(m), max_exp(m), inf_sig(m), inf_exp(m);

13
src/ast/fpa/fpa2bv_converter.h
View file

@ -26,19 +26,6 @@ Notes:
#include"bv_decl_plugin.h"
#include"basic_simplifier_plugin.h"
struct func_decl_triple {
func_decl_triple () { f_sgn = 0; f_sig = 0; f_exp = 0; }
func_decl_triple (func_decl * sgn, func_decl * sig, func_decl * exp)
{
f_sgn = sgn;
f_sig = sig;
f_exp = exp;
}
func_decl * f_sgn;
func_decl * f_sig;
func_decl * f_exp;
};
class fpa2bv_converter {
protected:
ast_manager & m;

270
src/ast/fpa/fpa2bv_rewriter.cpp Normal file
View file

@ -0,0 +1,270 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
fpa2bv_rewriter.cpp
Abstract:
Rewriter for converting FPA to BV
Author:
Christoph (cwinter) 2012-02-09
Notes:
--*/
#include"rewriter_def.h"
#include"fpa2bv_rewriter.h"
#include"cooperate.h"
#include"fpa2bv_rewriter_params.hpp"
fpa2bv_rewriter_cfg::fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, params_ref const & p) :
m_manager(m),
m_out(m),
m_conv(c),
m_bindings(m)
{
updt_params(p);
// We need to make sure that the mananger has the BV plugin loaded.
symbol s_bv("bv");
if (!m_manager.has_plugin(s_bv))
m_manager.register_plugin(s_bv, alloc(bv_decl_plugin));
}
void fpa2bv_rewriter_cfg::updt_local_params(params_ref const & _p) {
fpa2bv_rewriter_params p(_p);
bool v = p.hi_fp_unspecified();
m_conv.set_unspecified_fp_hi(v);
}
void fpa2bv_rewriter_cfg::updt_params(params_ref const & p) {
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_max_steps = p.get_uint("max_steps", UINT_MAX);
updt_local_params(p);
}
bool fpa2bv_rewriter_cfg::max_steps_exceeded(unsigned num_steps) const {
cooperate("fpa2bv");
return num_steps > m_max_steps;
}
br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
TRACE("fpa2bv_rw", tout << "APP: " << f->get_name() << std::endl; );
if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_float(f->get_range())) {
m_conv.mk_const(f, result);
return BR_DONE;
}
if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm(f->get_range())) {
m_conv.mk_rm_const(f, result);
return BR_DONE;
}
if (m().is_eq(f)) {
SASSERT(num == 2);
TRACE("fpa2bv_rw", tout << "(= " << mk_ismt2_pp(args[0], m()) << " " <<
mk_ismt2_pp(args[1], m()) << ")" << std::endl;);
SASSERT(m().get_sort(args[0]) == m().get_sort(args[1]));
sort * ds = f->get_domain()[0];
if (m_conv.is_float(ds)) {
m_conv.mk_eq(args[0], args[1], result);
return BR_DONE;
}
else if (m_conv.is_rm(ds)) {
result = m().mk_eq(args[0], args[1]);
return BR_DONE;
}
return BR_FAILED;
}
else if (m().is_ite(f)) {
SASSERT(num == 3);
if (m_conv.is_float(args[1])) {
m_conv.mk_ite(args[0], args[1], args[2], result);
return BR_DONE;
}
return BR_FAILED;
}
else if (m().is_distinct(f)) {
sort * ds = f->get_domain()[0];
if (m_conv.is_float(ds) || m_conv.is_rm(ds)) {
m_conv.mk_distinct(f, num, args, result);
return BR_DONE;
}
return BR_FAILED;
}
if (m_conv.is_float_family(f)) {
switch (f->get_decl_kind()) {
case OP_FPA_RM_NEAREST_TIES_TO_AWAY:
case OP_FPA_RM_NEAREST_TIES_TO_EVEN:
case OP_FPA_RM_TOWARD_NEGATIVE:
case OP_FPA_RM_TOWARD_POSITIVE:
case OP_FPA_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f, result); return BR_DONE;
case OP_FPA_NUM: m_conv.mk_numeral(f, num, args, result); return BR_DONE;
case OP_FPA_PLUS_INF: m_conv.mk_pinf(f, result); return BR_DONE;
case OP_FPA_MINUS_INF: m_conv.mk_ninf(f, result); return BR_DONE;
case OP_FPA_PLUS_ZERO: m_conv.mk_pzero(f, result); return BR_DONE;
case OP_FPA_MINUS_ZERO: m_conv.mk_nzero(f, result); return BR_DONE;
case OP_FPA_NAN: m_conv.mk_nan(f, result); return BR_DONE;
case OP_FPA_ADD: m_conv.mk_add(f, num, args, result); return BR_DONE;
case OP_FPA_SUB: m_conv.mk_sub(f, num, args, result); return BR_DONE;
case OP_FPA_NEG: m_conv.mk_neg(f, num, args, result); return BR_DONE;
case OP_FPA_MUL: m_conv.mk_mul(f, num, args, result); return BR_DONE;
case OP_FPA_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE;
case OP_FPA_REM: m_conv.mk_rem(f, num, args, result); return BR_DONE;
case OP_FPA_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE;
case OP_FPA_FMA: m_conv.mk_fma(f, num, args, result); return BR_DONE;
case OP_FPA_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE;
case OP_FPA_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE;
case OP_FPA_EQ: m_conv.mk_float_eq(f, num, args, result); return BR_DONE;
case OP_FPA_LT: m_conv.mk_float_lt(f, num, args, result); return BR_DONE;
case OP_FPA_GT: m_conv.mk_float_gt(f, num, args, result); return BR_DONE;
case OP_FPA_LE: m_conv.mk_float_le(f, num, args, result); return BR_DONE;
case OP_FPA_GE: m_conv.mk_float_ge(f, num, args, result); return BR_DONE;
case OP_FPA_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE;
case OP_FPA_IS_NAN: m_conv.mk_is_nan(f, num, args, result); return BR_DONE;
case OP_FPA_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE;
case OP_FPA_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE;
case OP_FPA_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE;
case OP_FPA_IS_POSITIVE: m_conv.mk_is_positive(f, num, args, result); return BR_DONE;
case OP_FPA_IS_NEGATIVE: m_conv.mk_is_negative(f, num, args, result); return BR_DONE;
case OP_FPA_TO_FP: m_conv.mk_to_fp(f, num, args, result); return BR_DONE;
case OP_FPA_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE;
case OP_FPA_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE;
case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE;
case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_REWRITE_FULL;
case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_REWRITE_FULL;
case OP_FPA_INTERNAL_MIN_UNSPECIFIED: result = m_conv.mk_min_unspecified(f, args[0], args[1]); return BR_DONE;
case OP_FPA_INTERNAL_MAX_UNSPECIFIED: result = m_conv.mk_max_unspecified(f, args[0], args[1]); return BR_DONE;
case OP_FPA_INTERNAL_MIN_I: m_conv.mk_min_i(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_RM:
case OP_FPA_INTERNAL_BVWRAP:
case OP_FPA_INTERNAL_BVUNWRAP:
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: return BR_FAILED;
default:
TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n";
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);
NOT_IMPLEMENTED_YET();
}
}
else {
SASSERT(!m_conv.is_float_family(f));
bool is_float_uf = m_conv.is_float(f->get_range()) || m_conv.is_rm(f->get_range());
for (unsigned i = 0; i < f->get_arity(); i++) {
sort * di = f->get_domain()[i];
is_float_uf |= m_conv.is_float(di) || m_conv.is_rm(di);
}
if (is_float_uf) {
m_conv.mk_uninterpreted_function(f, num, args, result);
return BR_DONE;
}
}
return BR_FAILED;
}
bool fpa2bv_rewriter_cfg::pre_visit(expr * t)
{
TRACE("fpa2bv", tout << "pre_visit: " << mk_ismt2_pp(t, m()) << std::endl;);
if (is_quantifier(t)) {
quantifier * q = to_quantifier(t);
TRACE("fpa2bv", tout << "pre_visit quantifier [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m()) << std::endl;);
sort_ref_vector new_bindings(m_manager);
for (unsigned i = 0 ; i < q->get_num_decls(); i++)
new_bindings.push_back(q->get_decl_sort(i));
SASSERT(new_bindings.size() == q->get_num_decls());
m_bindings.append(new_bindings);
}
return true;
}
bool fpa2bv_rewriter_cfg::reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr) {
unsigned curr_sz = m_bindings.size();
SASSERT(old_q->get_num_decls() <= curr_sz);
unsigned num_decls = old_q->get_num_decls();
unsigned old_sz = curr_sz - num_decls;
string_buffer<> name_buffer;
ptr_buffer<sort> new_decl_sorts;
sbuffer<symbol> new_decl_names;
for (unsigned i = 0; i < num_decls; i++) {
symbol const & n = old_q->get_decl_name(i);
sort * s = old_q->get_decl_sort(i);
if (m_conv.is_float(s)) {
unsigned ebits = m_conv.fu().get_ebits(s);
unsigned sbits = m_conv.fu().get_sbits(s);
name_buffer.reset();
name_buffer << n << ".bv";
new_decl_names.push_back(symbol(name_buffer.c_str()));
new_decl_sorts.push_back(m_conv.bu().mk_sort(sbits+ebits));
}
else {
new_decl_sorts.push_back(s);
new_decl_names.push_back(n);
}
}
result = m().mk_quantifier(old_q->is_forall(), new_decl_sorts.size(), new_decl_sorts.c_ptr(), new_decl_names.c_ptr(),
new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(),
old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns);
result_pr = 0;
m_bindings.shrink(old_sz);
TRACE("fpa2bv", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " <<
mk_ismt2_pp(old_q->get_expr(), m()) << std::endl <<
" new body: " << mk_ismt2_pp(new_body, m()) << std::endl;
tout << "result = " << mk_ismt2_pp(result, m()) << std::endl;);
return true;
}
bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & result_pr) {
if (t->get_idx() >= m_bindings.size())
return false;
// unsigned inx = m_bindings.size() - t->get_idx() - 1;
expr_ref new_exp(m());
sort * s = t->get_sort();
if (m_conv.is_float(s))
{
expr_ref new_var(m());
unsigned ebits = m_conv.fu().get_ebits(s);
unsigned sbits = m_conv.fu().get_sbits(s);
new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(sbits+ebits));
m_conv.mk_fp(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var),
m_conv.bu().mk_extract(ebits - 1, 0, new_var),
m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var),
new_exp);
}
else
new_exp = m().mk_var(t->get_idx(), s);
result = new_exp;
result_pr = 0;
TRACE("fpa2bv", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;);
return true;
}
template class rewriter_tpl<fpa2bv_rewriter_cfg>;

253
src/ast/fpa/fpa2bv_rewriter.h
View file

@ -20,15 +20,13 @@ Notes:
#ifndef FPA2BV_REWRITER_H_
#define FPA2BV_REWRITER_H_
#include"cooperate.h"
#include"rewriter_def.h"
#include"rewriter.h"
#include"bv_decl_plugin.h"
#include"fpa2bv_converter.h"
#include"fpa2bv_rewriter_params.hpp"
struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
ast_manager & m_manager;
expr_ref_vector m_out;
ast_manager & m_manager;
expr_ref_vector m_out;
fpa2bv_converter & m_conv;
sort_ref_vector m_bindings;
@ -37,19 +35,9 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
ast_manager & m() const { return m_manager; }
fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, params_ref const & p) :
m_manager(m),
m_out(m),
m_conv(c),
m_bindings(m) {
updt_params(p);
// We need to make sure that the mananger has the BV plugin loaded.
symbol s_bv("bv");
if (!m_manager.has_plugin(s_bv))
m_manager.register_plugin(s_bv, alloc(bv_decl_plugin));
}
fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, params_ref const & p);
~fpa2bv_rewriter_cfg() {
~fpa2bv_rewriter_cfg() {
}
void cleanup_buffers() {
@ -59,241 +47,32 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
void reset() {
}
void updt_local_params(params_ref const & _p) {
fpa2bv_rewriter_params p(_p);
bool v = p.hi_fp_unspecified();
m_conv.set_unspecified_fp_hi(v);
}
void updt_local_params(params_ref const & _p);
void updt_params(params_ref const & p) {
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_max_steps = p.get_uint("max_steps", UINT_MAX);
updt_local_params(p);
}
void updt_params(params_ref const & p);
bool max_steps_exceeded(unsigned num_steps) const {
cooperate("fpa2bv");
return num_steps > m_max_steps;
}
bool max_steps_exceeded(unsigned num_steps) const;
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
TRACE("fpa2bv_rw", tout << "APP: " << f->get_name() << std::endl; );
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr);
if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_float(f->get_range())) {
m_conv.mk_const(f, result);
return BR_DONE;
}
bool pre_visit(expr * t);
if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm(f->get_range())) {
m_conv.mk_rm_const(f, result);
return BR_DONE;
}
if (m().is_eq(f)) {
SASSERT(num == 2);
TRACE("fpa2bv_rw", tout << "(= " << mk_ismt2_pp(args[0], m()) << " " <<
mk_ismt2_pp(args[1], m()) << ")" << std::endl;);
SASSERT(m().get_sort(args[0]) == m().get_sort(args[1]));
sort * ds = f->get_domain()[0];
if (m_conv.is_float(ds)) {
m_conv.mk_eq(args[0], args[1], result);
return BR_DONE;
}
else if (m_conv.is_rm(ds)) {
result = m().mk_eq(args[0], args[1]);
return BR_DONE;
}
return BR_FAILED;
}
else if (m().is_ite(f)) {
SASSERT(num == 3);
if (m_conv.is_float(args[1])) {
m_conv.mk_ite(args[0], args[1], args[2], result);
return BR_DONE;
}
return BR_FAILED;
}
else if (m().is_distinct(f)) {
sort * ds = f->get_domain()[0];
if (m_conv.is_float(ds) || m_conv.is_rm(ds)) {
m_conv.mk_distinct(f, num, args, result);
return BR_DONE;
}
return BR_FAILED;
}
if (m_conv.is_float_family(f)) {
switch (f->get_decl_kind()) {
case OP_FPA_RM_NEAREST_TIES_TO_AWAY:
case OP_FPA_RM_NEAREST_TIES_TO_EVEN:
case OP_FPA_RM_TOWARD_NEGATIVE:
case OP_FPA_RM_TOWARD_POSITIVE:
case OP_FPA_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f, result); return BR_DONE;
case OP_FPA_NUM: m_conv.mk_numeral(f, num, args, result); return BR_DONE;
case OP_FPA_PLUS_INF: m_conv.mk_pinf(f, result); return BR_DONE;
case OP_FPA_MINUS_INF: m_conv.mk_ninf(f, result); return BR_DONE;
case OP_FPA_PLUS_ZERO: m_conv.mk_pzero(f, result); return BR_DONE;
case OP_FPA_MINUS_ZERO: m_conv.mk_nzero(f, result); return BR_DONE;
case OP_FPA_NAN: m_conv.mk_nan(f, result); return BR_DONE;
case OP_FPA_ADD: m_conv.mk_add(f, num, args, result); return BR_DONE;
case OP_FPA_SUB: m_conv.mk_sub(f, num, args, result); return BR_DONE;
case OP_FPA_NEG: m_conv.mk_neg(f, num, args, result); return BR_DONE;
case OP_FPA_MUL: m_conv.mk_mul(f, num, args, result); return BR_DONE;
case OP_FPA_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE;
case OP_FPA_REM: m_conv.mk_rem(f, num, args, result); return BR_DONE;
case OP_FPA_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE;
case OP_FPA_FMA: m_conv.mk_fma(f, num, args, result); return BR_DONE;
case OP_FPA_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE;
case OP_FPA_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE;
case OP_FPA_EQ: m_conv.mk_float_eq(f, num, args, result); return BR_DONE;
case OP_FPA_LT: m_conv.mk_float_lt(f, num, args, result); return BR_DONE;
case OP_FPA_GT: m_conv.mk_float_gt(f, num, args, result); return BR_DONE;
case OP_FPA_LE: m_conv.mk_float_le(f, num, args, result); return BR_DONE;
case OP_FPA_GE: m_conv.mk_float_ge(f, num, args, result); return BR_DONE;
case OP_FPA_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE;
case OP_FPA_IS_NAN: m_conv.mk_is_nan(f, num, args, result); return BR_DONE;
case OP_FPA_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE;
case OP_FPA_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE;
case OP_FPA_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE;
case OP_FPA_IS_POSITIVE: m_conv.mk_is_positive(f, num, args, result); return BR_DONE;
case OP_FPA_IS_NEGATIVE: m_conv.mk_is_negative(f, num, args, result); return BR_DONE;
case OP_FPA_TO_FP: m_conv.mk_to_fp(f, num, args, result); return BR_DONE;
case OP_FPA_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE;
case OP_FPA_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE;
case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE;
case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_REWRITE_FULL;
case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_REWRITE_FULL;
case OP_FPA_INTERNAL_MIN_UNSPECIFIED: result = m_conv.mk_min_unspecified(f, args[0], args[1]); return BR_DONE;
case OP_FPA_INTERNAL_MAX_UNSPECIFIED: result = m_conv.mk_max_unspecified(f, args[0], args[1]); return BR_DONE;
case OP_FPA_INTERNAL_MIN_I: m_conv.mk_min_i(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_RM:
case OP_FPA_INTERNAL_BVWRAP:
case OP_FPA_INTERNAL_BVUNWRAP:
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: return BR_FAILED;
default:
TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n";
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);
NOT_IMPLEMENTED_YET();
}
}
else {
SASSERT(!m_conv.is_float_family(f));
bool is_float_uf = m_conv.is_float(f->get_range()) || m_conv.is_rm(f->get_range());
for (unsigned i = 0; i < f->get_arity(); i++) {
sort * di = f->get_domain()[i];
is_float_uf |= m_conv.is_float(di) || m_conv.is_rm(di);
}
if (is_float_uf) {
m_conv.mk_uninterpreted_function(f, num, args, result);
return BR_DONE;
}
}
return BR_FAILED;
}
bool pre_visit(expr * t)
{
TRACE("fpa2bv", tout << "pre_visit: " << mk_ismt2_pp(t, m()) << std::endl;);
if (is_quantifier(t)) {
quantifier * q = to_quantifier(t);
TRACE("fpa2bv", tout << "pre_visit quantifier [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m()) << std::endl;);
sort_ref_vector new_bindings(m_manager);
for (unsigned i = 0 ; i < q->get_num_decls(); i++)
new_bindings.push_back(q->get_decl_sort(i));
SASSERT(new_bindings.size() == q->get_num_decls());
m_bindings.append(new_bindings);
}
return true;
}
bool reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
bool reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr) {
unsigned curr_sz = m_bindings.size();
SASSERT(old_q->get_num_decls() <= curr_sz);
unsigned num_decls = old_q->get_num_decls();
unsigned old_sz = curr_sz - num_decls;
string_buffer<> name_buffer;
ptr_buffer<sort> new_decl_sorts;
sbuffer<symbol> new_decl_names;
for (unsigned i = 0; i < num_decls; i++) {
symbol const & n = old_q->get_decl_name(i);
sort * s = old_q->get_decl_sort(i);
if (m_conv.is_float(s)) {
unsigned ebits = m_conv.fu().get_ebits(s);
unsigned sbits = m_conv.fu().get_sbits(s);
name_buffer.reset();
name_buffer << n << ".bv";
new_decl_names.push_back(symbol(name_buffer.c_str()));
new_decl_sorts.push_back(m_conv.bu().mk_sort(sbits+ebits));
}
else {
new_decl_sorts.push_back(s);
new_decl_names.push_back(n);
}
}
result = m().mk_quantifier(old_q->is_forall(), new_decl_sorts.size(), new_decl_sorts.c_ptr(), new_decl_names.c_ptr(),
new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(),
old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns);
result_pr = 0;
m_bindings.shrink(old_sz);
TRACE("fpa2bv", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " <<
mk_ismt2_pp(old_q->get_expr(), m()) << std::endl <<
" new body: " << mk_ismt2_pp(new_body, m()) << std::endl;
tout << "result = " << mk_ismt2_pp(result, m()) << std::endl;);
return true;
}
proof_ref & result_pr);
bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr) {
if (t->get_idx() >= m_bindings.size())
return false;
// unsigned inx = m_bindings.size() - t->get_idx() - 1;
bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr);
expr_ref new_exp(m());
sort * s = t->get_sort();
if (m_conv.is_float(s))
{
expr_ref new_var(m());
unsigned ebits = m_conv.fu().get_ebits(s);
unsigned sbits = m_conv.fu().get_sbits(s);
new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(sbits+ebits));
m_conv.mk_fp(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var),
m_conv.bu().mk_extract(ebits - 1, 0, new_var),
m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var),
new_exp);
}
else
new_exp = m().mk_var(t->get_idx(), s);
result = new_exp;
result_pr = 0;
TRACE("fpa2bv", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;);
return true;
}
};
template class rewriter_tpl<fpa2bv_rewriter_cfg>;
struct fpa2bv_rewriter : public rewriter_tpl<fpa2bv_rewriter_cfg> {
fpa2bv_rewriter_cfg m_cfg;
fpa2bv_rewriter(ast_manager & m, fpa2bv_converter & c, params_ref const & p):
rewriter_tpl<fpa2bv_rewriter_cfg>(m, m.proofs_enabled(), m_cfg),
rewriter_tpl<fpa2bv_rewriter_cfg>(m, m.proofs_enabled(), m_cfg),
m_cfg(m, c, p) {
}
};

8
src/ast/rewriter/arith_rewriter.cpp
View file

@ -61,8 +61,10 @@ br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
case OP_ADD: st = mk_add_core(num_args, args, result); break;
case OP_MUL: st = mk_mul_core(num_args, args, result); break;
case OP_SUB: st = mk_sub(num_args, args, result); break;
case OP_DIV: SASSERT(num_args == 2); st = mk_div_core(args[0], args[1], result); break;
case OP_IDIV: SASSERT(num_args == 2); st = mk_idiv_core(args[0], args[1], result); break;
case OP_DIV: if (num_args == 1) { result = args[0]; st = BR_DONE; break; }
SASSERT(num_args == 2); st = mk_div_core(args[0], args[1], result); break;
case OP_IDIV: if (num_args == 1) { result = args[0]; st = BR_DONE; break; }
SASSERT(num_args == 2); st = mk_idiv_core(args[0], args[1], result); break;
case OP_MOD: SASSERT(num_args == 2); st = mk_mod_core(args[0], args[1], result); break;
case OP_REM: SASSERT(num_args == 2); st = mk_rem_core(args[0], args[1], result); break;
case OP_UMINUS: SASSERT(num_args == 1); st = mk_uminus(args[0], result); break;
@ -292,7 +294,7 @@ expr * arith_rewriter::reduce_power(expr * arg, bool is_eq) {
for (unsigned i = 0; i < sz; i++) {
expr * arg = args[i];
expr * arg0, *arg1;
if (m_util.is_power(arg, arg0, arg1) && m_util.is_numeral(arg1, k) && k.is_int() &&
if (m_util.is_power(arg, arg0, arg1) && m_util.is_numeral(arg1, k) && k.is_int() &&
((is_eq && k > rational(1)) || (!is_eq && k > rational(2)))) {
if (is_eq || !k.is_even()) {
new_args.push_back(arg0);

74
src/ast/rewriter/bool_rewriter.cpp
View file

@ -572,35 +572,61 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_
*/
br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) {
SASSERT(m().is_ite(ite));
expr* cond, *t, *e;
VERIFY(m().is_ite(ite, cond, t, e));
SASSERT(m().is_value(val));
expr * t = ite->get_arg(1);
expr * e = ite->get_arg(2);
if (!m().is_value(t) || !m().is_value(e))
return BR_FAILED;
if (t != val && e != val) {
TRACE("try_ite_value", tout << mk_ismt2_pp(t, m()) << " " << mk_ismt2_pp(e, m()) << " " << mk_ismt2_pp(val, m()) << "\n";
tout << t << " " << e << " " << val << "\n";);
result = m().mk_false();
if (m().is_value(t) && m().is_value(e)) {
if (t != val && e != val) {
TRACE("try_ite_value", tout << mk_ismt2_pp(t, m()) << " " << mk_ismt2_pp(e, m()) << " " << mk_ismt2_pp(val, m()) << "\n";
tout << t << " " << e << " " << val << "\n";);
result = m().mk_false();
}
else if (t == val && e == val) {
result = m().mk_true();
}
else if (t == val) {
result = cond;
}
else {
SASSERT(e == val);
mk_not(cond, result);
}
return BR_DONE;
}
if (t == val && e == val) {
result = m().mk_true();
return BR_DONE;
if (m().is_value(t)) {
if (val == t) {
result = m().mk_or(cond, m().mk_eq(val, e));
}
else {
mk_not(cond, result);
result = m().mk_and(result, m().mk_eq(val, e));
}
return BR_REWRITE2;
}
if (m().is_value(e)) {
if (val == e) {
mk_not(cond, result);
result = m().mk_or(result, m().mk_eq(val, t));
}
else {
result = m().mk_and(cond, m().mk_eq(val, t));
}
return BR_REWRITE2;
}
expr* cond2, *t2, *e2;
if (m().is_ite(t, cond2, t2, e2) && m().is_value(t2) && m().is_value(e2)) {
try_ite_value(to_app(t), val, result);
result = m().mk_ite(cond, result, m().mk_eq(e, val));
return BR_REWRITE2;
}
if (m().is_ite(e, cond2, t2, e2) && m().is_value(t2) && m().is_value(e2)) {
try_ite_value(to_app(e), val, result);
result = m().mk_ite(cond, m().mk_eq(t, val), result);
return BR_REWRITE2;
}
if (t == val) {
result = ite->get_arg(0);
return BR_DONE;
}
SASSERT(e == val);
mk_not(ite->get_arg(0), result);
return BR_DONE;
return BR_FAILED;
}
#if 0
@ -645,7 +671,7 @@ static bool is_ite_value_tree_neq_value(ast_manager & m, app * ite, app * val) {
#endif
br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
if (lhs == rhs) {
if (m().are_equal(lhs, rhs)) {
result = m().mk_true();
return BR_DONE;
}

2
src/ast/rewriter/rewriter.cpp
View file

@ -51,6 +51,8 @@ void rewriter_core::cache_result(expr * k, expr * v) {
TRACE("rewriter_cache_result", tout << mk_ismt2_pp(k, m()) << "\n--->\n" << mk_ismt2_pp(v, m()) << "\n";);
SASSERT(m().get_sort(k) == m().get_sort(v));
m_cache->insert(k, v);
#if 0
static unsigned num_cached = 0;

7
src/ast/rewriter/rewriter.h
View file

@ -214,10 +214,12 @@ protected:
unsigned m_num_steps;
ptr_vector<expr> m_bindings;
var_shifter m_shifter;
inv_var_shifter m_inv_shifter;
expr_ref m_r;
proof_ref m_pr;
proof_ref m_pr2;
unsigned_vector m_shifts;
svector<frame> & frame_stack() { return this->m_frame_stack; }
svector<frame> const & frame_stack() const { return this->m_frame_stack; }
expr_ref_vector & result_stack() { return this->m_result_stack; }
@ -225,6 +227,8 @@ protected:
proof_ref_vector & result_pr_stack() { return this->m_result_pr_stack; }
proof_ref_vector const & result_pr_stack() const { return this->m_result_pr_stack; }
void display_bindings(std::ostream& out);
void set_new_child_flag(expr * old_t) {
SASSERT(frame_stack().empty() || frame_stack().back().m_state != PROCESS_CHILDREN || this->is_child_of_top_frame(old_t));
if (!frame_stack().empty())
@ -232,7 +236,6 @@ protected:
}
void set_new_child_flag(expr * old_t, expr * new_t) { if (old_t != new_t) set_new_child_flag(old_t); }
// cache the result of shared non atomic expressions.
bool cache_results() const { return m_cfg.cache_results(); }
// cache all results share and non shared expressions non atomic expressions.

98
src/ast/rewriter/rewriter_def.h
View file

@ -24,11 +24,13 @@ template<bool ProofGen>
void rewriter_tpl<Config>::process_var(var * v) {
if (m_cfg.reduce_var(v, m_r, m_pr)) {
result_stack().push_back(m_r);
SASSERT(v->get_sort() == m().get_sort(m_r));
if (ProofGen) {
result_pr_stack().push_back(m_pr);
m_pr = 0;
}
set_new_child_flag(v);
TRACE("rewriter", tout << mk_ismt2_pp(v, m()) << " -> " << m_r << "\n";);
m_r = 0;
return;
}
@ -36,18 +38,22 @@ void rewriter_tpl<Config>::process_var(var * v) {
// bindings are only used when Proof Generation is not enabled.
unsigned idx = v->get_idx();
if (idx < m_bindings.size()) {
expr * r = m_bindings[m_bindings.size() - idx - 1];
TRACE("process_var", if (r) tout << "idx: " << idx << " --> " << mk_ismt2_pp(r, m()) << "\n";
tout << "bindings:\n";
for (unsigned i = 0; i < m_bindings.size(); i++) if (m_bindings[i]) tout << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << "\n";);
unsigned index = m_bindings.size() - idx - 1;
expr * r = m_bindings[index];
if (r != 0) {
if (m_num_qvars == 0 || is_ground(r)) {
result_stack().push_back(r);
SASSERT(v->get_sort() == m().get_sort(r));
if (!is_ground(r) && m_shifts[index] != m_bindings.size()) {
unsigned shift_amount = m_bindings.size() - m_shifts[index];
expr_ref tmp(m());
m_shifter(r, shift_amount, tmp);
result_stack().push_back(tmp);
TRACE("rewriter", tout << "shift: " << shift_amount << " idx: " << idx << " --> " << tmp << "\n";
display_bindings(tout););
}
else {
expr_ref new_term(m());
m_shifter(r, m_num_qvars, new_term);
result_stack().push_back(new_term);
result_stack().push_back(r);
TRACE("rewriter", tout << idx << " " << mk_ismt2_pp(r, m()) << "\n";);
}
set_new_child_flag(v);
return;
@ -64,6 +70,7 @@ template<bool ProofGen>
void rewriter_tpl<Config>::process_const(app * t) {
SASSERT(t->get_num_args() == 0);
br_status st = m_cfg.reduce_app(t->get_decl(), 0, 0, m_r, m_pr);
SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t));
SASSERT(st == BR_FAILED || st == BR_DONE);
if (st == BR_DONE) {
result_stack().push_back(m_r.get());
@ -100,6 +107,7 @@ bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
proof * new_t_pr;
if (m_cfg.get_subst(t, new_t, new_t_pr)) {
TRACE("rewriter_subst", tout << "subst\n" << mk_ismt2_pp(t, m()) << "\n---->\n" << mk_ismt2_pp(new_t, m()) << "\n";);
SASSERT(m().get_sort(t) == m().get_sort(new_t));
result_stack().push_back(new_t);
set_new_child_flag(t, new_t);
if (ProofGen)
@ -124,6 +132,7 @@ bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
#endif
expr * r = get_cached(t);
if (r) {
SASSERT(m().get_sort(r) == m().get_sort(t));
result_stack().push_back(r);
set_new_child_flag(t, r);
if (ProofGen) {
@ -213,6 +222,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
}
}
br_status st = m_cfg.reduce_app(f, new_num_args, new_args, m_r, m_pr2);
SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t));
TRACE("reduce_app",
tout << mk_ismt2_pp(t, m()) << "\n";
tout << "st: " << st;
@ -220,6 +230,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
tout << "\n";);
if (st != BR_FAILED) {
result_stack().shrink(fr.m_spos);
SASSERT(m().get_sort(m_r) == m().get_sort(t));
result_stack().push_back(m_r);
if (ProofGen) {
result_pr_stack().shrink(fr.m_spos);
@ -295,6 +306,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
if (get_macro(f, def, def_q, def_pr)) {
SASSERT(!f->is_associative() || !flat_assoc(f));
SASSERT(new_num_args == t->get_num_args());
SASSERT(m().get_sort(def) == m().get_sort(t));
if (is_ground(def)) {
m_r = def;
if (ProofGen) {
@ -317,16 +329,18 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
TRACE("get_macro", tout << "f: " << f->get_name() << ", def: \n" << mk_ismt2_pp(def, m()) << "\n";
tout << "Args num: " << num_args << "\n";
for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(new_args[i], m()) << "\n";);
unsigned sz = m_bindings.size();
unsigned i = num_args;
while (i > 0) {
--i;
m_bindings.push_back(new_args[i]);
m_bindings.push_back(new_args[i]); // num_args - i - 1]);
m_shifts.push_back(sz);
}
result_stack().push_back(def);
TRACE("get_macro", tout << "bindings:\n";
for (unsigned j = 0; j < m_bindings.size(); j++) tout << j << ": " << mk_ismt2_pp(m_bindings[j], m()) << "\n";);
TRACE("get_macro", display_bindings(tout););
begin_scope();
m_num_qvars = 0;
m_num_qvars += num_args;
//m_num_qvars = 0;
m_root = def;
push_frame(def, false, RW_UNBOUNDED_DEPTH);
return;
@ -383,9 +397,17 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
SASSERT(fr.m_spos + t->get_num_args() + 2 == result_stack().size());
SASSERT(t->get_num_args() <= m_bindings.size());
if (!ProofGen) {
m_bindings.shrink(m_bindings.size() - t->get_num_args());
expr_ref tmp(m());
unsigned num_args = t->get_num_args();
m_bindings.shrink(m_bindings.size() - num_args);
m_shifts.shrink(m_shifts.size() - num_args);
m_num_qvars -= num_args;
end_scope();
m_r = result_stack().back();
if (!is_ground(m_r)) {
m_inv_shifter(m_r, num_args, tmp);
m_r = tmp;
}
result_stack().shrink(fr.m_spos);
result_stack().push_back(m_r);
cache_result<ProofGen>(t, m_r, m_pr, fr.m_cache_result);
@ -411,23 +433,26 @@ template<typename Config>
template<bool ProofGen>
void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
SASSERT(fr.m_state == PROCESS_CHILDREN);
unsigned num_decls = q->get_num_decls();
if (fr.m_i == 0) {
if (!ProofGen) {
begin_scope();
m_root = q->get_expr();
}
m_num_qvars += q->get_num_decls();
if (!ProofGen) {
for (unsigned i = 0; i < q->get_num_decls(); i++)
unsigned sz = m_bindings.size();
for (unsigned i = 0; i < num_decls; i++) {
m_bindings.push_back(0);
m_shifts.push_back(sz);
}
}
m_num_qvars += num_decls;
}
unsigned num_children = rewrite_patterns() ? q->get_num_children() : 1;
while (fr.m_i < num_children) {
expr * child = q->get_child(fr.m_i);
fr.m_i++;
if (!visit<ProofGen>(child, fr.m_max_depth))
if (!visit<ProofGen>(child, fr.m_max_depth)) {
return;
}
}
SASSERT(fr.m_spos + num_children == result_stack().size());
expr * const * it = result_stack().c_ptr() + fr.m_spos;
@ -456,6 +481,8 @@ void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
result_pr_stack().push_back(m_pr);
}
else {
expr_ref tmp(m());
if (!m_cfg.reduce_quantifier(q, new_body, new_pats, new_no_pats, m_r, m_pr)) {
if (fr.m_new_child) {
m_r = m().update_quantifier(q, q->get_num_patterns(), new_pats, q->get_num_no_patterns(), new_no_pats, new_body);
@ -468,9 +495,11 @@ void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
}
result_stack().shrink(fr.m_spos);
result_stack().push_back(m_r.get());
SASSERT(m().is_bool(m_r));
if (!ProofGen) {
SASSERT(q->get_num_decls() <= m_bindings.size());
m_bindings.shrink(m_bindings.size() - q->get_num_decls());
SASSERT(num_decls <= m_bindings.size());
m_bindings.shrink(m_bindings.size() - num_decls);
m_shifts.shrink(m_shifts.size() - num_decls);
end_scope();
cache_result<ProofGen>(q, m_r, m_pr, fr.m_cache_result);
}
@ -496,6 +525,7 @@ rewriter_tpl<Config>::rewriter_tpl(ast_manager & m, bool proof_gen, Config & cfg
m_cfg(cfg),
m_num_steps(0),
m_shifter(m),
m_inv_shifter(m),
m_r(m),
m_pr(m),
m_pr2(m) {
@ -510,7 +540,9 @@ void rewriter_tpl<Config>::reset() {
m_cfg.reset();
rewriter_core::reset();
m_bindings.reset();
m_shifts.reset();
m_shifter.reset();
m_inv_shifter.reset();
}
template<typename Config>
@ -519,6 +551,17 @@ void rewriter_tpl<Config>::cleanup() {
rewriter_core::cleanup();
m_bindings.finalize();
m_shifter.cleanup();
m_shifts.finalize();
m_inv_shifter.cleanup();
}
template<typename Config>
void rewriter_tpl<Config>::display_bindings(std::ostream& out) {
out << "bindings:\n";
for (unsigned i = 0; i < m_bindings.size(); i++) {
if (m_bindings[i])
out << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << "\n";
}
}
template<typename Config>
@ -526,11 +569,14 @@ void rewriter_tpl<Config>::set_bindings(unsigned num_bindings, expr * const * bi
SASSERT(!m_proof_gen);
SASSERT(not_rewriting());
m_bindings.reset();
m_shifts.reset();
unsigned i = num_bindings;
while (i > 0) {
--i;
m_bindings.push_back(bindings[i]);
m_shifts.push_back(num_bindings);
}
TRACE("rewriter", display_bindings(tout););
}
template<typename Config>
@ -538,9 +584,12 @@ void rewriter_tpl<Config>::set_inv_bindings(unsigned num_bindings, expr * const
SASSERT(!m_proof_gen);
SASSERT(not_rewriting());
m_bindings.reset();
m_shifts.reset();
for (unsigned i = 0; i < num_bindings; i++) {
m_bindings.push_back(bindings[i]);
m_shifts.push_back(num_bindings);
}
TRACE("rewriter", display_bindings(tout););
}
template<typename Config>
@ -562,9 +611,11 @@ void rewriter_tpl<Config>::main_loop(expr * t, expr_ref & result, proof_ref & re
result_pr = m().mk_reflexivity(t);
SASSERT(result_pr_stack().empty());
}
return;
}
resume_core<ProofGen>(result, result_pr);
else {
resume_core<ProofGen>(result, result_pr);
}
TRACE("rewriter", tout << mk_ismt2_pp(t, m()) << "\n=>\n" << result << "\n";;);
}
/**
@ -587,6 +638,7 @@ void rewriter_tpl<Config>::resume_core(expr_ref & result, proof_ref & result_pr)
if (first_visit(fr) && fr.m_cache_result) {
expr * r = get_cached(t);
if (r) {
SASSERT(m().get_sort(r) == m().get_sort(t));
result_stack().push_back(r);
if (ProofGen) {
proof * pr = get_cached_pr(t);

2
src/ast/rewriter/seq_rewriter.cpp
View file

@ -579,7 +579,7 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
unsigned lenA = 0, lenB = 0;
bool lA = min_length(as.size(), as.c_ptr(), lenA);
if (lA) {
bool lB = min_length(bs.size(), bs.c_ptr(), lenB);
min_length(bs.size(), bs.c_ptr(), lenB);
if (lenB > lenA) {
result = m().mk_false();
return BR_DONE;

0
src/interp/iz3params.pyg → src/interp/interp_params.pyg
View file

0
src/math/polynomial/algebraic.pyg → src/math/polynomial/algebraic_params.pyg
View file

0
src/math/realclosure/rcf.pyg → src/math/realclosure/rcf_params.pyg
View file

1
src/model/model_core.cpp
View file

@ -29,7 +29,6 @@ model_core::~model_core() {
decl2finterp::iterator it2 = m_finterp.begin();
decl2finterp::iterator end2 = m_finterp.end();
for (; it2 != end2; ++it2) {
func_decl* d = it2->m_key;
m_manager.dec_ref(it2->m_key);
dealloc(it2->m_value);
}

15
src/model/model_evaluator.cpp
View file

@ -31,8 +31,9 @@ Revision History:
#include"rewriter_def.h"
#include"cooperate.h"
struct evaluator_cfg : public default_rewriter_cfg {
model_core & m_model;
model_core & m_model;
bool_rewriter m_b_rw;
arith_rewriter m_a_rw;
bv_rewriter m_bv_rw;
@ -59,9 +60,10 @@ struct evaluator_cfg : public default_rewriter_cfg {
m_pb_rw(m),
m_f_rw(m),
m_seq_rw(m) {
m_b_rw.set_flat(false);
m_a_rw.set_flat(false);
m_bv_rw.set_flat(false);
bool flat = true;
m_b_rw.set_flat(flat);
m_a_rw.set_flat(flat);
m_bv_rw.set_flat(flat);
m_bv_rw.set_mkbv2num(true);
updt_params(p);
}
@ -181,10 +183,12 @@ struct evaluator_cfg : public default_rewriter_cfg {
}
bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) {
TRACE("model_evaluator", tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ")\n";);
#define TRACE_MACRO TRACE("model_evaluator", tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ")\n";);
func_interp * fi = m_model.get_func_interp(f);
if (fi != 0) {
TRACE_MACRO;
if (fi->is_partial()) {
if (m_model_completion) {
sort * s = f->get_range();
@ -204,6 +208,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
(f->get_family_id() == null_family_id ||
m().get_plugin(f->get_family_id())->is_considered_uninterpreted(f)))
{
TRACE_MACRO;
sort * s = f->get_range();
expr * val = m_model.get_some_value(s);
func_interp * new_fi = alloc(func_interp, m(), f->get_arity());

1
src/model/model_params.pyg
View file

@ -4,5 +4,6 @@ def_module_params('model',
('v1', BOOL, False, 'use Z3 version 1.x pretty printer'),
('v2', BOOL, False, 'use Z3 version 2.x (x <= 16) pretty printer'),
('compact', BOOL, False, 'try to compact function graph (i.e., function interpretations that are lookup tables)'),
('new_eval', BOOL, True, 'use new evaluator (temporary parameter for testing)'),
))

36
src/smt/arith_eq_adapter.cpp
View file

@ -152,40 +152,7 @@ namespace smt {
// 5) theory_arith fails to internalize (+ (* -1 x) (* -1 x)), and Z3 crashes.
//
#if 0
// This block of code uses the simplifier for creating the literals t1 >= t2 and t1 <= t2.
// It has serious performance problems in VCC benchmarks.
// The problem seems to be the following:
// t1 and t2 are slacks (i.e., names for linear polynomials).
// The simplifier will create inequalities that will indirectly imply that t1 >= t2 and t1 <= t2.
// Example if: t1 := 1 + a
// t2 := 2 + b
// the simplifier will create
// a - b >= -1
// a - b <= -1
// These inequalities imply that 1+a >= 2+b and 1+a <= 2+b,
// but the tableau is complete different.
// BTW, note that we don't really need to handle the is_numeral case when using
// the simplifier. However, doing that, it seems we minimize the performance problem.
expr_ref le(m);
expr_ref ge(m);
if (m_util.is_numeral(t1))
std::swap(t1, t2);
if (m_util.is_numeral(t2)) {
le = m_util.mk_le(t1, t2);
ge = m_util.mk_ge(t1, t2);
}
else {
arith_simplifier_plugin & s = *(get_simplifier());
s.mk_le(t1, t2, le);
s.mk_ge(t1, t2, ge);
}
TRACE("arith_eq_adapter_perf", tout << mk_ismt2_pp(t1_eq_t2, m) << "\n" << mk_ismt2_pp(le, m) << "\n" << mk_ismt2_pp(ge, m) << "\n";);
#else
// Old version that used to be buggy.
// I fixed the theory arithmetic internalizer to accept non simplified terms of the form t1 - t2
// Requires that the theory arithmetic internalizer accept non simplified terms of the form t1 - t2
// if t1 and t2 already have slacks (theory variables) associated with them.
// It also accepts terms with repeated variables (Issue #429).
app * le = 0;
@ -207,7 +174,6 @@ namespace smt {
}
TRACE("arith_eq_adapter_perf",
tout << mk_ismt2_pp(t1_eq_t2, m) << "\n" << mk_ismt2_pp(le, m) << "\n" << mk_ismt2_pp(ge, m) << "\n";);
#endif
ctx.push_trail(already_processed_trail(m_already_processed, n1, n2));
m_already_processed.insert(n1, n2, data(t1_eq_t2, le, ge));

3
src/smt/arith_eq_adapter.h
View file

@ -65,7 +65,6 @@ namespace smt {
theory & m_owner;
theory_arith_params & m_params;
arith_util & m_util;
arith_simplifier_plugin * m_as;
already_processed m_already_processed;
enode_pair_vector m_restart_pairs;
@ -76,7 +75,7 @@ namespace smt {
enode * get_enode(theory_var v) const { return m_owner.get_enode(v); }
public:
arith_eq_adapter(theory & owner, theory_arith_params & params, arith_util & u):m_owner(owner), m_params(params), m_util(u), m_as(0) {}
arith_eq_adapter(theory & owner, theory_arith_params & params, arith_util & u):m_owner(owner), m_params(params), m_util(u) {}
void new_eq_eh(theory_var v1, theory_var v2);
void new_diseq_eh(theory_var v1, theory_var v2);
void reset_eh();

17
src/smt/proto_model/proto_model.cpp
View file

@ -30,12 +30,14 @@ Revision History:
proto_model::proto_model(ast_manager & m, simplifier & s, params_ref const & p):
model_core(m),
m_simplifier(s),
m_afid(m.mk_family_id(symbol("array"))) {
m_afid(m.mk_family_id(symbol("array"))),
m_eval(*this) {
register_factory(alloc(basic_factory, m));
m_user_sort_factory = alloc(user_sort_factory, m);
register_factory(m_user_sort_factory);
m_model_partial = model_params(p).partial();
m_use_new_eval = model_params(p).new_eval();
}
@ -157,6 +159,19 @@ bool proto_model::is_select_of_model_value(expr* e) const {
So, if model_completion == true, the evaluator never fails if it doesn't contain quantifiers.
*/
bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
if (m_use_new_eval) {
m_eval.set_model_completion(model_completion);
try {
m_eval(e, result);
return true;
}
catch (model_evaluator_exception & ex) {
(void)ex;
TRACE("model_evaluator", tout << ex.msg() << "\n";);
return false;
}
}
bool is_ok = true;
SASSERT(is_well_sorted(m_manager, e));
TRACE("model_eval", tout << mk_pp(e, m_manager) << "\n";

3
src/smt/proto_model/proto_model.h
View file

@ -29,6 +29,7 @@ Revision History:
#define PROTO_MODEL_H_
#include"model_core.h"
#include"model_evaluator.h"
#include"value_factory.h"
#include"plugin_manager.h"
#include"simplifier.h"
@ -44,8 +45,10 @@ class proto_model : public model_core {
family_id m_afid; //!< array family id: hack for displaying models in V1.x style
func_decl_set m_aux_decls;
ptr_vector<expr> m_tmp;
model_evaluator m_eval;
bool m_model_partial;
bool m_use_new_eval;
expr * mk_some_interp_for(func_decl * d);

16
src/smt/smt_model_checker.cpp
View file

@ -95,7 +95,8 @@ namespace smt {
expr * e = *it;
eqs.push_back(m.mk_eq(sk, e));
}
m_aux_context->assert_expr(m.mk_or(eqs.size(), eqs.c_ptr()));
expr_ref fml(m.mk_or(eqs.size(), eqs.c_ptr()), m);
m_aux_context->assert_expr(fml);
}
#define PP_DEPTH 8
@ -105,9 +106,13 @@ namespace smt {
The variables are replaced by skolem constants. These constants are stored in sks.
*/
void model_checker::assert_neg_q_m(quantifier * q, expr_ref_vector & sks) {
expr_ref tmp(m);
m_curr_model->eval(q->get_expr(), tmp, true);
if (!m_curr_model->eval(q->get_expr(), tmp, true)) {
return;
}
//std::cout << tmp << "\n";
TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m) << "\n";);
ptr_buffer<expr> subst_args;
unsigned num_decls = q->get_num_decls();
@ -261,10 +266,11 @@ namespace smt {
lbool r = m_aux_context->check();
TRACE("model_checker", tout << "[complete] model-checker result: " << to_sat_str(r) << "\n";);
if (r == l_false) {
if (r != l_true) {
m_aux_context->pop(1);
return true; // quantifier is satisfied by m_curr_model
return r == l_false; // quantifier is satisfied by m_curr_model
}
model_ref complete_cex;
m_aux_context->get_model(complete_cex);
@ -276,7 +282,7 @@ namespace smt {
while (true) {
lbool r = m_aux_context->check();
TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";);
if (r == l_false)
if (r != l_true)
break;
model_ref cex;
m_aux_context->get_model(cex);

2
src/smt/theory_arith_core.h
View file

@ -1619,6 +1619,7 @@ namespace smt {
m_found_underspecified_op(false),
m_arith_eq_adapter(*this, params, m_util),
m_asserted_qhead(0),
m_row_vars_top(0),
m_to_patch(1024),
m_blands_rule(false),
m_random(params.m_arith_random_seed),
@ -1631,7 +1632,6 @@ namespace smt {
m_liberal_final_check(true),
m_changed_assignment(false),
m_assume_eq_head(0),
m_row_vars_top(0),
m_nl_rounds(0),
m_nl_gb_exhausted(false),
m_nl_new_exprs(m),

1
src/smt/theory_seq.cpp
View file

@ -1591,7 +1591,6 @@ bool theory_seq::solve_ne(unsigned idx) {
}
bool theory_seq::solve_nc(unsigned idx) {
context& ctx = get_context();
nc const& n = m_ncs[idx];
dependency* deps = n.deps();

3
src/tactic/bv/bvarray2uf_rewriter.cpp
View file

@ -24,6 +24,7 @@ Notes:
#include"params.h"
#include"ast_pp.h"
#include"bvarray2uf_rewriter.h"
#include"rewriter_def.h"
// [1] C. M. Wintersteiger, Y. Hamadi, and L. de Moura: Efficiently Solving
// Quantified Bit-Vector Formulas, in Formal Methods in System Design,
@ -345,3 +346,5 @@ bool bvarray2uf_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref &
NOT_IMPLEMENTED_YET();
return true;
}
template class rewriter_tpl<bvarray2uf_rewriter_cfg>;

3
src/tactic/bv/bvarray2uf_rewriter.h
View file

@ -20,7 +20,7 @@ Notes:
#ifndef BVARRAY2UF_REWRITER_H_
#define BVARRAY2UF_REWRITER_H_
#include"rewriter_def.h"
#include"rewriter.h"
#include"extension_model_converter.h"
#include"filter_model_converter.h"
@ -71,7 +71,6 @@ protected:
func_decl_ref mk_uf_for_array(expr * e);
};
template class rewriter_tpl<bvarray2uf_rewriter_cfg>;
struct bvarray2uf_rewriter : public rewriter_tpl<bvarray2uf_rewriter_cfg> {
bvarray2uf_rewriter_cfg m_cfg;

9
src/tactic/fpa/fpa2bv_tactic.cpp
View file

@ -91,11 +91,10 @@ class fpa2bv_tactic : public tactic {
// that is (= e (fp #b0 #b1...1 #b0...01)), so that the value propagation
// has a value to propagate.
expr * sgn, *sig, *exp;
expr_ref top_exp(m);
m_conv.split_fp(new_curr, sgn, exp, sig);
m.mk_eq(sgn, m_conv.bu().mk_numeral(0, 1));
m.mk_eq(exp, m_conv.bu().mk_numeral(-1, m_conv.bu().get_bv_size(exp)));
m.mk_eq(sig, m_conv.bu().mk_numeral(1, m_conv.bu().get_bv_size(sig)));
result.back()->assert_expr(m.mk_eq(sgn, m_conv.bu().mk_numeral(0, 1)));
result.back()->assert_expr(m.mk_eq(exp, m_conv.bu().mk_numeral(-1, m_conv.bu().get_bv_size(exp))));
result.back()->assert_expr(m.mk_eq(sig, m_conv.bu().mk_numeral(1, m_conv.bu().get_bv_size(sig))));
}
}
}
@ -155,7 +154,7 @@ public:
virtual void cleanup() {
imp * d = alloc(imp, m_imp->m, m_params);
std::swap(d, m_imp);
std::swap(d, m_imp);
dealloc(d);
}

1
src/test/main.cpp
View file

@ -226,6 +226,7 @@ int main(int argc, char ** argv) {
TST(sat_user_scope);
TST(pdr);
TST_ARGV(ddnf);
TST(model_evaluator);
//TST_ARGV(hs);
}

66
src/test/model_evaluator.cpp Normal file
View file

@ -0,0 +1,66 @@
#include "model.h"
#include "model_evaluator.h"
#include "model_pp.h"
#include "arith_decl_plugin.h"
#include "reg_decl_plugins.h"
#include "ast_pp.h"
void tst_model_evaluator() {
ast_manager m;
reg_decl_plugins(m);
arith_util a(m);
model mdl(m);
sort* sI = a.mk_int();
sort* dom[2] = { sI, m.mk_bool_sort() };
func_decl_ref f(m.mk_func_decl(symbol("f"), 2, dom, sI), m);
func_decl_ref g(m.mk_func_decl(symbol("g"), 2, dom, sI), m);
func_decl_ref h(m.mk_func_decl(symbol("h"), 2, dom, sI), m);
func_decl_ref F(m.mk_func_decl(symbol("F"), 2, dom, sI), m);
func_decl_ref G(m.mk_func_decl(symbol("G"), 2, dom, sI), m);
expr_ref vI0(m.mk_var(0, sI), m);
expr_ref vI1(m.mk_var(1, sI), m);
expr_ref vB0(m.mk_var(0, m.mk_bool_sort()), m);
expr_ref vB1(m.mk_var(1, m.mk_bool_sort()), m);
expr_ref vB2(m.mk_var(2, m.mk_bool_sort()), m);
expr_ref f01(m.mk_app(f, vI0, vB1), m);
expr_ref g01(m.mk_app(g, vI0, vB1), m);
expr_ref h01(m.mk_app(h, vI0, vB1), m);
func_interp* fi = alloc(func_interp, m, 2);
func_interp* gi = alloc(func_interp, m, 2);
func_interp* hi = alloc(func_interp, m, 2);
hi->set_else(m.mk_ite(vB1, m.mk_app(f, vI0, vB1), m.mk_app(g, vI0, vB1)));
mdl.register_decl(h, hi);
model_evaluator eval(mdl);
expr_ref e(m), v(m);
{
symbol nI("N");
fi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0, m.mk_app(F, vI1, vB2))), vI0, a.mk_int(1)));
gi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0, m.mk_app(G, vI1, vB2))), a.mk_int(2), vI0));
mdl.register_decl(g, gi);
mdl.register_decl(f, fi);
model_pp(std::cout, mdl);
e = m.mk_app(h, vI0, vB1);
eval(e, v);
std::cout << e << " " << v << "\n";
}
{
fi->set_else(m.mk_app(F, vI0, vB1));
gi->set_else(m.mk_app(G, vI0, vB1));
mdl.register_decl(g, gi);
mdl.register_decl(h, hi);
model_pp(std::cout, mdl);
e = m.mk_app(h, vI0, vB1);
eval(e, v);
std::cout << e << " " << v << "\n";
}
}

5
src/util/version.h.in Normal file
View file

@ -0,0 +1,5 @@
// automatically generated file.
#define Z3_MAJOR_VERSION @Z3_VERSION_MAJOR@
#define Z3_MINOR_VERSION @Z3_VERSION_MINOR@
#define Z3_BUILD_NUMBER @Z3_VERSION_PATCH@
#define Z3_REVISION_NUMBER @Z3_VERSION_TWEAK@