Skip to content

Commit

Permalink
replace iterators by for, looking at @2596
Browse files Browse the repository at this point in the history 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Oct 12, 2019
1 parent 8d942ed commit ce06cd0
Show file tree
Hide file tree
Showing 4 changed files with 155 additions and 114 deletions.
184 changes: 76 additions & 108 deletions src/ast/fpa/bv2fpa_converter.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,50 +38,37 @@ bv2fpa_converter::bv2fpa_converter(ast_manager & m, fpa2bv_converter & conv) :
m_fpa_util(m),
m_bv_util(m),
m_th_rw(m) {
for (obj_map<func_decl, expr*>::iterator it = conv.m_const2bv.begin();
it != conv.m_const2bv.end();
it++)
{
m_const2bv.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
m.inc_ref(it->m_value);
for (auto const& kv : conv.m_const2bv) {
m_const2bv.insert(kv.m_key, kv.m_value);
m.inc_ref(kv.m_key);
m.inc_ref(kv.m_value);
}
for (obj_map<func_decl, expr*>::iterator it = conv.m_rm_const2bv.begin();
it != conv.m_rm_const2bv.end();
it++)
{
m_rm_const2bv.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
m.inc_ref(it->m_value);
for (auto const& kv : conv.m_rm_const2bv) {
m_rm_const2bv.insert(kv.m_key, kv.m_value);
m.inc_ref(kv.m_key);
m.inc_ref(kv.m_value);
}
for (obj_map<func_decl, func_decl*>::iterator it = conv.m_uf2bvuf.begin();
it != conv.m_uf2bvuf.end();
it++)
{
m_uf2bvuf.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
m.inc_ref(it->m_value);
for (auto const& kv : conv.m_uf2bvuf) {
m_uf2bvuf.insert(kv.m_key, kv.m_value);
m.inc_ref(kv.m_key);
m.inc_ref(kv.m_value);
}
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = conv.m_min_max_ufs.begin();
it != conv.m_min_max_ufs.end();
it++) {
m_specials.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
m.inc_ref(it->m_value.first);
m.inc_ref(it->m_value.second);
for (auto const& kv : conv.m_min_max_ufs) {
m_specials.insert(kv.m_key, kv.m_value);
m.inc_ref(kv.m_key);
m.inc_ref(kv.m_value.first);
m.inc_ref(kv.m_value.second);
}
}

bv2fpa_converter::~bv2fpa_converter() {
dec_ref_map_key_values(m, m_const2bv);
dec_ref_map_key_values(m, m_rm_const2bv);
dec_ref_map_key_values(m, m_uf2bvuf);
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
it != m_specials.end();
it++) {
m.dec_ref(it->m_key);
m.dec_ref(it->m_value.first);
m.dec_ref(it->m_value.second);
for (auto const& kv : m_specials) {
m.dec_ref(kv.m_key);
m.dec_ref(kv.m_value.first);
m.dec_ref(kv.m_value.second);
}
}

Expand Down Expand Up @@ -313,12 +300,9 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
}

void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen) {
for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
it != m_const2bv.end();
it++)
{
func_decl * var = it->m_key;
app * val = to_app(it->m_value);
for (auto const& kv : m_const2bv) {
func_decl * var = kv.m_key;
app * val = to_app(kv.m_value);
SASSERT(m_fpa_util.is_float(var->get_range()));
SASSERT(var->get_range()->get_num_parameters() == 2);
unsigned ebits = m_fpa_util.get_ebits(var->get_range());
Expand Down Expand Up @@ -383,13 +367,10 @@ void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model
}

void bv2fpa_converter::convert_rm_consts(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen) {
for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
it != m_rm_const2bv.end();
it++)
{
func_decl * var = it->m_key;
for (auto const& kv : m_rm_const2bv) {
func_decl * var = kv.m_key;
SASSERT(m_fpa_util.is_rm(var->get_range()));
expr * val = it->m_value;
expr * val = kv.m_value;
SASSERT(m_fpa_util.is_bv2rm(val));
expr * bvval = to_app(val)->get_arg(0);
expr_ref fv = convert_bv2rm(mc, to_app(bvval));
Expand All @@ -400,12 +381,10 @@ void bv2fpa_converter::convert_rm_consts(model_core * mc, model_core * target_mo
}

void bv2fpa_converter::convert_min_max_specials(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen) {
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
it != m_specials.end();
it++) {
func_decl * f = it->m_key;
app * pn_cnst = it->m_value.first;
app * np_cnst = it->m_value.second;
for (auto const& kv : m_specials) {
func_decl * f = kv.m_key;
app * pn_cnst = kv.m_value.first;
app * np_cnst = kv.m_value.second;

expr_ref pzero(m), nzero(m);
pzero = m_fpa_util.mk_pzero(f->get_range());
Expand Down Expand Up @@ -434,17 +413,16 @@ void bv2fpa_converter::convert_min_max_specials(model_core * mc, model_core * ta
}

void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen) {
for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
it != m_uf2bvuf.end();
it++) {
seen.insert(it->m_value);
for (auto const& kv : m_uf2bvuf) {
seen.insert(kv.m_value);

func_decl * f = it->m_key;
func_decl * f = kv.m_key;
std::cout << f->get_name() << "\n";
if (f->get_arity() == 0)
{
array_util au(m);
if (au.is_array(f->get_range())) {
array_model am = convert_array_func_interp(mc, f, it->m_value);
array_model am = convert_array_func_interp(mc, f, kv.m_value);
if (am.new_float_fd) target_model->register_decl(am.new_float_fd, am.new_float_fi);
if (am.result) target_model->register_decl(f, am.result);
if (am.bv_fd) seen.insert(am.bv_fd);
Expand All @@ -453,92 +431,82 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode
// Just keep.
SASSERT(!m_fpa_util.is_float(f->get_range()) && !m_fpa_util.is_rm(f->get_range()));
expr_ref val(m);
if (mc->eval(it->m_value, val))
if (mc->eval(kv.m_value, val))
target_model->register_decl(f, val);
}
}
else {
if (it->get_key().get_family_id() == m_fpa_util.get_fid()) {
// it->m_value contains the model for the unspecified cases of it->m_key.
target_model->register_decl(f, convert_func_interp(mc, f, it->m_value));
}
else if (f->get_family_id() == m_fpa_util.get_fid()) {

// kv.m_value contains the model for the unspecified cases of kv.m_key.
// TBD: instead of mapping the interpretation of f to just the graph for the
// uninterpreted case, map it to a condition, ite, that filters out the
// pre-condition for which argument combinations are interpreted vs. uninterpreted.
// if (m_fpa_util.is_to_ieee_bv(f)) {
// }
// if (m_fpa_util.is_to_sbv(f)) {
// }


target_model->register_decl(f, convert_func_interp(mc, f, kv.m_value));
}
}
}

void bv2fpa_converter::display(std::ostream & out) {
for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
it != m_const2bv.end();
it++) {
const symbol & n = it->m_key->get_name();
for (auto const& kv : m_const2bv) {
const symbol & n = kv.m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
out << mk_ismt2_pp(it->m_value, m, indent) << ")";
out << mk_ismt2_pp(kv.m_value, m, indent) << ")";
}
for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
it != m_rm_const2bv.end();
it++) {
const symbol & n = it->m_key->get_name();
for (auto const& kv : m_rm_const2bv) {
const symbol & n = kv.m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
out << mk_ismt2_pp(it->m_value, m, indent) << ")";
out << mk_ismt2_pp(kv.m_value, m, indent) << ")";
}
for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
it != m_uf2bvuf.end();
it++) {
const symbol & n = it->m_key->get_name();
for (auto const& kv : m_uf2bvuf) {
const symbol & n = kv.m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
out << mk_ismt2_pp(it->m_value, m, indent) << ")";
out << mk_ismt2_pp(kv.m_value, m, indent) << ")";
}
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
it != m_specials.end();
it++) {
const symbol & n = it->m_key->get_name();
for (auto const& kv : m_specials) {
const symbol & n = kv.m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
out << mk_ismt2_pp(it->m_value.first, m, indent) << "; " <<
mk_ismt2_pp(it->m_value.second, m, indent) << ")";
out << mk_ismt2_pp(kv.m_value.first, m, indent) << "; " <<
mk_ismt2_pp(kv.m_value.second, m, indent) << ")";
}
}

bv2fpa_converter * bv2fpa_converter::translate(ast_translation & translator) {
bv2fpa_converter * res = alloc(bv2fpa_converter, translator.to());
for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
it != m_const2bv.end();
it++)
{
func_decl * k = translator(it->m_key);
expr * v = translator(it->m_value);
for (auto const& kv : m_const2bv) {
func_decl * k = translator(kv.m_key);
expr * v = translator(kv.m_value);
res->m_const2bv.insert(k, v);
translator.to().inc_ref(k);
translator.to().inc_ref(v);
}
for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
it != m_rm_const2bv.end();
it++)
{
func_decl * k = translator(it->m_key);
expr * v = translator(it->m_value);
for (auto const& kv : m_rm_const2bv) {
func_decl * k = translator(kv.m_key);
expr * v = translator(kv.m_value);
res->m_rm_const2bv.insert(k, v);
translator.to().inc_ref(k);
translator.to().inc_ref(v);
}
for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
it != m_uf2bvuf.end();
it++) {
func_decl * k = translator(it->m_key);
func_decl * v = translator(it->m_value);
for (auto const& kv : m_uf2bvuf) {
func_decl * k = translator(kv.m_key);
func_decl * v = translator(kv.m_value);
res->m_uf2bvuf.insert(k, v);
translator.to().inc_ref(k);
translator.to().inc_ref(v);
}
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
it != m_specials.end();
it++) {
func_decl * k = translator(it->m_key);
app * v1 = translator(it->m_value.first);
app * v2 = translator(it->m_value.second);
for (auto const& kv : m_specials) {
func_decl * k = translator(kv.m_key);
app * v1 = translator(kv.m_value.first);
app * v2 = translator(kv.m_value.second);
res->m_specials.insert(k, std::pair<app*, app*>(v1, v2));
translator.to().inc_ref(k);
translator.to().inc_ref(v1);
Expand Down
10 changes: 4 additions & 6 deletions src/ast/fpa/fpa2bv_converter.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4174,12 +4174,10 @@ void fpa2bv_converter::reset() {
dec_ref_map_key_values(m, m_const2bv);
dec_ref_map_key_values(m, m_rm_const2bv);
dec_ref_map_key_values(m, m_uf2bvuf);
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_min_max_ufs.begin();
it != m_min_max_ufs.end();
it++) {
m.dec_ref(it->m_key);
m.dec_ref(it->m_value.first);
m.dec_ref(it->m_value.second);
for (auto const& kv : m_min_max_ufs) {
m.dec_ref(kv.m_key);
m.dec_ref(kv.m_value.first);
m.dec_ref(kv.m_value.second);
}
m_min_max_ufs.reset();
m_extra_assertions.reset();
Expand Down
1 change: 1 addition & 0 deletions src/ast/fpa_decl_plugin.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -354,6 +354,7 @@ class fpa_util {
bool is_bv2rm(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_BV2RM; }
bool is_to_ubv(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_UBV; }
bool is_to_sbv(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_SBV; }
bool is_to_ieee_bv(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_IEEE_BV; }

bool contains_floats(ast * a);
};
Expand Down
74 changes: 74 additions & 0 deletions src/tactic/fd_solver/smtfd_solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1394,6 +1394,7 @@ namespace smtfd {
}
}
ap.global_check(core);

TRACE("smtfd", context.display(tout););
for (expr* f : context) {
IF_VERBOSE(10, verbose_stream() << "lemma: " << expr_ref(rep(f), m) << "\n");
Expand Down Expand Up @@ -1624,6 +1625,79 @@ namespace smtfd {
return l_undef;
}

#if 0

lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override {
init();
flush_assertions();
lbool r = l_undef;
expr_ref_vector core(m);
while (true) {
IF_VERBOSE(1, verbose_stream() << "(smtfd-check-sat " << m_stats.m_num_rounds << " " << m_stats.m_num_lemmas << " " << m_stats.m_num_mbqi << ")\n");
m_stats.m_num_rounds++;
checkpoint();

// phase 1: check sat of abs
r = check_abs(num_assumptions, assumptions);
if (r != l_true) {
break;
}

// phase 2: find prime implicate over FD (abstraction)
r = get_prime_implicate(num_assumptions, assumptions, core);
if (r != l_false) {
break;
}

// phase 3: check if prime implicate is really valid, or add theory lemmas until there is a theory core
r = refine_core(core);
if (r != l_false) {
break;
}
assert_fd(m.mk_not(mk_and(abs(core))));
}
return r;
}

lbool refine_core(expr_ref_vector & core) {
plugin_context context(m_abs, m, UINT_MAX);
a_plugin ap(context, m_model);
uf_plugin uf(context, m_model);

lbool r = l_undef;
unsigned max_rounds = std::max(ap.max_rounds(), uf.max_rounds());
for (unsigned round = 0; round < max_rounds; ++round) {
for (expr* t : subterms(core)) {
ap.check_term(t, round);
uf.check_term(t, round);
}
r = refine_core(context, core);
if (r != l_true) {
return r;
}
}
ap.global_check(core);
r = refine_core(context, core);
if (r != l_true) {
return r;
}

// m_stats.m_num_lemmas += number of literals that are not from original core;

return l_undef;
}

lbool refine_core(plugin_context& context, expr_ref_vector& core) {
// add theory axioms to core
// check sat
// return unsat cores if unsat
// update m_model by checking satisfiability after round
return l_undef;
}

#endif


void updt_params(params_ref const & p) override {
::solver::updt_params(p);
if (m_fd_sat_solver) {
Expand Down

0 comments on commit ce06cd0

Please sign in to comment.