More aggressive conditional rewriting for quantified formulas. Bug fix set incomplete for fmc.

3 files changed, 97 insertions, 46 deletions

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 00a5241f5..ff0da13e1 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -819,8 +819,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
       }
     }
     d_addedLemmas += addedLemmas;
-    Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << std::endl;
-    return true;
+    Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << ", incomplete=" << riter.d_incomplete << std::endl;
+    return addedLemmas>0 || !riter.d_incomplete;
   }else{
     Trace("fmc-exh") << "----Finished Exhaustive instantiate, failed." << std::endl;
     return false;
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index fc1f052c3..bf91f74c6 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -349,6 +349,9 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool&
   }else if( n.getKind()==ITE ){
     newHasPol = (child!=0) && hasPol;
     newPol = pol;
+  }else if( n.getKind()==FORALL ){
+    newHasPol = (child==1) && hasPol;
+    newPol = pol;
   }else{
     newHasPol = false;
     newPol = pol;
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 462f8377f..afe8cd598 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -391,7 +391,7 @@ Node QuantifiersRewriter::computeNNF( Node body ){
 void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons,
                                                    std::vector< Node >& conj ){
   if( n.getKind()==ITE && n[0].getKind()==APPLY_TESTER && n[1].getType().isBoolean() ){
-  Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl;
+    Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl;
     Node x = n[0][0];
     std::map< Node, Node >::iterator itp = pcons.find( x );
     if( itp!=pcons.end() ){
@@ -506,35 +506,42 @@ int getEntailedCond( Node n, std::map< Node, bool >& currCond ){
   return 0;
 }
 
-bool addEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond ) {
+bool addEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond, bool& conflict ) {
   std::map< Node, bool >::iterator it = currCond.find( n );
   if( it==currCond.end() ){
-    Trace("quantifiers-rewrite-ite-debug") << "ITE cond : " << n << " -> " << pol << std::endl;
+    Trace("quantifiers-rewrite-term-debug") << "cond : " << n << " -> " << pol << std::endl;
     new_cond.push_back( n );
     currCond[n] = pol;
     return true;
   }else{
-    Assert( it->second==pol );
+    if( it->second!=pol ){
+      Trace("quantifiers-rewrite-term-debug") << "CONFLICTING cond : " << n << " -> " << pol << std::endl;
+      conflict = true;
+    }
     return false;
   }
 }
 
-void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond ) {
+void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond, bool& conflict ) {
   if( ( n.getKind()==AND && pol ) || ( n.getKind()==OR && !pol ) ){
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      setEntailedCond( n[i], pol, currCond, new_cond );
+      setEntailedCond( n[i], pol, currCond, new_cond, conflict );
+      if( conflict ){
+        break;
+      }
     }
   }else if( n.getKind()==NOT ){
-    setEntailedCond( n[0], !pol, currCond, new_cond );
+    setEntailedCond( n[0], !pol, currCond, new_cond, conflict );
+    return;
   }else if( n.getKind()==ITE ){
     int pol = getEntailedCond( n, currCond );
     if( pol==1 ){
-      setEntailedCond( n[1], pol, currCond, new_cond );
+      setEntailedCond( n[1], pol, currCond, new_cond, conflict );
     }else if( pol==-1 ){
-      setEntailedCond( n[2], pol, currCond, new_cond );
+      setEntailedCond( n[2], pol, currCond, new_cond, conflict );
     }
   }
-  if( addEntailedCond( n, pol, currCond, new_cond ) ){
+  if( addEntailedCond( n, pol, currCond, new_cond, conflict ) ){
     if( n.getKind()==APPLY_TESTER ){
       const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
       unsigned index = Datatype::indexOf(n.getOperator().toExpr());
@@ -543,14 +550,14 @@ void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::v
         for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
           if( i!=index ){
             Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n[0] );
-            addEntailedCond( t, false, currCond, new_cond );
+            addEntailedCond( t, false, currCond, new_cond, conflict );
           }
         }
       }else{
         if( dt.getNumConstructors()==2 ){
           int oindex = 1-index;
           Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[oindex].getTester() ), n[0] );
-          addEntailedCond( t, true, currCond, new_cond );
+          addEntailedCond( t, true, currCond, new_cond, conflict );
         }
       }
     }
