Fix unsat-core issues related to rewrite rules, quantifiers preprocessing, and strings preprocessing. Minor fix for conjecture generation for finite types.

8 files changed, 59 insertions, 40 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index cb18b8464..25ac4c516 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3165,15 +3165,10 @@ void SmtEnginePrivate::processAssertions() {
   if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
     dumpAssertions("pre-strings-pp", d_assertions);
     CVC4::theory::strings::StringsPreprocess sp;
-    std::vector<Node> newNodes;
-    newNodes.push_back(d_assertions[d_realAssertionsEnd - 1]);
-    sp.simplify( d_assertions.ref(), newNodes );
-    if(newNodes.size() > 1) {
-      d_assertions[d_realAssertionsEnd - 1] = NodeManager::currentNM()->mkNode(kind::AND, newNodes);
-    }
-    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
-      d_assertions[i] = Rewriter::rewrite( d_assertions[i] );
-    }
+    sp.simplify( d_assertions.ref() );
+    //for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+    //  d_assertions.replace( i, Rewriter::rewrite( d_assertions[i] ) );
+    //}
     dumpAssertions("post-strings-pp", d_assertions);
   }
   if( d_smt.d_logic.isQuantified() ){
@@ -3182,7 +3177,7 @@ void SmtEnginePrivate::processAssertions() {
       if( d_assertions[i].getKind() == kind::REWRITE_RULE ){
         Node prev = d_assertions[i];
         Trace("quantifiers-rewrite-debug") << "Rewrite rewrite rule " << prev << "..." << std::endl;
-        d_assertions[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::rewriteRewriteRule( d_assertions[i] ) );
+        d_assertions.replace(i, Rewriter::rewrite( quantifiers::QuantifiersRewriter::rewriteRewriteRule( d_assertions[i] ) ) );
         Trace("quantifiers-rewrite") << "*** rr-rewrite " << prev << endl;
         Trace("quantifiers-rewrite") << "   ...got " << d_assertions[i] << endl;
       }
@@ -3235,10 +3230,6 @@ void SmtEnginePrivate::processAssertions() {
     }
   }
 
-  //if( options::quantConflictFind() ){
-  //  d_smt.d_theoryEngine->getQuantConflictFind()->registerAssertions( d_assertions );
-  //}
-
   if( options::pbRewrites() ){
     d_pbsProcessor.learn(d_assertions.ref());
     if(d_pbsProcessor.likelyToHelp()){
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 48d3f3902..116debb7c 100755
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -1159,6 +1159,8 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
             vec[i] = 0;

           }

           vec_sum = -1;

+        }else{

+          return;

         }

       }

     }

diff --git a/src/theory/quantifiers/first_order_reasoning.cpp b/src/theory/quantifiers/first_order_reasoning.cpp
index 5435fba34..23e18bb02 100644
--- a/src/theory/quantifiers/first_order_reasoning.cpp
+++ b/src/theory/quantifiers/first_order_reasoning.cpp
@@ -17,6 +17,7 @@
 
 #include "theory/quantifiers/first_order_reasoning.h"
 #include "theory/rewriter.h"
+#include "proof/proof_manager.h"
 
 using namespace CVC4;
 using namespace std;
@@ -100,7 +101,12 @@ void FirstOrderPropagation::simplify( std::vector< Node >& assertions ){
   }while( num_processed>0 );
   Trace("fo-rsn-sum") << "Simplified " << num_true << " / " << assertions.size() << " in " << num_rounds << " rounds." << std::endl;
   for( unsigned i=0; i<assertions.size(); i++ ){
-    assertions[i] = theory::Rewriter::rewrite( simplify( assertions[i] ) );
+    Node curr = simplify( assertions[i] );
+    if( curr!=assertions[i] ){
+      curr = Rewriter::rewrite( curr );
+      PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); );
+      assertions[i] = curr;
+    }
   }
 }
 
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index b80d9d744..f47cb8f1e 100644
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -20,6 +20,7 @@
 #include "theory/rewriter.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/quant_util.h"
+#include "proof/proof_manager.h"
 
 using namespace CVC4;
 using namespace std;
@@ -75,8 +76,10 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
 
       Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << std::endl;
       Trace("fmf-fun-def") << "  to " << std::endl;
-      assertions[i] = NodeManager::currentNM()->mkNode( FORALL, bvl, bd );
-      assertions[i] = Rewriter::rewrite( assertions[i] );
+      Node new_q = NodeManager::currentNM()->mkNode( FORALL, bvl, bd );
+      new_q = Rewriter::rewrite( new_q );
+      PROOF( ProofManager::currentPM()->addDependence(new_q, assertions[i]); );
+      assertions[i] = new_q;
       Trace("fmf-fun-def") << "  " << assertions[i] << std::endl;
       fd_assertions.push_back( i );
     }
@@ -95,6 +98,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
         Trace("fmf-fun-def-rewrite") << "FMF fun def : rewrite " << assertions[i] << std::endl;
         Trace("fmf-fun-def-rewrite") << "  to " << std::endl;
         Trace("fmf-fun-def-rewrite") << "  " << n << std::endl;
+        PROOF( ProofManager::currentPM()->addDependence(n, assertions[i]); );
         assertions[i] = n;
       }
     }
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 81cd5948a..d9a31f4b5 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -18,6 +18,7 @@
 
 #include "theory/quantifiers/macros.h"
 #include "theory/rewriter.h"
+#include "proof/proof_manager.h"
 
 using namespace CVC4;
 using namespace std;
