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

Merge pull request #5525 from Z3Prover/polysat-pull

Browse source 
remove scoped
This commit is contained in:
Jakob Rath 2021-09-01 09:37:50 +02:00 • committed by GitHub
commit 8b374c3745
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
11 changed files with 51 additions and 121 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/clause_builder.cpp
View file

@ -52,13 +52,13 @@ namespace polysat {
m_literals.push_back(lit);
}
void clause_builder::push_new_constraint(scoped_signed_constraint c) {
void clause_builder::push_new_constraint(signed_constraint c) {
SASSERT(c);
if (c.is_always_false())
return;
m_level = std::max(m_level, c->level());
m_literals.push_back(c.blit());
m_new_constraints.push_back(c.detach());
m_new_constraints.push_back(c.get());
}
}

2
src/math/polysat/clause_builder.h
View file

@ -47,7 +47,7 @@ namespace polysat {
void push_literal(sat::literal lit);
/// Add a constraint to the clause that does not yet exist in the solver so far.
void push_new_constraint(scoped_signed_constraint c);
void push_new_constraint(signed_constraint c);
};
}

14
src/math/polysat/constraint.cpp
View file

@ -21,8 +21,8 @@ Author:
namespace polysat {
static_assert(!std::is_copy_assignable_v<scoped_signed_constraint>);
static_assert(!std::is_copy_constructible_v<scoped_signed_constraint>);
//static_assert(!std::is_copy_assignable_v<scoped_signed_constraint>);
//static_assert(!std::is_copy_constructible_v<scoped_signed_constraint>);
void constraint_manager::assign_bv2c(sat::bool_var bv, constraint* c) {
SASSERT_EQ(get_bv2c(bv), nullptr);
@ -185,15 +185,15 @@ namespace polysat {
return true;
}
scoped_signed_constraint constraint_manager::eq(unsigned lvl, pdd const& p) {
signed_constraint constraint_manager::eq(unsigned lvl, pdd const& p) {
return {dedup(alloc(eq_constraint, *this, lvl, p)), true};
}
scoped_signed_constraint constraint_manager::ule(unsigned lvl, pdd const& a, pdd const& b) {
signed_constraint constraint_manager::ule(unsigned lvl, pdd const& a, pdd const& b) {
return {dedup(alloc(ule_constraint, *this, lvl, a, b)), true};
}
scoped_signed_constraint constraint_manager::ult(unsigned lvl, pdd const& a, pdd const& b) {
signed_constraint constraint_manager::ult(unsigned lvl, pdd const& a, pdd const& b) {
// a < b <=> !(b <= a)
return ~ule(lvl, b, a);
}
@ -214,12 +214,12 @@ namespace polysat {
//
// Argument: flipping the msb swaps the negative and non-negative blocks
//
scoped_signed_constraint constraint_manager::sle(unsigned lvl, pdd const& a, pdd const& b) {
signed_constraint constraint_manager::sle(unsigned lvl, pdd const& a, pdd const& b) {
auto shift = rational::power_of_two(a.power_of_2() - 1);
return ule(lvl, a + shift, b + shift);
}
scoped_signed_constraint constraint_manager::slt(unsigned lvl, pdd const& a, pdd const& b) {
signed_constraint constraint_manager::slt(unsigned lvl, pdd const& a, pdd const& b) {
auto shift = rational::power_of_two(a.power_of_2() - 1);
return ult(lvl, a + shift, b + shift);
}

104
src/math/polysat/constraint.h
View file

@ -28,13 +28,8 @@ namespace polysat {
class constraint;
class eq_constraint;
class ule_constraint;
class signed_constraint;
class scoped_constraint_ptr;
template <bool is_owned>
class signed_constraint_base;
using signed_constraint = signed_constraint_base<false>;
using scoped_signed_constraint = signed_constraint_base<true>;
class clause;
using clause_ref = ref<clause>;
@ -96,11 +91,11 @@ namespace polysat {
signed_constraint lookup(sat::literal lit) const;
constraint* lookup_external(unsigned dep) const { return m_external_constraints.get(dep, nullptr); }
scoped_signed_constraint eq(unsigned lvl, pdd const& p);
scoped_signed_constraint ule(unsigned lvl, pdd const& a, pdd const& b);
scoped_signed_constraint ult(unsigned lvl, pdd const& a, pdd const& b);
scoped_signed_constraint sle(unsigned lvl, pdd const& a, pdd const& b);
scoped_signed_constraint slt(unsigned lvl, pdd const& a, pdd const& b);
signed_constraint eq(unsigned lvl, pdd const& p);
signed_constraint ule(unsigned lvl, pdd const& a, pdd const& b);
signed_constraint ult(unsigned lvl, pdd const& a, pdd const& b);
signed_constraint sle(unsigned lvl, pdd const& a, pdd const& b);
signed_constraint slt(unsigned lvl, pdd const& a, pdd const& b);
};
@ -183,82 +178,25 @@ namespace polysat {
* \returns True iff a forbidden interval exists and the output parameters were set.
*/
// TODO: we can probably remove this and unify the implementations for both cases by relying on as_inequality().
virtual bool forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, scoped_signed_constraint& out_neg_cond) { return false; }
virtual bool forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond) { return false; }
};
inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }
// Like scoped_ptr<constraint>, but only deallocates the constraint if it is temporary (i.e., does not have a boolean variable).
// This is needed because when a constraint is created, due to deduplication, we might get either a new constraint or an existing one.
// (We want early deduplication because otherwise we might overlook possible boolean resolutions during conflict resolution.)
// (TODO: we could replace this class by std::unique_ptr with a custom deleter)
class scoped_constraint_ptr {
constraint* m_ptr;
void dealloc_ptr() const {
if (m_ptr && !m_ptr->has_bvar())
dealloc(m_ptr);
}
class signed_constraint final {
public:
scoped_constraint_ptr(constraint* ptr = nullptr): m_ptr(ptr) {}
scoped_constraint_ptr(scoped_constraint_ptr &&other) noexcept : m_ptr(nullptr) {
std::swap(m_ptr, other.m_ptr);
}
~scoped_constraint_ptr() {
dealloc_ptr();
}
scoped_constraint_ptr& operator=(scoped_constraint_ptr&& other) {
*this = other.detach();
return *this;
};
scoped_constraint_ptr& operator=(constraint* n) {
if (m_ptr != n) {
dealloc_ptr();
m_ptr = n;
}
return *this;
}
void swap(scoped_constraint_ptr& p) {
std::swap(m_ptr, p.m_ptr);
}
constraint* detach() {
constraint* tmp = m_ptr;
m_ptr = nullptr;
return tmp;
}
explicit operator bool() const { return !!m_ptr; }
bool operator!() const { return !m_ptr; }
constraint* get() const { return m_ptr; }
constraint* operator->() const { return m_ptr; }
const constraint& operator*() const { return *m_ptr; }
constraint &operator*() { return *m_ptr; }
};
template <bool is_owned>
class signed_constraint_base final {
public:
using ptr_t = std::conditional_t<is_owned, scoped_constraint_ptr, constraint*>;
using ptr_t = constraint*;
private:
ptr_t m_constraint = nullptr;
bool m_positive = true;
public:
signed_constraint_base() {}
signed_constraint_base(constraint* c, bool is_positive):
signed_constraint() {}
signed_constraint(constraint* c, bool is_positive):
m_constraint(c), m_positive(is_positive) {}
signed_constraint_base(constraint* c, sat::literal lit):
signed_constraint_base(c, !lit.sign()) {
signed_constraint(constraint* c, sat::literal lit):
signed_constraint(c, !lit.sign()) {
SASSERT_EQ(blit(), lit);
}
@ -279,10 +217,8 @@ namespace polysat {
sat::bool_var bvar() const { return m_constraint->bvar(); }
sat::literal blit() const { return sat::literal(bvar(), is_negative()); }
constraint* get() const { if constexpr (is_owned) return m_constraint.get(); else return m_constraint; }
signed_constraint get_signed() const { return {get(), m_positive}; }
template <bool Owned = is_owned>
std::enable_if_t<Owned, constraint*> detach() { return m_constraint.detach(); }
constraint* get() const { return m_constraint; }
explicit operator bool() const { return !!m_constraint; }
bool operator!() const { return !m_constraint; }
@ -290,9 +226,9 @@ namespace polysat {
constraint& operator*() { return *m_constraint; }
constraint const& operator*() const { return *m_constraint; }
signed_constraint_base<is_owned>& operator=(std::nullptr_t) { m_constraint = nullptr; return *this; }
signed_constraint& operator=(std::nullptr_t) { m_constraint = nullptr; return *this; }
bool operator==(signed_constraint_base<is_owned> const& other) const {
bool operator==(signed_constraint const& other) const {
return get() == other.get() && is_positive() == other.is_positive();
}
@ -304,8 +240,7 @@ namespace polysat {
}
};
template <bool is_owned>
inline std::ostream& operator<<(std::ostream& out, signed_constraint_base<is_owned> const& c) {
inline std::ostream& operator<<(std::ostream& out, signed_constraint const& c) {
return c.display(out);
}
@ -313,9 +248,6 @@ namespace polysat {
return {c.get(), !c.is_positive()};
}
inline scoped_signed_constraint operator~(scoped_signed_constraint&& c) {
return {c.detach(), !c.is_positive()};
}
/// Disjunction of constraints represented by boolean literals
// NB code review:

2
src/math/polysat/eq_constraint.cpp
View file

@ -121,7 +121,7 @@ namespace polysat {
/// Compute forbidden interval for equality constraint by considering it as p <=u 0 (or p >u 0 for disequality)
bool eq_constraint::forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, scoped_signed_constraint& out_neg_cond)
bool eq_constraint::forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond)
{
// Current only works when degree(v) is at most one
unsigned const deg = p().degree(v);

2
src/math/polysat/eq_constraint.h
View file

@ -31,7 +31,7 @@ namespace polysat {
bool is_currently_false(solver& s, bool is_positive) override;
bool is_currently_true(solver& s, bool is_positive) override;
void narrow(solver& s, bool is_positive) override;
bool forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, scoped_signed_constraint& out_neg_cond) override;
bool forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond) override;
inequality as_inequality(bool is_positive) const override;
unsigned hash() const override;
bool operator==(constraint const& other) const override;

8
src/math/polysat/forbidden_intervals.cpp
View file

@ -22,7 +22,7 @@ namespace polysat {
struct fi_record {
eval_interval interval;
scoped_signed_constraint neg_cond; // could be multiple constraints later
signed_constraint neg_cond; // could be multiple constraints later
signed_constraint src;
};
@ -74,7 +74,7 @@ namespace polysat {
for (signed_constraint c : conflict) {
LOG_H3("Computing forbidden interval for: " << c);
eval_interval interval = eval_interval::full();
scoped_signed_constraint neg_cond;
signed_constraint neg_cond;
if (c->forbidden_interval(s, c.is_positive(), v, interval, neg_cond)) {
LOG("interval: " << interval);
LOG("neg_cond: " << neg_cond);
@ -160,12 +160,12 @@ namespace polysat {
auto const& next_hi = records[next_i].interval.hi();
auto const& lhs = hi - next_lo;
auto const& rhs = next_hi - next_lo;
scoped_signed_constraint c = ~s.m_constraints.ult(lemma_lvl, lhs, rhs);
signed_constraint c = ~s.m_constraints.ult(lemma_lvl, lhs, rhs);
LOG("constraint: " << c);
clause.push_new_constraint(std::move(c));
// Side conditions
// TODO: check whether the condition is subsumed by c? maybe at the end do a "lemma reduction" step, to try and reduce branching?
scoped_signed_constraint& neg_cond = records[i].neg_cond;
signed_constraint& neg_cond = records[i].neg_cond;
if (neg_cond)
clause.push_new_constraint(std::move(neg_cond));
}

18
src/math/polysat/solver.cpp
View file

@ -114,36 +114,34 @@ namespace polysat {
m_free_vars.del_var_eh(v);
}
scoped_signed_constraint solver::mk_eq(pdd const& p) {
signed_constraint solver::mk_eq(pdd const& p) {
return m_constraints.eq(m_level, p);
}
scoped_signed_constraint solver::mk_diseq(pdd const& p) {
signed_constraint solver::mk_diseq(pdd const& p) {
return ~m_constraints.eq(m_level, p);
}
scoped_signed_constraint solver::mk_ule(pdd const& p, pdd const& q) {
signed_constraint solver::mk_ule(pdd const& p, pdd const& q) {
return m_constraints.ule(m_level, p, q);
}
scoped_signed_constraint solver::mk_ult(pdd const& p, pdd const& q) {
signed_constraint solver::mk_ult(pdd const& p, pdd const& q) {
return m_constraints.ult(m_level, p, q);
}
scoped_signed_constraint solver::mk_sle(pdd const& p, pdd const& q) {
signed_constraint solver::mk_sle(pdd const& p, pdd const& q) {
return m_constraints.sle(m_level, p, q);
}
scoped_signed_constraint solver::mk_slt(pdd const& p, pdd const& q) {
signed_constraint solver::mk_slt(pdd const& p, pdd const& q) {
return m_constraints.slt(m_level, p, q);
}
void solver::new_constraint(scoped_signed_constraint sc, unsigned dep, bool activate) {
void solver::new_constraint(signed_constraint c, unsigned dep, bool activate) {
VERIFY(at_base_level());
SASSERT(sc);
SASSERT(c);
SASSERT(activate || dep != null_dependency); // if we don't activate the constraint, we need the dependency to access it again later.
signed_constraint c = sc.get_signed();
sc.detach();
clause* unit = m_constraints.store(clause::from_unit(c, mk_dep_ref(dep)));
c->set_unit_clause(unit);
if (dep != null_dependency)

14
src/math/polysat/solver.h
View file

@ -219,13 +219,13 @@ namespace polysat {
void backjump(unsigned new_level);
void add_lemma(clause_ref lemma);
scoped_signed_constraint mk_eq(pdd const& p);
scoped_signed_constraint mk_diseq(pdd const& p);
scoped_signed_constraint mk_ule(pdd const& p, pdd const& q);
scoped_signed_constraint mk_ult(pdd const& p, pdd const& q);
scoped_signed_constraint mk_sle(pdd const& p, pdd const& q);
scoped_signed_constraint mk_slt(pdd const& p, pdd const& q);
void new_constraint(scoped_signed_constraint c, unsigned dep, bool activate);
signed_constraint mk_eq(pdd const& p);
signed_constraint mk_diseq(pdd const& p);
signed_constraint mk_ule(pdd const& p, pdd const& q);
signed_constraint mk_ult(pdd const& p, pdd const& q);
signed_constraint mk_sle(pdd const& p, pdd const& q);
signed_constraint mk_slt(pdd const& p, pdd const& q);
void new_constraint(signed_constraint c, unsigned dep, bool activate);
static void insert_constraint(signed_constraints& cs, signed_constraint c);
bool invariant();

2
src/math/polysat/ule_constraint.cpp
View file

@ -113,7 +113,7 @@ namespace polysat {
return p.is_val() && q.is_val() && p.val() > q.val();
}
bool ule_constraint::forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, scoped_signed_constraint& out_neg_cond)
bool ule_constraint::forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond)
{
// Current only works when degree(v) is at most one on both sides
unsigned const deg1 = lhs().degree(v);

2
src/math/polysat/ule_constraint.h
View file

@ -37,7 +37,7 @@ namespace polysat {
bool is_currently_false(solver& s, bool is_positive) override;
bool is_currently_true(solver& s, bool is_positive) override;
void narrow(solver& s, bool is_positive) override;
bool forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, scoped_signed_constraint& out_neg_cond) override;
bool forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond) override;
inequality as_inequality(bool is_positive) const override;
unsigned hash() const override;
bool operator==(constraint const& other) const override;