This commit adds new infrastructure for preprocessing passes. It is preparation only, it does not change how the current preprocessing passes work (this will be done in future commits).
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 \
# parse attributes
i=$(($type_pos+1))
+ colon_pattern='^\:'
while [ $i -lt ${#args[@]} ]; do
attribute="${args[$i]}"
case "$attribute" in
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
;;
: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
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\"
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\"
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')"
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
#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"
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;
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;
/** 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 */
finishRegisterTheory(d_theoryEngine->theoryOf(id));
}
});
-
+ d_private->finishInit();
Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl;
}
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) {
}
// 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
class UserContext;
}/* CVC4::context namespace */
+namespace preprocessing {
+class PreprocessingPassContext;
+}
+
namespace prop {
class PropEngine;
}/* CVC4::prop namespace */
*/
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;
projects / cvc5.git / commitdiff