diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-31 14:36:25 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-31 14:36:25 -0500 |
| commit | ccc9cd5aad5248b4a2c86b617d76bc98063a7ea2 (patch) | |
| tree | cd710b7174eb3724d1b08c3261f69c7e4745a4d0 /src/theory/quantifiers/term_database.h | |
| parent | 2abcda1cfcb0c6388c00d65f8a6b3e63de9d96df (diff) | |
Improvements to trigger selection, min triggers by default. Optimizations for E-matching. Minor work to equality infer.
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
| -rw-r--r-- | src/theory/quantifiers/term_database.h | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 62da8c347..dc1f9990b 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -126,6 +126,8 @@ public: /** the data */ std::map< TNode, TermArgTrie > d_data; public: + bool hasNodeData() { return !d_data.empty(); } + TNode getNodeData() { return d_data.begin()->first; } TNode existsTerm( std::vector< TNode >& reps, int argIndex = 0 ); TNode addOrGetTerm( TNode n, std::vector< TNode >& reps, int argIndex = 0 ); bool addTerm( TNode n, std::vector< TNode >& reps, int argIndex = 0 ); @@ -358,26 +360,26 @@ public: //for triggers private: /** helper function for compute var contains */ - void computeVarContains2( Node n, std::vector< Node >& varContains, std::map< Node, bool >& visited ); + static void computeVarContains2( Node n, std::vector< Node >& varContains, std::map< Node, bool >& visited ); /** triggers for each operator */ std::map< Node, std::vector< inst::Trigger* > > d_op_triggers; /** helper for is instance of */ - bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs ); + static bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs ); /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */ - int isInstanceOf2( Node n1, Node n2, std::vector< Node >& varContains1, std::vector< Node >& varContains2 ); + static int isInstanceOf2( Node n1, Node n2, std::vector< Node >& varContains1, std::vector< Node >& varContains2 ); public: /** compute var contains */ - void computeVarContains( Node n, std::vector< Node >& varContains ); + static void computeVarContains( Node n, std::vector< Node >& varContains ); /** get var contains for each of the patterns in pats */ - void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ); + static void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ); /** get var contains for node n */ - void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ); - /** register trigger (for eager quantifier instantiation) */ - void registerTrigger( inst::Trigger* tr, Node op ); + static void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ); /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */ - int isInstanceOf( Node n1, Node n2 ); + static int isInstanceOf( Node n1, Node n2 ); /** filter all nodes that have instances */ - void filterInstances( std::vector< Node >& nodes ); + static void filterInstances( std::vector< Node >& nodes ); + /** register trigger (for eager quantifier instantiation) */ + void registerTrigger( inst::Trigger* tr, Node op ); //for term ordering private: |