diff options
47 files changed, 1252 insertions, 2202 deletions
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index b71f07852..b2d1b9f09 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -43,9 +43,7 @@ libarith_la_SOURCES = \ arith_unate_lemma_mode.h \ arith_unate_lemma_mode.cpp \ arith_propagation_mode.h \ - arith_propagation_mode.cpp \ - theory_arith_instantiator.h \ - theory_arith_instantiator.cpp + arith_propagation_mode.cpp EXTRA_DIST = \ kinds \ diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 0be7d31a5..07cfcc9e5 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -6,7 +6,6 @@ theory THEORY_ARITH ::CVC4::theory::arith::TheoryArith "theory/arith/theory_arith.h" typechecker "theory/arith/theory_arith_type_rules.h" -instantiator ::CVC4::theory::arith::InstantiatorTheoryArith "theory/arith/theory_arith_instantiator.h" properties stable-infinite properties check propagate ppStaticLearn presolve notifyRestart diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index ad041208d..6a83c501b 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -50,9 +50,12 @@ namespace CVC4 { namespace theory { -namespace arith { -class InstStrategySimplex; +namespace quantifiers { + class InstStrategySimplex; +} + +namespace arith { /** * Implementation of QF_LRA. @@ -60,7 +63,7 @@ class InstStrategySimplex; * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf */ class TheoryArith : public Theory { - friend class InstStrategySimplex; + friend class quantifiers::InstStrategySimplex; private: bool d_nlIncomplete; // TODO A better would be: diff --git a/src/theory/arith/theory_arith_instantiator.h b/src/theory/arith/theory_arith_instantiator.h deleted file mode 100644 index 70bc97bd8..000000000 --- a/src/theory/arith/theory_arith_instantiator.h +++ /dev/null @@ -1,110 +0,0 @@ -/********************* */ -/*! \file theory_arith_instantiator.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__INSTANTIATOR_ARITH_H -#define __CVC4__INSTANTIATOR_ARITH_H - -#include "theory/quantifiers_engine.h" -#include "theory/arith/arithvar_node_map.h" - -#include "util/statistics_registry.h" - -namespace CVC4 { -namespace theory { -namespace arith { - -class TheoryArith; -class InstantiatorTheoryArith; - -class InstStrategySimplex : public InstStrategy{ -private: - /** delta */ - std::map< TypeNode, Node > d_deltas; - /** for each quantifier, simplex rows */ - std::map< Node, std::vector< ArithVar > > d_instRows; - /** tableaux */ - std::map< ArithVar, Node > d_tableaux_term; - std::map< ArithVar, std::map< Node, Node > > d_tableaux_ce_term; - std::map< ArithVar, std::map< Node, Node > > d_tableaux; - /** ce tableaux */ - std::map< ArithVar, std::map< Node, Node > > d_ceTableaux; - /** get value */ - Node getTableauxValue( Node n, bool minus_delta = false ); - Node getTableauxValue( ArithVar v, bool minus_delta = false ); - /** do instantiation */ - bool doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var ); - bool doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta = false ); - /** add term to row */ - void addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t ); - /** get arith theory */ - TheoryArith* getTheoryArith(); - /** print debug */ - void debugPrint( const char* c ); -private: - /** InstantiatorTheoryUf class */ - InstantiatorTheoryArith* d_th; - /** */ - 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( InstantiatorTheoryArith* th, QuantifiersEngine* ie ); - ~InstStrategySimplex(){} - /** identify */ - std::string identify() const { return std::string("Simplex"); } - - class Statistics { - public: - IntStat d_instantiations; - IntStat d_instantiations_minus; - Statistics(); - ~Statistics(); - }; - Statistics d_statistics; -}; - -class InstantiatorTheoryArith : public Instantiator{ - friend class QuantifiersEngine; - friend class InstStrategySimplex; - friend class InstStrategySimplexUfMatch; -public: - InstantiatorTheoryArith(context::Context* c, QuantifiersEngine* ie, Theory* th); - ~InstantiatorTheoryArith() {} - - /** assertNode function, assertion is asserted to theory */ - void assertNode( Node assertion ); - /** Pre-register a term. Done one time for a Node, ever. */ - void preRegisterTerm( Node t ); - /** identify */ - std::string identify() const { return std::string("InstantiatorTheoryArith"); } -private: - /** reset instantiation */ - void processResetInstantiationRound( Theory::Effort effort ); - /** process at effort */ - int process( Node f, Theory::Effort effort, int e ); - - -};/* class InstantiatiorTheoryArith */ - -} -} -} - -#endif
\ No newline at end of file diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am index 8b8a5bd48..be3f25ef5 100644 --- a/src/theory/arrays/Makefile.am +++ b/src/theory/arrays/Makefile.am @@ -17,8 +17,6 @@ libarrays_la_SOURCES = \ array_info.cpp \ static_fact_manager.h \ static_fact_manager.cpp \ - theory_arrays_instantiator.h \ - theory_arrays_instantiator.cpp \ theory_arrays_model.h \ theory_arrays_model.cpp diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index 46cd5781a..a731d3677 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -6,7 +6,6 @@ theory THEORY_ARRAY ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h" typechecker "theory/arrays/theory_arrays_type_rules.h" -instantiator ::CVC4::theory::arrays::InstantiatorTheoryArrays "theory/arrays/theory_arrays_instantiator.h" properties polite stable-infinite parametric properties check propagate presolve getNextDecisionRequest diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index b8c1ace4b..f4661c389 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -21,7 +21,6 @@ #include <map> #include "theory/rewriter.h" #include "expr/command.h" -#include "theory/arrays/theory_arrays_instantiator.h" #include "theory/arrays/theory_arrays_model.h" #include "theory/model.h" #include "theory/arrays/options.h" @@ -721,7 +720,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ) } } - // Find all stores in which n[0] appears and get corresponding read terms + // Find all stores in which n[0] appears and get corresponding read terms const CTNodeList* instores = d_infoMap.getInStores(array_eqc); size_t it = 0; for(; it < instores->size(); ++it) { diff --git a/src/theory/arrays/theory_arrays_instantiator.cpp b/src/theory/arrays/theory_arrays_instantiator.cpp deleted file mode 100644 index 4c6c1a967..000000000 --- a/src/theory/arrays/theory_arrays_instantiator.cpp +++ /dev/null @@ -1,119 +0,0 @@ -/********************* */ -/*! \file theory_arrays_instantiator.cpp - ** \verbatim - ** Original author: ajreynol - ** Major contributors: bobot - ** 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_arrays_instantiator class - **/ - -#include "theory/theory_engine.h" -#include "theory/arrays/theory_arrays_instantiator.h" -#include "theory/arrays/theory_arrays.h" -#include "theory/quantifiers/options.h" -#include "theory/rewriterules/rr_candidate_generator.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::arrays; - -InstantiatorTheoryArrays::InstantiatorTheoryArrays(context::Context* c, QuantifiersEngine* ie, Theory* th) : -Instantiator( c, ie, th ){ - -} - -void InstantiatorTheoryArrays::preRegisterTerm( Node t ){ - -} - -void InstantiatorTheoryArrays::assertNode( Node assertion ){ - Debug("quant-arrays-assert") << "InstantiatorTheoryArrays::assertNode: " << assertion << std::endl; - //INST_ELIM_TRY//d_quantEngine->addTermToDatabase( assertion ); - if( options::cbqi() ){ - if( assertion.hasAttribute(InstConstantAttribute()) ){ - setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) ); - }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){ - setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) ); - } - } -} - - -void InstantiatorTheoryArrays::processResetInstantiationRound( Theory::Effort effort ){ - -} - -int InstantiatorTheoryArrays::process( Node f, Theory::Effort effort, int e ){ - return InstStrategy::STATUS_SAT; -} - -bool InstantiatorTheoryArrays::hasTerm( Node a ){ - return ((TheoryArrays*)d_th)->getEqualityEngine()->hasTerm( a ); -} - -bool InstantiatorTheoryArrays::areEqual( Node a, Node b ){ - if( a==b ){ - return true; - }else if( hasTerm( a ) && hasTerm( b ) ){ - return ((TheoryArrays*)d_th)->getEqualityEngine()->areEqual( a, b ); - }else{ - return false; - } -} - -bool InstantiatorTheoryArrays::areDisequal( Node a, Node b ){ - if( a==b ){ - return false; - }else if( hasTerm( a ) && hasTerm( b ) ){ - return ((TheoryArrays*)d_th)->getEqualityEngine()->areDisequal( a, b, false ); - }else{ - return false; - } -} - -Node InstantiatorTheoryArrays::getRepresentative( Node a ){ - if( hasTerm( a ) ){ - return ((TheoryArrays*)d_th)->getEqualityEngine()->getRepresentative( a ); - }else{ - return a; - } -} - -eq::EqualityEngine* InstantiatorTheoryArrays::getEqualityEngine(){ - return ((TheoryArrays*)d_th)->getEqualityEngine(); -} - -void InstantiatorTheoryArrays::getEquivalenceClass( Node a, std::vector< Node >& eqc ){ - if( hasTerm( a ) ){ - a = getEqualityEngine()->getRepresentative( a ); - eq::EqClassIterator eqc_iter( a, getEqualityEngine() ); - while( !eqc_iter.isFinished() ){ - if( std::find( eqc.begin(), eqc.end(), *eqc_iter )==eqc.end() ){ - eqc.push_back( *eqc_iter ); - } - eqc_iter++; - } - } -} - -rrinst::CandidateGenerator* InstantiatorTheoryArrays::getRRCanGenClasses(){ - arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(getTheory()); - eq::EqualityEngine* ee = - static_cast<eq::EqualityEngine*>(ar->getEqualityEngine()); - return new eq::rrinst::CandidateGeneratorTheoryEeClasses(ee); -} - -rrinst::CandidateGenerator* InstantiatorTheoryArrays::getRRCanGenClass(){ - arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(getTheory()); - eq::EqualityEngine* ee = - static_cast<eq::EqualityEngine*>(ar->getEqualityEngine()); - return new eq::rrinst::CandidateGeneratorTheoryEeClass(ee); -} diff --git a/src/theory/arrays/theory_arrays_instantiator.h b/src/theory/arrays/theory_arrays_instantiator.h deleted file mode 100644 index accbff06b..000000000 --- a/src/theory/arrays/theory_arrays_instantiator.h +++ /dev/null @@ -1,61 +0,0 @@ -/********************* */ -/*! \file theory_arrays_instantiator.h - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** 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 Instantiator for theory of arrays - **/ - - -#include "cvc4_private.h" - -#ifndef __CVC4__INSTANTIATOR_THEORY_ARRAYS_H -#define __CVC4__INSTANTIATOR_THEORY_ARRAYS_H - -#include "theory/quantifiers_engine.h" -#include "theory/uf/equality_engine.h" - -namespace CVC4 { -namespace theory { -namespace arrays { - -class InstantiatorTheoryArrays : 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: - InstantiatorTheoryArrays(context::Context* c, QuantifiersEngine* ie, Theory* th); - ~InstantiatorTheoryArrays() {} - /** Pre-register a term. */ - void preRegisterTerm( Node t ); - /** assertNode function, assertion is asserted to theory */ - void assertNode( Node assertion ); - /** identify */ - std::string identify() const { return std::string("InstantiatorTheoryArrays"); } -public: - /** general queries about equality */ - bool hasTerm( Node a ); - bool areEqual( Node a, Node b ); - bool areDisequal( Node a, Node b ); - Node getRepresentative( Node a ); - eq::EqualityEngine* getEqualityEngine(); - void getEquivalenceClass( Node a, std::vector< Node >& eqc ); - /** general creators of candidate generators */ - rrinst::CandidateGenerator* getRRCanGenClasses(); - rrinst::CandidateGenerator* getRRCanGenClass(); -};/* class Instantiatior */ - -} -} -} - -#endif diff --git a/src/theory/datatypes/Makefile.am b/src/theory/datatypes/Makefile.am index b3aa318d5..323e18de9 100644 --- a/src/theory/datatypes/Makefile.am +++ b/src/theory/datatypes/Makefile.am @@ -10,9 +10,7 @@ libdatatypes_la_SOURCES = \ type_enumerator.h \ theory_datatypes.h \ datatypes_rewriter.h \ - theory_datatypes.cpp \ - theory_datatypes_instantiator.h \ - theory_datatypes_instantiator.cpp + theory_datatypes.cpp EXTRA_DIST = \ kinds diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 3968af4dd..2e58677df 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -6,7 +6,7 @@ theory THEORY_DATATYPES ::CVC4::theory::datatypes::TheoryDatatypes "theory/datatypes/theory_datatypes.h" typechecker "theory/datatypes/theory_datatypes_type_rules.h" -instantiator ::CVC4::theory::datatypes::InstantiatorTheoryDatatypes "theory/datatypes/theory_datatypes_instantiator.h" + properties check presolve parametric propagate diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 7c8f4014e..e23d9deae 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -20,7 +20,6 @@ #include "expr/kind.h" #include "util/datatype.h" #include "util/cvc4_assert.h" -#include "theory/datatypes/theory_datatypes_instantiator.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/theory_datatypes_type_rules.h" #include "theory/model.h" diff --git a/src/theory/datatypes/theory_datatypes_instantiator.cpp b/src/theory/datatypes/theory_datatypes_instantiator.cpp deleted file mode 100644 index f1ac2da24..000000000 --- a/src/theory/datatypes/theory_datatypes_instantiator.cpp +++ /dev/null @@ -1,231 +0,0 @@ -/********************* */ -/*! \file theory_datatypes_instantiator.cpp - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): mdeters, 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 theory_datatypes_instantiator class - **/ - -#include "theory/datatypes/theory_datatypes_instantiator.h" -#include "theory/datatypes/theory_datatypes.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" -#include "theory/rewriterules/rr_candidate_generator.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::datatypes; - -InstStrategyDatatypesValue::InstStrategyDatatypesValue( QuantifiersEngine* qe ) : InstStrategy( qe ){ - -} - -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(); - } - } - } - } - } - */ -} - -InstStrategyDatatypesValue::Statistics::Statistics(): - d_instantiations("InstStrategyDatatypesValue::Instantiations_Total", 0) -{ - StatisticsRegistry::registerStat(&d_instantiations); -} - -InstStrategyDatatypesValue::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_instantiations); -} - - - -InstantiatorTheoryDatatypes::InstantiatorTheoryDatatypes(context::Context* c, QuantifiersEngine* ie, TheoryDatatypes* th) : -Instantiator( c, ie, th ){ - if( options::cbqi() ){ - addInstStrategy( new InstStrategyDatatypesValue( ie ) ); - } -} - -void InstantiatorTheoryDatatypes::assertNode( Node assertion ){ - Debug("quant-datatypes-assert") << "InstantiatorTheoryDatatypes::check: " << assertion << std::endl; - //INST_ELIM_TRY//d_quantEngine->addTermToDatabase( assertion ); - if( options::cbqi() ){ - if( assertion.hasAttribute(InstConstantAttribute()) ){ - setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) ); - }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){ - setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) ); - } - } -} - -void InstantiatorTheoryDatatypes::processResetInstantiationRound( Theory::Effort effort ){ - -} - -int InstantiatorTheoryDatatypes::process( Node f, Theory::Effort effort, int e ){ - return InstStrategy::STATUS_UNKNOWN; -} - -bool InstantiatorTheoryDatatypes::hasTerm( Node a ){ - return ((TheoryDatatypes*)d_th)->getEqualityEngine()->hasTerm( a ); -} - -bool InstantiatorTheoryDatatypes::areEqual( Node a, Node b ){ - if( a==b ){ - return true; - }else if( hasTerm( a ) && hasTerm( b ) ){ - return ((TheoryDatatypes*)d_th)->getEqualityEngine()->areEqual( a, b ); - }else{ - return false; - } -} - -bool InstantiatorTheoryDatatypes::areDisequal( Node a, Node b ){ - if( a==b ){ - return false; - }else if( hasTerm( a ) && hasTerm( b ) ){ - return ((TheoryDatatypes*)d_th)->getEqualityEngine()->areDisequal( a, b, false ); - }else{ - return false; - } -} - -Node InstantiatorTheoryDatatypes::getRepresentative( Node a ){ - if( hasTerm( a ) ){ - return ((TheoryDatatypes*)d_th)->getEqualityEngine()->getRepresentative( a ); - }else{ - return a; - } -} - -eq::EqualityEngine* InstantiatorTheoryDatatypes::getEqualityEngine(){ - return &((TheoryDatatypes*)d_th)->d_equalityEngine; -} - -void InstantiatorTheoryDatatypes::getEquivalenceClass( Node a, std::vector< Node >& eqc ){ - if( hasTerm( a ) ){ - a = getEqualityEngine()->getRepresentative( a ); - eq::EqClassIterator eqc_iter( a, getEqualityEngine() ); - while( !eqc_iter.isFinished() ){ - if( std::find( eqc.begin(), eqc.end(), *eqc_iter )==eqc.end() ){ - eqc.push_back( *eqc_iter ); - } - eqc_iter++; - } - } -} - -CVC4::theory::rrinst::CandidateGenerator* InstantiatorTheoryDatatypes::getRRCanGenClass(){ - datatypes::TheoryDatatypes* dt = static_cast<datatypes::TheoryDatatypes*>(getTheory()); - eq::EqualityEngine* ee = - static_cast<eq::EqualityEngine*>(dt->getEqualityEngine()); - return new eq::rrinst::CandidateGeneratorTheoryEeClass(ee); -} diff --git a/src/theory/datatypes/theory_datatypes_instantiator.h b/src/theory/datatypes/theory_datatypes_instantiator.h deleted file mode 100644 index d7806a21d..000000000 --- a/src/theory/datatypes/theory_datatypes_instantiator.h +++ /dev/null @@ -1,88 +0,0 @@ -/********************* */ -/*! \file theory_datatypes_instantiator.h - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): mdeters, 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 instantiator_datatypes_instantiator - **/ - - -#include "cvc4_private.h" - -#ifndef __CVC4__INSTANTIATOR_DATATYPES_H -#define __CVC4__INSTANTIATOR_DATATYPES_H - -#include "theory/quantifiers_engine.h" - -#include "util/statistics_registry.h" - -namespace CVC4 { -namespace theory { -namespace datatypes { - -class TheoryDatatypes; - -class InstStrategyDatatypesValue : public InstStrategy -{ -private: - Node getValueFor( Node n ); -public: - //constructor - InstStrategyDatatypesValue( 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 Statistics { - public: - IntStat d_instantiations; - Statistics(); - ~Statistics(); - }; - Statistics d_statistics; -};/* class InstStrategy */ - - -class InstantiatorTheoryDatatypes : public Instantiator{ - friend class QuantifiersEngine; -public: - InstantiatorTheoryDatatypes(context::Context* c, QuantifiersEngine* ie, TheoryDatatypes* th); - ~InstantiatorTheoryDatatypes() {} - - /** assertNode function, assertion is asserted to theory */ - void assertNode( Node assertion ); - /** identify */ - std::string identify() const { return std::string("InstantiatorTheoryDatatypes"); } -private: - /** reset instantiation */ - void processResetInstantiationRound( Theory::Effort effort ); - /** process at effort */ - int process( Node f, Theory::Effort effort, int e ); -public: - /** general queries about equality */ - bool hasTerm( Node a ); - bool areEqual( Node a, Node b ); - bool areDisequal( Node a, Node b ); - Node getRepresentative( Node a ); - eq::EqualityEngine* getEqualityEngine(); - void getEquivalenceClass( Node a, std::vector< Node >& eqc ); - /** general creators of candidate generators */ - CVC4::theory::rrinst::CandidateGenerator* getRRCanGenClass(); -};/* class InstantiatiorTheoryDatatypes */ - - -} -} -} - -#endif 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/arith/theory_arith_instantiator.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index d8dceef80..d79ddee31 100644..100755 --- a/src/theory/arith/theory_arith_instantiator.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -1,337 +1,403 @@ -/********************* */ -/*! \file theory_arith_instantiator.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_arith_instantiator class - **/ - -#include "theory/arith/theory_arith_instantiator.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::arith; - -#define ARITH_INSTANTIATOR_USE_MINUS_DELTA - -InstStrategySimplex::InstStrategySimplex( InstantiatorTheoryArith* th, QuantifiersEngine* ie ) : - InstStrategy( ie ), d_th( th ), d_counter( 0 ){ - d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) ); -} - -TheoryArith* InstStrategySimplex::getTheoryArith(){ - return (TheoryArith*)d_th->getTheory(); -} - -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 = getTheoryArith()->d_arithvarNodeMap.getArithVarToNodeMap(); - for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){ - ArithVar x = (*it).first; - if( getTheoryArith()->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; - d_th->setQuantifierActive( f ); - //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 = getTheoryArith()->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( getTheoryArith()->d_partialModel.hasLowerBound( x ) ){ - Debug(c) << getTheoryArith()->d_partialModel.getLowerBound( x ); - }else{ - Debug(c) << "-infty"; - } - Debug(c) << " <= "; - Debug(c) << getTheoryArith()->d_partialModel.getAssignment( x ); - Debug(c) << " <= "; - if( getTheoryArith()->d_partialModel.hasUpperBound( x ) ){ - Debug(c) << getTheoryArith()->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_statistics.d_instantiations); - return true; - }else{ -#ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA - //otherwise try -delta - if( doInstantiation2( f, term, x, m, var, true ) ){ - ++(d_statistics.d_instantiations_minus); - ++(d_statistics.d_instantiations); - 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( getTheoryArith()->d_arithvarNodeMap.hasArithVar(n) ){ - ArithVar v = getTheoryArith()->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 = getTheoryArith()->d_partialModel.getDelta(); - DeltaRational drv = getTheoryArith()->d_partialModel.getAssignment( v ); - Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta ); - return mkRationalNode(qmodel); -} - - - -InstStrategySimplex::Statistics::Statistics(): - d_instantiations("InstStrategySimplex::Instantiations_Total", 0), - d_instantiations_minus("InstStrategySimplex::Instantiations_minus_delta", 0) -{ - StatisticsRegistry::registerStat(&d_instantiations); - StatisticsRegistry::registerStat(&d_instantiations_minus); -} - -InstStrategySimplex::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_instantiations); - StatisticsRegistry::unregisterStat(&d_instantiations_minus); -} - - - - - - - -InstantiatorTheoryArith::InstantiatorTheoryArith(context::Context* c, QuantifiersEngine* ie, Theory* th) : -Instantiator( c, ie, th ){ - if( options::cbqi() ){ - addInstStrategy( new InstStrategySimplex( this, d_quantEngine ) ); - } -} - -void InstantiatorTheoryArith::preRegisterTerm( Node t ){ - -} - -void InstantiatorTheoryArith::assertNode( Node assertion ){ - Debug("quant-arith-assert") << "InstantiatorTheoryArith::check: " << assertion << std::endl; - //INST_ELIM_TRY//d_quantEngine->addTermToDatabase( assertion ); - if( options::cbqi() ){ - if( assertion.hasAttribute(InstConstantAttribute()) ){ - setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) ); - }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){ - setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) ); - } - } -} - -void InstantiatorTheoryArith::processResetInstantiationRound( Theory::Effort effort ){ - -} - -int InstantiatorTheoryArith::process( Node f, Theory::Effort effort, int e ){ - Debug("quant-arith") << "Arith: Try to solve (" << effort << ") for " << f << "... " << std::endl; - return InstStrategy::STATUS_UNKNOWN; -} +/********************* */
+/*! \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/uf/inst_strategy.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 8c90d569a..48af334ff 100644..100755 --- a/src/theory/uf/inst_strategy.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -1,381 +1,379 @@ -/********************* */ -/*! \file inst_strategy.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 theory uf instantiation strategies - **/ - -#include "theory/uf/inst_strategy.h" - -#include "theory/uf/theory_uf_instantiator.h" -#include "theory/theory_engine.h" -#include "theory/uf/theory_uf.h" -#include "theory/uf/equality_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::uf; -using namespace CVC4::theory::inst; - -#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_statistics.d_instantiations += 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_statistics.d_instantiations_min += numInst; - //}else{ - // d_statistics.d_instantiations += 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_statistics.d_instantiations); - //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); -} -*/
\ No newline at end of file +/********************* */
+/*! \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/uf/inst_strategy.h b/src/theory/quantifiers/inst_strategy_e_matching.h index 42d401126..ea22486a6 100644..100755 --- a/src/theory/uf/inst_strategy.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -1,168 +1,132 @@ -/********************* */ -/*! \file inst_strategy.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 Theory uf instantiation strategies - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__INST_STRATEGY_H -#define __CVC4__INST_STRATEGY_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/uf/theory_uf.h" - -namespace CVC4 { -namespace theory { -namespace uf { - -class InstantiatorTheoryUf; - -//instantiation strategies - -class InstStrategyUserPatterns : public InstStrategy{ -private: - /** InstantiatorTheoryUf class */ - InstantiatorTheoryUf* d_th; - /** 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( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : - InstStrategy( ie ), d_th( th ){} - ~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"); } -public: - /** statistics class */ - //class Statistics { - //public: - // IntStat d_instantiations; - // Statistics(); - // ~Statistics(); - //}; - //Statistics d_statistics; -};/* class InstStrategyUserPatterns */ - -class InstStrategyAutoGenTriggers : public InstStrategy{ -public: - enum { - RELEVANCE_NONE, - RELEVANCE_DEFAULT, - }; -private: - /** InstantiatorTheoryUf class */ - InstantiatorTheoryUf* d_th; - /** 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( InstantiatorTheoryUf* th, QuantifiersEngine* ie, int tstrt, int rstrt, int rgfr = -1 ) : - InstStrategy( ie ), d_th( th ), 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; } -public: - /** statistics class */ - //class Statistics { - //public: - // IntStat d_instantiations; - // IntStat d_instantiations_min; - // Statistics(); - // ~Statistics(); - //}; - //Statistics d_statistics; -};/* class InstStrategyAutoGenTriggers */ - -class InstStrategyFreeVariable : public InstStrategy{ -private: - /** InstantiatorTheoryUf class */ - InstantiatorTheoryUf* d_th; - /** 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( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : - InstStrategy( ie ), d_th( th ){} - ~InstStrategyFreeVariable(){} - /** identify */ - std::string identify() const { return std::string("FreeVariable"); } -public: - /** statistics class */ - //class Statistics { - //public: - // IntStat d_instantiations; - // Statistics(); - // ~Statistics(); - //}; - //Statistics d_statistics; -};/* class InstStrategyFreeVariable */ - -}/* CVC4::theory::uf namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif +/********************* */
+/*! \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" diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ce62e2f8b..c04920ab8 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -14,7 +14,6 @@ #include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" -#include "theory/uf/theory_uf_instantiator.h" #include "theory/uf/theory_uf_strong_solver.h" #include "theory/uf/equality_engine.h" #include "theory/arrays/theory_arrays.h" @@ -25,6 +24,7 @@ #include "theory/quantifiers/instantiation_engine.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/trigger.h" #include "theory/rewriterules/efficient_e_matching.h" #include "theory/rewriterules/rr_trigger.h" @@ -84,9 +84,9 @@ EqualityQuery* QuantifiersEngine::getEqualityQuery() { return d_eq_query; } -Instantiator* QuantifiersEngine::getInstantiator( theory::TheoryId id ){ - return d_te->theoryOf( id )->getInstantiator(); -} +//Instantiator* QuantifiersEngine::getInstantiator( theory::TheoryId id ){ +// return d_te->theoryOf( id )->getInstantiator(); +//} context::Context* QuantifiersEngine::getSatContext(){ return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext(); @@ -100,6 +100,12 @@ Valuation& QuantifiersEngine::getValuation(){ return d_te->theoryOf( THEORY_QUANTIFIERS )->getValuation(); } +void QuantifiersEngine::finishInit(){ + for( int i=0; i<(int)d_modules.size(); i++ ){ + d_modules[i]->finishInit(); + } +} + void QuantifiersEngine::check( Theory::Effort e ){ CodeTimer codeTimer(d_time); bool needsCheck = e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 719620e76..8169c78fb 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -45,6 +45,8 @@ public: virtual ~QuantifiersModule(){} //get quantifiers engine QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; } + /** initialize */ + virtual void finishInit() {} /* whether this module needs to check this round */ virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; } /* Call during quantifier engine's check */ @@ -122,7 +124,7 @@ public: QuantifiersEngine(context::Context* c, TheoryEngine* te); ~QuantifiersEngine(); /** get instantiator for id */ - Instantiator* getInstantiator( theory::TheoryId id ); + //Instantiator* getInstantiator( theory::TheoryId id ); /** get theory engine */ TheoryEngine* getTheoryEngine() { return d_te; } /** get equality query object for the given type. The default is the @@ -147,6 +149,8 @@ public: /** get efficient e-matching utility */ EfficientEMatcher* getEfficientEMatcher() { return d_eem; } public: + /** initialize */ + void finishInit(); /** check at level */ void check( Theory::Effort e ); /** register quantifier */ diff --git a/src/theory/rewriterules/efficient_e_matching.cpp b/src/theory/rewriterules/efficient_e_matching.cpp index 7f03bf8f8..2f39d8098 100755 --- a/src/theory/rewriterules/efficient_e_matching.cpp +++ b/src/theory/rewriterules/efficient_e_matching.cpp @@ -92,7 +92,8 @@ EfficientEMatcher::EfficientEMatcher( CVC4::theory::QuantifiersEngine* qe ) : d_ }
eq::EqualityEngine* EfficientEMatcher::getEqualityEngine(){
- return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getEqualityEngine();
+ //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getEqualityEngine();
+ return d_quantEngine->getMasterEqualityEngine();
}
/** new node */
diff --git a/src/theory/rewriterules/rr_candidate_generator.cpp b/src/theory/rewriterules/rr_candidate_generator.cpp index 2957b4ddb..3f2895397 100644 --- a/src/theory/rewriterules/rr_candidate_generator.cpp +++ b/src/theory/rewriterules/rr_candidate_generator.cpp @@ -24,100 +24,44 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::rrinst; -GenericCandidateGeneratorClasses::GenericCandidateGeneratorClasses(QuantifiersEngine * qe){ - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - if(qe->getInstantiator(i) != NULL) - d_can_gen[i] = qe->getInstantiator(i)->getRRCanGenClasses(); - else d_can_gen[i] = NULL; - } +GenericCandidateGeneratorClasses::GenericCandidateGeneratorClasses(QuantifiersEngine * qe) : d_qe(qe){ + d_master_can_gen = new eq::rrinst::CandidateGeneratorTheoryEeClasses(d_qe->getMasterEqualityEngine()); } GenericCandidateGeneratorClasses::~GenericCandidateGeneratorClasses(){ - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - delete(d_can_gen[i]); - } + delete d_master_can_gen; } void GenericCandidateGeneratorClasses::resetInstantiationRound(){ - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - if(d_can_gen[i] != NULL) d_can_gen[i]->resetInstantiationRound(); - } - d_can_gen_id=THEORY_FIRST; + d_master_can_gen->resetInstantiationRound(); } void GenericCandidateGeneratorClasses::reset(TNode eqc){ - Assert(eqc.isNull()); - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - if(d_can_gen[i] != NULL) d_can_gen[i]->reset(eqc); - } - d_can_gen_id=THEORY_FIRST; - lookForNextTheory(); + d_master_can_gen->reset(eqc); } TNode GenericCandidateGeneratorClasses::getNextCandidate(){ - Assert(THEORY_FIRST <= d_can_gen_id && d_can_gen_id <= THEORY_LAST); - /** No more */ - if(d_can_gen_id == THEORY_LAST) return TNode::null(); - /** Try with this theory */ - TNode cand = d_can_gen[d_can_gen_id]->getNextCandidate(); - if( !cand.isNull() ) return cand; - lookForNextTheory(); - return getNextCandidate(); + return d_master_can_gen->getNextCandidate(); } -void GenericCandidateGeneratorClasses::lookForNextTheory(){ - do{ /* look for the next available generator */ - ++d_can_gen_id; - } while( d_can_gen_id < THEORY_LAST && d_can_gen[d_can_gen_id] == NULL); -} GenericCandidateGeneratorClass::GenericCandidateGeneratorClass(QuantifiersEngine * qe): d_qe(qe) { - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - if(d_qe->getInstantiator(i) != NULL) - d_can_gen[i] = d_qe->getInstantiator(i)->getRRCanGenClass(); - else d_can_gen[i] = NULL; - } + d_master_can_gen = new eq::rrinst::CandidateGeneratorTheoryEeClass(d_qe->getMasterEqualityEngine()); } GenericCandidateGeneratorClass::~GenericCandidateGeneratorClass(){ - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - delete(d_can_gen[i]); - } + delete d_master_can_gen; } void GenericCandidateGeneratorClass::resetInstantiationRound(){ - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - if(d_can_gen[i] != NULL) d_can_gen[i]->resetInstantiationRound(); - } - d_can_gen_id=THEORY_FIRST; + d_master_can_gen->resetInstantiationRound(); } void GenericCandidateGeneratorClass::reset(TNode eqc){ - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - if(d_can_gen[i] != NULL) d_can_gen[i]->reset(eqc); - } - d_can_gen_id=THEORY_FIRST; - d_node = eqc; - lookForNextTheory(); + d_master_can_gen->reset(eqc); } TNode GenericCandidateGeneratorClass::getNextCandidate(){ - Assert(THEORY_FIRST <= d_can_gen_id && d_can_gen_id <= THEORY_LAST); - /** No more */ - if(d_can_gen_id == THEORY_LAST) return TNode::null(); - /** Try with this theory */ - TNode cand = d_can_gen[d_can_gen_id]->getNextCandidate(); - if( !cand.isNull() ) return cand; - lookForNextTheory(); - return getNextCandidate(); + return d_master_can_gen->getNextCandidate(); } -void GenericCandidateGeneratorClass::lookForNextTheory(){ - do{ /* look for the next available generator, where the element is */ - ++d_can_gen_id; - } while( - d_can_gen_id < THEORY_LAST && - (d_can_gen[d_can_gen_id] == NULL || - !d_qe->getInstantiator( d_can_gen_id )->hasTerm( d_node )) - ); -} diff --git a/src/theory/rewriterules/rr_candidate_generator.h b/src/theory/rewriterules/rr_candidate_generator.h index 8ebaae343..97c710219 100644 --- a/src/theory/rewriterules/rr_candidate_generator.h +++ b/src/theory/rewriterules/rr_candidate_generator.h @@ -166,10 +166,9 @@ public: class GenericCandidateGeneratorClasses: public rrinst::CandidateGenerator{ /** The candidate generators */ - rrinst::CandidateGenerator* d_can_gen[theory::THEORY_LAST]; - /** The current theory which candidategenerator is used */ - TheoryId d_can_gen_id; - + rrinst::CandidateGenerator* d_master_can_gen; + /** QuantifierEngine */ + QuantifiersEngine* d_qe; public: GenericCandidateGeneratorClasses(QuantifiersEngine * qe); ~GenericCandidateGeneratorClasses(); @@ -183,22 +182,15 @@ public: class GenericCandidateGeneratorClass: public rrinst::CandidateGenerator{ /** The candidate generators */ - rrinst::CandidateGenerator* d_can_gen[theory::THEORY_LAST]; - /** The current theory which candidategenerator is used */ - TheoryId d_can_gen_id; - /** current node to look for equivalence class */ - Node d_node; + rrinst::CandidateGenerator* d_master_can_gen; /** QuantifierEngine */ QuantifiersEngine* d_qe; - public: GenericCandidateGeneratorClass(QuantifiersEngine * qe); ~GenericCandidateGeneratorClass(); void resetInstantiationRound(); - void reset(TNode eqc); TNode getNextCandidate(); - void lookForNextTheory(); }; }/* CVC4::theory namespace */ diff --git a/src/theory/rewriterules/rr_inst_match.cpp b/src/theory/rewriterules/rr_inst_match.cpp index 5f10e1daa..5c3a55831 100644 --- a/src/theory/rewriterules/rr_inst_match.cpp +++ b/src/theory/rewriterules/rr_inst_match.cpp @@ -15,7 +15,6 @@ #include "theory/quantifiers/inst_match.h" #include "theory/theory_engine.h" #include "theory/quantifiers_engine.h" -#include "theory/uf/theory_uf_instantiator.h" #include "theory/uf/equality_engine.h" #include "theory/arrays/theory_arrays.h" #include "theory/datatypes/theory_datatypes.h" diff --git a/src/theory/rewriterules/rr_trigger.cpp b/src/theory/rewriterules/rr_trigger.cpp index ad77f0bcb..4f48a72ae 100644 --- a/src/theory/rewriterules/rr_trigger.cpp +++ b/src/theory/rewriterules/rr_trigger.cpp @@ -15,7 +15,6 @@ #include "theory/rewriterules/rr_trigger.h" #include "theory/theory_engine.h" #include "theory/quantifiers_engine.h" -#include "theory/uf/theory_uf_instantiator.h" #include "theory/rewriterules/rr_candidate_generator.h" #include "theory/uf/equality_engine.h" diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index f8e2ec777..ea3902d59 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -17,7 +17,6 @@ #include "theory/theory.h" #include "util/cvc4_assert.h" #include "theory/quantifiers_engine.h" -#include "theory/quantifiers/instantiator_default.h" #include <vector> @@ -184,15 +183,18 @@ Instantiator::~Instantiator() { } void Instantiator::resetInstantiationRound(Theory::Effort effort) { + /* for(int i = 0; i < (int) d_instStrategies.size(); ++i) { if(isActiveStrategy(d_instStrategies[i])) { d_instStrategies[i]->processResetInstantiationRound(effort); } } processResetInstantiationRound(effort); + */ } int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e ) { + /* if( getQuantifierActive(f) ) { int status = process(f, effort, e ); if(d_instStrategies.empty()) { @@ -215,6 +217,8 @@ int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e ) { Debug("inst-engine-inst") << "We have no constraints from this quantifier." << endl; return InstStrategy::STATUS_SAT; } + */ + return 0; } //void Instantiator::doInstantiation(int effort) { diff --git a/src/theory/theory.h b/src/theory/theory.h index 4d535a8af..1f55a4b90 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -820,40 +820,6 @@ namespace eq{ class EqualityEngine; } -/** 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; - - -public: - InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){} - virtual ~InstStrategy(){} - - /** 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 */ /** instantiator class */ class Instantiator { @@ -863,21 +829,6 @@ protected: QuantifiersEngine* d_quantEngine; /** reference to the theory that it looks at */ Theory* d_th; - /** instantiation strategies */ - std::vector< InstStrategy* > d_instStrategies; - /** instantiation strategies active */ - std::map< InstStrategy*, bool > d_instStrategyActive; - /** has constraints from quantifier */ - std::map< Node, bool > d_quantActive; - /** 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; - } /** reset instantiation round */ virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; /** process quantifier */ @@ -899,10 +850,6 @@ public: /** print debug information */ virtual void debugPrint( const char* c ) {} public: - /** set has constraints from quantifier f */ - void setQuantifierActive( Node f ) { d_quantActive[f] = true; } - /** has constraints from */ - bool getQuantifierActive( Node f ) { return d_quantActive.find(f) != d_quantActive.end() && d_quantActive[f]; } /** reset instantiation round */ void resetInstantiationRound( Theory::Effort effort ); /** do instantiation method*/ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index ce3ccebf3..c0aa58647 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -53,6 +53,7 @@ using namespace CVC4::theory; void TheoryEngine::finishInit() { if (d_logicInfo.isQuantified()) { + d_quantEngine->finishInit(); Assert(d_masterEqualityEngine == 0); d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master"); @@ -70,6 +71,9 @@ void TheoryEngine::eqNotifyNewClass(TNode t){ void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){ //TODO: add notification to efficient E-matching + if (d_logicInfo.isQuantified()) { + d_quantEngine->getEfficientEMatcher()->merge( t1, t2 ); + } } void TheoryEngine::eqNotifyPostMerge(TNode t1, TNode t2){ diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index e027f8909..82129c72b 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -15,12 +15,8 @@ libuf_la_SOURCES = \ equality_engine.cpp \ symmetry_breaker.h \ symmetry_breaker.cpp \ - theory_uf_instantiator.h \ - theory_uf_instantiator.cpp \ theory_uf_strong_solver.h \ theory_uf_strong_solver.cpp \ - inst_strategy.h \ - inst_strategy.cpp \ theory_uf_model.h \ theory_uf_model.cpp diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index 1d179248c..fa24df717 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -6,7 +6,6 @@ theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h" typechecker "theory/uf/theory_uf_type_rules.h" -instantiator ::CVC4::theory::uf::InstantiatorTheoryUf "theory/uf/theory_uf_instantiator.h" properties stable-infinite parametric properties check propagate ppStaticLearn presolve getNextDecisionRequest diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 23f100f74..3f033f3b8 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -18,12 +18,9 @@ #include "theory/uf/theory_uf.h" #include "theory/uf/options.h" #include "theory/quantifiers/options.h" -#include "theory/uf/theory_uf_instantiator.h" #include "theory/uf/theory_uf_strong_solver.h" #include "theory/model.h" #include "theory/type_enumerator.h" -//included since efficient e matching needs notifications from UF -#include "theory/rewriterules/efficient_e_matching.h" using namespace std; using namespace CVC4; @@ -479,15 +476,11 @@ void TheoryUF::eqNotifyNewClass(TNode t) { if (d_thss != NULL) { d_thss->newEqClass(t); } - // this can be called very early, during initialization - if (!getLogicInfo().isLocked() || getLogicInfo().isQuantified()) { - //getQuantifiersEngine()->addTermToDatabase( t ); - } } void TheoryUF::eqNotifyPreMerge(TNode t1, TNode t2) { if (getLogicInfo().isQuantified()) { - getQuantifiersEngine()->getEfficientEMatcher()->merge( t1, t2 ); + //getQuantifiersEngine()->getEfficientEMatcher()->merge( t1, t2 ); } } diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp deleted file mode 100644 index 9ae6bbd37..000000000 --- a/src/theory/uf/theory_uf_instantiator.cpp +++ /dev/null @@ -1,185 +0,0 @@ -/********************* */ -/*! \file theory_uf_instantiator.cpp - ** \verbatim - ** Original author: ajreynol - ** Major contributors: bobot - ** 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 uf instantiator class - **/ - -#include "theory/uf/theory_uf_instantiator.h" -#include "theory/theory_engine.h" -#include "theory/uf/theory_uf.h" -#include "theory/uf/equality_engine.h" -#include "theory/quantifiers/options.h" -#include "theory/rewriterules/options.h" -#include "theory/quantifiers/term_database.h" -#include "theory/rewriterules/rr_candidate_generator.h" -#include "theory/rewriterules/efficient_e_matching.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::uf; -using namespace CVC4::theory::inst; - -namespace CVC4 { -namespace theory { -namespace uf { - -InstantiatorTheoryUf::InstantiatorTheoryUf(context::Context* c, CVC4::theory::QuantifiersEngine* qe, Theory* th) : -Instantiator( c, qe, th ) -{ - if( !options::finiteModelFind() || options::fmfInstEngine() ){ - //if( options::cbqi() ){ - // addInstStrategy( new InstStrategyCheckCESolved( this, qe ) ); - //} - //these are the instantiation strategies for basic E-matching - if( options::userPatternsQuant() ){ - d_isup = new InstStrategyUserPatterns( this, qe ); - addInstStrategy( d_isup ); - }else{ - d_isup = NULL; - } - InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( this, qe, 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( this, qe ) ); - } - //d_isup->setPriorityOver( i_ag ); - //d_isup->setPriorityOver( i_agm ); - //i_ag->setPriorityOver( i_agm ); - } -} - -void InstantiatorTheoryUf::preRegisterTerm( Node t ){ - //d_quantEngine->addTermToDatabase( t ); -} - -void InstantiatorTheoryUf::assertNode( Node assertion ) -{ - Debug("quant-uf-assert") << "InstantiatorTheoryUf::check: " << assertion << std::endl; - //preRegisterTerm( assertion ); - //INST_ELIM_TRY//d_quantEngine->addTermToDatabase( assertion ); - if( options::cbqi() ){ - if( assertion.hasAttribute(InstConstantAttribute()) ){ - setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) ); - }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){ - setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) ); - } - } -} - -void InstantiatorTheoryUf::addUserPattern( Node f, Node pat ){ - if( d_isup ){ - d_isup->addUserPattern( f, pat ); - setQuantifierActive( f ); - } -} - - -void InstantiatorTheoryUf::processResetInstantiationRound( Theory::Effort effort ){ - //d_ground_reps.clear(); -} - -int InstantiatorTheoryUf::process( Node f, Theory::Effort effort, int e ){ - Debug("quant-uf") << "UF: Try to solve (" << e << ") for " << f << "... " << std::endl; - return InstStrategy::STATUS_SAT; -} - -void InstantiatorTheoryUf::debugPrint( const char* c ) -{ - -} - -bool InstantiatorTheoryUf::hasTerm( Node a ){ - return ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( a ); -} - -bool InstantiatorTheoryUf::areEqual( Node a, Node b ){ - if( a==b ){ - return true; - }else if( hasTerm( a ) && hasTerm( b ) ){ - return ((TheoryUF*)d_th)->d_equalityEngine.areEqual( a, b ); - }else{ - return false; - } -} - -bool InstantiatorTheoryUf::areDisequal( Node a, Node b ){ - if( a==b ){ - return false; - }else if( hasTerm( a ) && hasTerm( b ) ){ - return ((TheoryUF*)d_th)->d_equalityEngine.areDisequal( a, b, false ); - }else{ - return false; - } -} - -Node InstantiatorTheoryUf::getRepresentative( Node a ){ - if( hasTerm( a ) ){ - return ((TheoryUF*)d_th)->d_equalityEngine.getRepresentative( a ); - }else{ - return a; - } -} - -eq::EqualityEngine* InstantiatorTheoryUf::getEqualityEngine(){ - return &((TheoryUF*)d_th)->d_equalityEngine; -} - -void InstantiatorTheoryUf::getEquivalenceClass( Node a, std::vector< Node >& eqc ){ - if( hasTerm( a ) ){ - a = getEqualityEngine()->getRepresentative( a ); - eq::EqClassIterator eqc_iter( a, getEqualityEngine() ); - while( !eqc_iter.isFinished() ){ - if( std::find( eqc.begin(), eqc.end(), *eqc_iter )==eqc.end() ){ - eqc.push_back( *eqc_iter ); - } - eqc_iter++; - } - } -} - -void InstantiatorTheoryUf::outputEqClass( const char* c, Node n ){ - if( ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( n ) ){ - eq::EqClassIterator eqc_iter( getRepresentative( n ), - &((TheoryUF*)d_th)->d_equalityEngine ); - bool firstTime = true; - while( !eqc_iter.isFinished() ){ - if( !firstTime ){ Debug(c) << ", "; } - Debug(c) << (*eqc_iter); - firstTime = false; - eqc_iter++; - } - }else{ - Debug(c) << n; - } -} - -rrinst::CandidateGenerator* InstantiatorTheoryUf::getRRCanGenClasses(){ - uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(getTheory()); - eq::EqualityEngine* ee = static_cast<eq::EqualityEngine*>(uf->getEqualityEngine()); - return new eq::rrinst::CandidateGeneratorTheoryEeClasses(ee); -} - -rrinst::CandidateGenerator* InstantiatorTheoryUf::getRRCanGenClass(){ - uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(getTheory()); - eq::EqualityEngine* ee = static_cast<eq::EqualityEngine*>(uf->getEqualityEngine()); - return new eq::rrinst::CandidateGeneratorTheoryEeClass(ee); -} - - -} /* namespace uf */ -} /* namespace theory */ -} /* namespace cvc4 */ diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h deleted file mode 100644 index fe34c9487..000000000 --- a/src/theory/uf/theory_uf_instantiator.h +++ /dev/null @@ -1,87 +0,0 @@ -/********************* */ -/*! \file theory_uf_instantiator.h - ** \verbatim - ** Original author: ajreynol - ** Major contributors: bobot - ** 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 Theory uf instantiator - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY_UF_INSTANTIATOR_H -#define __CVC4__THEORY_UF_INSTANTIATOR_H - -#include "theory/uf/inst_strategy.h" - -#include "context/context.h" -#include "context/context_mm.h" -#include "context/cdchunk_list.h" - -#include "util/statistics_registry.h" -#include "theory/uf/theory_uf.h" -#include "theory/quantifiers/trigger.h" -#include "theory/quantifiers/inst_match_generator.h" -#include "util/ntuple.h" -#include "context/cdqueue.h" - -namespace CVC4 { -namespace theory { - -namespace quantifiers{ - class TermDb; -} - -namespace uf { - -class InstantiatorTheoryUf : public Instantiator{ -protected: - /** instantiation strategies */ - InstStrategyUserPatterns* d_isup; -public: - InstantiatorTheoryUf(context::Context* c, CVC4::theory::QuantifiersEngine* qe, Theory* th); - ~InstantiatorTheoryUf() {} - /** assertNode method */ - void assertNode( Node assertion ); - /** Pre-register a term. Done one time for a Node, ever. */ - void preRegisterTerm( Node t ); - /** identify */ - std::string identify() const { return std::string("InstantiatorTheoryUf"); } - /** debug print */ - void debugPrint( const char* c ); - /** add user pattern */ - void addUserPattern( Node f, Node pat ); -private: - /** reset instantiation */ - void processResetInstantiationRound( Theory::Effort effort ); - /** calculate matches for quantifier f at effort */ - int process( Node f, Theory::Effort effort, int e ); -public: - /** general queries about equality */ - bool hasTerm( Node a ); - bool areEqual( Node a, Node b ); - bool areDisequal( Node a, Node b ); - Node getRepresentative( Node a ); - Node getInternalRepresentative( Node a ); - eq::EqualityEngine* getEqualityEngine(); - void getEquivalenceClass( Node a, std::vector< Node >& eqc ); - /** general creators of candidate generators */ - rrinst::CandidateGenerator* getRRCanGenClasses(); - rrinst::CandidateGenerator* getRRCanGenClass(); -public: - /** output eq class */ - void outputEqClass( const char* c, Node n ); -};/* class InstantiatorTheoryUf */ - - - -} -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY_UF_INSTANTIATOR_H */ diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 0ec89af0b..46ac5aa60 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -15,8 +15,8 @@ #include "theory/uf/theory_uf_strong_solver.h" #include "theory/uf/theory_uf.h" #include "theory/uf/equality_engine.h" -#include "theory/uf/theory_uf_instantiator.h" #include "theory/theory_engine.h" +#include "theory/quantifiers_engine.h" #include "theory/quantifiers/term_database.h" #include "theory/uf/options.h" #include "theory/model.h" |