mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 17:15:31 +00:00
v2 of polysat
This commit is contained in:
Nikolaj Bjorner
parent
064832e891
commit
c11f558451
10 changed files with 1108 additions and 526 deletions
119
src/sat/smt/polysat_assignment.cpp
Normal file
119
src/sat/smt/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_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;
|
||||
}
|
||||
}
|
||||
120
src/sat/smt/polysat_assignment.h
Normal file
120
src/sat/smt/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_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); }
|
||||
}
|
||||
|
||||
25
src/sat/smt/polysat_constraints.cpp
Normal file
25
src/sat/smt/polysat_constraints.cpp
Normal file
|
|
@ -0,0 +1,25 @@
|
|||
/*++
|
||||
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);
|
||||
}
|
||||
}
|
||||
128
src/sat/smt/polysat_constraints.h
Normal file
128
src/sat/smt/polysat_constraints.h
Normal file
|
|
@ -0,0 +1,128 @@
|
|||
/*++
|
||||
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); }
|
||||
};
|
||||
}
|
||||
276
src/sat/smt/polysat_core.cpp
Normal file
276
src/sat/smt/polysat_core.cpp
Normal file
|
|
@ -0,0 +1,276 @@
|
|||
/*++
|
||||
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_solver.h"
|
||||
#include "sat/smt/euf_solver.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] = nullptr;
|
||||
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;
|
||||
unsigned m_idx;
|
||||
public:
|
||||
mk_add_watch(core& c, unsigned idx) : c(c), m_idx(idx) {}
|
||||
void undo() override {
|
||||
auto& sc = c.m_prop_queue[m_idx].first;
|
||||
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();
|
||||
}
|
||||
};
|
||||
|
||||
core::core(solver& s) :
|
||||
s(s),
|
||||
m_viable(*this),
|
||||
m_constraints(s.get_trail_stack()),
|
||||
m_assignment(*this),
|
||||
m_dep(s.get_region()),
|
||||
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(nullptr);
|
||||
m_watch.push_back({});
|
||||
m_var_queue.mk_var_eh(v);
|
||||
s.ctx.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);
|
||||
}
|
||||
|
||||
// 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.ctx.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:
|
||||
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.ctx.push(value_trail(m_qhead));
|
||||
for (; m_qhead < m_prop_queue.size() && !s.ctx.inconsistent(); ++m_qhead)
|
||||
propagate_constraint(m_qhead, m_prop_queue[m_qhead]);
|
||||
s.ctx.push(value_trail(m_vqhead));
|
||||
for (; m_vqhead < m_prop_queue.size() && !s.ctx.inconsistent(); ++m_vqhead)
|
||||
propagate_value(m_vqhead, m_prop_queue[m_vqhead]);
|
||||
return true;
|
||||
}
|
||||
|
||||
void core::propagate_constraint(unsigned idx, dependent_constraint& dc) {
|
||||
auto [sc, dep] = dc;
|
||||
if (sc.is_eq(m_var, m_value)) {
|
||||
propagate_assignment(m_var, m_value, dep);
|
||||
return;
|
||||
}
|
||||
add_watch(idx, sc);
|
||||
}
|
||||
|
||||
void core::add_watch(unsigned idx, signed_constraint& sc) {
|
||||
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.ctx.push(mk_add_watch(*this, idx));
|
||||
}
|
||||
|
||||
void core::add_watch(unsigned idx, unsigned var) {
|
||||
m_watch[var].push_back(idx);
|
||||
}
|
||||
|
||||
void core::propagate_assignment(pvar v, rational const& value, stacked_dependency* dep) {
|
||||
if (is_assigned(v))
|
||||
return;
|
||||
if (m_var_queue.contains(v)) {
|
||||
m_var_queue.del_var_eh(v);
|
||||
s.ctx.push(mk_dqueue_var(v, *this));
|
||||
}
|
||||
m_values[v] = value;
|
||||
m_justification[v] = dep;
|
||||
m_assignment.push(v , value);
|
||||
s.ctx.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, dep] = m_prop_queue[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;
|
||||
}
|
||||
}
|
||||
if (!swapped) {
|
||||
m_watch[v][j++] = idx;
|
||||
}
|
||||
|
||||
// constraint is unitary, add to viable set
|
||||
if (vars.size() >= 2 && is_assigned(vars[0]) && !is_assigned(vars[1])) {
|
||||
// m_viable.add_unitary(vars[1], idx);
|
||||
}
|
||||
}
|
||||
m_watch[v].shrink(j);
|
||||
}
|
||||
|
||||
void core::propagate_value(unsigned idx, dependent_constraint const& dc) {
|
||||
auto [sc, dep] = dc;
|
||||
// check if sc evaluates to false
|
||||
switch (eval(sc)) {
|
||||
case l_true:
|
||||
return;
|
||||
case l_false:
|
||||
m_unsat_core = explain_eval(dc);
|
||||
propagate_unsat_core();
|
||||
return;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
// if sc is v == value, then check the watch list for v if they evaluate to false.
|
||||
if (sc.is_eq(m_var, m_value)) {
|
||||
for (auto idx : m_watch[m_var]) {
|
||||
auto [sc, dep] = m_prop_queue[idx];
|
||||
if (eval(sc) == l_false) {
|
||||
m_unsat_core = explain_eval({ sc, dep });
|
||||
propagate_unsat_core();
|
||||
return;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
throw default_exception("nyi");
|
||||
}
|
||||
|
||||
bool core::propagate_unsat_core() {
|
||||
// default is to use unsat core:
|
||||
s.set_conflict(m_unsat_core);
|
||||
// if core is based on viable, use s.set_lemma();
|
||||
throw default_exception("nyi");
|
||||
}
|
||||
|
||||
void core::assign_eh(signed_constraint const& sc, dependency const& dep) {
|
||||
m_prop_queue.push_back({ sc, m_dep.mk_leaf(dep) });
|
||||
s.ctx.push(push_back_vector(m_prop_queue));
|
||||
}
|
||||
|
||||
|
||||
|
||||
}
|
||||
128
src/sat/smt/polysat_core.h
Normal file
128
src/sat/smt/polysat_core.h
Normal file
|
|
@ -0,0 +1,128 @@
|
|||
/*++
|
||||
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_types.h"
|
||||
#include "sat/smt/polysat_constraints.h"
|
||||
#include "sat/smt/polysat_viable.h"
|
||||
#include "sat/smt/polysat_assignment.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
class core;
|
||||
class solver;
|
||||
|
||||
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;
|
||||
friend class viable;
|
||||
friend class constraints;
|
||||
friend class assignment;
|
||||
|
||||
solver& s;
|
||||
viable m_viable;
|
||||
constraints m_constraints;
|
||||
assignment m_assignment;
|
||||
unsigned m_qhead = 0, m_vqhead = 0;
|
||||
svector<dependent_constraint> m_prop_queue;
|
||||
stacked_dependency_manager<dependency> m_dep;
|
||||
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
|
||||
ptr_vector<stacked_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
|
||||
|
||||
vector<pdd> m_subst; // substitution, one for each size.
|
||||
|
||||
// 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;
|
||||
unsigned size(pvar v) const { return var2pdd(v).power_of_2(); }
|
||||
void del_var();
|
||||
|
||||
bool is_assigned(pvar v) { return nullptr != m_justification[v]; }
|
||||
void propagate_constraint(unsigned idx, dependent_constraint& dc);
|
||||
void propagate_value(unsigned idx, dependent_constraint const& dc);
|
||||
void propagate_assignment(pvar v, rational const& value, stacked_dependency* dep);
|
||||
bool propagate_unsat_core();
|
||||
|
||||
void add_watch(unsigned idx, signed_constraint& sc);
|
||||
void add_watch(unsigned idx, unsigned var);
|
||||
|
||||
lbool eval(signed_constraint sc) { throw default_exception("nyi"); }
|
||||
dependency_vector explain_eval(dependent_constraint const& dc) { throw default_exception("nyi"); }
|
||||
|
||||
public:
|
||||
core(solver& s);
|
||||
|
||||
sat::check_result check();
|
||||
|
||||
bool propagate();
|
||||
void assign_eh(signed_constraint const& sc, dependency const& dep);
|
||||
|
||||
expr_ref constraint2expr(signed_constraint const& sc) const { throw default_exception("nyi"); }
|
||||
|
||||
pdd value(rational const& v, unsigned sz);
|
||||
|
||||
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]; }
|
||||
|
||||
std::ostream& display(std::ostream& out) const { throw default_exception("nyi"); }
|
||||
};
|
||||
|
||||
}
|
||||
|
|
@ -1,526 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2022 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
polysat_internalize.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
PolySAT internalize
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2022-01-26
|
||||
|
||||
--*/
|
||||
|
||||
#include "params/bv_rewriter_params.hpp"
|
||||
#include "sat/smt/polysat_solver.h"
|
||||
#include "sat/smt/euf_solver.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
euf::theory_var solver::mk_var(euf::enode* n) {
|
||||
theory_var v = euf::th_euf_solver::mk_var(n);
|
||||
ctx.attach_th_var(n, this, v);
|
||||
return v;
|
||||
}
|
||||
|
||||
sat::literal solver::internalize(expr* e, bool sign, bool root) {
|
||||
force_push();
|
||||
SASSERT(m.is_bool(e));
|
||||
if (!visit_rec(m, e, sign, root))
|
||||
return sat::null_literal;
|
||||
sat::literal lit = expr2literal(e);
|
||||
if (sign)
|
||||
lit.neg();
|
||||
return lit;
|
||||
}
|
||||
|
||||
void solver::internalize(expr* e) {
|
||||
force_push();
|
||||
visit_rec(m, e, false, false);
|
||||
}
|
||||
|
||||
bool solver::visit(expr* e) {
|
||||
force_push();
|
||||
if (!is_app(e) || to_app(e)->get_family_id() != get_id()) {
|
||||
ctx.internalize(e);
|
||||
return true;
|
||||
}
|
||||
m_stack.push_back(sat::eframe(e));
|
||||
return false;
|
||||
}
|
||||
|
||||
bool solver::visited(expr* e) {
|
||||
euf::enode* n = expr2enode(e);
|
||||
return n && n->is_attached_to(get_id());
|
||||
}
|
||||
|
||||
bool solver::post_visit(expr* e, bool sign, bool root) {
|
||||
euf::enode* n = expr2enode(e);
|
||||
app* a = to_app(e);
|
||||
|
||||
if (visited(e))
|
||||
return true;
|
||||
|
||||
SASSERT(!n || !n->is_attached_to(get_id()));
|
||||
if (!n)
|
||||
n = mk_enode(e, false);
|
||||
|
||||
SASSERT(!n->is_attached_to(get_id()));
|
||||
mk_var(n);
|
||||
SASSERT(n->is_attached_to(get_id()));
|
||||
internalize_polysat(a);
|
||||
return true;
|
||||
}
|
||||
|
||||
void solver::internalize_polysat(app* a) {
|
||||
|
||||
#define if_unary(F) if (a->get_num_args() == 1) { internalize_unary(a, [&](pdd const& p) { return F(p); }); break; }
|
||||
|
||||
switch (a->get_decl_kind()) {
|
||||
case OP_BMUL: internalize_binary(a, [&](pdd const& p, pdd const& q) { return p * q; }); break;
|
||||
case OP_BADD: internalize_binary(a, [&](pdd const& p, pdd const& q) { return p + q; }); break;
|
||||
case OP_BSUB: internalize_binary(a, [&](pdd const& p, pdd const& q) { return p - q; }); break;
|
||||
case OP_BLSHR: internalize_lshr(a); break;
|
||||
case OP_BSHL: internalize_shl(a); break;
|
||||
case OP_BASHR: internalize_ashr(a); break;
|
||||
case OP_BAND: internalize_band(a); break;
|
||||
case OP_BOR: internalize_bor(a); break;
|
||||
case OP_BXOR: internalize_bxor(a); break;
|
||||
case OP_BNAND: if_unary(m_core.bnot); internalize_bnand(a); break;
|
||||
case OP_BNOR: if_unary(m_core.bnot); internalize_bnor(a); break;
|
||||
case OP_BXNOR: if_unary(m_core.bnot); internalize_bxnor(a); break;
|
||||
case OP_BNOT: internalize_unary(a, [&](pdd const& p) { return m_core.bnot(p); }); break;
|
||||
case OP_BNEG: internalize_unary(a, [&](pdd const& p) { return -p; }); break;
|
||||
case OP_MKBV: internalize_mkbv(a); break;
|
||||
case OP_BV_NUM: internalize_num(a); break;
|
||||
case OP_ULEQ: internalize_le<false, false, false>(a); break;
|
||||
case OP_SLEQ: internalize_le<true, false, false>(a); break;
|
||||
case OP_UGEQ: internalize_le<false, true, false>(a); break;
|
||||
case OP_SGEQ: internalize_le<true, true, false>(a); break;
|
||||
case OP_ULT: internalize_le<false, true, true>(a); break;
|
||||
case OP_SLT: internalize_le<true, true, true>(a); break;
|
||||
case OP_UGT: internalize_le<false, false, true>(a); break;
|
||||
case OP_SGT: internalize_le<true, false, true>(a); break;
|
||||
|
||||
case OP_BUMUL_NO_OVFL: internalize_binaryc(a, [&](pdd const& p, pdd const& q) { return m_core.umul_ovfl(p, q); }); break;
|
||||
case OP_BSMUL_NO_OVFL: internalize_binaryc(a, [&](pdd const& p, pdd const& q) { return m_core.smul_ovfl(p, q); }); break;
|
||||
case OP_BSMUL_NO_UDFL: internalize_binaryc(a, [&](pdd const& p, pdd const& q) { return m_core.smul_udfl(p, q); }); break;
|
||||
|
||||
case OP_BUMUL_OVFL:
|
||||
case OP_BSMUL_OVFL:
|
||||
case OP_BSDIV_OVFL:
|
||||
case OP_BNEG_OVFL:
|
||||
case OP_BUADD_OVFL:
|
||||
case OP_BSADD_OVFL:
|
||||
case OP_BUSUB_OVFL:
|
||||
case OP_BSSUB_OVFL:
|
||||
verbose_stream() << mk_pp(a, m) << "\n";
|
||||
// handled by bv_rewriter for now
|
||||
UNREACHABLE();
|
||||
break;
|
||||
|
||||
case OP_BUDIV_I: internalize_udiv_i(a); break;
|
||||
case OP_BUREM_I: internalize_urem_i(a); break;
|
||||
|
||||
case OP_BUDIV: internalize_div_rem(a, true); break;
|
||||
case OP_BUREM: internalize_div_rem(a, false); break;
|
||||
case OP_BSDIV0: UNREACHABLE(); break;
|
||||
case OP_BUDIV0: UNREACHABLE(); break;
|
||||
case OP_BSREM0: UNREACHABLE(); break;
|
||||
case OP_BUREM0: UNREACHABLE(); break;
|
||||
case OP_BSMOD0: UNREACHABLE(); break;
|
||||
|
||||
case OP_EXTRACT: internalize_extract(a); break;
|
||||
case OP_CONCAT: internalize_concat(a); break;
|
||||
case OP_ZERO_EXT: internalize_zero_extend(a); break;
|
||||
case OP_SIGN_EXT: internalize_sign_extend(a); break;
|
||||
|
||||
// polysat::solver should also support at least:
|
||||
case OP_BREDAND: // x == 2^K - 1 unary, return single bit, 1 if all input bits are set.
|
||||
case OP_BREDOR: // x > 0 unary, return single bit, 1 if at least one input bit is set.
|
||||
case OP_BCOMP: // x == y binary, return single bit, 1 if the arguments are equal.
|
||||
case OP_BSDIV:
|
||||
case OP_BSREM:
|
||||
case OP_BSMOD:
|
||||
case OP_BSDIV_I:
|
||||
case OP_BSREM_I:
|
||||
case OP_BSMOD_I:
|
||||
|
||||
IF_VERBOSE(0, verbose_stream() << mk_pp(a, m) << "\n");
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return;
|
||||
default:
|
||||
IF_VERBOSE(0, verbose_stream() << mk_pp(a, m) << "\n");
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return;
|
||||
}
|
||||
#undef if_unary
|
||||
}
|
||||
|
||||
class solver::mk_atom_trail : public trail {
|
||||
solver& th;
|
||||
sat::bool_var m_var;
|
||||
public:
|
||||
mk_atom_trail(sat::bool_var v, solver& th) : th(th), m_var(v) {}
|
||||
void undo() override {
|
||||
th.erase_bv2a(m_var);
|
||||
}
|
||||
};
|
||||
|
||||
void solver::mk_atom(sat::bool_var bv, signed_constraint& sc) {
|
||||
if (get_bv2a(bv))
|
||||
return;
|
||||
sat::literal lit(bv, false);
|
||||
auto index = m_core.register_constraint(sc, dependency(lit, 0));
|
||||
auto a = new (get_region()) atom(bv, index);
|
||||
insert_bv2a(bv, a);
|
||||
ctx.push(mk_atom_trail(bv, *this));
|
||||
}
|
||||
|
||||
void solver::internalize_binaryc(app* e, std::function<polysat::signed_constraint(pdd, pdd)> const& fn) {
|
||||
auto p = expr2pdd(e->get_arg(0));
|
||||
auto q = expr2pdd(e->get_arg(1));
|
||||
auto sc = ~fn(p, q);
|
||||
sat::literal lit = expr2literal(e);
|
||||
if (lit.sign())
|
||||
sc = ~sc;
|
||||
mk_atom(lit.var(), sc);
|
||||
}
|
||||
|
||||
void solver::internalize_udiv_i(app* e) {
|
||||
expr* x, *y;
|
||||
expr_ref rm(m);
|
||||
if (bv.is_bv_udivi(e, x, y))
|
||||
rm = bv.mk_bv_urem_i(x, y);
|
||||
else if (bv.is_bv_udiv(e, x, y))
|
||||
rm = bv.mk_bv_urem(x, y);
|
||||
else
|
||||
UNREACHABLE();
|
||||
internalize(rm);
|
||||
}
|
||||
|
||||
// From "Hacker's Delight", section 2-2. Addition Combined with Logical Operations;
|
||||
// found via Int-Blasting paper; see https://doi.org/10.1007/978-3-030-94583-1_24
|
||||
// (p + q) - band(p, q);
|
||||
void solver::internalize_bor(app* n) {
|
||||
internalize_binary(n, [&](expr* const& x, expr* const& y) { return bv.mk_bv_sub(bv.mk_bv_add(x, y), bv.mk_bv_and(x, y)); });
|
||||
}
|
||||
|
||||
// From "Hacker's Delight", section 2-2. Addition Combined with Logical Operations;
|
||||
// found via Int-Blasting paper; see https://doi.org/10.1007/978-3-030-94583-1_24
|
||||
// (p + q) - 2*band(p, q);
|
||||
void solver::internalize_bxor(app* n) {
|
||||
internalize_binary(n, [&](expr* const& x, expr* const& y) {
|
||||
return bv.mk_bv_sub(bv.mk_bv_add(x, y), bv.mk_bv_add(bv.mk_bv_and(x, y), bv.mk_bv_and(x, y)));
|
||||
});
|
||||
}
|
||||
|
||||
void solver::internalize_bnor(app* n) {
|
||||
internalize_binary(n, [&](expr* const& x, expr* const& y) { return bv.mk_bv_not(bv.mk_bv_or(x, y)); });
|
||||
}
|
||||
|
||||
void solver::internalize_bnand(app* n) {
|
||||
internalize_binary(n, [&](expr* const& x, expr* const& y) { return bv.mk_bv_not(bv.mk_bv_and(x, y)); });
|
||||
}
|
||||
|
||||
void solver::internalize_bxnor(app* n) {
|
||||
internalize_binary(n, [&](expr* const& x, expr* const& y) { return bv.mk_bv_not(bv.mk_bv_xor(x, y)); });
|
||||
}
|
||||
|
||||
void solver::internalize_band(app* n) {
|
||||
if (n->get_num_args() == 2) {
|
||||
expr* x, * y;
|
||||
VERIFY(bv.is_bv_and(n, x, y));
|
||||
m_core.band(expr2pdd(x), expr2pdd(y), expr2pdd(n));
|
||||
}
|
||||
else {
|
||||
expr_ref z(n->get_arg(0), m);
|
||||
for (unsigned i = 1; i < n->get_num_args(); ++i) {
|
||||
z = bv.mk_bv_and(z, n->get_arg(i));
|
||||
ctx.internalize(z);
|
||||
}
|
||||
internalize_set(n, expr2pdd(z));
|
||||
}
|
||||
}
|
||||
|
||||
void solver::internalize_lshr(app* n) {
|
||||
expr* x, * y;
|
||||
VERIFY(bv.is_bv_lshr(n, x, y));
|
||||
m_core.lshr(expr2pdd(x), expr2pdd(y), expr2pdd(n));
|
||||
}
|
||||
|
||||
void solver::internalize_ashr(app* n) {
|
||||
expr* x, * y;
|
||||
VERIFY(bv.is_bv_ashr(n, x, y));
|
||||
m_core.ashr(expr2pdd(x), expr2pdd(y), expr2pdd(n));
|
||||
}
|
||||
|
||||
void solver::internalize_shl(app* n) {
|
||||
expr* x, * y;
|
||||
VERIFY(bv.is_bv_shl(n, x, y));
|
||||
m_core.shl(expr2pdd(x), expr2pdd(y), expr2pdd(n));
|
||||
}
|
||||
|
||||
void solver::internalize_urem_i(app* rem) {
|
||||
expr* x, *y;
|
||||
euf::enode* n = expr2enode(rem);
|
||||
SASSERT(n && n->is_attached_to(get_id()));
|
||||
theory_var v = n->get_th_var(get_id());
|
||||
if (m_var2pdd_valid.get(v, false))
|
||||
return;
|
||||
expr_ref quot(m);
|
||||
if (bv.is_bv_uremi(rem, x, y))
|
||||
quot = bv.mk_bv_udiv_i(x, y);
|
||||
else if (bv.is_bv_urem(rem, x, y))
|
||||
quot = bv.mk_bv_udiv(x, y);
|
||||
else
|
||||
UNREACHABLE();
|
||||
m_var2pdd_valid.setx(v, true, false);
|
||||
ctx.internalize(quot);
|
||||
m_var2pdd_valid.setx(v, false, false);
|
||||
quot_rem(quot, rem, x, y);
|
||||
}
|
||||
|
||||
void solver::quot_rem(expr* quot, expr* rem, expr* x, expr* y) {
|
||||
pdd a = expr2pdd(x);
|
||||
pdd b = expr2pdd(y);
|
||||
euf::enode* qn = expr2enode(quot);
|
||||
euf::enode* rn = expr2enode(rem);
|
||||
auto& m = a.manager();
|
||||
unsigned sz = m.power_of_2();
|
||||
if (b.is_zero()) {
|
||||
// By SMT-LIB specification, b = 0 ==> q = -1, r = a.
|
||||
internalize_set(quot, m.mk_val(m.max_value()));
|
||||
internalize_set(rem, a);
|
||||
return;
|
||||
}
|
||||
if (b.is_one()) {
|
||||
internalize_set(quot, a);
|
||||
internalize_set(rem, m.zero());
|
||||
return;
|
||||
}
|
||||
|
||||
if (a.is_val() && b.is_val()) {
|
||||
rational const av = a.val();
|
||||
rational const bv = b.val();
|
||||
SASSERT(!bv.is_zero());
|
||||
rational rv;
|
||||
rational qv = machine_div_rem(av, bv, rv);
|
||||
pdd q = m.mk_val(qv);
|
||||
pdd r = m.mk_val(rv);
|
||||
SASSERT_EQ(a, b * q + r);
|
||||
SASSERT(b.val() * q.val() + r.val() <= m.max_value());
|
||||
SASSERT(r.val() <= (b * q + r).val());
|
||||
SASSERT(r.val() < b.val());
|
||||
internalize_set(quot, q);
|
||||
internalize_set(rem, r);
|
||||
return;
|
||||
}
|
||||
|
||||
pdd r = var2pdd(rn->get_th_var(get_id()));
|
||||
pdd q = var2pdd(qn->get_th_var(get_id()));
|
||||
|
||||
// Axioms for quotient/remainder
|
||||
//
|
||||
// a = b*q + r
|
||||
// multiplication does not overflow in b*q
|
||||
// addition does not overflow in (b*q) + r; for now expressed as: r <= bq+r
|
||||
// b ≠ 0 ==> r < b
|
||||
// b = 0 ==> q = -1
|
||||
// TODO: when a,b become evaluable, can we actually propagate q,r? doesn't seem like it.
|
||||
// Maybe we need something like an op_constraint for better propagation.
|
||||
add_polysat_clause("[axiom] quot_rem 1", { m_core.eq(b * q + r - a) }, false);
|
||||
add_polysat_clause("[axiom] quot_rem 2", { ~m_core.umul_ovfl(b, q) }, false);
|
||||
// r <= b*q+r
|
||||
// { apply equivalence: p <= q <=> q-p <= -p-1 }
|
||||
// b*q <= -r-1
|
||||
add_polysat_clause("[axiom] quot_rem 3", { m_core.ule(b * q, -r - 1) }, false);
|
||||
|
||||
auto c_eq = m_core.eq(b);
|
||||
if (!c_eq.is_always_true())
|
||||
add_polysat_clause("[axiom] quot_rem 4", { c_eq, ~m_core.ule(b, r) }, false);
|
||||
if (!c_eq.is_always_false())
|
||||
add_polysat_clause("[axiom] quot_rem 5", { ~c_eq, m_core.eq(q + 1) }, false);
|
||||
}
|
||||
|
||||
void solver::internalize_sign_extend(app* e) {
|
||||
expr* arg = e->get_arg(0);
|
||||
unsigned sz = bv.get_bv_size(e);
|
||||
unsigned arg_sz = bv.get_bv_size(arg);
|
||||
unsigned sz2 = sz - arg_sz;
|
||||
var2pdd(expr2enode(e)->get_th_var(get_id()));
|
||||
if (arg_sz == sz)
|
||||
add_clause(eq_internalize(e, arg), nullptr);
|
||||
else {
|
||||
sat::literal lt0 = ctx.mk_literal(bv.mk_slt(arg, bv.mk_numeral(0, arg_sz)));
|
||||
// arg < 0 ==> e = concat(arg, 1...1)
|
||||
// arg >= 0 ==> e = concat(arg, 0...0)
|
||||
add_clause(lt0, eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(rational::power_of_two(sz2) - 1, sz2))), nullptr);
|
||||
add_clause(~lt0, eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz2))), nullptr);
|
||||
}
|
||||
}
|
||||
|
||||
void solver::internalize_zero_extend(app* e) {
|
||||
expr* arg = e->get_arg(0);
|
||||
unsigned sz = bv.get_bv_size(e);
|
||||
unsigned arg_sz = bv.get_bv_size(arg);
|
||||
unsigned sz2 = sz - arg_sz;
|
||||
var2pdd(expr2enode(e)->get_th_var(get_id()));
|
||||
if (arg_sz == sz)
|
||||
add_clause(eq_internalize(e, arg), nullptr);
|
||||
else
|
||||
// e = concat(arg, 0...0)
|
||||
add_clause(eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz2))), nullptr);
|
||||
}
|
||||
|
||||
void solver::internalize_div_rem(app* e, bool is_div) {
|
||||
bv_rewriter_params p(s().params());
|
||||
if (p.hi_div0()) {
|
||||
if (is_div)
|
||||
internalize_udiv_i(e);
|
||||
else
|
||||
internalize_urem_i(e);
|
||||
return;
|
||||
}
|
||||
expr* arg1 = e->get_arg(0);
|
||||
expr* arg2 = e->get_arg(1);
|
||||
unsigned sz = bv.get_bv_size(e);
|
||||
expr_ref zero(bv.mk_numeral(0, sz), m);
|
||||
sat::literal eqZ = eq_internalize(arg2, zero);
|
||||
sat::literal eqU = eq_internalize(e, is_div ? bv.mk_bv_udiv0(arg1) : bv.mk_bv_urem0(arg1));
|
||||
sat::literal eqI = eq_internalize(e, is_div ? bv.mk_bv_udiv_i(arg1, arg2) : bv.mk_bv_urem_i(arg1, arg2));
|
||||
add_clause(~eqZ, eqU);
|
||||
add_clause(eqZ, eqI);
|
||||
ctx.add_aux(~eqZ, eqU);
|
||||
ctx.add_aux(eqZ, eqI);
|
||||
}
|
||||
|
||||
void solver::internalize_num(app* a) {
|
||||
rational val;
|
||||
unsigned sz = 0;
|
||||
VERIFY(bv.is_numeral(a, val, sz));
|
||||
auto p = m_core.value(val, sz);
|
||||
internalize_set(a, p);
|
||||
}
|
||||
|
||||
// TODO - test that internalize works with recursive call on bit2bool
|
||||
void solver::internalize_mkbv(app* a) {
|
||||
unsigned i = 0;
|
||||
for (expr* arg : *a) {
|
||||
expr_ref b2b(m);
|
||||
b2b = bv.mk_bit2bool(a, i);
|
||||
sat::literal bit_i = ctx.internalize(b2b, false, false);
|
||||
sat::literal lit = expr2literal(arg);
|
||||
add_equiv(lit, bit_i);
|
||||
#if 0
|
||||
ctx.add_aux_equiv(lit, bit_i);
|
||||
#endif
|
||||
++i;
|
||||
}
|
||||
}
|
||||
|
||||
void solver::internalize_extract(app* e) {
|
||||
var2pdd(expr2enode(e)->get_th_var(get_id()));
|
||||
}
|
||||
|
||||
void solver::internalize_concat(app* e) {
|
||||
SASSERT(bv.is_concat(e));
|
||||
var2pdd(expr2enode(e)->get_th_var(get_id()));
|
||||
}
|
||||
|
||||
void solver::internalize_par_unary(app* e, std::function<pdd(pdd,unsigned)> const& fn) {
|
||||
pdd const p = expr2pdd(e->get_arg(0));
|
||||
unsigned const par = e->get_parameter(0).get_int();
|
||||
internalize_set(e, fn(p, par));
|
||||
}
|
||||
|
||||
void solver::internalize_binary(app* e, std::function<pdd(pdd, pdd)> const& fn) {
|
||||
SASSERT(e->get_num_args() >= 1);
|
||||
auto p = expr2pdd(e->get_arg(0));
|
||||
for (unsigned i = 1; i < e->get_num_args(); ++i)
|
||||
p = fn(p, expr2pdd(e->get_arg(i)));
|
||||
internalize_set(e, p);
|
||||
}
|
||||
|
||||
void solver::internalize_binary(app* e, std::function<expr* (expr*, expr*)> const& fn) {
|
||||
SASSERT(e->get_num_args() >= 1);
|
||||
expr* r = e->get_arg(0);
|
||||
for (unsigned i = 1; i < e->get_num_args(); ++i)
|
||||
r = fn(r, e->get_arg(i));
|
||||
ctx.internalize(r);
|
||||
internalize_set(e, var2pdd(expr2enode(r)->get_th_var(get_id())));
|
||||
}
|
||||
|
||||
void solver::internalize_unary(app* e, std::function<pdd(pdd)> const& fn) {
|
||||
SASSERT(e->get_num_args() == 1);
|
||||
auto p = expr2pdd(e->get_arg(0));
|
||||
internalize_set(e, fn(p));
|
||||
}
|
||||
|
||||
template<bool Signed, bool Rev, bool Negated>
|
||||
void solver::internalize_le(app* e) {
|
||||
SASSERT(e->get_num_args() == 2);
|
||||
auto p = expr2pdd(e->get_arg(0));
|
||||
auto q = expr2pdd(e->get_arg(1));
|
||||
if (Rev)
|
||||
std::swap(p, q);
|
||||
auto sc = Signed ? m_core.sle(p, q) : m_core.ule(p, q);
|
||||
if (Negated)
|
||||
sc = ~sc;
|
||||
|
||||
sat::literal lit = expr2literal(e);
|
||||
if (lit.sign())
|
||||
sc = ~sc;
|
||||
mk_atom(lit.var(), sc);
|
||||
}
|
||||
|
||||
dd::pdd solver::expr2pdd(expr* e) {
|
||||
return var2pdd(get_th_var(e));
|
||||
}
|
||||
|
||||
dd::pdd solver::var2pdd(euf::theory_var v) {
|
||||
if (!m_var2pdd_valid.get(v, false)) {
|
||||
unsigned bv_size = get_bv_size(v);
|
||||
pvar pv = m_core.add_var(bv_size);
|
||||
m_pddvar2var.setx(pv, v, UINT_MAX);
|
||||
pdd p = m_core.var(pv);
|
||||
internalize_set(v, p);
|
||||
return p;
|
||||
}
|
||||
return m_var2pdd[v];
|
||||
}
|
||||
|
||||
void solver::apply_sort_cnstr(euf::enode* n, sort* s) {
|
||||
if (!bv.is_bv(n->get_expr()))
|
||||
return;
|
||||
theory_var v = n->get_th_var(get_id());
|
||||
if (v == euf::null_theory_var)
|
||||
v = mk_var(n);
|
||||
var2pdd(v);
|
||||
}
|
||||
|
||||
void solver::internalize_set(expr* e, pdd const& p) {
|
||||
internalize_set(get_th_var(e), p);
|
||||
}
|
||||
|
||||
void solver::internalize_set(euf::theory_var v, pdd const& p) {
|
||||
SASSERT_EQ(get_bv_size(v), p.power_of_2());
|
||||
m_var2pdd.reserve(get_num_vars(), p);
|
||||
m_var2pdd_valid.reserve(get_num_vars(), false);
|
||||
ctx.push(set_bitvector_trail(m_var2pdd_valid, v));
|
||||
#if 0
|
||||
m_var2pdd[v].reset(p.manager());
|
||||
#endif
|
||||
m_var2pdd[v] = p;
|
||||
}
|
||||
|
||||
void solver::eq_internalized(euf::enode* n) {
|
||||
SASSERT(m.is_eq(n->get_expr()));
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
212
src/sat/smt/polysat_substitution.h
Normal file
212
src/sat/smt/polysat_substitution.h
Normal file
|
|
@ -0,0 +1,212 @@
|
|||
/*++
|
||||
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); }
|
||||
|
||||
}
|
||||
45
src/sat/smt/polysat_types.h
Normal file
45
src/sat/smt/polysat_types.h
Normal file
|
|
@ -0,0 +1,45 @@
|
|||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-06
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
|
||||
#include "math/dd/dd_pdd.h"
|
||||
#include "util/sat_literal.h"
|
||||
#include "util/dependency.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
using pdd = dd::pdd;
|
||||
using pvar = unsigned;
|
||||
|
||||
|
||||
class dependency {
|
||||
unsigned m_index;
|
||||
unsigned m_level;
|
||||
public:
|
||||
dependency(sat::literal lit, unsigned level) : m_index(2 * lit.index()), m_level(level) {}
|
||||
dependency(unsigned var_idx, unsigned level) : m_index(1 + 2 * var_idx), m_level(level) {}
|
||||
bool is_literal() const { return m_index % 2 == 0; }
|
||||
sat::literal literal() const { SASSERT(is_literal()); return sat::to_literal(m_index / 2); }
|
||||
unsigned index() const { SASSERT(!is_literal()); return (m_index - 1) / 2; }
|
||||
unsigned level() const { return m_level; }
|
||||
};
|
||||
|
||||
using stacked_dependency = stacked_dependency_manager<dependency>::dependency;
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, dependency d) {
|
||||
if (d.is_literal())
|
||||
return out << d.literal() << "@" << d.level();
|
||||
else
|
||||
return out << "v" << d.index() << "@" << d.level();
|
||||
}
|
||||
|
||||
using dependency_vector = vector<dependency>;
|
||||
|
||||
}
|
||||
55
src/sat/smt/polysat_viable.h
Normal file
55
src/sat/smt/polysat_viable.h
Normal file
|
|
@ -0,0 +1,55 @@
|
|||
/*++
|
||||
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 "sat/smt/polysat_types.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
enum class find_t {
|
||||
empty,
|
||||
singleton,
|
||||
multiple,
|
||||
resource_out,
|
||||
};
|
||||
|
||||
class core;
|
||||
|
||||
class viable {
|
||||
core& c;
|
||||
public:
|
||||
viable(core& c) : c(c) {}
|
||||
|
||||
/**
|
||||
* Find a next viable value for variable.
|
||||
*/
|
||||
find_t find_viable(pvar v, rational& out_val) { throw default_exception("nyi"); }
|
||||
|
||||
/*
|
||||
* Explain why the current variable is not viable or signleton.
|
||||
*/
|
||||
dependency_vector explain() { throw default_exception("nyi"); }
|
||||
|
||||
/*
|
||||
* Register constraint at index 'idx' as unitary in v.
|
||||
*/
|
||||
void add_unitary(pvar v, unsigned idx) { throw default_exception("nyi"); }
|
||||
|
||||
};
|
||||
|
||||
}
|
||||
Loading…
Add table
Add a link
Reference in a new issue