mirror of
https://github.com/Z3Prover/z3
synced 2025-06-25 15:23:41 +00:00
remove stale files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
54160d2efe
commit
7bcb4936c7
6 changed files with 0 additions and 734 deletions
|
|
@ -1,119 +0,0 @@
|
||||||
/*++
|
|
||||||
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_assignment.h"
|
|
||||||
#include "sat/smt/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;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,120 +0,0 @@
|
||||||
/*++
|
|
||||||
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_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); }
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
@ -1,25 +0,0 @@
|
||||||
/*++
|
|
||||||
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_core.h"
|
|
||||||
#include "sat/smt/polysat_solver.h"
|
|
||||||
#include "sat/smt/polysat_constraints.h"
|
|
||||||
|
|
||||||
namespace polysat {
|
|
||||||
|
|
||||||
signed_constraint constraints::ule(pdd const& p, pdd const& q) {
|
|
||||||
auto* c = alloc(ule_constraint, p, q);
|
|
||||||
m_trail.push(new_obj_trail(c));
|
|
||||||
return signed_constraint(ckind_t::ule_t, c);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,128 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2021 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
polysat constraints
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
|
||||||
Jakob Rath 2021-04-06
|
|
||||||
|
|
||||||
--*/
|
|
||||||
|
|
||||||
|
|
||||||
#pragma once
|
|
||||||
#include "sat/smt/polysat_types.h"
|
|
||||||
|
|
||||||
namespace polysat {
|
|
||||||
|
|
||||||
class core;
|
|
||||||
|
|
||||||
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); }
|
|
||||||
};
|
|
||||||
|
|
||||||
class ule_constraint : public constraint {
|
|
||||||
pdd m_lhs, m_rhs;
|
|
||||||
public:
|
|
||||||
ule_constraint(pdd const& lhs, pdd const& rhs) : m_lhs(lhs), m_rhs(rhs) {}
|
|
||||||
};
|
|
||||||
|
|
||||||
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; }
|
|
||||||
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); }
|
|
||||||
bool is_ule() const { return m_op == ule_t; }
|
|
||||||
ule_constraint& to_ule() { return *reinterpret_cast<ule_constraint*>(m_constraint); }
|
|
||||||
bool is_eq(pvar& v, rational& val) { throw default_exception("nyi"); }
|
|
||||||
};
|
|
||||||
|
|
||||||
using dependent_constraint = std::pair<signed_constraint, stacked_dependency*>;
|
|
||||||
|
|
||||||
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) { throw default_exception("nyi"); }
|
|
||||||
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); }
|
|
||||||
};
|
|
||||||
}
|
|
||||||
|
|
@ -1,212 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2021 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
polysat substitution
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
|
||||||
Jakob Rath 2021-04-06
|
|
||||||
|
|
||||||
--*/
|
|
||||||
#pragma once
|
|
||||||
#include "sat/smt/polysat_types.h"
|
|
||||||
|
|
||||||
namespace polysat {
|
|
||||||
|
|
||||||
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 {
|
|
||||||
vector<assignment_item_t> m_pairs;
|
|
||||||
mutable scoped_ptr_vector<substitution> m_subst;
|
|
||||||
vector<substitution> m_subst_trail;
|
|
||||||
|
|
||||||
substitution& subst(unsigned sz);
|
|
||||||
solver& s() const { return *m_solver; }
|
|
||||||
public:
|
|
||||||
assignment(solver& 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); }
|
|
||||||
}
|
|
||||||
|
|
||||||
namespace polysat {
|
|
||||||
|
|
||||||
enum class search_item_k
|
|
||||||
{
|
|
||||||
assignment,
|
|
||||||
boolean,
|
|
||||||
};
|
|
||||||
|
|
||||||
class search_item {
|
|
||||||
search_item_k m_kind;
|
|
||||||
union {
|
|
||||||
pvar m_var;
|
|
||||||
sat::literal m_lit;
|
|
||||||
};
|
|
||||||
bool m_resolved = false; // when marked as resolved it is no longer valid to reduce the conflict state
|
|
||||||
|
|
||||||
search_item(pvar var): m_kind(search_item_k::assignment), m_var(var) {}
|
|
||||||
search_item(sat::literal lit): m_kind(search_item_k::boolean), m_lit(lit) {}
|
|
||||||
public:
|
|
||||||
static search_item assignment(pvar var) { return search_item(var); }
|
|
||||||
static search_item boolean(sat::literal lit) { return search_item(lit); }
|
|
||||||
bool is_assignment() const { return m_kind == search_item_k::assignment; }
|
|
||||||
bool is_boolean() const { return m_kind == search_item_k::boolean; }
|
|
||||||
bool is_resolved() const { return m_resolved; }
|
|
||||||
search_item_k kind() const { return m_kind; }
|
|
||||||
pvar var() const { SASSERT(is_assignment()); return m_var; }
|
|
||||||
sat::literal lit() const { SASSERT(is_boolean()); return m_lit; }
|
|
||||||
void set_resolved() { m_resolved = true; }
|
|
||||||
};
|
|
||||||
|
|
||||||
class search_state {
|
|
||||||
solver& s;
|
|
||||||
|
|
||||||
vector<search_item> m_items;
|
|
||||||
assignment m_assignment;
|
|
||||||
|
|
||||||
// store index into m_items
|
|
||||||
unsigned_vector m_pvar_to_idx;
|
|
||||||
unsigned_vector m_bool_to_idx;
|
|
||||||
|
|
||||||
bool value(pvar v, rational& r) const;
|
|
||||||
|
|
||||||
public:
|
|
||||||
search_state(solver& s): s(s), m_assignment(s) {}
|
|
||||||
unsigned size() const { return m_items.size(); }
|
|
||||||
search_item const& back() const { return m_items.back(); }
|
|
||||||
search_item const& operator[](unsigned i) const { return m_items[i]; }
|
|
||||||
|
|
||||||
assignment const& get_assignment() const { return m_assignment; }
|
|
||||||
substitution const& subst(unsigned sz) const { return m_assignment.subst(sz); }
|
|
||||||
|
|
||||||
// TODO: implement the following method if we actually need the assignments without resolved items already during conflict resolution
|
|
||||||
// (no separate trail needed, just a second m_subst and an index into the trail, I think)
|
|
||||||
// (update on set_resolved? might be one iteration too early, looking at the old solver::resolve_conflict loop)
|
|
||||||
substitution const& unresolved_assignment(unsigned sz) const;
|
|
||||||
|
|
||||||
void push_assignment(pvar v, rational const& r);
|
|
||||||
void push_boolean(sat::literal lit);
|
|
||||||
void pop();
|
|
||||||
|
|
||||||
unsigned get_pvar_index(pvar v) const;
|
|
||||||
unsigned get_bool_index(sat::bool_var var) const;
|
|
||||||
unsigned get_bool_index(sat::literal lit) const { return get_bool_index(lit.var()); }
|
|
||||||
|
|
||||||
void set_resolved(unsigned i) { m_items[i].set_resolved(); }
|
|
||||||
|
|
||||||
using const_iterator = decltype(m_items)::const_iterator;
|
|
||||||
const_iterator begin() const { return m_items.begin(); }
|
|
||||||
const_iterator end() const { return m_items.end(); }
|
|
||||||
|
|
||||||
std::ostream& display(std::ostream& out) const;
|
|
||||||
std::ostream& display(search_item const& item, std::ostream& out) const;
|
|
||||||
std::ostream& display_verbose(std::ostream& out) const;
|
|
||||||
std::ostream& display_verbose(search_item const& item, std::ostream& out) const;
|
|
||||||
};
|
|
||||||
|
|
||||||
struct search_state_pp {
|
|
||||||
search_state const& s;
|
|
||||||
bool verbose;
|
|
||||||
search_state_pp(search_state const& s, bool verbose = false) : s(s), verbose(verbose) {}
|
|
||||||
};
|
|
||||||
|
|
||||||
struct search_item_pp {
|
|
||||||
search_state const& s;
|
|
||||||
search_item const& i;
|
|
||||||
bool verbose;
|
|
||||||
search_item_pp(search_state const& s, search_item const& i, bool verbose = false) : s(s), i(i), verbose(verbose) {}
|
|
||||||
};
|
|
||||||
|
|
||||||
inline std::ostream& operator<<(std::ostream& out, search_state const& s) { return s.display(out); }
|
|
||||||
|
|
||||||
inline std::ostream& operator<<(std::ostream& out, search_state_pp const& p) { return p.verbose ? p.s.display_verbose(out) : p.s.display(out); }
|
|
||||||
|
|
||||||
inline std::ostream& operator<<(std::ostream& out, search_item_pp const& p) { return p.verbose ? p.s.display_verbose(p.i, out) : p.s.display(p.i, out); }
|
|
||||||
|
|
||||||
}
|
|
||||||
|
|
@ -1,130 +0,0 @@
|
||||||
/*++
|
|
||||||
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_types.h"
|
|
||||||
#include "sat/smt/polysat_fi.h"
|
|
||||||
|
|
||||||
namespace polysat {
|
|
||||||
|
|
||||||
enum class find_t {
|
|
||||||
empty,
|
|
||||||
singleton,
|
|
||||||
multiple,
|
|
||||||
resource_out,
|
|
||||||
};
|
|
||||||
|
|
||||||
class core;
|
|
||||||
class constraints;
|
|
||||||
|
|
||||||
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