summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/preproc/preprocessing_pass.h9
-rw-r--r--src/preproc/preprocessing_passes_core.cpp37
-rw-r--r--src/preproc/preprocessing_passes_core.h38
-rw-r--r--src/smt/smt_engine.cpp13
4 files changed, 48 insertions, 49 deletions
diff --git a/src/preproc/preprocessing_pass.h b/src/preproc/preprocessing_pass.h
index ee719e2c4..1c8125a58 100644
--- a/src/preproc/preprocessing_pass.h
+++ b/src/preproc/preprocessing_pass.h
@@ -13,7 +13,7 @@
namespace CVC4 {
-namespace smt {
+namespace preproc {
class AssertionPipeline {
std::vector<Node> d_nodes;
@@ -36,14 +36,11 @@ public:
d_nodes[i] = n;
}
};// class AssertionPipeline
-} //namespace smt
-
-namespace preproc {
class PreprocessingPass {
public:
- virtual void apply(smt::AssertionPipeline* assertionsToPreprocess) = 0;
- void dumpAssertions(const char* key, const smt::AssertionPipeline& assertionList) {
+ virtual void apply(AssertionPipeline* assertionsToPreprocess) = 0;
+ void dumpAssertions(const char* key, const AssertionPipeline& assertionList) {
if( Dump.isOn("assertions") &&
Dump.isOn(std::string("assertions:") + key) ) {
// Push the simplified assertions to the dump output stream
diff --git a/src/preproc/preprocessing_passes_core.cpp b/src/preproc/preprocessing_passes_core.cpp
index d364f17ce..f931fedb6 100644
--- a/src/preproc/preprocessing_passes_core.cpp
+++ b/src/preproc/preprocessing_passes_core.cpp
@@ -84,7 +84,7 @@ CEGuidedInstPass::CEGuidedInstPass(ResourceManager* resourceManager,
d_theoryEngine(theoryEngine){
}
-void CEGuidedInstPass::apply(smt::AssertionPipeline* assertionsToPreprocess){
+void CEGuidedInstPass::apply(AssertionPipeline* assertionsToPreprocess){
for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) {
d_theoryEngine->getQuantifiersEngine()->getCegInstantiation()->preregisterAssertion( (*assertionsToPreprocess)[i] );
}
@@ -94,7 +94,7 @@ SolveRealAsIntPass::SolveRealAsIntPass(ResourceManager* resourceManager) :
PreprocessingPass(resourceManager){
}
-void SolveRealAsIntPass::apply(smt::AssertionPipeline* assertionsToPreprocess) {
+void SolveRealAsIntPass::apply(AssertionPipeline* assertionsToPreprocess) {
Chat() << "converting reals to ints..." << std::endl;
std::unordered_map<Node, Node, NodeHashFunction> cache;
std::vector<Node> var_eq;
@@ -202,7 +202,7 @@ SolveIntAsBVPass::SolveIntAsBVPass(ResourceManager* resourceManager) :
PreprocessingPass(resourceManager){
}
-void SolveIntAsBVPass::apply(smt::AssertionPipeline* assertionsToPreprocess)
+void SolveIntAsBVPass::apply(AssertionPipeline* assertionsToPreprocess)
{
Chat() << "converting ints to bit-vectors..." << std::endl;
std::unordered_map<Node, Node, NodeHashFunction> cache;
@@ -447,7 +447,7 @@ BitBlastModePass::BitBlastModePass(ResourceManager* resourceManager,
d_theoryEngine(theoryEngine){
}
-void BitBlastModePass::apply(smt::AssertionPipeline* assertionsToPreprocess){
+void BitBlastModePass::apply(AssertionPipeline* assertionsToPreprocess){
d_theoryEngine->mkAckermanizationAsssertions(assertionsToPreprocess->ref());
}
@@ -457,7 +457,7 @@ BVAbstractionPass::BVAbstractionPass(ResourceManager* resourceManager,
d_theoryEngine(theoryEngine){
}
-void BVAbstractionPass::bvAbstraction(smt::AssertionPipeline* assertionsToPreprocess){
+void BVAbstractionPass::bvAbstraction(AssertionPipeline* assertionsToPreprocess){
Trace("bv-abstraction") << "SmtEnginePrivate::bvAbstraction()" << std::endl;
std::vector<Node> new_assertions;
bool changed = d_theoryEngine->ppBvAbstraction(assertionsToPreprocess->ref(), new_assertions);
@@ -474,7 +474,7 @@ void BVAbstractionPass::bvAbstraction(smt::AssertionPipeline* assertionsToPrepro
}
}
-void BVAbstractionPass::apply(smt::AssertionPipeline* assertionsToPreprocess){
+void BVAbstractionPass::apply(AssertionPipeline* assertionsToPreprocess){
dumpAssertions("pre-bv-abstraction", *assertionsToPreprocess);
bvAbstraction(assertionsToPreprocess);
dumpAssertions("post-bv-abstraction", *assertionsToPreprocess);
@@ -487,7 +487,7 @@ UnconstrainedSimpPass::UnconstrainedSimpPass(ResourceManager* resourceManager,
d_theoryEngine(theoryEngine){
}
-void UnconstrainedSimpPass::apply(smt::AssertionPipeline* assertionsToPreprocess){
+void UnconstrainedSimpPass::apply(AssertionPipeline* assertionsToPreprocess){
TimerStat::CodeTimer unconstrainedSimpTimer(d_unconstrainedSimpTime);
spendResource(options::preprocessStep());
Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << std::endl;
@@ -498,7 +498,7 @@ RewritePass::RewritePass(ResourceManager* resourceManager) :
PreprocessingPass(resourceManager){
}
-void RewritePass::apply(smt::AssertionPipeline* assertionsToPreprocess){
+void RewritePass::apply(AssertionPipeline* assertionsToPreprocess){
for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) {
assertionsToPreprocess->replace(i, theory::Rewriter::rewrite((*assertionsToPreprocess)[i]));
}
@@ -510,7 +510,7 @@ NotUnsatCoresPass::NotUnsatCoresPass(ResourceManager* resourceManager,
d_topLevelSubstitutions(topLevelSubstitutions){
}
-void NotUnsatCoresPass::apply(smt::AssertionPipeline* assertionsToPreprocess){
+void NotUnsatCoresPass::apply(AssertionPipeline* assertionsToPreprocess){
Chat() << "applying substitutions..." << std::endl;
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
<< "applying substitutions" << std::endl;
@@ -527,7 +527,7 @@ BVToBoolPass::BVToBoolPass(ResourceManager* resourceManager,
d_theoryEngine(theoryEngine){
}
-void BVToBoolPass::apply(smt::AssertionPipeline* assertionsToPreprocess){
+void BVToBoolPass::apply(AssertionPipeline* assertionsToPreprocess){
dumpAssertions("pre-bv-to-bool", *assertionsToPreprocess);
Chat() << "...doing bvToBool..." << std::endl;
bvToBool(assertionsToPreprocess);
@@ -536,7 +536,7 @@ void BVToBoolPass::apply(smt::AssertionPipeline* assertionsToPreprocess){
Trace("smt") << "POST bvToBool" << std::endl;
}
-void BVToBoolPass::bvToBool(smt::AssertionPipeline* assertionsToPreprocess) {
+void BVToBoolPass::bvToBool(AssertionPipeline* assertionsToPreprocess) {
Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << std::endl;
spendResource(options::preprocessStep());
std::vector<Node> new_assertions;
@@ -552,7 +552,7 @@ BoolToBVPass::BoolToBVPass(ResourceManager* resourceManager,
d_theoryEngine(theoryEngine){
}
-void BoolToBVPass::boolToBv(smt::AssertionPipeline* assertionsToPreprocess) {
+void BoolToBVPass::boolToBv(AssertionPipeline* assertionsToPreprocess) {
Trace("bool-to-bv") << "SmtEnginePrivate::boolToBv()" << std::endl;
spendResource(options::preprocessStep());
std::vector<Node> new_assertions;
@@ -563,7 +563,7 @@ void BoolToBVPass::boolToBv(smt::AssertionPipeline* assertionsToPreprocess) {
assertionsToPreprocess->ref().swap(new_assertions);
}
-void BoolToBVPass::apply(smt::AssertionPipeline* assertionsToPreprocess){
+void BoolToBVPass::apply(AssertionPipeline* assertionsToPreprocess){
dumpAssertions("pre-bool-to-bv", *assertionsToPreprocess);
Chat() << "...doing boolToBv..." << std::endl;
boolToBv(assertionsToPreprocess);
@@ -574,7 +574,7 @@ void BoolToBVPass::apply(smt::AssertionPipeline* assertionsToPreprocess){
SepPreSkolemEmpPass::SepPreSkolemEmpPass(ResourceManager* resourceManager) : PreprocessingPass(resourceManager){
}
-void SepPreSkolemEmpPass::apply(smt::AssertionPipeline* assertionsToPreprocess){
+void SepPreSkolemEmpPass::apply(AssertionPipeline* assertionsToPreprocess){
for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) {
Node prev = (*assertionsToPreprocess)[i];
Node next = theory::sep::TheorySepRewriter::preprocess( prev );
@@ -587,16 +587,16 @@ void SepPreSkolemEmpPass::apply(smt::AssertionPipeline* assertionsToPreprocess){
}
QuantifiedPass::QuantifiedPass(ResourceManager* resourceManager,
- TheoryEngine* theoryEngine, NodeList* fmfRecFunctionsDefined,
- std::map<Node,TypeNode> fmfRecFunctionsAbs,
- std::map<Node, std::vector<Node> > fmfRecFunctionsConcrete) :
+ TheoryEngine* theoryEngine, NodeList* &fmfRecFunctionsDefined,
+ std::map<Node,TypeNode> &fmfRecFunctionsAbs,
+ std::map<Node, std::vector<Node> > &fmfRecFunctionsConcrete) :
PreprocessingPass(resourceManager), d_theoryEngine(theoryEngine),
d_fmfRecFunctionsDefined(fmfRecFunctionsDefined),
d_fmfRecFunctionsAbs(fmfRecFunctionsAbs),
d_fmfRecFunctionsConcrete(fmfRecFunctionsConcrete){
}
-void QuantifiedPass::apply(smt::AssertionPipeline* assertionsToPreprocess){
+void QuantifiedPass::apply(AssertionPipeline* assertionsToPreprocess){
Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << std::endl;
dumpAssertions("pre-skolem-quant", *assertionsToPreprocess);
@@ -654,6 +654,5 @@ void QuantifiedPass::apply(smt::AssertionPipeline* assertionsToPreprocess){
Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << std::endl;
}
-
} // namespace preproc
} // namespace CVC4
diff --git a/src/preproc/preprocessing_passes_core.h b/src/preproc/preprocessing_passes_core.h
index 8470feefb..b644ded2b 100644
--- a/src/preproc/preprocessing_passes_core.h
+++ b/src/preproc/preprocessing_passes_core.h
@@ -16,7 +16,7 @@ typedef context::CDList<Node> NodeList;
class NlExtPurifyPass : public PreprocessingPass {
public:
- virtual void apply(smt::AssertionPipeline* assertionsToPreprocess);
+ virtual void apply(AssertionPipeline* assertionsToPreprocess);
NlExtPurifyPass(ResourceManager* resourceManager);
private:
Node purifyNlTerms(TNode n, NodeMap& cache, NodeMap& bcache,
@@ -25,7 +25,7 @@ class NlExtPurifyPass : public PreprocessingPass {
class CEGuidedInstPass : public PreprocessingPass {
public:
- virtual void apply(smt::AssertionPipeline* assertionsToPreprocess);
+ virtual void apply(AssertionPipeline* assertionsToPreprocess);
CEGuidedInstPass(ResourceManager* resourceManager, TheoryEngine* theoryEngine);
private:
TheoryEngine* d_theoryEngine;
@@ -33,7 +33,7 @@ class CEGuidedInstPass : public PreprocessingPass {
class SolveRealAsIntPass : public PreprocessingPass {
public:
- virtual void apply(smt::AssertionPipeline* assertionsToPreprocess);
+ virtual void apply(AssertionPipeline* assertionsToPreprocess);
SolveRealAsIntPass(ResourceManager* resourceManager);
private:
Node realToInt(TNode n, NodeMap& cache, std::vector<Node>& var_eq);
@@ -41,7 +41,7 @@ class SolveRealAsIntPass : public PreprocessingPass {
class SolveIntAsBVPass : public PreprocessingPass {
public:
- virtual void apply(smt::AssertionPipeline* assertionsToPreprocess);
+ virtual void apply(AssertionPipeline* assertionsToPreprocess);
SolveIntAsBVPass(ResourceManager* resourceManager);
private:
Node intToBV(TNode n, NodeToNodeHashMap& cache);
@@ -50,7 +50,7 @@ class SolveIntAsBVPass : public PreprocessingPass {
class BitBlastModePass : public PreprocessingPass {
public:
- virtual void apply(smt::AssertionPipeline* assertionsToPreprocess);
+ virtual void apply(AssertionPipeline* assertionsToPreprocess);
BitBlastModePass(ResourceManager* resourceManager,
TheoryEngine* theoryEngine);
private:
@@ -59,7 +59,7 @@ class BitBlastModePass : public PreprocessingPass {
class BVAbstractionPass : public PreprocessingPass {
public:
- virtual void apply(smt::AssertionPipeline* assertionsToPreprocess);
+ virtual void apply(AssertionPipeline* assertionsToPreprocess);
BVAbstractionPass(ResourceManager* resourceManager,
SmtEngine* smt, TheoryEngine* theoryEngine);
private:
@@ -67,12 +67,12 @@ class BVAbstractionPass : public PreprocessingPass {
TheoryEngine* d_theoryEngine;
// Abstract common structure over small domains to UF
// return true if changes were made.
- void bvAbstraction(smt::AssertionPipeline* assertionsToPreprocess);
+ void bvAbstraction(AssertionPipeline* assertionsToPreprocess);
};
class UnconstrainedSimpPass : public PreprocessingPass {
public:
- virtual void apply(smt::AssertionPipeline* assertionsToPreprocess);
+ virtual void apply(AssertionPipeline* assertionsToPreprocess);
UnconstrainedSimpPass(ResourceManager* resourceManager,
TimerStat unconstrainedSimpTime, TheoryEngine* theoryEngine);
private:
@@ -83,13 +83,13 @@ class UnconstrainedSimpPass : public PreprocessingPass {
class RewritePass : public PreprocessingPass {
public:
- virtual void apply(smt::AssertionPipeline* assertionsToPreprocess);
+ virtual void apply(AssertionPipeline* assertionsToPreprocess);
RewritePass(ResourceManager* resourceManager);
};
class NotUnsatCoresPass : public PreprocessingPass {
public:
- virtual void apply(smt::AssertionPipeline* assertionsToPreprocess);
+ virtual void apply(AssertionPipeline* assertionsToPreprocess);
NotUnsatCoresPass(ResourceManager* resourceManager,
theory::SubstitutionMap* topLevelSubstitutions);
private:
@@ -98,39 +98,39 @@ class NotUnsatCoresPass : public PreprocessingPass {
class BVToBoolPass : public PreprocessingPass {
public:
- virtual void apply(smt::AssertionPipeline* assertionsToPreprocess);
+ virtual void apply(AssertionPipeline* assertionsToPreprocess);
BVToBoolPass(ResourceManager* resourceManager,
TheoryEngine* theoryEngine);
private:
// Lift bit-vectors of size 1 to booleans
TheoryEngine* d_theoryEngine;
- void bvToBool(smt::AssertionPipeline* assertionsToPreprocess);
+ void bvToBool(AssertionPipeline* assertionsToPreprocess);
};
class BoolToBVPass : public PreprocessingPass {
public:
- virtual void apply(smt::AssertionPipeline* assertionsTopreprocess);
+ virtual void apply(AssertionPipeline* assertionsTopreprocess);
BoolToBVPass(ResourceManager* resourceManager,
TheoryEngine* theoryEngine);
private:
// Convert booleans to bit-vectors of size 1
TheoryEngine* d_theoryEngine;
- void boolToBv(smt::AssertionPipeline* assertionsToPreprocess);
+ void boolToBv(AssertionPipeline* assertionsToPreprocess);
};
class SepPreSkolemEmpPass : public PreprocessingPass {
public:
- virtual void apply(smt::AssertionPipeline* assertionsToPreprocess);
+ virtual void apply(AssertionPipeline* assertionsToPreprocess);
SepPreSkolemEmpPass(ResourceManager* resourceManager);
};
class QuantifiedPass : public PreprocessingPass {
public:
- virtual void apply(smt::AssertionPipeline* assertionsToPreprocess);
+ virtual void apply(AssertionPipeline* assertionsToPreprocess);
QuantifiedPass(ResourceManager* resourceManager,
- TheoryEngine* theoryEngine, NodeList* fmfRecFunctionsDefined,
- std::map<Node,TypeNode> fmfRecFunctionsAbs,
- std::map<Node, std::vector<Node> > fmfRecFunctionsConcrete);
+ TheoryEngine* theoryEngine, NodeList* &fmfRecFunctionsDefined,
+ std::map<Node,TypeNode> &fmfRecFunctionsAbs,
+ std::map<Node, std::vector<Node> > &fmfRecFunctionsConcrete);
private:
TheoryEngine* d_theoryEngine;
NodeList* d_fmfRecFunctionsDefined;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7881449dd..4f3b1b5d6 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -110,6 +110,7 @@ using namespace CVC4::smt;
using namespace CVC4::prop;
using namespace CVC4::context;
using namespace CVC4::theory;
+using namespace CVC4::preproc;
namespace CVC4 {
namespace smt {
@@ -3630,6 +3631,11 @@ void SmtEnginePrivate::processAssertions() {
}
if( d_smt.d_logic.isQuantified() ){
+/* preproc::QuantifiedPass pass(d_resourceManager, d_smt.d_theoryEngine,
+ d_smt.d_fmfRecFunctionsDefined, d_smt.d_fmfRecFunctionsAbs,
+ d_smt.d_fmfRecFunctionsConcrete);
+ pass.apply(&d_assertions);*/
+
Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << std::endl;
dumpAssertions("pre-skolem-quant", d_assertions);
@@ -3655,6 +3661,7 @@ void SmtEnginePrivate::processAssertions() {
qm.finalizeDefinitions();
}
+
//fmf-fun : assume admissible functions, applying preprocessing reduction to FMF
if( options::fmfFunWellDefined() ){
quantifiers::FunDefFmf fdf;
@@ -3685,11 +3692,7 @@ void SmtEnginePrivate::processAssertions() {
}
}
Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << std::endl;
- /* preproc::QuantifiedPass pass(d_resourceManager, d_smt.d_theoryEngine,
- d_smt.d_fmfRecFunctionsDefined, d_smt.d_fmfRecFunctionsAbs,
- d_smt.d_fmfRecFunctionsConcrete);
- pass.apply(&d_assertions);*/
- }
+}
if( options::sortInference() || options::ufssFairnessMonotone() ){
//sort inference technique
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback