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.h | |
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.h')
-rw-r--r-- | src/theory/quantifiers/trigger.h | 37 |
1 files changed, 32 insertions, 5 deletions
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 945b5db2a..267debb02 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -18,11 +18,19 @@ #define __CVC4__THEORY__QUANTIFIERS__TRIGGER_H #include "theory/quantifiers/inst_match.h" +#include "expr/node.h" +#include "util/hash.h" +#include <map> namespace CVC4 { namespace theory { + +class QuantifiersEngine; + namespace inst { +class IMGenerator; + //a collect of nodes representing a trigger class Trigger { private: @@ -56,11 +64,6 @@ public: bool getMatch( Node t, InstMatch& m); /** add ground term t, called when t is added to the TermDb */ int addTerm( Node t ); - /** return true if whatever Node is subsituted for the variables the - given Node can't match the pattern */ - bool nonunifiable( TNode t, const std::vector<Node> & vars){ - return d_mg->nonunifiable(t,vars); - } /** return whether this is a multi-trigger */ bool isMultiTrigger() { return d_nodes.size()>1; } public: @@ -127,6 +130,30 @@ inline std::ostream& operator<<(std::ostream& out, const Trigger & tr) { return out; } + +/** a trie of triggers */ +class TriggerTrie { +private: + inst::Trigger* getTrigger2( std::vector< Node >& nodes ); + void addTrigger2( std::vector< Node >& nodes, inst::Trigger* t ); +public: + TriggerTrie() : d_tr( NULL ){} + inst::Trigger* d_tr; + std::map< TNode, TriggerTrie* > d_children; + inst::Trigger* getTrigger( std::vector< Node >& nodes ){ + std::vector< Node > temp; + temp.insert( temp.begin(), nodes.begin(), nodes.end() ); + std::sort( temp.begin(), temp.end() ); + return getTrigger2( temp ); + } + void addTrigger( std::vector< Node >& nodes, inst::Trigger* t ){ + std::vector< Node > temp; + temp.insert( temp.begin(), nodes.begin(), nodes.end() ); + std::sort( temp.begin(), temp.end() ); + return addTrigger2( temp, t ); + } +};/* class inst::Trigger::Trigger */ + }/* CVC4::theory::inst namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |