summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/Makefile.am10
-rwxr-xr-xsrc/theory/quantifiers/inst_strategy_cbqi.cpp403
-rwxr-xr-xsrc/theory/quantifiers/inst_strategy_cbqi.h110
-rwxr-xr-xsrc/theory/quantifiers/inst_strategy_e_matching.cpp379
-rwxr-xr-xsrc/theory/quantifiers/inst_strategy_e_matching.h132
-rw-r--r--src/theory/quantifiers/instantiation_engine.cpp108
-rw-r--r--src/theory/quantifiers/instantiation_engine.h81
-rw-r--r--src/theory/quantifiers/instantiator_default.cpp54
-rw-r--r--src/theory/quantifiers/instantiator_default.h46
-rw-r--r--src/theory/quantifiers/kinds1
-rw-r--r--src/theory/quantifiers/model_builder.cpp2
-rw-r--r--src/theory/quantifiers/model_engine.cpp1
-rw-r--r--src/theory/quantifiers/term_database.cpp2
-rw-r--r--src/theory/quantifiers/theory_quantifiers.cpp1
-rw-r--r--src/theory/quantifiers/theory_quantifiers_instantiator.cpp73
-rw-r--r--src/theory/quantifiers/theory_quantifiers_instantiator.h58
-rw-r--r--src/theory/quantifiers/trigger.cpp1
17 files changed, 1199 insertions, 263 deletions
diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am
index 371aa5543..316af7616 100644
--- a/src/theory/quantifiers/Makefile.am
+++ b/src/theory/quantifiers/Makefile.am
@@ -11,16 +11,12 @@ libquantifiers_la_SOURCES = \
quantifiers_rewriter.h \
quantifiers_rewriter.cpp \
theory_quantifiers.cpp \
- theory_quantifiers_instantiator.h \
- theory_quantifiers_instantiator.cpp \
instantiation_engine.h \
instantiation_engine.cpp \
trigger.h \
trigger.cpp \
candidate_generator.h \
candidate_generator.cpp \
- instantiator_default.h \
- instantiator_default.cpp \
inst_match.h \
inst_match.cpp \
model_engine.h \
@@ -44,7 +40,11 @@ libquantifiers_la_SOURCES = \
inst_match_generator.h \
inst_match_generator.cpp \
macros.h \
- macros.cpp
+ macros.cpp \
+ inst_strategy_e_matching.h \
+ inst_strategy_e_matching.cpp \
+ inst_strategy_cbqi.h \
+ inst_strategy_cbqi.cpp
EXTRA_DIST = \
kinds \
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
new file mode 100755
index 000000000..d79ddee31
--- /dev/null
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -0,0 +1,403 @@
+/********************* */
+/*! \file inst_strategy_cbqi.cpp
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): bobot, mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of cbqi instantiation strategies
+ **/
+
+#include "theory/quantifiers/inst_strategy_cbqi.h"
+#include "theory/arith/theory_arith.h"
+#include "theory/theory_engine.h"
+#include "theory/quantifiers/options.h"
+#include "theory/quantifiers/term_database.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::theory::arith;
+using namespace CVC4::theory::datatypes;
+
+#define ARITH_INSTANTIATOR_USE_MINUS_DELTA
+
+InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) :
+ InstStrategy( ie ), d_th( th ), d_counter( 0 ){
+ d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) );
+}
+
+bool InstStrategySimplex::calculateShouldProcess( Node f ){
+ //DO_THIS
+ return false;
+}
+
+void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ){
+ Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl;
+ d_instRows.clear();
+ d_tableaux_term.clear();
+ d_tableaux.clear();
+ d_ceTableaux.clear();
+ //search for instantiation rows in simplex tableaux
+ ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap();
+ for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){
+ ArithVar x = (*it).first;
+ if( d_th->d_partialModel.hasEitherBound( x ) ){
+ Node n = (*it).second;
+ Node f;
+ NodeBuilder<> t(kind::PLUS);
+ if( n.getKind()==PLUS ){
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ addTermToRow( x, n[i], f, t );
+ }
+ }else{
+ addTermToRow( x, n, f, t );
+ }
+ if( f!=Node::null() ){
+ d_instRows[f].push_back( x );
+ //this theory has constraints from f
+ Debug("quant-arith") << "Has constraints from " << f << std::endl;
+ //set that we should process it
+ d_quantActive[ f ] = true;
+ //set tableaux term
+ if( t.getNumChildren()==0 ){
+ d_tableaux_term[x] = NodeManager::currentNM()->mkConst( Rational(0) );
+ }else if( t.getNumChildren()==1 ){
+ d_tableaux_term[x] = t.getChild( 0 );
+ }else{
+ d_tableaux_term[x] = t;
+ }
+ }
+ }
+ }
+ //print debug
+ debugPrint( "quant-arith-debug" );
+ d_counter++;
+}
+
+int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
+ if( e<2 ){
+ return STATUS_UNFINISHED;
+ }else if( e==2 ){
+ //Notice() << f << std::endl;
+ //Notice() << "Num inst rows = " << d_th->d_instRows[f].size() << std::endl;
+ //Notice() << "Num inst constants = " << d_quantEngine->getNumInstantiationConstants( f ) << std::endl;
+ Debug("quant-arith-simplex") << "InstStrategySimplex check " << f << ", rows = " << d_instRows[f].size() << std::endl;
+ for( int j=0; j<(int)d_instRows[f].size(); j++ ){
+ ArithVar x = d_instRows[f][j];
+ if( !d_ceTableaux[x].empty() ){
+ Debug("quant-arith-simplex") << "Check row " << x << std::endl;
+ //instantiation row will be A*e + B*t = beta,
+ // where e is a vector of terms , and t is vector of ground terms.
+ // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant
+ // We will construct the term ( beta - B*t)/coeff to use for e_i.
+ InstMatch m;
+ //By default, choose the first instantiation constant to be e_i.
+ Node var = d_ceTableaux[x].begin()->first;
+ if( var.getType().isInteger() ){
+ std::map< Node, Node >::iterator it = d_ceTableaux[x].begin();
+ //try to find coefficent that is +/- 1
+ while( !var.isNull() && !d_ceTableaux[x][var].isNull() && d_ceTableaux[x][var]!=d_negOne ){
+ ++it;
+ if( it==d_ceTableaux[x].end() ){
+ var = Node::null();
+ }else{
+ var = it->first;
+ }
+ }
+ //otherwise, try one that divides all ground term coefficients? DO_THIS
+ }
+ if( !var.isNull() ){
+ Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
+ doInstantiation( f, d_tableaux_term[x], x, m, var );
+ }else{
+ Debug("quant-arith-simplex") << "Could not find var." << std::endl;
+ }
+ ////choose a new variable based on alternation strategy
+ //int index = d_counter%(int)d_th->d_ceTableaux[x].size();
+ //Node var;
+ //for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){
+ // if( index==0 ){
+ // var = it->first;
+ // break;
+ // }
+ // index--;
+ //}
+ //d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, &m, var );
+ }
+ }
+ }
+ return STATUS_UNKNOWN;
+}
+
+
+void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t ){
+ if( n.getKind()==MULT ){
+ if( n[1].hasAttribute(InstConstantAttribute()) ){
+ f = n[1].getAttribute(InstConstantAttribute());
+ if( n[1].getKind()==INST_CONSTANT ){
+ d_ceTableaux[x][ n[1] ] = n[0];
+ }else{
+ d_tableaux_ce_term[x][ n[1] ] = n[0];
+ }
+ }else{
+ d_tableaux[x][ n[1] ] = n[0];
+ t << n;
+ }
+ }else{
+ if( n.hasAttribute(InstConstantAttribute()) ){
+ f = n.getAttribute(InstConstantAttribute());
+ if( n.getKind()==INST_CONSTANT ){
+ d_ceTableaux[x][ n ] = Node::null();
+ }else{
+ d_tableaux_ce_term[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );
+ }
+ }else{
+ d_tableaux[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );
+ t << n;
+ }
+ }
+}
+
+void InstStrategySimplex::debugPrint( const char* c ){
+ ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap();
+ for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){
+ ArithVar x = (*it).first;
+ Node n = (*it).second;
+ //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){
+ Debug(c) << x << " : " << n << ", bounds = ";
+ if( d_th->d_partialModel.hasLowerBound( x ) ){
+ Debug(c) << d_th->d_partialModel.getLowerBound( x );
+ }else{
+ Debug(c) << "-infty";
+ }
+ Debug(c) << " <= ";
+ Debug(c) << d_th->d_partialModel.getAssignment( x );
+ Debug(c) << " <= ";
+ if( d_th->d_partialModel.hasUpperBound( x ) ){
+ Debug(c) << d_th->d_partialModel.getUpperBound( x );
+ }else{
+ Debug(c) << "+infty";
+ }
+ Debug(c) << std::endl;
+ //Debug(c) << " Term = " << d_tableaux_term[x] << std::endl;
+ //Debug(c) << " ";
+ //for( std::map< Node, Node >::iterator it2 = d_tableaux[x].begin(); it2 != d_tableaux[x].end(); ++it2 ){
+ // Debug(c) << "( " << it2->first << ", " << it2->second << " ) ";
+ //}
+ //for( std::map< Node, Node >::iterator it2 = d_ceTableaux[x].begin(); it2 != d_ceTableaux[x].end(); ++it2 ){
+ // Debug(c) << "(CE)( " << it2->first << ", " << it2->second << " ) ";
+ //}
+ //for( std::map< Node, Node >::iterator it2 = d_tableaux_ce_term[x].begin(); it2 != d_tableaux_ce_term[x].end(); ++it2 ){
+ // Debug(c) << "(CE-term)( " << it2->first << ", " << it2->second << " ) ";
+ //}
+ //Debug(c) << std::endl;
+ //}
+ }
+ Debug(c) << std::endl;
+
+ for( int q=0; q<d_quantEngine->getNumQuantifiers(); q++ ){
+ Node f = d_quantEngine->getQuantifier( q );
+ Debug(c) << f << std::endl;
+ Debug(c) << " Inst constants: ";
+ for( int i=0; i<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
+ if( i>0 ){
+ Debug( c ) << ", ";
+ }
+ Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
+ }
+ Debug(c) << std::endl;
+ Debug(c) << " Instantiation rows: ";
+ for( int i=0; i<(int)d_instRows[f].size(); i++ ){
+ if( i>0 ){
+ Debug(c) << ", ";
+ }
+ Debug(c) << d_instRows[f][i];
+ }
+ Debug(c) << std::endl;
+ }
+}
+
+//say instantiation row x for quantifier f is coeff*var + A*t[e] + term = beta,
+// where var is an instantiation constant from f,
+// t[e] is a vector of terms containing instantiation constants from f,
+// and term is a ground term (c1*t1 + ... + cn*tn).
+// We construct the term ( beta - term )/coeff to use as an instantiation for var.
+bool InstStrategySimplex::doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var ){
+ //first try +delta
+ if( doInstantiation2( f, term, x, m, var ) ){
+ ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith);
+ return true;
+ }else{
+#ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA
+ //otherwise try -delta
+ if( doInstantiation2( f, term, x, m, var, true ) ){
+ ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith_minus);
+ return true;
+ }else{
+ return false;
+ }
+#else
+ return false;
+#endif
+ }
+}
+
+bool InstStrategySimplex::doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){
+ // make term ( beta - term )/coeff
+ Node beta = getTableauxValue( x, minus_delta );
+ Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term );
+ if( !d_ceTableaux[x][var].isNull() ){
+ if( var.getType().isInteger() ){
+ Assert( d_ceTableaux[x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) );
+ instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[x][var], instVal );
+ }else{
+ Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[x][var].getConst<Rational>() );
+ instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal );
+ }
+ }
+ instVal = Rewriter::rewrite( instVal );
+ //use as instantiation value for var
+ m.set(var, instVal);
+ Debug("quant-arith") << "Add instantiation " << m << std::endl;
+ return d_quantEngine->addInstantiation( f, m );
+}
+
+Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){
+ if( d_th->d_arithvarNodeMap.hasArithVar(n) ){
+ ArithVar v = d_th->d_arithvarNodeMap.asArithVar( n );
+ return getTableauxValue( v, minus_delta );
+ }else{
+ return NodeManager::currentNM()->mkConst( Rational(0) );
+ }
+}
+
+Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){
+ const Rational& delta = d_th->d_partialModel.getDelta();
+ DeltaRational drv = d_th->d_partialModel.getAssignment( v );
+ Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta );
+ return mkRationalNode(qmodel);
+}
+
+
+InstStrategyDatatypesValue::InstStrategyDatatypesValue( TheoryDatatypes* th, QuantifiersEngine* qe ) :
+ InstStrategy( qe ), d_th( th ){
+
+}
+
+bool InstStrategyDatatypesValue::calculateShouldProcess( Node f ){
+ //DO_THIS
+ return false;
+}
+
+void InstStrategyDatatypesValue::processResetInstantiationRound( Theory::Effort effort ){
+
+}
+
+int InstStrategyDatatypesValue::process( Node f, Theory::Effort effort, int e ){
+ Debug("quant-datatypes") << "Datatypes: Try to solve (" << e << ") for " << f << "... " << std::endl;
+ if( e<2 ){
+ return InstStrategy::STATUS_UNFINISHED;
+ }else if( e==2 ){
+ InstMatch m;
+ for( int j = 0; j<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
+ Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
+ if( i.getType().isDatatype() ){
+ Node n = getValueFor( i );
+ Debug("quant-datatypes-debug") << "Value for " << i << " is " << n << std::endl;
+ m.set(i,n);
+ }
+ }
+ //d_quantEngine->addInstantiation( f, m );
+ }
+ return InstStrategy::STATUS_UNKNOWN;
+}
+
+Node InstStrategyDatatypesValue::getValueFor( Node n ){
+ //simply get the ground value for n in the current model, if it exists,
+ // or return an arbitrary ground term otherwise
+ if( !n.hasAttribute(InstConstantAttribute()) ){
+ return n;
+ }else{
+ return n;
+ }
+ /* FIXME
+
+ Debug("quant-datatypes-debug") << "get value for " << n << std::endl;
+ if( !n.hasAttribute(InstConstantAttribute()) ){
+ return n;
+ }else{
+ Assert( n.getType().isDatatype() );
+ //check if in equivalence class with ground term
+ Node rep = getRepresentative( n );
+ Debug("quant-datatypes-debug") << "Rep is " << rep << std::endl;
+ if( !rep.hasAttribute(InstConstantAttribute()) ){
+ return rep;
+ }else{
+ if( !n.getType().isDatatype() ){
+ return n.getType().mkGroundTerm();
+ }else{
+ if( n.getKind()==APPLY_CONSTRUCTOR ){
+ std::vector< Node > children;
+ children.push_back( n.getOperator() );
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ children.push_back( getValueFor( n[i] ) );
+ }
+ return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
+ }else{
+ const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();
+ TheoryDatatypes::EqLists* labels = &((TheoryDatatypes*)d_th)->d_labels;
+ //otherwise, use which constructor the inst constant is current chosen to be
+ if( labels->find( n )!=labels->end() ){
+ TheoryDatatypes::EqList* lbl = (*labels->find( n )).second;
+ int tIndex = -1;
+ if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind()==APPLY_TESTER ){
+ Debug("quant-datatypes-debug") << n << " tester is " << (*lbl)[ lbl->size()-1 ] << std::endl;
+ tIndex = Datatype::indexOf((*lbl)[ lbl->size()-1 ].getOperator().toExpr());
+ }else{
+ Debug("quant-datatypes-debug") << "find possible tester choice" << std::endl;
+ //must find a possible choice
+ vector< bool > possibleCons;
+ possibleCons.resize( dt.getNumConstructors(), true );
+ for( TheoryDatatypes::EqList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ) {
+ Node leqn = (*j);
+ possibleCons[ Datatype::indexOf( leqn[0].getOperator().toExpr() ) ] = false;
+ }
+ for( unsigned int j=0; j<possibleCons.size(); j++ ) {
+ if( possibleCons[j] ){
+ tIndex = j;
+ break;
+ }
+ }
+ }
+ Assert( tIndex!=-1 );
+ Node cons = Node::fromExpr( dt[ tIndex ].getConstructor() );
+ Debug("quant-datatypes-debug") << n << " cons is " << cons << std::endl;
+ std::vector< Node > children;
+ children.push_back( cons );
+ for( int i=0; i<(int)dt[ tIndex ].getNumArgs(); i++ ) {
+ Node sn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[tIndex][i].getSelector() ), n );
+ if( n.hasAttribute(InstConstantAttribute()) ){
+ InstConstantAttribute ica;
+ sn.setAttribute(ica,n.getAttribute(InstConstantAttribute()) );
+ }
+ Node snn = getValueFor( sn );
+ children.push_back( snn );
+ }
+ return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
+ }else{
+ return n.getType().mkGroundTerm();
+ }
+ }
+ }
+ }
+ }
+ */
+}
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
new file mode 100755
index 000000000..3ee423fe7
--- /dev/null
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -0,0 +1,110 @@
+/********************* */
+/*! \file inst_strategy_cbqi.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief instantiator_arith_instantiator
+ **/
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__INST_STRATEGT_CBQI_H
+#define __CVC4__INST_STRATEGT_CBQI_H
+
+#include "theory/quantifiers/instantiation_engine.h"
+#include "theory/arith/arithvar_node_map.h"
+
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace theory {
+
+namespace arith {
+ class TheoryArith;
+}
+
+namespace datatypes {
+ class TheoryDatatypes;
+}
+
+namespace quantifiers {
+
+
+class InstStrategySimplex : public InstStrategy{
+protected:
+ /** calculate if we should process this quantifier */
+ bool calculateShouldProcess( Node f );
+private:
+ /** reference to theory arithmetic */
+ arith::TheoryArith* d_th;
+ /** delta */
+ std::map< TypeNode, Node > d_deltas;
+ /** for each quantifier, simplex rows */
+ std::map< Node, std::vector< arith::ArithVar > > d_instRows;
+ /** tableaux */
+ std::map< arith::ArithVar, Node > d_tableaux_term;
+ std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux_ce_term;
+ std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux;
+ /** ce tableaux */
+ std::map< arith::ArithVar, std::map< Node, Node > > d_ceTableaux;
+ /** get value */
+ Node getTableauxValue( Node n, bool minus_delta = false );
+ Node getTableauxValue( arith::ArithVar v, bool minus_delta = false );
+ /** do instantiation */
+ bool doInstantiation( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var );
+ bool doInstantiation2( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var, bool minus_delta = false );
+ /** add term to row */
+ void addTermToRow( arith::ArithVar x, Node n, Node& f, NodeBuilder<>& t );
+ /** print debug */
+ void debugPrint( const char* c );
+private:
+ /** */
+ int d_counter;
+ /** negative one */
+ Node d_negOne;
+ /** process functions */
+ void processResetInstantiationRound( Theory::Effort effort );
+ int process( Node f, Theory::Effort effort, int e );
+public:
+ InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie );
+ ~InstStrategySimplex(){}
+ /** identify */
+ std::string identify() const { return std::string("Simplex"); }
+};
+
+
+class InstStrategyDatatypesValue : public InstStrategy
+{
+protected:
+ /** calculate if we should process this quantifier */
+ bool calculateShouldProcess( Node f );
+private:
+ /** reference to theory datatypes */
+ datatypes::TheoryDatatypes* d_th;
+ /** get value function */
+ Node getValueFor( Node n );
+public:
+ //constructor
+ InstStrategyDatatypesValue( datatypes::TheoryDatatypes* th, QuantifiersEngine* qe );
+ ~InstStrategyDatatypesValue(){}
+ /** reset instantiation */
+ void processResetInstantiationRound( Theory::Effort effort );
+ /** process method, returns a status */
+ int process( Node f, Theory::Effort effort, int e );
+ /** identify */
+ std::string identify() const { return std::string("InstStrategyDatatypesValue"); }
+
+};/* class InstStrategy */
+
+}
+}
+}
+
+#endif \ No newline at end of file
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
new file mode 100755
index 000000000..48af334ff
--- /dev/null
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -0,0 +1,379 @@
+/********************* */
+/*! \file inst_strategy_e_matching.cpp
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): bobot
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of e matching instantiation strategies
+ **/
+
+#include "theory/quantifiers/inst_strategy_e_matching.h"
+
+#include "theory/theory_engine.h"
+#include "theory/quantifiers/options.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/inst_match_generator.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;
+
+#define USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER
+//#define MULTI_TRIGGER_FULL_EFFORT_HALF
+#define MULTI_MULTI_TRIGGERS
+
+struct sortQuantifiersForSymbol {
+ QuantifiersEngine* d_qe;
+ bool operator() (Node i, Node j) {
+ int nqfsi = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( i.getOperator() );
+ int nqfsj = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( j.getOperator() );
+ if( nqfsi<nqfsj ){
+ return true;
+ }else if( nqfsi>nqfsj ){
+ return false;
+ }else{
+ return false;
+ }
+ }
+};
+
+void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){
+ //reset triggers
+ for( std::map< Node, std::vector< Trigger* > >::iterator it = d_user_gen.begin(); it != d_user_gen.end(); ++it ){
+ for( int i=0; i<(int)it->second.size(); i++ ){
+ it->second[i]->resetInstantiationRound();
+ it->second[i]->reset( Node::null() );
+ }
+ }
+}
+
+int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
+ if( e==0 ){
+ return STATUS_UNFINISHED;
+ }else if( e==1 ){
+ d_counter[f]++;
+ Debug("quant-uf-strategy") << "Try user-provided patterns..." << std::endl;
+ //Notice() << "Try user-provided patterns..." << std::endl;
+ for( int i=0; i<(int)d_user_gen[f].size(); i++ ){
+ bool processTrigger = true;
+ if( effort!=Theory::EFFORT_LAST_CALL && d_user_gen[f][i]->isMultiTrigger() ){
+//#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF
+// processTrigger = d_counter[f]%2==0;
+//#endif
+ }
+ if( processTrigger ){
+ //if( d_user_gen[f][i]->isMultiTrigger() )
+ //Notice() << " Process (user) " << (*d_user_gen[f][i]) << " for " << f << "..." << std::endl;
+ InstMatch baseMatch;
+ int numInst = d_user_gen[f][i]->addInstantiations( baseMatch );
+ //if( d_user_gen[f][i]->isMultiTrigger() )
+ //Notice() << " Done, numInst = " << numInst << "." << std::endl;
+ d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_user_patterns += numInst;
+ if( d_user_gen[f][i]->isMultiTrigger() ){
+ d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
+ }
+ //d_quantEngine->d_hasInstantiated[f] = true;
+ }
+ }
+ Debug("quant-uf-strategy") << "done." << std::endl;
+ //Notice() << "done" << std::endl;
+ }
+ return STATUS_UNKNOWN;
+}
+
+void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){
+ //add to generators
+ std::vector< Node > nodes;
+ for( int i=0; i<(int)pat.getNumChildren(); i++ ){
+ nodes.push_back( pat[i] );
+ }
+ if( Trigger::isUsableTrigger( nodes, f ) ){
+ //extend to literal matching
+ d_quantEngine->getPhaseReqTerms( f, nodes );
+ //check match option
+ int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;
+ d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW,
+ options::smartTriggers() ) );
+ }
+}
+/*
+InstStrategyUserPatterns::Statistics::Statistics():
+ d_instantiations("InstStrategyUserPatterns::Instantiations", 0)
+{
+ StatisticsRegistry::registerStat(&d_instantiations);
+}
+
+InstStrategyUserPatterns::Statistics::~Statistics(){
+ StatisticsRegistry::unregisterStat(&d_instantiations);
+}
+*/
+
+void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){
+ //reset triggers
+ for( std::map< Node, std::map< Trigger*, bool > >::iterator it = d_auto_gen_trigger.begin(); it != d_auto_gen_trigger.end(); ++it ){
+ for( std::map< Trigger*, bool >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){
+ itt->first->resetInstantiationRound();
+ itt->first->reset( Node::null() );
+ }
+ }
+}
+
+int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){
+ int peffort = f.getNumChildren()==3 ? 2 : 1;
+ //int peffort = f.getNumChildren()==3 ? 2 : 1;
+ //int peffort = 1;
+ if( e<peffort ){
+ return STATUS_UNFINISHED;
+ }else{
+ bool gen = false;
+ if( e==peffort ){
+ if( d_counter.find( f )==d_counter.end() ){
+ d_counter[f] = 0;
+ gen = true;
+ }else{
+ d_counter[f]++;
+ gen = d_regenerate && d_counter[f]%d_regenerate_frequency==0;
+ }
+ }else{
+ gen = true;
+ }
+ if( gen ){
+ generateTriggers( f );
+ }
+ Debug("quant-uf-strategy") << "Try auto-generated triggers... " << d_tr_strategy << " " << e << std::endl;
+ //Notice() << "Try auto-generated triggers..." << std::endl;
+ for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[f].begin(); itt != d_auto_gen_trigger[f].end(); ++itt ){
+ Trigger* tr = itt->first;
+ if( tr ){
+ bool processTrigger = itt->second;
+ if( effort!=Theory::EFFORT_LAST_CALL && tr->isMultiTrigger() ){
+#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF
+ processTrigger = d_counter[f]%2==0;
+#endif
+ }
+ if( processTrigger ){
+ //if( tr->isMultiTrigger() )
+ Debug("quant-uf-strategy-auto-gen-triggers") << " Process " << (*tr) << "..." << std::endl;
+ InstMatch baseMatch;
+ int numInst = tr->addInstantiations( baseMatch );
+ //if( tr->isMultiTrigger() )
+ Debug("quant-uf-strategy-auto-gen-triggers") << " Done, numInst = " << numInst << "." << std::endl;
+ if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){
+ d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen_min += numInst;
+ }else{
+ d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen += numInst;
+ }
+ if( tr->isMultiTrigger() ){
+ d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
+ }
+ //d_quantEngine->d_hasInstantiated[f] = true;
+ }
+ }
+ }
+ Debug("quant-uf-strategy") << "done." << std::endl;
+ //Notice() << "done" << std::endl;
+ }
+ return STATUS_UNKNOWN;
+}
+
+void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
+ Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
+ if( d_patTerms[0].find( f )==d_patTerms[0].end() ){
+ //determine all possible pattern terms based on trigger term selection strategy d_tr_strategy
+ d_patTerms[0][f].clear();
+ d_patTerms[1][f].clear();
+ std::vector< Node > patTermsF;
+ Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, true );
+ Debug("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << std::endl;
+ Debug("auto-gen-trigger") << " ";
+ for( int i=0; i<(int)patTermsF.size(); i++ ){
+ Debug("auto-gen-trigger") << patTermsF[i] << " ";
+ }
+ Debug("auto-gen-trigger") << std::endl;
+ //extend to literal matching (if applicable)
+ d_quantEngine->getPhaseReqTerms( f, patTermsF );
+ //sort into single/multi triggers
+ std::map< Node, std::vector< Node > > varContains;
+ d_quantEngine->getTermDatabase()->getVarContains( f, patTermsF, varContains );
+ for( std::map< Node, std::vector< Node > >::iterator it = varContains.begin(); it != varContains.end(); ++it ){
+ if( it->second.size()==f[0].getNumChildren() ){
+ d_patTerms[0][f].push_back( it->first );
+ d_is_single_trigger[ it->first ] = true;
+ }else{
+ d_patTerms[1][f].push_back( it->first );
+ d_is_single_trigger[ it->first ] = false;
+ }
+ }
+ d_made_multi_trigger[f] = false;
+ Debug("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl;
+ Debug("auto-gen-trigger") << " ";
+ for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){
+ Debug("auto-gen-trigger") << d_patTerms[0][f][i] << " ";
+ }
+ Debug("auto-gen-trigger") << std::endl;
+ Debug("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl;
+ Debug("auto-gen-trigger") << " ";
+ for( int i=0; i<(int)d_patTerms[1][f].size(); i++ ){
+ Debug("auto-gen-trigger") << d_patTerms[1][f][i] << " ";
+ }
+ Debug("auto-gen-trigger") << std::endl;
+ }
+
+ //populate candidate pattern term vector for the current trigger
+ std::vector< Node > patTerms;
+#ifdef USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER
+ //try to add single triggers first
+ for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){
+ if( !d_single_trigger_gen[d_patTerms[0][f][i]] ){
+ patTerms.push_back( d_patTerms[0][f][i] );
+ }
+ }
+ //if no single triggers exist, add multi trigger terms
+ if( patTerms.empty() ){
+ patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );
+ }
+#else
+ patTerms.insert( patTerms.begin(), d_patTerms[0][f].begin(), d_patTerms[0][f].end() );
+ patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );
+#endif
+
+ if( !patTerms.empty() ){
+ Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
+ //sort terms based on relevance
+ if( d_rlv_strategy==RELEVANCE_DEFAULT ){
+ sortQuantifiersForSymbol sqfs;
+ sqfs.d_qe = d_quantEngine;
+ //sort based on # occurrences (this will cause Trigger to select rarer symbols)
+ std::sort( patTerms.begin(), patTerms.end(), sqfs );
+ Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;
+ for( int i=0; i<(int)patTerms.size(); i++ ){
+ Debug("relevant-trigger") << " " << patTerms[i] << " (";
+ Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;
+ }
+ //Notice() << "Terms based on relevance: " << std::endl;
+ //for( int i=0; i<(int)patTerms.size(); i++ ){
+ // Notice() << " " << patTerms[i] << " (";
+ // Notice() << d_quantEngine->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;
+ //}
+ }
+ //now, generate the trigger...
+ int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;
+ Trigger* tr = NULL;
+ if( d_is_single_trigger[ patTerms[0] ] ){
+ tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL,
+ options::smartTriggers() );
+ d_single_trigger_gen[ patTerms[0] ] = true;
+ }else{
+ //if we are re-generating triggers, shuffle based on some method
+ if( d_made_multi_trigger[f] ){
+#ifndef MULTI_MULTI_TRIGGERS
+ return;
+#endif
+ std::random_shuffle( patTerms.begin(), patTerms.end() ); //shuffle randomly
+ }else{
+ d_made_multi_trigger[f] = true;
+ }
+ //will possibly want to get an old trigger
+ tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD,
+ options::smartTriggers() );
+ }
+ if( tr ){
+ if( tr->isMultiTrigger() ){
+ //disable all other multi triggers
+ for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[f].begin(); it != d_auto_gen_trigger[f].end(); ++it ){
+ if( it->first->isMultiTrigger() ){
+ d_auto_gen_trigger[f][ it->first ] = false;
+ }
+ }
+ }
+ //making it during an instantiation round, so must reset
+ if( d_auto_gen_trigger[f].find( tr )==d_auto_gen_trigger[f].end() ){
+ tr->resetInstantiationRound();
+ tr->reset( Node::null() );
+ }
+ d_auto_gen_trigger[f][tr] = true;
+ //if we are generating additional triggers...
+ if( d_generate_additional && d_is_single_trigger[ patTerms[0] ] ){
+ int index = 0;
+ if( index<(int)patTerms.size() ){
+ //Notice() << "check add additional" << std::endl;
+ //check if similar patterns exist, and if so, add them additionally
+ int nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() );
+ index++;
+ bool success = true;
+ while( success && index<(int)patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){
+ success = false;
+ if( d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){
+ d_single_trigger_gen[ patTerms[index] ] = true;
+ Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL,
+ options::smartTriggers() );
+ if( tr2 ){
+ //Notice() << "Add additional trigger " << patTerms[index] << std::endl;
+ tr2->resetInstantiationRound();
+ tr2->reset( Node::null() );
+ d_auto_gen_trigger[f][tr2] = true;
+ }
+ success = true;
+ }
+ index++;
+ }
+ //Notice() << "done check add additional" << std::endl;
+ }
+ }
+ }
+ }
+}
+/*
+InstStrategyAutoGenTriggers::Statistics::Statistics():
+ d_instantiations("InstStrategyAutoGenTriggers::Instantiations", 0),
+ d_instantiations_min("InstStrategyAutoGenTriggers::Instantiations_min", 0)
+{
+ StatisticsRegistry::registerStat(&d_instantiations);
+ StatisticsRegistry::registerStat(&d_instantiations_min);
+}
+
+InstStrategyAutoGenTriggers::Statistics::~Statistics(){
+ StatisticsRegistry::unregisterStat(&d_instantiations);
+ StatisticsRegistry::unregisterStat(&d_instantiations_min);
+}
+*/
+
+void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){
+}
+
+int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
+ if( e<5 ){
+ return STATUS_UNFINISHED;
+ }else{
+ if( d_guessed.find( f )==d_guessed.end() ){
+ d_guessed[f] = true;
+ Debug("quant-uf-alg") << "Add guessed instantiation" << std::endl;
+ InstMatch m;
+ if( d_quantEngine->addInstantiation( f, m ) ){
+ ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
+ //d_quantEngine->d_hasInstantiated[f] = true;
+ }
+ }
+ return STATUS_UNKNOWN;
+ }
+}
+/*
+InstStrategyFreeVariable::Statistics::Statistics():
+ d_instantiations("InstStrategyGuess::Instantiations", 0)
+{
+ StatisticsRegistry::registerStat(&d_instantiations);
+}
+
+InstStrategyFreeVariable::Statistics::~Statistics(){
+ StatisticsRegistry::unregisterStat(&d_instantiations);
+}
+*/
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
new file mode 100755
index 000000000..ea22486a6
--- /dev/null
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -0,0 +1,132 @@
+/********************* */
+/*! \file inst_strategy_e_matching.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): bobot, mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief E matching instantiation strategies
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__INST_STRATEGY_E_MATCHING_H
+#define __CVC4__INST_STRATEGY_E_MATCHING_H
+
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/trigger.h"
+
+#include "context/context.h"
+#include "context/context_mm.h"
+
+#include "util/statistics_registry.h"
+#include "theory/quantifiers/instantiation_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+//instantiation strategies
+
+class InstStrategyUserPatterns : public InstStrategy{
+private:
+ /** explicitly provided patterns */
+ std::map< Node, std::vector< inst::Trigger* > > d_user_gen;
+ /** counter for quantifiers */
+ std::map< Node, int > d_counter;
+ /** process functions */
+ void processResetInstantiationRound( Theory::Effort effort );
+ int process( Node f, Theory::Effort effort, int e );
+public:
+ InstStrategyUserPatterns( QuantifiersEngine* ie ) :
+ InstStrategy( ie ){}
+ ~InstStrategyUserPatterns(){}
+public:
+ /** add pattern */
+ void addUserPattern( Node f, Node pat );
+ /** get num patterns */
+ int getNumUserGenerators( Node f ) { return (int)d_user_gen[f].size(); }
+ /** get user pattern */
+ inst::Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; }
+ /** identify */
+ std::string identify() const { return std::string("UserPatterns"); }
+};/* class InstStrategyUserPatterns */
+
+class InstStrategyAutoGenTriggers : public InstStrategy{
+public:
+ enum {
+ RELEVANCE_NONE,
+ RELEVANCE_DEFAULT,
+ };
+private:
+ /** trigger generation strategy */
+ int d_tr_strategy;
+ /** relevance strategy */
+ int d_rlv_strategy;
+ /** regeneration */
+ bool d_regenerate;
+ int d_regenerate_frequency;
+ /** generate additional triggers */
+ bool d_generate_additional;
+ /** triggers for each quantifier */
+ std::map< Node, std::map< inst::Trigger*, bool > > d_auto_gen_trigger;
+ std::map< Node, int > d_counter;
+ /** single, multi triggers for each quantifier */
+ std::map< Node, std::vector< Node > > d_patTerms[2];
+ std::map< Node, bool > d_is_single_trigger;
+ std::map< Node, bool > d_single_trigger_gen;
+ std::map< Node, bool > d_made_multi_trigger;
+private:
+ /** process functions */
+ void processResetInstantiationRound( Theory::Effort effort );
+ int process( Node f, Theory::Effort effort, int e );
+ /** generate triggers */
+ void generateTriggers( Node f );
+public:
+ InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt, int rstrt, int rgfr = -1 ) :
+ InstStrategy( qe ), d_tr_strategy( tstrt ), d_rlv_strategy( rstrt ), d_generate_additional( false ){
+ setRegenerateFrequency( rgfr );
+ }
+ ~InstStrategyAutoGenTriggers(){}
+public:
+ /** get auto-generated trigger */
+ inst::Trigger* getAutoGenTrigger( Node f );
+ /** identify */
+ std::string identify() const { return std::string("AutoGenTriggers"); }
+ /** set regenerate frequency, if fr<0, turn off regenerate */
+ void setRegenerateFrequency( int fr ){
+ if( fr<0 ){
+ d_regenerate = false;
+ }else{
+ d_regenerate_frequency = fr;
+ d_regenerate = true;
+ }
+ }
+ /** set generate additional */
+ void setGenerateAdditional( bool val ) { d_generate_additional = val; }
+};/* class InstStrategyAutoGenTriggers */
+
+class InstStrategyFreeVariable : public InstStrategy{
+private:
+ /** guessed instantiations */
+ std::map< Node, bool > d_guessed;
+ /** process functions */
+ void processResetInstantiationRound( Theory::Effort effort );
+ int process( Node f, Theory::Effort effort, int e );
+public:
+ InstStrategyFreeVariable( QuantifiersEngine* qe ) :
+ InstStrategy( qe ){}
+ ~InstStrategyFreeVariable(){}
+ /** identify */
+ std::string identify() const { return std::string("FreeVariable"); }
+};/* class InstStrategyFreeVariable */
+
+}
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 8d935a323..579c53665 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -15,10 +15,12 @@
#include "theory/quantifiers/instantiation_engine.h"
#include "theory/theory_engine.h"
-#include "theory/uf/theory_uf_instantiator.h"
#include "theory/quantifiers/options.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/inst_strategy_e_matching.h"
+#include "theory/quantifiers/inst_strategy_cbqi.h"
+#include "theory/quantifiers/trigger.h"
using namespace std;
using namespace CVC4;
@@ -26,12 +28,49 @@ using namespace CVC4::kind;
using namespace CVC4::context;
using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
+using namespace CVC4::theory::inst;
InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) :
QuantifiersModule( qe ), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ), d_performCheck( false ){
}
+void InstantiationEngine::finishInit(){
+ //for UF terms
+ if( !options::finiteModelFind() || options::fmfInstEngine() ){
+ //if( options::cbqi() ){
+ // addInstStrategy( new InstStrategyCheckCESolved( this, d_quantEngine ) );
+ //}
+ //these are the instantiation strategies for basic E-matching
+ if( options::userPatternsQuant() ){
+ d_isup = new InstStrategyUserPatterns( d_quantEngine );
+ addInstStrategy( d_isup );
+ }else{
+ d_isup = NULL;
+ }
+ InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL,
+ InstStrategyAutoGenTriggers::RELEVANCE_DEFAULT, 3 );
+ i_ag->setGenerateAdditional( true );
+ addInstStrategy( i_ag );
+ //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) );
+ if( !options::finiteModelFind() ){
+ addInstStrategy( new InstStrategyFreeVariable( d_quantEngine ) );
+ }
+ //d_isup->setPriorityOver( i_ag );
+ //d_isup->setPriorityOver( i_agm );
+ //i_ag->setPriorityOver( i_agm );
+ }
+ //CBQI: FIXME
+ //for arithmetic
+ //if( options::cbqi() ){
+ // addInstStrategy( new InstStrategySimplex( d_quantEngine ) );
+ //}
+ //for datatypes
+ //if( options::cbqi() ){
+ // addInstStrategy( new InstStrategyDatatypesValue( d_quantEngine ) );
+ //}
+}
+
bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
//if counterexample-based quantifier instantiation is active
@@ -68,9 +107,10 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
//reset the quantifiers engine
Debug("inst-engine-ctrl") << "Reset IE" << std::endl;
//reset the instantiators
- for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
- if( d_quantEngine->getInstantiator( i ) ){
- d_quantEngine->getInstantiator( i )->resetInstantiationRound( effort );
+ for( size_t i=0; i<d_instStrategies.size(); ++i ){
+ InstStrategy* is = d_instStrategies[i];
+ if( isActiveStrategy( is ) ){
+ is->processResetInstantiationRound( effort );
}
}
//iterate over an internal effort level e
@@ -90,11 +130,12 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
//int e_use = d_quantEngine->getRelevance( f )==-1 ? e - 1 : e;
int e_use = e;
if( e_use>=0 ){
- //use each theory instantiator to instantiate f
- for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
- if( d_quantEngine->getInstantiator( i ) ){
- Debug("inst-engine-debug") << "Do " << d_quantEngine->getInstantiator( i )->identify() << " " << e_use << std::endl;
- int quantStatus = d_quantEngine->getInstantiator( i )->doInstantiation( f, effort, e_use );
+ //check each instantiation strategy
+ for( size_t i=0; i<d_instStrategies.size(); ++i ){
+ InstStrategy* is = d_instStrategies[i];
+ if( isActiveStrategy( is ) && is->shouldProcess( f ) ){
+ Debug("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
+ int quantStatus = is->process( f, effort, e_use );
Debug("inst-engine-debug") << " -> status is " << quantStatus << std::endl;
InstStrategy::updateStatus( d_inst_round_status, quantStatus );
}
@@ -112,13 +153,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
Debug("inst-engine") << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl;
//Notice() << "All instantiators finished, # added lemmas = " << (int)d_lemmas_waiting.size() << std::endl;
if( !d_quantEngine->hasAddedLemma() ){
- Debug("inst-engine-stuck") << "No instantiations produced at this state: " << std::endl;
- for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
- if( d_quantEngine->getInstantiator( i ) ){
- d_quantEngine->getInstantiator( i )->debugPrint("inst-engine-stuck");
- Debug("inst-engine-stuck") << std::endl;
- }
- }
+ Debug("inst-engine-stuck") << "No instantiations produced at this state." << std::endl;
Debug("inst-engine-ctrl") << "---Fail." << std::endl;
return false;
}else{
@@ -238,9 +273,6 @@ void InstantiationEngine::registerQuantifier( Node f ){
Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
if( !doCbqi( f ) ){
d_quantEngine->addTermToDatabase( ceBody, true );
- //need to tell which instantiators will be responsible
- //by default, just chose the UF instantiator
- d_quantEngine->getInstantiator( theory::THEORY_UF )->setQuantifierActive( f );
}
//take into account user patterns
@@ -249,7 +281,7 @@ void InstantiationEngine::registerQuantifier( Node f ){
//add patterns
for( int i=0; i<(int)subsPat.getNumChildren(); i++ ){
//Notice() << "Add pattern " << subsPat[i] << " for " << f << std::endl;
- ((uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( theory::THEORY_UF ))->addUserPattern( f, subsPat[i] );
+ addUserPattern( f, subsPat[i] );
}
}
}
@@ -359,4 +391,38 @@ Node InstantiationEngine::getNextDecisionRequest(){
}
}
return Node::null();
-} \ No newline at end of file
+}
+
+void InstantiationEngine::addUserPattern( Node f, Node pat ){
+ if( d_isup ){
+ d_isup->addUserPattern( f, pat );
+ }
+}
+
+InstantiationEngine::Statistics::Statistics():
+ d_instantiations_user_patterns("InstantiationEngine::Instantiations_User_Patterns", 0),
+ d_instantiations_auto_gen("InstantiationEngine::Instantiations_Auto_Gen", 0),
+ d_instantiations_auto_gen_min("InstantiationEngine::Instantiations_Auto_Gen_Min", 0),
+ d_instantiations_guess("InstantiationEngine::Instantiations_Guess", 0),
+ d_instantiations_cbqi_arith("InstantiationEngine::Instantiations_Cbqi_Arith", 0),
+ d_instantiations_cbqi_arith_minus("InstantiationEngine::Instantiations_Cbqi_Arith_Minus", 0),
+ d_instantiations_cbqi_datatypes("InstantiationEngine::Instantiations_Cbqi_Datatypes", 0)
+{
+ StatisticsRegistry::registerStat(&d_instantiations_user_patterns);
+ StatisticsRegistry::registerStat(&d_instantiations_auto_gen);
+ StatisticsRegistry::registerStat(&d_instantiations_auto_gen_min);
+ StatisticsRegistry::registerStat(&d_instantiations_guess);
+ StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith);
+ StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith_minus);
+ StatisticsRegistry::registerStat(&d_instantiations_cbqi_datatypes);
+}
+
+InstantiationEngine::Statistics::~Statistics(){
+ StatisticsRegistry::unregisterStat(&d_instantiations_user_patterns);
+ StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen);
+ StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen_min);
+ StatisticsRegistry::unregisterStat(&d_instantiations_guess);
+ StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith);
+ StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith_minus);
+ StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_datatypes);
+}
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index b3bbbce4a..a7ae1ae8e 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -24,9 +24,71 @@ namespace CVC4 {
namespace theory {
namespace quantifiers {
+class InstStrategyUserPatterns;
+
+/** instantiation strategy class */
+class InstStrategy {
+public:
+ enum Status {
+ STATUS_UNFINISHED,
+ STATUS_UNKNOWN,
+ STATUS_SAT,
+ };/* enum Status */
+protected:
+ /** reference to the instantiation engine */
+ QuantifiersEngine* d_quantEngine;
+ /** should process a quantifier */
+ std::map< Node, bool > d_quantActive;
+ /** calculate should process */
+ virtual bool calculateShouldProcess( Node f ) { return true; }
+public:
+ InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
+ virtual ~InstStrategy(){}
+
+ /** should process quantified formula f? */
+ bool shouldProcess( Node f ) {
+ if( d_quantActive.find( f )==d_quantActive.end() ){
+ d_quantActive[f] = calculateShouldProcess( f );
+ }
+ return d_quantActive[f];
+ }
+ /** reset instantiation */
+ virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
+ /** process method, returns a status */
+ virtual int process( Node f, Theory::Effort effort, int e ) = 0;
+ /** update status */
+ static void updateStatus( int& currStatus, int addStatus ){
+ if( addStatus==STATUS_UNFINISHED ){
+ currStatus = STATUS_UNFINISHED;
+ }else if( addStatus==STATUS_UNKNOWN ){
+ if( currStatus==STATUS_SAT ){
+ currStatus = STATUS_UNKNOWN;
+ }
+ }
+ }
+ /** identify */
+ virtual std::string identify() const { return std::string("Unknown"); }
+};/* class InstStrategy */
+
class InstantiationEngine : public QuantifiersModule
{
private:
+ /** instantiation strategies */
+ std::vector< InstStrategy* > d_instStrategies;
+ /** instantiation strategies active */
+ std::map< InstStrategy*, bool > d_instStrategyActive;
+ /** user-pattern instantiation strategy */
+ InstStrategyUserPatterns* d_isup;
+ /** is instantiation strategy active */
+ bool isActiveStrategy( InstStrategy* is ) {
+ return d_instStrategyActive.find( is )!=d_instStrategyActive.end() && d_instStrategyActive[is];
+ }
+ /** add inst strategy */
+ void addInstStrategy( InstStrategy* is ){
+ d_instStrategies.push_back( is );
+ d_instStrategyActive[is] = true;
+ }
+private:
typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
/** status of instantiation round (one of InstStrategy::STATUS_*) */
int d_inst_round_status;
@@ -62,6 +124,8 @@ private:
public:
InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete = true );
~InstantiationEngine(){}
+ /** initialize */
+ void finishInit();
bool needsCheck( Theory::Effort e );
void check( Theory::Effort e );
@@ -69,6 +133,23 @@ public:
void assertNode( Node f );
Node explain(TNode n){ return Node::null(); }
Node getNextDecisionRequest();
+ /** add user pattern */
+ void addUserPattern( Node f, Node pat );
+public:
+ /** statistics class */
+ class Statistics {
+ public:
+ IntStat d_instantiations_user_patterns;
+ IntStat d_instantiations_auto_gen;
+ IntStat d_instantiations_auto_gen_min;
+ IntStat d_instantiations_guess;
+ IntStat d_instantiations_cbqi_arith;
+ IntStat d_instantiations_cbqi_arith_minus;
+ IntStat d_instantiations_cbqi_datatypes;
+ Statistics();
+ ~Statistics();
+ };
+ Statistics d_statistics;
};/* class InstantiationEngine */
}/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/instantiator_default.cpp b/src/theory/quantifiers/instantiator_default.cpp
deleted file mode 100644
index def3c9f58..000000000
--- a/src/theory/quantifiers/instantiator_default.cpp
+++ /dev/null
@@ -1,54 +0,0 @@
-/********************* */
-/*! \file instantiator_default.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): bobot, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of instantiator_default class
- **/
-
-#include "theory/quantifiers/instantiator_default.h"
-#include "theory/theory_engine.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-
-InstantiatorDefault::InstantiatorDefault(context::Context* c, QuantifiersEngine* ie, Theory* th) :
- Instantiator( c, ie, th ) {
-}
-
-void InstantiatorDefault::assertNode( Node assertion ){
-}
-
-void InstantiatorDefault::processResetInstantiationRound( Theory::Effort effort ){
-}
-
-int InstantiatorDefault::process( Node f, Theory::Effort effort, int e ){
- /*
- if( e < 4 ){
- return InstStrategy::STATUS_UNFINISHED;
- }else if( e == 4 ){
- Debug("quant-default") << "Process " << f << " : " << std::endl;
- InstMatch m;
- for( int j=0; j<(int)d_quantEngine->getNumInstantiationConstants( f ); j++ ){
- Node i = d_quantEngine->getInstantiationConstant( f, j );
- Debug("quant-default") << "Getting value for " << i << std::endl;
- if( d_quantEngine->getTheoryEngine()->theoryOf( i )==getTheory() ){ //if it belongs to this theory
- Node val = d_th->getValue( i );
- Debug("quant-default") << "Default Instantiate for " << d_th->getId() << ", setting " << i << " = " << val << std::endl;
- m.set( i, val);
- }
- }
- d_quantEngine->addInstantiation( f, m );
- }
- */
- return InstStrategy::STATUS_UNKNOWN;
-}
diff --git a/src/theory/quantifiers/instantiator_default.h b/src/theory/quantifiers/instantiator_default.h
deleted file mode 100644
index d21499ae0..000000000
--- a/src/theory/quantifiers/instantiator_default.h
+++ /dev/null
@@ -1,46 +0,0 @@
-/********************* */
-/*! \file instantiator_default.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief instantiator_default
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATOR_DEFAULT_H
-#define __CVC4__THEORY__QUANTIFIERS__INSTANTIATOR_DEFAULT_H
-
-#include <string>
-#include "theory/quantifiers_engine.h"
-
-namespace CVC4 {
-namespace theory {
-
-class InstantiatorDefault : public Instantiator {
- friend class QuantifiersEngine;
-protected:
- /** reset instantiation round */
- void processResetInstantiationRound(Theory::Effort effort);
- /** process quantifier */
- int process( Node f, Theory::Effort effort, int e );
-public:
- InstantiatorDefault(context::Context* c, QuantifiersEngine* ie, Theory* th);
- ~InstantiatorDefault() { }
- /** check function, assertion is asserted to theory */
- void assertNode( Node assertion );
- /** identify */
- std::string identify() const { return std::string("InstantiatorDefault"); }
-};/* class InstantiatorDefault */
-
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATOR_DEFAULT_H */
diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds
index c81816528..ab0e9d934 100644
--- a/src/theory/quantifiers/kinds
+++ b/src/theory/quantifiers/kinds
@@ -6,7 +6,6 @@
theory THEORY_QUANTIFIERS ::CVC4::theory::quantifiers::TheoryQuantifiers "theory/quantifiers/theory_quantifiers.h"
typechecker "theory/quantifiers/theory_quantifiers_type_rules.h"
-instantiator ::CVC4::theory::quantifiers::InstantiatorTheoryQuantifiers "theory/quantifiers/theory_quantifiers_instantiator.h"
properties check propagate presolve getNextDecisionRequest
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index c7e68acb1..2f44140c2 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -17,7 +17,6 @@
#include "theory/uf/equality_engine.h"
#include "theory/uf/theory_uf.h"
#include "theory/uf/theory_uf_model.h"
-#include "theory/uf/theory_uf_instantiator.h"
#include "theory/uf/theory_uf_strong_solver.h"
#include "theory/arrays/theory_arrays_model.h"
#include "theory/quantifiers/first_order_model.h"
@@ -25,6 +24,7 @@
#include "theory/quantifiers/model_builder.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/inst_gen.h"
+#include "theory/quantifiers/trigger.h"
using namespace std;
using namespace CVC4;
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 456914818..bf6ea11f0 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -17,7 +17,6 @@
#include "theory/uf/equality_engine.h"
#include "theory/uf/theory_uf.h"
#include "theory/uf/theory_uf_strong_solver.h"
-#include "theory/uf/theory_uf_instantiator.h"
#include "theory/quantifiers/options.h"
#include "theory/arrays/theory_arrays_model.h"
#include "theory/quantifiers/first_order_model.h"
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 9a26878b5..d60aa2ef4 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -106,7 +106,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
addedLemmas += d_op_triggers[op][i]->addTerm( n );
}
//Message() << "Terms, added lemmas: " << addedLemmas << std::endl;
- d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel() );
+ d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
}
}
}
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 446c9285e..cfdb30f38 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -22,7 +22,6 @@
#include "theory/quantifiers/model_engine.h"
#include "expr/kind.h"
#include "util/cvc4_assert.h"
-#include "theory/quantifiers/theory_quantifiers_instantiator.h"
#include "theory/quantifiers/options.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/quantifiers_attributes.h"
diff --git a/src/theory/quantifiers/theory_quantifiers_instantiator.cpp b/src/theory/quantifiers/theory_quantifiers_instantiator.cpp
deleted file mode 100644
index eabb4ceda..000000000
--- a/src/theory/quantifiers/theory_quantifiers_instantiator.cpp
+++ /dev/null
@@ -1,73 +0,0 @@
-/********************* */
-/*! \file theory_quantifiers_instantiator.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of theory_quantifiers_instantiator class
- **/
-
-#include "theory/quantifiers/theory_quantifiers_instantiator.h"
-#include "theory/quantifiers/theory_quantifiers.h"
-#include "theory/quantifiers/options.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::quantifiers;
-
-InstantiatorTheoryQuantifiers::InstantiatorTheoryQuantifiers(context::Context* c, QuantifiersEngine* ie, Theory* th) :
-Instantiator( c, ie, th ){
-
-}
-
-void InstantiatorTheoryQuantifiers::assertNode( Node assertion ){
- Debug("quant-quant-assert") << "InstantiatorTheoryQuantifiers::check: " << assertion << std::endl;
- if( options::cbqi() ){
- if( assertion.hasAttribute(InstConstantAttribute()) ){
- Debug("quant-quant-assert") << " -> has constraints from " << assertion.getAttribute(InstConstantAttribute()) << std::endl;
- setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
- }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
- Debug("quant-quant-assert") << " -> has constraints from " << assertion[0].getAttribute(InstConstantAttribute()) << std::endl;
- setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) );
- }
- }
-}
-
-void InstantiatorTheoryQuantifiers::processResetInstantiationRound( Theory::Effort effort ){
-
-}
-
-
-int InstantiatorTheoryQuantifiers::process( Node f, Theory::Effort effort, int e ){
- Debug("quant-quant") << "Quant: Try to solve (" << e << ") for " << f << "... " << std::endl;
- if( e<5 ){
- return InstStrategy::STATUS_UNFINISHED;
- }else if( e==5 ){
- //add random addition
- InstMatch m;
- if( d_quantEngine->addInstantiation( f, m ) ){
- ++(d_statistics.d_instantiations);
- }
- }
- return InstStrategy::STATUS_UNKNOWN;
-}
-
-InstantiatorTheoryQuantifiers::Statistics::Statistics():
- d_instantiations("InstantiatorTheoryQuantifiers::Instantiations_Total", 0)
-{
- StatisticsRegistry::registerStat(&d_instantiations);
-}
-
-InstantiatorTheoryQuantifiers::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_instantiations);
-}
-
diff --git a/src/theory/quantifiers/theory_quantifiers_instantiator.h b/src/theory/quantifiers/theory_quantifiers_instantiator.h
deleted file mode 100644
index 5722c264f..000000000
--- a/src/theory/quantifiers/theory_quantifiers_instantiator.h
+++ /dev/null
@@ -1,58 +0,0 @@
-/********************* */
-/*! \file theory_quantifiers_instantiator.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief instantiator_quantifiers_instantiator
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_INSTANTIATOR_H
-#define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_INSTANTIATOR_H
-
-#include "theory/quantifiers_engine.h"
-
-#include "util/statistics_registry.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class InstantiatorTheoryQuantifiers : public Instantiator{
- friend class QuantifiersEngine;
-public:
- InstantiatorTheoryQuantifiers(context::Context* c, QuantifiersEngine* ie, Theory* th);
- ~InstantiatorTheoryQuantifiers() {}
-
- /** check function, assertion is asserted to theory */
- void assertNode( Node assertion );
- /** identify */
- std::string identify() const { return std::string("InstantiatorTheoryQuantifiers"); }
-private:
- /** reset instantiation */
- void processResetInstantiationRound( Theory::Effort effort );
- /** process at effort */
- int process( Node f, Theory::Effort effort, int e );
-
- class Statistics {
- public:
- IntStat d_instantiations;
- Statistics();
- ~Statistics();
- };
- Statistics d_statistics;
-};/* class InstantiatiorTheoryQuantifiers */
-
-}/* CVC4::theory::quantifiers namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_INSTANTIATOR_H */
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 4d5efcd8d..bc577fda6 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -15,7 +15,6 @@
#include "theory/quantifiers/trigger.h"
#include "theory/theory_engine.h"
#include "theory/quantifiers_engine.h"
-#include "theory/uf/theory_uf_instantiator.h"
#include "theory/quantifiers/candidate_generator.h"
#include "theory/uf/equality_engine.h"
#include "theory/quantifiers/options.h"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback