mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

pull unstable

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
This commit is contained in:
Nikolaj Bjorner 2015-04-01 14:57:11 -07:00
commit 52619b9dbb
337 changed files with 24943 additions and 30606 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/asserted_formulas.cpp
View file

@ -22,6 +22,7 @@ Revision History:
#include"arith_simplifier_plugin.h"
#include"array_simplifier_plugin.h"
#include"datatype_simplifier_plugin.h"
#include"fpa_simplifier_plugin.h"
#include"bv_simplifier_plugin.h"
#include"for_each_expr.h"
#include"well_sorted.h"
@ -96,7 +97,8 @@ void asserted_formulas::setup_simplifier_plugins(simplifier & s, basic_simplifie
s.register_plugin(alloc(array_simplifier_plugin, m_manager, *bsimp, s, m_params));
bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, m_params);
s.register_plugin(bvsimp);
s.register_plugin(alloc(datatype_simplifier_plugin, m_manager, *bsimp));
s.register_plugin(alloc(datatype_simplifier_plugin, m_manager, *bsimp));
s.register_plugin(alloc(fpa_simplifier_plugin, m_manager, *bsimp));
}
void asserted_formulas::init(unsigned num_formulas, expr * const * formulas, proof * const * prs) {
@ -601,7 +603,7 @@ void asserted_formulas::propagate_values() {
proof_ref_vector new_prs1(m_manager);
expr_ref_vector new_exprs2(m_manager);
proof_ref_vector new_prs2(m_manager);
unsigned i = m_asserted_qhead;
unsigned i = 0;
unsigned sz = m_asserted_formulas.size();
for (; i < sz; i++) {
expr * n = m_asserted_formulas.get(i);

2
src/smt/database.h
View file

@ -1,4 +1,4 @@
static char const * g_pattern_database =
static char const g_pattern_database[] =
"(benchmark patterns \n"
" :status unknown \n"
" :logic ALL \n"

22
src/smt/params/dyn_ack_params.cpp
View file

@ -17,16 +17,14 @@ Revision History:
--*/
#include"dyn_ack_params.h"
#include"smt_params_helper.hpp"
#if 0
void dyn_ack_params::register_params(ini_params & p) {
p.register_int_param("dack", 0, 2, reinterpret_cast<int&>(m_dack),
"0 - disable dynamic ackermannization, 1 - expand Leibniz's axiom if a congruence is the root of a conflict, 2 - expand Leibniz's axiom if a congruence is used during conflict resolution.");
p.register_bool_param("dack_eq", m_dack_eq, "enable dynamic ackermannization for transtivity of equalities");
p.register_unsigned_param("dack_threshold", m_dack_threshold, "number of times the congruence rule must be used before Leibniz's axiom is expanded");
p.register_double_param("dack_factor", m_dack_factor, "number of instance per conflict");
p.register_unsigned_param("dack_gc", m_dack_gc, "Dynamic ackermannization garbage collection frequency (per conflict).");
p.register_double_param("dack_gc_inv_decay", m_dack_gc_inv_decay);
}
#endif
void dyn_ack_params::updt_params(params_ref const & _p) {
smt_params_helper p(_p);
m_dack = static_cast<dyn_ack_strategy>(p.dack());
m_dack_eq = p.dack_eq();
m_dack_factor = p.dack_factor();
m_dack_threshold = p.dack_threshold();
m_dack_gc = p.dack_gc();
m_dack_gc_inv_decay = p.dack_gc_inv_decay();
}

6
src/smt/params/dyn_ack_params.h
View file

@ -19,6 +19,8 @@ Revision History:
#ifndef _DYN_ACK_PARAMS_H_
#define _DYN_ACK_PARAMS_H_
#include"params.h"
enum dyn_ack_strategy {
DACK_DISABLED,
DACK_ROOT, // congruence is the root of the conflict
@ -34,15 +36,17 @@ struct dyn_ack_params {
double m_dack_gc_inv_decay;
public:
dyn_ack_params():
dyn_ack_params(params_ref const & p = params_ref()) :
m_dack(DACK_ROOT),
m_dack_eq(false),
m_dack_factor(0.1),
m_dack_threshold(10),
m_dack_gc(2000),
m_dack_gc_inv_decay(0.8) {
updt_params(p);
}
void updt_params(params_ref const & _p);
};

3
src/smt/params/smt_params.cpp
View file

@ -34,7 +34,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
m_delay_units = p.delay_units();
m_delay_units_threshold = p.delay_units_threshold();
m_preprocess = _p.get_bool("preprocess", true); // hidden parameter
m_soft_timeout = p.soft_timeout();
m_timeout = p.timeout();
model_params mp(_p);
m_model_compact = mp.compact();
if (_p.get_bool("arith.greatest_error_pivot", false))
@ -46,6 +46,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
void smt_params::updt_params(params_ref const & p) {
preprocessor_params::updt_params(p);
dyn_ack_params::updt_params(p);
qi_params::updt_params(p);
theory_arith_params::updt_params(p);
theory_bv_params::updt_params(p);

4
src/smt/params/smt_params.h
View file

@ -204,7 +204,7 @@ struct smt_params : public preprocessor_params,
bool m_preprocess; // temporary hack for disabling all preprocessing..
bool m_user_theory_preprocess_axioms;
bool m_user_theory_persist_axioms;
unsigned m_soft_timeout;
unsigned m_timeout;
bool m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples.
bool m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples.
bool m_dump_goal_as_smt;
@ -272,7 +272,7 @@ struct smt_params : public preprocessor_params,
m_preprocess(true), // temporary hack for disabling all preprocessing..
m_user_theory_preprocess_axioms(false),
m_user_theory_persist_axioms(false),
m_soft_timeout(0),
m_timeout(0),
m_at_labels_cex(false),
m_check_at_labels(false),
m_dump_goal_as_smt(false),

10
src/smt/params/smt_params_helper.pyg
View file

@ -15,7 +15,7 @@ def_module_params(module_name='smt',
('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ingored if delay_units is false'),
('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),
('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'),
('soft_timeout', UINT, 0, 'soft timeout (0 means no timeout)'),
('timeout', UINT, 0, 'timeout (0 means no timeout)'),
('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),
('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'),
('mbqi.max_cexs_incr', UINT, 0, 'increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI'),
@ -50,5 +50,11 @@ def_module_params(module_name='smt',
('pb.enable_compilation', BOOL, True, 'enable compilation into sorting circuits for Pseudo-Boolean'),
('pb.enable_simplex', BOOL, False, 'enable simplex to check rational feasibility'),
('array.weak', BOOL, False, 'weak array theory'),
('array.extensional', BOOL, True, 'extensional array theory')
('array.extensional', BOOL, True, 'extensional array theory'),
('dack', UINT, 1, '0 - disable dynamic ackermannization, 1 - expand Leibniz\'s axiom if a congruence is the root of a conflict, 2 - expand Leibniz\'s axiom if a congruence is used during conflict resolution'),
('dack.eq', BOOL, False, 'enable dynamic ackermannization for transtivity of equalities'),
('dack.factor', DOUBLE, 0.1, 'number of instance per conflict'),
('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'),
('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'),
('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded')
))

2
src/smt/smt_case_split_queue.cpp
View file

@ -1091,7 +1091,7 @@ namespace smt {
case_split_queue * mk_case_split_queue(context & ctx, smt_params & p) {
if (p.m_relevancy_lvl < 2 && (p.m_case_split_strategy == CS_RELEVANCY || p.m_case_split_strategy == CS_RELEVANCY_ACTIVITY ||
p.m_case_split_strategy == CS_RELEVANCY_GOAL)) {
warning_msg("relevacy must be enabled to use option CASE_SPLIT=3, 4 or 5");
warning_msg("relevancy must be enabled to use option CASE_SPLIT=3, 4 or 5");
p.m_case_split_strategy = CS_ACTIVITY;
}
if (p.m_auto_config && (p.m_case_split_strategy == CS_RELEVANCY || p.m_case_split_strategy == CS_RELEVANCY_ACTIVITY ||

9
src/smt/smt_context.cpp
View file

@ -3328,13 +3328,13 @@ namespace smt {
CASSERT("dyn_ack", check_clauses(m_lemmas) && check_clauses(m_aux_clauses));
}
if (resource_limits_exceeded()) {
SASSERT(!inconsistent());
if (resource_limits_exceeded() && !inconsistent()) {
return l_undef;
}
if (m_base_lvl == m_scope_lvl && m_fparams.m_simplify_clauses)
simplify_clauses();
if (!decide()) {
final_check_status fcs = final_check();
@ -3349,8 +3349,7 @@ namespace smt {
}
}
if (resource_limits_exceeded()) {
SASSERT(!inconsistent());
if (resource_limits_exceeded() && !inconsistent()) {
return l_undef;
}
}
@ -3363,7 +3362,7 @@ namespace smt {
if (m_last_search_failure != OK)
return true;
if (m_timer.ms_timeout(m_fparams.m_soft_timeout)) {
if (m_timer.ms_timeout(m_fparams.m_timeout)) {
m_last_search_failure = TIMEOUT;
return true;
}

3
src/smt/smt_implied_equalities.cpp
View file

@ -166,11 +166,10 @@ namespace smt {
terms[i].term = m.mk_app(m_array_util.get_family_id(), OP_SELECT, 0, 0, args.size(), args.c_ptr());
}
assert_relevant(terms);
lbool is_sat = m_solver.check_sat(0,0);
VERIFY(m_solver.check_sat(0,0) != l_false);
model_ref model1;
m_solver.get_model(model1);
SASSERT(model1.get());
SASSERT(is_sat != l_false);
get_implied_equalities_model_based(model1, terms);
m_solver.pop(1);
return;

4
src/smt/smt_kernel.cpp
View file

@ -236,8 +236,8 @@ namespace smt {
params_ref ps = m_imp->params();
#pragma omp critical (smt_kernel)
{
dealloc(m_imp);
m_imp = alloc(imp, _m, fps, ps);
m_imp->~imp();
m_imp = new (m_imp) imp(_m, fps, ps);
}
}

1
src/smt/smt_model_checker.cpp
View file

@ -282,6 +282,7 @@ namespace smt {
if (!m_fparams) {
m_fparams = alloc(smt_params, m_context->get_fparams());
m_fparams->m_relevancy_lvl = 0; // no relevancy since the model checking problems are quantifier free
m_fparams->m_case_split_strategy = CS_ACTIVITY; // avoid warning messages about smt.case_split >= 3.
}
if (!m_aux_context) {
symbol logic;

4
src/smt/smt_quantifier.cpp
View file

@ -361,8 +361,8 @@ namespace smt {
context & ctx = m_imp->m_context;
smt_params & p = m_imp->m_params;
quantifier_manager_plugin * plugin = m_imp->m_plugin->mk_fresh();
dealloc(m_imp);
m_imp = alloc(imp, *this, ctx, p, plugin);
m_imp->~imp();
m_imp = new (m_imp) imp(*this, ctx, p, plugin);
plugin->set_manager(*this);
}
}

58
src/smt/smt_setup.cpp
View file

@ -31,6 +31,7 @@ Revision History:
#include"theory_dl.h"
#include"theory_seq_empty.h"
#include"theory_pb.h"
#include"theory_fpa.h"
namespace smt {
@ -113,6 +114,10 @@ namespace smt {
setup_UFLRA();
else if (m_logic == "LRA")
setup_LRA();
else if (m_logic == "QF_FP")
setup_QF_FP();
else if (m_logic == "QF_FPBV")
setup_QF_FPBV();
else
setup_unknown();
}
@ -694,6 +699,16 @@ namespace smt {
setup_mi_arith();
}
void setup::setup_QF_FP() {
setup_QF_BV();
m_context.register_plugin(alloc(smt::theory_fpa, m_manager));
}
void setup::setup_QF_FPBV() {
setup_QF_BV();
m_context.register_plugin(alloc(smt::theory_fpa, m_manager));
}
bool is_arith(static_features const & st) {
return st.m_num_arith_ineqs > 0 || st.m_num_arith_terms > 0 || st.m_num_arith_eqs > 0;
}
@ -810,6 +825,11 @@ namespace smt {
m_context.register_plugin(alloc(theory_pb, m_manager, m_params));
}
void setup::setup_fpa() {
setup_bv();
m_context.register_plugin(alloc(theory_fpa, m_manager));
}
void setup::setup_unknown() {
setup_arith();
setup_arrays();
@ -818,6 +838,7 @@ namespace smt {
setup_dl();
setup_seq();
setup_card();
setup_fpa();
}
void setup::setup_unknown(static_features & st) {
@ -829,6 +850,7 @@ namespace smt {
setup_AUFLIA(false);
setup_datatypes();
setup_bv();
setup_fpa();
return;
}
@ -839,7 +861,10 @@ namespace smt {
tout << "is_arith: " << is_arith(st) << "\n";
tout << "has UF: " << st.has_uf() << "\n";
tout << "has real: " << st.m_has_real << "\n";
tout << "has int: " << st.m_has_int << "\n";);
tout << "has int: " << st.m_has_int << "\n";
tout << "has bv: " << st.m_has_bv << "\n";
tout << "has fpa: " << st.m_has_fpa << "\n";
tout << "has arrays: " << st.m_has_arrays << "\n";);
if (st.num_non_uf_theories() == 0) {
setup_QF_UF(st);
@ -882,7 +907,36 @@ namespace smt {
return;
}
// TODO QF_BV, QF_AUFBV, QF_AUFLIA
if (st.num_theories() == 1 && st.m_has_bv) {
setup_QF_BV();
return;
}
if (st.num_theories() == 1 && st.m_has_fpa) {
setup_QF_FP();
return;
}
if (st.num_theories() == 2 && st.m_has_fpa && st.m_has_bv) {
setup_QF_FPBV();
return;
}
if (st.num_theories() == 1 && st.m_has_arrays) {
setup_QF_AX();
return;
}
if (st.num_theories() == 2 && st.has_uf() && st.m_has_arrays && st.m_has_bv) {
setup_QF_AUFBV();
return;
}
if (st.num_theories() == 2 && st.has_uf() && st.m_has_arrays && st.m_has_int) {
setup_QF_AUFLIA();
return;
}
setup_unknown();
}

4
src/smt/smt_setup.h
View file

@ -75,6 +75,8 @@ namespace smt {
void setup_QF_AX(static_features const & st);
void setup_QF_AUFLIA();
void setup_QF_AUFLIA(static_features const & st);
void setup_QF_FP();
void setup_QF_FPBV();
void setup_LRA();
void setup_AUFLIA(bool simple_array = true);
void setup_AUFLIA(static_features const & st);
@ -95,6 +97,8 @@ namespace smt {
void setup_card();
void setup_i_arith();
void setup_mi_arith();
void setup_fpa();
public:
setup(context & c, smt_params & params);
void mark_already_configured() { m_already_configured = true; }

42
src/smt/theory_arith_core.h
View file

@ -340,8 +340,9 @@ namespace smt {
theory_var theory_arith<Ext>::internalize_rem(app * n) {
theory_var s = mk_binary_op(n);
context & ctx = get_context();
if (!ctx.relevancy())
if (!ctx.relevancy()) {
mk_rem_axiom(n->get_arg(0), n->get_arg(1));
}
return s;
}
@ -460,22 +461,20 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::mk_rem_axiom(expr * dividend, expr * divisor) {
if (!m_util.is_zero(divisor)) {
// if divisor is zero, then rem is an uninterpreted function.
ast_manager & m = get_manager();
expr * zero = m_util.mk_numeral(rational(0), true);
expr * rem = m_util.mk_rem(dividend, divisor);
expr * mod = m_util.mk_mod(dividend, divisor);
expr_ref dltz(m), eq1(m), eq2(m);
dltz = m_util.mk_lt(divisor, zero);
eq1 = m.mk_eq(rem, mod);
eq2 = m.mk_eq(rem, m_util.mk_sub(zero, mod));
// n < 0 || rem(a,n) = mod(a, n)
mk_axiom(dltz, eq1);
dltz = m.mk_not(dltz);
// !n < 0 || rem(a,n) = -mod(a, n)
mk_axiom(dltz, eq2);
}
// if divisor is zero, then rem is an uninterpreted function.
ast_manager & m = get_manager();
expr * zero = m_util.mk_numeral(rational(0), true);
expr * rem = m_util.mk_rem(dividend, divisor);
expr * mod = m_util.mk_mod(dividend, divisor);
expr_ref dltz(m), eq1(m), eq2(m);
dltz = m_util.mk_lt(divisor, zero);
eq1 = m.mk_eq(rem, mod);
eq2 = m.mk_eq(rem, m_util.mk_sub(zero, mod));
// n < 0 || rem(a,n) = mod(a, n)
mk_axiom(dltz, eq1);
dltz = m.mk_not(dltz);
// !n < 0 || rem(a,n) = -mod(a, n)
mk_axiom(dltz, eq2);
}
//
@ -569,11 +568,9 @@ namespace smt {
template<typename Ext>
theory_var theory_arith<Ext>::internalize_numeral(app * n) {
rational _val;
context & ctx = get_context();
bool flag = m_util.is_numeral(n, _val);
VERIFY(m_util.is_numeral(n, _val));
numeral val(_val);
SASSERT(flag);
SASSERT(!ctx.e_internalized(n));
SASSERT(!get_context().e_internalized(n));
enode * e = mk_enode(n);
// internalizer is marking enodes as interpreted whenever the associated ast is a value and a constant.
// e->mark_as_interpreted();
@ -3146,8 +3143,7 @@ namespace smt {
del_vars(get_old_num_vars(num_scopes));
m_scopes.shrink(new_lvl);
theory::pop_scope_eh(num_scopes);
bool r = make_feasible();
SASSERT(r);
VERIFY(make_feasible());
SASSERT(m_to_patch.empty());
m_to_check.reset();
m_in_to_check.reset();

3
src/smt/theory_array_base.cpp
View file

@ -645,11 +645,10 @@ namespace smt {
if (is_store(n)) {
theory_var w = n->get_arg(0)->get_th_var(get_id());
SASSERT(w != null_theory_var);
ast_manager& m = get_manager();
mg_merge(v, get_representative(w));
TRACE("array", tout << "merge: " << mk_pp(n->get_owner(), m) << " " << v << " " << w << "\n";);
TRACE("array", tout << "merge: " << mk_pp(n->get_owner(), get_manager()) << " " << v << " " << w << "\n";);
}
else if (is_const(n)) {
set_default(v, n->get_arg(0));

789
src/smt/theory_fpa.cpp
View file

@ -17,30 +17,801 @@ Revision History:
--*/
#include"ast_smt2_pp.h"
#include"smt_context.h"
#include"theory_fpa.h"
#include"theory_bv.h"
#include"smt_model_generator.h"
namespace smt {
class fpa2bv_conversion_trail_elem : public trail<theory_fpa> {
ast_manager & m;
obj_map<expr, expr*> & m_conversions;
expr * m_e;
public:
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) {
expr * v = m_conversions.find(m_e);
m_conversions.remove(m_e);
m.dec_ref(v);
}
};
void theory_fpa::fpa2bv_converter_wrapped::mk_const(func_decl * f, expr_ref & result) {
SASSERT(f->get_family_id() == null_family_id);
SASSERT(f->get_arity() == 0);
expr * r;
if (m_const2bv.find(f, r)) {
result = r;
}
else {
sort * s = f->get_range();
expr_ref bv(m);
bv = m_th.wrap(m.mk_const(f));
unsigned bv_sz = m_th.m_bv_util.get_bv_size(bv);
unsigned ebits = m_th.m_fpa_util.get_ebits(s);
unsigned sbits = m_th.m_fpa_util.get_sbits(s);
SASSERT(bv_sz == ebits + sbits);
m_th.m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv),
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv),
m_bv_util.mk_extract(sbits - 2, 0, bv),
result);
SASSERT(m_th.m_fpa_util.is_float(result));
m_const2bv.insert(f, result);
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);
SASSERT(f->get_arity() == 0);
expr * r;
if (m_rm_const2bv.find(f, r)) {
result = r;
}
else {
SASSERT(is_rm(f->get_range()));
result = m_th.wrap(m.mk_const(f));
m_rm_const2bv.insert(f, result);
m.inc_ref(f);
m.inc_ref(result);
}
}
theory_fpa::theory_fpa(ast_manager & m) :
theory(m.mk_family_id("fpa")),
m_converter(m, this),
m_rw(m, m_converter, params_ref()),
m_th_rw(m),
m_trail_stack(*this),
m_fpa_util(m_converter.fu()),
m_bv_util(m_converter.bu()),
m_arith_util(m_converter.au())
{
params_ref p;
p.set_bool("arith_lhs", true);
m_th_rw.updt_params(p);
}
theory_fpa::~theory_fpa()
{
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);
}
app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
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;
scoped_mpz bias(mpzm);
mpzm.power(mpz(2), m_ebits - 1, bias);
mpzm.dec(bias);
scoped_mpz sgn_z(mpzm), sig_z(mpzm), exp_z(mpzm);
unsigned bv_sz;
if (values.size() == 1) {
SASSERT(m_bu.is_bv(values[0]));
SASSERT(m_bu.get_bv_size(values[0]) == (m_ebits + m_sbits));
rational all_r(0);
scoped_mpz all_z(mpzm);
bool r = m_bu.is_numeral(values[0], all_r, bv_sz);
SASSERT(r);
SASSERT(bv_sz == (m_ebits + m_sbits));
SASSERT(all_r.is_int());
mpzm.set(all_z, all_r.to_mpq().numerator());
mpzm.machine_div2k(all_z, m_ebits + m_sbits - 1, sgn_z);
mpzm.mod(all_z, mpfm.m_powers2(m_ebits + m_sbits - 1), all_z);
mpzm.machine_div2k(all_z, m_sbits - 1, exp_z);
mpzm.mod(all_z, mpfm.m_powers2(m_sbits - 1), all_z);
mpzm.set(sig_z, all_z);
}
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);
SASSERT(r && bv_sz == 1);
r = m_bu.is_numeral(values[1], exp_r, bv_sz);
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()));
mpzm.set(sgn_z, sgn_r.to_mpq().numerator());
mpzm.set(exp_z, exp_r.to_mpq().numerator());
mpzm.set(sig_z, sig_r.to_mpq().numerator());
}
else
UNREACHABLE();
scoped_mpz exp_u = exp_z - bias;
SASSERT(mpzm.is_int64(exp_u));
scoped_mpf f(mpfm);
mpfm.set(f, m_ebits, m_sbits, mpzm.is_one(sgn_z), sig_z, mpzm.get_int64(exp_u));
result = m_fu.mk_value(f);
TRACE("t_fpa", tout << "fpa_value_proc::mk_value [" <<
mpzm.to_string(sgn_z) << "," <<
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;
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;
case BV_RM_TIES_TO_EVEN: result = m_fu.mk_round_nearest_ties_to_even(); break;
case BV_RM_TO_NEGATIVE: result = m_fu.mk_round_toward_negative(); break;
case BV_RM_TO_POSITIVE: result = m_fu.mk_round_toward_positive(); break;
case BV_RM_TO_ZERO:
default: result = m_fu.mk_round_toward_zero();
}
TRACE("t_fpa", tout << "fpa_rm_value_proc::mk_value result: " <<
mk_ismt2_pp(result, m_th.get_manager()) << "\n";);
return result;
}
app_ref theory_fpa::wrap(expr * e) {
SASSERT(!m_fpa_util.is_wrap(e));
ast_manager & m = get_manager();
sort * e_srt = m.get_sort(e);
func_decl *w;
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);
else {
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);
}
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);
}
app_ref res(m);
res = m.mk_app(w, e);
return res;
}
app_ref theory_fpa::unwrap(expr * e, sort * s) {
SASSERT(!m_fpa_util.is_unwrap(e));
ast_manager & m = get_manager();
sort * bv_srt = m.get_sort(e);
func_decl *u;
if (!m_unwraps.find(bv_srt, u)) {
SASSERT(!m_unwraps.contains(bv_srt));
u = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVUNWRAP, 0, 0, 1, &bv_srt, s);
m_unwraps.insert(bv_srt, u);
m.inc_ref(u);
}
app_ref res(m);
res = m.mk_app(u, e);
return res;
}
expr_ref theory_fpa::convert_atom(expr * e) {
ast_manager & m = get_manager();
expr_ref res(m);
proof_ref pr(m);
m_rw(e, res);
m_th_rw(res, res);
SASSERT(is_app(res));
SASSERT(m.is_bool(res));
return res;
}
expr_ref theory_fpa::convert_term(expr * e) {
ast_manager & m = get_manager();
expr_ref e_conv(m), res(m);
proof_ref pr(m);
m_rw(e, e_conv);
if (m_fpa_util.is_rm(e)) {
SASSERT(is_sort_of(m.get_sort(e_conv), m_bv_util.get_family_id(), BV_SORT));
SASSERT(m_bv_util.get_bv_size(e_conv) == 3);
m_th_rw(e_conv, res);
}
else if (m_fpa_util.is_float(e)) {
expr_ref sgn(m), sig(m), exp(m);
m_converter.split_fp(e_conv, sgn, exp, sig);
m_th_rw(sgn);
m_th_rw(exp);
m_th_rw(sig);
m_converter.mk_fp(sgn, exp, sig, res);
}
else
UNREACHABLE();
SASSERT(res.get() != 0);
return res;
}
expr_ref theory_fpa::convert_conversion_term(expr * e) {
/* This is for the conversion functions fp.to_* */
ast_manager & m = get_manager();
expr_ref res(m);
proof_ref pr(m);
SASSERT(m_arith_util.is_real(e) || m_bv_util.is_bv(e));
m_rw(e, res);
m_th_rw(res, res);
return res;
}
expr_ref theory_fpa::convert_unwrap(expr * e) {
SASSERT(m_fpa_util.is_unwrap(e));
ast_manager & m = get_manager();
sort * srt = m.get_sort(e);
expr_ref res(m);
if (m_fpa_util.is_rm(srt)) {
res = to_app(e)->get_arg(0);
}
else {
SASSERT(m_fpa_util.is_float(srt));
unsigned sbits = m_fpa_util.get_sbits(srt);
expr_ref bv(m);
bv = to_app(e)->get_arg(0);
unsigned bv_sz = m_bv_util.get_bv_size(bv);
m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv),
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv),
m_bv_util.mk_extract(sbits - 2, 0, bv),
res);
}
return res;
}
expr_ref theory_fpa::convert(expr * e)
{
ast_manager & m = get_manager();
expr_ref res(m);
if (m_conversions.contains(e)) {
res = m_conversions.find(e);
TRACE("t_fpa_detail", tout << "cached:" << std::endl;
tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl <<
mk_ismt2_pp(res, m) << std::endl;);
return res;
}
else {
if (m_fpa_util.is_unwrap(e))
res = convert_unwrap(e);
else if (m.is_bool(e))
res = convert_atom(e);
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);
else
UNREACHABLE();
TRACE("t_fpa_detail", tout << "converted; caching:" << std::endl;
tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl <<
mk_ismt2_pp(res, m) << std::endl;);
m_conversions.insert(e, res);
m.inc_ref(res);
m_trail_stack.push(fpa2bv_conversion_trail_elem(m, m_conversions, e));
}
return res;
}
expr_ref theory_fpa::mk_side_conditions()
{
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();
expr_ref_vector::iterator it = m_converter.m_extra_assertions.begin();
expr_ref_vector::iterator end = m_converter.m_extra_assertions.end();
for (; it != end; it++) {
simp(*it, t, t_pr);
res = m.mk_and(res, t);
}
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";);
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);
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();
theory_var v = mk_var(n);
ctx.attach_th_var(n, this, v);
TRACE("t_fpa_detail", tout << "new theory var: " << mk_ismt2_pp(n->get_owner(), get_manager()) << " := " << v << "\n";);
}
bool theory_fpa::internalize_atom(app * atom, bool gate_ctx) {
TRACE("bv", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << "\n";);
TRACE("t_fpa", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << "\n";);
SASSERT(atom->get_family_id() == get_family_id());
NOT_IMPLEMENTED_YET();
ast_manager & m = get_manager();
context & ctx = get_context();
if (ctx.b_internalized(atom))
return true;
unsigned num_args = atom->get_num_args();
for (unsigned i = 0; i < num_args; i++)
ctx.internalize(atom->get_arg(i), false);
literal l(ctx.mk_bool_var(atom));
ctx.set_var_theory(l.var(), get_id());
expr_ref bv_atom(m);
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;
}
void theory_fpa::new_eq_eh(theory_var, theory_var) {
NOT_IMPLEMENTED_YET();
bool theory_fpa::internalize_term(app * term) {
ast_manager & m = get_manager();
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));
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
// 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_IEEE_BV: {
expr_ref conv(m);
conv = convert(term);
assert_cnstr(m.mk_eq(term, conv));
assert_cnstr(mk_side_conditions());
break;
}
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(n->get_owner()->get_family_id() == get_family_id() ||
n->get_owner()->get_family_id() == null_theory_id);
SASSERT(s->get_family_id() == get_family_id());
if (!is_attached_to_var(n)) {
attach_new_th_var(n);
ast_manager & m = get_manager();
context & ctx = get_context();
app_ref owner(m);
sort_ref owner_sort(m);
owner = n->get_owner();
owner_sort = m.get_sort(owner);
if (m_fpa_util.is_rm(owner_sort)) {
// For every RM term, we need to make sure that it's
// 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);
valid = m_bv_util.mk_ule(wrap(owner), limit);
assert_cnstr(valid);
}
}
if (!ctx.relevancy() && !m_fpa_util.is_unwrap(owner))
assert_cnstr(m.mk_eq(unwrap(wrap(owner), owner_sort), owner));
}
}
void theory_fpa::new_diseq_eh(theory_var, theory_var) {
NOT_IMPLEMENTED_YET();
void theory_fpa::new_eq_eh(theory_var x, theory_var y) {
ast_manager & m = get_manager();
TRACE("t_fpa", tout << "new eq: " << x << " = " << y << std::endl;);
TRACE("t_fpa_detail", tout << mk_ismt2_pp(get_enode(x)->get_owner(), m) << " = " <<
mk_ismt2_pp(get_enode(y)->get_owner(), m) << std::endl;);
fpa_util & fu = m_fpa_util;
expr_ref xe(m), ye(m);
xe = get_enode(x)->get_owner();
ye = get_enode(y)->get_owner();
if ((m.is_bool(xe) && m.is_bool(ye)) ||
(m_bv_util.is_bv(xe) && m_bv_util.is_bv(ye))) {
SASSERT(to_app(xe)->get_decl()->get_family_id() == get_family_id());
return;
}
expr_ref xc(m), yc(m);
xc = convert(xe);
yc = convert(ye);
TRACE("t_fpa_detail", tout << "xc=" << mk_ismt2_pp(xc, m) << std::endl;
tout << "yc=" << mk_ismt2_pp(yc, m) << std::endl;);
expr_ref c(m);
if (fu.is_float(xe) && fu.is_float(ye))
{
expr *x_sgn, *x_sig, *x_exp;
m_converter.split_fp(xc, x_sgn, x_exp, x_sig);
expr *y_sgn, *y_sig, *y_exp;
m_converter.split_fp(yc, y_sgn, y_exp, y_sig);
c = m.mk_eq(m_bv_util.mk_concat(m_bv_util.mk_concat(x_sgn, x_exp), x_sig),
m_bv_util.mk_concat(m_bv_util.mk_concat(y_sgn, y_exp), y_sig));
}
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());
return;
}
void theory_fpa::new_diseq_eh(theory_var x, theory_var y) {
ast_manager & m = get_manager();
TRACE("t_fpa", tout << "new diseq: " << x << " != " << y << std::endl;);
TRACE("t_fpa_detail", tout << mk_ismt2_pp(get_enode(x)->get_owner(), m) << " != " <<
mk_ismt2_pp(get_enode(y)->get_owner(), m) << std::endl;);
expr_ref xe(m), ye(m);
xe = get_enode(x)->get_owner();
ye = get_enode(y)->get_owner();
if ((m.is_bool(xe) && m.is_bool(ye)) ||
(m_bv_util.is_bv(xe) && m_bv_util.is_bv(ye))) {
SASSERT(to_app(xe)->get_decl()->get_family_id() == get_family_id());
return;
}
fpa_util & fu = m_fpa_util;
expr_ref xc(m), yc(m);
xc = convert(xe);
yc = convert(ye);
expr_ref c(m);
if (fu.is_float(xe) && fu.is_float(ye))
{
expr *x_sgn, *x_sig, *x_exp;
m_converter.split_fp(xc, x_sgn, x_exp, x_sig);
expr *y_sgn, *y_sig, *y_exp;
m_converter.split_fp(yc, y_sgn, y_exp, y_sig);
c = m.mk_not(m.mk_eq(m_bv_util.mk_concat(m_bv_util.mk_concat(x_sgn, x_exp), x_sig),
m_bv_util.mk_concat(m_bv_util.mk_concat(y_sgn, y_exp), y_sig)));
}
else
c = m.mk_not(m.mk_eq(xc, yc));
m_th_rw(c);
assert_cnstr(m.mk_iff(m.mk_not(m.mk_eq(xe, ye)), c));
assert_cnstr(mk_side_conditions());
return;
}
void theory_fpa::push_scope_eh() {
NOT_IMPLEMENTED_YET();
theory::push_scope_eh();
m_trail_stack.push_scope();
}
void theory_fpa::pop_scope_eh(unsigned num_scopes) {
NOT_IMPLEMENTED_YET();
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);
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)));
}
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();
if (m_fpa_util.is_float(n) || m_fpa_util.is_rm(n)) {
if (!m_fpa_util.is_unwrap(n)) {
expr_ref wrapped(m), c(m);
wrapped = wrap(n);
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));
assert_cnstr(c);
}
else if (m_fpa_util.is_numeral(n, val)) {
expr_ref bv_val_e(m);
bv_val_e = convert(n);
SASSERT(is_app(bv_val_e));
SASSERT(to_app(bv_val_e)->get_num_args() == 3);
app_ref bv_val_a(to_app(bv_val_e.get()), m);
expr * args[] = { bv_val_a->get_arg(0), bv_val_a->get_arg(1), bv_val_a->get_arg(2) };
c = m.mk_eq(wrapped, m_bv_util.mk_concat(3, args));
c = m.mk_and(c, mk_side_conditions());
assert_cnstr(c);
}
else {
c = m.mk_eq(unwrap(wrapped, m.get_sort(n)), n);
assert_cnstr(c);
}
}
}
else if (n->get_family_id() == get_family_id()) {
// These are the conversion functions fp.to_* */
SASSERT(!m_fpa_util.is_float(n) && !m_fpa_util.is_rm(n));
}
else
UNREACHABLE();
}
void theory_fpa::reset_eh() {
TRACE("t_fpa", tout << "reset_eh\n";);
pop_scope_eh(m_trail_stack.get_num_scopes());
m_converter.reset();
m_rw.reset();
m_th_rw.reset();
m_trail_stack.pop_scope(m_trail_stack.get_num_scopes());
if (m_factory) dealloc(m_factory); m_factory = 0;
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);
theory::reset_eh();
}
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;
}
void theory_fpa::init_model(model_generator & mg) {
TRACE("t_fpa", tout << "initializing model" << std::endl; display(tout););
m_factory = alloc(fpa_value_factory, get_manager(), get_family_id());
mg.register_factory(m_factory);
}
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()) <<
" (sort " << mk_ismt2_pp(get_manager().get_sort(n->get_owner()), get_manager()) << ")\n";);
ast_manager & m = get_manager();
context & ctx = get_context();
app_ref owner(m);
owner = n->get_owner();
// 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);
wrapped = wrap(owner);
SASSERT(m_bv_util.is_bv(wrapped));
CTRACE("t_fpa_detail", !ctx.e_internalized(wrapped),
tout << "Model dependency not internalized: " <<
mk_ismt2_pp(wrapped, m) <<
" (owner " << (!ctx.e_internalized(owner) ? "not" : "is") <<
" internalized)" << std::endl;);
if (is_app_of(owner, get_family_id(), OP_FPA_FP)) {
SASSERT(to_app(owner)->get_num_args() == 3);
app_ref a0(m), a1(m), a2(m);
a0 = to_app(owner->get_arg(0));
a1 = to_app(owner->get_arg(1));
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);
vp->add_dependency(ctx.get_enode(a0));
vp->add_dependency(ctx.get_enode(a1));
vp->add_dependency(ctx.get_enode(a2));
TRACE("t_fpa_detail", tout << "Depends on: " <<
mk_ismt2_pp(a0, m) << " eq. cls. #" << get_enode(a0)->get_root()->get_owner()->get_id() << std::endl <<
mk_ismt2_pp(a1, m) << " eq. cls. #" << get_enode(a1)->get_root()->get_owner()->get_id() << std::endl <<
mk_ismt2_pp(a2, m) << " eq. cls. #" << get_enode(a2)->get_root()->get_owner()->get_id() << std::endl;);
res = vp;
}
else if (ctx.e_internalized(wrapped)) {
if (m_fpa_util.is_rm(owner)) {
fpa_rm_value_proc * vp = alloc(fpa_rm_value_proc, this);
vp->add_dependency(ctx.get_enode(wrapped));
res = vp;
}
else if (m_fpa_util.is_float(owner)) {
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);
enode * en = ctx.get_enode(wrapped);
vp->add_dependency(en);
TRACE("t_fpa_detail", tout << "Depends on: " << mk_ismt2_pp(wrapped, m) << " eq. cls. #" << en->get_root()->get_owner()->get_id() << std::endl;);
res = vp;
}
}
else {
unsigned ebits = m_fpa_util.get_ebits(m.get_sort(owner));
unsigned sbits = m_fpa_util.get_sbits(m.get_sort(owner));
return alloc(expr_wrapper_proc, m_fpa_util.mk_pzero(ebits, sbits));
}
SASSERT(res != 0);
return res;
}
void theory_fpa::finalize_model(model_generator & mg) {}
void theory_fpa::display(std::ostream & out) const
{
ast_manager & m = get_manager();
context & ctx = get_context();
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++) {
theory_var v = (*it)->get_th_var(get_family_id());
if (v != -1) out << v << " -> " <<
mk_ismt2_pp((*it)->get_owner(), m) << std::endl;
}
out << "bv theory variables:" << std::endl;
it = ctx.begin_enodes();
end = ctx.end_enodes();
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;
}
out << "arith theory variables:" << std::endl;
it = ctx.begin_enodes();
end = ctx.end_enodes();
for (; it != end; it++) {
theory_var v = (*it)->get_th_var(m_arith_util.get_family_id());
if (v != -1) out << v << " -> " <<
mk_ismt2_pp((*it)->get_owner(), m) << std::endl;
}
out << "equivalence classes:\n";
it = ctx.begin_enodes();
end = ctx.end_enodes();
for (; it != end; ++it) {
expr * n = (*it)->get_owner();
expr * r = (*it)->get_root()->get_owner();
out << r->get_id() << " --> " << mk_ismt2_pp(n, m) << std::endl;
}
}
};

