diff options
author | Justin Xu <justinx@barrett5.stanford.edu> | 2017-07-24 15:15:57 -0700 |
---|---|---|
committer | Justin Xu <justinx@barrett5.stanford.edu> | 2017-07-24 15:15:57 -0700 |
commit | 93c2bbb764e34cd5285607dcb2bc4872bbe92456 (patch) | |
tree | ab5bee0e86f4f87e5ec0cdbf15836d01724a56e2 | |
parent | e07aa10dea10fcc6ce1775cc7c67b6baa0d09750 (diff) |
CNFPass and RemoveITE and TheoryPreprocess
-rw-r--r-- | src/preproc/preprocessing_passes_core.cpp | 43 | ||||
-rw-r--r-- | src/preproc/preprocessing_passes_core.h | 28 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 36 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 2 |
4 files changed, 84 insertions, 25 deletions
diff --git a/src/preproc/preprocessing_passes_core.cpp b/src/preproc/preprocessing_passes_core.cpp index 14599ea22..69d3434ed 100644 --- a/src/preproc/preprocessing_passes_core.cpp +++ b/src/preproc/preprocessing_passes_core.cpp @@ -946,6 +946,22 @@ PreprocessingPassResult PBRewritePass::apply(AssertionPipeline* assertionsToPrep DoStaticLearningPass::DoStaticLearningPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine, SmtEngine* smt, TimerStat staticLearningTime) : PreprocessingPass(resourceManager), d_theoryEngine(theoryEngine), d_smt(smt), d_staticLearningTime(staticLearningTime){ } +RemoveITEPass::RemoveITEPass(ResourceManager* resourceManager, SmtEngine* smt, IteSkolemMap* iteSkolemMap, RemoveTermFormulas* iteRemover) : PreprocessingPass(resourceManager), d_smt(smt), d_iteSkolemMap(iteSkolemMap), d_iteRemover(iteRemover){ +} + +PreprocessingPassResult RemoveITEPass::apply(AssertionPipeline* assertionsToPreprocess){ + d_smt->finalOptionsAreSet(); + spendResource(options::preprocessStep()); + Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl; + + // Remove all of the ITE occurrences and normalize + d_iteRemover->run(assertionsToPreprocess->ref(), *d_iteSkolemMap, true); + for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) { + assertionsToPreprocess->replace(i, theory::Rewriter::rewrite((*assertionsToPreprocess)[i])); + } + return PreprocessingPassResult(true); +} + void DoStaticLearningPass::staticLearning(AssertionPipeline* assertionsToPreprocess){ d_smt->finalOptionsAreSet(); spendResource(options::preprocessStep()); @@ -1049,6 +1065,20 @@ PreprocessingPassResult RewriteApplyToConstPass::apply(AssertionPipeline* assert return PreprocessingPassResult(true); } +TheoryPreprocessPass::TheoryPreprocessPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine, TimerStat theoryPreprocessTime) : PreprocessingPass(resourceManager), d_theoryEngine(theoryEngine), d_theoryPreprocessTime(theoryPreprocessTime){ +} + +PreprocessingPassResult TheoryPreprocessPass::apply(AssertionPipeline* assertionsToPreprocess){ + Chat() << "theory preprocessing..." << endl; + TimerStat::CodeTimer codeTimer(d_theoryPreprocessTime); + // Call the theory preprocessors + d_theoryEngine->preprocessStart(); + for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) { + assertionsToPreprocess->replace(i, d_theoryEngine->preprocess((*assertionsToPreprocess)[i])); + } + return PreprocessingPassResult(true); +} + BitBlastModeEagerPass::BitBlastModeEagerPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine) : PreprocessingPass(resourceManager), d_theoryEngine(theoryEngine){ } @@ -1074,6 +1104,19 @@ PreprocessingPassResult NoConflictPass::apply(AssertionPipeline* assertionsToPre return PreprocessingPassResult(true); } +CNFPass::CNFPass(ResourceManager* resourceManager, prop::PropEngine* propEngine, TimerStat cnfConversionTime) : PreprocessingPass(resourceManager), d_propEngine(propEngine), d_cnfConversionTime(cnfConversionTime){ +} + +PreprocessingPassResult CNFPass::apply(AssertionPipeline* assertionsToPreprocess){ + Chat() << "converting to CNF..." << endl; + TimerStat::CodeTimer codeTimer(d_cnfConversionTime); + for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) { + Chat() << "+ " << (*assertionsToPreprocess)[i] << std::endl; + d_propEngine->assertFormula((*assertionsToPreprocess)[i]); + } + return PreprocessingPassResult(true); +} + /** RepeatSimpPass::RepeatSimpPass(ResourceManager* resourceManager, theory::SubstitutionMap* topLevelSubstitutions, diff --git a/src/preproc/preprocessing_passes_core.h b/src/preproc/preprocessing_passes_core.h index 0e113a761..9f8e91c3d 100644 --- a/src/preproc/preprocessing_passes_core.h +++ b/src/preproc/preprocessing_passes_core.h @@ -177,6 +177,16 @@ class PBRewritePass : public PreprocessingPass { theory::arith::PseudoBooleanProcessor* d_pbsProcessor; }; +class RemoveITEPass : public PreprocessingPass { + public: + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); + RemoveITEPass(ResourceManager* resourceManager, SmtEngine* smt, IteSkolemMap* iteSkolemMap, RemoveTermFormulas* iteRemover); + private: + SmtEngine* d_smt; + IteSkolemMap* d_iteSkolemMap; + RemoveTermFormulas* d_iteRemover; +}; + class DoStaticLearningPass : public PreprocessingPass { public: virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); @@ -198,6 +208,15 @@ class RewriteApplyToConstPass : public PreprocessingPass { Node rewriteApplyToConst(TNode n); }; +class TheoryPreprocessPass : public PreprocessingPass { + public : + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); + TheoryPreprocessPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine, TimerStat theoryPreprocessTime); + private: + TheoryEngine* d_theoryEngine; + TimerStat d_theoryPreprocessTime; +}; + class BitBlastModeEagerPass : public PreprocessingPass { public: virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); @@ -216,6 +235,15 @@ class NoConflictPass : public PreprocessingPass { IteSkolemMap* d_iteSkolemMap; }; +class CNFPass : public PreprocessingPass{ + public: + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); + CNFPass(ResourceManager* resourceManager, prop::PropEngine* propEngine, TimerStat cnfConversionTime); + private: + prop::PropEngine* d_propEngine; + TimerStat d_cnfConversionTime; +}; + /* class RepeatSimpPass : public PreprocessingPass { public: diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 63840cb52..2de0114d0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3741,20 +3741,12 @@ void SmtEnginePrivate::processAssertions() { if(options::doStaticLearning()) { preproc::DoStaticLearningPass pass(d_resourceManager, d_smt.d_theoryEngine, &d_smt, d_smt.d_stats->d_staticLearningTime); pass.apply(&d_assertions); + } -/* Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-static-learning" << endl; - // Perform static learning - Chat() << "doing static learning..." << endl; - Trace("simplify") << "SmtEnginePrivate::simplify(): " - << "performing static learning" << endl; - staticLearning(); - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-static-learning" << endl;*/ - } dumpAssertions("post-static-learning", d_assertions); Debug("smt") << " d_assertions : " << d_assertions.size() << endl; - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-ite-removal" << endl; dumpAssertions("pre-ite-removal", d_assertions); { @@ -3762,7 +3754,10 @@ void SmtEnginePrivate::processAssertions() { TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_iteRemovalTime); // Remove ITEs, updating d_iteSkolemMap d_smt.d_stats->d_numAssertionsPre += d_assertions.size(); - removeITEs(); + + preproc::RemoveITEPass pass(d_resourceManager, &d_smt, &d_iteSkolemMap, &d_iteRemover); + pass.apply(&d_assertions); +//removeITEs(); d_smt.d_stats->d_numAssertionsPost += d_assertions.size(); } Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-ite-removal" << endl; @@ -3866,14 +3861,9 @@ void SmtEnginePrivate::processAssertions() { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-theory-preprocessing" << endl; dumpAssertions("pre-theory-preprocessing", d_assertions); { - Chat() << "theory preprocessing..." << endl; - TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime); - // Call the theory preprocessors - d_smt.d_theoryEngine->preprocessStart(); - for (unsigned i = 0; i < d_assertions.size(); ++ i) { - d_assertions.replace(i, d_smt.d_theoryEngine->preprocess(d_assertions[i])); - } - } + preproc::TheoryPreprocessPass pass(d_resourceManager, d_smt.d_theoryEngine, d_smt.d_stats->d_theoryPreprocessTime); + pass.apply(&d_assertions); + } Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-theory-preprocessing" << endl; dumpAssertions("post-theory-preprocessing", d_assertions); @@ -3901,13 +3891,9 @@ void SmtEnginePrivate::processAssertions() { // Push the formula to SAT { - Chat() << "converting to CNF..." << endl; - TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_cnfConversionTime); - for (unsigned i = 0; i < d_assertions.size(); ++ i) { - Chat() << "+ " << d_assertions[i] << std::endl; - d_smt.d_propEngine->assertFormula(d_assertions[i]); - } - } + preproc::CNFPass pass(d_resourceManager, d_smt.d_propEngine, d_smt.d_stats->d_cnfConversionTime); + pass.apply(&d_assertions); + } d_assertionsProcessed = true; diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index faf718334..6e23c493d 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -112,6 +112,7 @@ namespace preproc{ class SimplifyAssertionsPass; class ExpandingDefinitionsPass; class ConstrainSubtypesPass; + class RemoveITEPass; }/* CVC4::preproc namespace */ // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the @@ -362,6 +363,7 @@ class CVC4_PUBLIC SmtEngine { friend class ::CVC4::preproc::SimplifyAssertionsPass; friend class ::CVC4::preproc::ExpandingDefinitionsPass; friend class ::CVC4::preproc::ConstrainSubtypesPass; + friend class ::CVC4::preproc::RemoveITEPass; friend class ::CVC4::smt::SmtEnginePrivate; friend class ::CVC4::smt::SmtScope; friend class ::CVC4::smt::BooleanTermConverter; |