mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-20 12:03:33 -07:00
commit 82bc6474a3
11 changed files with 596 additions and 301 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -57,13 +57,13 @@ namespace polysat {
if (try_narrow_with(q, s)) {
rational val;
switch (s.find_viable(other_var, val)) {
case dd::find_result::empty:
case dd::find_t::empty:
s.set_conflict(*this);
return false;
case dd::find_result::singleton:
case dd::find_t::singleton:
s.propagate(other_var, val, *this);
return false;
case dd::find_result::multiple:
case dd::find_t::multiple:
/* do nothing */
break;
}
@ -95,7 +95,7 @@ namespace polysat {
pvar v = q.var();
rational a = q.hi().val();
rational b = q.lo().val();
bddv const& x = s.m_bdd.mk_var(s.sz2bits(s.size(v)));
bddv const& x = s.sz2bits(s.size(v)).var();
bdd xs = (a * x + b == rational(0));
s.intersect_viable(v, xs);
s.push_cjust(v, this);

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

@ -30,20 +30,18 @@ namespace polysat {
return *m_pdd[sz];
}
unsigned_vector const& solver::sz2bits(unsigned sz) {
dd::fdd const& solver::sz2bits(unsigned sz) {
m_bits.reserve(sz + 1);
auto* bits = m_bits[sz];
if (!bits) {
m_bits.set(sz, alloc(unsigned_vector));
m_bits.set(sz, alloc(dd::fdd, m_bdd, sz));
bits = m_bits[sz];
for (unsigned i = 0; i < sz; ++i)
bits->push_back(i);
}
return *bits;
}
bool solver::is_viable(pvar v, rational const& val) {
return m_viable[v].contains_num(val, sz2bits(size(v)));
return sz2bits(size(v)).contains(m_viable[v], val);
}
void solver::add_non_viable(pvar v, rational const& val) {
@ -51,7 +49,7 @@ namespace polysat {
TRACE("polysat", tout << "v" << v << " /= " << val << "\n";);
SASSERT(is_viable(v, val));
auto& bits = sz2bits(size(v));
intersect_viable(v, !m_bdd.mk_eq(bits, val));
intersect_viable(v, bits.var() != val);
}
void solver::intersect_viable(pvar v, bdd vals) {
@ -61,8 +59,8 @@ namespace polysat {
set_conflict(v);
}
dd::find_result solver::find_viable(pvar v, rational & val) {
return m_viable[v].find_num(sz2bits(size(v)), val);
dd::find_t solver::find_viable(pvar v, rational & val) {
return sz2bits(size(v)).find(m_viable[v], val);
}
solver::solver(reslimit& lim):
@ -326,15 +324,15 @@ namespace polysat {
IF_LOGGING(log_viable(v));
rational val;
switch (find_viable(v, val)) {
case dd::find_result::empty:
case dd::find_t::empty:
LOG("Conflict: no value for pvar " << v);
set_conflict(v);
break;
case dd::find_result::singleton:
case dd::find_t::singleton:
LOG("Propagation: pvar " << v << " := " << val << " (due to unique value)");
assign_core(v, val, justification::propagation(m_level));
break;
case dd::find_result::multiple:
case dd::find_t::multiple:
LOG("Decision: pvar " << v << " := " << val);
push_level();
assign_core(v, val, justification::decision(m_level));

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

@ -46,7 +46,7 @@ namespace polysat {
reslimit& m_lim;
scoped_ptr_vector<dd::pdd_manager> m_pdd;
scoped_ptr_vector<unsigned_vector> m_bits;
scoped_ptr_vector<dd::fdd> m_bits;
dd::bdd_manager m_bdd;
dep_value_manager m_value_manager;
small_object_allocator m_alloc;
@ -133,7 +133,7 @@ namespace polysat {
/**
* Find a next viable value for variable.
*/
dd::find_result find_viable(pvar v, rational & val);
dd::find_t find_viable(pvar v, rational & val);
/** Log all viable values for the given variable.
* (Inefficient, but useful for debugging small instances.)
@ -148,7 +148,7 @@ namespace polysat {
void del_var();
dd::pdd_manager& sz2pdd(unsigned sz);
unsigned_vector const& sz2bits(unsigned sz);
dd::fdd const& sz2bits(unsigned sz);
void push_level();
void pop_levels(unsigned num_levels);

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

@ -20,6 +20,7 @@ Author:
#include "util/ref_vector.h"
#include "math/dd/dd_pdd.h"
#include "math/dd/dd_bdd.h"
#include "math/dd/dd_fdd.h"
namespace polysat {