summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Makefile.am6
-rwxr-xr-xsrc/options/mkoptions28
-rw-r--r--src/preprocessing/preprocessing_pass.cpp94
-rw-r--r--src/preprocessing/preprocessing_pass.h126
-rw-r--r--src/preprocessing/preprocessing_pass_context.cpp26
-rw-r--r--src/preprocessing/preprocessing_pass_context.h49
-rw-r--r--src/preprocessing/preprocessing_pass_registry.cpp49
-rw-r--r--src/preprocessing/preprocessing_pass_registry.h60
-rw-r--r--src/smt/smt_engine.cpp43
-rw-r--r--src/smt/smt_engine.h6
10 files changed, 450 insertions, 37 deletions
diff --git a/src/Makefile.am b/src/Makefile.am
index ff79cc4a4..098fe4025 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -62,6 +62,12 @@ libcvc4_la_SOURCES = \
decision/decision_strategy.h \
decision/justification_heuristic.cpp \
decision/justification_heuristic.h \
+ preprocessing/preprocessing_pass.cpp \
+ preprocessing/preprocessing_pass.h \
+ preprocessing/preprocessing_pass_context.cpp \
+ preprocessing/preprocessing_pass_context.h \
+ preprocessing/preprocessing_pass_registry.cpp \
+ preprocessing/preprocessing_pass_registry.h \
printer/dagification_visitor.cpp \
printer/dagification_visitor.h \
printer/printer.cpp \
diff --git a/src/options/mkoptions b/src/options/mkoptions
index dd5575644..4c640c9c3 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -407,6 +407,7 @@ function handle_option {
# parse attributes
i=$(($type_pos+1))
+ colon_pattern='^\:'
while [ $i -lt ${#args[@]} ]; do
attribute="${args[$i]}"
case "$attribute" in
@@ -422,19 +423,19 @@ function handle_option {
handlers="${args[$i]}"
;;
:predicate)
- while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
+ while [ $(($i+1)) -lt ${#args[@]} ] && ! [[ ${args[$(($i+1))]} =~ $colon_pattern ]]; do
let ++i
predicates="${predicates} ${args[$i]}"
done
;;
:notify)
- while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
+ while [ $(($i+1)) -lt ${#args[@]} ] && ! [[ ${args[$(($i+1))]} =~ $colon_pattern ]]; do
let ++i
notifications="${notifications} ${args[$i]}"
done
;;
:link)
- while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
+ while [ $(($i+1)) -lt ${#args[@]} ] && ! [[ ${args[$(($i+1))]} =~ $colon_pattern ]]; do
let ++i
link="${args[$i]}"
if expr "${args[$i]}" : '.*/' &>/dev/null; then
@@ -447,7 +448,7 @@ function handle_option {
;;
:link-smt)
j=0
- while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
+ while [ $(($i+1)) -lt ${#args[@]} ] && ! [[ ${args[$(($i+1))]} =~ $colon_pattern ]]; do
let ++i
let ++j
if [ $j -eq 3 ]; then
@@ -465,7 +466,7 @@ function handle_option {
fi
;;
:include)
- while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
+ while [ $(($i+1)) -lt ${#args[@]} ] && ! [[ ${args[$(($i+1))]} =~ $colon_pattern ]]; do
let ++i
module_includes="${module_includes}
#line $lineno \"$kf\"
@@ -473,7 +474,7 @@ function handle_option {
done
;;
:handler-include|:predicate-include)
- while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
+ while [ $(($i+1)) -lt ${#args[@]} ] && ! [[ ${args[$(($i+1))]} =~ $colon_pattern ]]; do
let ++i
option_handler_includes="${option_handler_includes}
#line $lineno \"$kf\"
@@ -1582,18 +1583,23 @@ function scan_module {
while IFS= read -r line; do
let ++lineno
# read any continuations of the line
- while expr "$line" : '.*\\$' &>/dev/null; do
+ continuation_pattern='^.*\\$'
+ while [[ $line =~ $continuation_pattern ]]; do
IFS= read -r line2
line="$(echo "$line" | sed 's,\\$,,')$line2"
let ++lineno
done
- if expr "$line" : '[ ].*' &>/dev/null; then
+ doc_pattern='^[ ].*'
+ empty_doc_pattern='^\.[ ]*$'
+ malformed_pattern='^\.'
+ doc_alternate_pattern='^/.*'
+ if [[ $line =~ $doc_pattern ]]; then
doc "$(echo "$line" | sed 's,^[ ],,')"
- elif expr "$line" : '\.[ ]*$' &>/dev/null; then
+ elif [[ $line =~ $empty_doc_pattern ]]; then
doc ""
- elif expr "$line" : '\.' &>/dev/null; then
+ elif [[ $line =~ $malformed_pattern ]]; then
ERR "malformed line during processing of option \`$internal': continuation lines should not have content"
- elif expr "$line" : '/.*' &>/dev/null; then
+ elif [[ $line =~ $doc_alternate_pattern ]]; then
doc-alternate "$(echo "$line" | sed 's,^/,,')"
else
line="$(echo "$line" | sed 's,\([<>&()!?*]\),\\\1,g')"
diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp
new file mode 100644
index 000000000..bf2e59229
--- /dev/null
+++ b/src/preprocessing/preprocessing_pass.cpp
@@ -0,0 +1,94 @@
+/********************* */
+/*! \file preprocessing_pass.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Justin Xu
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The preprocessing pass super class
+ **
+ ** Preprocessing pass super class.
+ **/
+
+#include "preprocessing/preprocessing_pass.h"
+
+#include "expr/node_manager.h"
+#include "proof/proof.h"
+#include "smt/dump.h"
+#include "smt/smt_statistics_registry.h"
+
+namespace CVC4 {
+namespace preprocessing {
+
+void AssertionPipeline::replace(size_t i, Node n) {
+ PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]););
+ d_nodes[i] = n;
+}
+
+void AssertionPipeline::replace(size_t i,
+ Node n,
+ const std::vector<Node>& addnDeps)
+{
+ PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]);
+ for (const auto& addnDep
+ : addnDeps) {
+ ProofManager::currentPM()->addDependence(n, addnDep);
+ });
+ d_nodes[i] = n;
+}
+
+void AssertionPipeline::replace(size_t i, const std::vector<Node>& ns)
+{
+ PROOF(
+ for (const auto& n
+ : ns) { ProofManager::currentPM()->addDependence(n, d_nodes[i]); });
+ d_nodes[i] = NodeManager::currentNM()->mkConst<bool>(true);
+
+ for (const auto& n : ns)
+ {
+ d_nodes.push_back(n);
+ }
+}
+
+PreprocessingPassResult PreprocessingPass::apply(
+ AssertionPipeline* assertionsToPreprocess) {
+ TimerStat::CodeTimer codeTimer(d_timer);
+ Trace("preprocessing") << "PRE " << d_name << std::endl;
+ Chat() << d_name << "..." << std::endl;
+ dumpAssertions(("pre-" + d_name).c_str(), *assertionsToPreprocess);
+ PreprocessingPassResult result = applyInternal(assertionsToPreprocess);
+ dumpAssertions(("post-" + d_name).c_str(), *assertionsToPreprocess);
+ Trace("preprocessing") << "POST " << d_name << std::endl;
+ return result;
+}
+
+void PreprocessingPass::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
+ for (const auto& n : assertionList) {
+ Dump("assertions") << AssertCommand(Expr(n.toExpr()));
+ }
+ }
+}
+
+PreprocessingPass::PreprocessingPass(PreprocessingPassContext* preprocContext,
+ const std::string& name)
+ : d_name(name), d_timer("preprocessing::" + name) {
+ d_preprocContext = preprocContext;
+ smtStatisticsRegistry()->registerStat(&d_timer);
+}
+
+PreprocessingPass::~PreprocessingPass() {
+ Assert(smt::smtEngineInScope());
+ if (smtStatisticsRegistry() != nullptr) {
+ smtStatisticsRegistry()->unregisterStat(&d_timer);
+ }
+}
+
+} // namespace preprocessing
+} // namespace CVC4
diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h
new file mode 100644
index 000000000..f7b30aa74
--- /dev/null
+++ b/src/preprocessing/preprocessing_pass.h
@@ -0,0 +1,126 @@
+/********************* */
+/*! \file preprocessing_pass.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Justin Xu
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The preprocessing pass super class
+ **
+ ** Implementation of the preprocessing pass super class. Preprocessing passes
+ ** that inherit from this class, need to pass their name to the constructor to
+ ** register the pass appropriately. The core of a preprocessing pass lives
+ ** in applyInternal(), which operates on a list of assertions and is called
+ ** from apply() in the super class. The apply() method automatically takes
+ ** care of the following:
+ **
+ ** - Dumping assertions before and after the pass
+ ** - Initializing the timer
+ ** - Tracing and chatting
+ **
+ ** Optionally, preprocessing passes can overwrite the initInteral() method to
+ ** do work that only needs to be done once.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_H
+#define __CVC4__PREPROCESSING__PREPROCESSING_PASS_H
+
+#include <string>
+#include <vector>
+
+#include "expr/node.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "smt/smt_engine_scope.h"
+
+namespace CVC4 {
+namespace preprocessing {
+
+/* Assertion Pipeline stores a list of assertions modified by preprocessing
+ * passes. */
+class AssertionPipeline {
+ std::vector<Node> d_nodes;
+
+ public:
+ size_t size() const { return d_nodes.size(); }
+
+ void resize(size_t n) { d_nodes.resize(n); }
+ void clear() { d_nodes.clear(); }
+
+ Node& operator[](size_t i) { return d_nodes[i]; }
+ const Node& operator[](size_t i) const { return d_nodes[i]; }
+ void push_back(Node n) { d_nodes.push_back(n); }
+
+ std::vector<Node>& ref() { return d_nodes; }
+ const std::vector<Node>& ref() const { return d_nodes; }
+
+ std::vector<Node>::const_iterator begin() const { return d_nodes.cbegin(); }
+ std::vector<Node>::const_iterator end() const { return d_nodes.cend(); }
+
+ /*
+ * Replaces assertion i with node n and records the dependency between the
+ * original assertion and its replacement.
+ */
+ void replace(size_t i, Node n);
+
+ /*
+ * Replaces assertion i with node n and records that this replacement depends
+ * on assertion i and the nodes listed in addnDeps. The dependency
+ * information is used for unsat cores and proofs.
+ */
+ void replace(size_t i, Node n, const std::vector<Node>& addnDeps);
+
+ /*
+ * Replaces an assertion with a vector of assertions and records the
+ * dependencies.
+ */
+ void replace(size_t i, const std::vector<Node>& ns);
+}; /* class AssertionPipeline */
+
+/**
+ * Preprocessing passes return a result which indicates whether a conflict has
+ * been detected during preprocessing.
+ */
+enum PreprocessingPassResult { CONFLICT, NO_CONFLICT };
+
+class PreprocessingPass {
+ public:
+ /* Preprocesses a list of assertions assertionsToPreprocess */
+ PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess);
+
+ PreprocessingPass(PreprocessingPassContext* preprocContext,
+ const std::string& name);
+ virtual ~PreprocessingPass();
+
+ protected:
+ /*
+ * Method for dumping assertions within a pass. Also called before and after
+ * applying the pass.
+ */
+ void dumpAssertions(const char* key, const AssertionPipeline& assertionList);
+
+ /*
+ * Abstract method that each pass implements to do the actual preprocessing.
+ */
+ virtual PreprocessingPassResult applyInternal(
+ AssertionPipeline* assertionsToPreprocess) = 0;
+
+ /* Context for Preprocessing Passes that initializes necessary variables */
+ PreprocessingPassContext* d_preprocContext;
+
+ private:
+ /* Name of pass */
+ std::string d_name;
+ /* Timer for registering the preprocessing time of this pass */
+ TimerStat d_timer;
+};
+
+} // namespace preprocessing
+} // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PREPROCESSING_PASS_H */
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
new file mode 100644
index 000000000..a738f9484
--- /dev/null
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -0,0 +1,26 @@
+/********************* */
+/*! \file preprocessing_pass_context.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Justin Xu
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The preprocessing pass context for passes
+ **
+ ** The preprocessing pass context for passes.
+ **/
+
+#include "preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+
+PreprocessingPassContext::PreprocessingPassContext(SmtEngine* smt)
+ : d_smt(smt) {}
+
+} // namespace preprocessing
+} // namespace CVC4
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
new file mode 100644
index 000000000..2e7a4eaf2
--- /dev/null
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -0,0 +1,49 @@
+/********************* */
+/*! \file preprocessing_pass_context.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Justin Xu
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The preprocessing pass context for passes
+ **
+ ** Implementation of the preprocessing pass context for passes. This context
+ ** allows preprocessing passes to retrieve information besides the assertions
+ ** from the solver and interact with it without getting full access.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
+#define __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
+
+#include "decision/decision_engine.h"
+#include "smt/smt_engine.h"
+#include "theory/arith/pseudoboolean_proc.h"
+#include "theory/booleans/circuit_propagator.h"
+#include "theory/theory_engine.h"
+
+namespace CVC4 {
+namespace preprocessing {
+
+class PreprocessingPassContext {
+ public:
+ PreprocessingPassContext(SmtEngine* smt);
+ SmtEngine* getSmt() { return d_smt; }
+ TheoryEngine* getTheoryEngine() { return d_smt->d_theoryEngine; }
+ DecisionEngine* getDecisionEngine() { return d_smt->d_decisionEngine; }
+ prop::PropEngine* getPropEngine() { return d_smt->d_propEngine; }
+
+ private:
+ /* Pointer to the SmtEngine that this context was created in. */
+ SmtEngine* d_smt;
+}; // class PreprocessingPassContext
+
+} // namespace preprocessing
+} // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H */
diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp
new file mode 100644
index 000000000..4f0693a25
--- /dev/null
+++ b/src/preprocessing/preprocessing_pass_registry.cpp
@@ -0,0 +1,49 @@
+/********************* */
+/*! \file preprocessing_pass_registry.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Justin Xu
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The preprocessing pass registry
+ **
+ ** The preprocessing pass registry.
+ **/
+
+#include "preprocessing/preprocessing_pass_registry.h"
+
+#include <utility>
+
+#include "base/cvc4_assert.h"
+#include "base/output.h"
+#include "preprocessing/preprocessing_pass.h"
+
+namespace CVC4 {
+namespace preprocessing {
+
+void PreprocessingPassRegistry::registerPass(
+ const std::string& ppName,
+ std::unique_ptr<PreprocessingPass> preprocessingPass) {
+ Debug("pp-registry") << "Registering pass " << ppName << std::endl;
+ Assert(preprocessingPass != nullptr);
+ Assert(!this->hasPass(ppName));
+ d_stringToPreprocessingPass[ppName] = std::move(preprocessingPass);
+}
+
+bool PreprocessingPassRegistry::hasPass(const std::string& ppName) {
+ return d_stringToPreprocessingPass.find(ppName) !=
+ d_stringToPreprocessingPass.end();
+}
+
+PreprocessingPass* PreprocessingPassRegistry::getPass(
+ const std::string& ppName) {
+ Assert(this->hasPass(ppName));
+ return d_stringToPreprocessingPass[ppName].get();
+}
+
+} // namespace preprocessing
+} // namespace CVC4
diff --git a/src/preprocessing/preprocessing_pass_registry.h b/src/preprocessing/preprocessing_pass_registry.h
new file mode 100644
index 000000000..75c66a035
--- /dev/null
+++ b/src/preprocessing/preprocessing_pass_registry.h
@@ -0,0 +1,60 @@
+/********************* */
+/*! \file preprocessing_pass_registry.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Justin Xu
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The preprocessing pass registry
+ **
+ ** The preprocessing pass registry keeps track of all the instances of
+ ** preprocessing passes. Upon creation, preprocessing passes are registered in
+ ** the registry, which then takes ownership of them.
+ **/
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H
+#define __CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H
+
+#include <memory>
+#include <string>
+#include <unordered_map>
+
+#include "decision/decision_engine.h"
+#include "preprocessing/preprocessing_pass.h"
+#include "theory/arith/pseudoboolean_proc.h"
+#include "theory/booleans/circuit_propagator.h"
+#include "theory/theory_engine.h"
+
+namespace CVC4 {
+namespace preprocessing {
+
+class PreprocessingPassRegistry {
+ public:
+ /**
+ * Registers a pass with a unique name and takes ownership of it.
+ */
+ void registerPass(const std::string& ppName,
+ std::unique_ptr<PreprocessingPass> preprocessingPass);
+
+ /**
+ * Retrieves a pass with a given name from registry.
+ */
+ PreprocessingPass* getPass(const std::string& ppName);
+
+ private:
+ bool hasPass(const std::string& ppName);
+
+ /* Stores all the registered preprocessing passes. */
+ std::unordered_map<std::string, std::unique_ptr<PreprocessingPass>>
+ d_stringToPreprocessingPass;
+}; // class PreprocessingPassRegistry
+
+} // namespace preprocessing
+} // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a007fa412..e7736ebfc 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -67,6 +67,9 @@
#include "options/strings_options.h"
#include "options/theory_options.h"
#include "options/uf_options.h"
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "preprocessing/preprocessing_pass_registry.h"
#include "printer/printer.h"
#include "proof/proof.h"
#include "proof/proof_manager.h"
@@ -110,6 +113,7 @@
using namespace std;
using namespace CVC4;
using namespace CVC4::smt;
+using namespace CVC4::preprocessing;
using namespace CVC4::prop;
using namespace CVC4::context;
using namespace CVC4::theory;
@@ -162,29 +166,6 @@ public:
Node getFormula() const { return d_formula; }
};/* class DefinedFunction */
-class AssertionPipeline {
- vector<Node> d_nodes;
-
-public:
-
- size_t size() const { return d_nodes.size(); }
-
- void resize(size_t n) { d_nodes.resize(n); }
- void clear() { d_nodes.clear(); }
-
- Node& operator[](size_t i) { return d_nodes[i]; }
- const Node& operator[](size_t i) const { return d_nodes[i]; }
- void push_back(Node n) { d_nodes.push_back(n); }
-
- vector<Node>& ref() { return d_nodes; }
- const vector<Node>& ref() const { return d_nodes; }
-
- void replace(size_t i, Node n) {
- PROOF( ProofManager::currentPM()->addDependence(n, d_nodes[i]); );
- d_nodes[i] = n;
- }
-};/* class AssertionPipeline */
-
struct SmtEngineStatistics {
/** time spent in gaussian elimination */
TimerStat d_gaussElimTime;
@@ -571,8 +552,12 @@ public:
/** Instance of the ITE remover */
RemoveTermFormulas d_iteRemover;
-private:
+ /* Finishes the initialization of the private portion of SMTEngine. */
+ void finishInit();
+ private:
+ std::unique_ptr<PreprocessingPassContext> d_preprocessingPassContext;
+ PreprocessingPassRegistry d_preprocessingPassRegistry;
theory::arith::PseudoBooleanProcessor d_pbsProcessor;
/** The top level substitutions */
@@ -1138,7 +1123,7 @@ void SmtEngine::finishInit() {
finishRegisterTheory(d_theoryEngine->theoryOf(id));
}
});
-
+ d_private->finishInit();
Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl;
}
@@ -2459,6 +2444,11 @@ bool SmtEngine::isDefinedFunction( Expr func ){
return d_definedFunctions->find(nf) != d_definedFunctions->end();
}
+void SmtEnginePrivate::finishInit() {
+ d_preprocessingPassContext.reset(new PreprocessingPassContext(&d_smt));
+ //TODO: register passes here
+}
+
Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
@@ -3018,7 +3008,8 @@ void SmtEnginePrivate::staticLearning() {
}
// do dumping (before/after any preprocessing pass)
-static void dumpAssertions(const char* key, const AssertionPipeline& assertionList) {
+static void dumpAssertions(const char* key,
+ const AssertionPipeline& assertionList) {
if( Dump.isOn("assertions") &&
Dump.isOn(string("assertions:") + key) ) {
// Push the simplified assertions to the dump output stream
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 404c9ebe1..c628a1952 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -70,6 +70,10 @@ namespace context {
class UserContext;
}/* CVC4::context namespace */
+namespace preprocessing {
+class PreprocessingPassContext;
+}
+
namespace prop {
class PropEngine;
}/* CVC4::prop namespace */
@@ -343,6 +347,8 @@ class CVC4_PUBLIC SmtEngine {
*/
void setLogicInternal() throw();
+ // TODO (Issue #1096): Remove this friend relationship.
+ friend class ::CVC4::preprocessing::PreprocessingPassContext;
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