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

moving out viable functionality

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-06-21 15:50:04 -07:00
parent 19099244c4
commit 6f93ed8dc2
9 changed files with 242 additions and 121 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/dd/dd_bdd.cpp
View file

@ -1181,14 +1181,14 @@ namespace dd {
bdd bddv::all0() const {
bdd r = m->mk_true();
for (unsigned i = size(); i-- > 0; )
for (unsigned i = 0; i < size() && !r.is_false(); ++i)
r &= !m_bits[i];
return r;
}
bdd bddv::all1() const {
bdd r = m->mk_true();
for (unsigned i = size(); i-- > 0; )
for (unsigned i = 0; i < size() && !r.is_false(); ++i)
r &= m_bits[i];
return r;
}

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

@ -12,6 +12,7 @@ z3_add_component(polysat
solver.cpp
ule_constraint.cpp
var_constraint.cpp
viable.cpp
COMPONENT_DEPENDENCIES
util
dd

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

@ -63,24 +63,11 @@ namespace polysat {
rational a = q.hi().val();
rational b = q.lo().val();
bddv const& x = s.var2bits(v).var();
if (b == 0 && a.is_odd()) {
// hacky test optimizing special case.
// general case is compute inverse(a)*-b for equality 2^k*a*x + b == 0
// then constrain x.
//
s.intersect_viable(v, is_positive() ? x.all0() : !x.all0());
}
else {
IF_VERBOSE(10, verbose_stream() << a << "*x + " << b << "\n");
bddv lhs = a * x + b;
bdd xs = is_positive() ? lhs.all0() : !lhs.all0();
s.intersect_viable(v, xs);
}
s.m_vble.intersect_eq(a, v, b, is_positive());
rational val;
if (s.find_viable(v, val) == dd::find_t::singleton)
if (s.m_vble.find_viable(v, val) == dd::find_t::singleton)
s.propagate(v, val, *this);
return;
}

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

@ -34,6 +34,7 @@ namespace polysat {
return *m_pdd[sz];
}
#if 0
dd::fdd const& solver::sz2bits(unsigned sz) {
m_bits.reserve(sz + 1);
auto* bits = m_bits[sz];
@ -70,11 +71,14 @@ namespace polysat {
return var2bits(v).find_hint(m_viable[v], m_value[v], val);
}
#endif
solver::solver(reslimit& lim):
m_lim(lim),
m_linear_solver(*this),
m_bdd(1000),
m_vble(*this),
// m_bdd(1000),
m_dm(m_value_manager, m_alloc),
m_linear_solver(*this),
m_free_vars(m_activity),
m_bvars(),
m_constraints(m_bvars) {
@ -85,31 +89,6 @@ namespace polysat {
m_conflict.reset();
}
#if POLYSAT_LOGGING_ENABLED
void solver::log_viable() {
// only for small problems
if (m_viable.size() < 10) {
for (pvar v = 0; v < m_viable.size(); ++v) {
log_viable(v);
}
}
}
void solver::log_viable(pvar v) {
if (size(v) <= 5) {
vector<rational> xs;
for (rational x = rational::zero(); x < rational::power_of_two(size(v)); x += 1) {
if (is_viable(v, x)) {
xs.push_back(x);
}
}
LOG("Viable for pvar " << v << ": " << xs);
} else {
LOG("Viable for pvar " << v << ": <range too big>");
}
}
#endif
bool solver::should_search() {
return
m_lim.inc() &&
@ -126,7 +105,7 @@ namespace polysat {
LOG("Free variables: " << m_free_vars);
LOG("Assignment: " << assignments_pp(*this));
if (!m_conflict.empty()) LOG("Conflict: " << m_conflict);
IF_LOGGING(log_viable());
IF_LOGGING(m_vble.log());
if (pending_disjunctive_lemma()) { LOG_H2("UNDEF (handle lemma externally)"); return l_undef; }
else if (is_conflict() && at_base_level()) { LOG_H2("UNSAT"); return l_false; }
@ -140,10 +119,10 @@ namespace polysat {
}
unsigned solver::add_var(unsigned sz) {
pvar v = m_viable.size();
pvar v = m_value.size();
m_value.push_back(rational::zero());
m_justification.push_back(justification::unassigned());
m_viable.push_back(m_bdd.mk_true());
m_vble.push();
m_cjust.push_back(constraints());
m_watch.push_back(ptr_vector<constraint>());
m_activity.push_back(0);
@ -161,8 +140,8 @@ namespace polysat {
void solver::del_var() {
// TODO also remove v from all learned constraints.
pvar v = m_viable.size() - 1;
m_viable.pop_back();
pvar v = m_value.size() - 1;
m_vble.pop();
m_cjust.pop_back();
m_value.pop_back();
m_justification.pop_back();
@ -189,7 +168,7 @@ namespace polysat {
auto slack = add_var(sz);
auto q = p + var(slack);
add_eq(q, dep); // TODO: 'dep' now refers to two constraints; this is not yet supported
auto non_zero = sz2bits(sz).non_zero();
auto non_zero = m_vble.sz2bits(sz).non_zero();
return m_constraints.viable(m_level, pos_t, slack, non_zero, mk_dep_ref(dep));
}
@ -287,7 +266,7 @@ namespace polysat {
void solver::propagate(pvar v, rational const& val, constraint& c) {
LOG("Propagation: " << assignment_pp(*this, v, val) << ", due to " << c);
if (is_viable(v, val)) {
if (m_vble.is_viable(v, val)) {
m_free_vars.del_var_eh(v);
assign_core(v, val, justification::propagation(m_level));
}
@ -326,10 +305,7 @@ namespace polysat {
break;
}
case trail_instr_t::viable_i: {
auto p = m_viable_trail.back();
LOG_V("Undo viable_i");
m_viable[p.first] = p.second;
m_viable_trail.pop_back();
m_vble.pop_viable();
break;
}
case trail_instr_t::assign_i: {
@ -418,9 +394,9 @@ namespace polysat {
void solver::decide(pvar v) {
LOG("Decide v" << v);
IF_LOGGING(log_viable(v));
IF_LOGGING(m_vble.log(v));
rational val;
switch (find_viable(v, val)) {
switch (m_vble.find_viable(v, val)) {
case dd::find_t::empty:
// NOTE: all such cases should be discovered elsewhere (e.g., during propagation/narrowing)
// (fail here in debug mode so we notice if we miss some)
@ -445,7 +421,7 @@ namespace polysat {
else
++m_stats.m_num_propagations;
LOG(assignment_pp(*this, v, val) << " by " << j);
SASSERT(is_viable(v, val));
SASSERT(m_vble.is_viable(v, val));
SASSERT(std::all_of(assignment().begin(), assignment().end(), [v](auto p) { return p.first != v; }));
m_value[v] = val;
m_search.push_assignment(v, val);
@ -531,7 +507,7 @@ namespace polysat {
pvar conflict_var = null_var;
clause_ref lemma;
for (auto v : m_conflict.vars(m_constraints))
if (!has_viable(v)) {
if (!m_vble.has_viable(v)) {
SASSERT(conflict_var == null_var || conflict_var == v); // at most one variable can be empty
conflict_var = v;
}
@ -799,7 +775,7 @@ namespace polysat {
// Guess a literal from the given clause; returns the guessed constraint
sat::literal solver::decide_bool(clause& lemma) {
LOG_H3("Guessing literal in lemma: " << lemma);
IF_LOGGING(log_viable());
IF_LOGGING(m_vble.log());
LOG("Boolean assignment: " << m_bvars);
// To make a guess, we need to find an unassigned literal that is not false in the current model.
@ -887,20 +863,14 @@ namespace polysat {
rational val = m_value[v];
LOG_H3("Reverting decision: pvar " << v << " := " << val);
SASSERT(m_justification[v].is_decision());
bdd viable = m_viable[v];
constraints just(m_cjust[v]);
backjump(m_justification[v].level()-1);
// Since decision "v -> val" caused a conflict, we may keep all
// viability restrictions on v and additionally exclude val.
// TODO: viability restrictions on 'v' must have happened before decision on 'v'. Do we really need to save/restore m_viable here?
SASSERT(m_viable[v] == viable); // check this with assertion
SASSERT(m_cjust[v] == just); // check this with assertion
// push_viable(v);
// m_viable[v] = viable;
// for (unsigned i = m_cjust[v].size(); i < just.size(); ++i)
// push_cjust(v, just[i]);
add_non_viable(v, val);
m_vble.add_non_viable(v, val);
auto confl = std::move(m_conflict);
m_conflict.reset();

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

@ -28,6 +28,7 @@ Author:
#include "math/polysat/linear_solver.h"
#include "math/polysat/search_state.h"
#include "math/polysat/trail.h"
#include "math/polysat/viable.h"
#include "math/polysat/log.h"
namespace polysat {
@ -52,15 +53,15 @@ namespace polysat {
friend class conflict_explainer;
friend class forbidden_intervals;
friend class linear_solver;
friend class viable;
friend class assignment_pp;
friend class assignments_pp;
typedef ptr_vector<constraint> constraints;
reslimit& m_lim;
dd::bdd_manager m_bdd;
viable m_vble; // viable sets per variable
scoped_ptr_vector<dd::pdd_manager> m_pdd;
scoped_ptr_vector<dd::fdd> m_bits;
dep_value_manager m_value_manager;
small_object_allocator m_alloc;
poly_dep_manager m_dm;
@ -85,7 +86,6 @@ namespace polysat {
svector<sat::bool_var> m_disjunctive_lemma;
// Per variable information
vector<bdd> m_viable; // set of viable values.
vector<rational> m_value; // assigned value
vector<justification> m_justification; // justification for variable assignment
vector<constraints> m_cjust; // constraints justifying variable range.
@ -110,7 +110,6 @@ namespace polysat {
svector<trail_instr_t> m_trail;
unsigned_vector m_qhead_trail;
vector<std::pair<pvar, bdd>> m_viable_trail;
unsigned_vector m_cjust_trail;
ptr_vector<constraint> m_activate_trail;
@ -119,8 +118,7 @@ namespace polysat {
void push_viable(pvar v) {
m_trail.push_back(trail_instr_t::viable_i);
m_viable_trail.push_back(std::make_pair(v, m_viable[v]));
m_vble.push_viable(v);
}
void push_qhead() {
@ -144,43 +142,6 @@ namespace polysat {
unsigned size(pvar v) const { return m_size[v]; }
/**
* 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);
/**
* Register all values that are not contained in vals as non-viable.
*/
void intersect_viable(pvar v, bdd vals);
/**
* Add dependency for variable viable range.
*/
void add_viable_dep(pvar v, p_dependency* dep);
/**
* 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_viable(pvar v);
/** Like log_viable but for all variables */
void log_viable();
/**
* undo trail operations for backtracking.
* Each struct is a subclass of trail and implements undo().
@ -188,10 +149,7 @@ namespace polysat {
void del_var();
dd::bdd_manager& get_bdd() { return m_bdd; }
dd::pdd_manager& sz2pdd(unsigned sz);
dd::fdd const& sz2bits(unsigned sz);
dd::fdd const& var2bits(pvar v) { return sz2bits(size(v)); }
void push_level();
void pop_levels(unsigned num_levels);

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

@ -74,22 +74,22 @@ namespace polysat {
d = q.lo().val();
}
if (v != null_var) {
bddv const& x = s.var2bits(v).var();
bddv const& x = s.m_vble.var2bits(v).var();
s.push_cjust(v, this);
// hacky special case
if (a == 1 && b == 0 && c == 0 && d == 0)
// x <= 0
s.intersect_viable(v, is_positive() ? x.all0() : !x.all0());
s.m_vble.intersect_viable(v, is_positive() ? x.all0() : !x.all0());
else {
IF_VERBOSE(10, verbose_stream() << a << "*x + " << b << (is_positive() ? " <= " : " > ") << c << "*x + " << d << "\n");
bddv l = a * x + b;
bddv r = c * x + d;
bdd xs = is_positive() ? (l <= r) : (l > r);
s.intersect_viable(v, xs);
s.m_vble.intersect_viable(v, xs);
}
rational val;
if (s.find_viable(v, val) == dd::find_t::singleton) {
if (s.m_vble.find_viable(v, val) == dd::find_t::singleton) {
s.propagate(v, val, *this);
}

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

@ -32,15 +32,15 @@ namespace polysat {
}
bool var_constraint::is_currently_false(solver& s) {
return s.m_viable[m_var].is_false();
return s.m_vble.is_false(m_var);
}
bool var_constraint::is_currently_true(solver& s) {
return !s.m_viable[m_var].is_false();
return !is_currently_false(s);
}
void var_constraint::narrow(solver& s) {
s.intersect_viable(m_var, m_viable);
s.m_vble.intersect_viable(m_var, m_viable);
}
}

114
src/math/polysat/viable.cpp Normal file
View file

@ -0,0 +1,114 @@
#include "math/polysat/viable.h"
#include "math/polysat/solver.h"
namespace polysat {
viable::viable(solver& s):
s(s),
m_bdd(1000)
{}
void viable::push_viable(pvar v) {
s.m_trail.push_back(trail_instr_t::viable_i);
m_viable_trail.push_back(std::make_pair(v, m_viable[v]));
}
void viable::pop_viable() {
auto p = m_viable_trail.back();
LOG_V("Undo viable_i");
m_viable[p.first] = p.second;
m_viable_trail.pop_back();
}
// a*v + b == 0 or a*v + b != 0
void viable::intersect_eq(rational const& a, pvar v, rational const& b, bool is_positive) {
bddv const& x = var2bits(v).var();
if (b == 0 && a.is_odd()) {
// hacky test optimizing special case.
// general case is compute inverse(a)*-b for equality 2^k*a*x + b == 0
// then constrain x.
//
intersect_viable(v, is_positive ? x.all0() : !x.all0());
}
else if (a.is_odd()) {
rational a_inv;
VERIFY(a.mult_inverse(x.size(), a_inv));
bdd eq = x == mod(a_inv * -b, rational::power_of_two(x.size()));
intersect_viable(v, is_positive ? eq : !eq);
}
else {
IF_VERBOSE(10, verbose_stream() << a << "*x + " << b << "\n");
bddv lhs = a * x + b;
bdd xs = is_positive ? lhs.all0() : !lhs.all0();
intersect_viable(v, xs);
}
}
bool viable::has_viable(pvar v) {
return !m_viable[v].is_false();
}
bool viable::is_viable(pvar v, rational const& val) {
return var2bits(v).contains(m_viable[v], val);
}
void viable::add_non_viable(pvar v, rational const& val) {
LOG("pvar " << v << " /= " << val);
SASSERT(is_viable(v, val));
auto const& bits = var2bits(v);
intersect_viable(v, bits.var() != val);
}
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);
}
dd::find_t viable::find_viable(pvar v, rational & val) {
return var2bits(v).find_hint(m_viable[v], s.m_value[v], val);
}
dd::fdd const& viable::sz2bits(unsigned sz) {
m_bits.reserve(sz + 1);
auto* bits = m_bits[sz];
if (!bits) {
m_bits.set(sz, alloc(dd::fdd, m_bdd, sz));
bits = m_bits[sz];
}
return *bits;
}
#if POLYSAT_LOGGING_ENABLED
void viable::log() {
// only for small problems
if (m_viable.size() < 10) {
for (pvar v = 0; v < m_viable.size(); ++v) {
log(v);
}
}
}
void viable::log(pvar v) {
if (s.size(v) <= 5) {
vector<rational> xs;
for (rational x = rational::zero(); x < rational::power_of_two(s.size(v)); x += 1) {
if (is_viable(v, x)) {
xs.push_back(x);
}
}
LOG("Viable for pvar " << v << ": " << xs);
} else {
LOG("Viable for pvar " << v << ": <range too big>");
}
}
#endif
dd::fdd const& viable::var2bits(pvar v) { return sz2bits(s.size(v)); }
}

91
src/math/polysat/viable.h Normal file
View file

@ -0,0 +1,91 @@
/*++
Copyright (c) 2021 Microsoft Corporation
Module Name:
maintain viable domains
Author:
Nikolaj Bjorner (nbjorner) 2021-03-19
Jakob Rath 2021-04-6
--*/
#pragma once
#include <limits>
#include "math/dd/dd_bdd.h"
#include "math/polysat/types.h"
namespace polysat {
class solver;
class viable {
typedef dd::bdd bdd;
solver& s;
dd::bdd_manager m_bdd;
scoped_ptr_vector<dd::fdd> m_bits;
vector<bdd> m_viable; // set of viable values.
vector<std::pair<pvar, bdd>> m_viable_trail;
public:
viable(solver& s);
void push() { m_viable.push_back(m_bdd.mk_true()); }
void pop() { m_viable.pop_back(); }
void push_viable(pvar v);
void pop_viable();
void intersect_eq(rational const& a, pvar v, rational const& b, bool is_positive);
/**
* Check whether variable v has any viable values left according to m_viable.
*/
bool has_viable(pvar v);
bool is_false(pvar v) { return m_viable[v].is_false(); }
/**
* 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);
/**
* Register all values that are not contained in vals as non-viable.
*/
void intersect_viable(pvar v, bdd vals);
/**
* Add dependency for variable viable range.
*/
void add_viable_dep(pvar v, p_dependency* dep);
/**
* 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_viable but for all variables */
void log();
dd::bdd_manager& get_bdd() { return m_bdd; }
dd::fdd const& sz2bits(unsigned sz);
dd::fdd const& var2bits(pvar v);
};
}