* more complete support for --dump assertions:{pre,post}-PREPROCESSING-PASS

* more minor cleanup/doc

(this commit was certified error- and warning-free by the test-and-commit script.)

diff --git a/src/main/options b/src/main/options
index e78acf7d94bad0002f67ab04c6ce345c9ead4f46..9fdef38658d91967e6c9bd4fe3e524f2ef10b12e 100644 (file)
--- a/src/main/options
+++ b/src/main/options
@@ -26,9 +26,9 @@ expert-option earlyExit --early-exit bool :default true
 option printWinner bool
  enable printing the winning thread (pcvc4 only)
 option threads --threads=N unsigned :default 2 :predicate greater(0)
- Total number of threads
+ Total number of threads for portfolio
 option - --threadN=string void :handler CVC4::main::threadN :handler-include "main/options_handlers.h"
- configures thread N (0..#threads-1)
+ configures portfolio thread N (0..#threads-1)
 option threadArgv std::vector<std::string> :include <vector> <string>
  Thread configuration (a string to be passed to parseOptions)
 option thread_id int :default -1
@@ -36,7 +36,7 @@ option thread_id int :default -1
 option separateOutput bool :default false
  In multi-threaded setting print output of each thread at the end of run, separated by a divider ("----").
 option sharingFilterByLength --filter-lemma-length=N int :default -1 :read-write
- don't share lemmas strictly longer than N
+ don't share (among portfolio threads) lemmas strictly longer than N
 
 expert-option waitToJoin --wait-to-join bool :default true
  wait for other threads to join before quitting

diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index 43d53ee4c92af53fab8afff1bceecb602790bbee..60b3b48c2edc3175bfa8ff48e47016c4ae6c67b8 100644 (file)
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -83,7 +83,8 @@ skolems\n\
 assertions\n\
 + Output the assertions after preprocessing and before clausification.\n\
   Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
-  where PASS is one of the preprocessing passes: skolem-quant simplify\n\
+  where PASS is one of the preprocessing passes: definition-expansion\n\
+  constrain-subtypes substitution skolem-quant simplify\n\
   static-learning ite-removal repeat-simplify theory-preprocessing.\n\
   PASS can also be the special value \"everything\", in which case the\n\
   assertions are printed before any preprocessing (with\n\
@@ -176,6 +177,9 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
                               optargPtr + "'.  Please consult --dump help.");
       }
       if(!strcmp(p, "everything")) {
+      } else if(!strcmp(p, "definition-expansion")) {
+      } else if(!strcmp(p, "constrain-subtypes")) {
+      } else if(!strcmp(p, "substitution")) {
       } else if(!strcmp(p, "skolem-quant")) {
       } else if(!strcmp(p, "simplify")) {
       } else if(!strcmp(p, "static-learning")) {

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d63a63ba20cf59c1637eae53af29e0de45ce6759..cc126d6cdead09cb84a1e7c23e4a5efd5ae24144 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -252,7 +252,7 @@ private:
   void unconstrainedSimp();
 
   /**
-   * Any variable in a assertion that is declared as a subtype type
+   * Any variable in an assertion that is declared as a subtype type
    * (predicate subtype or integer subrange type) must be constrained
    * to be in that type.
    */
@@ -1529,7 +1529,7 @@ void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertion
   } while(! worklist.empty());
 }
 
-// returns false if simpflication led to "false"
+// returns false if simplification led to "false"
 bool SmtEnginePrivate::simplifyAssertions()
   throw(TypeCheckingException) {
   Assert(d_smt.d_pendingPops == 0);
@@ -1689,19 +1689,7 @@ void SmtEnginePrivate::processAssertions() {
     return;
   }
 
-  // Any variables of subtype types need to be constrained properly.
-  // Careful, here: constrainSubtypes() adds to the back of
-  // d_assertionsToPreprocess, but we don't need to reprocess those.
-  // We also can't use an iterator, because the vector may be moved in
-  // memory during this loop.
-  Chat() << "constraining subtypes..." << endl;
-  for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) {
-    constrainSubtypes(d_assertionsToPreprocess[i], d_assertionsToPreprocess);
-  }
-
-  Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
-  Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
-
+  dumpAssertions("pre-definition-expansion", d_assertionsToPreprocess);
   {
     Chat() << "expanding definitions..." << endl;
     Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl;
@@ -1712,7 +1700,29 @@ void SmtEnginePrivate::processAssertions() {
         expandDefinitions(d_assertionsToPreprocess[i], cache);
     }
   }
+  dumpAssertions("post-definition-expansion", d_assertionsToPreprocess);
+
+  Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
+  Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+
+  dumpAssertions("pre-constrain-subtypes", d_assertionsToPreprocess);
+  {
+    // Any variables of subtype types need to be constrained properly.
+    // Careful, here: constrainSubtypes() adds to the back of
+    // d_assertionsToPreprocess, but we don't need to reprocess those.
+    // We also can't use an iterator, because the vector may be moved in
+    // memory during this loop.
+    Chat() << "constraining subtypes..." << endl;
+    for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) {
+      constrainSubtypes(d_assertionsToPreprocess[i], d_assertionsToPreprocess);
+    }
+  }
+  dumpAssertions("post-constrain-subtypes", d_assertionsToPreprocess);
+
+  Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
+  Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
+  dumpAssertions("pre-substitution", d_assertionsToPreprocess);
   // Apply the substitutions we already have, and normalize
   Chat() << "applying substitutions..." << endl;
   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
@@ -1723,6 +1733,7 @@ void SmtEnginePrivate::processAssertions() {
       Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i]));
     Trace("simplify") << "  got " << d_assertionsToPreprocess[i] << endl;
   }
+  dumpAssertions("post-substitution", d_assertionsToPreprocess);
 
   dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess);
   if( options::preSkolemQuant() ){