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

test stub

Browse source
This commit is contained in:
Jakob Rath 2023-06-15 11:53:06 +02:00
parent 136e819cb9
commit 40f794c5b4
3 changed files with 25 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -42,7 +42,7 @@ namespace polysat {
m_free_pvars(m_activity),
m_constraints(*this),
m_names(*this),
m_slicing(*this),
// m_slicing(*this),
m_search(*this) {
}
@ -148,6 +148,7 @@ namespace polysat {
m_trail.push_back(trail_instr_t::add_var_i);
m_free_pvars.mk_var_eh(v);
m_names.push_var(var(v)); // needs m_vars
m_slicing.add_var(sz);
return v;
}
@ -612,6 +613,7 @@ namespace polysat {
void solver::push_level() {
++m_level;
m_reinit_heads.push_back(m_clauses_to_reinit.size());
m_slicing.push_scope();
m_trail.push_back(trail_instr_t::inc_level_i);
}
@ -621,6 +623,7 @@ namespace polysat {
SASSERT(m_level >= num_levels);
unsigned const target_level = m_level - num_levels;
LOG("Pop " << num_levels << " levels (lvl " << m_level << " -> " << target_level << ")");
m_slicing.pop_scope(num_levels);
while (num_levels > 0) {
switch (m_trail.back()) {
case trail_instr_t::qhead_i: {

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

@ -141,6 +141,7 @@ namespace polysat {
friend class constraint_manager;
friend class name_manager;
friend class scoped_solverv;
friend class scoped_solver_slicing;
friend class test_polysat;
friend class test_fi;
friend struct inf_resolve_evaluated;