mirror of
https://github.com/Z3Prover/z3
synced 2025-06-22 22:03:39 +00:00
remove stale files
This commit is contained in:
Nikolaj Bjorner
parent
81c6f00c99
commit
faa6c14610
2 changed files with 0 additions and 436 deletions
|
|
@ -1,224 +0,0 @@
|
||||||
/*++
|
|
||||||
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_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()) << "[";
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
}
|
|
||||||
|
|
@ -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); }
|
|
||||||
|
|
||||||
}
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue