diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-23 23:40:29 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-23 23:40:29 +0000 |
commit | 304404e3709ff7e95156c87f65a3e2647d9f3441 (patch) | |
tree | 10fd1c4cc42567c3fac5fd91ad76aef3d49975b5 /src/theory/quantifiers/trigger.cpp | |
parent | 697dd317af39a896865c99b922e80baac2bb4b23 (diff) |
more major cleanup of quantifiers code, separating rewrite-rules-specific code from quantifiers-specific code
Diffstat (limited to 'src/theory/quantifiers/trigger.cpp')
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 36 |
1 files changed, 34 insertions, 2 deletions
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 90a673715..c64a75ec4 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -20,6 +20,7 @@ #include "theory/uf/equality_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; @@ -97,6 +98,10 @@ int Trigger::addTerm( Node t ){ return d_mg->addTerm( d_f, t, d_quantEngine ); } +//bool Trigger::nonunifiable( TNode t, const std::vector<Node> & vars){ +// return d_mg->nonunifiable(t,vars); +//} + int Trigger::addInstantiations( InstMatch& baseMatch ){ int addedLemmas = d_mg->addInstantiations( d_f, baseMatch, d_quantEngine ); if( addedLemmas>0 ){ @@ -183,7 +188,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& // Notice() << "Trigger new old = " << trNew << " " << trOld << std::endl; //} }else{ - Trigger* t = qe->getTermDatabase()->getTrigger( trNodes ); + Trigger* t = qe->getTriggerDatabase()->getTrigger( trNodes ); if( t ){ if( trOption==TR_GET_OLD ){ //just return old trigger @@ -194,7 +199,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& } } Trigger* t = new Trigger( qe, f, trNodes, matchOption, smartTriggers ); - qe->getTermDatabase()->addTrigger( trNodes, t ); + qe->getTriggerDatabase()->addTrigger( trNodes, t ); return t; } Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption, bool smartTriggers ){ @@ -470,3 +475,30 @@ bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coef } return false; } + +Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){ + if( nodes.empty() ){ + return d_tr; + }else{ + Node n = nodes.back(); + nodes.pop_back(); + if( d_children.find( n )!=d_children.end() ){ + return d_children[n]->getTrigger2( nodes ); + }else{ + return NULL; + } + } +} + +void TriggerTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){ + if( nodes.empty() ){ + d_tr = t; + }else{ + Node n = nodes.back(); + nodes.pop_back(); + if( d_children.find( n )==d_children.end() ){ + d_children[n] = new TriggerTrie; + } + d_children[n]->addTrigger2( nodes, t ); + } +} |