summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/arith/theory_arith_instantiator.cpp2
-rw-r--r--src/theory/arrays/theory_arrays_instantiator.cpp2
-rw-r--r--src/theory/datatypes/theory_datatypes_instantiator.cpp2
-rw-r--r--src/theory/quantifiers/term_database.cpp1
-rw-r--r--src/theory/quantifiers/theory_quantifiers.h1
-rw-r--r--src/theory/quantifiers/trigger.cpp10
-rw-r--r--src/theory/quantifiers_engine.cpp72
-rw-r--r--src/theory/quantifiers_engine.h1
-rwxr-xr-xsrc/theory/rewriterules/efficient_e_matching.cpp30
-rwxr-xr-xsrc/theory/rewriterules/efficient_e_matching.h5
-rw-r--r--src/theory/theory_engine.cpp22
-rw-r--r--src/theory/theory_engine.h25
-rw-r--r--src/theory/uf/inst_strategy.cpp56
-rw-r--r--src/theory/uf/inst_strategy.h28
-rw-r--r--src/theory/uf/theory_uf.cpp9
-rw-r--r--src/theory/uf/theory_uf_instantiator.cpp49
-rw-r--r--src/theory/uf/theory_uf_instantiator.h52
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback