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

n/a

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-07 20:53:04 -08:00
parent f3fa6fdb84
commit 8207732d27
4 changed files with 52 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/sat/smt/polysat_constraints.h
View file

@ -39,6 +39,16 @@ namespace polysat {
pdd m_lhs, m_rhs;
public:
ule_constraint(pdd const& lhs, pdd const& rhs) : m_lhs(lhs), m_rhs(rhs) {}
pdd const& lhs() const { return m_lhs; }
pdd const& rhs() const { return m_rhs; }
};
class umul_ovfl_constraint : public constraint {
pdd m_lhs, m_rhs;
public:
umul_ovfl_constraint(pdd const& lhs, pdd const& rhs) : m_lhs(lhs), m_rhs(rhs) {}
pdd const& lhs() const { return m_lhs; }
pdd const& rhs() const { return m_rhs; }
};
class signed_constraint {
@ -54,8 +64,12 @@ namespace polysat {
unsigned_vector const& vars() const { return m_constraint->vars(); }
unsigned var(unsigned idx) const { return m_constraint->var(idx); }
bool contains_var(pvar v) const { return m_constraint->contains_var(v); }
ckind_t op() const { return m_op; }
bool is_ule() const { return m_op == ule_t; }
ule_constraint& to_ule() { return *reinterpret_cast<ule_constraint*>(m_constraint); }
bool is_umul_ovfl() const { return m_op == umul_ovfl_t; }
bool is_smul_fl() const { return m_op == smul_fl_t; }
ule_constraint const& to_ule() const { return *reinterpret_cast<ule_constraint*>(m_constraint); }
umul_ovfl_constraint const& to_umul_ovfl() const { return *reinterpret_cast<umul_ovfl_constraint*>(m_constraint); }
bool is_eq(pvar& v, rational& val) { throw default_exception("nyi"); }
};

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

@ -102,8 +102,6 @@ namespace polysat {
bool propagate();
void assign_eh(unsigned idx, signed_constraint const& sc, dependency const& dep);
expr_ref constraint2expr(signed_constraint const& sc) const { throw default_exception("nyi"); }
pdd value(rational const& v, unsigned sz);
signed_constraint eq(pdd const& p) { return m_constraints.eq(p); }

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

@ -113,7 +113,7 @@ namespace polysat {
m_lemma_level = level;
m_lemma.reset();
for (auto sc : lemma)
m_lemma.push_back(m_core.constraint2expr(sc));
m_lemma.push_back(constraint2expr(sc));
ctx.set_conflict(ex);
}
@ -172,7 +172,7 @@ namespace polysat {
// The polysat::solver takes care of translating signed constraints into expressions, which translate into literals.
// Everything goes over expressions/literals. polysat::core is not responsible for replaying expressions.
void solver::propagate(signed_constraint sc, dependency_vector const& deps) {
sat::literal lit = ctx.mk_literal(m_core.constraint2expr(sc));
sat::literal lit = ctx.mk_literal(constraint2expr(sc));
auto [core, eqs] = explain_deps(deps);
auto ex = euf::th_explain::propagate(*this, core, eqs, lit, nullptr);
ctx.propagate(lit, ex);
@ -200,7 +200,7 @@ namespace polysat {
void solver::add_lemma(vector<signed_constraint> const& lemma) {
sat::literal_vector lits;
for (auto sc : lemma)
lits.push_back(ctx.mk_literal(m_core.constraint2expr(sc)));
lits.push_back(ctx.mk_literal(constraint2expr(sc)));
s().add_clause(lits.size(), lits.data(), sat::status::th(true, get_id(), nullptr));
}
@ -209,4 +209,35 @@ namespace polysat {
ctx.get_th_antecedents(l, jst, r, probing);
}
expr_ref solver::constraint2expr(signed_constraint const& sc) {
switch (sc.op()) {
case ckind_t::ule_t: {
auto l = pdd2expr(sc.to_ule().lhs());
auto h = pdd2expr(sc.to_ule().rhs());
return expr_ref(bv.mk_ule(l, h), m);
}
case ckind_t::umul_ovfl_t: {
auto l = pdd2expr(sc.to_umul_ovfl().lhs());
auto r = pdd2expr(sc.to_umul_ovfl().rhs());
return expr_ref(bv.mk_bvumul_ovfl(l, r), m);
}
case ckind_t::smul_fl_t:
case ckind_t::op_t:
break;
}
throw default_exception("nyi");
}
expr_ref solver::pdd2expr(pdd const& p) {
if (p.is_val()) {
expr* n = bv.mk_numeral(p.val(), p.power_of_2());
return expr_ref(n, m);
}
auto lo = pdd2expr(p.lo());
auto hi = pdd2expr(p.hi());
auto v = var2enode(m_pddvar2var[p.var()]);
hi = bv.mk_bv_mul(v->get_expr(), hi);
return expr_ref(bv.mk_bv_add(lo, hi), m);
}
}

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

@ -139,6 +139,9 @@ namespace polysat {
void add_lemma(vector<signed_constraint> const& lemma);
std::pair<sat::literal_vector, euf::enode_pair_vector> explain_deps(dependency_vector const& deps);
expr_ref constraint2expr(signed_constraint const& sc);
expr_ref pdd2expr(pdd const& p);
public:
solver(euf::solver& ctx, theory_id id);