mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity

adding new viable using forbidden intervals

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-11-10 08:23:45 -08:00
parent 733f44d141
commit 0bec8520e1
9 changed files with 201 additions and 254 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/CMakeLists.txt
View file

@ -15,6 +15,7 @@ z3_add_component(polysat
solver.cpp
ule_constraint.cpp
viable.cpp
viable2.cpp
variable_elimination.cpp
COMPONENT_DEPENDENCIES
util

6
src/math/polysat/conflict.cpp
View file

@ -264,8 +264,8 @@ namespace polysat {
for (auto v : m_vars)
a.push_back(std::make_pair(v, s.get_value(v)));
for (unsigned i = 0; i < a.size(); ++i) {
auto save = a[i];
auto last = a.back();
std::pair<pvar, rational> save = a[i];
std::pair<pvar, rational> last = a.back();
a[i] = last;
a.pop_back();
if (c.is_currently_false(a))
@ -278,7 +278,7 @@ namespace polysat {
if (a.size() == m_vars.num_elems())
return;
m_vars.reset();
for (auto [v, val] : a)
for (auto const& [v, val] : a)
m_vars.insert(v);
LOG("reduced " << m_vars);
}

30
src/math/polysat/forbidden_intervals.cpp
View file

@ -147,9 +147,9 @@ namespace polysat {
unsigned const next_i = seq[(seq_i + 1) % seq.size()];
// Build constraint: upper bound of each interval is not contained in the next interval,
// using the equivalence: t \in [l;h[ <=> t-l < h-l
auto hi = records[i].interval.hi();
auto next_lo = records[next_i].interval.lo();
auto next_hi = records[next_i].interval.hi();
auto const& hi = records[i].interval.hi();
auto const& next_lo = records[next_i].interval.lo();
auto const& next_hi = records[next_i].interval.hi();
auto lhs = hi - next_lo;
auto rhs = next_hi - next_lo;
signed_constraint c = s.m_constraints.ult(lhs, rhs);
@ -315,9 +315,9 @@ namespace polysat {
bool is_trivial = (b2 + 1).is_zero();
push_eq(is_trivial, e2 + 1, side_cond);
auto lo = e2 - e1 + 1;
auto lo_val = (b2 - b1 + 1).val();
rational lo_val = (b2 - b1 + 1).val();
auto hi = -e1;
auto hi_val = (-b1).val();
rational hi_val = (-b1).val();
interval = to_interval(c, is_trivial, a1, lo_val, lo, hi_val, hi);
return true;
}
@ -337,9 +337,9 @@ namespace polysat {
bool is_trivial = b1.is_zero();
push_eq(is_trivial, e1, side_cond);
auto lo = -e2;
auto lo_val = (-b2).val();
rational lo_val = (-b2).val();
auto hi = e1 - e2;
auto hi_val = (b1 - b2).val();
rational hi_val = (b1 - b2).val();
interval = to_interval(c, is_trivial, a2, lo_val, lo, hi_val, hi);
return true;
}
@ -358,9 +358,9 @@ namespace polysat {
bool is_trivial = b1.val() == b2.val();
push_eq(is_trivial, e1 - e2, side_cond);
auto lo = -e2;
auto lo_val = (-b2).val();
rational lo_val = (-b2).val();
auto hi = -e1;
auto hi_val = (-b1).val();
rational hi_val = (-b1).val();
interval = to_interval(c, is_trivial, a1, lo_val, lo, hi_val, hi);
return true;
}
@ -432,8 +432,8 @@ namespace polysat {
a2 < b1.val() && e1.is_val()) {
if (!e2.is_val())
side_cond.push_back(s.eq(e2));
auto lo_val = rational::zero();
auto hi_val = floor((b1.val() - 1) / a2) + 1;
rational lo_val = rational::zero();
rational hi_val = floor((b1.val() - 1) / a2) + 1;
SASSERT(lo_val < hi_val);
auto lo = m.mk_val(lo_val);
auto hi = m.mk_val(hi_val);
@ -447,8 +447,8 @@ namespace polysat {
a1.is_zero() && e1.is_val() && a2 < b1.val()) {
if (!e2.is_val())
side_cond.push_back(s.eq(e2));
auto lo_val = ceil(b1.val() / a2);
auto hi_val = floor(m.max_value() / a2) + 1;
rational lo_val = ceil(b1.val() / a2);
rational hi_val = floor(m.max_value() / a2) + 1;
auto lo = m.mk_val(lo_val);
auto hi = m.mk_val(hi_val);
interval = eval_interval::proper(lo, lo_val, hi, hi_val);
@ -461,8 +461,8 @@ namespace polysat {
a2.is_zero() && e2.is_val() && a1 <= b2.val()) {
if (!e1.is_val())
side_cond.push_back(s.eq(e2));
auto lo_val = rational::zero();
auto hi_val = floor(b2.val() / a1) + 1;
rational lo_val = rational::zero();
rational hi_val = floor(b2.val() / a1) + 1;
auto lo = m.mk_val(lo_val);
auto hi = m.mk_val(hi_val);
interval = eval_interval::proper(lo, lo_val, hi, hi_val);

3
src/math/polysat/forbidden_intervals.h
View file

@ -24,7 +24,7 @@ namespace polysat {
solver& s;
void revert_core(conflict& core);
void full_interval_conflict(signed_constraint c, vector<signed_constraint> const & side_cond, conflict& core);
bool get_interval(signed_constraint const& c, pvar v, eval_interval& out_interval, vector<signed_constraint>& side_cond);
void push_eq(bool is_trivial, pdd const& p, vector<signed_constraint>& side_cond);
eval_interval to_interval(signed_constraint const& c, bool is_trivial, rational const& coeff,
rational & lo_val, pdd & lo, rational & hi_val, pdd & hi);
@ -61,5 +61,6 @@ namespace polysat {
public:
forbidden_intervals(solver& s) :s(s) {}
bool perform(pvar v, vector<signed_constraint> const& just, conflict& core);
bool get_interval(signed_constraint const& c, pvar v, eval_interval& out_interval, vector<signed_constraint>& side_cond);
};
}

1
src/math/polysat/solver.h
View file

@ -60,6 +60,7 @@ namespace polysat {
friend class forbidden_intervals;
friend class linear_solver;
friend class viable;
friend class viable2;
friend class assignment_pp;
friend class assignments_pp;
friend class ex_polynomial_superposition;

143
src/math/polysat/viable.cpp
View file

@ -12,47 +12,25 @@ Author:
Notes:
Use cheap heuristics to narrow viable sets whenever possible.
If the cheap heuristics fail, compute a BDD representing the viable sets
and narrow the range using the BDDs that are cached.
--*/
#include "math/polysat/viable.h"
#include "math/polysat/solver.h"
#if NEW_VIABLE
#include "math/polysat/viable_set_def.h"
#endif
namespace polysat {
viable::viable(solver& s):
s(s),
m_bdd(1000)
{}
viable::~viable() {
#if NEW_VIABLE
ptr_vector<cached_constraint> entries;
for (auto* e : m_constraint_cache)
entries.push_back(e);
m_constraint_cache.reset();
for (auto* e : entries)
dealloc(e);
#endif
}
void viable::push_viable(pvar v) {
s.m_trail.push_back(trail_instr_t::viable_i);
#if NEW_VIALBLE
m_viable_trail.push_back(std::make_pair(v, alloc(viable_set, *m_viable[v])));
#else
m_viable_trail.push_back(std::make_pair(v, m_viable[v]));
#endif
}
@ -65,13 +43,6 @@ namespace polysat {
// a*v + b == 0 or a*v + b != 0
void viable::intersect_eq(rational const& a, pvar v, rational const& b, bool is_positive) {
#if NEW_VIABLE
push_viable(v);
if (!m_viable[v]->intersect_eq(a, b, is_positive))
intersect_eq_bdd(v, a, b, is_positive);
if (m_viable[v]->is_empty())
s.set_conflict(v);
#else
bddv const& x = var2bits(v).var();
if (b == 0 && a.is_odd()) {
@ -94,17 +65,9 @@ namespace polysat {
bdd xs = is_positive ? lhs.all0() : !lhs.all0();
intersect_viable(v, xs);
}
#endif
}
void viable::intersect_ule(pvar v, rational const& a, rational const& b, rational const& c, rational const& d, bool is_positive) {
#if NEW_VIABLE
push_viable(v);
if (!m_viable[v]->intersect_le(a, b, c, d, is_positive))
intersect_ule_bdd(v, a, b, c, d, is_positive);
if (m_viable[v]->is_empty())
s.set_conflict(v);
#else
bddv const& x = var2bits(v).var();
// hacky special case
if (a == 1 && b == 0 && c == 0 && d == 0)
@ -117,144 +80,40 @@ namespace polysat {
bdd xs = is_positive ? (l <= r) : (l > r);
intersect_viable(v, xs);
}
#endif
}
#if NEW_VIABLE
viable::cached_constraint& viable::cache_constraint(pvar v, cached_constraint& entry0, std::function<bdd(void)>& mk_constraint) {
cached_constraint* other = nullptr;
if (!m_constraint_cache.find(&entry0, other)) {
gc_cached_constraints();
other = alloc(cached_constraint, entry0);
other->repr = mk_constraint();
m_constraint_cache.insert(other);
}
other->m_activity++;
return *other;
}
void viable::gc_cached_constraints() {
//
// TODO: instead of using activity for GC, use the Move-To-Front approach
// see sat/smt/bv_ackerman.h or sat/smt/euf_ackerman.h
// where hash table entries use a dll_base.
//
unsigned max_entries = 10000;
if (m_constraint_cache.size() > max_entries) {
ptr_vector<cached_constraint> entries;
for (auto* e : m_constraint_cache)
entries.push_back(e);
std::stable_sort(entries.begin(), entries.end(), [&](cached_constraint* a, cached_constraint* b) { return a->m_activity < b->m_activity; });
for (auto* e : entries)
e->m_activity /= 2;
for (unsigned i = 0; i < max_entries/2; ++i) {
m_constraint_cache.remove(entries[i]);
dealloc(entries[i]);
}
}
}
void viable::narrow(pvar v, bdd const& is_false) {
rational bound = m_viable[v]->lo;
if (var2bits(v).sup(is_false, bound))
m_viable[v]->update_lo(m_viable[v]->next(bound));
bound = m_viable[v]->prev(m_viable[v]->hi);
if (var2bits(v).inf(is_false, bound))
m_viable[v]->update_hi(m_viable[v]->prev(bound));
}
void viable::intersect_ule_bdd(pvar v, rational const& a, rational const& b, rational const& c, rational const& d, bool is_positive) {
unsigned sz = var2bits(v).num_bits();
std::function<bdd(void)> le = [&]() {
bddv const& x = var2bits(v).var();
return ((a * x) + b) <= ((c * x) + d);
};
cached_constraint entry0(sz, a, b, c, d, m_bdd.mk_true());
cached_constraint& entry = cache_constraint(v, entry0, le);
// le(lo) is false: find min x >= lo, such that le(x) is false, le(x+1) is true
// le(hi) is false: find max x =< hi, such that le(x) is false, le(x-1) is true
bdd gt = is_positive ? !entry.repr : entry.repr;
narrow(v, gt);
}
void viable::intersect_eq_bdd(pvar v, rational const& a, rational const& b, bool is_positive) {
unsigned sz = var2bits(v).num_bits();
std::function<bdd(void)> eq = [&]() {
bddv const& x = var2bits(v).var();
return ((a * x) + b) == rational(0);
};
cached_constraint entry0(sz, a, b, m_bdd.mk_true());
cached_constraint& entry = cache_constraint(v, entry0, eq);
bdd ne = is_positive ? !entry.repr : entry.repr;
narrow(v, ne);
}
#endif
bool viable::has_viable(pvar v) {
#if NEW_VIABLE
return !m_viable[v]->is_empty();
#else
return !m_viable[v].is_false();
#endif
}
bool viable::is_viable(pvar v, rational const& val) {
#if NEW_VIABLE
return m_viable[v]->contains(val);
#else
return var2bits(v).contains(m_viable[v], val);
#endif
}
void viable::add_non_viable(pvar v, rational const& val) {
#if NEW_VIABLE
push_viable(v);
IF_VERBOSE(10, verbose_stream() << " v" << v << " != " << val << "\n");
m_viable[v]->intersect_diff(val);
if (m_viable[v]->is_empty())
s.set_conflict(v);
#else
LOG("pvar " << v << " /= " << val);
SASSERT(is_viable(v, val));
auto const& bits = var2bits(v);
intersect_viable(v, bits.var() != val);
#endif
}
#if !NEW_VIABLE
void viable::intersect_viable(pvar v, bdd vals) {
push_viable(v);
m_viable[v] &= vals;
if (m_viable[v].is_false())
s.set_conflict(v);
}
#endif
dd::find_t viable::find_viable(pvar v, rational & val) {
#if NEW_VIABLE
return m_viable[v]->find_hint(s.m_value[v], val);
#else
return var2bits(v).find_hint(m_viable[v], s.m_value[v], val);
#endif
}
rational viable::min_viable(pvar v) {
#if !NEW_VIABLE
return var2bits(v).min(m_viable[v]);
#else
return rational(0);
#endif
}
rational viable::max_viable(pvar v) {
#if NEW_VIABLE
return m_viable[v]->max();
#else
return var2bits(v).max(m_viable[v]);
#endif
}
dd::fdd const& viable::sz2bits(unsigned sz) {
@ -267,7 +126,6 @@ namespace polysat {
return *bits;
}
#if POLYSAT_LOGGING_ENABLED
void viable::log() {
// only for small problems
for (pvar v = 0; v < std::min(10u, m_viable.size()); ++v)
@ -284,7 +142,6 @@ namespace polysat {
LOG("Viable for v" << v << ": " << xs);
}
}
#endif
dd::fdd const& viable::var2bits(pvar v) { return sz2bits(s.size(v)); }

96
src/math/polysat/viable.h
View file

@ -14,63 +14,15 @@ Author:
Notes:
NEW_VIABLE uses cheaper book-keeping, but is partial.
Alternative to using rational, instead use fixed-width numerals.
map from num_bits to template set
class viable_trail_base {
public:
virtual pop(pvar v) = 0;
virtual push(pvar v) = 0;
static viable_trail_base* mk_trail(unsigned num_bits);
};
class viable_trail<Numeral> : public viable_trail_base {
vector<viable_set<Numeral>> m_viable;
vector<viable_set<Numeral>> m_trail;
public:
void pop(pvar v) override {
m_viable[v] = m_trail.back();
m_trail.pop_back();
}
void push(pvar v) override {
m_trail.push_back(m_viable[v]);
}
};
// from num-bits to viable_trail_base*
scoped_ptr_vector<viable_trail_base> m_viable_trails;
viable_set_base& to_viable(pvar v) {
return (*m_viable_trails[num_bits(v)])[v];
}
viable_set_base is required to expose functions:
lo, hi,
prev, next alternative as bit-vectors
update_lo (a)
update_hi (a)
intersect_le (a, b, c, d)
intersect_diff (a, b)
intersect_eq (a, b)
is_empty
contains
--*/
#pragma once
#define NEW_VIABLE 0
#include <limits>
#include "math/dd/dd_bdd.h"
#include "math/polysat/types.h"
#if NEW_VIABLE
#include "math/polysat/viable_set.h"
#endif
namespace polysat {
@ -82,43 +34,7 @@ namespace polysat {
typedef dd::fdd fdd;
solver& s;
dd::bdd_manager m_bdd;
scoped_ptr_vector<dd::fdd> m_bits;
#if NEW_VIABLE
struct cached_constraint {
enum op_code { is_ule, is_eq };
op_code m_op;
unsigned m_num_bits;
rational a, b, c, d;
bdd repr;
unsigned m_activity = 0;
cached_constraint(unsigned n, rational const& a, rational const& b, rational const& c, rational const& d, bdd& f) :
m_op(op_code::is_ule), m_num_bits(n), a(a), b(b), c(c), d(d), repr(f) {}
cached_constraint(unsigned n, rational const& a, rational const& b, bdd& f) :
m_op(op_code::is_eq), m_num_bits(n), a(a), b(b), repr(f) {}
struct hash {
unsigned operator()(cached_constraint const* e) const {
return mk_mix(e->a.hash(), e->b.hash(), mk_mix(e->c.hash(), e->d.hash(), e->m_num_bits)) + e->m_op;
}
};
struct eq {
bool operator()(cached_constraint const* x, cached_constraint const* y) const {
return x->m_op == y->m_op && x->a == y->a && x->b == y->b && x->c == y->c && x->d == y->d && x->m_num_bits == y->m_num_bits;
}
};
};
scoped_ptr_vector<viable_set> m_viable;
vector<std::pair<pvar, viable_set*>> m_viable_trail;
hashtable<cached_constraint*, cached_constraint::hash, cached_constraint::eq> m_constraint_cache;
void intersect_ule_bdd(pvar v, rational const& a, rational const& b, rational const& c, rational const& d, bool is_positive);
void intersect_eq_bdd(pvar v, rational const& a, rational const& b, bool is_positive);
cached_constraint& cache_constraint(pvar v, cached_constraint& entry0, std::function<bdd(void)>& mk_constraint);
void gc_cached_constraints();
void narrow(pvar v, bdd const& is_false);
#else
scoped_ptr_vector<dd::fdd> m_bits;
vector<bdd> m_viable; // set of viable values.
vector<std::pair<pvar, bdd>> m_viable_trail;
@ -127,7 +43,7 @@ namespace polysat {
* Register all values that are not contained in vals as non-viable.
*/
void intersect_viable(pvar v, bdd vals);
#endif
dd::bdd_manager& get_bdd() { return m_bdd; }
dd::fdd const& sz2bits(unsigned sz);
dd::fdd const& var2bits(pvar v);
@ -139,11 +55,7 @@ namespace polysat {
~viable();
void push(unsigned num_bits) {
#if NEW_VIABLE
m_viable.push_back(alloc(viable_set, num_bits));
#else
m_viable.push_back(m_bdd.mk_true());
#endif
}
void pop() {

74
src/math/polysat/viable2.cpp Normal file
View file

@ -0,0 +1,74 @@
/*++
Copyright (c) 2021 Microsoft Corporation
Module Name:
maintain viable domains
Author:
Nikolaj Bjorner (nbjorner) 2021-03-19
Jakob Rath 2021-04-6
--*/
#include "math/polysat/viable2.h"
#include "math/polysat/solver.h"
namespace polysat {
viable2::viable2(solver& s) : s(s) {}
viable2::~viable2() {}
void viable2::push_viable(pvar v) {
m_trail.push_back(std::make_pair(v, m_viable[v]));
}
void viable2::pop_viable() {
auto const& [v, s] = m_trail.back();
m_viable[v] = s;
m_trail.pop_back();
}
void viable2::intersect(pvar v, signed_constraint const& c) {
auto& fi = s.m_forbidden_intervals;
vector<signed_constraint> side_cond;
eval_interval interval = eval_interval::full();
if (!fi.get_interval(c, v, interval, side_cond))
return;
auto& s = m_viable[v];
for (unsigned i = 0; i < s.size(); ++i) {
}
}
bool viable2::has_viable(pvar v) { return true; }
bool viable2::is_viable(pvar v, rational const& val) { return true; }
void viable2::add_non_viable(pvar v, rational const& val) { }
rational viable2::min_viable(pvar v) { return rational::zero(); }
rational viable2::max_viable(pvar v) { return rational::zero(); }
dd::find_t viable2::find_viable(pvar v, rational& val) { return dd::find_t::multiple; }
void viable2::log(pvar v) {
auto const& s = m_viable[v];
for (auto const& [i, c] : s)
LOG("v" << v << ": " << i);
}
void viable2::log() {
for (pvar v = 0; v < std::min(10u, m_viable.size()); ++v)
log(v);
}
}

101
src/math/polysat/viable2.h Normal file
View file

@ -0,0 +1,101 @@
/*++
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-6
--*/
#pragma once
#include <limits>
#include "math/polysat/types.h"
#include "math/polysat/constraint.h"
namespace polysat {
class solver;
class viable2 {
solver& s;
typedef std::tuple<eval_interval, vector<signed_constraint>> entry;
typedef vector<entry> state;
vector<state> m_viable; // set of viable values.
vector<std::pair<pvar, state>> m_trail;
public:
viable2(solver& s);
~viable2();
void push(unsigned) {
m_viable.push_back({});
}
void pop() {
m_viable.pop_back();
}
void push_viable(pvar v);
void pop_viable();
/**
* update state of viable for pvar v
* based on affine constraints
*/
void intersect(pvar v, signed_constraint const& c);
/**
* Check whether variable v has any viable values left according to m_viable.
*/
bool has_viable(pvar v);
/**
* check if value is viable according to m_viable.
*/
bool is_viable(pvar v, rational const& val);
/**
* register that val is non-viable for var.
*/
void add_non_viable(pvar v, rational const& val);
/*
* Extract min and max viable values for v
*/
rational min_viable(pvar v);
rational max_viable(pvar v);
/**
* Find a next viable value for variable.
*/
dd::find_t find_viable(pvar v, rational & val);
/** Log all viable values for the given variable.
* (Inefficient, but useful for debugging small instances.)
*/
void log(pvar v);
/** Like log(v) but for all variables */
void log();
};
}