mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
include more qsat features
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
c4472ce717
commit
76d637626a
|
@ -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);
|
||||
|
||||
|
|
|
@ -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();
|
||||
|
|
Loading…
Reference in a new issue