163
src/smt/theory_fpa.h
View file

@ -20,26 +20,173 @@ Revision History:
#define _THEORY_FPA_H_
#include"smt_theory.h"
#include"trail.h"
#include"fpa2bv_converter.h"
#include"fpa2bv_rewriter.h"
#include"th_rewriter.h"
#include"value_factory.h"
#include"smt_model_generator.h"
namespace smt {
class theory_fpa : public theory {
fpa2bv_converter m_converter;
virtual final_check_status final_check_eh() { return FC_DONE; }
virtual bool internalize_atom(app*, bool);
virtual bool internalize_term(app*) { return internalize_atom(0, false); }
class fpa_value_factory : public value_factory {
fpa_util m_util;
virtual app * mk_value_core(mpf const & val, sort * s) {
SASSERT(m_util.get_ebits(s) == val.get_ebits());
SASSERT(m_util.get_sbits(s) == val.get_sbits());
return m_util.mk_value(val);
}
public:
fpa_value_factory(ast_manager & m, family_id fid) :
value_factory(m, fid),
m_util(m) {}
virtual ~fpa_value_factory() {}
virtual expr * get_some_value(sort * s) {
mpf_manager & mpfm = m_util.fm();
scoped_mpf q(mpfm);
mpfm.set(q, m_util.get_ebits(s), m_util.get_sbits(s), 0);
return m_util.mk_value(q);
}
virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
mpf_manager & mpfm = m_util.fm();
scoped_mpf q(mpfm);
mpfm.set(q, m_util.get_ebits(s), m_util.get_sbits(s), 0);
v1 = m_util.mk_value(q);
mpfm.set(q, m_util.get_ebits(s), m_util.get_sbits(s), 1);
v2 = m_util.mk_value(q);
return true;
}
virtual expr * get_fresh_value(sort * s) { NOT_IMPLEMENTED_YET(); }
virtual void register_value(expr * n) { /* Ignore */ }
app * mk_value(mpf const & x) {
return m_util.mk_value(x);
}
};
class theory_fpa : public theory {
protected:
typedef trail_stack<theory_fpa> th_trail_stack;
class fpa2bv_converter_wrapped : public fpa2bv_converter {
public:
theory_fpa & m_th;
fpa2bv_converter_wrapped(ast_manager & m, theory_fpa * th) :
fpa2bv_converter(m),
m_th(*th) {}
virtual ~fpa2bv_converter_wrapped() {}
virtual void mk_const(func_decl * f, expr_ref & result);
virtual void mk_rm_const(func_decl * f, expr_ref & result);
};
class fpa_value_proc : public model_value_proc {
protected:
theory_fpa & m_th;
ast_manager & m;
fpa_util & m_fu;
bv_util & m_bu;
buffer<model_value_dependency> m_deps;
unsigned m_ebits;
unsigned m_sbits;
public:
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)); }
virtual void get_dependencies(buffer<model_value_dependency> & result) {
result.append(m_deps);
}
virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values);
};
class fpa_rm_value_proc : public model_value_proc {
theory_fpa & m_th;
ast_manager & m;
fpa_util & m_fu;
bv_util & m_bu;
buffer<model_value_dependency> m_deps;
public:
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)); }
virtual void get_dependencies(buffer<model_value_dependency> & result) {
result.append(m_deps);
}
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;
th_rewriter m_th_rw;
th_trail_stack m_trail_stack;
fpa_value_factory * m_factory;
fpa_util & m_fpa_util;
bv_util & m_bv_util;
arith_util & m_arith_util;
obj_map<sort, func_decl*> m_wraps;
obj_map<sort, func_decl*> m_unwraps;
obj_map<expr, expr*> m_conversions;
virtual final_check_status final_check_eh();
virtual bool internalize_atom(app * atom, bool gate_ctx);
virtual bool internalize_term(app * term);
virtual void apply_sort_cnstr(enode * n, sort * s);
virtual void new_eq_eh(theory_var, theory_var);
virtual void new_diseq_eh(theory_var, theory_var);
virtual void push_scope_eh();
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);
virtual void finalize_model(model_generator & mg);
public:
theory_fpa(ast_manager& m) : theory(m.mk_family_id("fpa")), m_converter(m) {}
theory_fpa(ast_manager& m);
virtual ~theory_fpa();
virtual void display(std::ostream & out) const;
protected:
expr_ref mk_side_conditions();
expr_ref convert(expr * e);
expr_ref convert_atom(expr * e);
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);
};
};
#endif /* _THEORY_FPA_H_ */