mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-11 13:40:52 +00:00
Code Activity

reworking cancellation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-11 16:43:48 -08:00
parent baee4225a7
commit 96d1066c6a
13 changed files with 42 additions and 47 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/math/subpaving/tactic/subpaving_tactic.cpp
View file

@ -103,11 +103,11 @@ class subpaving_tactic : public tactic {
if (m_kind != new_kind) {
m_kind = new_kind;
switch (m_kind) {
case MPQ: m_ctx = subpaving::mk_mpq_context(m_qm); break;
case MPF: m_ctx = subpaving::mk_mpf_context(m_fm); break;
case HWF: m_ctx = subpaving::mk_hwf_context(m_hm, m_qm); break;
case MPFF: m_ctx = subpaving::mk_mpff_context(m_ffm, m_qm); break;
case MPFX: m_ctx = subpaving::mk_mpfx_context(m_fxm, m_qm); break;
case MPQ: m_ctx = subpaving::mk_mpq_context(m().limit(), m_qm); break;
case MPF: m_ctx = subpaving::mk_mpf_context(m().limit(), m_fm); break;
case HWF: m_ctx = subpaving::mk_hwf_context(m().limit(), m_hm, m_qm); break;
case MPFF: m_ctx = subpaving::mk_mpff_context(m().limit(), m_ffm, m_qm); break;
case MPFX: m_ctx = subpaving::mk_mpfx_context(m().limit(), m_fxm, m_qm); break;
default: UNREACHABLE(); break;
}
m_e2s = alloc(expr2subpaving, m_manager, *m_ctx, &m_e2v);
@ -123,10 +123,6 @@ class subpaving_tactic : public tactic {
m_ctx->reset_statistics();
}
void set_cancel(bool f) {
m_ctx->set_cancel(f);
}
subpaving::ineq * mk_ineq(expr * a) {
bool neg = false;
while (m().is_not(a, a))