From aa3b60104a0026c078eea1d19506e8bf4c3d9763 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 23 May 2014 16:59:48 -0500
Subject: Fix bug in E-matching Real/Int terms.

---
 src/theory/quantifiers/candidate_generator.cpp  |  4 ++--
 src/theory/quantifiers/inst_match_generator.cpp |  6 ++++--
 src/theory/quantifiers/term_database.cpp        | 17 +++++++++++++++++
 src/theory/quantifiers/term_database.h          |  1 +
 4 files changed, 24 insertions(+), 4 deletions(-)

(limited to 'src/theory')

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 9b5e506ea..799513171 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -175,7 +175,7 @@ Node CandidateGeneratorQELitEq::getNextCandidate(){
   while( !d_eq.isFinished() ){
     Node n = (*d_eq);
     ++d_eq;
-    if( n.getType()==d_match_pattern[0].getType() ){
+    if( n.getType().isSubtypeOf( d_match_pattern[0].getType() ) ){
       //an equivalence class with the same type as the pattern, return reflexive equality
       return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n );
     }
@@ -228,7 +228,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() {
   while( !d_eq.isFinished() ){
     Node n = (*d_eq);
     ++d_eq;
-    if( n.getType()==d_match_pattern.getType() ){
+    if( n.getType().isSubtypeOf( d_match_pattern.getType() ) ){
       //an equivalence class with the same type as the pattern, return it
       return n;
     }
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index da0a3c4f6..9031104c8 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -32,6 +32,7 @@ namespace inst {
 
 
 InstMatchGenerator::InstMatchGenerator( Node pat, int matchPolicy ) : d_matchPolicy( matchPolicy ){
+  d_needsReset = true;
   d_active_add = false;
   Assert( quantifiers::TermDb::hasInstConstAttr(pat) );
   d_pattern = pat;
@@ -298,7 +299,7 @@ bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine*
     t = d_cg->getNextCandidate();
     Trace("matching-debug2") << "Matching candidate : " << t << std::endl;
     //if t not null, try to fit it into match m
-    if( !t.isNull() && t.getType()==d_match_pattern.getType() ){
+    if( !t.isNull() && t.getType().isSubtypeOf( d_match_pattern.getType() ) ){
       success = getMatch( f, t, m, qe );
     }
   }while( !success && !t.isNull() );
@@ -628,6 +629,7 @@ int InstMatchGeneratorSimple::addInstantiations( Node f, InstMatch& baseMatch, Q
 }
 
 void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ){
+  Debug("simple-trigger-debug") << "Add inst " << argIndex << " " << d_match_pattern << std::endl;
   if( argIndex==(int)d_match_pattern.getNumChildren() ){
     //m is an instantiation
     if( qe->addInstantiation( d_f, m ) ){
@@ -640,7 +642,7 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin
       for( std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
         Node t = it->first;
         Node prev = m.get( v );
-        if( ( prev.isNull() || prev==t ) && d_match_pattern[argIndex].getType()==t.getType() ){
+        if( ( prev.isNull() || prev==t ) && t.getType().isSubtypeOf( d_match_pattern[argIndex].getType() ) ){
           m.setValue( v, t);
           addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
           m.setValue( v, prev);
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 64965f5ce..36859ddaa 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -48,6 +48,14 @@ bool TermArgTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){
   }
 }
 
+void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) {
+  for( std::map< Node, TermArgTrie >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
+    for( unsigned i=0; i<depth; i++ ){ Debug(c) << "  "; }
+    Debug(c) << it->first << std::endl;
+    it->second.debugPrint( c, n, depth+1 );
+  }
+}
+
 TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ) {
 
 }
@@ -204,6 +212,15 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
    Debug("term-db-cong") << "TermDb: Reset" << std::endl;
    Debug("term-db-cong") << "Congruent/Non-Congruent = ";
    Debug("term-db-cong") << congruentCount << "(" << alreadyCongruentCount << ") / " << nonCongruentCount << std::endl;
+   if( Debug.isOn("term-db") ){
+      Debug("term-db") << "functions : " << std::endl;
+      for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
+        if( it->second.size()>0 ){
+          Debug("term-db") << "- " << it->first << std::endl;
+          d_func_map_trie[ it->first ].debugPrint("term-db", it->second[0]);
+        }
+      }
+   }
 }
 
 Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 2a72cf808..2592e1fd6 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -76,6 +76,7 @@ public:
   std::map< Node, TermArgTrie > d_data;
 public:
   bool addTerm( QuantifiersEngine* qe, Node n ) { return addTerm2( qe, n, 0 ); }
+  void debugPrint( const char * c, Node n, unsigned depth = 0 );
 };/* class TermArgTrie */
 
 
-- 
cgit v1.2.3