mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 17:15:31 +00:00
remove stale files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
7c5996c2f0
commit
01e5d2dbf1
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