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

prepare for new viable

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-11-21 06:18:35 +01:00
parent b0bf03457c
commit d86570ce75
8 changed files with 99 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -81,7 +81,7 @@ namespace polysat {
}
else {
SASSERT(c.is_currently_false(s));
// TBD: fails with test_subst SASSERT(c.bvalue(s) == l_true);
// TBD: fails with test_subst SASSERT(c.bvalue(s) == l_true);
c->set_var_dependent();
insert(c);
}
@ -100,10 +100,12 @@ namespace polysat {
LOG("Conflict: v" << v);
SASSERT(empty());
m_conflict_var = v;
#if !NEW_VIABLE
for (auto c : s.m_cjust[v]) {
c->set_var_dependent(); // ??
insert(c);
}
#endif
SASSERT(!empty());
}
@ -286,7 +288,7 @@ namespace polysat {
}
bool conflict::resolve_value(pvar v, vector<signed_constraint> const& cjust_v) {
bool conflict::resolve_value(pvar v) {
// NOTE:
// In the "standard" case where "v = val" is on the stack:
// - cjust_v contains true constraints
@ -298,13 +300,23 @@ namespace polysat {
return false;
}
#if NEW_VIABLE
if (conflict_var() == v && s.m_viable.resolve(v, *this))
return true;
#else
if (conflict_var() == v && s.m_forbidden_intervals.perform(v, cjust_v, *this))
return true;
#endif
m_vars.remove(v);
#if NEW_VIABLE
for (auto const& c : s.m_viable.get_constraints(v))
insert(c);
#else
for (auto c : cjust_v)
insert(c);
#endif
for (auto* engine : ex_engines)
if (engine->try_explain(v, *this))

2
src/math/polysat/conflict.h
View file

@ -103,7 +103,7 @@ namespace polysat {
/** Perform value resolution by applying various inference rules.
* Returns true if it was possible to eliminate the variable 'v'.
*/
bool resolve_value(pvar v, vector<signed_constraint> const& cjust_v);
bool resolve_value(pvar v);
/** Convert the core into a lemma to be learned. */
clause_builder build_lemma();

7
src/math/polysat/saturation.cpp
View file

@ -180,10 +180,17 @@ namespace polysat {
if (x_max * y_max > pddm.max_value())
push_omega_bisect(x, x_max, y, y_max);
else {
#if NEW_VIABLE
for (auto const& c : s.m_viable.get_constraints(y.var()))
m_new_constraints.insert(c);
for (auto const& c : s.m_viable.get_constraints(x.var()))
m_new_constraints.insert(c);
#else
for (auto c : s.m_cjust[y.var()])
m_new_constraints.insert(c);
for (auto c : s.m_cjust[x.var()])
m_new_constraints.insert(c);
#endif
}
}

19
src/math/polysat/solver.cpp
View file

@ -98,7 +98,9 @@ namespace polysat {
m_value.push_back(rational::zero());
m_justification.push_back(justification::unassigned());
m_viable.push(sz);
#if !NEW_VIABLE
m_cjust.push_back({});
#endif
m_pwatch.push_back({});
m_activity.push_back(0);
m_vars.push_back(sz2pdd(sz).mk_var(v));
@ -116,7 +118,9 @@ namespace polysat {
// TODO also remove v from all learned constraints.
pvar v = m_value.size() - 1;
m_viable.pop();
#if !NEW_VIABLE
m_cjust.pop_back();
#endif
m_value.pop_back();
m_justification.pop_back();
m_pwatch.pop_back();
@ -342,10 +346,12 @@ namespace polysat {
break;
}
case trail_instr_t::just_i: {
#if !NEW_VIABLE
auto v = m_cjust_trail.back();
LOG_V("Undo just_i");
m_cjust[v].pop_back();
m_cjust_trail.pop_back();
#endif
break;
}
default:
@ -474,8 +480,12 @@ namespace polysat {
LOG_H2("Resolve conflict");
LOG("\n" << *this);
LOG("search state: " << m_search);
#if NEW_VIABLE
m_viable.log();
#else
for (pvar v = 0; v < m_cjust.size(); ++v)
LOG("cjust[v" << v << "]: " << m_cjust[v]);
#endif
++m_stats.m_num_conflicts;
SASSERT(is_conflict());
@ -527,7 +537,7 @@ namespace polysat {
/** Conflict resolution case where propagation 'v := ...' is on top of the stack */
bool solver::resolve_value(pvar v) {
return m_conflict.resolve_value(v, m_cjust[v]);
return m_conflict.resolve_value(v);
}
/** Conflict resolution case where boolean literal 'lit' is on top of the stack
@ -762,6 +772,7 @@ namespace polysat {
void solver::narrow(pvar v) {
if (is_conflict())
return;
// TODO
}
// Add lemma to storage
@ -793,7 +804,7 @@ namespace polysat {
unsigned base_level = m_base_levels[m_base_levels.size() - num_scopes];
LOG("Pop " << num_scopes << " user scopes; lowest popped level = " << base_level << "; current level = " << m_level);
pop_levels(m_level - base_level + 1);
m_conflict.reset(); // TODO: maybe keep conflict if level of all constraints is lower than base_level?
m_conflict.reset();
}
bool solver::at_base_level() const {
@ -817,9 +828,11 @@ namespace polysat {
if (item.is_assignment()) {
pvar v = item.var();
auto const& j = m_justification[v];
out << "\t" << assignment_pp(*this, v, get_value(v)) << " @" << j.level();
out << "\t" << assignment_pp(*this, v, get_value(v)) << " @" << j.level();
#if !NEW_VIABLE
if (j.is_propagation())
out << " " << m_cjust[v];
#endif
out << "\n";
}
else {

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

@ -32,8 +32,12 @@ Author:
#include "math/polysat/forbidden_intervals.h"
#include "math/polysat/trail.h"
#include "math/polysat/viable.h"
#include "math/polysat/viable2.h"
#include "math/polysat/log.h"
#define NEW_VIABLE 0
namespace polysat {
class solver {
@ -71,7 +75,11 @@ namespace polysat {
reslimit& m_lim;
params_ref m_params;
#if NEW_VIABLE
viable2 m_viable;
#else
viable m_viable; // viable sets per variable
#endif
scoped_ptr_vector<dd::pdd_manager> m_pdd;
linear_solver m_linear_solver;
conflict m_conflict;
@ -92,7 +100,9 @@ namespace polysat {
// Per variable information
vector<rational> m_value; // assigned value
vector<justification> m_justification; // justification for variable assignment
#if !NEW_VIABLE
vector<signed_constraints> m_cjust; // constraints justifying variable range.
#endif
vector<signed_constraints> m_pwatch; // watch list datastructure into constraints.
unsigned_vector m_activity;
@ -121,6 +131,7 @@ namespace polysat {
m_qhead_trail.pop_back();
}
#if !NEW_VIABLE
void push_cjust(pvar v, signed_constraint c) {
if (m_cjust[v].contains(c)) // TODO: better check (flag on constraint?)
return;
@ -130,6 +141,7 @@ namespace polysat {
m_trail.push_back(trail_instr_t::just_i);
m_cjust_trail.push_back(v);
}
#endif
unsigned size(pvar v) const { return m_size[v]; }

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

@ -129,7 +129,7 @@ namespace polysat {
return;
}
#if 0
#if NEW_VIABLE
// setup with viable2:
// we no longer need cjust
pvar v = null_var;
@ -139,9 +139,9 @@ namespace polysat {
v = q.var();
if (v != null_var) {
signed_constraint sc(this, is_positive);
s.m_viable2.intersect(v, sc);
s.m_viable.intersect(v, sc);
rational val;
switch (s.m_viable2.find_viable(v, val)) {
switch (s.m_viable.find_viable(v, val)) {
case dd::find_t::singleton:
s.propagate(v, val, sc);
break;

8
src/math/polysat/viable2.cpp
View file

@ -246,12 +246,13 @@ namespace polysat {
return dd::find_t::multiple;
}
void viable2::get_core(pvar v, conflict& core) {
core.reset();
bool viable2::resolve(pvar v, conflict& core) {
if (has_viable(v))
return false;
auto* e = m_viable[v];
entry* first = e;
SASSERT(e);
SASSERT(!has_viable(v));
core.reset();
do {
// 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
@ -280,6 +281,7 @@ namespace polysat {
break;
}
}
return true;
}
void viable2::log(pvar v) {

42
src/math/polysat/viable2.h
View file

@ -97,7 +97,7 @@ namespace polysat {
* Retrieve the unsat core for v.
* \pre there are no viable values for v
*/
void get_core(pvar v, conflict& core);
bool resolve(pvar v, conflict& core);
/** Log all viable values for the given variable.
* (Inefficient, but useful for debugging small instances.)
@ -108,6 +108,46 @@ namespace polysat {
void log();
std::ostream& display(std::ostream& out) const;
class iterator {
entry* curr = nullptr;
bool visited = false;
public:
iterator(entry* curr, bool visited) :
curr(curr), visited(visited || !curr) {}
iterator& operator++() {
visited = true;
curr = curr->next();
return *this;
}
signed_constraint& operator*() {
return curr->src;
}
bool operator==(iterator const& other) const {
return visited == other.visited && curr == other.curr;
}
bool operator!=(iterator const& other) const {
return !(*this == other);
}
};
class constraints {
viable2& viable;
pvar var;
public:
constraints(viable2& viable, pvar var) : viable(viable), var(var) {}
iterator begin() const { return iterator(viable.m_viable[var], false); }
iterator end() const { return iterator(viable.m_viable[var], true); }
};
constraints get_constraints(pvar v) {
return constraints(*this, v);
}
};
inline std::ostream& operator<<(std::ostream& out, viable2 const& v) {