mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-04-04 16:20:09 -07:00
parent 52d37f131d
commit 446654b680
5 changed files with 92 additions and 69 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/dd/dd_pdd.cpp
View file

@ -126,7 +126,7 @@ namespace dd {
* Example: 2^4*x + 2 is non-zero for every x.
*/
bool pdd_manager::is_non_zero(PDD p) {
bool pdd_manager::is_never_zero(PDD p) {
if (is_val(p))
return !is_zero(p);
if (m_semantics != mod2N_e)

4
src/math/dd/dd_pdd.h
View file

@ -206,7 +206,7 @@ namespace dd {
inline bool is_one(PDD p) const { return p == one_pdd; }
inline bool is_val(PDD p) const { return m_nodes[p].is_val(); }
inline bool is_internal(PDD p) const { return m_nodes[p].is_internal(); }
bool is_non_zero(PDD p);
bool is_never_zero(PDD p);
inline unsigned level(PDD p) const { return m_nodes[p].m_level; }
inline unsigned var(PDD p) const { return m_level2var[level(p)]; }
inline PDD lo(PDD p) const { return m_nodes[p].m_lo; }
@ -343,7 +343,7 @@ namespace dd {
bool is_unary() const { return !is_val() && lo().is_zero() && hi().is_val(); }
bool is_binary() const { return m.is_binary(root); }
bool is_monomial() const { return m.is_monomial(root); }
bool is_non_zero() const { return m.is_non_zero(root); }
bool is_never_zero() const { return m.is_never_zero(root); }
bool var_is_leaf(unsigned v) const { return m.var_is_leaf(root, v); }
pdd operator-() const { return m.minus(*this); }

122
src/math/polysat/polysat.cpp
View file

@ -73,20 +73,18 @@ namespace polysat {
return l_undef;
}
struct solver::t_del_var : public trail {
solver& s;
t_del_var(solver& s): s(s) {}
void undo() override { s.del_var(); }
};
solver::solver(trail_stack& s, reslimit& lim):
m_trail(s),
m_lim(lim),
m_bdd(1000),
m_dep_manager(m_value_manager, m_alloc),
m_conflict_dep(nullptr, m_dep_manager),
m_dm(m_value_manager, m_alloc),
m_conflict_dep(nullptr, m_dm),
m_free_vars(m_activity) {
}
@ -108,7 +106,7 @@ namespace polysat {
m_value.push_back(rational::zero());
m_justification.push_back(justification::unassigned());
m_viable.push_back(m_bdd.mk_true());
m_vdeps.push_back(m_dep_manager.mk_empty());
m_vdeps.push_back(m_dm.mk_empty());
m_cjust.push_back(constraints());
m_watch.push_back(ptr_vector<constraint>());
m_activity.push_back(0);
@ -134,7 +132,7 @@ namespace polysat {
}
void solver::add_eq(pdd const& p, unsigned dep) {
p_dependency_ref d(mk_dep(dep), m_dep_manager);
p_dependency_ref d(mk_dep(dep), m_dm);
constraint* c = constraint::eq(m_level, p, d);
m_constraints.push_back(c);
add_watch(*c);
@ -178,7 +176,7 @@ namespace polysat {
if (!dep)
return;
m_trail.push(vector_value_trail<p_dependency*, false>(m_vdeps, var));
m_vdeps[var] = m_dep_manager.mk_join(m_vdeps[var], dep);
m_vdeps[var] = m_dm.mk_join(m_vdeps[var], dep);
}
bool solver::can_propagate() {
@ -232,15 +230,11 @@ namespace polysat {
}
}
vector<std::pair<unsigned, rational>> sub;
for (auto w : vars)
if (is_assigned(w))
sub.push_back(std::make_pair(w, m_value[w]));
auto p = c.p().subst_val(sub);
auto p = c.p().subst_val(m_sub);
if (p.is_zero())
return false;
if (p.is_non_zero()) {
if (p.is_never_zero()) {
// we could tag constraint to allow early substitution before
// swapping watch variable in case we can detect conflict earlier.
set_conflict(c);
@ -266,7 +260,7 @@ namespace polysat {
VERIFY(a.mult_inverse(sz, inv_a));
rational val = mod(inv_a * -b, rational::power_of_two(sz));
m_cjust[other_var].push_back(&c);
propagate(other_var, val, justification::propagation(m_level));
propagate(other_var, val, c);
return false;
}
@ -277,12 +271,11 @@ namespace polysat {
return false;
}
void solver::propagate(unsigned var, rational const& val, justification const& j) {
SASSERT(j.is_propagation());
void solver::propagate(unsigned var, rational const& val, constraint& c) {
if (is_viable(var, val))
assign_core(var, val, j);
assign_core(var, val, justification::propagation(m_level));
else
set_conflict(*m_cjust[var].back());
set_conflict(c);
}
void solver::push_level() {
@ -312,9 +305,8 @@ namespace polysat {
*/
void solver::pop_assignment() {
while (!m_search.empty() && m_justification[m_search.back()].level() > m_level) {
auto v = m_search.back();
undo_var(m_search.back());
m_search.pop_back();
pop_search();
}
}
@ -322,7 +314,18 @@ namespace polysat {
m_justification[v] = justification::unassigned();
m_free_vars.unassign_var_eh(v);
m_cjust[v].reset();
m_viable[v] = m_bdd.mk_true();
m_viable[v] = m_bdd.mk_true(); // TBD does not work with external bit-assignments
}
void solver::pop_search() {
m_search.pop_back();
m_sub.pop_back();
}
void solver::push_search(unsigned var, rational const& val) {
m_search.push_back(var);
m_value[var] = val;
m_sub.push_back(std::make_pair(var, val));
}
void solver::add_watch(constraint& c) {
@ -361,7 +364,7 @@ namespace polysat {
unsigned var = m_free_vars.next_var();
switch (find_viable(var, val)) {
case l_false:
set_conflict(m_cjust[var]);
set_conflict(var);
break;
case l_true:
assign_core(var, val, justification::propagation(m_level));
@ -375,15 +378,30 @@ namespace polysat {
void solver::assign_core(unsigned var, rational const& val, justification const& j) {
SASSERT(is_viable(var, val));
m_search.push_back(var);
m_value[var] = val;
push_search(var, val);
m_justification[var] = j;
}
void solver::set_conflict(constraint& c) {
SASSERT(m_conflict_cs.empty());
m_conflict_cs.push_back(&c);
m_conflict_dep = nullptr;
}
void solver::set_conflict(unsigned v) {
SASSERT(m_conflict_cs.empty());
m_conflict_cs.append(m_cjust[v]);
m_conflict_dep = m_vdeps[v];
if (m_cjust[v].empty())
m_conflict_cs.push_back(nullptr);
}
/**
* Conflict resolution.
* - m_conflict are constraints that are infeasible in the current assignment.
* 1. walk m_search from top down until last variable in m_conflict.
* - m_conflict_cs are constraints that are infeasible in the current assignment.
* - m_conflict_dep are dependencies for infeasibility
* 1. walk m_search from top down until last variable in m_conflict_cs.
* 2. resolve constraints in m_cjust to isolate lowest degree polynomials
* using variable.
* Use Olm-Seidl division by powers of 2 to preserve invertibility.
@ -399,12 +417,10 @@ namespace polysat {
*
*/
void solver::resolve_conflict() {
vector<pdd> ps = init_conflict();
unsigned v = UINT_MAX;
unsigned i = m_search.size();
vector<std::pair<unsigned, rational>> sub;
for (auto w : m_search)
sub.push_back(std::make_pair(w, m_value[w]));
for (; i-- > 0; ) {
v = m_search[i];
@ -422,12 +438,12 @@ namespace polysat {
return;
}
pdd r = resolve(v, ps);
pdd rval = r.subst_val(sub);
if (r.is_val() && rval.is_non_zero()) {
pdd rval = r.subst_val(m_sub);
if (r.is_val() && rval.is_never_zero()) {
report_unsat();
return;
}
if (!rval.is_non_zero()) {
if (!rval.is_never_zero()) {
backtrack(i);
return;
}
@ -442,28 +458,23 @@ namespace polysat {
}
vector<pdd> solver::init_conflict() {
SASSERT(!m_conflict.empty());
SASSERT(!m_conflict_cs.empty());
m_conflict_level = 0;
vector<pdd> ps;
reset_marks();
m_conflict_level = 0;
m_conflict_dep = nullptr;
for (auto* c : m_conflict) {
for (auto* c : m_conflict_cs) {
if (!c)
continue;
for (auto v : c->vars())
set_mark(v);
ps.push_back(c->p());
m_conflict_level = std::max(m_conflict_level, c->level());
m_conflict_dep = m_dep_manager.mk_join(m_conflict_dep, c->dep());
m_conflict_dep = m_dm.mk_join(m_conflict_dep, c->dep());
}
m_conflict.reset();
m_conflict_cs.reset();
return ps;
}
/**
* TBD: m_conflict_dep is a justification that m_value[v] is not viable.
* it is currently not yet being accounted for.
* A more general data-structure could be to maintain a p_dependency
* with each variable state. The dependencies are augmented on backtracking.
*/
void solver::backtrack(unsigned i) {
do {
auto v = m_search[i];
@ -481,16 +492,17 @@ namespace polysat {
void solver::report_unsat() {
backjump(base_level());
m_conflict.push_back(nullptr);
SASSERT(m_conflict_cs.empty());
m_conflict_cs.push_back(nullptr);
}
void solver::unsat_core(unsigned_vector& deps) {
deps.reset();
for (auto* c : m_conflict) {
for (auto* c : m_conflict_cs) {
if (c)
m_conflict_dep = m_dep_manager.mk_join(c->dep(), m_conflict_dep);
m_conflict_dep = m_dm.mk_join(c->dep(), m_conflict_dep);
}
m_dep_manager.linearize(m_conflict_dep, deps);
m_dm.linearize(m_conflict_dep, deps);
}
@ -520,16 +532,15 @@ namespace polysat {
backjump(new_level + 1);
while (m_search.back() != v) {
undo_var(m_search.back());
m_search.pop_back();
pop_search();
}
SASSERT(!m_search.empty());
SASSERT(m_search.back() == v);
m_search.pop_back();
pop_search();
add_non_viable(v, m_value[v]);
add_viable_dep(v, m_conflict_dep);
m_qhead = m_search.size();
rational value;
m_conflict_dep = nullptr;
switch (find_viable(v, value)) {
case l_true:
assign_core(v, value, justification::propagation(new_level));
@ -538,7 +549,7 @@ namespace polysat {
assign_core(v, value, justification::decision(new_level));
break;
case l_false:
set_conflict(m_cjust[v]);
set_conflict(v);
break;
}
}
@ -569,6 +580,7 @@ namespace polysat {
auto const& cs = m_cjust[v];
pdd r = isolate(v, ps);
auto degree = r.degree(v);
m_conflict_dep = m_dm.mk_join(m_conflict_dep, m_vdeps[v]);
while (degree > 0) {
for (auto * c : cs) {
if (degree >= c->p().degree(v)) {
@ -576,7 +588,7 @@ namespace polysat {
// add parity condition to presere falsification
degree = r.degree(v);
m_conflict_level = std::max(m_conflict_level, c->level());
m_conflict_dep = m_dep_manager.mk_join(m_conflict_dep.get(), c->dep());
m_conflict_dep = m_dm.mk_join(m_conflict_dep.get(), c->dep());
}
}
}
@ -624,6 +636,10 @@ namespace polysat {
}
std::ostream& solver::display(std::ostream& out) const {
for (auto v : m_search) {
out << "v" << v << " := " << m_value[v] << "\n";
out << m_viable[v] << "\n";
}
for (auto* c : m_constraints)
out << *c << "\n";
for (auto* c : m_redundant)

21
src/math/polysat/polysat.h
View file

@ -32,6 +32,7 @@ namespace polysat {
typedef dd::bdd bdd;
const unsigned null_dependency = UINT_MAX;
const unsigned null_var = UINT_MAX;
struct dep_value_manager {
void inc_ref(unsigned) {}
@ -120,9 +121,10 @@ namespace polysat {
dd::bdd_manager m_bdd;
dep_value_manager m_value_manager;
small_object_allocator m_alloc;
poly_dep_manager m_dep_manager;
p_dependency_ref m_conflict_dep;
poly_dep_manager m_dm;
var_queue m_free_vars;
p_dependency_ref m_conflict_dep;
ptr_vector<constraint> m_conflict_cs;
// Per constraint state
scoped_ptr_vector<constraint> m_constraints;
@ -133,7 +135,7 @@ namespace polysat {
ptr_vector<p_dependency> m_vdeps; // dependencies for viable values
vector<rational> m_value; // assigned value
vector<justification> m_justification; // justification for variable assignment
vector<constraints> m_cjust; // constraints used for justification
vector<constraints> m_cjust; // constraints justifying variable range.
vector<constraints> m_watch; // watch list datastructure into constraints.
unsigned_vector m_activity;
vector<pdd> m_vars;
@ -141,6 +143,8 @@ namespace polysat {
// search state that lists assigned variables
unsigned_vector m_search;
vector<std::pair<unsigned, rational>> m_sub;
unsigned m_qhead { 0 };
unsigned m_level { 0 };
@ -190,6 +194,9 @@ namespace polysat {
void pop_assignment();
void pop_constraints(scoped_ptr_vector<constraint>& cs);
void push_search(unsigned v, rational const& val);
void pop_search();
void assign_core(unsigned var, rational const& val, justification const& j);
bool is_assigned(unsigned var) const { return !m_justification[var].is_unassigned(); }
@ -197,13 +204,13 @@ namespace polysat {
void propagate(unsigned v);
bool propagate(unsigned v, constraint& c);
bool propagate_eq(unsigned v, constraint& c);
void propagate(unsigned var, rational const& val, justification const& j);
void propagate(unsigned var, rational const& val, constraint& c);
void erase_watch(unsigned v, constraint& c);
void erase_watch(constraint& c);
void add_watch(constraint& c);
void set_conflict(constraint& c) { m_conflict.push_back(&c); }
void set_conflict(ptr_vector<constraint>& cs) { m_conflict.append(cs); }
void set_conflict(constraint& c);
void set_conflict(unsigned v);
unsigned_vector m_marks;
unsigned m_clock { 0 };
@ -219,7 +226,7 @@ namespace polysat {
bool can_decide() const { return !m_free_vars.empty(); }
void decide();
p_dependency* mk_dep(unsigned dep) { return dep == null_dependency ? nullptr : m_dep_manager.mk_leaf(dep); }
p_dependency* mk_dep(unsigned dep) { return dep == null_dependency ? nullptr : m_dm.mk_leaf(dep); }
bool is_conflict() const { return !m_conflict.empty(); }
bool at_base_level() const;

12
src/test/pdd.cpp
View file

@ -314,12 +314,12 @@ public :
std::cout << "sub 2 " << p.subst_val(sub2) << "\n";
std::cout << "sub 3 " << p.subst_val(sub3) << "\n";
std::cout << "expect 1 " << (2*a + 1).is_non_zero() << "\n";
std::cout << "expect 1 " << (2*a*b + 2*b + 1).is_non_zero() << "\n";
std::cout << "expect 0 " << (2*a + 2).is_non_zero() << "\n";
SASSERT((2*a + 1).is_non_zero());
SASSERT((2*a + 2*b + 1).is_non_zero());
SASSERT(!(2*a*b + 3*b + 2).is_non_zero());
std::cout << "expect 1 " << (2*a + 1).is_never_zero() << "\n";
std::cout << "expect 1 " << (2*a*b + 2*b + 1).is_never_zero() << "\n";
std::cout << "expect 0 " << (2*a + 2).is_never_zero() << "\n";
SASSERT((2*a + 1).is_never_zero());
SASSERT((2*a + 2*b + 1).is_never_zero());
SASSERT(!(2*a*b + 3*b + 2).is_never_zero());
}
};