mirror of
https://github.com/Z3Prover/z3
synced 2025-08-22 19:17:53 +00:00
reorganize polysat functionality to use abstract solver interface
make dependency be self-contained
This commit is contained in:
Nikolaj Bjorner
parent
837e111d93
commit
81c6f00c99
23 changed files with 381 additions and 123 deletions
15
src/sat/smt/polysat/CMakeLists.txt
Normal file
15
src/sat/smt/polysat/CMakeLists.txt
Normal file
|
|
@ -0,0 +1,15 @@
|
|||
z3_add_component(polysat
|
||||
SOURCES
|
||||
polysat_assignment.cpp
|
||||
polysat_constraints.cpp
|
||||
polysat_core.cpp
|
||||
polysat_fi.cpp
|
||||
polysat_ule.cpp
|
||||
polysat_umul_ovfl.cpp
|
||||
polysat_viable.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
util
|
||||
dd
|
||||
smt_params
|
||||
)
|
||||
|
||||
119
src/sat/smt/polysat/polysat_assignment.cpp
Normal file
119
src/sat/smt/polysat/polysat_assignment.cpp
Normal file
|
|
@ -0,0 +1,119 @@
|
|||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
polysat substitution and assignment
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-06
|
||||
|
||||
--*/
|
||||
|
||||
#include "sat/smt/polysat/polysat_assignment.h"
|
||||
#include "sat/smt/polysat/polysat_core.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
substitution::substitution(pdd p)
|
||||
: m_subst(std::move(p)) { }
|
||||
|
||||
substitution::substitution(dd::pdd_manager& m)
|
||||
: m_subst(m.one()) { }
|
||||
|
||||
substitution substitution::add(pvar var, rational const& value) const {
|
||||
return {m_subst.subst_add(var, value)};
|
||||
}
|
||||
|
||||
pdd substitution::apply_to(pdd const& p) const {
|
||||
return p.subst_val(m_subst);
|
||||
}
|
||||
|
||||
bool substitution::contains(pvar var) const {
|
||||
rational out_value;
|
||||
return value(var, out_value);
|
||||
}
|
||||
|
||||
bool substitution::value(pvar var, rational& out_value) const {
|
||||
return m_subst.subst_get(var, out_value);
|
||||
}
|
||||
|
||||
assignment::assignment(core& s)
|
||||
: m_core(s) { }
|
||||
|
||||
|
||||
assignment assignment::clone() const {
|
||||
assignment a(s());
|
||||
a.m_pairs = m_pairs;
|
||||
a.m_subst.reserve(m_subst.size());
|
||||
for (unsigned i = m_subst.size(); i-- > 0; )
|
||||
if (m_subst[i])
|
||||
a.m_subst.set(i, alloc(substitution, *m_subst[i]));
|
||||
a.m_subst_trail = m_subst_trail;
|
||||
return a;
|
||||
}
|
||||
|
||||
bool assignment::contains(pvar var) const {
|
||||
return subst(s().size(var)).contains(var);
|
||||
}
|
||||
|
||||
bool assignment::value(pvar var, rational& out_value) const {
|
||||
return subst(s().size(var)).value(var, out_value);
|
||||
}
|
||||
|
||||
substitution& assignment::subst(unsigned sz) {
|
||||
return const_cast<substitution&>(std::as_const(*this).subst(sz));
|
||||
}
|
||||
|
||||
substitution const& assignment::subst(unsigned sz) const {
|
||||
m_subst.reserve(sz + 1);
|
||||
if (!m_subst[sz])
|
||||
m_subst.set(sz, alloc(substitution, s().sz2pdd(sz)));
|
||||
return *m_subst[sz];
|
||||
}
|
||||
|
||||
void assignment::push(pvar var, rational const& value) {
|
||||
SASSERT(all_of(m_pairs, [var](assignment_item_t const& item) { return item.first != var; }));
|
||||
m_pairs.push_back({var, value});
|
||||
unsigned const sz = s().size(var);
|
||||
substitution& sub = subst(sz);
|
||||
m_subst_trail.push_back(sub);
|
||||
sub = sub.add(var, value);
|
||||
SASSERT_EQ(sub, *m_subst[sz]);
|
||||
}
|
||||
|
||||
void assignment::pop() {
|
||||
substitution& sub = m_subst_trail.back();
|
||||
unsigned sz = sub.bit_width();
|
||||
SASSERT_EQ(sz, s().size(m_pairs.back().first));
|
||||
*m_subst[sz] = sub;
|
||||
m_subst_trail.pop_back();
|
||||
m_pairs.pop_back();
|
||||
}
|
||||
|
||||
pdd assignment::apply_to(pdd const& p) const {
|
||||
unsigned const sz = p.power_of_2();
|
||||
return subst(sz).apply_to(p);
|
||||
}
|
||||
|
||||
std::ostream& substitution::display(std::ostream& out) const {
|
||||
char const* delim = "";
|
||||
pdd p = m_subst;
|
||||
while (!p.is_val()) {
|
||||
SASSERT(p.lo().is_val());
|
||||
out << delim << "v" << p.var() << " := " << p.lo();
|
||||
delim = " ";
|
||||
p = p.hi();
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& assignment::display(std::ostream& out) const {
|
||||
char const* delim = "";
|
||||
for (auto const& [var, value] : m_pairs)
|
||||
out << delim << var << " == " << value, delim = " ";
|
||||
return out;
|
||||
}
|
||||
}
|
||||
120
src/sat/smt/polysat/polysat_assignment.h
Normal file
120
src/sat/smt/polysat/polysat_assignment.h
Normal file
|
|
@ -0,0 +1,120 @@
|
|||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
polysat substitution and assignment
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-06
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
#include "util/scoped_ptr_vector.h"
|
||||
#include "sat/smt/polysat/polysat_types.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
class core;
|
||||
|
||||
using assignment_item_t = std::pair<pvar, rational>;
|
||||
|
||||
class substitution_iterator {
|
||||
pdd m_current;
|
||||
substitution_iterator(pdd current) : m_current(std::move(current)) {}
|
||||
friend class substitution;
|
||||
|
||||
public:
|
||||
using value_type = assignment_item_t;
|
||||
using difference_type = std::ptrdiff_t;
|
||||
using pointer = value_type const*;
|
||||
using reference = value_type const&;
|
||||
using iterator_category = std::input_iterator_tag;
|
||||
|
||||
substitution_iterator& operator++() {
|
||||
SASSERT(!m_current.is_val());
|
||||
m_current = m_current.hi();
|
||||
return *this;
|
||||
}
|
||||
|
||||
value_type operator*() const {
|
||||
SASSERT(!m_current.is_val());
|
||||
return { m_current.var(), m_current.lo().val() };
|
||||
}
|
||||
|
||||
bool operator==(substitution_iterator const& other) const { return m_current == other.m_current; }
|
||||
bool operator!=(substitution_iterator const& other) const { return !operator==(other); }
|
||||
};
|
||||
|
||||
/** Substitution for a single bit width. */
|
||||
class substitution {
|
||||
pdd m_subst;
|
||||
|
||||
substitution(pdd p);
|
||||
|
||||
public:
|
||||
substitution(dd::pdd_manager& m);
|
||||
[[nodiscard]] substitution add(pvar var, rational const& value) const;
|
||||
[[nodiscard]] pdd apply_to(pdd const& p) const;
|
||||
|
||||
[[nodiscard]] bool contains(pvar var) const;
|
||||
[[nodiscard]] bool value(pvar var, rational& out_value) const;
|
||||
|
||||
[[nodiscard]] bool empty() const { return m_subst.is_one(); }
|
||||
|
||||
pdd const& to_pdd() const { return m_subst; }
|
||||
unsigned bit_width() const { return to_pdd().power_of_2(); }
|
||||
|
||||
bool operator==(substitution const& other) const { return &m_subst.manager() == &other.m_subst.manager() && m_subst == other.m_subst; }
|
||||
bool operator!=(substitution const& other) const { return !operator==(other); }
|
||||
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
|
||||
using const_iterator = substitution_iterator;
|
||||
const_iterator begin() const { return {m_subst}; }
|
||||
const_iterator end() const { return {m_subst.manager().one()}; }
|
||||
};
|
||||
|
||||
/** Full variable assignment, may include variables of varying bit widths. */
|
||||
class assignment {
|
||||
core& m_core;
|
||||
vector<assignment_item_t> m_pairs;
|
||||
mutable scoped_ptr_vector<substitution> m_subst;
|
||||
vector<substitution> m_subst_trail;
|
||||
|
||||
substitution& subst(unsigned sz);
|
||||
core& s() const { return m_core; }
|
||||
public:
|
||||
assignment(core& s);
|
||||
// prevent implicit copy, use clone() if you do need a copy
|
||||
assignment(assignment const&) = delete;
|
||||
assignment& operator=(assignment const&) = delete;
|
||||
assignment(assignment&&) = default;
|
||||
assignment& operator=(assignment&&) = default;
|
||||
assignment clone() const;
|
||||
|
||||
void push(pvar var, rational const& value);
|
||||
void pop();
|
||||
|
||||
pdd apply_to(pdd const& p) const;
|
||||
|
||||
bool contains(pvar var) const;
|
||||
bool value(pvar var, rational& out_value) const;
|
||||
rational value(pvar var) const { rational val; VERIFY(value(var, val)); return val; }
|
||||
bool empty() const { return pairs().empty(); }
|
||||
substitution const& subst(unsigned sz) const;
|
||||
vector<assignment_item_t> const& pairs() const { return m_pairs; }
|
||||
using const_iterator = decltype(m_pairs)::const_iterator;
|
||||
const_iterator begin() const { return pairs().begin(); }
|
||||
const_iterator end() const { return pairs().end(); }
|
||||
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
};
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, substitution const& sub) { return sub.display(out); }
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, assignment const& a) { return a.display(out); }
|
||||
}
|
||||
|
||||
47
src/sat/smt/polysat/polysat_constraints.cpp
Normal file
47
src/sat/smt/polysat/polysat_constraints.cpp
Normal file
|
|
@ -0,0 +1,47 @@
|
|||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
polysat constraints
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-06
|
||||
|
||||
--*/
|
||||
|
||||
#include "sat/smt/polysat/polysat_core.h"
|
||||
#include "sat/smt/polysat/polysat_constraints.h"
|
||||
#include "sat/smt/polysat/polysat_ule.h"
|
||||
#include "sat/smt/polysat/polysat_umul_ovfl.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
signed_constraint constraints::ule(pdd const& p, pdd const& q) {
|
||||
pdd lhs = p, rhs = q;
|
||||
bool is_positive = true;
|
||||
ule_constraint::simplify(is_positive, lhs, rhs);
|
||||
auto* c = alloc(ule_constraint, p, q);
|
||||
m_trail.push(new_obj_trail(c));
|
||||
auto sc = signed_constraint(ckind_t::ule_t, c);
|
||||
return is_positive ? sc : ~sc;
|
||||
}
|
||||
|
||||
signed_constraint constraints::umul_ovfl(pdd const& p, pdd const& q) {
|
||||
auto* c = alloc(umul_ovfl_constraint, p, q);
|
||||
m_trail.push(new_obj_trail(c));
|
||||
return signed_constraint(ckind_t::umul_ovfl_t, c);
|
||||
}
|
||||
|
||||
lbool signed_constraint::eval(assignment& a) const {
|
||||
lbool r = m_constraint->eval(a);
|
||||
return m_sign ? ~r : r;
|
||||
}
|
||||
|
||||
std::ostream& signed_constraint::display(std::ostream& out) const {
|
||||
if (m_sign) out << "~";
|
||||
return out << *m_constraint;
|
||||
}
|
||||
}
|
||||
141
src/sat/smt/polysat/polysat_constraints.h
Normal file
141
src/sat/smt/polysat/polysat_constraints.h
Normal file
|
|
@ -0,0 +1,141 @@
|
|||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
polysat constraints
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-06
|
||||
|
||||
--*/
|
||||
|
||||
|
||||
#pragma once
|
||||
#include "util/trail.h"
|
||||
#include "sat/smt/polysat/polysat_types.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
class core;
|
||||
class ule_constraint;
|
||||
class umul_ovfl_constraint;
|
||||
class assignment;
|
||||
|
||||
using pdd = dd::pdd;
|
||||
using pvar = unsigned;
|
||||
|
||||
enum ckind_t { ule_t, umul_ovfl_t, smul_fl_t, op_t };
|
||||
|
||||
class constraint {
|
||||
unsigned_vector m_vars;
|
||||
public:
|
||||
virtual ~constraint() {}
|
||||
unsigned_vector& vars() { return m_vars; }
|
||||
unsigned_vector const& vars() const { return m_vars; }
|
||||
unsigned var(unsigned idx) const { return m_vars[idx]; }
|
||||
bool contains_var(pvar v) const { return m_vars.contains(v); }
|
||||
virtual std::ostream& display(std::ostream& out, lbool status) const = 0;
|
||||
virtual std::ostream& display(std::ostream& out) const = 0;
|
||||
virtual lbool eval() const = 0;
|
||||
virtual lbool eval(assignment const& a) const = 0;
|
||||
};
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }
|
||||
|
||||
|
||||
class signed_constraint {
|
||||
bool m_sign = false;
|
||||
ckind_t m_op = ule_t;
|
||||
constraint* m_constraint = nullptr;
|
||||
public:
|
||||
signed_constraint() {}
|
||||
signed_constraint(ckind_t c, constraint* p) : m_op(c), m_constraint(p) {}
|
||||
signed_constraint operator~() const { signed_constraint r(*this); r.m_sign = !r.m_sign; return r; }
|
||||
bool sign() const { return m_sign; }
|
||||
bool is_positive() const { return !m_sign; }
|
||||
bool is_negative() const { return m_sign; }
|
||||
unsigned_vector& vars() { return m_constraint->vars(); }
|
||||
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); }
|
||||
lbool eval(assignment& a) const;
|
||||
ckind_t op() const { return m_op; }
|
||||
bool is_ule() const { return m_op == ule_t; }
|
||||
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"); }
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
};
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, signed_constraint const& c) { return c.display(out); }
|
||||
|
||||
class constraints {
|
||||
trail_stack& m_trail;
|
||||
public:
|
||||
constraints(trail_stack& c) : m_trail(c) {}
|
||||
|
||||
signed_constraint eq(pdd const& p) { return ule(p, p.manager().mk_val(0)); }
|
||||
signed_constraint eq(pdd const& p, rational const& v) { return eq(p - p.manager().mk_val(v)); }
|
||||
signed_constraint ule(pdd const& p, pdd const& q);
|
||||
signed_constraint sle(pdd const& p, pdd const& q) { throw default_exception("nyi"); }
|
||||
signed_constraint ult(pdd const& p, pdd const& q) { throw default_exception("nyi"); }
|
||||
signed_constraint slt(pdd const& p, pdd const& q) { throw default_exception("nyi"); }
|
||||
signed_constraint umul_ovfl(pdd const& p, pdd const& q);
|
||||
signed_constraint smul_ovfl(pdd const& p, pdd const& q) { throw default_exception("nyi"); }
|
||||
signed_constraint smul_udfl(pdd const& p, pdd const& q) { throw default_exception("nyi"); }
|
||||
signed_constraint bit(pdd const& p, unsigned i) { throw default_exception("nyi"); }
|
||||
|
||||
signed_constraint diseq(pdd const& p) { return ~eq(p); }
|
||||
signed_constraint diseq(pdd const& p, pdd const& q) { return diseq(p - q); }
|
||||
signed_constraint diseq(pdd const& p, rational const& q) { return diseq(p - q); }
|
||||
signed_constraint diseq(pdd const& p, int q) { return diseq(p, rational(q)); }
|
||||
signed_constraint diseq(pdd const& p, unsigned q) { return diseq(p, rational(q)); }
|
||||
|
||||
signed_constraint ule(pdd const& p, rational const& q) { return ule(p, p.manager().mk_val(q)); }
|
||||
signed_constraint ule(rational const& p, pdd const& q) { return ule(q.manager().mk_val(p), q); }
|
||||
signed_constraint ule(pdd const& p, int q) { return ule(p, rational(q)); }
|
||||
signed_constraint ule(pdd const& p, unsigned q) { return ule(p, rational(q)); }
|
||||
signed_constraint ule(int p, pdd const& q) { return ule(rational(p), q); }
|
||||
signed_constraint ule(unsigned p, pdd const& q) { return ule(rational(p), q); }
|
||||
|
||||
signed_constraint uge(pdd const& p, pdd const& q) { return ule(q, p); }
|
||||
signed_constraint uge(pdd const& p, rational const& q) { return ule(q, p); }
|
||||
|
||||
signed_constraint ult(pdd const& p, rational const& q) { return ult(p, p.manager().mk_val(q)); }
|
||||
signed_constraint ult(rational const& p, pdd const& q) { return ult(q.manager().mk_val(p), q); }
|
||||
signed_constraint ult(int p, pdd const& q) { return ult(rational(p), q); }
|
||||
signed_constraint ult(unsigned p, pdd const& q) { return ult(rational(p), q); }
|
||||
signed_constraint ult(pdd const& p, int q) { return ult(p, rational(q)); }
|
||||
signed_constraint ult(pdd const& p, unsigned q) { return ult(p, rational(q)); }
|
||||
|
||||
signed_constraint slt(pdd const& p, rational const& q) { return slt(p, p.manager().mk_val(q)); }
|
||||
signed_constraint slt(rational const& p, pdd const& q) { return slt(q.manager().mk_val(p), q); }
|
||||
signed_constraint slt(pdd const& p, int q) { return slt(p, rational(q)); }
|
||||
signed_constraint slt(pdd const& p, unsigned q) { return slt(p, rational(q)); }
|
||||
signed_constraint slt(int p, pdd const& q) { return slt(rational(p), q); }
|
||||
signed_constraint slt(unsigned p, pdd const& q) { return slt(rational(p), q); }
|
||||
|
||||
|
||||
signed_constraint sgt(pdd const& p, pdd const& q) { return slt(q, p); }
|
||||
signed_constraint sgt(pdd const& p, int q) { return slt(q, p); }
|
||||
signed_constraint sgt(pdd const& p, unsigned q) { return slt(q, p); }
|
||||
signed_constraint sgt(int p, pdd const& q) { return slt(q, p); }
|
||||
signed_constraint sgt(unsigned p, pdd const& q) { return slt(q, p); }
|
||||
|
||||
signed_constraint umul_ovfl(pdd const& p, rational const& q) { return umul_ovfl(p, p.manager().mk_val(q)); }
|
||||
signed_constraint umul_ovfl(rational const& p, pdd const& q) { return umul_ovfl(q.manager().mk_val(p), q); }
|
||||
signed_constraint umul_ovfl(pdd const& p, int q) { return umul_ovfl(p, rational(q)); }
|
||||
signed_constraint umul_ovfl(pdd const& p, unsigned q) { return umul_ovfl(p, rational(q)); }
|
||||
signed_constraint umul_ovfl(int p, pdd const& q) { return umul_ovfl(rational(p), q); }
|
||||
signed_constraint umul_ovfl(unsigned p, pdd const& q) { return umul_ovfl(rational(p), q); }
|
||||
|
||||
|
||||
//signed_constraint even(pdd const& p) { return parity_at_least(p, 1); }
|
||||
//signed_constraint odd(pdd const& p) { return ~even(p); }
|
||||
};
|
||||
}
|
||||
314
src/sat/smt/polysat/polysat_core.cpp
Normal file
314
src/sat/smt/polysat/polysat_core.cpp
Normal file
|
|
@ -0,0 +1,314 @@
|
|||
/*++
|
||||
Copyright (c) 2022 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
polysat_core.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
PolySAT core functionality
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2022-01-26
|
||||
Jakob Rath 2021-04-06
|
||||
|
||||
Notes:
|
||||
|
||||
polysat::solver
|
||||
- adds assignments
|
||||
- calls propagation and check
|
||||
|
||||
polysat::core
|
||||
- propagates literals
|
||||
- crates case splits by value assignment (equalities)
|
||||
- detects conflicts based on Literal assignmets
|
||||
- adds lemmas based on projections
|
||||
|
||||
--*/
|
||||
|
||||
#include "params/bv_rewriter_params.hpp"
|
||||
#include "sat/smt/polysat/polysat_core.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
class core::mk_assign_var : public trail {
|
||||
pvar m_var;
|
||||
core& c;
|
||||
public:
|
||||
mk_assign_var(pvar v, core& c) : m_var(v), c(c) {}
|
||||
void undo() {
|
||||
c.m_justification[m_var] = null_dependency;
|
||||
c.m_assignment.pop();
|
||||
}
|
||||
};
|
||||
|
||||
class core::mk_dqueue_var : public trail {
|
||||
pvar m_var;
|
||||
core& c;
|
||||
public:
|
||||
mk_dqueue_var(pvar v, core& c) : m_var(v), c(c) {}
|
||||
void undo() {
|
||||
c.m_var_queue.unassign_var_eh(m_var);
|
||||
}
|
||||
};
|
||||
|
||||
class core::mk_add_var : public trail {
|
||||
core& c;
|
||||
public:
|
||||
mk_add_var(core& c) : c(c) {}
|
||||
void undo() override {
|
||||
c.del_var();
|
||||
}
|
||||
};
|
||||
|
||||
class core::mk_add_watch : public trail {
|
||||
core& c;
|
||||
public:
|
||||
mk_add_watch(core& c) : c(c) {}
|
||||
void undo() override {
|
||||
auto& [sc, lit] = c.m_constraint_trail.back();
|
||||
auto& vars = sc.vars();
|
||||
if (vars.size() > 0)
|
||||
c.m_watch[vars[0]].pop_back();
|
||||
if (vars.size() > 1)
|
||||
c.m_watch[vars[1]].pop_back();
|
||||
c.m_constraint_trail.pop_back();
|
||||
}
|
||||
};
|
||||
|
||||
core::core(solver_interface& s) :
|
||||
s(s),
|
||||
m_viable(*this),
|
||||
m_constraints(s.trail()),
|
||||
m_assignment(*this),
|
||||
m_var_queue(m_activity)
|
||||
{}
|
||||
|
||||
pdd core::value(rational const& v, unsigned sz) {
|
||||
return sz2pdd(sz).mk_val(v);
|
||||
}
|
||||
|
||||
dd::pdd_manager& core::sz2pdd(unsigned sz) const {
|
||||
m_pdd.reserve(sz + 1);
|
||||
if (!m_pdd[sz])
|
||||
m_pdd.set(sz, alloc(dd::pdd_manager, 1000, dd::pdd_manager::semantics::mod2N_e, sz));
|
||||
return *m_pdd[sz];
|
||||
}
|
||||
|
||||
dd::pdd_manager& core::var2pdd(pvar v) const {
|
||||
return sz2pdd(size(v));
|
||||
}
|
||||
|
||||
pvar core::add_var(unsigned sz) {
|
||||
unsigned v = m_vars.size();
|
||||
m_vars.push_back(sz2pdd(sz).mk_var(v));
|
||||
m_activity.push_back({ sz, 0 });
|
||||
m_justification.push_back(null_dependency);
|
||||
m_watch.push_back({});
|
||||
m_var_queue.mk_var_eh(v);
|
||||
s.trail().push(mk_add_var(*this));
|
||||
return v;
|
||||
}
|
||||
|
||||
void core::del_var() {
|
||||
unsigned v = m_vars.size() - 1;
|
||||
m_vars.pop_back();
|
||||
m_activity.pop_back();
|
||||
m_justification.pop_back();
|
||||
m_watch.pop_back();
|
||||
m_var_queue.del_var_eh(v);
|
||||
}
|
||||
|
||||
unsigned core::register_constraint(signed_constraint& sc, dependency d) {
|
||||
unsigned idx = m_constraint_trail.size();
|
||||
m_constraint_trail.push_back({ sc, d });
|
||||
auto& vars = sc.vars();
|
||||
unsigned i = 0, j = 0, sz = vars.size();
|
||||
for (; i < sz && j < 2; ++i)
|
||||
if (!is_assigned(vars[i]))
|
||||
std::swap(vars[i], vars[j++]);
|
||||
if (vars.size() > 0)
|
||||
add_watch(idx, vars[0]);
|
||||
if (vars.size() > 1)
|
||||
add_watch(idx, vars[1]);
|
||||
s.trail().push(mk_add_watch(*this));
|
||||
return idx;
|
||||
}
|
||||
|
||||
// case split on unassigned variables until all are assigned values.
|
||||
// create equality literal for unassigned variable.
|
||||
// return new_eq if there is a new literal.
|
||||
|
||||
sat::check_result core::check() {
|
||||
if (m_var_queue.empty())
|
||||
return sat::check_result::CR_DONE;
|
||||
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:
|
||||
m_unsat_core = m_viable.explain();
|
||||
propagate_unsat_core();
|
||||
return sat::check_result::CR_CONTINUE;
|
||||
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;
|
||||
case find_t::resource_out:
|
||||
return sat::check_result::CR_GIVEUP;
|
||||
}
|
||||
UNREACHABLE();
|
||||
return sat::check_result::CR_GIVEUP;
|
||||
}
|
||||
|
||||
// First propagate Boolean assignment, then propagate value assignment
|
||||
bool core::propagate() {
|
||||
if (m_qhead == m_prop_queue.size() && m_vqhead == m_prop_queue.size())
|
||||
return false;
|
||||
s.trail().push(value_trail(m_qhead));
|
||||
for (; m_qhead < m_prop_queue.size() && !s.inconsistent(); ++m_qhead)
|
||||
propagate_assignment(m_prop_queue[m_qhead]);
|
||||
s.trail().push(value_trail(m_vqhead));
|
||||
for (; m_vqhead < m_prop_queue.size() && !s.inconsistent(); ++m_vqhead)
|
||||
propagate_value(m_prop_queue[m_vqhead]);
|
||||
return true;
|
||||
}
|
||||
|
||||
signed_constraint core::get_constraint(unsigned idx, bool sign) {
|
||||
auto sc = m_constraint_trail[idx].sc;
|
||||
if (sign)
|
||||
sc = ~sc;
|
||||
return sc;
|
||||
}
|
||||
|
||||
|
||||
void core::propagate_assignment(prop_item& dc) {
|
||||
auto [idx, sign, dep] = dc;
|
||||
auto sc = get_constraint(idx, sign);
|
||||
if (sc.is_eq(m_var, m_value))
|
||||
propagate_assignment(m_var, m_value, dep);
|
||||
}
|
||||
|
||||
void core::add_watch(unsigned idx, unsigned var) {
|
||||
m_watch[var].push_back(idx);
|
||||
}
|
||||
|
||||
void core::propagate_assignment(pvar v, rational const& value, dependency dep) {
|
||||
if (is_assigned(v))
|
||||
return;
|
||||
if (m_var_queue.contains(v)) {
|
||||
m_var_queue.del_var_eh(v);
|
||||
s.trail().push(mk_dqueue_var(v, *this));
|
||||
}
|
||||
m_values[v] = value;
|
||||
m_justification[v] = dep;
|
||||
m_assignment.push(v , value);
|
||||
s.trail().push(mk_assign_var(v, *this));
|
||||
|
||||
// update the watch lists for pvars
|
||||
// remove constraints from m_watch[v] that have more than 2 free variables.
|
||||
// for entries where there is only one free variable left add to viable set
|
||||
unsigned j = 0;
|
||||
for (auto idx : m_watch[v]) {
|
||||
auto [sc, as] = m_constraint_trail[idx];
|
||||
auto& vars = sc.vars();
|
||||
if (vars[0] != v)
|
||||
std::swap(vars[0], vars[1]);
|
||||
SASSERT(vars[0] == v);
|
||||
bool swapped = false;
|
||||
for (unsigned i = vars.size(); i-- > 2; ) {
|
||||
if (!is_assigned(vars[i])) {
|
||||
add_watch(idx, vars[i]);
|
||||
std::swap(vars[i], vars[0]);
|
||||
swapped = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
SASSERT(!swapped || vars.size() <= 1 || (!is_assigned(vars[0]) && !is_assigned(vars[1])));
|
||||
if (swapped)
|
||||
continue;
|
||||
m_watch[v][j++] = idx;
|
||||
if (vars.size() <= 1)
|
||||
continue;
|
||||
auto v1 = vars[1];
|
||||
if (is_assigned(v1))
|
||||
continue;
|
||||
SASSERT(is_assigned(vars[0]) && vars.size() >= 2);
|
||||
// detect unitary, add to viable, detect conflict?
|
||||
m_viable.add_unitary(v1, idx);
|
||||
}
|
||||
m_watch[v].shrink(j);
|
||||
}
|
||||
|
||||
void core::propagate_value(prop_item const& dc) {
|
||||
auto [idx, sign, dep] = dc;
|
||||
auto sc = get_constraint(idx, sign);
|
||||
// check if sc evaluates to false
|
||||
switch (eval(sc)) {
|
||||
case l_true:
|
||||
break;
|
||||
case l_false:
|
||||
m_unsat_core = explain_eval(sc);
|
||||
m_unsat_core.push_back(dep);
|
||||
propagate_unsat_core();
|
||||
return;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
// if sc is v == value, then check the watch list for v to propagate truth assignments
|
||||
if (sc.is_eq(m_var, m_value)) {
|
||||
for (auto idx1 : m_watch[m_var]) {
|
||||
if (idx == idx1)
|
||||
continue;
|
||||
auto [sc, d] = m_constraint_trail[idx1];
|
||||
switch (eval(sc)) {
|
||||
case l_false:
|
||||
s.propagate(d, true, explain_eval(sc));
|
||||
break;
|
||||
case l_true:
|
||||
s.propagate(d, false, explain_eval(sc));
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void core::propagate_unsat_core() {
|
||||
// default is to use unsat core:
|
||||
// if core is based on viable, use s.set_lemma();
|
||||
|
||||
s.set_conflict(m_unsat_core);
|
||||
}
|
||||
|
||||
void core::assign_eh(unsigned index, bool sign, dependency const& dep) {
|
||||
m_prop_queue.push_back({ index, sign, dep });
|
||||
s.trail().push(push_back_vector(m_prop_queue));
|
||||
}
|
||||
|
||||
dependency_vector core::explain_eval(signed_constraint const& sc) {
|
||||
dependency_vector deps;
|
||||
for (auto v : sc.vars())
|
||||
if (is_assigned(v))
|
||||
deps.push_back(m_justification[v]);
|
||||
return deps;
|
||||
}
|
||||
|
||||
lbool core::eval(signed_constraint const& sc) {
|
||||
return sc.eval(m_assignment);
|
||||
}
|
||||
|
||||
pdd core::subst(pdd const& p) {
|
||||
return m_assignment.apply_to(p);
|
||||
}
|
||||
|
||||
trail_stack& core::trail() {
|
||||
return s.trail();
|
||||
}
|
||||
|
||||
}
|
||||
136
src/sat/smt/polysat/polysat_core.h
Normal file
136
src/sat/smt/polysat/polysat_core.h
Normal file
|
|
@ -0,0 +1,136 @@
|
|||
/*++
|
||||
Copyright (c) 2020 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
polysat_core.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Core solver for polysat
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2020-08-30
|
||||
Jakob Rath 2021-04-06
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
|
||||
#include "util/dependency.h"
|
||||
#include "math/dd/dd_pdd.h"
|
||||
#include "sat/smt/sat_th.h"
|
||||
#include "sat/smt/polysat/polysat_types.h"
|
||||
#include "sat/smt/polysat/polysat_constraints.h"
|
||||
#include "sat/smt/polysat/polysat_viable.h"
|
||||
#include "sat/smt/polysat/polysat_assignment.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
class core;
|
||||
class solver_interface;
|
||||
|
||||
class core {
|
||||
class mk_add_var;
|
||||
class mk_dqueue_var;
|
||||
class mk_assign_var;
|
||||
class mk_add_watch;
|
||||
typedef svector<std::pair<unsigned, unsigned>> activity;
|
||||
typedef std::tuple<unsigned, bool, dependency> prop_item;
|
||||
friend class viable;
|
||||
friend class constraints;
|
||||
friend class assignment;
|
||||
|
||||
struct constraint_info {
|
||||
signed_constraint sc;
|
||||
dependency d;
|
||||
};
|
||||
solver_interface& s;
|
||||
viable m_viable;
|
||||
constraints m_constraints;
|
||||
assignment m_assignment;
|
||||
unsigned m_qhead = 0, m_vqhead = 0;
|
||||
svector<prop_item> m_prop_queue;
|
||||
svector<constraint_info> m_constraint_trail; // index of constraints
|
||||
mutable scoped_ptr_vector<dd::pdd_manager> m_pdd;
|
||||
dependency_vector m_unsat_core;
|
||||
|
||||
|
||||
// attributes associated with variables
|
||||
vector<pdd> m_vars; // for each variable a pdd
|
||||
vector<rational> m_values; // current value of assigned variable
|
||||
svector<dependency> m_justification; // justification for assignment
|
||||
activity m_activity; // activity of variables
|
||||
var_queue<activity> m_var_queue; // priority queue of variables to assign
|
||||
vector<unsigned_vector> m_watch; // watch lists for variables for constraints on m_prop_queue where they occur
|
||||
|
||||
// values to split on
|
||||
rational m_value;
|
||||
pvar m_var = 0;
|
||||
|
||||
dd::pdd_manager& sz2pdd(unsigned sz) const;
|
||||
dd::pdd_manager& var2pdd(pvar v) const;
|
||||
|
||||
void del_var();
|
||||
|
||||
bool is_assigned(pvar v) { return !m_justification[v].is_null(); }
|
||||
void propagate_value(prop_item const& dc);
|
||||
void propagate_assignment(prop_item& dc);
|
||||
void propagate_assignment(pvar v, rational const& value, dependency dep);
|
||||
void propagate_unsat_core();
|
||||
|
||||
void add_watch(unsigned idx, unsigned var);
|
||||
|
||||
signed_constraint get_constraint(unsigned idx, bool sign);
|
||||
|
||||
lbool eval(signed_constraint const& sc);
|
||||
dependency_vector explain_eval(signed_constraint const& sc);
|
||||
|
||||
public:
|
||||
core(solver_interface& s);
|
||||
|
||||
sat::check_result check();
|
||||
|
||||
unsigned register_constraint(signed_constraint& sc, dependency d);
|
||||
bool propagate();
|
||||
void assign_eh(unsigned idx, bool sign, dependency const& d);
|
||||
|
||||
pdd value(rational const& v, unsigned sz);
|
||||
pdd subst(pdd const&);
|
||||
|
||||
signed_constraint eq(pdd const& p) { return m_constraints.eq(p); }
|
||||
signed_constraint eq(pdd const& p, pdd const& q) { return m_constraints.eq(p - q); }
|
||||
signed_constraint ule(pdd const& p, pdd const& q) { return m_constraints.ule(p, q); }
|
||||
signed_constraint sle(pdd const& p, pdd const& q) { return m_constraints.sle(p, q); }
|
||||
signed_constraint umul_ovfl(pdd const& p, pdd const& q) { return m_constraints.umul_ovfl(p, q); }
|
||||
signed_constraint smul_ovfl(pdd const& p, pdd const& q) { return m_constraints.smul_ovfl(p, q); }
|
||||
signed_constraint smul_udfl(pdd const& p, pdd const& q) { return m_constraints.smul_udfl(p, q); }
|
||||
signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); }
|
||||
|
||||
|
||||
pdd lshr(pdd a, pdd b) { throw default_exception("nyi"); }
|
||||
pdd ashr(pdd a, pdd b) { throw default_exception("nyi"); }
|
||||
pdd shl(pdd a, pdd b) { throw default_exception("nyi"); }
|
||||
pdd band(pdd a, pdd b) { throw default_exception("nyi"); }
|
||||
pdd bxor(pdd a, pdd b) { throw default_exception("nyi"); }
|
||||
pdd bor(pdd a, pdd b) { throw default_exception("nyi"); }
|
||||
pdd bnand(pdd a, pdd b) { throw default_exception("nyi"); }
|
||||
pdd bxnor(pdd a, pdd b) { throw default_exception("nyi"); }
|
||||
pdd bnor(pdd a, pdd b) { throw default_exception("nyi"); }
|
||||
pdd bnot(pdd a) { throw default_exception("nyi"); }
|
||||
std::pair<pdd, pdd> quot_rem(pdd const& n, pdd const& d) { throw default_exception("nyi"); }
|
||||
pdd zero_ext(pdd a, unsigned sz) { throw default_exception("nyi"); }
|
||||
pdd sign_ext(pdd a, unsigned sz) { throw default_exception("nyi"); }
|
||||
pdd extract(pdd src, unsigned hi, unsigned lo) { throw default_exception("nyi"); }
|
||||
pdd concat(unsigned n, pdd const* args) { throw default_exception("nyi"); }
|
||||
pvar add_var(unsigned sz);
|
||||
pdd var(pvar p) { return m_vars[p]; }
|
||||
unsigned size(pvar v) const { return var2pdd(v).power_of_2(); }
|
||||
|
||||
constraints& cs() { return m_constraints; }
|
||||
trail_stack& trail();
|
||||
|
||||
std::ostream& display(std::ostream& out) const { throw default_exception("nyi"); }
|
||||
};
|
||||
|
||||
}
|
||||
588
src/sat/smt/polysat/polysat_fi.cpp
Normal file
588
src/sat/smt/polysat/polysat_fi.cpp
Normal file
|
|
@ -0,0 +1,588 @@
|
|||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
Conflict explanation using forbidden intervals as described in
|
||||
"Solving bitvectors with MCSAT: explanations from bits and pieces"
|
||||
by S. Graham-Lengrand, D. Jovanovic, B. Dutertre.
|
||||
|
||||
Author:
|
||||
|
||||
Jakob Rath 2021-04-06
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
|
||||
--*/
|
||||
#include "sat/smt/polysat/polysat_fi.h"
|
||||
#include "sat/smt/polysat/polysat_interval.h"
|
||||
#include "sat/smt/polysat/polysat_umul_ovfl.h"
|
||||
#include "sat/smt/polysat/polysat_ule.h"
|
||||
#include "sat/smt/polysat/polysat_core.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
/**
|
||||
*
|
||||
* \param[in] c Original constraint
|
||||
* \param[in] v Variable that is bounded by constraint
|
||||
* \param[out] fi "forbidden interval" record that captures values not allowed for v
|
||||
* \returns True iff a forbidden interval exists and the output parameters were set.
|
||||
*/
|
||||
bool forbidden_intervals::get_interval(signed_constraint const& c, pvar v, fi_record& fi) {
|
||||
// verbose_stream() << "get_interval for v" << v << " " << c << "\n";
|
||||
SASSERT(fi.side_cond.empty());
|
||||
SASSERT(fi.src.empty());
|
||||
fi.bit_width = s.size(v); // TODO: preliminary
|
||||
if (c.is_ule())
|
||||
return get_interval_ule(c, v, fi);
|
||||
if (c.is_umul_ovfl())
|
||||
return get_interval_umul_ovfl(c, v, fi);
|
||||
return false;
|
||||
}
|
||||
|
||||
bool forbidden_intervals::get_interval_umul_ovfl(signed_constraint const& c, pvar v, fi_record& fi) {
|
||||
using std::swap;
|
||||
|
||||
backtrack _backtrack(fi.side_cond);
|
||||
|
||||
fi.coeff = 1;
|
||||
fi.src.push_back(c);
|
||||
|
||||
// eval(lhs) = a1*v + eval(e1) = a1*v + b1
|
||||
// eval(rhs) = a2*v + eval(e2) = a2*v + b2
|
||||
// We keep the e1, e2 around in case we need side conditions such as e1=b1, e2=b2.
|
||||
auto [ok1, a1, e1, b1] = linear_decompose(v, c.to_umul_ovfl().p(), fi.side_cond);
|
||||
auto [ok2, a2, e2, b2] = linear_decompose(v, c.to_umul_ovfl().q(), fi.side_cond);
|
||||
|
||||
auto& m = e1.manager();
|
||||
rational bound = m.max_value();
|
||||
|
||||
if (ok2 && !ok1) {
|
||||
swap(a1, a2);
|
||||
swap(e1, e2);
|
||||
swap(b1, b2);
|
||||
swap(ok1, ok2);
|
||||
}
|
||||
if (ok1 && !ok2 && a1.is_one() && b1.is_zero()) {
|
||||
if (c.is_positive()) {
|
||||
_backtrack.released = true;
|
||||
rational lo_val(0);
|
||||
rational hi_val(2);
|
||||
pdd lo = m.mk_val(lo_val);
|
||||
pdd hi = m.mk_val(hi_val);
|
||||
fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
if (!ok1 || !ok2)
|
||||
return false;
|
||||
|
||||
|
||||
if (a2.is_one() && a1.is_zero()) {
|
||||
swap(a1, a2);
|
||||
swap(e1, e2);
|
||||
swap(b1, b2);
|
||||
}
|
||||
|
||||
if (!a1.is_one() || !a2.is_zero())
|
||||
return false;
|
||||
|
||||
if (!b1.is_zero())
|
||||
return false;
|
||||
|
||||
_backtrack.released = true;
|
||||
|
||||
// Ovfl(v, e2)
|
||||
|
||||
|
||||
if (c.is_positive()) {
|
||||
if (b2.val() <= 1) {
|
||||
fi.interval = eval_interval::full();
|
||||
fi.side_cond.push_back(s.cs().ule(e2, 1));
|
||||
}
|
||||
else {
|
||||
// [0, div(bound, b2.val()) + 1[
|
||||
rational lo_val(0);
|
||||
rational hi_val(div(bound, b2.val()) + 1);
|
||||
pdd lo = m.mk_val(lo_val);
|
||||
pdd hi = m.mk_val(hi_val);
|
||||
fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
|
||||
fi.side_cond.push_back(s.cs().ule(e2, b2.val()));
|
||||
}
|
||||
|
||||
}
|
||||
else {
|
||||
if (b2.val() <= 1) {
|
||||
_backtrack.released = false;
|
||||
return false;
|
||||
}
|
||||
else {
|
||||
// [div(bound, b2.val()) + 1, 0[
|
||||
rational lo_val(div(bound, b2.val()) + 1);
|
||||
rational hi_val(0);
|
||||
pdd lo = m.mk_val(lo_val);
|
||||
pdd hi = m.mk_val(hi_val);
|
||||
fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
|
||||
fi.side_cond.push_back(s.cs().ule(b2.val(), e2));
|
||||
}
|
||||
}
|
||||
|
||||
// LOG("overflow interval " << fi.interval);
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
static char const* _last_function = "";
|
||||
|
||||
bool forbidden_intervals::get_interval_ule(signed_constraint const& c, pvar v, fi_record& fi) {
|
||||
|
||||
backtrack _backtrack(fi.side_cond);
|
||||
|
||||
fi.coeff = 1;
|
||||
fi.src.push_back(c);
|
||||
|
||||
struct show {
|
||||
forbidden_intervals& f;
|
||||
signed_constraint const& c;
|
||||
pvar v;
|
||||
fi_record& fi;
|
||||
backtrack& _backtrack;
|
||||
show(forbidden_intervals& f,
|
||||
signed_constraint const& c,
|
||||
pvar v,
|
||||
fi_record& fi,
|
||||
backtrack& _backtrack):f(f), c(c), v(v), fi(fi), _backtrack(_backtrack) {}
|
||||
~show() {
|
||||
if (!_backtrack.released)
|
||||
return;
|
||||
IF_VERBOSE(0, verbose_stream() << _last_function << " " << v << " " << c << " " << fi.interval << " " << fi.side_cond << "\n");
|
||||
}
|
||||
};
|
||||
// uncomment to trace intervals
|
||||
// show _show(*this, c, v, fi, _backtrack);
|
||||
|
||||
// eval(lhs) = a1*v + eval(e1) = a1*v + b1
|
||||
// eval(rhs) = a2*v + eval(e2) = a2*v + b2
|
||||
// We keep the e1, e2 around in case we need side conditions such as e1=b1, e2=b2.
|
||||
auto [ok1, a1, e1, b1] = linear_decompose(v, c.to_ule().lhs(), fi.side_cond);
|
||||
auto [ok2, a2, e2, b2] = linear_decompose(v, c.to_ule().rhs(), fi.side_cond);
|
||||
|
||||
_backtrack.released = true;
|
||||
|
||||
// v > q
|
||||
if (false && ok1 && !ok2 && match_non_zero(c, a1, b1, e1, c.to_ule().rhs(), fi))
|
||||
return true;
|
||||
|
||||
// p > v
|
||||
if (false && !ok1 && ok2 && match_non_max(c, c.to_ule().lhs(), a2, b2, e2, fi))
|
||||
return true;
|
||||
|
||||
if (!ok1 || !ok2 || (a1.is_zero() && a2.is_zero())) {
|
||||
_backtrack.released = false;
|
||||
return false;
|
||||
}
|
||||
SASSERT(b1.is_val());
|
||||
SASSERT(b2.is_val());
|
||||
|
||||
// a*v + b <= 0, a odd
|
||||
// a*v + b > 0, a odd
|
||||
if (match_zero(c, a1, b1, e1, a2, b2, e2, fi))
|
||||
return true;
|
||||
|
||||
// -1 <= a*v + b, a odd
|
||||
// -1 > a*v + b, a odd
|
||||
if (match_max(c, a1, b1, e1, a2, b2, e2, fi))
|
||||
return true;
|
||||
|
||||
if (match_linear1(c, a1, b1, e1, a2, b2, e2, fi))
|
||||
return true;
|
||||
if (match_linear2(c, a1, b1, e1, a2, b2, e2, fi))
|
||||
return true;
|
||||
if (match_linear3(c, a1, b1, e1, a2, b2, e2, fi))
|
||||
return true;
|
||||
if (match_linear4(c, a1, b1, e1, a2, b2, e2, fi))
|
||||
return true;
|
||||
|
||||
_backtrack.released = false;
|
||||
return false;
|
||||
}
|
||||
|
||||
void forbidden_intervals::push_eq(bool is_zero, pdd const& p, vector<signed_constraint>& side_cond) {
|
||||
SASSERT(!p.is_val() || (is_zero == p.is_zero()));
|
||||
if (p.is_val())
|
||||
return;
|
||||
else if (is_zero)
|
||||
side_cond.push_back(s.eq(p));
|
||||
else
|
||||
side_cond.push_back(~s.eq(p));
|
||||
}
|
||||
|
||||
std::tuple<bool, rational, pdd, pdd> forbidden_intervals::linear_decompose(pvar v, pdd const& p, vector<signed_constraint>& out_side_cond) {
|
||||
auto& m = p.manager();
|
||||
pdd q = m.zero();
|
||||
pdd e = m.zero();
|
||||
unsigned const deg = p.degree(v);
|
||||
if (deg == 0)
|
||||
// p = 0*v + e
|
||||
e = p;
|
||||
else if (deg == 1)
|
||||
// p = q*v + e
|
||||
p.factor(v, 1, q, e);
|
||||
else
|
||||
return std::tuple(false, rational(0), q, e);
|
||||
|
||||
// r := eval(q)
|
||||
// Add side constraint q = r.
|
||||
if (!q.is_val()) {
|
||||
pdd r = s.subst(q);
|
||||
|
||||
|
||||
if (!r.is_val())
|
||||
return std::tuple(false, rational(0), q, e);
|
||||
out_side_cond.push_back(s.eq(q, r));
|
||||
q = r;
|
||||
}
|
||||
auto b = s.subst(e);
|
||||
return std::tuple(b.is_val(), q.val(), e, b);
|
||||
};
|
||||
|
||||
eval_interval forbidden_intervals::to_interval(
|
||||
signed_constraint const& c, bool is_trivial, rational & coeff,
|
||||
rational & lo_val, pdd & lo,
|
||||
rational & hi_val, pdd & hi) {
|
||||
|
||||
dd::pdd_manager& m = lo.manager();
|
||||
|
||||
if (is_trivial) {
|
||||
if (c.is_positive())
|
||||
// TODO: we cannot use empty intervals for interpolation. So we
|
||||
// can remove the empty case (make it represent 'full' instead),
|
||||
// and return 'false' here. Then we do not need the proper/full
|
||||
// tag on intervals.
|
||||
return eval_interval::empty(m);
|
||||
else
|
||||
return eval_interval::full();
|
||||
}
|
||||
|
||||
rational pow2 = m.two_to_N();
|
||||
|
||||
if (coeff > pow2/2) {
|
||||
// TODO: if coeff != pow2 - 1, isn't this counterproductive now? considering the gap condition on refine-equal-lin acceleration.
|
||||
|
||||
coeff = pow2 - coeff;
|
||||
SASSERT(coeff > 0);
|
||||
// Transform according to: y \in [l;u[ <=> -y \in [1-u;1-l[
|
||||
// -y \in [1-u;1-l[
|
||||
// <=> -y - (1 - u) < (1 - l) - (1 - u) { by: y \in [l;u[ <=> y - l < u - l }
|
||||
// <=> u - y - 1 < u - l { simplified }
|
||||
// <=> (u-l) - (u-y-1) - 1 < u-l { by: a < b <=> b - a - 1 < b }
|
||||
// <=> y - l < u - l { simplified }
|
||||
// <=> y \in [l;u[.
|
||||
lo = 1 - lo;
|
||||
hi = 1 - hi;
|
||||
swap(lo, hi);
|
||||
lo_val = mod(1 - lo_val, pow2);
|
||||
hi_val = mod(1 - hi_val, pow2);
|
||||
lo_val.swap(hi_val);
|
||||
}
|
||||
|
||||
if (c.is_positive())
|
||||
return eval_interval::proper(lo, lo_val, hi, hi_val);
|
||||
else
|
||||
return eval_interval::proper(hi, hi_val, lo, lo_val);
|
||||
}
|
||||
|
||||
/**
|
||||
* Match e1 + t <= e2, with t = a1*y
|
||||
* condition for empty/full: e2 == -1
|
||||
*/
|
||||
bool forbidden_intervals::match_linear1(signed_constraint const& c,
|
||||
rational const & a1, pdd const& b1, pdd const& e1,
|
||||
rational const & a2, pdd const& b2, pdd const& e2,
|
||||
fi_record& fi) {
|
||||
_last_function = __func__;
|
||||
if (a2.is_zero() && !a1.is_zero()) {
|
||||
SASSERT(!a1.is_zero());
|
||||
bool is_trivial = (b2 + 1).is_zero();
|
||||
push_eq(is_trivial, e2 + 1, fi.side_cond);
|
||||
auto lo = e2 - e1 + 1;
|
||||
rational lo_val = (b2 - b1 + 1).val();
|
||||
auto hi = -e1;
|
||||
rational hi_val = (-b1).val();
|
||||
fi.coeff = a1;
|
||||
fi.interval = to_interval(c, is_trivial, fi.coeff, lo_val, lo, hi_val, hi);
|
||||
add_non_unit_side_conds(fi, b1, e1, b2, e2);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
/**
|
||||
* e1 <= e2 + t, with t = a2*y
|
||||
* condition for empty/full: e1 == 0
|
||||
*/
|
||||
bool forbidden_intervals::match_linear2(signed_constraint const& c,
|
||||
rational const & a1, pdd const& b1, pdd const& e1,
|
||||
rational const & a2, pdd const& b2, pdd const& e2,
|
||||
fi_record& fi) {
|
||||
_last_function = __func__;
|
||||
if (a1.is_zero() && !a2.is_zero()) {
|
||||
SASSERT(!a2.is_zero());
|
||||
bool is_trivial = b1.is_zero();
|
||||
push_eq(is_trivial, e1, fi.side_cond);
|
||||
auto lo = -e2;
|
||||
rational lo_val = (-b2).val();
|
||||
auto hi = e1 - e2;
|
||||
rational hi_val = (b1 - b2).val();
|
||||
fi.coeff = a2;
|
||||
fi.interval = to_interval(c, is_trivial, fi.coeff, lo_val, lo, hi_val, hi);
|
||||
add_non_unit_side_conds(fi, b1, e1, b2, e2);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
/**
|
||||
* e1 + t <= e2 + t, with t = a1*y = a2*y
|
||||
* condition for empty/full: e1 == e2
|
||||
*/
|
||||
bool forbidden_intervals::match_linear3(signed_constraint const& c,
|
||||
rational const & a1, pdd const& b1, pdd const& e1,
|
||||
rational const & a2, pdd const& b2, pdd const& e2,
|
||||
fi_record& fi) {
|
||||
_last_function = __func__;
|
||||
if (a1 == a2 && !a1.is_zero()) {
|
||||
bool is_trivial = b1.val() == b2.val();
|
||||
push_eq(is_trivial, e1 - e2, fi.side_cond);
|
||||
auto lo = -e2;
|
||||
rational lo_val = (-b2).val();
|
||||
auto hi = -e1;
|
||||
rational hi_val = (-b1).val();
|
||||
fi.coeff = a1;
|
||||
fi.interval = to_interval(c, is_trivial, fi.coeff, lo_val, lo, hi_val, hi);
|
||||
add_non_unit_side_conds(fi, b1, e1, b2, e2);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
/**
|
||||
* e1 + t <= e2 + t', with t = a1*y, t' = a2*y, a1 != a2, a1, a2 non-zero
|
||||
*/
|
||||
bool forbidden_intervals::match_linear4(signed_constraint const& c,
|
||||
rational const & a1, pdd const& b1, pdd const& e1,
|
||||
rational const & a2, pdd const& b2, pdd const& e2,
|
||||
fi_record& fi) {
|
||||
_last_function = __func__;
|
||||
if (a1 != a2 && !a1.is_zero() && !a2.is_zero()) {
|
||||
// NOTE: we don't have an interval here in the same sense as in the other cases.
|
||||
// We use the interval to smuggle out the values a1,b1,a2,b2 without adding additional fields.
|
||||
// to_interval flips a1,b1 with a2,b2 for negative constraints, which we also need for this case.
|
||||
auto lo = b1;
|
||||
rational lo_val = a1;
|
||||
auto hi = b2;
|
||||
rational hi_val = a2;
|
||||
// We use fi.coeff = -1 to tell the caller to treat it as a diseq_lin.
|
||||
fi.coeff = -1;
|
||||
fi.interval = to_interval(c, false, fi.coeff, lo_val, lo, hi_val, hi);
|
||||
add_non_unit_side_conds(fi, b1, e1, b2, e2);
|
||||
SASSERT(!fi.interval.is_currently_empty());
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
/**
|
||||
* a*v <= 0, a odd
|
||||
* forbidden interval for v is [1;0[
|
||||
*
|
||||
* a*v + b <= 0, a odd
|
||||
* forbidden interval for v is [n+1;n[ where n = -b * a^-1
|
||||
*
|
||||
* TODO: extend to
|
||||
* 2^k*a*v <= 0, a odd
|
||||
* (using intervals for the lower bits of v)
|
||||
*/
|
||||
bool forbidden_intervals::match_zero(
|
||||
signed_constraint const& c,
|
||||
rational const & a1, pdd const& b1, pdd const& e1,
|
||||
rational const & a2, pdd const& b2, pdd const& e2,
|
||||
fi_record& fi) {
|
||||
_last_function = __func__;
|
||||
if (a1.is_odd() && a2.is_zero() && b2.is_zero()) {
|
||||
auto& m = e1.manager();
|
||||
rational const& mod_value = m.two_to_N();
|
||||
rational a1_inv;
|
||||
VERIFY(a1.mult_inverse(m.power_of_2(), a1_inv));
|
||||
|
||||
// interval for a*v + b > 0 is [n;n+1[ where n = -b * a^-1
|
||||
rational lo_val = mod(-b1.val() * a1_inv, mod_value);
|
||||
pdd lo = -e1 * a1_inv;
|
||||
rational hi_val = mod(lo_val + 1, mod_value);
|
||||
pdd hi = lo + 1;
|
||||
|
||||
// interval for a*v + b <= 0 is the complement
|
||||
if (c.is_positive()) {
|
||||
std::swap(lo_val, hi_val);
|
||||
std::swap(lo, hi);
|
||||
}
|
||||
|
||||
fi.coeff = 1;
|
||||
fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
|
||||
// RHS == 0 is a precondition because we can only multiply with a^-1 in equations, not inequalities
|
||||
if (b2 != e2)
|
||||
fi.side_cond.push_back(s.eq(b2, e2));
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
/**
|
||||
* -1 <= a*v + b, a odd
|
||||
* forbidden interval for v is [n+1;n[ where n = (-b-1) * a^-1
|
||||
*/
|
||||
bool forbidden_intervals::match_max(
|
||||
signed_constraint const& c,
|
||||
rational const & a1, pdd const& b1, pdd const& e1,
|
||||
rational const & a2, pdd const& b2, pdd const& e2,
|
||||
fi_record& fi) {
|
||||
_last_function = __func__;
|
||||
if (a1.is_zero() && b1.is_max() && a2.is_odd()) {
|
||||
auto& m = e2.manager();
|
||||
rational const& mod_value = m.two_to_N();
|
||||
rational a2_inv;
|
||||
VERIFY(a2.mult_inverse(m.power_of_2(), a2_inv));
|
||||
|
||||
// interval for -1 > a*v + b is [n;n+1[ where n = (-b-1) * a^-1
|
||||
rational lo_val = mod((-1 - b2.val()) * a2_inv, mod_value);
|
||||
pdd lo = (-1 - e2) * a2_inv;
|
||||
rational hi_val = mod(lo_val + 1, mod_value);
|
||||
pdd hi = lo + 1;
|
||||
|
||||
// interval for -1 <= a*v + b is the complement
|
||||
if (c.is_positive()) {
|
||||
std::swap(lo_val, hi_val);
|
||||
std::swap(lo, hi);
|
||||
}
|
||||
|
||||
fi.coeff = 1;
|
||||
fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
|
||||
// LHS == -1 is a precondition because we can only multiply with a^-1 in equations, not inequalities
|
||||
if (b1 != e1)
|
||||
fi.side_cond.push_back(s.eq(b1, e1));
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
/**
|
||||
* v > q
|
||||
* forbidden interval for v is [0,1[
|
||||
*
|
||||
* v - k > q
|
||||
* forbidden interval for v is [k,k+1[
|
||||
*
|
||||
* v > q
|
||||
* forbidden interval for v is [0;q+1[ but at least [0;1[
|
||||
*
|
||||
* The following cases are implemented, and subsume the simple ones above.
|
||||
*
|
||||
* v - k > q
|
||||
* forbidden interval for v is [k;k+q+1[ but at least [k;k+1[
|
||||
*
|
||||
* a*v - k > q, a odd
|
||||
* forbidden interval for v is [a^-1*k, a^-1*k + 1[
|
||||
*/
|
||||
bool forbidden_intervals::match_non_zero(
|
||||
signed_constraint const& c,
|
||||
rational const& a1, pdd const& b1, pdd const& e1,
|
||||
pdd const& q,
|
||||
fi_record& fi) {
|
||||
_last_function = __func__;
|
||||
SASSERT(b1.is_val());
|
||||
if (a1.is_one() && c.is_negative()) {
|
||||
// v - k > q
|
||||
auto& m = e1.manager();
|
||||
rational const& mod_value = m.two_to_N();
|
||||
rational lo_val = (-b1).val();
|
||||
pdd lo = -e1;
|
||||
rational hi_val = mod(lo_val + 1, mod_value);
|
||||
pdd hi = lo + q + 1;
|
||||
fi.coeff = 1;
|
||||
fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
|
||||
return true;
|
||||
}
|
||||
if (a1.is_odd() && c.is_negative()) {
|
||||
// a*v - k > q, a odd
|
||||
auto& m = e1.manager();
|
||||
rational const& mod_value = m.two_to_N();
|
||||
rational a1_inv;
|
||||
VERIFY(a1.mult_inverse(m.power_of_2(), a1_inv));
|
||||
rational lo_val(mod(-b1.val() * a1_inv, mod_value));
|
||||
auto lo = -e1 * a1_inv;
|
||||
rational hi_val(mod(lo_val + 1, mod_value));
|
||||
auto hi = lo + 1;
|
||||
fi.coeff = 1;
|
||||
fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
/**
|
||||
* p > v
|
||||
* forbidden interval for v is [p;0[ but at least [-1,0[
|
||||
*
|
||||
* p > v + k
|
||||
* forbidden interval for v is [p-k;-k[ but at least [-1-k,-k[
|
||||
*
|
||||
* p > a*v + k, a odd
|
||||
* forbidden interval for v is [ a^-1*(-1-k) ; a^-1*(-1-k) + 1 [
|
||||
*/
|
||||
bool forbidden_intervals::match_non_max(
|
||||
signed_constraint const& c,
|
||||
pdd const& p,
|
||||
rational const& a2, pdd const& b2, pdd const& e2,
|
||||
fi_record& fi) {
|
||||
_last_function = __func__;
|
||||
SASSERT(b2.is_val());
|
||||
if (a2.is_one() && c.is_negative()) {
|
||||
// p > v + k
|
||||
auto& m = e2.manager();
|
||||
rational const& mod_value = m.two_to_N();
|
||||
rational hi_val = (-b2).val();
|
||||
pdd hi = -e2;
|
||||
rational lo_val = mod(hi_val - 1, mod_value);
|
||||
pdd lo = p - e2;
|
||||
fi.coeff = 1;
|
||||
fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
|
||||
return true;
|
||||
}
|
||||
if (a2.is_odd() && c.is_negative()) {
|
||||
// p > a*v + k, a odd
|
||||
auto& m = e2.manager();
|
||||
rational const& mod_value = m.two_to_N();
|
||||
rational a2_inv;
|
||||
VERIFY(a2.mult_inverse(m.power_of_2(), a2_inv));
|
||||
rational lo_val = mod(a2_inv * (-1 - b2.val()), mod_value);
|
||||
pdd lo = a2_inv * (-1 - e2);
|
||||
rational hi_val = mod(lo_val + 1, mod_value);
|
||||
pdd hi = lo + 1;
|
||||
fi.coeff = 1;
|
||||
fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
void forbidden_intervals::add_non_unit_side_conds(fi_record& fi, pdd const& b1, pdd const& e1, pdd const& b2, pdd const& e2) {
|
||||
if (fi.coeff == 1)
|
||||
return;
|
||||
if (b1 != e1)
|
||||
fi.side_cond.push_back(s.eq(b1, e1));
|
||||
if (b2 != e2)
|
||||
fi.side_cond.push_back(s.eq(b2, e2));
|
||||
}
|
||||
}
|
||||
122
src/sat/smt/polysat/polysat_fi.h
Normal file
122
src/sat/smt/polysat/polysat_fi.h
Normal file
|
|
@ -0,0 +1,122 @@
|
|||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
Conflict explanation using forbidden intervals as described in
|
||||
"Solving bitvectors with MCSAT: explanations from bits and pieces"
|
||||
by S. Graham-Lengrand, D. Jovanovic, B. Dutertre.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-06
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
#include "sat/smt/polysat/polysat_types.h"
|
||||
#include "sat/smt/polysat/polysat_interval.h"
|
||||
#include "sat/smt/polysat/polysat_constraints.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
class core;
|
||||
|
||||
struct fi_record {
|
||||
eval_interval interval;
|
||||
vector<signed_constraint> side_cond;
|
||||
vector<signed_constraint> src; // only units may have multiple src (as they can consist of contracted bit constraints)
|
||||
rational coeff;
|
||||
unsigned bit_width = 0; // number of lower bits; TODO: should move this to viable::entry; where the coeff/bit-width is adapted accordingly
|
||||
|
||||
/** Create invalid fi_record */
|
||||
fi_record(): interval(eval_interval::full()) {}
|
||||
|
||||
void reset() {
|
||||
interval = eval_interval::full();
|
||||
side_cond.reset();
|
||||
src.reset();
|
||||
coeff.reset();
|
||||
bit_width = 0;
|
||||
}
|
||||
|
||||
struct less {
|
||||
bool operator()(fi_record const& a, fi_record const& b) const {
|
||||
return a.interval.lo_val() < b.interval.lo_val();
|
||||
}
|
||||
};
|
||||
};
|
||||
|
||||
class forbidden_intervals {
|
||||
|
||||
void push_eq(bool is_trivial, pdd const& p, vector<signed_constraint>& side_cond);
|
||||
eval_interval to_interval(signed_constraint const& c, bool is_trivial, rational& coeff,
|
||||
rational & lo_val, pdd & lo, rational & hi_val, pdd & hi);
|
||||
|
||||
|
||||
std::tuple<bool, rational, pdd, pdd> linear_decompose(pvar v, pdd const& p, vector<signed_constraint>& out_side_cond);
|
||||
|
||||
bool match_linear1(signed_constraint const& c,
|
||||
rational const& a1, pdd const& b1, pdd const& e1,
|
||||
rational const& a2, pdd const& b2, pdd const& e2,
|
||||
fi_record& fi);
|
||||
|
||||
bool match_linear2(signed_constraint const& c,
|
||||
rational const & a1, pdd const& b1, pdd const& e1,
|
||||
rational const & a2, pdd const& b2, pdd const& e2,
|
||||
fi_record& fi);
|
||||
|
||||
bool match_linear3(signed_constraint const& c,
|
||||
rational const & a1, pdd const& b1, pdd const& e1,
|
||||
rational const & a2, pdd const& b2, pdd const& e2,
|
||||
fi_record& fi);
|
||||
|
||||
bool match_linear4(signed_constraint const& c,
|
||||
rational const & a1, pdd const& b1, pdd const& e1,
|
||||
rational const & a2, pdd const& b2, pdd const& e2,
|
||||
fi_record& fi);
|
||||
|
||||
void add_non_unit_side_conds(fi_record& fi, pdd const& b1, pdd const& e1, pdd const& b2, pdd const& e2);
|
||||
|
||||
bool match_zero(signed_constraint const& c,
|
||||
rational const & a1, pdd const& b1, pdd const& e1,
|
||||
rational const & a2, pdd const& b2, pdd const& e2,
|
||||
fi_record& fi);
|
||||
|
||||
bool match_max(signed_constraint const& c,
|
||||
rational const & a1, pdd const& b1, pdd const& e1,
|
||||
rational const & a2, pdd const& b2, pdd const& e2,
|
||||
fi_record& fi);
|
||||
|
||||
bool match_non_zero(signed_constraint const& c,
|
||||
rational const& a1, pdd const& b1, pdd const& e1,
|
||||
pdd const& q,
|
||||
fi_record& fi);
|
||||
|
||||
bool match_non_max(signed_constraint const& c,
|
||||
pdd const& p,
|
||||
rational const& a2, pdd const& b2, pdd const& e2,
|
||||
fi_record& fi);
|
||||
|
||||
bool get_interval_ule(signed_constraint const& c, pvar v, fi_record& fi);
|
||||
|
||||
bool get_interval_umul_ovfl(signed_constraint const& c, pvar v, fi_record& fi);
|
||||
|
||||
struct backtrack {
|
||||
bool released = false;
|
||||
vector<signed_constraint>& side_cond;
|
||||
unsigned sz;
|
||||
backtrack(vector<signed_constraint>& s):side_cond(s), sz(s.size()) {}
|
||||
~backtrack() {
|
||||
if (!released)
|
||||
side_cond.shrink(sz);
|
||||
}
|
||||
};
|
||||
|
||||
core& s;
|
||||
|
||||
public:
|
||||
forbidden_intervals(core& s): s(s) {}
|
||||
bool get_interval(signed_constraint const& c, pvar v, fi_record& fi);
|
||||
};
|
||||
}
|
||||
224
src/sat/smt/polysat/polysat_interval.h
Normal file
224
src/sat/smt/polysat/polysat_interval.h
Normal file
|
|
@ -0,0 +1,224 @@
|
|||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
polysat intervals
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-6
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
#include "sat/smt/polysat/polysat_types.h"
|
||||
#include <optional>
|
||||
|
||||
namespace polysat {
|
||||
|
||||
struct pdd_bounds {
|
||||
pdd lo; ///< lower bound, inclusive
|
||||
pdd hi; ///< upper bound, exclusive
|
||||
};
|
||||
|
||||
/**
|
||||
* An interval is either [lo; hi[ (excl. upper bound) or the full domain Z_{2^w}.
|
||||
* If lo > hi, the interval wraps around, i.e., represents the union of [lo; 2^w[ and [0; hi[.
|
||||
* Membership test t \in [lo; hi[ is equivalent to t - lo < hi - lo.
|
||||
*/
|
||||
class interval {
|
||||
std::optional<pdd_bounds> m_bounds = std::nullopt;
|
||||
|
||||
interval() = default;
|
||||
interval(pdd const& lo, pdd const& hi): m_bounds({lo, hi}) {}
|
||||
public:
|
||||
static interval empty(dd::pdd_manager& m) { return proper(m.zero(), m.zero()); }
|
||||
static interval full() { return {}; }
|
||||
static interval proper(pdd const& lo, pdd const& hi) { return {lo, hi}; }
|
||||
|
||||
interval(interval const&) = default;
|
||||
interval(interval&&) = default;
|
||||
interval& operator=(interval const& other) {
|
||||
m_bounds = std::nullopt; // clear pdds first to allow changing pdd_manager (probably should change the PDD assignment operator; but for now I want to be able to detect manager confusions)
|
||||
m_bounds = other.m_bounds;
|
||||
return *this;
|
||||
}
|
||||
interval& operator=(interval&& other) {
|
||||
m_bounds = std::nullopt; // clear pdds first to allow changing pdd_manager
|
||||
m_bounds = std::move(other.m_bounds);
|
||||
return *this;
|
||||
}
|
||||
~interval() = default;
|
||||
|
||||
bool is_full() const { return !m_bounds; }
|
||||
bool is_proper() const { return !!m_bounds; }
|
||||
bool is_always_empty() const { return is_proper() && lo() == hi(); }
|
||||
pdd const& lo() const { SASSERT(is_proper()); return m_bounds->lo; }
|
||||
pdd const& hi() const { SASSERT(is_proper()); return m_bounds->hi; }
|
||||
};
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& os, interval const& i) {
|
||||
if (i.is_full())
|
||||
return os << "full";
|
||||
else
|
||||
return os << "[" << i.lo() << " ; " << i.hi() << "[";
|
||||
}
|
||||
|
||||
// distance from a to b, wrapping around at mod_value.
|
||||
// basically mod(b - a, mod_value), but distance(0, mod_value, mod_value) = mod_value.
|
||||
inline rational distance(rational const& a, rational const& b, rational const& mod_value) {
|
||||
SASSERT(mod_value.is_power_of_two());
|
||||
SASSERT(0 <= a && a < mod_value);
|
||||
SASSERT(0 <= b && b <= mod_value);
|
||||
rational x = b - a;
|
||||
if (x.is_neg())
|
||||
x += mod_value;
|
||||
return x;
|
||||
}
|
||||
|
||||
class r_interval {
|
||||
rational m_lo;
|
||||
rational m_hi;
|
||||
|
||||
r_interval(rational lo, rational hi)
|
||||
: m_lo(std::move(lo)), m_hi(std::move(hi))
|
||||
{}
|
||||
|
||||
public:
|
||||
|
||||
static r_interval empty() {
|
||||
return {rational::zero(), rational::zero()};
|
||||
}
|
||||
|
||||
static r_interval full() {
|
||||
return {rational(-1), rational::zero()};
|
||||
}
|
||||
|
||||
static r_interval proper(rational lo, rational hi) {
|
||||
SASSERT(0 <= lo);
|
||||
SASSERT(0 <= hi);
|
||||
return {std::move(lo), std::move(hi)};
|
||||
}
|
||||
|
||||
bool is_full() const { return m_lo.is_neg(); }
|
||||
bool is_proper() const { return !is_full(); }
|
||||
bool is_empty() const { return is_proper() && lo() == hi(); }
|
||||
rational const& lo() const { SASSERT(is_proper()); return m_lo; }
|
||||
rational const& hi() const { SASSERT(is_proper()); return m_hi; }
|
||||
|
||||
// this one also supports representing full intervals as [lo;mod_value[
|
||||
static rational len(rational const& lo, rational const& hi, rational const& mod_value) {
|
||||
SASSERT(mod_value.is_power_of_two());
|
||||
SASSERT(0 <= lo && lo < mod_value);
|
||||
SASSERT(0 <= hi && hi <= mod_value);
|
||||
SASSERT(hi != mod_value || lo == 0); // hi == mod_value only allowed when lo == 0
|
||||
rational len = hi - lo;
|
||||
if (len.is_neg())
|
||||
len += mod_value;
|
||||
return len;
|
||||
}
|
||||
|
||||
rational len(rational const& mod_value) const {
|
||||
SASSERT(is_proper());
|
||||
return len(lo(), hi(), mod_value);
|
||||
}
|
||||
|
||||
// deals only with proper intervals
|
||||
// but works with full intervals represented as [0;mod_value[ -- maybe we should just change representation of full intervals to this always
|
||||
static bool contains(rational const& lo, rational const& hi, rational const& val) {
|
||||
if (lo <= hi)
|
||||
return lo <= val && val < hi;
|
||||
else
|
||||
return val < hi || val >= lo;
|
||||
}
|
||||
|
||||
bool contains(rational const& val) const {
|
||||
if (is_full())
|
||||
return true;
|
||||
else
|
||||
return contains(lo(), hi(), val);
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
class eval_interval {
|
||||
interval m_symbolic;
|
||||
rational m_concrete_lo;
|
||||
rational m_concrete_hi;
|
||||
|
||||
eval_interval(interval&& i, rational const& lo_val, rational const& hi_val):
|
||||
m_symbolic(std::move(i)), m_concrete_lo(lo_val), m_concrete_hi(hi_val) {}
|
||||
public:
|
||||
static eval_interval empty(dd::pdd_manager& m) {
|
||||
return {interval::empty(m), rational::zero(), rational::zero()};
|
||||
}
|
||||
|
||||
static eval_interval full() {
|
||||
return {interval::full(), rational::zero(), rational::zero()};
|
||||
}
|
||||
|
||||
static eval_interval proper(pdd const& lo, rational const& lo_val, pdd const& hi, rational const& hi_val) {
|
||||
SASSERT(0 <= lo_val && lo_val <= lo.manager().max_value());
|
||||
SASSERT(0 <= hi_val && hi_val <= hi.manager().max_value());
|
||||
return {interval::proper(lo, hi), lo_val, hi_val};
|
||||
}
|
||||
|
||||
bool is_full() const { return m_symbolic.is_full(); }
|
||||
bool is_proper() const { return m_symbolic.is_proper(); }
|
||||
bool is_always_empty() const { return m_symbolic.is_always_empty(); }
|
||||
bool is_currently_empty() const { return is_proper() && lo_val() == hi_val(); }
|
||||
interval const& symbolic() const { return m_symbolic; }
|
||||
pdd const& lo() const { return m_symbolic.lo(); }
|
||||
pdd const& hi() const { return m_symbolic.hi(); }
|
||||
rational const& lo_val() const { SASSERT(is_proper()); return m_concrete_lo; }
|
||||
rational const& hi_val() const { SASSERT(is_proper()); return m_concrete_hi; }
|
||||
|
||||
rational current_len() const {
|
||||
SASSERT(is_proper());
|
||||
return mod(hi_val() - lo_val(), lo().manager().two_to_N());
|
||||
}
|
||||
|
||||
bool currently_contains(rational const& val) const {
|
||||
if (is_full())
|
||||
return true;
|
||||
else if (lo_val() <= hi_val())
|
||||
return lo_val() <= val && val < hi_val();
|
||||
else
|
||||
return val < hi_val() || val >= lo_val();
|
||||
}
|
||||
|
||||
bool currently_contains(eval_interval const& other) const {
|
||||
if (is_full())
|
||||
return true;
|
||||
if (other.is_full())
|
||||
return false;
|
||||
// lo <= lo' <= hi' <= hi'
|
||||
if (lo_val() <= other.lo_val() && other.lo_val() <= other.hi_val() && other.hi_val() <= hi_val())
|
||||
return true;
|
||||
if (lo_val() <= hi_val())
|
||||
return false;
|
||||
// hi < lo <= lo' <= hi'
|
||||
if (lo_val() <= other.lo_val() && other.lo_val() <= other.hi_val())
|
||||
return true;
|
||||
// lo' <= hi' <= hi < lo
|
||||
if (other.lo_val() <= other.hi_val() && other.hi_val() <= hi_val())
|
||||
return true;
|
||||
// hi' <= hi < lo <= lo'
|
||||
if (other.hi_val() <= hi_val() && lo_val() <= other.lo_val())
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
||||
}; // class eval_interval
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& os, eval_interval const& i) {
|
||||
if (i.is_full())
|
||||
return os << "full";
|
||||
else {
|
||||
auto& m = i.hi().manager();
|
||||
return os << i.symbolic() << " := [" << m.normalize(i.lo_val()) << ";" << m.normalize(i.hi_val()) << "[";
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
67
src/sat/smt/polysat/polysat_types.h
Normal file
67
src/sat/smt/polysat/polysat_types.h
Normal file
|
|
@ -0,0 +1,67 @@
|
|||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-06
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
|
||||
#include <variant>
|
||||
#include "math/dd/dd_pdd.h"
|
||||
#include "util/trail.h"
|
||||
#include "util/sat_literal.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
using pdd = dd::pdd;
|
||||
using pvar = unsigned;
|
||||
using theory_var = unsigned;
|
||||
|
||||
using pvar_vector = unsigned_vector;
|
||||
inline const pvar null_var = UINT_MAX;
|
||||
|
||||
|
||||
|
||||
class dependency {
|
||||
std::variant<sat::literal, std::pair<theory_var, theory_var>> m_data;
|
||||
unsigned m_level;
|
||||
public:
|
||||
dependency(sat::literal lit, unsigned level) : m_data(lit), m_level(level) {}
|
||||
dependency(theory_var v1, theory_var v2, unsigned level) : m_data(std::make_pair(v1, v2)), m_level(level) {}
|
||||
bool is_null() const { return is_literal() && *std::get_if<sat::literal>(&m_data) == sat::null_literal; }
|
||||
bool is_literal() const { return std::holds_alternative<sat::literal>(m_data); }
|
||||
sat::literal literal() const { SASSERT(is_literal()); return *std::get_if<sat::literal>(&m_data); }
|
||||
std::pair<theory_var, theory_var> eq() const { SASSERT(!is_literal()); return *std::get_if<std::pair<theory_var, theory_var>>(&m_data); }
|
||||
unsigned level() const { return m_level; }
|
||||
};
|
||||
|
||||
inline const dependency null_dependency = dependency(sat::null_literal, UINT_MAX);
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, dependency d) {
|
||||
if (d.is_null())
|
||||
return out << "null";
|
||||
else if (d.is_literal())
|
||||
return out << d.literal() << "@" << d.level();
|
||||
else
|
||||
return out << "v" << d.eq().first << " == v" << d.eq().second << "@" << d.level();
|
||||
}
|
||||
|
||||
using dependency_vector = vector<dependency>;
|
||||
|
||||
class signed_constraint;
|
||||
|
||||
class solver_interface {
|
||||
public:
|
||||
virtual void add_eq_literal(pvar v, rational const& val) = 0;
|
||||
virtual void set_conflict(dependency_vector const& core) = 0;
|
||||
virtual void set_lemma(vector<signed_constraint> const& lemma, unsigned level, dependency_vector const& core) = 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;
|
||||
virtual trail_stack& trail() = 0;
|
||||
virtual bool inconsistent() const = 0;
|
||||
};
|
||||
|
||||
}
|
||||
346
src/sat/smt/polysat/polysat_ule.cpp
Normal file
346
src/sat/smt/polysat/polysat_ule.cpp
Normal file
|
|
@ -0,0 +1,346 @@
|
|||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
polysat unsigned <= constraints
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-06
|
||||
|
||||
Notes:
|
||||
|
||||
Canonical representation of equation p == 0 is the constraint p <= 0.
|
||||
The alternatives p < 1, -1 <= q, q > -2 are eliminated.
|
||||
|
||||
Rewrite rules to simplify expressions.
|
||||
In the following let k, k1, k2 be values.
|
||||
|
||||
- k1 <= k2 ==> 0 <= 0 if k1 <= k2
|
||||
- k1 <= k2 ==> 1 <= 0 if k1 > k2
|
||||
- 0 <= p ==> 0 <= 0
|
||||
- p <= 0 ==> 1 <= 0 if p is never zero due to parity
|
||||
- p <= -1 ==> 0 <= 0
|
||||
- k <= p ==> p - k <= - k - 1
|
||||
- k*2^n*p <= 0 ==> 2^n*p <= 0 if k is odd, leading coeffient is always a power of 2.
|
||||
|
||||
Note: the rules will rewrite alternative formulations of equations:
|
||||
- -1 <= p ==> p + 1 <= 0
|
||||
- 1 <= p ==> p - 1 <= -2
|
||||
|
||||
Rewrite rules on signed constraints:
|
||||
|
||||
- p > -2 ==> p + 1 <= 0
|
||||
- p <= -2 ==> p + 1 > 0
|
||||
|
||||
At this point, all equations are in canonical form.
|
||||
|
||||
TODO: clause simplifications:
|
||||
|
||||
- p + k <= p ==> p + k <= k & p != 0 for k != 0
|
||||
- p*q = 0 ==> p = 0 or q = 0 applies to any factoring
|
||||
- 2*p <= 2*q ==> (p >= 2^n-1 & q < 2^n-1) or (p >= 2^n-1 = q >= 2^n-1 & p <= q)
|
||||
==> (p >= 2^n-1 => q < 2^n-1 or p <= q) &
|
||||
(p < 2^n-1 => p <= q) &
|
||||
(p < 2^n-1 => q < 2^n-1)
|
||||
|
||||
- 3*p <= 3*q ==> ?
|
||||
|
||||
Note:
|
||||
case p <= p + k is already covered because we test (lhs - rhs).is_val()
|
||||
|
||||
It can be seen as an instance of lemma 5.2 of Supratik and John.
|
||||
|
||||
The following forms are equivalent:
|
||||
|
||||
p <= q
|
||||
p <= p - q - 1
|
||||
q - p <= q
|
||||
q - p <= -p - 1
|
||||
-q - 1 <= -p - 1
|
||||
-q - 1 <= p - q - 1
|
||||
|
||||
Useful lemmas:
|
||||
|
||||
p <= q && q+1 != 0 ==> p+1 <= q+1
|
||||
|
||||
p <= q && p != 0 ==> -q <= -p
|
||||
|
||||
--*/
|
||||
|
||||
#include "sat/smt/polysat/polysat_constraints.h"
|
||||
#include "sat/smt/polysat/polysat_ule.h"
|
||||
|
||||
#define LOG(_msg_) verbose_stream() << _msg_ << "\n"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
// Simplify lhs <= rhs.
|
||||
//
|
||||
// NOTE: the result should not depend on the initial value of is_positive;
|
||||
// the purpose of is_positive is to allow flipping the sign as part of a rewrite rule.
|
||||
static void simplify_impl(bool& is_positive, pdd& lhs, pdd& rhs) {
|
||||
|
||||
SASSERT_EQ(lhs.power_of_2(), rhs.power_of_2());
|
||||
unsigned const N = lhs.power_of_2();
|
||||
|
||||
// 0 <= p --> 0 <= 0
|
||||
if (lhs.is_zero()) {
|
||||
rhs = 0;
|
||||
return;
|
||||
}
|
||||
// p <= -1 --> 0 <= 0
|
||||
if (rhs.is_max()) {
|
||||
lhs = 0, rhs = 0;
|
||||
return;
|
||||
}
|
||||
// p <= p --> 0 <= 0
|
||||
if (lhs == rhs) {
|
||||
lhs = 0, rhs = 0;
|
||||
return;
|
||||
}
|
||||
// Evaluate constants
|
||||
if (lhs.is_val() && rhs.is_val()) {
|
||||
if (lhs.val() <= rhs.val())
|
||||
lhs = 0, rhs = 0;
|
||||
else
|
||||
lhs = 0, rhs = 0, is_positive = !is_positive;
|
||||
return;
|
||||
}
|
||||
|
||||
// Try to reduce the number of variables on one side using one of these rules:
|
||||
//
|
||||
// p <= q --> p <= p - q - 1
|
||||
// p <= q --> q - p <= q
|
||||
//
|
||||
// Possible alternative to 1:
|
||||
// p <= q --> q - p <= -p - 1
|
||||
// Possible alternative to 2:
|
||||
// p <= q --> -q-1 <= p - q - 1
|
||||
//
|
||||
// Example:
|
||||
//
|
||||
// x <= x + y --> x <= - y - 1
|
||||
// x + y <= x --> -y <= x
|
||||
if (!lhs.is_val() && !rhs.is_val()) {
|
||||
unsigned const lhs_vars = lhs.free_vars().size();
|
||||
unsigned const rhs_vars = rhs.free_vars().size();
|
||||
unsigned const diff_vars = (lhs - rhs).free_vars().size();
|
||||
if (diff_vars < lhs_vars || diff_vars < rhs_vars) {
|
||||
LOG("reduce number of varables");
|
||||
// verbose_stream() << "IN: " << ule_pp(to_lbool(is_positive), lhs, rhs) << "\n";
|
||||
if (lhs_vars <= rhs_vars)
|
||||
rhs = lhs - rhs - 1;
|
||||
else
|
||||
lhs = rhs - lhs;
|
||||
// verbose_stream() << "OUT: " << ule_pp(to_lbool(is_positive), lhs, rhs) << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
// -p + k <= k --> p <= k
|
||||
if (rhs.is_val() && !rhs.is_zero() && lhs.offset() == rhs.val()) {
|
||||
LOG("-p + k <= k --> p <= k");
|
||||
lhs = rhs - lhs;
|
||||
}
|
||||
|
||||
// k <= p + k --> p <= -k-1
|
||||
if (lhs.is_val() && !lhs.is_zero() && lhs.val() == rhs.offset()) {
|
||||
LOG("k <= p + k --> p <= -k-1");
|
||||
pdd k = lhs;
|
||||
lhs = rhs - lhs;
|
||||
rhs = -k - 1;
|
||||
}
|
||||
|
||||
// k <= -p --> p-1 <= -k-1
|
||||
if (lhs.is_val() && rhs.leading_coefficient().get_bit(N - 1) && !rhs.offset().is_zero()) {
|
||||
LOG("k <= -p --> p-1 <= -k-1");
|
||||
pdd k = lhs;
|
||||
lhs = -(rhs + 1);
|
||||
rhs = -k - 1;
|
||||
}
|
||||
|
||||
// -p <= k --> -k-1 <= p-1
|
||||
// if (rhs.is_val() && lhs.leading_coefficient() > rational::power_of_two(N - 1) && !lhs.offset().is_zero()) {
|
||||
if (rhs.is_val() && lhs.leading_coefficient().get_bit(N - 1) && !lhs.offset().is_zero()) {
|
||||
LOG("-p <= k --> -k-1 <= p-1");
|
||||
pdd k = rhs;
|
||||
rhs = -(lhs + 1);
|
||||
lhs = -k - 1;
|
||||
}
|
||||
|
||||
// NOTE: do not use pdd operations in conditions when comparing pdd values.
|
||||
// e.g.: "lhs.offset() == (rhs + 1).val()" is problematic with the following evaluation:
|
||||
// 1. return reference into pdd_manager::m_values from lhs.offset()
|
||||
// 2. compute rhs+1, which may reallocate pdd_manager::m_values
|
||||
// 3. now the reference returned from lhs.offset() may be invalid
|
||||
pdd const rhs_plus_one = rhs + 1;
|
||||
|
||||
// p - k <= -k - 1 --> k <= p
|
||||
// TODO: potential bug here: first call offset(), then rhs+1 has to reallocate pdd_manager::m_values, then the reference to offset is broken.
|
||||
if (rhs.is_val() && !rhs.is_zero() && lhs.offset() == rhs_plus_one.val()) {
|
||||
LOG("p - k <= -k - 1 --> k <= p");
|
||||
pdd k = -(rhs + 1);
|
||||
rhs = lhs + k;
|
||||
lhs = k;
|
||||
}
|
||||
|
||||
pdd const lhs_minus_one = lhs - 1;
|
||||
|
||||
// k <= 2^(N-1)*p + q + k-1 --> k <= 2^(N-1)*p - q
|
||||
if (lhs.is_val() && rhs.leading_coefficient() == rational::power_of_two(N-1) && rhs.offset() == lhs_minus_one.val()) {
|
||||
LOG("k <= 2^(N-1)*p + q + k-1 --> k <= 2^(N-1)*p - q");
|
||||
rhs = (lhs - 1) - rhs;
|
||||
}
|
||||
|
||||
// -1 <= p --> p + 1 <= 0
|
||||
if (lhs.is_max()) {
|
||||
lhs = rhs + 1;
|
||||
rhs = 0;
|
||||
}
|
||||
|
||||
// 1 <= p --> p > 0
|
||||
if (lhs.is_one()) {
|
||||
lhs = rhs;
|
||||
rhs = 0;
|
||||
is_positive = !is_positive;
|
||||
}
|
||||
|
||||
// p > -2 --> p + 1 <= 0
|
||||
// p <= -2 --> p + 1 > 0
|
||||
if (rhs.is_val() && !rhs.is_zero() && (rhs + 2).is_zero()) {
|
||||
// Note: rhs.is_zero() iff rhs.manager().power_of_2() == 1 (the rewrite is not wrong for M=2, but useless)
|
||||
lhs = lhs + 1;
|
||||
rhs = 0;
|
||||
is_positive = !is_positive;
|
||||
}
|
||||
// 2p + 1 <= 0 --> 0 < 0
|
||||
if (rhs.is_zero() && lhs.is_never_zero()) {
|
||||
lhs = 0;
|
||||
is_positive = !is_positive;
|
||||
return;
|
||||
}
|
||||
// a*p + q <= 0 --> p + a^-1*q <= 0 for a odd
|
||||
if (rhs.is_zero() && !lhs.leading_coefficient().is_power_of_two()) {
|
||||
rational lc = lhs.leading_coefficient();
|
||||
rational x, y;
|
||||
gcd(lc, lhs.manager().two_to_N(), x, y);
|
||||
if (x.is_neg())
|
||||
x = mod(x, lhs.manager().two_to_N());
|
||||
lhs *= x;
|
||||
SASSERT(lhs.leading_coefficient().is_power_of_two());
|
||||
}
|
||||
} // simplify_impl
|
||||
}
|
||||
|
||||
|
||||
namespace polysat {
|
||||
|
||||
ule_constraint::ule_constraint(pdd const& l, pdd const& r) :
|
||||
m_lhs(l), m_rhs(r) {
|
||||
|
||||
SASSERT_EQ(m_lhs.power_of_2(), m_rhs.power_of_2());
|
||||
|
||||
vars().append(m_lhs.free_vars());
|
||||
for (auto v : m_rhs.free_vars())
|
||||
if (!vars().contains(v))
|
||||
vars().push_back(v);
|
||||
}
|
||||
|
||||
void ule_constraint::simplify(bool& is_positive, pdd& lhs, pdd& rhs) {
|
||||
SASSERT_EQ(lhs.power_of_2(), rhs.power_of_2());
|
||||
#ifndef NDEBUG
|
||||
bool const old_is_positive = is_positive;
|
||||
pdd const old_lhs = lhs;
|
||||
pdd const old_rhs = rhs;
|
||||
#endif
|
||||
simplify_impl(is_positive, lhs, rhs);
|
||||
#ifndef NDEBUG
|
||||
if (old_is_positive != is_positive || old_lhs != lhs || old_rhs != rhs) {
|
||||
ule_pp const old_ule(to_lbool(old_is_positive), old_lhs, old_rhs);
|
||||
ule_pp const new_ule(to_lbool(is_positive), lhs, rhs);
|
||||
// always-false and always-true constraints should be rewritten to 0 != 0 and 0 == 0, respectively.
|
||||
if (is_always_false(old_is_positive, old_lhs, old_rhs)) {
|
||||
SASSERT(!is_positive);
|
||||
SASSERT(lhs.is_zero());
|
||||
SASSERT(rhs.is_zero());
|
||||
}
|
||||
if (is_always_true(old_is_positive, old_lhs, old_rhs)) {
|
||||
SASSERT(is_positive);
|
||||
SASSERT(lhs.is_zero());
|
||||
SASSERT(rhs.is_zero());
|
||||
}
|
||||
}
|
||||
SASSERT(is_simplified(lhs, rhs)); // rewriting should be idempotent
|
||||
#endif
|
||||
}
|
||||
|
||||
bool ule_constraint::is_simplified(pdd const& lhs0, pdd const& rhs0) {
|
||||
bool const pos0 = true;
|
||||
bool pos1 = pos0;
|
||||
pdd lhs1 = lhs0;
|
||||
pdd rhs1 = rhs0;
|
||||
simplify_impl(pos1, lhs1, rhs1);
|
||||
bool const is_simplified = (pos1 == pos0 && lhs1 == lhs0 && rhs1 == rhs0);
|
||||
DEBUG_CODE({
|
||||
// check that simplification doesn't depend on initial sign
|
||||
bool pos2 = !pos0;
|
||||
pdd lhs2 = lhs0;
|
||||
pdd rhs2 = rhs0;
|
||||
simplify_impl(pos2, lhs2, rhs2);
|
||||
SASSERT_EQ(pos2, !pos1);
|
||||
SASSERT_EQ(lhs2, lhs1);
|
||||
SASSERT_EQ(rhs2, rhs1);
|
||||
});
|
||||
return is_simplified;
|
||||
}
|
||||
|
||||
std::ostream& ule_constraint::display(std::ostream& out, lbool status, pdd const& lhs, pdd const& rhs) {
|
||||
out << lhs;
|
||||
if (rhs.is_zero() && status == l_true) out << " == ";
|
||||
else if (rhs.is_zero() && status == l_false) out << " != ";
|
||||
else if (status == l_true) out << " <= ";
|
||||
else if (status == l_false) out << " > ";
|
||||
else out << " <=/> ";
|
||||
return out << rhs;
|
||||
}
|
||||
|
||||
std::ostream& ule_constraint::display(std::ostream& out, lbool status) const {
|
||||
return display(out, status, m_lhs, m_rhs);
|
||||
}
|
||||
|
||||
std::ostream& ule_constraint::display(std::ostream& out) const {
|
||||
return display(out, l_true, m_lhs, m_rhs);
|
||||
}
|
||||
|
||||
|
||||
|
||||
// Evaluate lhs <= rhs
|
||||
lbool ule_constraint::eval(pdd const& lhs, pdd const& rhs) {
|
||||
// NOTE: don't assume simplifications here because we also call this on partially substituted constraints
|
||||
if (lhs.is_zero())
|
||||
return l_true; // 0 <= p
|
||||
if (lhs == rhs)
|
||||
return l_true; // p <= p
|
||||
if (rhs.is_max())
|
||||
return l_true; // p <= -1
|
||||
if (rhs.is_zero() && lhs.is_never_zero())
|
||||
return l_false; // p <= 0 implies p == 0
|
||||
if (lhs.is_one() && rhs.is_never_zero())
|
||||
return l_true; // 1 <= p implies p != 0
|
||||
if (lhs.is_val() && rhs.is_val())
|
||||
return to_lbool(lhs.val() <= rhs.val());
|
||||
return l_undef;
|
||||
|
||||
}
|
||||
|
||||
lbool ule_constraint::eval() const {
|
||||
return eval(lhs(), rhs());
|
||||
}
|
||||
|
||||
lbool ule_constraint::eval(assignment const& a) const {
|
||||
return eval(a.apply_to(lhs()), a.apply_to(rhs()));
|
||||
}
|
||||
|
||||
}
|
||||
55
src/sat/smt/polysat/polysat_ule.h
Normal file
55
src/sat/smt/polysat/polysat_ule.h
Normal file
|
|
@ -0,0 +1,55 @@
|
|||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
polysat unsigned <= constraint
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-06
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
#include "sat/smt/polysat/polysat_assignment.h"
|
||||
#include "sat/smt/polysat/polysat_constraints.h"
|
||||
|
||||
|
||||
namespace polysat {
|
||||
|
||||
class ule_constraint final : public constraint {
|
||||
pdd m_lhs;
|
||||
pdd m_rhs;
|
||||
static bool is_always_true(bool is_positive, pdd const& lhs, pdd const& rhs) { return eval(lhs, rhs) == to_lbool(is_positive); }
|
||||
static bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) { return is_always_true(!is_positive, lhs, rhs); }
|
||||
static lbool eval(pdd const& lhs, pdd const& rhs);
|
||||
|
||||
public:
|
||||
ule_constraint(pdd const& l, pdd const& r);
|
||||
~ule_constraint() override {}
|
||||
pdd const& lhs() const { return m_lhs; }
|
||||
pdd const& rhs() const { return m_rhs; }
|
||||
static std::ostream& display(std::ostream& out, lbool status, pdd const& lhs, pdd const& rhs);
|
||||
std::ostream& display(std::ostream& out, lbool status) const override;
|
||||
std::ostream& display(std::ostream& out) const override;
|
||||
lbool eval() const override;
|
||||
lbool eval(assignment const& a) const override;
|
||||
bool is_eq() const { return m_rhs.is_zero(); }
|
||||
unsigned power_of_2() const { return m_lhs.power_of_2(); }
|
||||
|
||||
static void simplify(bool& is_positive, pdd& lhs, pdd& rhs);
|
||||
static bool is_simplified(pdd const& lhs, pdd const& rhs); // return true if lhs <= rhs is not simplified further. this is meant to be used in assertions.
|
||||
};
|
||||
|
||||
struct ule_pp {
|
||||
lbool status;
|
||||
pdd lhs;
|
||||
pdd rhs;
|
||||
ule_pp(lbool status, pdd const& lhs, pdd const& rhs): status(status), lhs(lhs), rhs(rhs) {}
|
||||
ule_pp(lbool status, ule_constraint const& ule): status(status), lhs(ule.lhs()), rhs(ule.rhs()) {}
|
||||
};
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, ule_pp const& u) { return ule_constraint::display(out, u.status, u.lhs, u.rhs); }
|
||||
|
||||
}
|
||||
73
src/sat/smt/polysat/polysat_umul_ovfl.cpp
Normal file
73
src/sat/smt/polysat/polysat_umul_ovfl.cpp
Normal file
|
|
@ -0,0 +1,73 @@
|
|||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
polysat multiplication overflow constraint
|
||||
|
||||
Author:
|
||||
|
||||
Jakob Rath, Nikolaj Bjorner (nbjorner) 2021-12-09
|
||||
|
||||
--*/
|
||||
#include "sat/smt/polysat/polysat_constraints.h"
|
||||
#include "sat/smt/polysat/polysat_assignment.h"
|
||||
#include "sat/smt/polysat/polysat_umul_ovfl.h"
|
||||
|
||||
|
||||
namespace polysat {
|
||||
|
||||
umul_ovfl_constraint::umul_ovfl_constraint(pdd const& p, pdd const& q):
|
||||
m_p(p), m_q(q) {
|
||||
simplify();
|
||||
vars().append(m_p.free_vars());
|
||||
for (auto v : m_q.free_vars())
|
||||
if (!vars().contains(v))
|
||||
vars().push_back(v);
|
||||
|
||||
}
|
||||
void umul_ovfl_constraint::simplify() {
|
||||
if (m_p.is_zero() || m_q.is_zero() || m_p.is_one() || m_q.is_one()) {
|
||||
m_q = 0;
|
||||
m_p = 0;
|
||||
return;
|
||||
}
|
||||
if (m_p.index() > m_q.index())
|
||||
swap(m_p, m_q);
|
||||
}
|
||||
|
||||
std::ostream& umul_ovfl_constraint::display(std::ostream& out, lbool status) const {
|
||||
switch (status) {
|
||||
case l_true: return display(out);
|
||||
case l_false: return display(out << "~");
|
||||
case l_undef: return display(out << "?");
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& umul_ovfl_constraint::display(std::ostream& out) const {
|
||||
return out << "ovfl*(" << m_p << ", " << m_q << ")";
|
||||
}
|
||||
|
||||
lbool umul_ovfl_constraint::eval(pdd const& p, pdd const& q) {
|
||||
if (p.is_zero() || q.is_zero() || p.is_one() || q.is_one())
|
||||
return l_false;
|
||||
|
||||
if (p.is_val() && q.is_val()) {
|
||||
if (p.val() * q.val() > p.manager().max_value())
|
||||
return l_true;
|
||||
else
|
||||
return l_false;
|
||||
}
|
||||
return l_undef;
|
||||
}
|
||||
|
||||
lbool umul_ovfl_constraint::eval() const {
|
||||
return eval(p(), q());
|
||||
}
|
||||
|
||||
lbool umul_ovfl_constraint::eval(assignment const& a) const {
|
||||
return eval(a.apply_to(p()), a.apply_to(q()));
|
||||
}
|
||||
|
||||
}
|
||||
39
src/sat/smt/polysat/polysat_umul_ovfl.h
Normal file
39
src/sat/smt/polysat/polysat_umul_ovfl.h
Normal file
|
|
@ -0,0 +1,39 @@
|
|||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
polysat multiplication overflow constraint
|
||||
|
||||
Author:
|
||||
|
||||
Jakob Rath, Nikolaj Bjorner (nbjorner) 2021-12-09
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
#include "sat/smt/polysat/polysat_constraints.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
class umul_ovfl_constraint final : public constraint {
|
||||
|
||||
pdd m_p;
|
||||
pdd m_q;
|
||||
|
||||
void simplify();
|
||||
static bool is_always_true(bool is_positive, pdd const& p, pdd const& q) { return eval(p, q) == to_lbool(is_positive); }
|
||||
static bool is_always_false(bool is_positive, pdd const& p, pdd const& q) { return is_always_true(!is_positive, p, q); }
|
||||
static lbool eval(pdd const& p, pdd const& q);
|
||||
|
||||
public:
|
||||
umul_ovfl_constraint(pdd const& p, pdd const& q);
|
||||
~umul_ovfl_constraint() override {}
|
||||
pdd const& p() const { return m_p; }
|
||||
pdd const& q() const { return m_q; }
|
||||
std::ostream& display(std::ostream& out, lbool status) const override;
|
||||
std::ostream& display(std::ostream& out) const override;
|
||||
lbool eval() const override;
|
||||
lbool eval(assignment const& a) const override;
|
||||
};
|
||||
|
||||
}
|
||||
475
src/sat/smt/polysat/polysat_viable.cpp
Normal file
475
src/sat/smt/polysat/polysat_viable.cpp
Normal file
|
|
@ -0,0 +1,475 @@
|
|||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
maintain viable domains
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-06
|
||||
|
||||
Notes:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
|
||||
#include "util/debug.h"
|
||||
#include "util/log.h"
|
||||
#include "sat/smt/polysat/polysat_viable.h"
|
||||
#include "sat/smt/polysat/polysat_core.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
using dd::val_pp;
|
||||
|
||||
viable::viable(core& c) : c(c), cs(c.cs()), m_forbidden_intervals(c) {}
|
||||
|
||||
viable::~viable() {
|
||||
for (auto* e : m_alloc)
|
||||
dealloc(e);
|
||||
}
|
||||
|
||||
std::ostream& operator<<(std::ostream& out, find_t f) {
|
||||
switch (f) {
|
||||
case find_t::empty: return out << "empty";
|
||||
case find_t::singleton: return out << "singleton";
|
||||
case find_t::multiple: return out << "multiple";
|
||||
case find_t::resource_out: return out << "resource-out";
|
||||
default: return out << "<unknown>";
|
||||
}
|
||||
}
|
||||
|
||||
struct viable::pop_viable_trail : public trail {
|
||||
viable& m_s;
|
||||
entry* e;
|
||||
pvar v;
|
||||
entry_kind k;
|
||||
public:
|
||||
pop_viable_trail(viable& s, entry* e, pvar v, entry_kind k)
|
||||
: m_s(s), e(e), v(v), k(k) {}
|
||||
void undo() override {
|
||||
m_s.pop_viable(e, v, k);
|
||||
}
|
||||
};
|
||||
|
||||
struct viable::push_viable_trail : public trail {
|
||||
viable& m_s;
|
||||
entry* e;
|
||||
pvar v;
|
||||
entry_kind k;
|
||||
public:
|
||||
push_viable_trail(viable& s, entry* e, pvar v, entry_kind k)
|
||||
: m_s(s), e(e), v(v), k(k) {}
|
||||
void undo() override {
|
||||
m_s.push_viable(e, v, k);
|
||||
}
|
||||
};
|
||||
|
||||
viable::entry* viable::alloc_entry(pvar var) {
|
||||
if (m_alloc.empty())
|
||||
return alloc(entry);
|
||||
auto* e = m_alloc.back();
|
||||
e->reset();
|
||||
e->var = var;
|
||||
m_alloc.pop_back();
|
||||
return e;
|
||||
}
|
||||
|
||||
find_t viable::find_viable(pvar v, rational& out_val) {
|
||||
ensure_var(v);
|
||||
throw default_exception("nyi");
|
||||
}
|
||||
|
||||
/*
|
||||
* Explain why the current variable is not viable or signleton.
|
||||
*/
|
||||
dependency_vector viable::explain() { throw default_exception("nyi"); }
|
||||
|
||||
/*
|
||||
* Register constraint at index 'idx' as unitary in v.
|
||||
*/
|
||||
void viable::add_unitary(pvar v, unsigned idx) {
|
||||
|
||||
ensure_var(v);
|
||||
|
||||
if (c.is_assigned(v))
|
||||
return;
|
||||
auto [sc, d] = c.m_constraint_trail[idx];
|
||||
|
||||
entry* ne = alloc_entry(v);
|
||||
if (!m_forbidden_intervals.get_interval(sc, v, *ne)) {
|
||||
m_alloc.push_back(ne);
|
||||
return;
|
||||
}
|
||||
|
||||
if (ne->interval.is_currently_empty()) {
|
||||
m_alloc.push_back(ne);
|
||||
return;
|
||||
}
|
||||
|
||||
if (ne->coeff == 1) {
|
||||
intersect(v, ne);
|
||||
return;
|
||||
}
|
||||
else if (ne->coeff == -1) {
|
||||
insert(ne, v, m_diseq_lin, entry_kind::diseq_e);
|
||||
return;
|
||||
}
|
||||
else {
|
||||
unsigned const w = c.size(v);
|
||||
unsigned const k = ne->coeff.parity(w);
|
||||
// unsigned const lo_parity = ne->interval.lo_val().parity(w);
|
||||
// unsigned const hi_parity = ne->interval.hi_val().parity(w);
|
||||
|
||||
display_one(std::cerr << "try to reduce entry: ", v, ne) << "\n";
|
||||
|
||||
if (k > 0 && ne->coeff.is_power_of_two()) {
|
||||
// reduction of coeff gives us a unit entry
|
||||
//
|
||||
// 2^k a x \not\in [ lo ; hi [
|
||||
//
|
||||
// new_lo = lo[w-1:k] if lo[k-1:0] = 0
|
||||
// lo[w-1:k] + 1 otherwise
|
||||
//
|
||||
// new_hi = hi[w-1:k] if hi[k-1:0] = 0
|
||||
// hi[w-1:k] + 1 otherwise
|
||||
//
|
||||
// Reference: Fig. 1 (dtrim) in BitvectorsMCSAT
|
||||
//
|
||||
pdd const& pdd_lo = ne->interval.lo();
|
||||
pdd const& pdd_hi = ne->interval.hi();
|
||||
rational const& lo = ne->interval.lo_val();
|
||||
rational const& hi = ne->interval.hi_val();
|
||||
|
||||
rational new_lo = machine_div2k(lo, k);
|
||||
if (mod2k(lo, k).is_zero())
|
||||
ne->side_cond.push_back(cs.eq(pdd_lo * rational::power_of_two(w - k)));
|
||||
else {
|
||||
new_lo += 1;
|
||||
ne->side_cond.push_back(~cs.eq(pdd_lo * rational::power_of_two(w - k)));
|
||||
}
|
||||
|
||||
rational new_hi = machine_div2k(hi, k);
|
||||
if (mod2k(hi, k).is_zero())
|
||||
ne->side_cond.push_back(cs.eq(pdd_hi * rational::power_of_two(w - k)));
|
||||
else {
|
||||
new_hi += 1;
|
||||
ne->side_cond.push_back(~cs.eq(pdd_hi * rational::power_of_two(w - k)));
|
||||
}
|
||||
|
||||
// we have to update also the pdd bounds accordingly, but it seems not worth introducing new variables for this eagerly
|
||||
// new_lo = lo[:k] etc.
|
||||
// TODO: for now just disable the FI-lemma if this case occurs
|
||||
ne->valid_for_lemma = false;
|
||||
|
||||
if (new_lo == new_hi) {
|
||||
// empty or full
|
||||
// if (ne->interval.currently_contains(rational::zero()))
|
||||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
|
||||
ne->coeff = machine_div2k(ne->coeff, k);
|
||||
ne->interval = eval_interval::proper(pdd_lo, new_lo, pdd_hi, new_hi);
|
||||
ne->bit_width -= k;
|
||||
display_one(std::cerr << "reduced entry: ", v, ne) << "\n";
|
||||
LOG("reduced entry to unit in bitwidth " << ne->bit_width);
|
||||
intersect(v, ne);
|
||||
}
|
||||
|
||||
// TODO: later, can reduce according to shared_parity
|
||||
// unsigned const shared_parity = std::min(coeff_parity, std::min(lo_parity, hi_parity));
|
||||
|
||||
insert(ne, v, m_equal_lin, entry_kind::equal_e);
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
||||
void viable::ensure_var(pvar v) {
|
||||
while (v >= m_units.size()) {
|
||||
m_units.push_back(layers());
|
||||
m_equal_lin.push_back(nullptr);
|
||||
m_diseq_lin.push_back(nullptr);
|
||||
}
|
||||
}
|
||||
|
||||
bool viable::intersect(pvar v, entry* ne) {
|
||||
SASSERT(!c.is_assigned(v));
|
||||
SASSERT(!ne->src.empty());
|
||||
entry*& entries = m_units[v].ensure_layer(ne->bit_width).entries;
|
||||
entry* e = entries;
|
||||
if (e && e->interval.is_full()) {
|
||||
m_alloc.push_back(ne);
|
||||
return false;
|
||||
}
|
||||
|
||||
if (ne->interval.is_currently_empty()) {
|
||||
m_alloc.push_back(ne);
|
||||
return false;
|
||||
}
|
||||
|
||||
auto create_entry = [&]() {
|
||||
c.trail().push(pop_viable_trail(*this, ne, v, entry_kind::unit_e));
|
||||
ne->init(ne);
|
||||
return ne;
|
||||
};
|
||||
|
||||
auto remove_entry = [&](entry* e) {
|
||||
c.trail().push(push_viable_trail(*this, e, v, entry_kind::unit_e));
|
||||
e->remove_from(entries, e);
|
||||
e->active = false;
|
||||
};
|
||||
|
||||
if (ne->interval.is_full()) {
|
||||
// for (auto const& l : m_units[v].get_layers())
|
||||
// while (l.entries)
|
||||
// remove_entry(l.entries);
|
||||
while (entries)
|
||||
remove_entry(entries);
|
||||
entries = create_entry();
|
||||
return true;
|
||||
}
|
||||
|
||||
if (!e)
|
||||
entries = create_entry();
|
||||
else {
|
||||
entry* first = e;
|
||||
do {
|
||||
if (e->interval.currently_contains(ne->interval)) {
|
||||
m_alloc.push_back(ne);
|
||||
return false;
|
||||
}
|
||||
while (ne->interval.currently_contains(e->interval)) {
|
||||
entry* n = e->next();
|
||||
remove_entry(e);
|
||||
if (!entries) {
|
||||
entries = create_entry();
|
||||
return true;
|
||||
}
|
||||
if (e == first)
|
||||
first = n;
|
||||
e = n;
|
||||
}
|
||||
SASSERT(e->interval.lo_val() != ne->interval.lo_val());
|
||||
if (e->interval.lo_val() > ne->interval.lo_val()) {
|
||||
if (first->prev()->interval.currently_contains(ne->interval)) {
|
||||
m_alloc.push_back(ne);
|
||||
return false;
|
||||
}
|
||||
e->insert_before(create_entry());
|
||||
if (e == first)
|
||||
entries = e->prev();
|
||||
SASSERT(well_formed(m_units[v]));
|
||||
return true;
|
||||
}
|
||||
e = e->next();
|
||||
} while (e != first);
|
||||
// otherwise, append to end of list
|
||||
first->insert_before(create_entry());
|
||||
}
|
||||
SASSERT(well_formed(m_units[v]));
|
||||
return true;
|
||||
}
|
||||
|
||||
void viable::log() {
|
||||
for (pvar v = 0; v < m_units.size(); ++v)
|
||||
log(v);
|
||||
}
|
||||
|
||||
void viable::log(pvar v) {
|
||||
throw default_exception("nyi");
|
||||
}
|
||||
|
||||
|
||||
viable::layer& viable::layers::ensure_layer(unsigned bit_width) {
|
||||
for (unsigned i = 0; i < m_layers.size(); ++i) {
|
||||
layer& l = m_layers[i];
|
||||
if (l.bit_width == bit_width)
|
||||
return l;
|
||||
else if (l.bit_width < bit_width) {
|
||||
m_layers.push_back(layer(0));
|
||||
for (unsigned j = m_layers.size(); --j > i; )
|
||||
m_layers[j] = m_layers[j - 1];
|
||||
m_layers[i] = layer(bit_width);
|
||||
return m_layers[i];
|
||||
}
|
||||
}
|
||||
m_layers.push_back(layer(bit_width));
|
||||
return m_layers.back();
|
||||
}
|
||||
|
||||
viable::layer* viable::layers::get_layer(unsigned bit_width) {
|
||||
return const_cast<layer*>(std::as_const(*this).get_layer(bit_width));
|
||||
}
|
||||
|
||||
viable::layer const* viable::layers::get_layer(unsigned bit_width) const {
|
||||
for (layer const& l : m_layers)
|
||||
if (l.bit_width == bit_width)
|
||||
return &l;
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
void viable::pop_viable(entry* e, pvar v, entry_kind k) {
|
||||
SASSERT(well_formed(m_units[v]));
|
||||
SASSERT(e->active);
|
||||
e->active = false;
|
||||
switch (k) {
|
||||
case entry_kind::unit_e:
|
||||
entry::remove_from(m_units[v].get_layer(e)->entries, e);
|
||||
SASSERT(well_formed(m_units[v]));
|
||||
break;
|
||||
case entry_kind::equal_e:
|
||||
entry::remove_from(m_equal_lin[v], e);
|
||||
break;
|
||||
case entry_kind::diseq_e:
|
||||
entry::remove_from(m_diseq_lin[v], e);
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
break;
|
||||
}
|
||||
m_alloc.push_back(e);
|
||||
}
|
||||
|
||||
void viable::push_viable(entry* e, pvar v, entry_kind k) {
|
||||
// display_one(verbose_stream() << "Push entry: ", v, e) << "\n";
|
||||
entry*& entries = m_units[v].get_layer(e)->entries;
|
||||
SASSERT(e->prev() != e || !entries);
|
||||
SASSERT(e->prev() != e || e->next() == e);
|
||||
SASSERT(k == entry_kind::unit_e);
|
||||
SASSERT(!e->active);
|
||||
e->active = true;
|
||||
(void)k;
|
||||
SASSERT(well_formed(m_units[v]));
|
||||
if (e->prev() != e) {
|
||||
entry* pos = e->prev();
|
||||
e->init(e);
|
||||
pos->insert_after(e);
|
||||
if (e->interval.lo_val() < entries->interval.lo_val())
|
||||
entries = e;
|
||||
}
|
||||
else
|
||||
entries = e;
|
||||
SASSERT(well_formed(m_units[v]));
|
||||
}
|
||||
|
||||
void viable::insert(entry* e, pvar v, ptr_vector<entry>& entries, entry_kind k) {
|
||||
SASSERT(well_formed(m_units[v]));
|
||||
|
||||
c.trail().push(pop_viable_trail(*this, e, v, k));
|
||||
|
||||
e->init(e);
|
||||
if (!entries[v])
|
||||
entries[v] = e;
|
||||
else
|
||||
e->insert_after(entries[v]);
|
||||
SASSERT(entries[v]->invariant());
|
||||
SASSERT(well_formed(m_units[v]));
|
||||
}
|
||||
|
||||
|
||||
std::ostream& viable::display_one(std::ostream& out, pvar v, entry const* e) const {
|
||||
auto& m = c.var2pdd(v);
|
||||
if (e->coeff == -1) {
|
||||
// p*val + q > r*val + s if e->src.is_positive()
|
||||
// p*val + q >= r*val + s if e->src.is_negative()
|
||||
// Note that e->interval is meaningless in this case,
|
||||
// we just use it to transport the values p,q,r,s
|
||||
rational const& p = e->interval.lo_val();
|
||||
rational const& q_ = e->interval.lo().val();
|
||||
rational const& r = e->interval.hi_val();
|
||||
rational const& s_ = e->interval.hi().val();
|
||||
out << "[ ";
|
||||
out << val_pp(m, p, true) << "*v" << v << " + " << val_pp(m, q_);
|
||||
out << (e->src[0].is_positive() ? " > " : " >= ");
|
||||
out << val_pp(m, r, true) << "*v" << v << " + " << val_pp(m, s_);
|
||||
out << " ] ";
|
||||
}
|
||||
else if (e->coeff != 1)
|
||||
out << e->coeff << " * v" << v << " " << e->interval << " ";
|
||||
else
|
||||
out << e->interval << " ";
|
||||
if (e->side_cond.size() <= 5)
|
||||
out << e->side_cond << " ";
|
||||
else
|
||||
out << e->side_cond.size() << " side-conditions ";
|
||||
unsigned count = 0;
|
||||
for (const auto& src : e->src) {
|
||||
++count;
|
||||
out << src << "; ";
|
||||
if (count > 10) {
|
||||
out << " ...";
|
||||
break;
|
||||
}
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& viable::display_all(std::ostream& out, pvar v, entry const* e, char const* delimiter) const {
|
||||
if (!e)
|
||||
return out;
|
||||
entry const* first = e;
|
||||
unsigned count = 0;
|
||||
do {
|
||||
display_one(out, v, e) << delimiter;
|
||||
e = e->next();
|
||||
++count;
|
||||
if (count > 10) {
|
||||
out << " ...";
|
||||
break;
|
||||
}
|
||||
}
|
||||
while (e != first);
|
||||
return out;
|
||||
}
|
||||
|
||||
/*
|
||||
* Lower bounds are strictly ascending.
|
||||
* Intervals don't contain each-other (since lower bounds are ascending, it suffices to check containment in one direction).
|
||||
*/
|
||||
bool viable::well_formed(entry* e) {
|
||||
if (!e)
|
||||
return true;
|
||||
entry* first = e;
|
||||
while (true) {
|
||||
if (!e->active)
|
||||
return false;
|
||||
|
||||
if (e->interval.is_full())
|
||||
return e->next() == e;
|
||||
if (e->interval.is_currently_empty())
|
||||
return false;
|
||||
|
||||
auto* n = e->next();
|
||||
if (n != e && e->interval.currently_contains(n->interval))
|
||||
return false;
|
||||
|
||||
if (n == first)
|
||||
break;
|
||||
if (e->interval.lo_val() >= n->interval.lo_val())
|
||||
return false;
|
||||
e = n;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
/*
|
||||
* Layers are ordered in strictly descending bit-width.
|
||||
* Entries in each layer are well-formed.
|
||||
*/
|
||||
bool viable::well_formed(layers const& ls) {
|
||||
unsigned prev_width = std::numeric_limits<unsigned>::max();
|
||||
for (layer const& l : ls.get_layers()) {
|
||||
if (!well_formed(l.entries))
|
||||
return false;
|
||||
if (!all_of(dll_elements(l.entries), [&l](entry const& e) { return e.bit_width == l.bit_width; }))
|
||||
return false;
|
||||
if (prev_width <= l.bit_width)
|
||||
return false;
|
||||
prev_width = l.bit_width;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
}
|
||||
132
src/sat/smt/polysat/polysat_viable.h
Normal file
132
src/sat/smt/polysat/polysat_viable.h
Normal file
|
|
@ -0,0 +1,132 @@
|
|||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
maintain viable domains
|
||||
It uses the interval extraction functions from forbidden intervals.
|
||||
An empty viable set corresponds directly to a conflict that does not rely on
|
||||
the non-viable variable.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-06
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
|
||||
#include "util/rational.h"
|
||||
#include "util/dlist.h"
|
||||
#include "util/map.h"
|
||||
#include "util/small_object_allocator.h"
|
||||
|
||||
#include "sat/smt/polysat/polysat_types.h"
|
||||
#include "sat/smt/polysat/polysat_fi.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
enum class find_t {
|
||||
empty,
|
||||
singleton,
|
||||
multiple,
|
||||
resource_out,
|
||||
};
|
||||
|
||||
class core;
|
||||
class constraints;
|
||||
|
||||
std::ostream& operator<<(std::ostream& out, find_t x);
|
||||
|
||||
class viable {
|
||||
core& c;
|
||||
constraints& cs;
|
||||
forbidden_intervals m_forbidden_intervals;
|
||||
|
||||
struct entry final : public dll_base<entry>, public fi_record {
|
||||
/// whether the entry has been created by refinement (from constraints in 'fi_record::src')
|
||||
bool refined = false;
|
||||
/// whether the entry is part of the current set of intervals, or stashed away for backtracking
|
||||
bool active = true;
|
||||
bool valid_for_lemma = true;
|
||||
pvar var = null_var;
|
||||
|
||||
void reset() {
|
||||
// dll_base<entry>::init(this); // we never did this in alloc_entry either
|
||||
fi_record::reset();
|
||||
refined = false;
|
||||
active = true;
|
||||
valid_for_lemma = true;
|
||||
var = null_var;
|
||||
}
|
||||
};
|
||||
|
||||
enum class entry_kind { unit_e, equal_e, diseq_e };
|
||||
|
||||
struct layer final {
|
||||
entry* entries = nullptr;
|
||||
unsigned bit_width = 0;
|
||||
layer(unsigned bw) : bit_width(bw) {}
|
||||
};
|
||||
|
||||
class layers final {
|
||||
svector<layer> m_layers;
|
||||
public:
|
||||
svector<layer> const& get_layers() const { return m_layers; }
|
||||
layer& ensure_layer(unsigned bit_width);
|
||||
layer* get_layer(unsigned bit_width);
|
||||
layer* get_layer(entry* e) { return get_layer(e->bit_width); }
|
||||
layer const* get_layer(unsigned bit_width) const;
|
||||
layer const* get_layer(entry* e) const { return get_layer(e->bit_width); }
|
||||
entry* get_entries(unsigned bit_width) const { layer const* l = get_layer(bit_width); return l ? l->entries : nullptr; }
|
||||
};
|
||||
|
||||
ptr_vector<entry> m_alloc;
|
||||
vector<layers> m_units; // set of viable values based on unit multipliers, layered by bit-width in descending order
|
||||
ptr_vector<entry> m_equal_lin; // entries that have non-unit multipliers, but are equal
|
||||
ptr_vector<entry> m_diseq_lin; // entries that have distinct non-zero multipliers
|
||||
|
||||
bool well_formed(entry* e);
|
||||
bool well_formed(layers const& ls);
|
||||
|
||||
entry* alloc_entry(pvar v);
|
||||
|
||||
std::ostream& display_one(std::ostream& out, pvar v, entry const* e) const;
|
||||
std::ostream& display_all(std::ostream& out, pvar v, entry const* e, char const* delimiter = "") const;
|
||||
void log();
|
||||
void log(pvar v);
|
||||
|
||||
struct pop_viable_trail;
|
||||
void pop_viable(entry* e, pvar v, entry_kind k);
|
||||
struct push_viable_trail;
|
||||
void push_viable(entry* e, pvar v, entry_kind k);
|
||||
|
||||
void insert(entry* e, pvar v, ptr_vector<entry>& entries, entry_kind k);
|
||||
|
||||
bool intersect(pvar v, entry* e);
|
||||
|
||||
void ensure_var(pvar v);
|
||||
|
||||
public:
|
||||
viable(core& c);
|
||||
|
||||
~viable();
|
||||
|
||||
/**
|
||||
* Find a next viable value for variable.
|
||||
*/
|
||||
find_t find_viable(pvar v, rational& out_val);
|
||||
|
||||
/*
|
||||
* Explain why the current variable is not viable or signleton.
|
||||
*/
|
||||
dependency_vector explain();
|
||||
|
||||
/*
|
||||
* Register constraint at index 'idx' as unitary in v.
|
||||
*/
|
||||
void add_unitary(pvar v, unsigned idx);
|
||||
|
||||
};
|
||||
|
||||
}
|
||||
Loading…
Add table
Add a link
Reference in a new issue