* Move, document, and rename enumerative instantiation.
* Clang format.
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 \
#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})
}
}
*/
-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; 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 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<bool>() ){
- 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; 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< 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; 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< 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<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< Node > 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?
- return false;
-}
-
-void FullSaturation::registerQuantifier( Node q ) {
-
-}
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
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 */
--- /dev/null
+/********************* */
+/*! \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<bool>())
+ {
+ 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; 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<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; 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<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 < 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<Node> 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 */
--- /dev/null
+/********************* */
+/*! \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
#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"
#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"
}
//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;
}
class AlphaEquivalence;
class FunDefEngine;
class QuantEqualityEngine;
- class FullSaturation;
+ class InstStrategyEnum;
class InstStrategyCbqi;
class InstStrategyCegqi;
class QuantDSplit;
/** 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 */
/** 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 */
projects / cvc5.git / commitdiff