diff options
34 files changed, 148 insertions, 90 deletions
diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp index e9c646f07..681c168f2 100644 --- a/src/theory/quantifiers/anti_skolem.cpp +++ b/src/theory/quantifiers/anti_skolem.cpp @@ -92,8 +92,10 @@ QuantAntiSkolem::QuantAntiSkolem(QuantifiersEngine* qe) QuantAntiSkolem::~QuantAntiSkolem() { delete d_sqc; } /* Call during quantifier engine's check */ -void QuantAntiSkolem::check( Theory::Effort e, unsigned quant_e ) { - if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ +void QuantAntiSkolem::check(Theory::Effort e, QEffort quant_e) +{ + if (quant_e == QEFFORT_STANDARD) + { d_sqtc.clear(); for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h index 078675420..bad98c04b 100644 --- a/src/theory/quantifiers/anti_skolem.h +++ b/src/theory/quantifiers/anti_skolem.h @@ -40,7 +40,7 @@ public: bool pconnected = true ); /* Call during quantifier engine's check */ - void check( Theory::Effort e, unsigned quant_e ); + void check(Theory::Effort e, QEffort quant_e); /* Called for new quantifiers */ void registerQuantifier( Node q ) {} void assertNode( Node n ) {} diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 972b404de..f99d0b080 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -350,8 +350,10 @@ bool BoundedIntegers::needsCheck( Theory::Effort e ) { return e==Theory::EFFORT_LAST_CALL; } -void BoundedIntegers::check( Theory::Effort e, unsigned quant_e ) { - if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ +void BoundedIntegers::check(Theory::Effort e, QEffort quant_e) +{ + if (quant_e == QEFFORT_STANDARD) + { Trace("bint-engine") << "---Bounded Integers---" << std::endl; bool addedLemma = false; //make sure proxies are up-to-date with range diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h index f0a3a85f5..a91b04ab3 100644 --- a/src/theory/quantifiers/bounded_integers.h +++ b/src/theory/quantifiers/bounded_integers.h @@ -146,7 +146,7 @@ public: void presolve(); bool needsCheck( Theory::Effort e ); - void check( Theory::Effort e, unsigned quant_e ); + void check(Theory::Effort e, QEffort quant_e); void registerQuantifier( Node q ); void preRegisterQuantifier( Node q ); void assertNode( Node n ); diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 12c3c8464..b54ce4805 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -44,12 +44,15 @@ bool CegInstantiation::needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; } -unsigned CegInstantiation::needsModel( Theory::Effort e ) { - return d_conj->isSingleInvocation() ? QuantifiersEngine::QEFFORT_STANDARD : QuantifiersEngine::QEFFORT_MODEL; +QuantifiersModule::QEffort CegInstantiation::needsModel(Theory::Effort e) +{ + return d_conj->isSingleInvocation() ? QEFFORT_STANDARD : QEFFORT_MODEL; } -void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) { - unsigned echeck = d_conj->isSingleInvocation() ? QuantifiersEngine::QEFFORT_STANDARD : QuantifiersEngine::QEFFORT_MODEL; +void CegInstantiation::check(Theory::Effort e, QEffort quant_e) +{ + unsigned echeck = + d_conj->isSingleInvocation() ? QEFFORT_STANDARD : QEFFORT_MODEL; if( quant_e==echeck ){ Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl; Trace("cegqi-engine-debug") << std::endl; diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 5e6cb3864..86f0c4c9f 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -44,9 +44,9 @@ public: ~CegInstantiation(); public: bool needsCheck( Theory::Effort e ); - unsigned needsModel( Theory::Effort e ); + QEffort needsModel(Theory::Effort e); /* Call during quantifier engine's check */ - void check( Theory::Effort e, unsigned quant_e ); + void check(Theory::Effort e, QEffort quant_e); /* Called for new quantifiers */ void registerQuantifier( Node q ); /** get the next decision request */ diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index e5a096c87..b7d1fe404 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -334,9 +334,10 @@ bool ConjectureGenerator::hasEnumeratedUf( Node n ) { void ConjectureGenerator::reset_round( Theory::Effort e ) { } - -void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { - if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ +void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) +{ + if (quant_e == QEFFORT_STANDARD) + { d_fullEffortCount++; if( d_fullEffortCount%optFullCheckFrequency()==0 ){ d_hasAddedLemma = false; diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index e4246e2ab..a67530556 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -407,7 +407,7 @@ public: /* reset at a round */ void reset_round( Theory::Effort e ); /* Call during quantifier engine's check */ - void check( Theory::Effort e, unsigned quant_e ); + void check(Theory::Effort e, QEffort quant_e); /* Called for new quantifiers */ void registerQuantifier( Node q ); void assertNode( Node n ); diff --git a/src/theory/quantifiers/fun_def_engine.cpp b/src/theory/quantifiers/fun_def_engine.cpp index 354d90b8b..650a68aa0 100644 --- a/src/theory/quantifiers/fun_def_engine.cpp +++ b/src/theory/quantifiers/fun_def_engine.cpp @@ -39,7 +39,8 @@ void FunDefEngine::reset_round( Theory::Effort e ){ } /* Call during quantifier engine's check */ -void FunDefEngine::check( Theory::Effort e, unsigned quant_e ) { +void FunDefEngine::check(Theory::Effort e, QEffort quant_e) +{ //TODO } diff --git a/src/theory/quantifiers/fun_def_engine.h b/src/theory/quantifiers/fun_def_engine.h index ea1dbbc59..48de4f36c 100644 --- a/src/theory/quantifiers/fun_def_engine.h +++ b/src/theory/quantifiers/fun_def_engine.h @@ -42,7 +42,7 @@ public: /* reset at a round */ void reset_round( Theory::Effort e ); /* Call during quantifier engine's check */ - void check( Theory::Effort e, unsigned quant_e ); + void check(Theory::Effort e, QEffort quant_e); /* Called for new quantifiers */ void registerQuantifier( Node q ); /** called for everything that gets asserted */ diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp index 0ae7adfec..3c351cad5 100644 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp @@ -623,7 +623,12 @@ bool InstPropagator::reset( Theory::Effort e ) { return d_qy.reset( e ); } -bool InstPropagator::notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) { +bool InstPropagator::notifyInstantiation(QuantifiersModule::QEffort quant_e, + Node q, + Node lem, + std::vector<Node>& terms, + Node body) +{ if( !d_conflict ){ if( Trace.isOn("qip-prop") ){ Trace("qip-prop") << "InstPropagator:: Notify instantiation " << q << " : " << std::endl; diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h index 580923fc9..b8ea2c49e 100644 --- a/src/theory/quantifiers/inst_propagator.h +++ b/src/theory/quantifiers/inst_propagator.h @@ -113,14 +113,23 @@ private: InstPropagator& d_ip; public: InstantiationNotifyInstPropagator(InstPropagator& ip): d_ip(ip) {} - virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) { + virtual bool notifyInstantiation(QuantifiersModule::QEffort quant_e, + Node q, + Node lem, + std::vector<Node>& terms, + Node body) + { return d_ip.notifyInstantiation( quant_e, q, lem, terms, body ); } virtual void filterInstantiations() { d_ip.filterInstantiations(); } }; InstantiationNotifyInstPropagator d_notify; /** notify instantiation method */ - bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ); + bool notifyInstantiation(QuantifiersModule::QEffort quant_e, + Node q, + Node lem, + std::vector<Node>& terms, + Node body); /** remove instance ids */ void filterInstantiations(); /** allocate instantiation */ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 8b5332c9d..24a9f1bdf 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -53,14 +53,15 @@ bool InstStrategyCbqi::needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; } -unsigned InstStrategyCbqi::needsModel( Theory::Effort e ) { +QuantifiersModule::QEffort InstStrategyCbqi::needsModel(Theory::Effort e) +{ for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ - return QuantifiersEngine::QEFFORT_STANDARD; + return QEFFORT_STANDARD; } } - return QuantifiersEngine::QEFFORT_NONE; + return QEFFORT_NONE; } bool InstStrategyCbqi::registerCbqiLemma( Node q ) { @@ -239,8 +240,10 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { processResetInstantiationRound( effort ); } -void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) { - if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ +void InstStrategyCbqi::check(Theory::Effort e, QEffort quant_e) +{ + if (quant_e == QEFFORT_STANDARD) + { Assert( !d_quantEngine->inConflict() ); double clSet = 0; if( Trace.isOn("cbqi-engine") ){ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index a1e6a2bdc..0b23de10d 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -100,9 +100,9 @@ public: bool doCbqi( Node q ); /** process functions */ bool needsCheck( Theory::Effort e ); - unsigned needsModel( Theory::Effort e ); + QEffort needsModel(Theory::Effort e); void reset_round( Theory::Effort e ); - void check( Theory::Effort e, unsigned quant_e ); + void check(Theory::Effort e, QEffort quant_e); bool checkComplete(); bool checkCompleteFor( Node q ); void preRegisterQuantifier( Node q ); diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index 3bd1ac495..edd15fa2c 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -55,19 +55,18 @@ bool InstStrategyEnum::needsCheck(Theory::Effort e) } void InstStrategyEnum::reset_round(Theory::Effort e) {} -void InstStrategyEnum::check(Theory::Effort e, unsigned quant_e) +void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) { bool doCheck = false; bool fullEffort = false; if (options::fullSaturateInterleave()) { // we only add when interleaved with other strategies - doCheck = quant_e == QuantifiersEngine::QEFFORT_STANDARD - && d_quantEngine->hasAddedLemma(); + doCheck = quant_e == QEFFORT_STANDARD && d_quantEngine->hasAddedLemma(); } if (options::fullSaturateQuant() && !doCheck) { - doCheck = quant_e == QuantifiersEngine::QEFFORT_LAST_CALL; + doCheck = quant_e == QEFFORT_LAST_CALL; fullEffort = !d_quantEngine->hasAddedLemma(); } if (doCheck) diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index d79917eda..cf97518fc 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -71,7 +71,7 @@ class InstStrategyEnum : public QuantifiersModule * Adds instantiations for all currently asserted * quantified formulas via calls to process(...) */ - void check(Theory::Effort e, unsigned quant_e) override; + void check(Theory::Effort e, QEffort quant_e) override; /** Register quantifier. */ void registerQuantifier(Node q) override; /** Identify. */ diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 22af9dd00..0c847b597 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -111,9 +111,11 @@ void InstantiationEngine::reset_round( Theory::Effort e ){ } } -void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ +void InstantiationEngine::check(Theory::Effort e, QEffort quant_e) +{ CodeTimer codeTimer(d_quantEngine->d_statistics.d_ematching_time); - if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ + if (quant_e == QEFFORT_STANDARD) + { double clSet = 0; if( Trace.isOn("inst-engine") ){ clSet = double(clock())/double(CLOCKS_PER_SEC); diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 140ea9250..18b5ea19c 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -79,7 +79,7 @@ class InstantiationEngine : public QuantifiersModule { void presolve(); bool needsCheck(Theory::Effort e); void reset_round(Theory::Effort e); - void check(Theory::Effort e, unsigned quant_e); + void check(Theory::Effort e, QEffort quant_e); bool checkCompleteFor(Node q); void preRegisterQuantifier(Node q); void registerQuantifier(Node q); diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp index e26c464e2..375754b26 100644 --- a/src/theory/quantifiers/local_theory_ext.cpp +++ b/src/theory/quantifiers/local_theory_ext.cpp @@ -128,9 +128,11 @@ bool LtePartialInst::needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_FULL && d_needsCheck; } /* Call during quantifier engine's check */ -void LtePartialInst::check( Theory::Effort e, unsigned quant_e ) { +void LtePartialInst::check(Theory::Effort e, QEffort quant_e) +{ //flush lemmas ASAP (they are a reduction) - if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT && d_needsCheck ){ + if (quant_e == QEFFORT_CONFLICT && d_needsCheck) + { std::vector< Node > lemmas; getInstantiations( lemmas ); //add lemmas to quantifiers engine diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h index 68b6a562a..3b19b8d55 100644 --- a/src/theory/quantifiers/local_theory_ext.h +++ b/src/theory/quantifiers/local_theory_ext.h @@ -63,7 +63,7 @@ public: /* whether this module needs to check this round */ bool needsCheck( Theory::Effort e ); /* Call during quantifier engine's check */ - void check( Theory::Effort e, unsigned quant_e ); + void check(Theory::Effort e, QEffort quant_e); /* Called for new quantifiers */ void registerQuantifier( Node q ) {} /* check complete */ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index c4a0b5c5d..5d01e04e6 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -53,25 +53,26 @@ bool ModelEngine::needsCheck( Theory::Effort e ) { return e==Theory::EFFORT_LAST_CALL; } -unsigned ModelEngine::needsModel( Theory::Effort e ) { +QuantifiersModule::QEffort ModelEngine::needsModel(Theory::Effort e) +{ if( options::mbqiInterleave() ){ - return QuantifiersEngine::QEFFORT_STANDARD; + return QEFFORT_STANDARD; }else{ - return QuantifiersEngine::QEFFORT_MODEL; + return QEFFORT_MODEL; } } void ModelEngine::reset_round( Theory::Effort e ) { d_incomplete_check = true; } - -void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ +void ModelEngine::check(Theory::Effort e, QEffort quant_e) +{ bool doCheck = false; if( options::mbqiInterleave() ){ - doCheck = quant_e==QuantifiersEngine::QEFFORT_STANDARD && d_quantEngine->hasAddedLemma(); + doCheck = quant_e == QEFFORT_STANDARD && d_quantEngine->hasAddedLemma(); } if( !doCheck ){ - doCheck = quant_e==QuantifiersEngine::QEFFORT_MODEL; + doCheck = quant_e == QEFFORT_MODEL; } if( doCheck ){ Assert( !d_quantEngine->inConflict() ); diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index ad77ae8dc..840ff4242 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -50,9 +50,9 @@ public: virtual ~ModelEngine(); public: bool needsCheck( Theory::Effort e ); - unsigned needsModel( Theory::Effort e ); + QEffort needsModel(Theory::Effort e); void reset_round( Theory::Effort e ); - void check( Theory::Effort e, unsigned quant_e ); + void check(Theory::Effort e, QEffort quant_e); bool checkComplete(); bool checkCompleteFor( Node q ); void registerQuantifier( Node f ); diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index bd56b9d9b..baf499d67 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -2031,9 +2031,11 @@ void QuantConflictFind::setIrrelevantFunction( TNode f ) { } /** check */ -void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { +void QuantConflictFind::check(Theory::Effort level, QEffort quant_e) +{ CodeTimer codeTimer(d_quantEngine->d_statistics.d_qcf_time); - if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){ + if (quant_e == QEFFORT_CONFLICT) + { Trace("qcf-check") << "QCF : check : " << level << std::endl; if( d_conflict ){ Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl; diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 794787bfc..0e5fe3c18 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -243,8 +243,9 @@ public: /** reset round */ void reset_round( Theory::Effort level ); /** check */ - void check( Theory::Effort level, unsigned quant_e ); -private: + void check(Theory::Effort level, QEffort quant_e); + + private: bool d_needs_computeRelEqr; public: void computeRelevantEqr(); diff --git a/src/theory/quantifiers/quant_equality_engine.cpp b/src/theory/quantifiers/quant_equality_engine.cpp index dab95f83b..859c4f3ea 100644 --- a/src/theory/quantifiers/quant_equality_engine.cpp +++ b/src/theory/quantifiers/quant_equality_engine.cpp @@ -74,7 +74,8 @@ void QuantEqualityEngine::reset_round( Theory::Effort e ){ } /* Call during quantifier engine's check */ -void QuantEqualityEngine::check( Theory::Effort e, unsigned quant_e ) { +void QuantEqualityEngine::check(Theory::Effort e, QEffort quant_e) +{ //TODO } diff --git a/src/theory/quantifiers/quant_equality_engine.h b/src/theory/quantifiers/quant_equality_engine.h index f827b4fd7..d2e9ec77b 100644 --- a/src/theory/quantifiers/quant_equality_engine.h +++ b/src/theory/quantifiers/quant_equality_engine.h @@ -80,7 +80,7 @@ public: /* reset at a round */ void reset_round( Theory::Effort e ); /* Call during quantifier engine's check */ - void check( Theory::Effort e, unsigned quant_e ); + void check(Theory::Effort e, QEffort quant_e); /* Called for new quantifiers */ void registerQuantifier( Node q ); /** called for everything that gets asserted */ diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 282ff3bc4..68a0f30dc 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -83,9 +83,11 @@ bool QuantDSplit::checkCompleteFor( Node q ) { } /* Call during quantifier engine's check */ -void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) { +void QuantDSplit::check(Theory::Effort e, QEffort quant_e) +{ //add lemmas ASAP (they are a reduction) - if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){ + if (quant_e == QEFFORT_CONFLICT) + { std::vector< Node > lemmas; for(std::map< Node, int >::iterator it = d_quant_to_reduce.begin(); it != d_quant_to_reduce.end(); ++it) { Node q = it->first; diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index daf4114bc..644583f04 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -39,7 +39,7 @@ public: /* whether this module needs to check this round */ bool needsCheck( Theory::Effort e ); /* Call during quantifier engine's check */ - void check( Theory::Effort e, unsigned quant_e ); + void check(Theory::Effort e, QEffort quant_e); /* Called for new quantifiers */ void registerQuantifier( Node q ) {} void assertNode( Node n ) {} diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index b8e29280d..571c3846a 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -25,8 +25,9 @@ using namespace CVC4::context; namespace CVC4 { namespace theory { -unsigned QuantifiersModule::needsModel( Theory::Effort e ) { - return QuantifiersEngine::QEFFORT_NONE; +QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e) +{ + return QEFFORT_NONE; } eq::EqualityEngine * QuantifiersModule::getEqualityEngine() { diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 95cd7e5e4..f958605b1 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -40,7 +40,23 @@ namespace quantifiers { * It has a similar interface to a Theory object. */ class QuantifiersModule { -public: + public: + /** effort levels for quantifiers modules check */ + enum QEffort + { + // conflict effort, for conflict-based instantiation + QEFFORT_CONFLICT, + // standard effort, for heuristic instantiation + QEFFORT_STANDARD, + // model effort, for model-based instantiation + QEFFORT_MODEL, + // last call effort, for last resort techniques + QEFFORT_LAST_CALL, + // none + QEFFORT_NONE, + }; + + public: QuantifiersModule( QuantifiersEngine* qe ) : d_quantEngine( qe ){} virtual ~QuantifiersModule(){} /** Presolve. @@ -62,7 +78,7 @@ public: * which specifies the quantifiers effort in which it requires the model to * be built. */ - virtual unsigned needsModel( Theory::Effort e ); + virtual QEffort needsModel(Theory::Effort e); /** Reset. * * Called at the beginning of QuantifiersEngine::check(e). @@ -73,7 +89,7 @@ public: * Called during QuantifiersEngine::check(e) depending * if needsCheck(e) returns true. */ - virtual void check( Theory::Effort e, unsigned quant_e ) = 0; + virtual void check(Theory::Effort e, QEffort quant_e) = 0; /** Check complete? * * Returns false if the module's reasoning was globally incomplete diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index b28dca1ed..2c85bceb8 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -69,8 +69,10 @@ bool RewriteEngine::needsCheck( Theory::Effort e ){ //return e>=Theory::EFFORT_LAST_CALL; } -void RewriteEngine::check( Theory::Effort e, unsigned quant_e ) { - if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ +void RewriteEngine::check(Theory::Effort e, QEffort quant_e) +{ + if (quant_e == QEFFORT_STANDARD) + { Assert( !d_quantEngine->inConflict() ); Trace("rewrite-engine") << "---Rewrite Engine Round, effort = " << e << "---" << std::endl; //if( e==Theory::EFFORT_LAST_CALL ){ diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index 34994f993..5d1918205 100644 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -53,7 +53,7 @@ public: ~RewriteEngine() throw() {} bool needsCheck( Theory::Effort e ); - void check( Theory::Effort e, unsigned quant_e ); + void check(Theory::Effort e, QEffort quant_e); void registerQuantifier( Node f ); void assertNode( Node n ); bool checkCompleteFor( Node q ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index f6b920cda..bc2b533be 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -120,7 +120,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, } d_tr_trie = new inst::TriggerTrie; - d_curr_effort_level = QEFFORT_NONE; + d_curr_effort_level = QuantifiersModule::QEFFORT_NONE; d_conflict = false; d_hasAddedLemma = false; d_useModelEe = false; @@ -444,7 +444,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ return; } bool needsCheck = !d_lemmas_waiting.empty(); - unsigned needsModelE = QEFFORT_NONE; + QuantifiersModule::QEffort needsModelE = QuantifiersModule::QEFFORT_NONE; std::vector< QuantifiersModule* > qm; if( d_model->checkNeeded() ){ needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call @@ -454,7 +454,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ needsCheck = true; //can only request model at last call since theory combination can find inconsistencies if( e>=Theory::EFFORT_LAST_CALL ){ - unsigned me = d_modules[i]->needsModel( e ); + QuantifiersModule::QEffort me = d_modules[i]->needsModel(e); needsModelE = me<needsModelE ? me : needsModelE; } } @@ -559,7 +559,12 @@ void QuantifiersEngine::check( Theory::Effort e ){ ++(d_statistics.d_instantiation_rounds); } Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl; - for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_LAST_CALL; quant_e++ ){ + for (unsigned qef = QuantifiersModule::QEFFORT_CONFLICT; + qef <= QuantifiersModule::QEFFORT_LAST_CALL; + ++qef) + { + QuantifiersModule::QEffort quant_e = + static_cast<QuantifiersModule::QEffort>(qef); d_curr_effort_level = quant_e; //build the model if any module requested it if( needsModelE==quant_e && !d_model->isBuilt() ){ @@ -590,7 +595,8 @@ void QuantifiersEngine::check( Theory::Effort e ){ break; }else{ Assert( !d_conflict ); - if( quant_e==QEFFORT_CONFLICT ){ + if (quant_e == QuantifiersModule::QEFFORT_CONFLICT) + { if( e==Theory::EFFORT_FULL ){ //increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase if( d_ierCounterLastLc!=d_ierCounter_lc || !options::instWhenStrictInterleave() || d_ierCounter%d_inst_when_phase!=0 ){ @@ -601,7 +607,9 @@ void QuantifiersEngine::check( Theory::Effort e ){ }else if( e==Theory::EFFORT_LAST_CALL ){ d_ierCounter_lc = d_ierCounter_lc + 1; } - }else if( quant_e==QEFFORT_MODEL ){ + } + else if (quant_e == QuantifiersModule::QEFFORT_MODEL) + { if( e==Theory::EFFORT_LAST_CALL ){ //sources of incompleteness if( !d_recorded_inst.empty() ){ @@ -655,7 +663,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } } - d_curr_effort_level = QEFFORT_NONE; + d_curr_effort_level = QuantifiersModule::QEFFORT_NONE; Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl; if( d_hasAddedLemma ){ //debug information @@ -1293,7 +1301,9 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo setInstantiationLevelAttr( orig_body, q[1], maxInstLevel+1 ); } } - if( d_curr_effort_level>QEFFORT_CONFLICT && d_curr_effort_level<QEFFORT_NONE ){ + if (d_curr_effort_level > QuantifiersModule::QEFFORT_CONFLICT + && d_curr_effort_level < QuantifiersModule::QEFFORT_NONE) + { //notify listeners for( unsigned j=0; j<d_inst_notify.size(); j++ ){ if( !d_inst_notify[j]->notifyInstantiation( d_curr_effort_level, q, lem, terms, body ) ){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index ffede2a5b..37691488e 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -44,7 +44,11 @@ class InstantiationNotify { public: InstantiationNotify(){} virtual ~InstantiationNotify() {} - virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) = 0; + virtual bool notifyInstantiation(QuantifiersModule::QEffort quant_e, + Node q, + Node lem, + std::vector<Node>& terms, + Node body) = 0; virtual void filterInstantiations() = 0; }; @@ -141,8 +145,6 @@ private: std::unique_ptr<quantifiers::Skolemize> d_skolemize; /** term enumeration utility */ std::unique_ptr<quantifiers::TermEnumeration> d_term_enum; - - private: /** instantiation engine */ quantifiers::InstantiationEngine* d_inst_engine; /** model engine */ @@ -174,26 +176,17 @@ private: /** quantifiers instantiation propagtor */ quantifiers::InstPropagator * d_inst_prop; - public: // effort levels (TODO : make an enum and use everywhere #1293) - enum { - QEFFORT_CONFLICT, - QEFFORT_STANDARD, - QEFFORT_MODEL, - QEFFORT_LAST_CALL, - //none - QEFFORT_NONE, - }; -private: //this information is reset during check - /** current effort level */ - unsigned d_curr_effort_level; + private: //this information is reset during check + /** current effort level */ + QuantifiersModule::QEffort d_curr_effort_level; /** are we in conflict */ bool d_conflict; - context::CDO< bool > d_conflict_c; + context::CDO<bool> d_conflict_c; /** has added lemma this round */ bool d_hasAddedLemma; /** whether to use model equality engine */ bool d_useModelEe; -private: + private: /** list of all quantifiers seen */ std::map< Node, bool > d_quants; /** quantifiers reduced */ |