mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

create insert-fresh and insert for indexed_uint_set to make use cases with non-fresh inserts easier

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-08-03 09:48:07 -07:00
parent 0478ab1498
commit 7b36563196
5 changed files with 13 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/sat_ddfw.cpp
View file

@ -317,7 +317,7 @@ namespace sat {
// cls becomes false: flip any variable in clause to receive reward w // cls becomes false: flip any variable in clause to receive reward w
switch (ci.m_num_trues) { switch (ci.m_num_trues) {
case 0: { case 0: {
m_unsat.insert(cls_idx); m_unsat.insert_fresh(cls_idx);
clause const& c = get_clause(cls_idx); clause const& c = get_clause(cls_idx);
for (literal l : c) { for (literal l : c) {
inc_reward(l, w); inc_reward(l, w);
@ -406,7 +406,7 @@ namespace sat {
inc_reward(lit, ci.m_weight); inc_reward(lit, ci.m_weight);
inc_make(lit); inc_make(lit);
} }
m_unsat.insert(i); m_unsat.insert_fresh(i);
break; break;
case 1: case 1:
dec_reward(to_literal(ci.m_trues), ci.m_weight); dec_reward(to_literal(ci.m_trues), ci.m_weight);

2
src/sat/sat_ddfw.h
View file

@ -178,7 +178,7 @@ namespace sat {
inline void inc_make(literal lit) { inline void inc_make(literal lit) {
bool_var v = lit.var(); bool_var v = lit.var();
if (make_count(v)++ == 0) m_unsat_vars.insert(v); if (make_count(v)++ == 0) m_unsat_vars.insert_fresh(v);
} }
inline void dec_make(literal lit) { inline void dec_make(literal lit) {

4
src/sat/sat_lookahead.cpp
View file

@ -990,7 +990,7 @@ namespace sat {
m_rating.push_back(0); m_rating.push_back(0);
m_vprefix.push_back(prefix()); m_vprefix.push_back(prefix());
if (!m_s.was_eliminated(v)) if (!m_s.was_eliminated(v))
m_freevars.insert(v); m_freevars.insert_fresh(v);
} }
void lookahead::init(bool learned) { void lookahead::init(bool learned) {
@ -1096,7 +1096,7 @@ namespace sat {
literal l = m_trail[i]; literal l = m_trail[i];
set_undef(l); set_undef(l);
TRACE("sat", tout << "inserting free var v" << l.var() << "\n";); TRACE("sat", tout << "inserting free var v" << l.var() << "\n";);
m_freevars.insert(l.var()); m_freevars.insert_fresh(l.var());
} }
m_num_tc1 = m_num_tc1_lim.back(); m_num_tc1 = m_num_tc1_lim.back();

4
src/sat/sat_prob.cpp
View file

@ -80,7 +80,7 @@ namespace sat {
ci.del(lit); ci.del(lit);
switch (ci.m_num_trues) { switch (ci.m_num_trues) {
case 0: case 0:
m_unsat.insert(cls_idx); m_unsat.insert_fresh(cls_idx);
dec_break(lit); dec_break(lit);
break; break;
case 1: case 1:
@ -184,7 +184,7 @@ namespace sat {
} }
switch (ci.m_num_trues) { switch (ci.m_num_trues) {
case 0: case 0:
m_unsat.insert(i); m_unsat.insert_fresh(i);
break; break;
case 1: case 1:
inc_break(to_literal(ci.m_trues)); inc_break(to_literal(ci.m_trues));

7
src/util/uint_set.h
View file

@ -318,7 +318,7 @@ public:
m_size(0) m_size(0)
{} {}
void insert(unsigned x) { void insert_fresh(unsigned x) {
SASSERT(!contains(x)); SASSERT(!contains(x));
m_index.reserve(x + 1, UINT_MAX); m_index.reserve(x + 1, UINT_MAX);
m_elems.reserve(m_size + 1); m_elems.reserve(m_size + 1);
@ -327,6 +327,11 @@ public:
m_size++; m_size++;
SASSERT(contains(x)); SASSERT(contains(x));
} }
void insert(unsigned x) {
if (!contains(x))
insert_fresh(x);
}
void remove(unsigned x) { void remove(unsigned x) {
SASSERT(contains(x)); SASSERT(contains(x));