diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-30 20:38:45 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-30 20:38:45 +0000 |
commit | f28bab562105548413cfca93de5c9b047157a076 (patch) | |
tree | bfbe95b9aed35f91b6bd9e3af50fad03ab86f23b /src | |
parent | 6369830eec077ef112e6cc806cd910c7209eb2db (diff) |
quantifiers now uses master equality engine, preparation work to cleanup code
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/theory_arith_instantiator.cpp | 2 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_instantiator.cpp | 2 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes_instantiator.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 72 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 1 | ||||
-rwxr-xr-x | src/theory/rewriterules/efficient_e_matching.cpp | 30 | ||||
-rwxr-xr-x | src/theory/rewriterules/efficient_e_matching.h | 5 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 22 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 25 | ||||
-rw-r--r-- | src/theory/uf/inst_strategy.cpp | 56 | ||||
-rw-r--r-- | src/theory/uf/inst_strategy.h | 28 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 9 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_instantiator.cpp | 49 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_instantiator.h | 52 |
17 files changed, 181 insertions, 186 deletions
diff --git a/src/theory/arith/theory_arith_instantiator.cpp b/src/theory/arith/theory_arith_instantiator.cpp index 6a783fc41..d8dceef80 100644 --- a/src/theory/arith/theory_arith_instantiator.cpp +++ b/src/theory/arith/theory_arith_instantiator.cpp @@ -317,7 +317,7 @@ void InstantiatorTheoryArith::preRegisterTerm( Node t ){ void InstantiatorTheoryArith::assertNode( Node assertion ){ Debug("quant-arith-assert") << "InstantiatorTheoryArith::check: " << assertion << std::endl; - d_quantEngine->addTermToDatabase( assertion ); + //INST_ELIM_TRY//d_quantEngine->addTermToDatabase( assertion ); if( options::cbqi() ){ if( assertion.hasAttribute(InstConstantAttribute()) ){ setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) ); diff --git a/src/theory/arrays/theory_arrays_instantiator.cpp b/src/theory/arrays/theory_arrays_instantiator.cpp index a93a01322..4c6c1a967 100644 --- a/src/theory/arrays/theory_arrays_instantiator.cpp +++ b/src/theory/arrays/theory_arrays_instantiator.cpp @@ -36,7 +36,7 @@ void InstantiatorTheoryArrays::preRegisterTerm( Node t ){ void InstantiatorTheoryArrays::assertNode( Node assertion ){ Debug("quant-arrays-assert") << "InstantiatorTheoryArrays::assertNode: " << assertion << std::endl; - d_quantEngine->addTermToDatabase( assertion ); + //INST_ELIM_TRY//d_quantEngine->addTermToDatabase( assertion ); if( options::cbqi() ){ if( assertion.hasAttribute(InstConstantAttribute()) ){ setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) ); diff --git a/src/theory/datatypes/theory_datatypes_instantiator.cpp b/src/theory/datatypes/theory_datatypes_instantiator.cpp index cfc45f4cc..f1ac2da24 100644 --- a/src/theory/datatypes/theory_datatypes_instantiator.cpp +++ b/src/theory/datatypes/theory_datatypes_instantiator.cpp @@ -156,7 +156,7 @@ Instantiator( c, ie, th ){ void InstantiatorTheoryDatatypes::assertNode( Node assertion ){ Debug("quant-datatypes-assert") << "InstantiatorTheoryDatatypes::check: " << assertion << std::endl; - d_quantEngine->addTermToDatabase( assertion ); + //INST_ELIM_TRY//d_quantEngine->addTermToDatabase( assertion ); if( options::cbqi() ){ if( assertion.hasAttribute(InstConstantAttribute()) ){ setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 2c2ee0bfe..9a26878b5 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -19,6 +19,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/options.h" #include "theory/rewriterules/efficient_e_matching.h" +#include "theory/quantifiers/theory_quantifiers.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 12b735497..c3987144c 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -71,6 +71,7 @@ public: std::string identify() const { return std::string("TheoryQuantifiers"); } bool flipDecision(); void setUserAttribute( std::string& attr, Node n ); + eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; } private: void assertUniversal( Node n ); void assertExistential( Node n ); diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index a9c5e8b96..4d5efcd8d 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -48,11 +48,11 @@ d_quantEngine( qe ), d_f( f ){ }else{ d_mg = new InstMatchGenerator( d_nodes, qe, matchOption ); } - Debug("trigger") << "Trigger for " << f << ": " << std::endl; + Trace("trigger") << "Trigger for " << f << ": " << std::endl; for( int i=0; i<(int)d_nodes.size(); i++ ){ - Debug("trigger") << " " << d_nodes[i] << std::endl; + Trace("trigger") << " " << d_nodes[i] << std::endl; } - Debug("trigger") << std::endl; + Trace("trigger") << std::endl; if( d_nodes.size()==1 ){ if( isSimpleTrigger( d_nodes[0] ) ){ ++(qe->d_statistics.d_triggers); @@ -230,7 +230,9 @@ bool Trigger::isUsable( Node n, Node f ){ bool Trigger::isUsableTrigger( Node n, Node f ){ //return n.getAttribute(InstConstantAttribute())==f && n.getKind()==APPLY_UF; - return n.getAttribute(InstConstantAttribute())==f && isAtomicTrigger( n ) && isUsable( n, f ); + bool usable = n.getAttribute(InstConstantAttribute())==f && isAtomicTrigger( n ) && isUsable( n, f ); + Trace("usable") << n << " usable : " << usable << std::endl; + return usable; } bool Trigger::isAtomicTrigger( Node n ){ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index b4e046506..ce62e2f8b 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -330,7 +330,7 @@ bool QuantifiersEngine::addLemma( Node lem ){ } bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool modInst, bool mkRep ){ - Trace("inst-add") << "Add instantiation: " << m << std::endl; + Trace("inst-add-debug") << "Add instantiation: " << m << std::endl; //make sure there are values for each variable we are instantiating for( size_t i=0; i<f[0].getNumChildren(); i++ ){ Node ic = d_term_db->getInstantiationConstant( f, i ); @@ -350,7 +350,7 @@ bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool } //check for duplication modulo equality if( !d_inst_match_trie[f].addInstMatch( this, f, m, modEq, modInst ) ){ - Trace("inst-add") << " -> Already exists." << std::endl; + Trace("inst-add-debug") << " -> Already exists." << std::endl; ++(d_statistics.d_inst_duplicate); return false; } @@ -365,10 +365,12 @@ bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms ); //report the result if( addedInst ){ - Trace("inst-add") << " -> Success." << std::endl; + Trace("inst-add") << "Added instantiation for " << f << ": " << std::endl; + Trace("inst-add") << " " << m << std::endl; + Trace("inst-add-debug") << " -> Success." << std::endl; return true; }else{ - Trace("inst-add") << " -> Lemma already exists." << std::endl; + Trace("inst-add-debug") << " -> Lemma already exists." << std::endl; return false; } } @@ -567,38 +569,24 @@ QuantifiersEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_multi_candidates_cache_miss); } +eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){ + return ((quantifiers::TheoryQuantifiers*)getTheoryEngine()->theoryOf( THEORY_QUANTIFIERS ))->getMasterEqualityEngine(); +} + void EqualityQueryQuantifiersEngine::reset(){ d_int_rep.clear(); d_reset_count++; } bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){ - eq::EqualityEngine* ee = d_qe->getTheoryEngine()->getSharedTermsDatabase()->getEqualityEngine(); - if( ee->hasTerm( a ) ){ - return true; - } - for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){ - if( d_qe->getInstantiator( i ) ){ - if( d_qe->getInstantiator( i )->hasTerm( a ) ){ - return true; - } - } - } - return false; + return getEngine()->hasTerm( a ); } Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){ - eq::EqualityEngine* ee = d_qe->getTheoryEngine()->getSharedTermsDatabase()->getEqualityEngine(); + eq::EqualityEngine* ee = getEngine(); if( ee->hasTerm( a ) ){ return ee->getRepresentative( a ); } - for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){ - if( d_qe->getInstantiator( i ) ){ - if( d_qe->getInstantiator( i )->hasTerm( a ) ){ - return d_qe->getInstantiator( i )->getRepresentative( a ); - } - } - } return a; } @@ -606,47 +594,31 @@ bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){ if( a==b ){ return true; }else{ - eq::EqualityEngine* ee = d_qe->getTheoryEngine()->getSharedTermsDatabase()->getEqualityEngine(); + eq::EqualityEngine* ee = getEngine(); if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ if( ee->areEqual( a, b ) ){ return true; } } - for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){ - if( d_qe->getInstantiator( i ) ){ - if( d_qe->getInstantiator( i )->areEqual( a, b ) ){ - return true; - } - } - } - //std::cout << "Equal = " << eq_sh << " " << eq_uf << " " << eq_a << " " << eq_dt << std::endl; return false; } } bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){ - eq::EqualityEngine* ee = d_qe->getTheoryEngine()->getSharedTermsDatabase()->getEqualityEngine(); + eq::EqualityEngine* ee = getEngine(); if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ if( ee->areDisequal( a, b, false ) ){ return true; } } - for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){ - if( d_qe->getInstantiator( i ) ){ - if( d_qe->getInstantiator( i )->areDisequal( a, b ) ){ - return true; - } - } - } return false; - //std::cout << "Disequal = " << deq_sh << " " << deq_uf << " " << deq_a << " " << deq_dt << std::endl; } Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a ){ + Node r = getRepresentative( a ); if( !options::internalReps() ){ - return d_qe->getInstantiator( THEORY_UF )->getRepresentative( a ); + return r; }else{ - Node r = d_qe->getInstantiator( THEORY_UF )->getRepresentative( a ); if( d_int_rep.find( r )==d_int_rep.end() ){ std::vector< Node > eqc; getEquivalenceClass( r, eqc ); @@ -680,11 +652,11 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a ){ } eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){ - return ((uf::TheoryUF*)d_qe->getTheoryEngine()->theoryOf( THEORY_UF ))->getEqualityEngine(); + return d_qe->getMasterEqualityEngine(); } void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){ - eq::EqualityEngine* ee = d_qe->getTheoryEngine()->getSharedTermsDatabase()->getEqualityEngine(); + eq::EqualityEngine* ee = getEngine(); if( ee->hasTerm( a ) ){ Node rep = ee->getRepresentative( a ); eq::EqClassIterator eqc_iter( rep, ee ); @@ -692,13 +664,7 @@ void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< N eqc.push_back( *eqc_iter ); eqc_iter++; } - } - for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){ - if( d_qe->getInstantiator( i ) ){ - d_qe->getInstantiator( i )->getEquivalenceClass( a, eqc ); - } - } - if( eqc.empty() ){ + }else{ eqc.push_back( a ); } //a should be in its equivalence class diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 20972a6a1..719620e76 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -203,6 +203,7 @@ public: rrinst::TriggerTrie* getRRTriggerDatabase() { return d_rr_tr_trie; } /** add term to database */ void addTermToDatabase( Node n, bool withinQuant = false ); + eq::EqualityEngine* getMasterEqualityEngine() ; public: /** statistics class */ class Statistics { diff --git a/src/theory/rewriterules/efficient_e_matching.cpp b/src/theory/rewriterules/efficient_e_matching.cpp index 482e460ce..7f03bf8f8 100755 --- a/src/theory/rewriterules/efficient_e_matching.cpp +++ b/src/theory/rewriterules/efficient_e_matching.cpp @@ -19,6 +19,8 @@ #include "theory/rewriterules/options.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/theory_engine.h"
+
using namespace std;
using namespace CVC4;
using namespace CVC4::kind;
@@ -89,6 +91,10 @@ EfficientEMatcher::EfficientEMatcher( CVC4::theory::QuantifiersEngine* qe ) : d_ }
+eq::EqualityEngine* EfficientEMatcher::getEqualityEngine(){
+ return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getEqualityEngine();
+}
+
/** new node */
void EfficientEMatcher::newEqClass( TNode n ){
@@ -193,7 +199,7 @@ EqClassInfo* EfficientEMatcher::getEquivalenceClassInfo( Node n ) { return d_eqc_ops.find( n )==d_eqc_ops.end() ? NULL : d_eqc_ops[n];
}
EqClassInfo* EfficientEMatcher::getOrCreateEquivalenceClassInfo( Node n ){
- Assert( n==d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative( n ) );
+ Assert( n==getEqualityEngine()->getRepresentative( n ) );
if( d_eqc_ops.find( n )==d_eqc_ops.end() ){
EqClassInfo* eci = new EqClassInfo( d_quantEngine->getSatContext() );
eci->setMember( n, d_quantEngine->getTermDatabase() );
@@ -319,9 +325,9 @@ void EfficientEMatcher::computeCandidatesConstants( Node a, EqClassInfo* eci_a, itc != end; ++itc ) {
//The constant
Debug("efficient-e-match") << " Checking constant " << a << std::endl;
- if(d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative(itc->first) != a) continue;
+ if(getEqualityEngine()->getRepresentative(itc->first) != a) continue;
SetNode s;
- eq::EqClassIterator eqc_iter( b, d_quantEngine->getEqualityQuery()->getEngine() );
+ eq::EqClassIterator eqc_iter( b, getEqualityEngine() );
while( !eqc_iter.isFinished() ){
Debug("efficient-e-match-debug") << "> look at " << (*eqc_iter)
<< std::endl;
@@ -375,11 +381,11 @@ void EfficientEMatcher::collectTermsIps( Ips& ips, SetNode& terms, int index ){ bool EfficientEMatcher::collectParentsTermsIps( Node n, Node f, int arg, SetNode & terms, bool addRep, bool modEq ){ //modEq default true
bool addedTerm = false;
- if( modEq && d_quantEngine->getEqualityQuery()->getEngine()->hasTerm( n )){
- Assert( d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative( n )==n );
+ if( modEq && getEqualityEngine()->hasTerm( n )){
+ Assert( getEqualityEngine()->getRepresentative( n )==n );
//collect modulo equality
//DO_THIS: this should (if necessary) compute a current set of (f, arg) parents for n and cache it
- eq::EqClassIterator eqc_iter( n, d_quantEngine->getEqualityQuery()->getEngine() );
+ eq::EqClassIterator eqc_iter( n, getEqualityEngine() );
while( !eqc_iter.isFinished() ){
Debug("efficient-e-match-debug") << "> look at " << (*eqc_iter)
<< std::endl;
@@ -399,7 +405,7 @@ bool EfficientEMatcher::collectParentsTermsIps( Node n, Node f, int arg, SetNode for( size_t i=0; i<parents.size(); ++i ){
TNode t = parents[i];
if(!CandidateGenerator::isLegalCandidate(t)) continue;
- if( addRep ) t = d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative( t );
+ if( addRep ) t = getEqualityEngine()->getRepresentative( t );
terms.insert(t);
addedTerm = true;
}
@@ -617,9 +623,9 @@ void EfficientEMatcher::registerEfficientHandler( EfficientHandler& handler, } else if( pats[0].getKind() == kind::NOT && pats[0][0].getKind() == kind::EQUAL){
Node cst = NodeManager::currentNM()->mkConst<bool>(false);
TNode op = pats[0][0].getOperator();
- cst = d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative(cst);
+ cst = getEqualityEngine()->getRepresentative(cst);
SetNode ele;
- eq::EqClassIterator eqc_iter( cst, d_quantEngine->getEqualityQuery()->getEngine() );
+ eq::EqClassIterator eqc_iter( cst, getEqualityEngine() );
while( !eqc_iter.isFinished() ){
Debug("efficient-e-match-debug") << "> look at " << (*eqc_iter)
<< std::endl;
@@ -652,9 +658,9 @@ void EfficientEMatcher::registerEfficientHandler( EfficientHandler& handler, }
void EfficientEMatcher::outputEqClass( const char* c, Node n ){
- if( d_quantEngine->getEqualityQuery()->getEngine()->hasTerm( n ) ){
- eq::EqClassIterator eqc_iter( d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative( n ),
- d_quantEngine->getEqualityQuery()->getEngine() );
+ if( getEqualityEngine()->hasTerm( n ) ){
+ eq::EqClassIterator eqc_iter( getEqualityEngine()->getRepresentative( n ),
+ getEqualityEngine() );
bool firstTime = true;
while( !eqc_iter.isFinished() ){
if( !firstTime ){ Debug(c) << ", "; }
diff --git a/src/theory/rewriterules/efficient_e_matching.h b/src/theory/rewriterules/efficient_e_matching.h index ea06ad06e..2f0a07184 100755 --- a/src/theory/rewriterules/efficient_e_matching.h +++ b/src/theory/rewriterules/efficient_e_matching.h @@ -27,6 +27,8 @@ #include "context/cdqueue.h"
#include "context/cdo.h"
+#include "theory/uf/equality_engine.h"
+
namespace CVC4 {
namespace theory {
@@ -374,6 +376,8 @@ public: delete(i->second.second);
}
}
+ /** get equality engine we are using */
+ eq::EqualityEngine* getEqualityEngine();
private:
//information for each equivalence class
std::map< Node, EqClassInfo* > d_eqc_ops;
@@ -390,7 +394,6 @@ public: typedef std::vector< std::pair< Node, int > > Ips;
typedef std::map< Node, std::vector< std::pair< Node, Ips > > > PpIpsMap;
typedef std::map< Node, std::vector< triple< size_t, Node, Ips > > > MultiPpIpsMap;
-
private:
/** Parent/Child Pairs (for efficient E-matching)
So, for example, if we have the pattern f( g( x ) ), then d_pc_pairs[g][f][f( g( x ) )] = { f.0 }.
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 1742a32a5..ce3ccebf3 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -44,6 +44,8 @@ #include "theory/uf/equality_engine.h" +#include "theory/rewriterules/efficient_e_matching.h" + using namespace std; using namespace CVC4; @@ -52,7 +54,7 @@ using namespace CVC4::theory; void TheoryEngine::finishInit() { if (d_logicInfo.isQuantified()) { Assert(d_masterEqualityEngine == 0); - d_masterEqualityEngine = new eq::EqualityEngine(getSatContext(), "theory::master"); + d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master"); for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { if (d_theoryTable[theoryId]) { @@ -62,6 +64,23 @@ void TheoryEngine::finishInit() { } } +void TheoryEngine::eqNotifyNewClass(TNode t){ + d_quantEngine->addTermToDatabase( t ); +} + +void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){ + //TODO: add notification to efficient E-matching +} + +void TheoryEngine::eqNotifyPostMerge(TNode t1, TNode t2){ + +} + +void TheoryEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){ + +} + + TheoryEngine::TheoryEngine(context::Context* context, context::UserContext* userContext, RemoveITE& iteRemover, @@ -73,6 +92,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_logicInfo(logicInfo), d_sharedTerms(this, context), d_masterEqualityEngine(NULL), + d_masterEENotify(*this), d_quantEngine(NULL), d_curr_model(NULL), d_curr_model_builder(NULL), diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index de872db42..4a1ab4ca0 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -43,6 +43,7 @@ #include "util/cvc4_assert.h" #include "theory/ite_simplifier.h" #include "theory/unconstrained_simplifier.h" +#include "theory/uf/equality_engine.h" namespace CVC4 { @@ -133,6 +134,30 @@ class TheoryEngine { */ theory::eq::EqualityEngine* d_masterEqualityEngine; + /** notify class for master equality engine */ + class NotifyClass : public theory::eq::EqualityEngineNotify { + TheoryEngine& d_te; + public: + NotifyClass(TheoryEngine& te): d_te(te) {} + bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; } + bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; } + bool eqNotifyTriggerTermEquality(theory::TheoryId tag, TNode t1, TNode t2, bool value) { return true; } + void eqNotifyConstantTermMerge(TNode t1, TNode t2) {} + void eqNotifyNewClass(TNode t) { d_te.eqNotifyNewClass(t); } + void eqNotifyPreMerge(TNode t1, TNode t2) { d_te.eqNotifyPreMerge(t1, t2); } + void eqNotifyPostMerge(TNode t1, TNode t2) { d_te.eqNotifyPostMerge(t1, t2); } + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { d_te.eqNotifyDisequal(t1, t2, reason); } + };/* class TheoryEngine::NotifyClass */ + NotifyClass d_masterEENotify; + + /** + * notification methods + */ + void eqNotifyNewClass(TNode t); + void eqNotifyPreMerge(TNode t1, TNode t2); + void eqNotifyPostMerge(TNode t1, TNode t2); + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); + /** * The quantifiers engine */ diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp index 433ceee85..8c90d569a 100644 --- a/src/theory/uf/inst_strategy.cpp +++ b/src/theory/uf/inst_strategy.cpp @@ -75,10 +75,11 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){ if( processTrigger ){ //if( d_user_gen[f][i]->isMultiTrigger() ) //Notice() << " Process (user) " << (*d_user_gen[f][i]) << " for " << f << "..." << std::endl; - int numInst = d_user_gen[f][i]->addInstantiations( d_th->d_baseMatch[f] ); + 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_th->d_statistics.d_instantiations_user_pattern += numInst; + //d_statistics.d_instantiations += numInst; if( d_user_gen[f][i]->isMultiTrigger() ){ d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst; } @@ -106,6 +107,17 @@ void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){ 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 @@ -153,14 +165,15 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) if( processTrigger ){ //if( tr->isMultiTrigger() ) Debug("quant-uf-strategy-auto-gen-triggers") << " Process " << (*tr) << "..." << std::endl; - int numInst = tr->addInstantiations( d_th->d_baseMatch[f] ); + 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_th->d_statistics.d_instantiations_auto_gen_min += numInst; - }else{ - d_th->d_statistics.d_instantiations_auto_gen += numInst; - } + //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; } @@ -321,6 +334,20 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ } } } +/* +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 ){ } @@ -334,10 +361,21 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ Debug("quant-uf-alg") << "Add guessed instantiation" << std::endl; InstMatch m; if( d_quantEngine->addInstantiation( f, m ) ){ - ++(d_th->d_statistics.d_instantiations_guess); + //++(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 diff --git a/src/theory/uf/inst_strategy.h b/src/theory/uf/inst_strategy.h index aaa5f27a1..42d401126 100644 --- a/src/theory/uf/inst_strategy.h +++ b/src/theory/uf/inst_strategy.h @@ -58,6 +58,15 @@ public: 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{ @@ -114,6 +123,16 @@ public: } /** 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{ @@ -131,6 +150,15 @@ public: ~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 */ diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index e6ae3747c..23f100f74 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -22,6 +22,8 @@ #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,13 +481,13 @@ void TheoryUF::eqNotifyNewClass(TNode t) { } // this can be called very early, during initialization if (!getLogicInfo().isLocked() || getLogicInfo().isQuantified()) { - ((InstantiatorTheoryUf*) getInstantiator())->newEqClass(t); + //getQuantifiersEngine()->addTermToDatabase( t ); } } void TheoryUF::eqNotifyPreMerge(TNode t1, TNode t2) { if (getLogicInfo().isQuantified()) { - ((InstantiatorTheoryUf*) getInstantiator())->merge(t1, t2); + getQuantifiersEngine()->getEfficientEMatcher()->merge( t1, t2 ); } } @@ -499,9 +501,6 @@ void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { if (d_thss != NULL) { d_thss->assertDisequal(t1, t2, reason); } - if (getLogicInfo().isQuantified()) { - ((InstantiatorTheoryUf*) getInstantiator())->assertDisequal(t1, t2, reason); - } } Node TheoryUF::ppRewrite(TNode node) { diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp index e45842481..9ae6bbd37 100644 --- a/src/theory/uf/theory_uf_instantiator.cpp +++ b/src/theory/uf/theory_uf_instantiator.cpp @@ -41,6 +41,7 @@ Instantiator( c, qe, th ) //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 ); @@ -69,7 +70,7 @@ void InstantiatorTheoryUf::assertNode( Node assertion ) { Debug("quant-uf-assert") << "InstantiatorTheoryUf::check: " << assertion << std::endl; //preRegisterTerm( assertion ); - d_quantEngine->addTermToDatabase( assertion ); + //INST_ELIM_TRY//d_quantEngine->addTermToDatabase( assertion ); if( options::cbqi() ){ if( assertion.hasAttribute(InstConstantAttribute()) ){ setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) ); @@ -150,52 +151,6 @@ void InstantiatorTheoryUf::getEquivalenceClass( Node a, std::vector< Node >& eqc } } -InstantiatorTheoryUf::Statistics::Statistics(): - //d_instantiations("InstantiatorTheoryUf::Total_Instantiations", 0), - d_instantiations_ce_solved("InstantiatorTheoryUf::Instantiations_CE-Solved", 0), - d_instantiations_e_induced("InstantiatorTheoryUf::Instantiations_E-Induced", 0), - d_instantiations_user_pattern("InstantiatorTheoryUf::Instantiations_User_Pattern", 0), - d_instantiations_guess("InstantiatorTheoryUf::Instantiations_Free_Var", 0), - d_instantiations_auto_gen("InstantiatorTheoryUf::Instantiations_Auto_Gen", 0), - d_instantiations_auto_gen_min("InstantiatorTheoryUf::Instantiations_Auto_Gen_Min", 0), - d_splits("InstantiatorTheoryUf::Total_Splits", 0) -{ - //StatisticsRegistry::registerStat(&d_instantiations); - StatisticsRegistry::registerStat(&d_instantiations_ce_solved); - StatisticsRegistry::registerStat(&d_instantiations_e_induced); - StatisticsRegistry::registerStat(&d_instantiations_user_pattern ); - StatisticsRegistry::registerStat(&d_instantiations_guess ); - StatisticsRegistry::registerStat(&d_instantiations_auto_gen ); - StatisticsRegistry::registerStat(&d_instantiations_auto_gen_min ); - StatisticsRegistry::registerStat(&d_splits); -} - -InstantiatorTheoryUf::Statistics::~Statistics(){ - //StatisticsRegistry::unregisterStat(&d_instantiations); - StatisticsRegistry::unregisterStat(&d_instantiations_ce_solved); - StatisticsRegistry::unregisterStat(&d_instantiations_e_induced); - StatisticsRegistry::unregisterStat(&d_instantiations_user_pattern ); - StatisticsRegistry::unregisterStat(&d_instantiations_guess ); - StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen ); - StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen_min ); - StatisticsRegistry::unregisterStat(&d_splits); -} - -/** new node */ -void InstantiatorTheoryUf::newEqClass( TNode n ){ - d_quantEngine->addTermToDatabase( n ); -} - -/** merge */ -void InstantiatorTheoryUf::merge( TNode a, TNode b ){ - d_quantEngine->getEfficientEMatcher()->merge( a, b ); -} - -/** assert terms are disequal */ -void InstantiatorTheoryUf::assertDisequal( TNode a, TNode b, TNode reason ){ - -} - void InstantiatorTheoryUf::outputEqClass( const char* c, Node n ){ if( ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( n ) ){ eq::EqClassIterator eqc_iter( getRepresentative( n ), diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h index b5a3aa765..fe34c9487 100644 --- a/src/theory/uf/theory_uf_instantiator.h +++ b/src/theory/uf/theory_uf_instantiator.h @@ -40,15 +40,6 @@ namespace quantifiers{ namespace uf { class InstantiatorTheoryUf : public Instantiator{ - friend class ::CVC4::theory::inst::InstMatchGenerator; - friend class ::CVC4::theory::quantifiers::TermDb; -protected: - typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap; - typedef context::CDHashMap<Node, int, NodeHashFunction> IntMap; - typedef context::CDChunkList<Node> NodeList; - typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeLists; - /** map to representatives used */ - //std::map< Node, Node > d_ground_reps; protected: /** instantiation strategies */ InstStrategyUserPatterns* d_isup; @@ -71,25 +62,6 @@ private: /** calculate matches for quantifier f at effort */ int process( Node f, Theory::Effort effort, int e ); public: - /** statistics class */ - class Statistics { - public: - //IntStat d_instantiations; - IntStat d_instantiations_ce_solved; - IntStat d_instantiations_e_induced; - IntStat d_instantiations_user_pattern; - IntStat d_instantiations_guess; - IntStat d_instantiations_auto_gen; - IntStat d_instantiations_auto_gen_min; - IntStat d_splits; - Statistics(); - ~Statistics(); - }; - Statistics d_statistics; -public: - /** the base match */ - std::map< Node, InstMatch > d_baseMatch; -public: /** general queries about equality */ bool hasTerm( Node a ); bool areEqual( Node a, Node b ); @@ -101,34 +73,12 @@ public: /** general creators of candidate generators */ rrinst::CandidateGenerator* getRRCanGenClasses(); rrinst::CandidateGenerator* getRRCanGenClass(); - /** new node */ - void newEqClass( TNode n ); - /** merge */ - void merge( TNode a, TNode b ); - /** assert terms are disequal */ - void assertDisequal( TNode a, TNode b, TNode reason ); public: /** output eq class */ void outputEqClass( const char* c, Node n ); };/* class InstantiatorTheoryUf */ -/** equality query object using instantiator theory uf */ -class EqualityQueryInstantiatorTheoryUf : public EqualityQuery -{ -private: - /** pointer to instantiator uf class */ - InstantiatorTheoryUf* d_ith; -public: - EqualityQueryInstantiatorTheoryUf( InstantiatorTheoryUf* ith ) : d_ith( ith ){} - ~EqualityQueryInstantiatorTheoryUf(){} - /** general queries about equality */ - bool hasTerm( Node a ) { return d_ith->hasTerm( a ); } - Node getRepresentative( Node a ) { return d_ith->getRepresentative( a ); } - bool areEqual( Node a, Node b ) { return d_ith->areEqual( a, b ); } - bool areDisequal( Node a, Node b ) { return d_ith->areDisequal( a, b ); } - eq::EqualityEngine* getEngine() { return d_ith->getEqualityEngine(); } - void getEquivalenceClass( Node a, std::vector< Node >& eqc ) { d_ith->getEquivalenceClass( a, eqc ); } -}; /* EqualityQueryInstantiatorTheoryUf */ + } }/* CVC4::theory namespace */ |