@@ -577,59 +584,100 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n
 Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond,
                                                 std::map< Node, Node >& cache, std::map< Node, Node >& icache,
                                                 std::vector< Node >& new_vars, std::vector< Node >& new_conds ) {
+  Trace("quantifiers-rewrite-term-debug2") << "computeProcessTerms " << body << " " << hasPol << " " << pol << std::endl;
   Node ret;
   std::map< Node, Node >::iterator iti = cache.find( body );
   if( iti!=cache.end() ){
     ret = iti->second;
+    Trace("quantifiers-rewrite-term-debug2") << "Return (cached) " << ret << " for " << body << std::endl;
   }else{
-    bool do_ite = false;
-    //only do context dependent processing up to ITE depth 8
-    if( body.getKind()==ITE && nCurrCond<8 ){
-      do_ite = true;
-      nCurrCond = nCurrCond + 1;
-    }
+    bool firstTimeCD = true;
     bool changed = false;
     std::vector< Node > children;
     for( size_t i=0; i<body.getNumChildren(); i++ ){
       std::vector< Node > new_cond;
-      if( do_ite && i>0 ){
-        setEntailedCond( children[0], i==1, currCond, new_cond );
-        cache.clear();
+      bool conflict = false;
+      //only do context dependent processing up to depth 8
+      if( nCurrCond<8 ){
+        if( firstTimeCD ){
+          firstTimeCD = false;
+          nCurrCond = nCurrCond + 1;
+        }
+        if( Trace.isOn("quantifiers-rewrite-term-debug") ){
+          //if( ( body.getKind()==ITE && i>0 ) || ( hasPol && ( ( body.getKind()==OR && pol ) || (body.getKind()==AND && !pol ) ) ) ){
+          if( ( body.getKind()==ITE && i>0 ) || body.getKind()==OR || body.getKind()==AND ){
+            Trace("quantifiers-rewrite-term-debug") << "---rewrite " << body[i] << " under conditions:----" << std::endl;
+          }
+        }
+        if( body.getKind()==ITE && i>0 ){
+          setEntailedCond( children[0], i==1, currCond, new_cond, conflict );
+          //should not conflict (entailment check failed) 
+          Assert( !conflict );
+        }
+        //if( hasPol && ( ( body.getKind()==OR && pol ) || ( body.getKind()==AND && !pol ) ) ){
+        //  bool use_pol = !pol;
+        if( body.getKind()==OR || body.getKind()==AND ){
+          bool use_pol = body.getKind()==AND;
+          for( unsigned j=0; j<body.getNumChildren(); j++ ){
+            if( j<i ){
+              setEntailedCond( children[j], use_pol, currCond, new_cond, conflict );
+            }else if( j>i ){
+              setEntailedCond( body[j], use_pol, currCond, new_cond, conflict );
+            }
+          }
+          if( conflict ){
+            Trace("quantifiers-rewrite-term-debug") << "-------conflict, return " << !use_pol << std::endl;
+            ret = NodeManager::currentNM()->mkConst( !use_pol );
+          }
+        }
+        if( !new_cond.empty() ){
+          cache.clear();
+        }
+        if( Trace.isOn("quantifiers-rewrite-term-debug") ){
+          //if( ( body.getKind()==ITE && i>0 ) || ( hasPol && ( ( body.getKind()==OR && pol ) || (body.getKind()==AND && !pol ) ) ) ){
+          if( ( body.getKind()==ITE && i>0 ) || body.getKind()==OR || body.getKind()==AND ){      
+            Trace("quantifiers-rewrite-term-debug") << "-------" << std::endl;
+          }
+        }
       }
-      bool newHasPol;
-      bool newPol;
-      QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
-      Node nn = computeProcessTerms2( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
-      if( body.getKind()==ITE ){
-        if( i==0 ){
+      if( !conflict ){
+        bool newHasPol;
+        bool newPol;
+        QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
+        Node nn = computeProcessTerms2( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
+        if( body.getKind()==ITE && i==0 ){
           int res = getEntailedCond( nn, currCond );
+          Trace("quantifiers-rewrite-term-debug") << "Condition for " << body << " is " << nn << ", entailment check=" << res << std::endl;
           if( res==1 ){
             ret = computeProcessTerms2( body[1], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
-            break;
           }else if( res==-1 ){
             ret = computeProcessTerms2( body[2], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
-            break;
-          }
-        }else{
-          if( !new_cond.empty() ){
-            for( unsigned j=0; j<new_cond.size(); j++ ){
-              currCond.erase( new_cond[j] );
-            }
-            cache.clear();
           }
         }
+        children.push_back( nn );
+        changed = changed || nn!=body[i];
+      }
+      if( !new_cond.empty() ){
+        for( unsigned j=0; j<new_cond.size(); j++ ){
+          currCond.erase( new_cond[j] );
+        }
+        cache.clear();
+      }
+      if( !ret.isNull() ){
+        break;
       }
-      children.push_back( nn );
-      changed = changed || nn!=body[i];
     }
-    if( ret.isNull() && changed ){
-      if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){
-        children.insert( children.begin(), body.getOperator() );
+    if( ret.isNull() ){
+      if( changed ){
+        if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){
+          children.insert( children.begin(), body.getOperator() );
+        }
+        ret = NodeManager::currentNM()->mkNode( body.getKind(), children );
+      }else{
+        ret = body;
       }
-      ret = NodeManager::currentNM()->mkNode( body.getKind(), children );
-    }else{
-      ret = body;
     }
+    Trace("quantifiers-rewrite-term-debug2") << "Returning " << ret << " for " << body << std::endl;
     cache[body] = ret;
   }