mirror of
https://github.com/Z3Prover/z3
synced 2025-08-10 21:20:52 +00:00
Removed trailing whitespace.
This commit is contained in:
Christoph M. Wintersteiger
parent
64fa2db3ff
commit
8fffa9f188
4 changed files with 137 additions and 136 deletions
|
|
@ -29,7 +29,7 @@ namespace smt {
|
|||
obj_map<expr, expr*> & m_conversions;
|
||||
expr * m_e;
|
||||
public:
|
||||
fpa2bv_conversion_trail_elem(ast_manager & m, obj_map<expr, expr*> & c, expr * e) :
|
||||
fpa2bv_conversion_trail_elem(ast_manager & m, obj_map<expr, expr*> & c, expr * e) :
|
||||
m(m), m_conversions(c), m_e(e) {}
|
||||
virtual ~fpa2bv_conversion_trail_elem() {}
|
||||
virtual void undo(theory_fpa & th) {
|
||||
|
|
@ -63,7 +63,7 @@ namespace smt {
|
|||
m.inc_ref(f);
|
||||
m.inc_ref(result);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void theory_fpa::fpa2bv_converter_wrapped::mk_rm_const(func_decl * f, expr_ref & result) {
|
||||
SASSERT(f->get_family_id() == null_family_id);
|
||||
|
|
@ -89,12 +89,12 @@ namespace smt {
|
|||
}
|
||||
|
||||
expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_min_unspecified(func_decl * f, expr * x, expr * y) {
|
||||
// The only cases in which min is unspecified for is when the arguments are +0.0 and -0.0.
|
||||
// The only cases in which min is unspecified for is when the arguments are +0.0 and -0.0.
|
||||
unsigned ebits = m_util.get_ebits(f->get_range());
|
||||
unsigned sbits = m_util.get_sbits(f->get_range());
|
||||
unsigned bv_sz = ebits + sbits;
|
||||
expr_ref res(m);
|
||||
|
||||
|
||||
expr * args[] = { x, y };
|
||||
func_decl * w = m.mk_func_decl(m_th.get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, 0, 0, 2, args, f->get_range());
|
||||
expr_ref a(m), wrapped(m);
|
||||
|
|
@ -110,7 +110,7 @@ namespace smt {
|
|||
m_extra_assertions.push_back(sc);
|
||||
return res;
|
||||
}
|
||||
|
||||
|
||||
expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_max_unspecified(func_decl * f, expr * x, expr * y) {
|
||||
// The only cases in which max is unspecified for is when the arguments are +0.0 and -0.0.
|
||||
unsigned ebits = m_util.get_ebits(f->get_range());
|
||||
|
|
@ -118,7 +118,7 @@ namespace smt {
|
|||
unsigned bv_sz = ebits + sbits;
|
||||
expr_ref res(m);
|
||||
|
||||
expr * args[] = { x, y };
|
||||
expr * args[] = { x, y };
|
||||
func_decl * w = m.mk_func_decl(m_th.get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, 0, 0, 2, args, f->get_range());
|
||||
expr_ref a(m), wrapped(m);
|
||||
a = m.mk_app(w, x, y);
|
||||
|
|
@ -154,15 +154,15 @@ namespace smt {
|
|||
ast_manager & m = get_manager();
|
||||
dec_ref_map_values(m, m_conversions);
|
||||
dec_ref_map_values(m, m_wraps);
|
||||
dec_ref_map_values(m, m_unwraps);
|
||||
dec_ref_map_values(m, m_unwraps);
|
||||
}
|
||||
|
||||
app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
|
||||
ast_manager & m = m_th.get_manager();
|
||||
ast_manager & m = m_th.get_manager();
|
||||
|
||||
TRACE("t_fpa_detail", for (unsigned i = 0; i < values.size(); i++)
|
||||
tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;);
|
||||
|
||||
|
||||
mpf_manager & mpfm = m_fu.fm();
|
||||
unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
|
||||
app * result;
|
||||
|
|
@ -195,7 +195,7 @@ namespace smt {
|
|||
|
||||
mpzm.set(sig_z, all_z);
|
||||
}
|
||||
else if (values.size() == 3) {
|
||||
else if (values.size() == 3) {
|
||||
rational sgn_r(0), exp_r(0), sig_r(0);
|
||||
|
||||
bool r = m_bu.is_numeral(values[0], sgn_r, bv_sz);
|
||||
|
|
@ -204,7 +204,7 @@ namespace smt {
|
|||
SASSERT(r && bv_sz == m_ebits);
|
||||
r = m_bu.is_numeral(values[2], sig_r, bv_sz);
|
||||
SASSERT(r && bv_sz == m_sbits - 1);
|
||||
|
||||
|
||||
SASSERT(mpzm.is_one(sgn_r.to_mpq().denominator()));
|
||||
SASSERT(mpzm.is_one(exp_r.to_mpq().denominator()));
|
||||
SASSERT(mpzm.is_one(sig_r.to_mpq().denominator()));
|
||||
|
|
@ -228,25 +228,25 @@ namespace smt {
|
|||
mpzm.to_string(exp_z) << "," <<
|
||||
mpzm.to_string(sig_z) << "] --> " <<
|
||||
mk_ismt2_pp(result, m_th.get_manager()) << "\n";);
|
||||
|
||||
|
||||
return result;
|
||||
}
|
||||
|
||||
app * theory_fpa::fpa_rm_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
|
||||
SASSERT(values.size() == 1);
|
||||
ast_manager & m = m_th.get_manager();
|
||||
|
||||
|
||||
TRACE("t_fpa_detail", for (unsigned i = 0; i < values.size(); i++)
|
||||
tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;);
|
||||
|
||||
app * result = 0;
|
||||
app * result = 0;
|
||||
unsigned bv_sz;
|
||||
|
||||
rational val(0);
|
||||
bool r = m_bu.is_numeral(values[0], val, bv_sz);
|
||||
SASSERT(r);
|
||||
SASSERT(bv_sz == 3);
|
||||
|
||||
|
||||
switch (val.get_uint64())
|
||||
{
|
||||
case BV_RM_TIES_TO_AWAY: result = m_fu.mk_round_nearest_ties_to_away(); break;
|
||||
|
|
@ -257,7 +257,7 @@ namespace smt {
|
|||
default: result = m_fu.mk_round_toward_zero();
|
||||
}
|
||||
|
||||
TRACE("t_fpa", tout << "fpa_rm_value_proc::mk_value result: " <<
|
||||
TRACE("t_fpa", tout << "fpa_rm_value_proc::mk_value result: " <<
|
||||
mk_ismt2_pp(result, m_th.get_manager()) << "\n";);
|
||||
|
||||
return result;
|
||||
|
|
@ -272,7 +272,7 @@ namespace smt {
|
|||
|
||||
if (!m_wraps.find(e_srt, w)) {
|
||||
SASSERT(!m_wraps.contains(e_srt));
|
||||
|
||||
|
||||
sort * bv_srt;
|
||||
if (m_converter.is_rm(e_srt))
|
||||
bv_srt = m_bv_util.mk_sort(3);
|
||||
|
|
@ -280,9 +280,9 @@ namespace smt {
|
|||
SASSERT(m_converter.is_float(e_srt));
|
||||
unsigned ebits = m_fpa_util.get_ebits(e_srt);
|
||||
unsigned sbits = m_fpa_util.get_sbits(e_srt);
|
||||
bv_srt = m_bv_util.mk_sort(ebits + sbits);
|
||||
bv_srt = m_bv_util.mk_sort(ebits + sbits);
|
||||
}
|
||||
|
||||
|
||||
w = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVWRAP, 0, 0, 1, &e_srt, bv_srt);
|
||||
m_wraps.insert(e_srt, w);
|
||||
m.inc_ref(w);
|
||||
|
|
@ -295,7 +295,7 @@ namespace smt {
|
|||
|
||||
app_ref theory_fpa::unwrap(expr * e, sort * s) {
|
||||
SASSERT(!m_fpa_util.is_unwrap(e));
|
||||
ast_manager & m = get_manager();
|
||||
ast_manager & m = get_manager();
|
||||
sort * bv_srt = m.get_sort(e);
|
||||
|
||||
func_decl *u;
|
||||
|
|
@ -311,7 +311,7 @@ namespace smt {
|
|||
res = m.mk_app(u, e);
|
||||
return res;
|
||||
}
|
||||
|
||||
|
||||
expr_ref theory_fpa::convert_atom(expr * e) {
|
||||
ast_manager & m = get_manager();
|
||||
TRACE("t_fpa_detail", tout << "converting atom: " << mk_ismt2_pp(e, get_manager()) << "\n";);
|
||||
|
|
@ -320,7 +320,7 @@ namespace smt {
|
|||
m_rw(e, res);
|
||||
m_th_rw(res, res);
|
||||
SASSERT(is_app(res));
|
||||
SASSERT(m.is_bool(res));
|
||||
SASSERT(m.is_bool(res));
|
||||
return res;
|
||||
}
|
||||
|
||||
|
|
@ -331,12 +331,12 @@ namespace smt {
|
|||
expr_ref e_conv(m), res(m);
|
||||
proof_ref pr(m);
|
||||
m_rw(e, e_conv);
|
||||
|
||||
if (is_app(e_conv) && to_app(e_conv)->get_family_id() != get_family_id()) {
|
||||
|
||||
if (is_app(e_conv) && to_app(e_conv)->get_family_id() != get_family_id()) {
|
||||
if (!m_fpa_util.is_float(e_conv))
|
||||
m_th_rw(e_conv, res);
|
||||
else {
|
||||
expr_ref bv(m);
|
||||
expr_ref bv(m);
|
||||
bv = wrap(e_conv);
|
||||
unsigned bv_sz = m_bv_util.get_bv_size(bv);
|
||||
unsigned ebits = m_fpa_util.get_ebits(m.get_sort(e_conv));
|
||||
|
|
@ -365,7 +365,7 @@ namespace smt {
|
|||
m_converter.mk_fp(sgn, exp, sig, res);
|
||||
}
|
||||
else
|
||||
UNREACHABLE();
|
||||
UNREACHABLE();
|
||||
|
||||
SASSERT(res.get() != 0);
|
||||
return res;
|
||||
|
|
@ -426,7 +426,7 @@ namespace smt {
|
|||
|
||||
expr_ref theory_fpa::convert_conversion_term(expr * e) {
|
||||
/* This is for the conversion functions fp.to_* */
|
||||
ast_manager & m = get_manager();
|
||||
ast_manager & m = get_manager();
|
||||
expr_ref res(m);
|
||||
proof_ref pr(m);
|
||||
|
||||
|
|
@ -480,7 +480,7 @@ namespace smt {
|
|||
else if (m_fpa_util.is_float(e) || m_fpa_util.is_rm(e))
|
||||
res = convert_term(e);
|
||||
else if (m_arith_util.is_real(e) || m_bv_util.is_bv(e))
|
||||
res = convert_conversion_term(e);
|
||||
res = convert_conversion_term(e);
|
||||
else
|
||||
UNREACHABLE();
|
||||
|
||||
|
|
@ -492,7 +492,7 @@ namespace smt {
|
|||
m.inc_ref(res);
|
||||
m_trail_stack.push(fpa2bv_conversion_trail_elem(m, m_conversions, e));
|
||||
}
|
||||
|
||||
|
||||
return res;
|
||||
}
|
||||
|
||||
|
|
@ -501,7 +501,7 @@ namespace smt {
|
|||
ast_manager & m = get_manager();
|
||||
context & ctx = get_context();
|
||||
simplifier & simp = ctx.get_simplifier();
|
||||
|
||||
|
||||
expr_ref res(m), t(m);
|
||||
proof_ref t_pr(m);
|
||||
res = m.mk_true();
|
||||
|
|
@ -515,21 +515,21 @@ namespace smt {
|
|||
m_converter.m_extra_assertions.reset();
|
||||
|
||||
m_th_rw(res);
|
||||
|
||||
|
||||
CTRACE("t_fpa", !m.is_true(res), tout << "side condition: " << mk_ismt2_pp(res, m) << "\n";);
|
||||
return res;
|
||||
}
|
||||
|
||||
void theory_fpa::assert_cnstr(expr * e) {
|
||||
if (get_manager().is_true(e)) return;
|
||||
TRACE("t_fpa_detail", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << "\n";);
|
||||
TRACE("t_fpa_detail", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << "\n";);
|
||||
context & ctx = get_context();
|
||||
ctx.internalize(e, false);
|
||||
literal lit(ctx.get_literal(e));
|
||||
ctx.mark_as_relevant(lit);
|
||||
ctx.mk_th_axiom(get_id(), 1, &lit);
|
||||
ctx.mk_th_axiom(get_id(), 1, &lit);
|
||||
TRACE("t_fpa_detail", tout << "done asserting " << mk_ismt2_pp(e, get_manager()) << "\n";);
|
||||
}
|
||||
}
|
||||
|
||||
void theory_fpa::attach_new_th_var(enode * n) {
|
||||
context & ctx = get_context();
|
||||
|
|
@ -556,10 +556,10 @@ namespace smt {
|
|||
ctx.set_var_theory(l.var(), get_id());
|
||||
|
||||
expr_ref bv_atom(m);
|
||||
bv_atom = convert_atom(atom);
|
||||
bv_atom = convert_atom(atom);
|
||||
SASSERT(is_app(bv_atom) && m.is_bool(bv_atom));
|
||||
bv_atom = m.mk_and(bv_atom, mk_side_conditions());
|
||||
|
||||
|
||||
assert_cnstr(m.mk_iff(atom, bv_atom));
|
||||
return true;
|
||||
}
|
||||
|
|
@ -569,29 +569,29 @@ namespace smt {
|
|||
context & ctx = get_context();
|
||||
TRACE("t_fpa", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";);
|
||||
SASSERT(term->get_family_id() == get_family_id());
|
||||
SASSERT(!ctx.e_internalized(term));
|
||||
SASSERT(!ctx.e_internalized(term));
|
||||
|
||||
unsigned num_args = term->get_num_args();
|
||||
for (unsigned i = 0; i < num_args; i++)
|
||||
ctx.internalize(term->get_arg(i), false);
|
||||
|
||||
|
||||
enode * e = (ctx.e_internalized(term)) ? ctx.get_enode(term) :
|
||||
ctx.mk_enode(term, false, false, true);
|
||||
|
||||
|
||||
if (is_attached_to_var(e))
|
||||
return false;
|
||||
|
||||
attach_new_th_var(e);
|
||||
|
||||
// The conversion operators fp.to_* appear in non-FP constraints.
|
||||
// The corresponding constraints will not be translated and added
|
||||
// The corresponding constraints will not be translated and added
|
||||
// via convert(...) and assert_cnstr(...) in initialize_atom(...).
|
||||
// Therefore, we translate and assert them here.
|
||||
fpa_op_kind k = (fpa_op_kind)term->get_decl_kind();
|
||||
switch (k) {
|
||||
case OP_FPA_TO_UBV:
|
||||
case OP_FPA_TO_SBV:
|
||||
case OP_FPA_TO_REAL:
|
||||
case OP_FPA_TO_REAL:
|
||||
case OP_FPA_TO_IEEE_BV: {
|
||||
expr_ref conv(m);
|
||||
conv = convert(term);
|
||||
|
|
@ -599,32 +599,32 @@ namespace smt {
|
|||
assert_cnstr(mk_side_conditions());
|
||||
break;
|
||||
}
|
||||
default: /* ignore */;
|
||||
default: /* ignore */;
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
void theory_fpa::apply_sort_cnstr(enode * n, sort * s) {
|
||||
TRACE("t_fpa", tout << "apply sort cnstr for: " << mk_ismt2_pp(n->get_owner(), get_manager()) << "\n";);
|
||||
SASSERT(s->get_family_id() == get_family_id());
|
||||
|
||||
|
||||
ast_manager & m = get_manager();
|
||||
context & ctx = get_context();
|
||||
|
||||
|
||||
app_ref owner(m);
|
||||
owner = n->get_owner();
|
||||
|
||||
|
||||
SASSERT(owner->get_decl()->get_range() == s);
|
||||
|
||||
if ((m_fpa_util.is_float(s) || m_fpa_util.is_rm(s)) &&
|
||||
if ((m_fpa_util.is_float(s) || m_fpa_util.is_rm(s)) &&
|
||||
!is_attached_to_var(n)) {
|
||||
|
||||
attach_new_th_var(n);
|
||||
|
||||
attach_new_th_var(n);
|
||||
|
||||
if (m_fpa_util.is_rm(s)) {
|
||||
// For every RM term, we need to make sure that it's
|
||||
// associated bit-vector is within the valid range.
|
||||
// associated bit-vector is within the valid range.
|
||||
if (!m_fpa_util.is_unwrap(owner)) {
|
||||
expr_ref valid(m), limit(m);
|
||||
limit = m_bv_util.mk_numeral(4, 3);
|
||||
|
|
@ -638,7 +638,7 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
void theory_fpa::new_eq_eh(theory_var x, theory_var y) {
|
||||
void theory_fpa::new_eq_eh(theory_var x, theory_var y) {
|
||||
ast_manager & m = get_manager();
|
||||
enode * e_x = get_enode(x);
|
||||
enode * e_y = get_enode(y);
|
||||
|
|
@ -646,7 +646,7 @@ namespace smt {
|
|||
TRACE("t_fpa", tout << "new eq: " << x << " = " << y << std::endl;);
|
||||
TRACE("t_fpa_detail", tout << mk_ismt2_pp(e_x->get_owner(), m) << " = " <<
|
||||
mk_ismt2_pp(e_y->get_owner(), m) << std::endl;);
|
||||
|
||||
|
||||
fpa_util & fu = m_fpa_util;
|
||||
|
||||
expr_ref xe(m), ye(m);
|
||||
|
|
@ -664,13 +664,13 @@ namespace smt {
|
|||
"yc = " << mk_ismt2_pp(yc, m) << std::endl;);
|
||||
|
||||
expr_ref c(m);
|
||||
|
||||
|
||||
if ((fu.is_float(xe) && fu.is_float(ye)) ||
|
||||
(fu.is_rm(xe) && fu.is_rm(ye)))
|
||||
m_converter.mk_eq(xc, yc, c);
|
||||
else
|
||||
else
|
||||
c = m.mk_eq(xc, yc);
|
||||
|
||||
|
||||
m_th_rw(c);
|
||||
assert_cnstr(m.mk_iff(m.mk_eq(xe, ye), c));
|
||||
assert_cnstr(mk_side_conditions());
|
||||
|
|
@ -722,33 +722,33 @@ namespace smt {
|
|||
m_trail_stack.push_scope();
|
||||
}
|
||||
|
||||
void theory_fpa::pop_scope_eh(unsigned num_scopes) {
|
||||
void theory_fpa::pop_scope_eh(unsigned num_scopes) {
|
||||
m_trail_stack.pop_scope(num_scopes);
|
||||
TRACE("t_fpa", tout << "pop " << num_scopes << "; now " << m_trail_stack.get_num_scopes() << "\n";);
|
||||
// unsigned num_old_vars = get_old_num_vars(num_scopes);
|
||||
// unsigned num_old_vars = get_old_num_vars(num_scopes);
|
||||
theory::pop_scope_eh(num_scopes);
|
||||
}
|
||||
}
|
||||
|
||||
void theory_fpa::assign_eh(bool_var v, bool is_true) {
|
||||
ast_manager & m = get_manager();
|
||||
context & ctx = get_context();
|
||||
expr * e = ctx.bool_var2expr(v);
|
||||
|
||||
|
||||
TRACE("t_fpa", tout << "assign_eh for: " << v << " (" << is_true << "):\n" << mk_ismt2_pp(e, m) << "\n";);
|
||||
|
||||
|
||||
expr_ref converted(m);
|
||||
converted = m.mk_and(convert(e), mk_side_conditions());
|
||||
if (is_true)
|
||||
assert_cnstr(m.mk_implies(e, converted));
|
||||
else
|
||||
assert_cnstr(m.mk_implies(m.mk_not(e), m.mk_not(converted)));
|
||||
else
|
||||
assert_cnstr(m.mk_implies(m.mk_not(e), m.mk_not(converted)));
|
||||
}
|
||||
|
||||
void theory_fpa::relevant_eh(app * n) {
|
||||
ast_manager & m = get_manager();
|
||||
TRACE("t_fpa", tout << "relevant_eh for: " << mk_ismt2_pp(n, m) << "\n";);
|
||||
|
||||
mpf_manager & mpfm = m_fpa_util.fm();
|
||||
mpf_manager & mpfm = m_fpa_util.fm();
|
||||
|
||||
if (m_fpa_util.is_float(n) || m_fpa_util.is_rm(n)) {
|
||||
if (!m_fpa_util.is_unwrap(n)) {
|
||||
|
|
@ -757,7 +757,7 @@ namespace smt {
|
|||
mpf_rounding_mode rm;
|
||||
scoped_mpf val(mpfm);
|
||||
if (m_fpa_util.is_rm_numeral(n, rm)) {
|
||||
c = m.mk_eq(wrapped, m_bv_util.mk_numeral(rm, 3));
|
||||
c = m.mk_eq(wrapped, m_bv_util.mk_numeral(rm, 3));
|
||||
assert_cnstr(c);
|
||||
}
|
||||
else if (m_fpa_util.is_numeral(n, val)) {
|
||||
|
|
@ -772,7 +772,7 @@ namespace smt {
|
|||
assert_cnstr(c);
|
||||
}
|
||||
else {
|
||||
c = m.mk_eq(unwrap(wrapped, m.get_sort(n)), n);
|
||||
c = m.mk_eq(unwrap(wrapped, m.get_sort(n)), n);
|
||||
assert_cnstr(c);
|
||||
}
|
||||
}
|
||||
|
|
@ -803,7 +803,7 @@ namespace smt {
|
|||
final_check_status theory_fpa::final_check_eh() {
|
||||
TRACE("t_fpa", tout << "final_check_eh\n";);
|
||||
SASSERT(m_converter.m_extra_assertions.empty());
|
||||
return FC_DONE;
|
||||
return FC_DONE;
|
||||
}
|
||||
|
||||
void theory_fpa::init_model(model_generator & mg) {
|
||||
|
|
@ -813,7 +813,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
model_value_proc * theory_fpa::mk_value(enode * n, model_generator & mg) {
|
||||
TRACE("t_fpa", tout << "mk_value for: " << mk_ismt2_pp(n->get_owner(), get_manager()) <<
|
||||
TRACE("t_fpa", tout << "mk_value for: " << mk_ismt2_pp(n->get_owner(), get_manager()) <<
|
||||
" (sort " << mk_ismt2_pp(get_manager().get_sort(n->get_owner()), get_manager()) << ")\n";);
|
||||
|
||||
ast_manager & m = get_manager();
|
||||
|
|
@ -821,14 +821,14 @@ namespace smt {
|
|||
app_ref owner(m);
|
||||
owner = n->get_owner();
|
||||
|
||||
// If the owner is not internalized, it doesn't have an enode associated.
|
||||
// If the owner is not internalized, it doesn't have an enode associated.
|
||||
SASSERT(ctx.e_internalized(owner));
|
||||
|
||||
|
||||
if (m_fpa_util.is_rm_numeral(owner) ||
|
||||
m_fpa_util.is_numeral(owner)) {
|
||||
return alloc(expr_wrapper_proc, owner);
|
||||
}
|
||||
|
||||
|
||||
model_value_proc * res = 0;
|
||||
|
||||
app_ref wrapped(m);
|
||||
|
|
@ -849,7 +849,7 @@ namespace smt {
|
|||
a2 = to_app(owner->get_arg(2));
|
||||
unsigned ebits = m_fpa_util.get_ebits(m.get_sort(owner));
|
||||
unsigned sbits = m_fpa_util.get_sbits(m.get_sort(owner));
|
||||
fpa_value_proc * vp = alloc(fpa_value_proc, this, ebits, sbits);
|
||||
fpa_value_proc * vp = alloc(fpa_value_proc, this, ebits, sbits);
|
||||
vp->add_dependency(ctx.get_enode(a0));
|
||||
vp->add_dependency(ctx.get_enode(a1));
|
||||
vp->add_dependency(ctx.get_enode(a2));
|
||||
|
|
@ -891,8 +891,8 @@ namespace smt {
|
|||
{
|
||||
ast_manager & m = get_manager();
|
||||
context & ctx = get_context();
|
||||
|
||||
out << "fpa theory variables:" << std::endl;
|
||||
|
||||
out << "fpa theory variables:" << std::endl;
|
||||
ptr_vector<enode>::const_iterator it = ctx.begin_enodes();
|
||||
ptr_vector<enode>::const_iterator end = ctx.end_enodes();
|
||||
for (; it != end; it++) {
|
||||
|
|
@ -907,7 +907,7 @@ namespace smt {
|
|||
for (; it != end; it++) {
|
||||
theory_var v = (*it)->get_th_var(m_bv_util.get_family_id());
|
||||
if (v != -1) out << v << " -> " <<
|
||||
mk_ismt2_pp((*it)->get_owner(), m) << std::endl;
|
||||
mk_ismt2_pp((*it)->get_owner(), m) << std::endl;
|
||||
}
|
||||
|
||||
out << "arith theory variables:" << std::endl;
|
||||
|
|
|
|||
|
|
@ -84,13 +84,13 @@ namespace smt {
|
|||
virtual void mk_const(func_decl * f, expr_ref & result);
|
||||
virtual void mk_rm_const(func_decl * f, expr_ref & result);
|
||||
virtual void mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
|
||||
|
||||
virtual expr_ref mk_min_unspecified(func_decl * f, expr * x, expr * y);
|
||||
virtual expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y);
|
||||
};
|
||||
|
||||
|
||||
class fpa_value_proc : public model_value_proc {
|
||||
protected:
|
||||
protected:
|
||||
theory_fpa & m_th;
|
||||
ast_manager & m;
|
||||
fpa_util & m_fu;
|
||||
|
|
@ -100,10 +100,10 @@ namespace smt {
|
|||
unsigned m_sbits;
|
||||
|
||||
public:
|
||||
fpa_value_proc(theory_fpa * th, unsigned ebits, unsigned sbits) :
|
||||
fpa_value_proc(theory_fpa * th, unsigned ebits, unsigned sbits) :
|
||||
m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util),
|
||||
m_ebits(ebits), m_sbits(sbits) {}
|
||||
|
||||
|
||||
virtual ~fpa_value_proc() {}
|
||||
|
||||
void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); }
|
||||
|
|
@ -123,7 +123,7 @@ namespace smt {
|
|||
buffer<model_value_dependency> m_deps;
|
||||
|
||||
public:
|
||||
fpa_rm_value_proc(theory_fpa * th) :
|
||||
fpa_rm_value_proc(theory_fpa * th) :
|
||||
m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util) {}
|
||||
|
||||
void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); }
|
||||
|
|
@ -135,7 +135,7 @@ namespace smt {
|
|||
virtual ~fpa_rm_value_proc() {}
|
||||
virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values);
|
||||
};
|
||||
|
||||
|
||||
protected:
|
||||
fpa2bv_converter_wrapped m_converter;
|
||||
fpa2bv_rewriter m_rw;
|
||||
|
|
@ -159,10 +159,10 @@ namespace smt {
|
|||
virtual void pop_scope_eh(unsigned num_scopes);
|
||||
virtual void reset_eh();
|
||||
virtual theory* mk_fresh(context*) { return alloc(theory_fpa, get_manager()); }
|
||||
virtual char const * get_name() const { return "fpa"; }
|
||||
virtual char const * get_name() const { return "fpa"; }
|
||||
|
||||
virtual model_value_proc * mk_value(enode * n, model_generator & mg);
|
||||
|
||||
|
||||
void assign_eh(bool_var v, bool is_true);
|
||||
virtual void relevant_eh(app * n);
|
||||
virtual void init_model(model_generator & m);
|
||||
|
|
@ -181,14 +181,14 @@ namespace smt {
|
|||
expr_ref convert_term(expr * e);
|
||||
expr_ref convert_conversion_term(expr * e);
|
||||
expr_ref convert_unwrap(expr * e);
|
||||
|
||||
|
||||
void add_trail(ast * a);
|
||||
|
||||
void attach_new_th_var(enode * n);
|
||||
void assert_cnstr(expr * e);
|
||||
|
||||
app_ref wrap(expr * e);
|
||||
app_ref unwrap(expr * e, sort * s);
|
||||
app_ref unwrap(expr * e, sort * s);
|
||||
};
|
||||
|
||||
};
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue