mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
add assertions
This commit is contained in:
parent
9a987237d5
commit
c11bd79484
|
@ -428,9 +428,8 @@ namespace sat {
|
|||
}
|
||||
|
||||
++m_stats.m_non_learned_generation;
|
||||
if (!m_searching) {
|
||||
m_mc.add_clause(num_lits, lits);
|
||||
}
|
||||
if (!m_searching)
|
||||
m_mc.add_clause(num_lits, lits);
|
||||
}
|
||||
|
||||
|
||||
|
@ -945,6 +944,7 @@ namespace sat {
|
|||
|
||||
void solver::assign_core(literal l, justification j) {
|
||||
SASSERT(value(l) == l_undef);
|
||||
SASSERT(!m_trail.contains(l) && !m_trail.contains(~l));
|
||||
TRACE("sat_assign_core", tout << l << " " << j << "\n";);
|
||||
if (j.level() == 0) {
|
||||
if (m_config.m_drat)
|
||||
|
@ -3654,11 +3654,14 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
m_trail.shrink(old_sz);
|
||||
DEBUG_CODE(for (literal l : m_trail) SASSERT(lvl(l.var()) <= new_lvl););
|
||||
m_qhead = m_trail.size();
|
||||
if (!m_replay_assign.empty()) IF_VERBOSE(20, verbose_stream() << "replay assign: " << m_replay_assign.size() << "\n");
|
||||
CTRACE("sat", !m_replay_assign.empty(), tout << "replay-assign: " << m_replay_assign << "\n";);
|
||||
for (unsigned i = m_replay_assign.size(); i-- > 0; ) {
|
||||
literal lit = m_replay_assign[i];
|
||||
SASSERT(value(lit) == l_true);
|
||||
SASSERT(!m_trail.contains(lit) && !m_trail.contains(~lit));
|
||||
m_trail.push_back(lit);
|
||||
}
|
||||
|
||||
|
@ -3709,11 +3712,11 @@ namespace sat {
|
|||
//
|
||||
|
||||
void solver::user_push() {
|
||||
|
||||
pop_to_base_level();
|
||||
m_free_var_freeze.push_back(m_free_vars);
|
||||
m_free_vars.reset(); // resetting free_vars forces new variables to be assigned above new_v
|
||||
bool_var new_v = mk_var(true, false);
|
||||
SASSERT(new_v + 1 == m_justification.size()); // there are no active variables that have higher values
|
||||
literal lit = literal(new_v, false);
|
||||
m_user_scope_literals.push_back(lit);
|
||||
m_cut_simplifier = nullptr; // for simplicity, wipe it out
|
||||
|
@ -3724,13 +3727,13 @@ namespace sat {
|
|||
|
||||
void solver::user_pop(unsigned num_scopes) {
|
||||
unsigned old_sz = m_user_scope_literals.size() - num_scopes;
|
||||
bool_var max_var = m_user_scope_literals[old_sz].var();
|
||||
bool_var max_var = m_user_scope_literals[old_sz].var();
|
||||
m_user_scope_literals.shrink(old_sz);
|
||||
|
||||
pop_to_base_level();
|
||||
if (m_ext)
|
||||
m_ext->user_pop(num_scopes);
|
||||
|
||||
|
||||
gc_vars(max_var);
|
||||
TRACE("sat", display(tout););
|
||||
|
||||
|
@ -3743,7 +3746,7 @@ namespace sat {
|
|||
m_free_vars.append(m_free_var_freeze[old_sz]);
|
||||
m_free_var_freeze.shrink(old_sz);
|
||||
scoped_suspend_rlimit _sp(m_rlimit);
|
||||
propagate(false);
|
||||
propagate(false);
|
||||
}
|
||||
|
||||
void solver::pop_to_base_level() {
|
||||
|
@ -4832,20 +4835,22 @@ namespace sat {
|
|||
return true;
|
||||
}
|
||||
|
||||
void solver::init_ts(unsigned n, svector<unsigned>& v, unsigned& ts) {
|
||||
if (v.empty())
|
||||
ts = 0;
|
||||
|
||||
ts++;
|
||||
if (ts == 0) {
|
||||
ts = 1;
|
||||
v.reset();
|
||||
}
|
||||
while (v.size() < n)
|
||||
v.push_back(0);
|
||||
}
|
||||
|
||||
void solver::init_visited() {
|
||||
if (m_visited.empty()) {
|
||||
m_visited_ts = 0;
|
||||
}
|
||||
m_visited_ts++;
|
||||
if (m_visited_ts == 0) {
|
||||
m_visited_ts = 1;
|
||||
m_visited.reset();
|
||||
}
|
||||
while (m_visited.size() < 2*num_vars()) {
|
||||
m_visited.push_back(0);
|
||||
}
|
||||
init_ts(2 * num_vars(), m_visited, m_visited_ts);
|
||||
}
|
||||
|
||||
|
||||
|
||||
};
|
||||
|
|
|
@ -343,6 +343,7 @@ namespace sat {
|
|||
void push_reinit_stack(clause & c);
|
||||
void push_reinit_stack(literal l1, literal l2);
|
||||
|
||||
void init_ts(unsigned n, svector<unsigned>& v, unsigned& ts);
|
||||
void init_visited();
|
||||
void mark_visited(literal l) { m_visited[l.index()] = m_visited_ts; }
|
||||
void mark_visited(bool_var v) { mark_visited(literal(v, false)); }
|
||||
|
|
Loading…
Reference in a new issue