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

1 files changed, 4 insertions, 3 deletions

diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 426adc02d..43c0d26c7 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -55,9 +55,9 @@ public:
   /** is complete? */
   bool isComplete( Node f ) { return d_map.size()==f[0].getNumChildren(); }
   /** make complete */
-  void makeComplete( Node f, QuantifiersEngine* qe );
+  //void makeComplete( Node f, QuantifiersEngine* qe );
   /** make internal: ensure that no term in d_map contains instantiation constants */
-  void makeInternal( QuantifiersEngine* qe );
+  //void makeInternal( QuantifiersEngine* qe );
   /** make representative */
   void makeRepresentative( QuantifiersEngine* qe );
   /** get value */
@@ -96,7 +96,8 @@ public:
     //std::cout << "var.getType() " << var.getType() << "n.getType() " << n.getType() << std::endl ;
     Assert( !var.isNull() );
     Assert( n.isNull() ||// For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations
-            var.getType() == n.getType() );
+            //var.getType() == n.getType()
+            n.getType().isSubtypeOf( var.getType() ) );
     d_map[var] = n;
   }
   size_t size(){ return d_map.size(); }