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

track dependency of base-level conflict

Browse source
This commit is contained in:
Jakob Rath 2023-02-01 10:47:26 +01:00
parent 3c822117d1
commit 1bb68a4fc1
4 changed files with 10 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -158,6 +158,7 @@ namespace polysat {
SASSERT(m_vars_occurring.empty());
SASSERT(m_lemmas.empty());
SASSERT(m_narrow_queue.empty());
SASSERT(m_dep.is_null());
}
return is_empty;
}
@ -170,6 +171,7 @@ namespace polysat {
m_lemmas.reset();
m_narrow_queue.reset();
m_level = UINT_MAX;
m_dep = null_dependency;
SASSERT(empty());
}
@ -181,10 +183,11 @@ namespace polysat {
return contains(lit) || contains(~lit);
}
void conflict::init_at_base_level() {
void conflict::init_at_base_level(dependency dep) {
SASSERT(empty());
SASSERT(s.at_base_level());
m_level = s.m_level;
m_dep = dep;
SASSERT(!empty());
// TODO: logger().begin_conflict???
// TODO: check uses of logger().begin_conflict(). sometimes we call it before adding constraints, sometimes after...
@ -434,7 +437,7 @@ namespace polysat {
clause_builder lemma(s);
for (auto c : *this)
for (signed_constraint c : *this)
lemma.insert(~c);
for (unsigned v : m_vars) {

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

@ -101,6 +101,7 @@ namespace polysat {
// Level at which the conflict was discovered
unsigned m_level = UINT_MAX;
dependency m_dep = null_dependency;
public:
conflict(solver& s);
@ -126,7 +127,7 @@ namespace polysat {
bool is_relevant(sat::literal lit) const;
/** conflict due to obvious input inconsistency */
void init_at_base_level();
void init_at_base_level(dependency dep);
/** conflict because the constraint c is false under current variable assignment */
void init(signed_constraint c);
/** boolean conflict with the given clause */

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

@ -158,8 +158,7 @@ namespace polysat {
case l_false:
// Input literal contradicts current boolean state (e.g., opposite literals in the input)
// => conflict only flags the inconsistency
set_conflict_at_base_level();
SASSERT(dep == null_dependency && "track dependencies is TODO");
set_conflict_at_base_level(dep);
return;
case l_true:
// constraint c is already asserted => ignore
@ -174,8 +173,7 @@ namespace polysat {
case l_false:
// asserted an always-false constraint => conflict at base level
LOG("Always false: " << c);
set_conflict_at_base_level();
SASSERT(dep == null_dependency && "track dependencies is TODO");
set_conflict_at_base_level(dep);
return;
case l_true:
// asserted an always-true constraint => ignore

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

@ -253,7 +253,7 @@ namespace polysat {
void erase_pwatch(pvar v, constraint* c);
void erase_pwatch(constraint* c);
void set_conflict_at_base_level() { m_conflict.init_at_base_level(); }
void set_conflict_at_base_level(dependency dep) { m_conflict.init_at_base_level(dep); }
void set_conflict(signed_constraint c) { m_conflict.init(c); }
void set_conflict(clause& cl) { m_conflict.init(cl); }
void set_conflict_by_viable_interval(pvar v) { m_conflict.init_by_viable_interval(v); }