diff options
author | Justin Xu <justinx@barrett5.stanford.edu> | 2017-07-12 22:05:26 -0700 |
---|---|---|
committer | Justin Xu <justinx@barrett5.stanford.edu> | 2017-07-24 15:47:17 -0700 |
commit | d6d90bb120c743ebae98f5a6cd87a87c524fbcb7 (patch) | |
tree | 17e47f44267249501d8388d4e10ef5d332f94adb | |
parent | 0e3c318e0d88687ab0c2d1bf380a25f9e41817af (diff) |
QuantifiedPass bugged,commented out
-rw-r--r-- | src/preproc/preprocessing_pass.h | 9 | ||||
-rw-r--r-- | src/preproc/preprocessing_passes_core.cpp | 37 | ||||
-rw-r--r-- | src/preproc/preprocessing_passes_core.h | 38 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 13 |
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 |