summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/preproc/preprocessing_passes_core.cpp43
-rw-r--r--src/preproc/preprocessing_passes_core.h28
-rw-r--r--src/smt/smt_engine.cpp36
-rw-r--r--src/smt/smt_engine.h2
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback