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

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-12 15:42:39 -08:00
parent 40e93d7478
commit 35eb95b447
7 changed files with 35 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -291,6 +291,26 @@ namespace euf {
}
}
void solver::get_eq_antecedents(enode* a, enode* b, literal_vector& r) {
m_egraph.begin_explain();
m_explain.reset();
m_egraph.explain_eq<size_t>(m_explain, nullptr, a, b);
for (unsigned qhead = 0; qhead < m_explain.size(); ++qhead) {
size_t* e = m_explain[qhead];
if (is_literal(e))
r.push_back(get_literal(e));
else {
size_t idx = get_justification(e);
auto* ext = sat::constraint_base::to_extension(idx);
SASSERT(ext != this);
sat::literal lit = sat::null_literal;
ext->get_antecedents(lit, idx, r, true);
}
}
m_egraph.end_explain();
}
void solver::get_th_antecedents(literal l, th_explain& jst, literal_vector& r, bool probing) {
for (auto lit : euf::th_explain::lits(jst))
r.push_back(lit);

1
src/sat/smt/euf_solver.h
View file

@ -369,6 +369,7 @@ namespace euf {
void flush_roots() override;
void get_antecedents(literal l, ext_justification_idx idx, literal_vector& r, bool probing) override;
void get_eq_antecedents(enode* a, enode* b, literal_vector& r);
void get_th_antecedents(literal l, th_explain& jst, literal_vector& r, bool probing);
void add_eq_antecedent(bool probing, enode* a, enode* b);
void explain_diseq(ptr_vector<size_t>& ex, cc_justification* cc, enode* a, enode* b);

2
src/sat/smt/intblast_solver.cpp
View file

@ -647,7 +647,7 @@ namespace intblast {
bv_rewriter_params p(ctx.s().params());
expr* x = arg(0), * y = umod(e, 1);
if (p.hi_div0())
r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(0), y));
r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(0), y);
else
r = a.mk_mod(x, y);
break;

9
src/sat/smt/polysat/core.cpp
View file

@ -149,13 +149,14 @@ namespace polysat {
m_var = m_var_queue.next_var();
s.trail().push(mk_dqueue_var(m_var, *this));
switch (m_viable.find_viable(m_var, m_value)) {
case find_t::empty:
s.set_lemma(m_viable.get_core(), 0, m_viable.explain());
// propagate_unsat_core();
case find_t::empty:
s.set_lemma(m_viable.get_core(), m_viable.explain());
// propagate_unsat_core();
return sat::check_result::CR_CONTINUE;
case find_t::singleton:
case find_t::singleton: {
s.propagate(m_constraints.eq(var2pdd(m_var), m_value), m_viable.explain());
return sat::check_result::CR_CONTINUE;
}
case find_t::multiple:
s.add_eq_literal(m_var, m_value);
return sat::check_result::CR_CONTINUE;

2
src/sat/smt/polysat/types.h
View file

@ -107,7 +107,7 @@ namespace polysat {
virtual ~solver_interface() {}
virtual void add_eq_literal(pvar v, rational const& val) = 0;
virtual void set_conflict(dependency_vector const& core) = 0;
virtual void set_lemma(core_vector const& aux_core, unsigned level, dependency_vector const& core) = 0;
virtual void set_lemma(core_vector const& aux_core, dependency_vector const& core) = 0;
virtual void add_polysat_clause(char const* name, core_vector cs, bool redundant) = 0;
virtual dependency propagate(signed_constraint sc, dependency_vector const& deps) = 0;
virtual void propagate(dependency const& d, bool sign, dependency_vector const& deps) = 0;

7
src/sat/smt/polysat_solver.cpp
View file

@ -130,8 +130,13 @@ namespace polysat {
return { core, eqs };
}
void solver::set_lemma(core_vector const& aux_core, unsigned level, dependency_vector const& core) {
void solver::set_lemma(core_vector const& aux_core, dependency_vector const& core) {
auto [lits, eqs] = explain_deps(core);
unsigned level = 0;
for (auto const& [n1, n2] : eqs)
ctx.get_eq_antecedents(n1, n2, lits);
for (auto lit : lits)
level = std::max(level, s().lvl(lit));
auto ex = euf::th_explain::conflict(*this, lits, eqs, nullptr);
ctx.push(value_trail<bool>(m_has_lemma));
m_has_lemma = true;

2
src/sat/smt/polysat_solver.h
View file

@ -144,7 +144,7 @@ namespace polysat {
// callbacks from core
void add_eq_literal(pvar v, rational const& val) override;
void set_conflict(dependency_vector const& core) override;
void set_lemma(core_vector const& aux_core, unsigned level, dependency_vector const& core) override;
void set_lemma(core_vector const& aux_core, dependency_vector const& core) override;
dependency propagate(signed_constraint sc, dependency_vector const& deps) override;
void propagate(dependency const& d, bool sign, dependency_vector const& deps) override;
trail_stack& trail() override;