diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/Makefile.am | 10 | ||||
-rwxr-xr-x | src/theory/quantifiers/inst_strategy_cbqi.cpp | 403 | ||||
-rwxr-xr-x | src/theory/quantifiers/inst_strategy_cbqi.h | 110 | ||||
-rwxr-xr-x | src/theory/quantifiers/inst_strategy_e_matching.cpp | 379 | ||||
-rwxr-xr-x | src/theory/quantifiers/inst_strategy_e_matching.h | 132 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 108 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.h | 81 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiator_default.cpp | 54 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiator_default.h | 46 | ||||
-rw-r--r-- | src/theory/quantifiers/kinds | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers_instantiator.cpp | 73 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers_instantiator.h | 58 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 1 |
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" |