cleaning up some of the equality query stuff, implemented a new representative selection strategy for quantifier instantiation

1 files changed, 3 insertions, 5 deletions

diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index d0348dff8..7331daf8e 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -23,6 +23,7 @@
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 
 /** Attribute true for nodes that should not be used when considered for inst-gen basis */
 struct BasisNoMatchAttributeId {};
@@ -35,17 +36,14 @@ typedef expr::Attribute< BasisNoMatchAttributeId,
 
 class TermArgBasisTrie {
 private:
-  bool addTerm2( QuantifiersEngine* qe, Node n, int argIndex );
+  bool addTerm2( FirstOrderModel* fm, Node n, int argIndex );
 public:
   /** the data */
   std::map< Node, TermArgBasisTrie > d_data;
 public:
-  bool addTerm( QuantifiersEngine* qe, Node n ) { return addTerm2( qe, n, 0 ); }
+  bool addTerm( FirstOrderModel* fm, Node n ) { return addTerm2( fm, n, 0 ); }
 };/* class TermArgBasisTrie */
 
-
-namespace quantifiers {
-
 /** model builder class
   *  This class is capable of building candidate models based on the current quantified formulas
   *  that are asserted.  Use: