From ccc9cd5aad5248b4a2c86b617d76bc98063a7ea2 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 31 Mar 2016 14:36:25 -0500
Subject: Improvements to trigger selection, min triggers by default.
 Optimizations for E-matching. Minor work to equality infer.

---
 src/theory/quantifiers/candidate_generator.h | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'src/theory/quantifiers/candidate_generator.h')

diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h
index 9d8e318aa..f40114897 100644
--- a/src/theory/quantifiers/candidate_generator.h
+++ b/src/theory/quantifiers/candidate_generator.h
@@ -23,6 +23,10 @@
 namespace CVC4 {
 namespace theory {
 
+namespace quantifiers {
+  class TermArgTrie;
+}
+
 class QuantifiersEngine;
 
 namespace inst {
@@ -79,6 +83,9 @@ private:
   //instantiator pointer
   QuantifiersEngine* d_qe;
   //the equality class iterator
+  unsigned d_op_arity;
+  std::vector< quantifiers::TermArgTrie* > d_tindex;
+  std::vector< std::map< TNode, quantifiers::TermArgTrie >::iterator > d_tindex_iter;
   eq::EqClassIterator d_eqc_iter;
   //std::vector< Node > d_eqc;
   int d_term_iter;
@@ -88,6 +95,7 @@ private:
     cand_term_db,
     cand_term_ident,
     cand_term_eqc,
+    cand_term_tindex,
     cand_term_none,
   };
   short d_mode;
@@ -95,7 +103,7 @@ private:
   Node d_n;
   std::map< Node, bool > d_exclude_eqc;
 public:
-  CandidateGeneratorQE( QuantifiersEngine* qe, Node op );
+  CandidateGeneratorQE( QuantifiersEngine* qe, Node pat );
   ~CandidateGeneratorQE() throw() {}
 
   void resetInstantiationRound();
-- 
cgit v1.2.3