mirror of
https://github.com/Z3Prover/z3
synced 2025-08-01 17:03:18 +00:00
add resolved attribute
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
e50c612068
commit
eb9bfbb3d8
4 changed files with 20 additions and 2 deletions
|
@ -49,6 +49,8 @@ namespace polysat {
|
||||||
for (auto si : s.m_search) {
|
for (auto si : s.m_search) {
|
||||||
if (!si.is_boolean())
|
if (!si.is_boolean())
|
||||||
continue;
|
continue;
|
||||||
|
if (si.is_resolved())
|
||||||
|
continue;
|
||||||
auto c1 = s.lit2cnstr(si.lit());
|
auto c1 = s.lit2cnstr(si.lit());
|
||||||
if (!c1->contains_var(v))
|
if (!c1->contains_var(v))
|
||||||
continue;
|
continue;
|
||||||
|
|
|
@ -323,6 +323,8 @@ namespace polysat {
|
||||||
for (auto si : s.m_search) {
|
for (auto si : s.m_search) {
|
||||||
if (!si.is_boolean())
|
if (!si.is_boolean())
|
||||||
continue;
|
continue;
|
||||||
|
if (si.is_resolved())
|
||||||
|
continue;
|
||||||
auto dd = s.lit2cnstr(si.lit());
|
auto dd = s.lit2cnstr(si.lit());
|
||||||
if (!dd->is_ule())
|
if (!dd->is_ule())
|
||||||
continue;
|
continue;
|
||||||
|
@ -347,6 +349,8 @@ namespace polysat {
|
||||||
for (auto si : s.m_search) {
|
for (auto si : s.m_search) {
|
||||||
if (!si.is_boolean())
|
if (!si.is_boolean())
|
||||||
continue;
|
continue;
|
||||||
|
if (si.is_resolved())
|
||||||
|
continue;
|
||||||
auto dd = s.lit2cnstr(si.lit());
|
auto dd = s.lit2cnstr(si.lit());
|
||||||
if (!dd->is_ule())
|
if (!dd->is_ule())
|
||||||
continue;
|
continue;
|
||||||
|
@ -380,6 +384,8 @@ namespace polysat {
|
||||||
for (auto si : s.m_search) {
|
for (auto si : s.m_search) {
|
||||||
if (!si.is_boolean())
|
if (!si.is_boolean())
|
||||||
continue;
|
continue;
|
||||||
|
if (si.is_resolved())
|
||||||
|
continue;
|
||||||
auto dd = s.lit2cnstr(si.lit());
|
auto dd = s.lit2cnstr(si.lit());
|
||||||
if (!dd->is_ule())
|
if (!dd->is_ule())
|
||||||
continue;
|
continue;
|
||||||
|
|
|
@ -32,6 +32,7 @@ namespace polysat {
|
||||||
pvar m_var;
|
pvar m_var;
|
||||||
sat::literal m_lit;
|
sat::literal m_lit;
|
||||||
};
|
};
|
||||||
|
bool m_resolved = false; // when marked as resolved it is no longer valid to reduce the conflict state
|
||||||
|
|
||||||
search_item(pvar var): m_kind(search_item_k::assignment), m_var(var) {}
|
search_item(pvar var): m_kind(search_item_k::assignment), m_var(var) {}
|
||||||
search_item(sat::literal lit): m_kind(search_item_k::boolean), m_lit(lit) {}
|
search_item(sat::literal lit): m_kind(search_item_k::boolean), m_lit(lit) {}
|
||||||
|
@ -40,9 +41,11 @@ namespace polysat {
|
||||||
static search_item boolean(sat::literal lit) { return search_item(lit); }
|
static search_item boolean(sat::literal lit) { return search_item(lit); }
|
||||||
bool is_assignment() const { return m_kind == search_item_k::assignment; }
|
bool is_assignment() const { return m_kind == search_item_k::assignment; }
|
||||||
bool is_boolean() const { return m_kind == search_item_k::boolean; }
|
bool is_boolean() const { return m_kind == search_item_k::boolean; }
|
||||||
|
bool is_resolved() const { return m_resolved; }
|
||||||
search_item_k kind() const { return m_kind; }
|
search_item_k kind() const { return m_kind; }
|
||||||
pvar var() const { SASSERT(is_assignment()); return m_var; }
|
pvar var() const { SASSERT(is_assignment()); return m_var; }
|
||||||
sat::literal lit() const { SASSERT(is_boolean()); return m_lit; }
|
sat::literal lit() const { SASSERT(is_boolean()); return m_lit; }
|
||||||
|
void set_resolved() { m_resolved = true; }
|
||||||
};
|
};
|
||||||
|
|
||||||
class search_state {
|
class search_state {
|
||||||
|
@ -65,6 +68,8 @@ namespace polysat {
|
||||||
|
|
||||||
void pop_asssignment();
|
void pop_asssignment();
|
||||||
|
|
||||||
|
void set_resolved(unsigned i) { m_items[i].set_resolved(); }
|
||||||
|
|
||||||
using const_iterator = decltype(m_items)::const_iterator;
|
using const_iterator = decltype(m_items)::const_iterator;
|
||||||
const_iterator begin() const { return m_items.begin(); }
|
const_iterator begin() const { return m_items.begin(); }
|
||||||
const_iterator end() const { return m_items.end(); }
|
const_iterator end() const { return m_items.end(); }
|
||||||
|
@ -128,7 +133,11 @@ namespace polysat {
|
||||||
init();
|
init();
|
||||||
}
|
}
|
||||||
|
|
||||||
search_item const& operator*() const {
|
void set_resolved() {
|
||||||
|
m_search->set_resolved(current);
|
||||||
|
}
|
||||||
|
|
||||||
|
search_item const& operator*() {
|
||||||
return (*m_search)[current];
|
return (*m_search)[current];
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -477,7 +477,8 @@ namespace polysat {
|
||||||
while (search_it.next()) {
|
while (search_it.next()) {
|
||||||
LOG("search state: " << m_search);
|
LOG("search state: " << m_search);
|
||||||
LOG("Conflict: " << m_conflict);
|
LOG("Conflict: " << m_conflict);
|
||||||
auto const& item = *search_it;
|
auto& item = *search_it;
|
||||||
|
search_it.set_resolved();
|
||||||
LOG_H2("Working on " << search_item_pp(m_search, item));
|
LOG_H2("Working on " << search_item_pp(m_search, item));
|
||||||
if (item.is_assignment()) {
|
if (item.is_assignment()) {
|
||||||
// Resolve over variable assignment
|
// Resolve over variable assignment
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue