Fix bug in E-matching Real/Int terms.

diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp
index b550c58a17cce01c8f226b91a04390d796e2ac8a..c96791aeb8c4cd9237ec5cb85b0b21929c4ba963 100644 (file)
--- a/proofs/lfsc_checker/check.cpp
+++ b/proofs/lfsc_checker/check.cpp
@@ -61,7 +61,7 @@ void report_error(const string &msg) {
     not_defeq2->print(cout);
   }
   cout.flush();
-  _exit(1);
+  exit(1);
 }
 
 Expr *call_run_code(Expr *code) {

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 9b5e506ead9b6a17afd47eab2f224396cbd78ad5..799513171105c940d0dd3a35ca5a084ff251483f 100644 (file)
--- 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 da0a3c4f67039d9fbffe635908d33b9a6589d873..9031104c87a8d3938bac0a8ae2375c1cbbf2ef92 100644 (file)
--- 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 64965f5ce0280d9a36fcf3884c781adb3d0d3771..36859ddaa4bb2b8023db9cd3bf485144f2f0ef73 100644 (file)
--- 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 2a72cf808c687b51b810d43926bb9b3f330dd7f7..2592e1fd646d648f17bf79e903322a3d9eb636aa 100644 (file)
--- 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 */
 
 

diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index e399b4b23b5b60b53c1404b2d0966eca69c07b9d..7e8e1ea9921e31399c9f1d59344222c10c1c7b9e 100644 (file)
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -42,7 +42,8 @@ TESTS =       \
        symmetric_unsat_7.smt2 \
        javafe.ast.StmtVec.009.smt2 \
        ARI176e1.smt2 \
-  bi-artm-s.smt2
+        bi-artm-s.smt2 \
+       simp-typ-test.smt2
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
 # set3.smt2

diff --git a/test/regress/regress0/quantifiers/simp-typ-test.smt2 b/test/regress/regress0/quantifiers/simp-typ-test.smt2
new file mode 100755 (executable)
index 0000000..366559b
--- /dev/null
+++ b/test/regress/regress0/quantifiers/simp-typ-test.smt2
@@ -0,0 +1,7 @@
+(set-logic UFLIRA)\r
+(set-info :status unsat)\r
+; ensure that E-matching matches on sub-types\r
+(declare-fun P (Real) Bool)\r
+(assert (forall ((x Real)) (P x)))\r
+(assert (not (P 5)))\r
+(check-sat)
\ No newline at end of file