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/theory/quantifiers | |
| parent | 6369830eec077ef112e6cc806cd910c7209eb2db (diff) | |
quantifiers now uses master equality engine, preparation work to cleanup code
Diffstat (limited to 'src/theory/quantifiers')
| -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 |
3 files changed, 8 insertions, 4 deletions
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 ){ |