From 0ff53d70b3e0a11e4ae5c1c8f612d809dca2d004 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 13 Feb 2021 08:42:36 -0600 Subject: [PATCH] Moving methods from quantifiers engine to quantifiers state (#5881) Towards eliminating dependencies on quantifiers engine. --- src/CMakeLists.txt | 1 + .../quantifiers/conjecture_generator.cpp | 2 +- .../quantifiers/ematching/inst_strategy.cpp | 45 ++++++ .../quantifiers/ematching/inst_strategy.h | 19 +-- .../ematching/inst_strategy_e_matching.cpp | 2 +- .../inst_strategy_e_matching_user.cpp | 4 +- .../ematching/inst_strategy_e_matching_user.h | 1 + .../ematching/instantiation_engine.cpp | 2 +- .../quantifiers/inst_strategy_enumerative.cpp | 3 +- src/theory/quantifiers/quantifiers_state.cpp | 129 +++++++++++++++++- src/theory/quantifiers/quantifiers_state.h | 39 ++++++ src/theory/quantifiers_engine.cpp | 117 ++-------------- src/theory/quantifiers_engine.h | 14 -- 13 files changed, 240 insertions(+), 138 deletions(-) create mode 100644 src/theory/quantifiers/ematching/inst_strategy.cpp diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 42370b8fc..12e3f24b3 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -664,6 +664,7 @@ libcvc4_add_sources( theory/quantifiers/ematching/inst_match_generator_multi_linear.h theory/quantifiers/ematching/inst_match_generator_simple.cpp theory/quantifiers/ematching/inst_match_generator_simple.h + theory/quantifiers/ematching/inst_strategy.cpp theory/quantifiers/ematching/inst_strategy.h theory/quantifiers/ematching/inst_strategy_e_matching.cpp theory/quantifiers/ematching/inst_strategy_e_matching.h diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 02b9ca635..57c5533a9 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -336,7 +336,7 @@ bool ConjectureGenerator::isGroundTerm( TNode n ) { bool ConjectureGenerator::needsCheck( Theory::Effort e ) { // synchonized with instantiation engine - return d_quantEngine->getInstWhenNeedsCheck( e ); + return d_qstate.getInstWhenNeedsCheck(e); } bool ConjectureGenerator::hasEnumeratedUf( Node n ) { diff --git a/src/theory/quantifiers/ematching/inst_strategy.cpp b/src/theory/quantifiers/ematching/inst_strategy.cpp new file mode 100644 index 000000000..fc85703c0 --- /dev/null +++ b/src/theory/quantifiers/ematching/inst_strategy.cpp @@ -0,0 +1,45 @@ +/********************* */ +/*! \file inst_strategy.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Instantiation engine strategy base class + **/ + +#include "theory/quantifiers/ematching/inst_strategy.h" + +#include "theory/quantifiers/quantifiers_state.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +InstStrategy::InstStrategy(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim) + : d_quantEngine(qe), d_qstate(qs), d_qim(qim) +{ +} +InstStrategy::~InstStrategy() {} +void InstStrategy::presolve() {} +std::string InstStrategy::identify() const { return std::string("Unknown"); } + +options::UserPatMode InstStrategy::getInstUserPatMode() const +{ + if (options::userPatternsQuant() == options::UserPatMode::INTERLEAVE) + { + return d_qstate.getInstRounds() % 2 == 0 ? options::UserPatMode::USE + : options::UserPatMode::RESORT; + } + return options::userPatternsQuant(); +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h index 3baa25fa0..b9d0aa745 100644 --- a/src/theory/quantifiers/ematching/inst_strategy.h +++ b/src/theory/quantifiers/ematching/inst_strategy.h @@ -9,7 +9,7 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Instantiation Engine classes + ** \brief Instantiation engine strategy base class **/ #include "cvc4_private.h" @@ -19,6 +19,7 @@ #include #include "expr/node.h" +#include "options/quantifiers_options.h" #include "theory/theory.h" namespace CVC4 { @@ -48,21 +49,23 @@ class InstStrategy public: InstStrategy(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim) - : d_quantEngine(qe), d_qstate(qs), d_qim(qim) - { - } - virtual ~InstStrategy() {} + QuantifiersInferenceManager& qim); + virtual ~InstStrategy(); /** presolve */ - virtual void presolve() {} + virtual void presolve(); /** reset instantiation */ virtual void processResetInstantiationRound(Theory::Effort effort) = 0; /** process method, returns a status */ virtual InstStrategyStatus process(Node f, Theory::Effort effort, int e) = 0; /** identify */ - virtual std::string identify() const { return std::string("Unknown"); } + virtual std::string identify() const; protected: + /** + * Get the current user pat mode, which may be interleaved based on counters + * maintained by the quantifiers state. + */ + options::UserPatMode getInstUserPatMode() const; /** reference to the instantiation engine */ QuantifiersEngine* d_quantEngine; /** The quantifiers state object */ diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 7c8ab5ec2..881133432 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -102,7 +102,7 @@ InstStrategyStatus InstStrategyAutoGenTriggers::process(Node f, Theory::Effort effort, int e) { - options::UserPatMode upMode = d_quantEngine->getInstUserPatMode(); + options::UserPatMode upMode = getInstUserPatMode(); if (hasUserPatterns(f) && upMode == options::UserPatMode::TRUST) { return InstStrategyStatus::STATUS_UNKNOWN; diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp index 9d730e055..cf6405b38 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp @@ -86,7 +86,7 @@ InstStrategyStatus InstStrategyUserPatterns::process(Node q, { return InstStrategyStatus::STATUS_UNFINISHED; } - options::UserPatMode upm = d_quantEngine->getInstUserPatMode(); + options::UserPatMode upm = getInstUserPatMode(); int peffort = upm == options::UserPatMode::RESORT ? 2 : 1; if (e < peffort) { @@ -159,7 +159,7 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat) } Trace("user-pat") << "Add user pattern: " << pat << " for " << q << std::endl; // check match option - if (d_quantEngine->getInstUserPatMode() == options::UserPatMode::RESORT) + if (getInstUserPatMode() == options::UserPatMode::RESORT) { d_user_gen_wait[q].push_back(nodes); return; diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h index 92b427621..996adc444 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h @@ -19,6 +19,7 @@ #include #include "expr/node.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/ematching/inst_strategy.h" #include "theory/quantifiers/ematching/trigger.h" diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index 4f3b207be..50d91a1e1 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -120,7 +120,7 @@ void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ } bool InstantiationEngine::needsCheck( Theory::Effort e ){ - return d_quantEngine->getInstWhenNeedsCheck( e ); + return d_qstate.getInstWhenNeedsCheck(e); } void InstantiationEngine::reset_round( Theory::Effort e ){ diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index 1b011481b..d448699af 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -52,7 +52,8 @@ bool InstStrategyEnum::needsCheck(Theory::Effort e) } if (options::fullSaturateInterleave()) { - if (d_quantEngine->getInstWhenNeedsCheck(e)) + // if interleaved, we run at the same time as E-matching + if (d_qstate.getInstWhenNeedsCheck(e)) { return true; } diff --git a/src/theory/quantifiers/quantifiers_state.cpp b/src/theory/quantifiers/quantifiers_state.cpp index 48b6b2b66..07bd97918 100644 --- a/src/theory/quantifiers/quantifiers_state.cpp +++ b/src/theory/quantifiers/quantifiers_state.cpp @@ -14,6 +14,8 @@ #include "theory/quantifiers/quantifiers_state.h" +#include "options/quantifiers_options.h" + namespace CVC4 { namespace theory { namespace quantifiers { @@ -21,8 +23,133 @@ namespace quantifiers { QuantifiersState::QuantifiersState(context::Context* c, context::UserContext* u, Valuation val) - : TheoryState(c, u, val) + : TheoryState(c, u, val), d_ierCounterc(c) +{ + // allow theory combination to go first, once initially + d_ierCounter = options::instWhenTcFirst() ? 0 : 1; + d_ierCounterc = d_ierCounter; + d_ierCounterLc = 0; + d_ierCounterLastLc = 0; + d_instWhenPhase = + 1 + (options::instWhenPhase() < 1 ? 1 : options::instWhenPhase()); +} + +void QuantifiersState::incrementInstRoundCounters(Theory::Effort e) +{ + 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_ierCounterLc + || !options::instWhenStrictInterleave() + || d_ierCounter % d_instWhenPhase != 0) + { + d_ierCounter = d_ierCounter + 1; + d_ierCounterLastLc = d_ierCounterLc; + d_ierCounterc = d_ierCounterc.get() + 1; + } + } + else if (e == Theory::EFFORT_LAST_CALL) + { + d_ierCounterLc = d_ierCounterLc + 1; + } +} + +bool QuantifiersState::getInstWhenNeedsCheck(Theory::Effort e) const +{ + Trace("qstate-debug") << "Get inst when needs check, counts=" << d_ierCounter + << ", " << d_ierCounterLc << std::endl; + // determine if we should perform check, based on instWhenMode + bool performCheck = false; + if (options::instWhenMode() == options::InstWhenMode::FULL) + { + performCheck = (e >= Theory::EFFORT_FULL); + } + else if (options::instWhenMode() == options::InstWhenMode::FULL_DELAY) + { + performCheck = (e >= Theory::EFFORT_FULL) && !d_valuation.needCheck(); + } + else if (options::instWhenMode() == options::InstWhenMode::FULL_LAST_CALL) + { + performCheck = + ((e == Theory::EFFORT_FULL && d_ierCounter % d_instWhenPhase != 0) + || e == Theory::EFFORT_LAST_CALL); + } + else if (options::instWhenMode() + == options::InstWhenMode::FULL_DELAY_LAST_CALL) + { + performCheck = ((e == Theory::EFFORT_FULL && !d_valuation.needCheck() + && d_ierCounter % d_instWhenPhase != 0) + || e == Theory::EFFORT_LAST_CALL); + } + else if (options::instWhenMode() == options::InstWhenMode::LAST_CALL) + { + performCheck = (e >= Theory::EFFORT_LAST_CALL); + } + else + { + performCheck = true; + } + Trace("qstate-debug") << "...returned " << performCheck << std::endl; + return performCheck; +} + +uint64_t QuantifiersState::getInstRoundDepth() const +{ + return d_ierCounterc.get(); +} + +uint64_t QuantifiersState::getInstRounds() const { return d_ierCounter; } + +void QuantifiersState::debugPrintEqualityEngine(const char* c) const { + bool traceEnabled = Trace.isOn(c); + if (!traceEnabled) + { + return; + } + eq::EqualityEngine* ee = getEqualityEngine(); + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee); + std::map tnum; + while (!eqcs_i.isFinished()) + { + TNode r = (*eqcs_i); + TypeNode tr = r.getType(); + if (tnum.find(tr) == tnum.end()) + { + tnum[tr] = 0; + } + tnum[tr]++; + bool firstTime = true; + Trace(c) << " " << r; + Trace(c) << " : { "; + eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee); + while (!eqc_i.isFinished()) + { + TNode n = (*eqc_i); + if (r != n) + { + if (firstTime) + { + Trace(c) << std::endl; + firstTime = false; + } + Trace(c) << " " << n << std::endl; + } + ++eqc_i; + } + if (!firstTime) + { + Trace(c) << " "; + } + Trace(c) << "}" << std::endl; + ++eqcs_i; + } + Trace(c) << std::endl; + for (const std::pair& t : tnum) + { + Trace(c) << "# eqc for " << t.first << " : " << t.second << std::endl; + } } } // namespace quantifiers diff --git a/src/theory/quantifiers/quantifiers_state.h b/src/theory/quantifiers/quantifiers_state.h index 76baab7ca..d45938f98 100644 --- a/src/theory/quantifiers/quantifiers_state.h +++ b/src/theory/quantifiers/quantifiers_state.h @@ -17,6 +17,7 @@ #ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H #define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H +#include "theory/theory.h" #include "theory/theory_state.h" namespace CVC4 { @@ -31,6 +32,44 @@ class QuantifiersState : public TheoryState public: QuantifiersState(context::Context* c, context::UserContext* u, Valuation val); ~QuantifiersState() {} + /** + * Increment the instantiation counters, called once at the beginning of when + * we perform a check with quantifiers engine for the given effort. + */ + void incrementInstRoundCounters(Theory::Effort e); + /** + * Get whether we need to check at effort e based on the inst-when mode. This + * option determines the policy of quantifier instantiation and theory + * combination, e.g. does it run before, after, or interleaved with theory + * combination. This is based on the state of the counters maintained by this + * class. + */ + bool getInstWhenNeedsCheck(Theory::Effort e) const; + /** Get the number of instantiation rounds performed in this SAT context */ + uint64_t getInstRoundDepth() const; + /** Get the total number of instantiation rounds performed */ + uint64_t getInstRounds() const; + /** debug print equality engine on trace c */ + void debugPrintEqualityEngine(const char* c) const; + + private: + /** The number of instantiation rounds in this SAT context */ + context::CDO d_ierCounterc; + /** The number of total instantiation rounds (full effort) */ + uint64_t d_ierCounter; + /** The number of total instantiation rounds (last call effort) */ + uint64_t d_ierCounterLc; + /** + * A counter to remember the last value of d_ierCounterLc where we a + * full effort check. This is used for interleaving theory combination + * and quantifier instantiation rounds. + */ + uint64_t d_ierCounterLastLc; + /** + * The number of instantiation rounds we run for each call to theory + * combination. + */ + uint64_t d_instWhenPhase; }; } // namespace quantifiers diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 33ec3cbf8..e85d6f2ff 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -54,7 +54,6 @@ QuantifiersEngine::QuantifiersEngine( d_term_enum(new quantifiers::TermEnumeration), d_quants_prereg(qstate.getUserContext()), d_quants_red(qstate.getUserContext()), - d_ierCounter_c(qstate.getSatContext()), d_presolve(qstate.getUserContext(), true), d_presolve_in(qstate.getUserContext()), d_presolve_cache(qstate.getUserContext()) @@ -77,13 +76,6 @@ QuantifiersEngine::QuantifiersEngine( //---- end utilities - //allow theory combination to go first, once initially - d_ierCounter = options::instWhenTcFirst() ? 0 : 1; - d_ierCounter_c = d_ierCounter; - d_ierCounter_lc = 0; - d_ierCounterLastLc = 0; - d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() ); - // Finite model finding requires specialized ways of building the model. // We require constructing the model and model builder here, since it is // required for initializing the CombinationEngine. @@ -377,7 +369,8 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( Trace.isOn("quant-engine-debug") ){ Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl; - Trace("quant-engine-debug") << " depth : " << d_ierCounter_c << std::endl; + Trace("quant-engine-debug") + << " depth : " << d_qstate.getInstRoundDepth() << std::endl; Trace("quant-engine-debug") << " modules to check : "; for( unsigned i=0; iidentify() << " "; @@ -398,7 +391,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ } if( Trace.isOn("quant-engine-ee-pre") ){ Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl; - debugPrintEqualityEngine( "quant-engine-ee-pre" ); + d_qstate.debugPrintEqualityEngine("quant-engine-ee-pre"); } if( Trace.isOn("quant-engine-assert") ){ Trace("quant-engine-assert") << "Assertions : " << std::endl; @@ -426,7 +419,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( Trace.isOn("quant-engine-ee") ){ Trace("quant-engine-ee") << "Equality engine : " << std::endl; - debugPrintEqualityEngine( "quant-engine-ee" ); + d_qstate.debugPrintEqualityEngine("quant-engine-ee"); } //reset the model @@ -499,16 +492,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ Assert(!d_qstate.isInConflict()); 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 ){ - d_ierCounter = d_ierCounter + 1; - d_ierCounterLastLc = d_ierCounter_lc; - d_ierCounter_c = d_ierCounter_c.get() + 1; - } - }else if( e==Theory::EFFORT_LAST_CALL ){ - d_ierCounter_lc = d_ierCounter_lc + 1; - } + d_qstate.incrementInstRoundCounters(e); } else if (quant_e == QuantifiersModule::QEFFORT_MODEL) { @@ -617,9 +601,9 @@ void QuantifiersEngine::check( Theory::Effort e ){ } void QuantifiersEngine::notifyCombineTheories() { - //if allowing theory combination to happen at most once between instantiation rounds - //d_ierCounter = 1; - //d_ierCounterLastLc = -1; + // If allowing theory combination to happen at most once between instantiation + // rounds, this would reset d_ierCounter to 1 and d_ierCounterLastLc to -1 + // in quantifiers state. } bool QuantifiersEngine::reduceQuantifier( Node q ) { @@ -789,55 +773,6 @@ void QuantifiersEngine::markRelevant( Node q ) { d_model->markRelevant( q ); } -bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { - Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl; - //determine if we should perform check, based on instWhenMode - bool performCheck = false; - if (options::instWhenMode() == options::InstWhenMode::FULL) - { - performCheck = ( e >= Theory::EFFORT_FULL ); - } - else if (options::instWhenMode() == options::InstWhenMode::FULL_DELAY) - { - performCheck = - (e >= Theory::EFFORT_FULL) && !d_qstate.getValuation().needCheck(); - } - else if (options::instWhenMode() == options::InstWhenMode::FULL_LAST_CALL) - { - performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%d_inst_when_phase!=0 ) || e==Theory::EFFORT_LAST_CALL ); - } - else if (options::instWhenMode() - == options::InstWhenMode::FULL_DELAY_LAST_CALL) - { - performCheck = - ((e == Theory::EFFORT_FULL && !d_qstate.getValuation().needCheck() - && d_ierCounter % d_inst_when_phase != 0) - || e == Theory::EFFORT_LAST_CALL); - } - else if (options::instWhenMode() == options::InstWhenMode::LAST_CALL) - { - performCheck = ( e >= Theory::EFFORT_LAST_CALL ); - } - else - { - performCheck = true; - } - return performCheck; -} - -options::UserPatMode QuantifiersEngine::getInstUserPatMode() -{ - if (options::userPatternsQuant() == options::UserPatMode::INTERLEAVE) - { - return d_ierCounter % 2 == 0 ? options::UserPatMode::USE - : options::UserPatMode::RESORT; - } - else - { - return options::userPatternsQuant(); - } -} - void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) { d_instantiate->getInstantiationTermVectors(q, tvecs); } @@ -960,41 +895,5 @@ bool QuantifiersEngine::getSynthSolutions( return d_qmodules->d_synth_e->getSynthSolutions(sol_map); } -void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { - eq::EqualityEngine* ee = d_qstate.getEqualityEngine(); - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); - std::map< TypeNode, int > typ_num; - while( !eqcs_i.isFinished() ){ - TNode r = (*eqcs_i); - TypeNode tr = r.getType(); - if( typ_num.find( tr )==typ_num.end() ){ - typ_num[tr] = 0; - } - typ_num[tr]++; - bool firstTime = true; - Trace(c) << " " << r; - Trace(c) << " : { "; - eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); - while( !eqc_i.isFinished() ){ - TNode n = (*eqc_i); - if( r!=n ){ - if( firstTime ){ - Trace(c) << std::endl; - firstTime = false; - } - Trace(c) << " " << n << std::endl; - } - ++eqc_i; - } - if( !firstTime ){ Trace(c) << " "; } - Trace(c) << "}" << std::endl; - ++eqcs_i; - } - Trace(c) << std::endl; - for( std::map< TypeNode, int >::iterator it = typ_num.begin(); it != typ_num.end(); ++it ){ - Trace(c) << "# eqc for " << it->first << " : " << it->second << std::endl; - } -} - } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index cab452e2b..99e4ad5cc 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -178,18 +178,10 @@ public: /** mark relevant quantified formula, this will indicate it should be checked * before the others */ void markRelevant(Node q); - /** get needs check */ - bool getInstWhenNeedsCheck(Theory::Effort e); - /** get user pat mode */ - options::UserPatMode getInstUserPatMode(); - -public: /** add term to database */ void addTermToDatabase(Node n, bool withinQuant = false); /** notification when master equality engine is updated */ void eqNotifyNewClass(TNode t); - /** debug print equality engine */ - void debugPrintEqualityEngine(const char* c); /** get internal representative * * Choose a term that is equivalent to a in the current context that is the @@ -329,12 +321,6 @@ public: /** quantifiers reduced */ BoolMap d_quants_red; std::map d_quants_red_lem; - /** inst round counters TODO: make context-dependent? */ - context::CDO d_ierCounter_c; - int d_ierCounter; - int d_ierCounter_lc; - int d_ierCounterLastLc; - int d_inst_when_phase; /** has presolve been called */ context::CDO d_presolve; /** presolve cache */ -- 2.30.2