mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

#5324

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-06 16:23:27 -07:00
parent 9afc59d5b4
commit 34fc0cdd5c
4 changed files with 53 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/sat/smt/euf_solver.cpp
View file

@ -332,10 +332,10 @@ namespace euf {
propagated1 = true;
}
for (auto* s : m_solvers) {
if (s->unit_propagate())
for (unsigned i = 0; i < m_solvers.size(); ++i)
if (m_solvers[i]->unit_propagate())
propagated1 = true;
}
if (!propagated1)
break;
propagated = true;

68
src/sat/smt/fpa_solver.cpp
View file

@ -122,6 +122,50 @@ namespace fpa {
n = mk_enode(e, false);
SASSERT(!n->is_attached_to(get_id()));
mk_var(n);
TRACE("fp", tout << "post: " << mk_bounded_pp(e, m) << "\n";);
m_nodes.push_back(std::tuple(n, sign, root));
ctx.push(push_back_trail(m_nodes));
return true;
}
void solver::apply_sort_cnstr(enode* n, sort* s) {
TRACE("t_fpa", tout << "apply sort cnstr for: " << mk_ismt2_pp(n->get_expr(), m) << "\n";);
SASSERT(s->get_family_id() == get_id());
SASSERT(m_fpa_util.is_float(s) || m_fpa_util.is_rm(s));
SASSERT(m_fpa_util.is_float(n->get_expr()) || m_fpa_util.is_rm(n->get_expr()));
SASSERT(n->get_decl()->get_range() == s);
if (is_attached_to_var(n))
return;
attach_new_th_var(n);
expr* owner = n->get_expr();
if (m_fpa_util.is_rm(s) && !m_fpa_util.is_bv2rm(owner)) {
// For every RM term, we need to make sure that it's
// associated bit-vector is within the valid range.
expr_ref valid(m), limit(m);
limit = m_bv_util.mk_numeral(4, 3);
valid = m_bv_util.mk_ule(m_converter.wrap(owner), limit);
add_unit(mk_literal(valid));
}
activate(owner);
}
bool solver::unit_propagate() {
if (m_nodes.size() <= m_nodes_qhead)
return false;
ctx.push(value_trail<unsigned>(m_nodes_qhead));
for (; m_nodes_qhead < m_nodes.size(); ++m_nodes_qhead)
unit_propagate(m_nodes[m_nodes_qhead]);
return true;
}
void solver::unit_propagate(std::tuple<enode*, bool, bool> const& t) {
auto [n, sign, root] = t;
expr* e = n->get_expr();
app* a = to_app(e);
if (m.is_bool(e)) {
sat::literal atom(ctx.get_si().add_bool_var(e), false);
atom = ctx.attach_lit(atom, e);
@ -151,31 +195,7 @@ namespace fpa {
break;
}
}
return true;
}
void solver::apply_sort_cnstr(enode* n, sort* s) {
TRACE("t_fpa", tout << "apply sort cnstr for: " << mk_ismt2_pp(n->get_expr(), m) << "\n";);
SASSERT(s->get_family_id() == get_id());
SASSERT(m_fpa_util.is_float(s) || m_fpa_util.is_rm(s));
SASSERT(m_fpa_util.is_float(n->get_expr()) || m_fpa_util.is_rm(n->get_expr()));
SASSERT(n->get_decl()->get_range() == s);
if (is_attached_to_var(n))
return;
attach_new_th_var(n);
expr* owner = n->get_expr();
if (m_fpa_util.is_rm(s) && !m_fpa_util.is_bv2rm(owner)) {
// For every RM term, we need to make sure that it's
// associated bit-vector is within the valid range.
expr_ref valid(m), limit(m);
limit = m_bv_util.mk_numeral(4, 3);
valid = m_bv_util.mk_ule(m_converter.wrap(owner), limit);
add_unit(mk_literal(valid));
}
activate(owner);
}
void solver::activate(expr* n) {

5
src/sat/smt/fpa_solver.h
View file

@ -36,6 +36,8 @@ namespace fpa {
bv_util & m_bv_util;
arith_util & m_arith_util;
obj_map<expr, expr*> m_conversions;
svector<std::tuple<enode*, bool, bool>> m_nodes;
unsigned m_nodes_qhead = 0;
bool visit(expr* e) override;
bool visited(expr* e) override;
@ -45,6 +47,7 @@ namespace fpa {
sat::literal_vector mk_side_conditions();
void attach_new_th_var(enode* n);
void activate(expr* e);
void unit_propagate(std::tuple<enode*, bool, bool> const& t);
void ensure_equality_relation(theory_var x, theory_var y);
public:
@ -67,7 +70,7 @@ namespace fpa {
bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
void finalize_model(model& mdl) override;
bool unit_propagate() override { return false; }
bool unit_propagate() override;
void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override { UNREACHABLE(); }
sat::check_result check() override { return sat::check_result::CR_DONE; }

4
src/sat/tactic/goal2sat.cpp
View file

@ -744,7 +744,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
};
void process(expr* n, bool is_root, bool redundant) {
TRACE("goal2sat", tout << "process-begin " << mk_bounded_pp(n, m, 3)
TRACE("goal2sat", tout << "process-begin " << mk_bounded_pp(n, m, 2)
<< " root: " << is_root
<< " result-stack: " << m_result_stack.size()
<< " frame-stack: " << m_frame_stack.size() << "\n";);
@ -784,7 +784,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
m_frame_stack[fsz - 1].m_idx++;
if (!visit(arg, false, false))
goto loop;
TRACE("goal2sat_bug", tout << "visit " << mk_bounded_pp(t, m, 2) << " result stack: " << m_result_stack.size() << "\n";);
TRACE("goal2sat_bug", tout << "visit " << mk_bounded_pp(arg, m, 2) << " result stack: " << m_result_stack.size() << "\n";);
}
TRACE("goal2sat_bug", tout << "converting\n";
tout << mk_bounded_pp(t, m, 2) << " root: " << root << " sign: " << sign << "\n";