From: Andrew Reynolds Date: Sat, 28 Oct 2017 21:53:55 +0000 (-0500) Subject: (Move only) Move enumerative instantiation strategy to its own file and document... X-Git-Tag: cvc5-1.0.0~5523 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d33fc58a4fccfe6bc9059e0dd47afea2ed69d1ad;p=cvc5.git (Move only) Move enumerative instantiation strategy to its own file and document (#1290) * Move, document, and rename enumerative instantiation. * Clang format. --- diff --git a/src/Makefile.am b/src/Makefile.am index 0bcd35215..3648e824b 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -392,6 +392,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/inst_strategy_cbqi.h \ theory/quantifiers/inst_strategy_e_matching.cpp \ theory/quantifiers/inst_strategy_e_matching.h \ + theory/quantifiers/inst_strategy_enumerative.cpp \ + theory/quantifiers/inst_strategy_enumerative.h \ theory/quantifiers/instantiation_engine.cpp \ theory/quantifiers/instantiation_engine.h \ theory/quantifiers/local_theory_ext.cpp \ diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 105f8f5e2..0b248056c 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -15,18 +15,22 @@ #include "theory/quantifiers/inst_strategy_e_matching.h" #include "theory/quantifiers/inst_match_generator.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/relevant_domain.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #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::inst; -using namespace CVC4::theory::quantifiers; + +namespace CVC4 { + +using namespace kind; +using namespace context; + +namespace theory { + +using namespace inst; + +namespace quantifiers { //priority levels : //1 : user patterns (when user-pat!={resort,ignore}), auto-gen patterns (for non-user pattern quantifiers, or when user-pat={resort,ignore}) @@ -600,198 +604,7 @@ bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) { } } */ -FullSaturation::FullSaturation( QuantifiersEngine* qe ) : QuantifiersModule( qe ){ - -} - -bool FullSaturation::needsCheck( Theory::Effort e ){ - if( options::fullSaturateInterleave() ){ - if( d_quantEngine->getInstWhenNeedsCheck( e ) ){ - return true; - } - } - if( options::fullSaturateQuant() ){ - if( e>=Theory::EFFORT_LAST_CALL ){ - return true; - } - } - return false; -} - -void FullSaturation::reset_round( Theory::Effort e ) { - -} - -void FullSaturation::check( Theory::Effort e, unsigned 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(); - } - if( options::fullSaturateQuant() && !doCheck ){ - doCheck = quant_e==QuantifiersEngine::QEFFORT_LAST_CALL; - fullEffort = !d_quantEngine->hasAddedLemma(); - } - if( doCheck ){ - double clSet = 0; - if( Trace.isOn("fs-engine") ){ - clSet = double(clock())/double(CLOCKS_PER_SEC); - Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---" << std::endl; - } - int addedLemmas = 0; - for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ - Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true ); - if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ - if( process( q, fullEffort ) ){ - //added lemma - addedLemmas++; - if( d_quantEngine->inConflict() ){ - break; - } - } - } - } - if( Trace.isOn("fs-engine") ){ - Trace("fs-engine") << "Added lemmas = " << addedLemmas << std::endl; - double clSet2 = double(clock())/double(CLOCKS_PER_SEC); - Trace("fs-engine") << "Finished full saturation engine, time = " << (clSet2-clSet) << std::endl; - } - } -} -bool FullSaturation::process( Node f, bool fullEffort ){ - // ignore if constant true (rare case of non-standard quantifier whose body is rewritten to true) - if( f[1].isConst() && f[1].getConst() ){ - return false; - } - //first, try from relevant domain - RelevantDomain * rd = d_quantEngine->getRelevantDomain(); - unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1; - unsigned rend = fullEffort ? 1 : rstart; - for( unsigned r=rstart; r<=rend; r++ ){ - if( rd || r>0 ){ - if( r==0 ){ - Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl; - }else{ - Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl; - } - Assert( rd!=NULL ); - Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl; - rd->compute(); - Trace("inst-alg-debug") << "...finished" << std::endl; - unsigned final_max_i = 0; - std::vector< unsigned > maxs; - std::vector< bool > max_zero; - bool has_zero = false; - std::map< TypeNode, std::vector< Node > > term_db_list; - std::vector< TypeNode > ftypes; - // iterate over substitutions for variables - for(unsigned i=0; igetRDomain( f, i )->d_terms.size(); - }else{ - ts = d_quantEngine->getTermDatabase()->getNumTypeGroundTerms( tn ); - std::map< TypeNode, std::vector< Node > >::iterator ittd = term_db_list.find( tn ); - if( ittd==term_db_list.end() ){ - std::map< Node, Node > reps_found; - for( unsigned j=0; jgetTermDatabase()->getTypeGroundTerm( ftypes[i], j ); - if( !options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr( gt ) ){ - Node r = d_quantEngine->getEqualityQuery()->getRepresentative( gt ); - if( reps_found.find( r )==reps_found.end() ){ - reps_found[r] = gt; - term_db_list[tn].push_back( gt ); - } - } - } - ts = term_db_list[tn].size(); - }else{ - ts = ittd->second.size(); - } - } - // consider a default value if at full effort - max_zero.push_back( fullEffort && ts==0 ); - ts = ( fullEffort && ts==0 ) ? 1 : ts; - Trace("inst-alg-rd") << "Variable " << i << " has " << ts << " in relevant domain." << std::endl; - if( ts==0 ){ - has_zero = true; - break; - }else{ - maxs.push_back( ts ); - if( ts>final_max_i ){ - final_max_i = ts; - } - } - } - if( !has_zero ){ - Trace("inst-alg-rd") << "Will do " << final_max_i << " stages of instantiation." << std::endl; - unsigned max_i = 0; - bool success; - while( max_i<=final_max_i ){ - Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl; - std::vector< unsigned > childIndex; - int index = 0; - do { - while( index>=0 && index<(int)f[0].getNumChildren() ){ - if( index==(int)childIndex.size() ){ - childIndex.push_back( -1 ); - }else{ - Assert( index==(int)(childIndex.size())-1 ); - unsigned nv = childIndex[index]+1; - if( nv=0; - if( success ){ - Trace("inst-alg-rd") << "Try instantiation { "; - for( unsigned j=0; j terms; - for( unsigned i=0; igetRDomain( f, i )->d_terms[childIndex[i]] ); - Trace("inst-alg-rd") << " " << rd->getRDomain( f, i )->d_terms[childIndex[i]] << std::endl; - }else{ - Assert( childIndex[i]addInstantiation( f, terms ) ){ - Trace("inst-alg-rd") << "Success!" << std::endl; - ++(d_quantEngine->d_statistics.d_instantiations_guess); - return true; - }else{ - index--; - } - } - }while( success ); - max_i++; - } - } - } - } - //TODO : term enumerator? - return false; -} - -void FullSaturation::registerQuantifier( Node q ) { - -} +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index 5a4f8e499..1a0ec9b44 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -111,23 +111,6 @@ public: void addUserNoPattern( Node q, Node pat ); };/* class InstStrategyAutoGenTriggers */ -class FullSaturation : public QuantifiersModule { -private: - /** guessed instantiations */ - std::map< Node, bool > d_guessed; - /** process functions */ - bool process( Node q, bool fullEffort ); -public: - FullSaturation( QuantifiersEngine* qe ); - ~FullSaturation(){} - bool needsCheck( Theory::Effort e ); - void reset_round( Theory::Effort e ); - void check( Theory::Effort e, unsigned quant_e ); - void registerQuantifier( Node q ); - /** identify */ - std::string identify() const { return std::string("FullSaturation"); } -};/* class FullSaturation */ - } }/* CVC4::theory namespace */ diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp new file mode 100644 index 000000000..8b825d50d --- /dev/null +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -0,0 +1,302 @@ +/********************* */ +/*! \file inst_strategy_enumerative.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 Implementation of an enumerative instantiation strategy. + **/ + +#include "theory/quantifiers/inst_strategy_enumerative.h" + +#include "options/quantifiers_options.h" +#include "theory/quantifiers/relevant_domain.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" + +namespace CVC4 { + +using namespace kind; +using namespace context; + +namespace theory { + +using namespace inst; + +namespace quantifiers { + +InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe) + : QuantifiersModule(qe) +{ +} + +bool InstStrategyEnum::needsCheck(Theory::Effort e) +{ + if (options::fullSaturateInterleave()) + { + if (d_quantEngine->getInstWhenNeedsCheck(e)) + { + return true; + } + } + if (options::fullSaturateQuant()) + { + if (e >= Theory::EFFORT_LAST_CALL) + { + return true; + } + } + return false; +} + +void InstStrategyEnum::reset_round(Theory::Effort e) {} +void InstStrategyEnum::check(Theory::Effort e, unsigned 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(); + } + if (options::fullSaturateQuant() && !doCheck) + { + doCheck = quant_e == QuantifiersEngine::QEFFORT_LAST_CALL; + fullEffort = !d_quantEngine->hasAddedLemma(); + } + if (doCheck) + { + double clSet = 0; + if (Trace.isOn("fs-engine")) + { + clSet = double(clock()) / double(CLOCKS_PER_SEC); + Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---" + << std::endl; + } + int addedLemmas = 0; + for (unsigned i = 0; + i < d_quantEngine->getModel()->getNumAssertedQuantifiers(); + i++) + { + Node q = d_quantEngine->getModel()->getAssertedQuantifier(i, true); + if (d_quantEngine->hasOwnership(q, this) + && d_quantEngine->getModel()->isQuantifierActive(q)) + { + if (process(q, fullEffort)) + { + // added lemma + addedLemmas++; + if (d_quantEngine->inConflict()) + { + break; + } + } + } + } + if (Trace.isOn("fs-engine")) + { + Trace("fs-engine") << "Added lemmas = " << addedLemmas << std::endl; + double clSet2 = double(clock()) / double(CLOCKS_PER_SEC); + Trace("fs-engine") << "Finished full saturation engine, time = " + << (clSet2 - clSet) << std::endl; + } + } +} + +bool InstStrategyEnum::process(Node f, bool fullEffort) +{ + // ignore if constant true (rare case of non-standard quantifier whose body is + // rewritten to true) + if (f[1].isConst() && f[1].getConst()) + { + return false; + } + // first, try from relevant domain + RelevantDomain* rd = d_quantEngine->getRelevantDomain(); + unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1; + unsigned rend = fullEffort ? 1 : rstart; + for (unsigned r = rstart; r <= rend; r++) + { + if (rd || r > 0) + { + if (r == 0) + { + Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." + << std::endl; + } + else + { + Trace("inst-alg") << "-> Ground term instantiate " << f << "..." + << std::endl; + } + Assert(rd != NULL); + Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl; + rd->compute(); + Trace("inst-alg-debug") << "...finished" << std::endl; + unsigned final_max_i = 0; + std::vector maxs; + std::vector max_zero; + bool has_zero = false; + std::map > term_db_list; + std::vector ftypes; + // iterate over substitutions for variables + for (unsigned i = 0; i < f[0].getNumChildren(); i++) + { + TypeNode tn = f[0][i].getType(); + ftypes.push_back(tn); + unsigned ts; + if (r == 0) + { + ts = rd->getRDomain(f, i)->d_terms.size(); + } + else + { + ts = d_quantEngine->getTermDatabase()->getNumTypeGroundTerms(tn); + std::map >::iterator ittd = + term_db_list.find(tn); + if (ittd == term_db_list.end()) + { + std::map reps_found; + for (unsigned j = 0; j < ts; j++) + { + Node gt = d_quantEngine->getTermDatabase()->getTypeGroundTerm( + ftypes[i], j); + if (!options::cbqi() + || !quantifiers::TermUtil::hasInstConstAttr(gt)) + { + Node r = + d_quantEngine->getEqualityQuery()->getRepresentative(gt); + if (reps_found.find(r) == reps_found.end()) + { + reps_found[r] = gt; + term_db_list[tn].push_back(gt); + } + } + } + ts = term_db_list[tn].size(); + } + else + { + ts = ittd->second.size(); + } + } + // consider a default value if at full effort + max_zero.push_back(fullEffort && ts == 0); + ts = (fullEffort && ts == 0) ? 1 : ts; + Trace("inst-alg-rd") << "Variable " << i << " has " << ts + << " in relevant domain." << std::endl; + if (ts == 0) + { + has_zero = true; + break; + } + else + { + maxs.push_back(ts); + if (ts > final_max_i) + { + final_max_i = ts; + } + } + } + if (!has_zero) + { + Trace("inst-alg-rd") << "Will do " << final_max_i + << " stages of instantiation." << std::endl; + unsigned max_i = 0; + bool success; + while (max_i <= final_max_i) + { + Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl; + std::vector childIndex; + int index = 0; + do + { + while (index >= 0 && index < (int)f[0].getNumChildren()) + { + if (index == (int)childIndex.size()) + { + childIndex.push_back(-1); + } + else + { + Assert(index == (int)(childIndex.size()) - 1); + unsigned nv = childIndex[index] + 1; + if (nv < maxs[index] && nv <= max_i) + { + childIndex[index] = nv; + index++; + } + else + { + childIndex.pop_back(); + index--; + } + } + } + success = index >= 0; + if (success) + { + Trace("inst-alg-rd") << "Try instantiation { "; + for (unsigned j = 0; j < childIndex.size(); j++) + { + Trace("inst-alg-rd") << childIndex[j] << " "; + } + Trace("inst-alg-rd") << "}" << std::endl; + // try instantiation + std::vector terms; + for (unsigned i = 0; i < f[0].getNumChildren(); i++) + { + if (max_zero[i]) + { + // no terms available, will report incomplete instantiation + terms.push_back(Node::null()); + Trace("inst-alg-rd") << " null" << std::endl; + } + else if (r == 0) + { + terms.push_back(rd->getRDomain(f, i)->d_terms[childIndex[i]]); + Trace("inst-alg-rd") + << " " << rd->getRDomain(f, i)->d_terms[childIndex[i]] + << std::endl; + } + else + { + Assert(childIndex[i] < term_db_list[ftypes[i]].size()); + terms.push_back(term_db_list[ftypes[i]][childIndex[i]]); + Trace("inst-alg-rd") << " " + << term_db_list[ftypes[i]][childIndex[i]] + << std::endl; + } + } + if (d_quantEngine->addInstantiation(f, terms)) + { + Trace("inst-alg-rd") << "Success!" << std::endl; + ++(d_quantEngine->d_statistics.d_instantiations_guess); + return true; + } + else + { + index--; + } + } + } while (success); + max_i++; + } + } + } + } + // TODO : term enumerator instantiation? + return false; +} + +void InstStrategyEnum::registerQuantifier(Node q) {} +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h new file mode 100644 index 000000000..d79917eda --- /dev/null +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -0,0 +1,105 @@ +/********************* */ +/*! \file inst_strategy_enumerative.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 Enumerative instantiation + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__INST_STRATEGY_ENUMERATIVE_H +#define __CVC4__INST_STRATEGY_ENUMERATIVE_H + +#include "context/context.h" +#include "context/context_mm.h" +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** Enumerative instantiation + * + * This class implements enumerative instantiation described + * in Reynolds et al., "Revisiting Enumerative Instantiation". + * + * It is an instance of QuantifiersModule, whose main + * task is to make calls to QuantifiersEngine during + * calls to QuantifiersModule::check(...). + * + * This class adds instantiations based on enumerating + * well-typed terms that occur in the current context + * based on a heuristically determined ordering on + * tuples of terms. This ordering incorporates + * reasoning about the relevant domain of quantified + * formulas (see theory/quantifiers/relevant_domain.h). + * We consider only ground terms that occur in the + * context due to Theorem 1 of "Revisiting Enumerative + * Instantiation". Notice this theorem holds only for theories + * with compactness. For theories such as arithmetic, + * this class may introduce "default" terms that are + * used in instantiations, say 0 for arithmetic, even + * when the term 0 does not occur in the context. + * + * This strategy is not enabled by default, and + * is enabled by the option: + * --full-saturate-quant + * + * It is generally called with lower priority than + * other instantiation strategies, although this + * option interleaves it with other strategies + * during quantifier effort level QEFFORT_STANDARD: + * --fs-interleave + */ +class InstStrategyEnum : public QuantifiersModule +{ + public: + InstStrategyEnum(QuantifiersEngine* qe); + ~InstStrategyEnum() {} + /** Needs check. */ + bool needsCheck(Theory::Effort e) override; + /** Reset round. */ + void reset_round(Theory::Effort e) override; + /** Check. + * Adds instantiations for all currently asserted + * quantified formulas via calls to process(...) + */ + void check(Theory::Effort e, unsigned quant_e) override; + /** Register quantifier. */ + void registerQuantifier(Node q) override; + /** Identify. */ + std::string identify() const override + { + return std::string("InstStrategyEnum"); + } + + private: + /** process quantified formula + * + * q is the quantified formula we are constructing instances for. + * fullEffort is whether we are called at full effort. + * + * If this function returns true, then one instantiation + * (determined by an enumeration) was added via a successful + * call to QuantifiersEngine::addInstantiation(...). + * + * If fullEffort is true, then we may introduce a "default" + * well-typed term *not* occurring in the current context. + * This handles corner cases where there are no well-typed + * ground terms in the current context to instantiate with. + */ + bool process(Node q, bool fullEffort); +}; /* class InstStrategyEnum */ + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index fdb70c85b..2d5f48a5c 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -19,25 +19,29 @@ #include "smt/smt_statistics_registry.h" #include "theory/arrays/theory_arrays.h" #include "theory/datatypes/theory_datatypes.h" -#include "theory/sep/theory_sep.h" #include "theory/quantifiers/alpha_equivalence.h" #include "theory/quantifiers/ambqi_builder.h" +#include "theory/quantifiers/anti_skolem.h" #include "theory/quantifiers/bounded_integers.h" #include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/ceg_t_instantiator.h" #include "theory/quantifiers/conjecture_generator.h" +#include "theory/quantifiers/equality_infer.h" #include "theory/quantifiers/equality_query.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/full_model_check.h" #include "theory/quantifiers/fun_def_engine.h" +#include "theory/quantifiers/inst_propagator.h" #include "theory/quantifiers/inst_strategy_cbqi.h" #include "theory/quantifiers/inst_strategy_e_matching.h" +#include "theory/quantifiers/inst_strategy_enumerative.h" #include "theory/quantifiers/instantiation_engine.h" #include "theory/quantifiers/local_theory_ext.h" #include "theory/quantifiers/model_engine.h" -#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/quant_equality_engine.h" +#include "theory/quantifiers/quant_split.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/relevant_domain.h" #include "theory/quantifiers/rewrite_engine.h" @@ -45,10 +49,7 @@ #include "theory/quantifiers/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers/trigger.h" -#include "theory/quantifiers/quant_split.h" -#include "theory/quantifiers/anti_skolem.h" -#include "theory/quantifiers/equality_infer.h" -#include "theory/quantifiers/inst_propagator.h" +#include "theory/sep/theory_sep.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" @@ -298,7 +299,7 @@ void QuantifiersEngine::finishInit(){ } //full saturation : instantiate from relevant domain, then arbitrary terms if( options::fullSaturateQuant() || options::fullSaturateInterleave() ){ - d_fs = new quantifiers::FullSaturation( this ); + d_fs = new quantifiers::InstStrategyEnum(this); d_modules.push_back( d_fs ); needsRelDom = true; } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 0bb5b10e5..be0c4cd43 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -74,7 +74,7 @@ namespace quantifiers { class AlphaEquivalence; class FunDefEngine; class QuantEqualityEngine; - class FullSaturation; + class InstStrategyEnum; class InstStrategyCbqi; class InstStrategyCegqi; class QuantDSplit; @@ -155,7 +155,7 @@ private: /** quantifiers equality engine */ quantifiers::QuantEqualityEngine * d_uee; /** full saturation */ - quantifiers::FullSaturation * d_fs; + quantifiers::InstStrategyEnum* d_fs; /** counterexample-based quantifier instantiation */ quantifiers::InstStrategyCbqi * d_i_cbqi; /** quantifiers splitting */ @@ -275,7 +275,7 @@ public: //modules /** quantifiers equality engine */ quantifiers::QuantEqualityEngine * getQuantEqualityEngine() { return d_uee; } /** get full saturation */ - quantifiers::FullSaturation * getFullSaturation() { return d_fs; } + quantifiers::InstStrategyEnum* getInstStrategyEnum() { return d_fs; } /** get inst strategy cbqi */ quantifiers::InstStrategyCbqi * getInstStrategyCbqi() { return d_i_cbqi; } /** get quantifiers splitting */