mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-12 10:14:42 +00:00
Code Activity

theory case split WIP

Browse source
This commit is contained in:
Murphy Berzish 2016-12-20 11:14:42 -05:00
parent 94762d276d
commit a04bc9974b
2 changed files with 37 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/smt/smt_context.cpp
View file

@ -1750,6 +1750,8 @@ namespace smt {
if (inconsistent())
return false;
unsigned qhead = m_qhead;
if (!propagate_th_case_split())
return false;
if (!bcp())
return false;
if (get_cancel_flag())
@ -2956,10 +2958,32 @@ namespace smt {
}
}
} else {
NOT_IMPLEMENTED_YET();
int_set new_case_split; // TODO is it okay to allocate this on the stack?
for (unsigned i = 0; i < num_lits; ++i) {
literal l = lits[i];
// TODO do we need to enforce this invariant? can we make undo information work without it?
SASSERT(!m_all_th_case_split_literals.contains(l.index()));
m_all_th_case_split_literals.insert(l.index());
// TODO add undo information for this insert
new_case_split.insert(l.index());
}
m_th_case_split_sets.push_back(new_case_split);
push_trail(push_back_vector<context, vector<int_set> >(m_th_case_split_sets));
for (unsigned i = 0; i < num_lits; ++i) {
literal l = lits[i];
m_literal2casesplitsets[l.index()].push_back(new_case_split);
push_trail(push_back_vector<context, vector<int_set> >(m_literal2casesplitsets[l.index()]));
}
}
}
bool context::propagate_th_case_split() {
if (m_all_th_case_split_literals.empty())
return true;
NOT_IMPLEMENTED_YET(); return true;
}
bool context::reduce_assertions() {
if (!m_asserted_formulas.inconsistent()) {
SASSERT(at_base_level());