From: Andrew Reynolds Date: Thu, 5 Sep 2019 00:58:51 +0000 (-0500) Subject: Refactoring CEGQI interface (#3239) X-Git-Tag: cvc5-1.0.0~3977 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=44490619ebd55d59fea574a1759482f4c37ef42e;p=cvc5.git Refactoring CEGQI interface (#3239) --- diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index 3a498277a..b1a2a2533 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -32,8 +32,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -ArithInstantiator::ArithInstantiator(QuantifiersEngine* qe, TypeNode tn) - : Instantiator(qe, tn) +ArithInstantiator::ArithInstantiator(TypeNode tn) : Instantiator(tn) { d_zero = NodeManager::currentNM()->mkConst(Rational(0)); d_one = NodeManager::currentNM()->mkConst(Rational(1)); @@ -267,7 +266,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, << pvmod << " -> " << uval << ", styp = " << uires << std::endl; } // take into account delta - if (ci->useVtsDelta() && (uires == 2 || uires == -2)) + if (uires == 2 || uires == -2) { if (options::cbqiModel()) { @@ -329,9 +328,8 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, return false; } NodeManager* nm = NodeManager::currentNM(); - bool use_inf = ci->useVtsInfinity() - && (d_type.isInteger() ? options::cbqiUseInfInt() - : options::cbqiUseInfReal()); + bool use_inf = + d_type.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal(); bool upper_first = Random::getRandom().pickWithProb(0.5); if (options::cbqiMinBounds()) { @@ -505,7 +503,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, // if using cbqiMidpoint, only add the instance based on one bound if // the bound is non-strict if (!options::cbqiMidpoint() || d_type.isInteger() - || (ci->useVtsDelta() && d_mbp_vts_coeff[rr][1][best].isNull())) + || d_mbp_vts_coeff[rr][1][best].isNull()) { Node val = d_mbp_bounds[rr][best]; val = getModelBasedProjectionValue(ci, @@ -917,7 +915,7 @@ int ArithInstantiator::solve_arith(CegInstantiator* ci, ? d_zero : (real_part.size() == 1 ? real_part[0] : nm->mkNode(PLUS, real_part)); - Assert(ci->getOutput()->isEligibleForInstantiation(realPart)); + Assert(ci->isEligibleForInstantiation(realPart)); // re-isolate Trace("cegqi-arith-debug") << "Re-isolate..." << std::endl; veq_c = Node::null(); diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h index 8799ce1cd..ee3e3e27d 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h @@ -42,7 +42,7 @@ namespace quantifiers { class ArithInstantiator : public Instantiator { public: - ArithInstantiator(QuantifiersEngine* qe, TypeNode tn); + ArithInstantiator(TypeNode tn); virtual ~ArithInstantiator() {} /** reset */ void reset(CegInstantiator* ci, diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index 90b7002b3..eacc3032c 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -53,15 +53,14 @@ class CegInstantiatorBvInverterQuery : public BvInverterQuery CegInstantiator* d_ci; }; -BvInstantiator::BvInstantiator(QuantifiersEngine* qe, TypeNode tn) - : Instantiator(qe, tn), d_inst_id_counter(0) +BvInstantiator::BvInstantiator(TypeNode tn, BvInverter* inv) + : Instantiator(tn), d_inverter(inv), d_inst_id_counter(0) { - // get the global inverter utility - // this must be global since we need to: + // The inverter utility d_inverter is global to all BvInstantiator classes. + // This must be global since we need to: // * process Skolem functions properly across multiple variables within the // same quantifier // * cache Skolem variables uniformly across multiple quantified formulas - d_inverter = qe->getBvInverter(); } BvInstantiator::~BvInstantiator() {} diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h index 466eba6a2..a548c959e 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h @@ -38,7 +38,7 @@ namespace quantifiers { class BvInstantiator : public Instantiator { public: - BvInstantiator(QuantifiersEngine* qe, TypeNode tn); + BvInstantiator(TypeNode tn, BvInverter* inv); ~BvInstantiator() override; /** reset */ void reset(CegInstantiator* ci, diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h index cf9736abe..ef43d50a5 100644 --- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h @@ -32,7 +32,7 @@ namespace quantifiers { class DtInstantiator : public Instantiator { public: - DtInstantiator(QuantifiersEngine* qe, TypeNode tn) : Instantiator(qe, tn) {} + DtInstantiator(TypeNode tn) : Instantiator(tn) {} virtual ~DtInstantiator() {} /** reset */ void reset(CegInstantiator* ci, diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h index 05932de7e..b32fa5d4c 100644 --- a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h @@ -33,7 +33,7 @@ namespace quantifiers { class EprInstantiator : public Instantiator { public: - EprInstantiator(QuantifiersEngine* qe, TypeNode tn) : Instantiator(qe, tn) {} + EprInstantiator(TypeNode tn) : Instantiator(tn) {} virtual ~EprInstantiator() {} /** reset */ void reset(CegInstantiator* ci, diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index bc21cce81..e2a6432db 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -23,6 +23,7 @@ #include "options/quantifiers_options.h" #include "smt/term_formula_removal.h" #include "theory/arith/arith_msum.h" +#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quant_epr.h" #include "theory/quantifiers/quantifiers_attributes.h" @@ -136,14 +137,10 @@ void SolvedForm::pop_back(Node pv, Node n, TermProperties& pv_prop) d_theta.pop_back(); } -CegInstantiator::CegInstantiator(QuantifiersEngine* qe, - CegqiOutput* out, - bool use_vts_delta, - bool use_vts_inf) - : d_qe(qe), - d_out(out), - d_use_vts_delta(use_vts_delta), - d_use_vts_inf(use_vts_inf), +CegInstantiator::CegInstantiator(Node q, InstStrategyCegqi* parent) + : d_quant(q), + d_parent(parent), + d_qe(parent->getQuantifiersEngine()), d_is_nested_quant(false), d_effort(CEG_INST_EFFORT_NONE) { @@ -171,7 +168,9 @@ void CegInstantiator::computeProgVars( Node n ){ if (d_vars_set.find(n) != d_vars_set.end()) { d_prog_var[n].insert(n); - }else if( !d_out->isEligibleForInstantiation( n ) ){ + } + else if (!isEligibleForInstantiation(n)) + { d_inelig.insert(n); return; } @@ -431,19 +430,19 @@ void CegInstantiator::activateInstantiationVariable(Node v, unsigned index) TypeNode tn = v.getType(); Instantiator * vinst; if( tn.isReal() ){ - vinst = new ArithInstantiator( d_qe, tn ); + vinst = new ArithInstantiator(tn); }else if( tn.isSort() ){ Assert( options::quantEpr() ); - vinst = new EprInstantiator( d_qe, tn ); + vinst = new EprInstantiator(tn); }else if( tn.isDatatype() ){ - vinst = new DtInstantiator( d_qe, tn ); + vinst = new DtInstantiator(tn); }else if( tn.isBitVector() ){ - vinst = new BvInstantiator( d_qe, tn ); + vinst = new BvInstantiator(tn, d_parent->getBvInverter()); }else if( tn.isBoolean() ){ - vinst = new ModelValueInstantiator( d_qe, tn ); + vinst = new ModelValueInstantiator(tn); }else{ //default - vinst = new Instantiator( d_qe, tn ); + vinst = new Instantiator(tn); } d_instantiator[v] = vinst; } @@ -1056,13 +1055,41 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector } } Trace("cbqi-inst-debug") << "Do the instantiation...." << std::endl; - bool ret = d_out->doAddInstantiation( subs ); + bool ret = d_parent->doAddInstantiation(subs); for( unsigned i=0; iaddLemma( lemmas[i] ); + d_parent->addLemma(lemmas[i]); } return ret; } +bool CegInstantiator::isEligibleForInstantiation(Node n) const +{ + if (n.getKind() != INST_CONSTANT && n.getKind() != SKOLEM) + { + return true; + } + if (n.getAttribute(VirtualTermSkolemAttribute())) + { + // virtual terms are allowed + return true; + } + TypeNode tn = n.getType(); + if (tn.isSort()) + { + QuantEPR* qepr = d_qe->getQuantEPR(); + if (qepr != NULL) + { + // legal if in the finite set of constants of type tn + if (qepr->isEPRConstant(tn, n)) + { + return true; + } + } + } + // only legal if current quantified formula contains n + return expr::hasSubterm(d_quant, n); +} + bool CegInstantiator::canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic ){ Assert( d_prog_var.find( n )!=d_prog_var.end() ); if( !non_basic.empty() ){ @@ -1700,8 +1727,8 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st } } - -Instantiator::Instantiator( QuantifiersEngine * qe, TypeNode tn ) : d_type( tn ){ +Instantiator::Instantiator(TypeNode tn) : d_type(tn) +{ d_closed_enum_type = tn.isClosedEnumerable(); } diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index da57cdd16..8110dcd95 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -30,16 +30,9 @@ class QuantifiersEngine; namespace quantifiers { -class CegqiOutput { -public: - virtual ~CegqiOutput() {} - virtual bool doAddInstantiation( std::vector< Node >& subs ) = 0; - virtual bool isEligibleForInstantiation( Node n ) = 0; - virtual bool addLemma( Node lem ) = 0; -}; - class Instantiator; class InstantiatorPreprocess; +class InstStrategyCegqi; /** Term Properties * @@ -181,10 +174,11 @@ std::ostream& operator<<(std::ostream& os, CegHandledStatus status); */ class CegInstantiator { public: - CegInstantiator(QuantifiersEngine* qe, - CegqiOutput* out, - bool use_vts_delta = true, - bool use_vts_inf = true); + /** + * The instantiator will be constructing instantiations for quantified formula + * q, parent is the owner of this object. + */ + CegInstantiator(Node q, InstStrategyCegqi* parent); virtual ~CegInstantiator(); /** check * This adds instantiations based on the state of d_vars in current context @@ -214,8 +208,6 @@ class CegInstantiator { */ void registerCounterexampleLemma(std::vector& lems, std::vector& ce_vars); - /** get the output channel of this class */ - CegqiOutput* getOutput() { return d_out; } //------------------------------interface for instantiators /** get quantifiers engine */ QuantifiersEngine* getQuantifiersEngine() { return d_qe; } @@ -276,12 +268,14 @@ class CegInstantiator { bool isEligible(Node n); /** does n have variable pv? */ bool hasVariable(Node n, Node pv); - /** are we using delta for LRA virtual term substitution? */ - bool useVtsDelta() { return d_use_vts_delta; } - /** are we using infinity for LRA virtual term substitution? */ - bool useVtsInfinity() { return d_use_vts_inf; } /** are we processing a nested quantified formula? */ - bool hasNestedQuantification() { return d_is_nested_quant; } + bool hasNestedQuantification() const { return d_is_nested_quant; } + /** + * Are we allowed to instantiate the current quantified formula with n? This + * includes restrictions such as if n is a variable, it must occur free in + * the current quantified formula. + */ + bool isEligibleForInstantiation(Node n) const; //------------------------------------ static queries /** Is k a kind for which counterexample-guided instantiation is possible? * @@ -333,18 +327,12 @@ class CegInstantiator { static CegHandledStatus isCbqiQuant(Node q, QuantifiersEngine* qe = nullptr); //------------------------------------ end static queries private: + /** The quantified formula of this instantiator */ + Node d_quant; + /** The parent of this instantiator */ + InstStrategyCegqi* d_parent; /** quantified formula associated with this instantiator */ QuantifiersEngine* d_qe; - /** output channel of this instantiator */ - CegqiOutput* d_out; - /** whether we are using delta for virtual term substitution - * (for quantified LRA). - */ - bool d_use_vts_delta; - /** whether we are using infinity for virtual term substitution - * (for quantified LRA). - */ - bool d_use_vts_inf; //-------------------------------globally cached /** cache from nodes to the set of variables it contains @@ -613,19 +601,19 @@ class CegInstantiator { */ class Instantiator { public: - Instantiator( QuantifiersEngine * qe, TypeNode tn ); - virtual ~Instantiator(){} - /** reset - * This is called once, prior to any of the below methods are called. - * This function sets up any initial information necessary for constructing - * instantiations for pv based on the current context. - */ - virtual void reset(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) - { - } + Instantiator(TypeNode tn); + virtual ~Instantiator() {} + /** reset + * This is called once, prior to any of the below methods are called. + * This function sets up any initial information necessary for constructing + * instantiations for pv based on the current context. + */ + virtual void reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) + { + } /** has process equal term * @@ -819,15 +807,15 @@ public: class ModelValueInstantiator : public Instantiator { public: - ModelValueInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} - virtual ~ModelValueInstantiator(){} - bool useModelValue(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override - { - return true; - } + ModelValueInstantiator(TypeNode tn) : Instantiator(tn) {} + virtual ~ModelValueInstantiator() {} + bool useModelValue(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override + { + return true; + } std::string identify() const override { return "ModelValue"; } }; diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index ab5bbc25f..ac4d05194 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -30,26 +30,12 @@ #include "theory/theory_engine.h" using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; -bool CegqiOutputInstStrategy::doAddInstantiation(std::vector& subs) -{ - return d_out->doAddInstantiation(subs); -} - -bool CegqiOutputInstStrategy::isEligibleForInstantiation(Node n) -{ - return d_out->isEligibleForInstantiation(n); -} - -bool CegqiOutputInstStrategy::addLemma(Node lem) -{ - return d_out->addLemma(lem); -} +namespace CVC4 { +namespace theory { +namespace quantifiers { InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe) : QuantifiersModule(qe), @@ -57,15 +43,19 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe) d_incomplete_check(false), d_added_cbqi_lemma(qe->getUserContext()), d_elim_quants(qe->getSatContext()), - d_out(new CegqiOutputInstStrategy(this)), + d_bv_invert(nullptr), d_nested_qe_waitlist_size(qe->getUserContext()), d_nested_qe_waitlist_proc(qe->getUserContext()) -//, d_added_inst( qe->getUserContext() ) { d_qid_count = 0; d_small_const = NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000)); d_check_vts_lemma_lc = false; + if (options::cbqiBv()) + { + // if doing instantiation for BV, need the inverter class + d_bv_invert.reset(new quantifiers::BvInverter); + } } InstStrategyCegqi::~InstStrategyCegqi() {} @@ -665,41 +655,22 @@ bool InstStrategyCegqi::addLemma( Node lem ) { return d_quantEngine->addLemma( lem ); } -bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) { - if( n.getKind()==INST_CONSTANT || n.getKind()==SKOLEM ){ - if( n.getAttribute(VirtualTermSkolemAttribute()) ){ - // virtual terms are allowed - return true; - }else{ - TypeNode tn = n.getType(); - if( tn.isSort() ){ - QuantEPR * qepr = d_quantEngine->getQuantEPR(); - if( qepr!=NULL ){ - //legal if in the finite set of constants of type tn - if( qepr->isEPRConstant( tn, n ) ){ - return true; - } - } - } - //only legal if current quantified formula contains n - return expr::hasSubterm(d_curr_quant, n); - } - }else{ - return true; - } -} CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) { std::map>::iterator it = d_cinst.find(q); if( it==d_cinst.end() ){ - d_cinst[q].reset( - new CegInstantiator(d_quantEngine, d_out.get(), true, true)); + d_cinst[q].reset(new CegInstantiator(q, this)); return d_cinst[q].get(); } return it->second.get(); } +BvInverter* InstStrategyCegqi::getBvInverter() const +{ + return d_bv_invert.get(); +} + void InstStrategyCegqi::presolve() { if (!options::cbqiPreRegInst()) { @@ -712,3 +683,6 @@ void InstStrategyCegqi::presolve() { } } +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index ecae4ab64..32f41e476 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -19,6 +19,7 @@ #define CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H #include "theory/decision_manager.h" +#include "theory/quantifiers/bv_inverter.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" #include "theory/quantifiers/quant_util.h" #include "util/statistics_registry.h" @@ -27,26 +28,6 @@ namespace CVC4 { namespace theory { namespace quantifiers { -class InstStrategyCegqi; - -/** - * An output channel class, used by instantiator objects below. The methods - * of this class call the corresponding functions of InstStrategyCegqi below. - */ -class CegqiOutputInstStrategy : public CegqiOutput -{ - public: - CegqiOutputInstStrategy(InstStrategyCegqi* out) : d_out(out) {} - /** The module whose functions we call. */ - InstStrategyCegqi* d_out; - /** add instantiation */ - bool doAddInstantiation(std::vector& subs) override; - /** is eligible for instantiation */ - bool isEligibleForInstantiation(Node n) override; - /** add lemma */ - bool addLemma(Node lem) override; -}; - /** * Counterexample-guided quantifier instantiation module. * @@ -82,6 +63,8 @@ class InstStrategyCegqi : public QuantifiersModule std::string identify() const override { return std::string("Cegqi"); } /** get instantiator for quantifier */ CegInstantiator* getInstantiator(Node q); + /** get the BV inverter utility */ + BvInverter* getBvInverter() const; /** pre-register quantifier */ void preRegisterQuantifier(Node q) override; // presolve @@ -92,12 +75,6 @@ class InstStrategyCegqi : public QuantifiersModule //------------------- interface for CegqiOutputInstStrategy /** Instantiate the current quantified formula forall x. Q with x -> subs. */ bool doAddInstantiation(std::vector& subs); - /** - * Are we allowed to instantiate the current quantified formula with n? This - * includes restrictions such as if n is a variable, it must occur free in - * the current quantified formula. - */ - bool isEligibleForInstantiation(Node n); /** Add lemma lem via the output channel of this class. */ bool addLemma(Node lem); //------------------- end interface for CegqiOutputInstStrategy @@ -126,16 +103,13 @@ class InstStrategyCegqi : public QuantifiersModule std::map< Node, bool > d_active_quant; /** Whether cegqi handles each quantified formula. */ std::map d_do_cbqi; - /** - * An output channel used by instantiators for communicating with this - * class. - */ - std::unique_ptr d_out; /** * The instantiator for each quantified formula q registered to this class. * This object is responsible for finding instantiatons for q. */ std::map> d_cinst; + /** inversion utility for BV instantiation */ + std::unique_ptr d_bv_invert; /** * The decision strategy for each quantified formula q registered to this * class. diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 5bac55462..f57667be5 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -190,7 +190,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_tr_trie(new inst::TriggerTrie), d_model(nullptr), d_rel_dom(nullptr), - d_bv_invert(nullptr), d_builder(nullptr), d_qepr(nullptr), d_term_util(new quantifiers::TermUtil(this)), @@ -256,12 +255,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, Assert( !options::incrementalSolving() ); d_qepr.reset(new quantifiers::QuantEPR); } - - if (options::cbqi() && options::cbqiBv()) - { - // if doing instantiation for BV, need the inverter class - d_bv_invert.reset(new quantifiers::BvInverter); - } //---- end utilities //allow theory combination to go first, once initially @@ -341,10 +334,6 @@ quantifiers::RelevantDomain* QuantifiersEngine::getRelevantDomain() const { return d_rel_dom.get(); } -quantifiers::BvInverter* QuantifiersEngine::getBvInverter() const -{ - return d_bv_invert.get(); -} quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const { return d_builder.get(); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index dfe8a44ad..1f8c13f7b 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -24,7 +24,6 @@ #include "context/cdlist.h" #include "expr/attribute.h" #include "expr/term_canonize.h" -#include "theory/quantifiers/bv_inverter.h" #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/equality_infer.h" @@ -114,8 +113,6 @@ public: quantifiers::EqualityInference* getEqualityInference() const; /** get relevant domain */ quantifiers::RelevantDomain* getRelevantDomain() const; - /** get the BV inverter utility */ - quantifiers::BvInverter* getBvInverter() const; //---------------------- end utilities //---------------------- modules (TODO remove these #1163) /** get bounded integers utility */ @@ -309,8 +306,6 @@ public: std::unique_ptr d_model; /** relevant domain */ std::unique_ptr d_rel_dom; - /** inversion utility for BV instantiation */ - std::unique_ptr d_bv_invert; /** model builder */ std::unique_ptr d_builder; /** utility for effectively propositional logic */