diff options
| -rw-r--r-- | src/main/options | 6 | ||||
| -rw-r--r-- | src/smt/options_handlers.h | 6 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 41 |
3 files changed, 34 insertions, 19 deletions
diff --git a/src/main/options b/src/main/options index e78acf7d9..9fdef3865 100644 --- 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 43d53ee4c..60b3b48c2 100644 --- 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 d63a63ba2..cc126d6cd 100644 --- 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() ){ |