@@ -36,11 +37,12 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite
   if( doRewrite && !d_macro_defs.empty() ){
     //now, rewrite based on macro definitions
     for( size_t i=0; i<assertions.size(); i++ ){
-      Node prev = assertions[i];
-      assertions[i] = simplify( assertions[i] );
-      if( prev!=assertions[i] ){
-        assertions[i] = Rewriter::rewrite( assertions[i] );
-        Trace("macros-rewrite") << "Rewrite " << prev << " to " << assertions[i] << std::endl;
+      Node curr = simplify( assertions[i] );
+      if( curr!=assertions[i] ){
+        curr = Rewriter::rewrite( curr );
+        Trace("macros-rewrite") << "Rewrite " << assertions[i] << " to " << curr << std::endl;
+        PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); );
+        assertions[i] = curr;
         retVal = true;
       }
     }
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index a8cbcfac0..b27cab223 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Tianyi Liang
  ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Minor contributors (to current version): Morgan Deters, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -19,6 +19,7 @@
 #include "theory/strings/options.h"
 #include "smt/logic_exception.h"
 #include <stdint.h>
+#include "proof/proof_manager.h"
 
 namespace CVC4 {
 namespace theory {
@@ -550,15 +551,15 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
       retNode = t;
     }
   }*/
-
-  Trace("strings-preprocess") << "StringsPreprocess::simplify returns: " << retNode << std::endl;
-  if(!new_nodes.empty()) {
-    Trace("strings-preprocess") << " ... new nodes (" << new_nodes.size() << "):\n";
-    for(unsigned int i=0; i<new_nodes.size(); ++i) {
-      Trace("strings-preprocess") << "\t" << new_nodes[i] << "\n";
+  if( t!=retNode ){
+    Trace("strings-preprocess") << "StringsPreprocess::simplify returns: " << retNode << std::endl;
+    if(!new_nodes.empty()) {
+      Trace("strings-preprocess") << " ... new nodes (" << new_nodes.size() << "):\n";
+      for(unsigned int i=0; i<new_nodes.size(); ++i) {
+        Trace("strings-preprocess") << "\t" << new_nodes[i] << "\n";
+      }
     }
   }
-
   return retNode;
 }
 
@@ -593,17 +594,28 @@ Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes) {
   }
 }
 
-void StringsPreprocess::simplify(std::vector< Node > &vec_node, std::vector< Node > &new_nodes) {
+void StringsPreprocess::simplify(std::vector< Node > &vec_node) {
   for( unsigned i=0; i<vec_node.size(); i++ ){
-    vec_node[i] = decompose( vec_node[i], new_nodes );
+    std::vector< Node > new_nodes;
+    Node curr = decompose( vec_node[i], new_nodes );
+    if( !new_nodes.empty() ){
+      new_nodes.insert( new_nodes.begin(), curr );
+      curr = NodeManager::currentNM()->mkNode( kind::AND, new_nodes );
+    }
+    if( curr!=vec_node[i] ){
+      curr = Rewriter::rewrite( curr );
+      PROOF( ProofManager::currentPM()->addDependence(curr, vec_node[i]); );
+      vec_node[i] = curr;
+    }
   }
 }
-
+/*
 void StringsPreprocess::simplify(std::vector< Node > &vec_node) {
   std::vector< Node > new_nodes;
   simplify(vec_node, new_nodes);
   vec_node.insert( vec_node.end(), new_nodes.begin(), new_nodes.end() );
 }
+*/
 
 }/* CVC4::theory::strings namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 334ac1d61..155b7b236 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Tianyi Liang
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -40,7 +40,6 @@ private:
   Node simplify( Node t, std::vector< Node > &new_nodes );
   Node decompose( Node t, std::vector< Node > &new_nodes );
 public:
-  void simplify(std::vector< Node > &vec_node, std::vector< Node > &new_nodes);
   void simplify(std::vector< Node > &vec_node);
   StringsPreprocess();
 };
diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp
index dbd1dcd16..14d37e068 100644
--- a/src/util/sort_inference.cpp
+++ b/src/util/sort_inference.cpp
@@ -24,6 +24,7 @@
 #include "smt/options.h"
 #include "theory/rewriter.h"
 #include "theory/quantifiers/options.h"
+#include "proof/proof_manager.h"
 
 using namespace CVC4;
 using namespace std;
@@ -172,13 +173,15 @@ bool SortInference::simplify( std::vector< Node >& assertions ){
       Node prev = assertions[i];
       std::map< Node, Node > var_bound;
       Trace("sort-inference-debug") << "Rewrite " << assertions[i] << std::endl;
-      assertions[i] = simplify( assertions[i], var_bound );
+      Node curr = simplify( assertions[i], var_bound );
       Trace("sort-inference-debug") << "Done." << std::endl;
-      if( prev!=assertions[i] ){
-        assertions[i] = theory::Rewriter::rewrite( assertions[i] );
+      if( curr!=assertions[i] ){
+        curr = theory::Rewriter::rewrite( curr );
         rewritten = true;
-        Trace("sort-inference-rewrite") << prev << std::endl;
-        Trace("sort-inference-rewrite") << " --> " << assertions[i] << std::endl;
+        Trace("sort-inference-rewrite") << assertions << std::endl;
+        Trace("sort-inference-rewrite") << " --> " << curr << std::endl;
+        PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); );
+        assertions[i] = curr;
       }
     }
     //now, ensure constants are distinct