mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

For now, do not delete variables.

Browse source
This commit is contained in:
Jakob Rath 2022-11-16 15:49:58 +01:00
parent aa59de9056
commit 2c4e3184d7
1 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -121,6 +121,7 @@ namespace polysat {
}
void solver::del_var() {
NOT_IMPLEMENTED_YET(); // need to take care of helper variables in learned constraints, arising e.g. from bitwise "and"-terms.
// TODO also remove v from all learned constraints.
pvar v = m_value.size() - 1;
m_viable.pop_var();
@ -427,7 +428,12 @@ namespace polysat {
break;
}
case trail_instr_t::add_var_i: {
// NOTE: currently we cannot delete variables during solving,
// since lemmas may introduce new helper variables if they use operations like bitwise and or pseudo-inverse.
// For easier experimentation with new lemmas, we simply keep all variables for now.
#if 0
del_var();
#endif
break;
}
case trail_instr_t::inc_level_i: {