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

use constraint_id type within viable

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-28 18:00:11 -08:00
parent 91b9d78cd3
commit 15f36f95a4
4 changed files with 16 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/sat/smt/polysat/core.cpp
View file

@ -190,7 +190,8 @@ namespace polysat {
case l_true:
propagate_assignment(m_var, m_value, d);
break;
case l_false:
case l_false:
// add m_var != m_value to m_viable but need a constraint index for that.
m_value = mod(m_value + 1, rational::power_of_two(size(m_var)));
goto try_again;
default:
@ -299,7 +300,7 @@ namespace polysat {
return;
v = w;
}
if (v != null_var && !m_viable.add_unitary(v, idx.id))
if (v != null_var && !m_viable.add_unitary(v, idx))
s.set_conflict(m_viable.explain(), "viable-conflict");
}
@ -352,7 +353,7 @@ namespace polysat {
if (!is_assigned(v0) || is_assigned(v1))
continue;
// detect unitary, add to viable, detect conflict?
if (value != l_undef && !m_viable.add_unitary(v1, idx))
if (value != l_undef && !m_viable.add_unitary(v1, {idx}))
s.set_conflict(m_viable.explain(), "viable-conflict");
}
SASSERT(m_watch[v].size() == sz && "size of watch list was not changed");

3
src/sat/smt/polysat/types.h
View file

@ -23,7 +23,8 @@ namespace polysat {
using pvar = unsigned;
using theory_var = unsigned;
struct constraint_id {
unsigned id; bool is_null() const { return id == UINT_MAX; }
unsigned id = UINT_MAX;
bool is_null() const { return id == UINT_MAX; }
static constraint_id null() { return constraint_id{ UINT_MAX }; }
};

12
src/sat/smt/polysat/viable.cpp
View file

@ -68,7 +68,7 @@ namespace polysat {
}
};
viable::entry* viable::alloc_entry(pvar var, unsigned constraint_index) {
viable::entry* viable::alloc_entry(pvar var, constraint_id constraint_index) {
entry* e = nullptr;
if (m_alloc.empty())
e = alloc(entry);
@ -532,12 +532,12 @@ namespace polysat {
uint_set seen;
for (auto e : m_explain) {
auto index = e->constraint_index;
if (seen.contains(index))
if (seen.contains(index.id))
continue;
if (m_var != e->var)
result.push_back(offset_claim(m_var, {e->var, 0}));
seen.insert(index);
auto const& [sc, d, value] = c.m_constraint_index[index];
seen.insert(index.id);
auto const& [sc, d, value] = c.m_constraint_index[index.id];
result.push_back(d);
result.append(c.explain_eval(sc));
}
@ -548,11 +548,11 @@ namespace polysat {
/*
* Register constraint at index 'idx' as unitary in v.
*/
bool viable::add_unitary(pvar v, unsigned idx) {
bool viable::add_unitary(pvar v, constraint_id idx) {
if (c.is_assigned(v))
return true;
auto [sc, d, value] = c.m_constraint_index[idx];
auto [sc, d, value] = c.m_constraint_index[idx.id];
SASSERT(value != l_undef);
if (value == l_false)
sc = ~sc;

8
src/sat/smt/polysat/viable.h
View file

@ -53,7 +53,7 @@ namespace polysat {
bool active = true;
bool valid_for_lemma = true;
pvar var = null_var;
unsigned constraint_index = UINT_MAX;
constraint_id constraint_index;
void reset() {
// dll_base<entry>::init(this); // we never did this in alloc_entry either
@ -62,7 +62,7 @@ namespace polysat {
active = true;
valid_for_lemma = true;
var = null_var;
constraint_index = UINT_MAX;
constraint_index = constraint_id::null();
}
};
@ -97,7 +97,7 @@ namespace polysat {
bool well_formed(entry* e);
bool well_formed(layers const& ls);
entry* alloc_entry(pvar v, unsigned constraint_index);
entry* alloc_entry(pvar v, constraint_id constraint_index);
std::ostream& display_one(std::ostream& out, pvar v, entry const* e) const;
std::ostream& display_all(std::ostream& out, pvar v, entry const* e, char const* delimiter = "") const;
@ -152,7 +152,7 @@ namespace polysat {
/*
* Register constraint at index 'idx' as unitary in v.
*/
bool add_unitary(pvar v, unsigned idx);
bool add_unitary(pvar v, constraint_id);
/*
* Ensure data-structures tracking variable v.