Module to infer alpha equivalence of quantified formulas. Minor clean up of options.

1 files changed, 1 insertions, 6 deletions

diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 6f99777f4..3aa932296 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -171,6 +171,7 @@ public:
   bool considerCurrentTermCanon( unsigned tg_id );
   void changeContext( bool add );
   bool isRelevantFunc( Node f );
+  bool isRelevantTerm( Node t );
   //carry
   TermDb * getTermDatabase();
   Node getGroundEqc( TNode r );
@@ -307,14 +308,8 @@ private:  //information regarding the conjectures
   /** conjecture index */
   TheoremIndex d_thm_index;
 private:  //free variable list
-  //free variables
-  std::map< TypeNode, std::vector< Node > > d_free_var;
-  //map from free variable to FV#
-  std::map< TNode, unsigned > d_free_var_num;
   // get canonical free variable #i of type tn
   Node getFreeVar( TypeNode tn, unsigned i );
-  // get canonical term, return null if it contains a term apart from handled signature
-  Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs );
 private:  //information regarding the terms
   //relevant patterns (the LHS's)
   std::map< TypeNode, std::vector< Node > > d_rel_patterns;