mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 22:03:39 +00:00
Code Activity

more stub

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-03-31 13:27:34 -07:00
parent 8730f0aef7
commit 2e4b1fb5e0
2 changed files with 19 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -102,10 +102,6 @@ namespace polysat {
} }
void solver::add_eq(pdd const& p, unsigned dep) { void solver::add_eq(pdd const& p, unsigned dep) {
//
// TODO reduce p using assignment (at current level,
// assuming constraint is removed also at current level).
//
constraint* c = constraint::eq(m_level, p, m_dep_manager.mk_leaf(dep)); constraint* c = constraint::eq(m_level, p, m_dep_manager.mk_leaf(dep));
m_constraints.push_back(c); m_constraints.push_back(c);
add_watch(*c); add_watch(*c);
@ -370,8 +366,7 @@ namespace polysat {
v = m_search[i]; v = m_search[i];
if (!is_marked(v)) if (!is_marked(v))
continue; continue;
pdd q = isolate(v); pdd r = resolve(v, p);
pdd r = resolve(v, q, p);
pdd rval = r.subst_val(sub); pdd rval = r.subst_val(sub);
if (!rval.is_non_zero()) if (!rval.is_non_zero())
goto backtrack; goto backtrack;
@ -426,8 +421,9 @@ namespace polysat {
pdd solver::isolate(unsigned v) { pdd solver::isolate(unsigned v) {
if (m_cjust[v].empty()) if (m_cjust[v].empty())
return sz2pdd(m_size[v]).zero(); return sz2pdd(m_size[v]).zero();
pdd p = m_cjust[v][0]->p(); auto const& cs = m_cjust[v];
for (unsigned i = m_cjust[v].size(); i-- > 1; ) { pdd p = cs[0]->p();
for (unsigned i = cs.size(); i-- > 1; ) {
// TBD reduce with respect to v // TBD reduce with respect to v
} }
return p; return p;
@ -436,9 +432,20 @@ namespace polysat {
/** /**
* Return residue of superposing p and q with respect to v. * Return residue of superposing p and q with respect to v.
*/ */
pdd solver::resolve(unsigned v, pdd const& p, pdd const& q) { pdd solver::resolve(unsigned v, pdd const& p) {
// TBD remove as much trace of v as possible. auto degree = p.degree(v);
return p; auto const& cs = m_cjust[v];
pdd r = p;
while (degree > 0) {
for (auto * c : cs) {
if (degree >= c->p().degree(v)) {
// TODO binary resolve, update r using result
// add parity condition to presere falsification
degree = r.degree(v);
}
}
}
return r;
} }
void solver::reset_marks() { void solver::reset_marks() {

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

@ -167,7 +167,7 @@ namespace polysat {
void set_mark(unsigned v) { m_marks[v] = m_clock; } void set_mark(unsigned v) { m_marks[v] = m_clock; }
pdd isolate(unsigned v); pdd isolate(unsigned v);
pdd resolve(unsigned v, pdd const& p, pdd const& q); pdd resolve(unsigned v, pdd const& p);
void decide(); void decide();
void resolve_conflict_core(); void resolve_conflict_core();