From dc0dd5e34f9b2fe1ef79602cc2a5f3deeb7d684a Mon Sep 17 00:00:00 2001 From: justinxu421 Date: Sun, 10 Dec 2017 16:39:02 -0800 Subject: [PATCH] Add new infrastructure for preprocessing passes (#1053) 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). --- src/Makefile.am | 6 + src/options/mkoptions | 28 ++-- src/preprocessing/preprocessing_pass.cpp | 94 +++++++++++++ src/preprocessing/preprocessing_pass.h | 126 ++++++++++++++++++ .../preprocessing_pass_context.cpp | 26 ++++ .../preprocessing_pass_context.h | 49 +++++++ .../preprocessing_pass_registry.cpp | 49 +++++++ .../preprocessing_pass_registry.h | 60 +++++++++ src/smt/smt_engine.cpp | 43 +++--- src/smt/smt_engine.h | 6 + 10 files changed, 450 insertions(+), 37 deletions(-) create mode 100644 src/preprocessing/preprocessing_pass.cpp create mode 100644 src/preprocessing/preprocessing_pass.h create mode 100644 src/preprocessing/preprocessing_pass_context.cpp create mode 100644 src/preprocessing/preprocessing_pass_context.h create mode 100644 src/preprocessing/preprocessing_pass_registry.cpp create mode 100644 src/preprocessing/preprocessing_pass_registry.h 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& 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& ns) +{ + PROOF( + for (const auto& n + : ns) { ProofManager::currentPM()->addDependence(n, d_nodes[i]); }); + d_nodes[i] = NodeManager::currentNM()->mkConst(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 +#include + +#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 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& ref() { return d_nodes; } + const std::vector& ref() const { return d_nodes; } + + std::vector::const_iterator begin() const { return d_nodes.cbegin(); } + std::vector::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& addnDeps); + + /* + * Replaces an assertion with a vector of assertions and records the + * dependencies. + */ + void replace(size_t i, const std::vector& 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 + +#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) { + 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 +#include +#include + +#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); + + /** + * 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> + 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 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& ref() { return d_nodes; } - const vector& 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 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& 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; -- 2.30.2