From 76d637626a484e41269f45ad6442142d043a1804 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 19 Mar 2016 12:30:24 -0700 Subject: [PATCH] include more qsat features Signed-off-by: Nikolaj Bjorner --- src/smt/asserted_formulas.cpp | 6 ------ src/smt/asserted_formulas.h | 2 -- 2 files changed, 8 deletions(-) diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index df4b528fd..749e6037c 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -797,13 +797,7 @@ MK_SIMPLIFIER(apply_bit2int, bit2int& functor = m_bit2int, "bit2int", "propagate MK_SIMPLIFIER(cheap_quant_fourier_motzkin, elim_bounds_star functor(m_manager), "elim_bounds", "cheap-fourier-motzkin", true); -// MK_SIMPLIFIER(quant_elim, qe::expr_quant_elim_star1 &functor = m_quant_elim, -// "quantifiers", "quantifier elimination procedures", true); -bool asserted_formulas::quant_elim() { - throw default_exception("QUANT_ELIM option is deprecated, please consider using the 'qe' tactic."); - return false; -} MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m_manager), "bv_elim", "eliminate-bit-vectors-from-quantifiers", true); diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h index f4658f101..75fb86703 100644 --- a/src/smt/asserted_formulas.h +++ b/src/smt/asserted_formulas.h @@ -55,7 +55,6 @@ class asserted_formulas { maximise_bv_sharing m_bv_sharing; bool m_inconsistent; - // qe::expr_quant_elim_star1 m_quant_elim; struct scope { unsigned m_asserted_formulas_lim; @@ -84,7 +83,6 @@ class asserted_formulas { void eliminate_and(); void refine_inj_axiom(); bool cheap_quant_fourier_motzkin(); - bool quant_elim(); void apply_distribute_forall(); bool apply_bit2int(); void lift_ite();