Bug fix for E-matching select terms, minor fix for bounded integers, bug fix to improve performance of quantifiers rewriter

7 files changed, 55 insertions, 24 deletions

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index ab6b35e01..080550a16 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -174,15 +174,15 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol,
               veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 );
             }
             Trace("bound-int-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;
-            Node bv = n1.getKind()==BOUND_VARIABLE ? n1 : n2;
-            if( !isBound( f, bv ) ){
-              if( !hasNonBoundVar( f, n1.getKind()==BOUND_VARIABLE ? n2 : n1 ) ) {
-                Trace("bound-int-debug") << "The bound is relevant." << std::endl;
-                int loru = n1.getKind()==BOUND_VARIABLE ? 0 : 1;
-                d_bounds[loru][f][bv] = (n1.getKind()==BOUND_VARIABLE ? n2 : n1);
-                bound_lit_map[loru][bv] = lit;
-                bound_lit_pol_map[loru][bv] = pol;
-              }
+            Node t = n1==it->first ? n2 : n1;
+            if( !hasNonBoundVar( f, t ) ) {
+              Trace("bound-int-debug") << "The bound is relevant." << std::endl;
+              int loru = n1==it->first ? 0 : 1;
+              d_bounds[loru][f][it->first] = t;
+              bound_lit_map[loru][it->first] = lit;
+              bound_lit_pol_map[loru][it->first] = pol;
+            }else{
+              Trace("bound-int-debug") << "The term " << t << " has non-bound variable." << std::endl;
             }
           }
         }
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index d55f72a88..ebe587765 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -36,7 +36,10 @@ InstMatch::InstMatch( InstMatch* m ) {
 
 bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m, bool & set ){
   std::map< Node, Node >::iterator vn = d_map.find( v );
-  if( vn==d_map.end() || vn->second.isNull() ){
+  if( !m.isNull() && !m.getType().isSubtypeOf( v.getType() ) ){
+    set = false;
+    return false;
+  }else if( vn==d_map.end() || vn->second.isNull() ){
     set = true;
     this->set(v,m);
     Debug("matching-debug") << "Add partial " << v << "->" << m << std::endl;
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 8e1083b7b..9cd12fbfb 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -119,7 +119,7 @@ bool QuantifierMacros::containsBadOp( Node n, Node n_op ){
 }
 
 bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){
-  return pol && n.getKind()==EQUAL;//( n.getKind()==EQUAL || n.getKind()==IFF );
+  return pol && ( n.getKind()==EQUAL || n.getKind()==IFF );
 }
 
 void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidates ){
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 5ff21bcff..99f5e8df6 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -125,7 +125,26 @@ void ModelEngine::check( Theory::Effort e ){
 }
 
 void ModelEngine::registerQuantifier( Node f ){
-
+  if( Trace.isOn("fmf-warn") ){
+    bool canHandle = true;
+    for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+      TypeNode tn = f[0][i].getType();
+      if( !tn.isSort() ){
+        if( !tn.getCardinality().isFinite() ){
+          if( tn.isInteger() ){
+            if( !options::fmfBoundInt() ){
+              canHandle = false;
+            }
+          }else{
+            canHandle = false;
+          }
+        }
+      }
+    }
+    if( !canHandle ){
+      Trace("fmf-warn") << "Warning : Model Engine : may not be able to answer SAT because of formula : " << f << std::endl;
+    }
+  }
 }
 
 void ModelEngine::assertNode( Node f ){
@@ -207,11 +226,9 @@ int ModelEngine::checkModel(){
     }
   }
   //print debug information
-  if( Trace.isOn("model-engine") ){
-    Trace("model-engine") << "Instantiate axioms : " << ( d_builder->d_considerAxioms ? "yes" : "no" ) << std::endl;
-    Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
-    Trace("model-engine") << d_totalLemmas << std::endl;
-  }
+  Trace("model-engine-debug") << "Instantiate axioms : " << ( d_builder->d_considerAxioms ? "yes" : "no" ) << std::endl;
+  Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
+  Trace("model-engine") << d_totalLemmas << std::endl;
   d_statistics.d_exh_inst_lemmas += d_addedLemmas;
   return d_addedLemmas;
 }
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index e27897a96..ecc3c02bc 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -117,16 +117,25 @@ bool QuantifiersRewriter::hasArg( std::vector< Node >& args, Node n ){
 }
 
 void QuantifiersRewriter::setNestedQuantifiers( Node n, Node q ){
-  if( n.getKind()==FORALL || n.getKind()==EXISTS ){
-    Trace("quantifiers-rewrite-debug") << "Set nested quant attribute " << n << std::endl;
-    NestedQuantAttribute nqai;
-    n.setAttribute(nqai,q);
-  }
-  for( int i=0; i<(int)n.getNumChildren(); i++ ){
-    setNestedQuantifiers( n[i], q );
+  std::vector< Node > processed;
+  setNestedQuantifiers2( n, q, processed );
+}
+
+void QuantifiersRewriter::setNestedQuantifiers2( Node n, Node q, std::vector< Node >& processed ) {
+  if( std::find( processed.begin(), processed.end(), n )==processed.end() ){
+    processed.push_back( n );
+    if( n.getKind()==FORALL || n.getKind()==EXISTS ){
+      Trace("quantifiers-rewrite-debug") << "Set nested quant attribute " << n << std::endl;
+      NestedQuantAttribute nqai;
+      n.setAttribute(nqai,q);
+    }
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      setNestedQuantifiers2( n[i], q, processed );
+    }
   }
 }
 
+
 RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
   Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in << " " << in.hasAttribute(NestedQuantAttribute()) << std::endl;
   if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index be3e333f3..40234904f 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -41,6 +41,7 @@ private:
   static void computeArgs( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n );
   static bool hasArg( std::vector< Node >& args, Node n );
   static void setNestedQuantifiers( Node n, Node q );
+  static void setNestedQuantifiers2( Node n, Node q, std::vector< Node >& processed );
   static Node computeClause( Node n );
 private:
   static Node computeMiniscoping( std::vector< Node >& args, Node body, Node ipl, bool isNested = false );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 54aa7f726..e9a69bd30 100755
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -190,6 +190,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
 
 void QuantifiersEngine::registerQuantifier( Node f ){
   if( std::find( d_quants.begin(), d_quants.end(), f )==d_quants.end() ){
+    Trace("quant") << "Register quantifier : " << f << std::endl;
     d_quants.push_back( f );
 
     ++(d_statistics.d_num_quant);