summaryrefslogtreecommitdiff
path: root/src/preprocessing
diff options
context:
space:
mode:
Diffstat (limited to 'src/preprocessing')
-rw-r--r--src/preprocessing/passes/apply_substs.cpp74
-rw-r--r--src/preprocessing/passes/apply_substs.h49
-rw-r--r--src/preprocessing/preprocessing_pass.cpp7
-rw-r--r--src/preprocessing/preprocessing_pass.h37
-rw-r--r--src/preprocessing/preprocessing_pass_context.cpp9
-rw-r--r--src/preprocessing/preprocessing_pass_context.h13
6 files changed, 176 insertions, 13 deletions
diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp
new file mode 100644
index 000000000..6fb4b7793
--- /dev/null
+++ b/src/preprocessing/passes/apply_substs.cpp
@@ -0,0 +1,74 @@
+/********************* */
+/*! \file apply_substs.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 Apply substitutions preprocessing pass.
+ **
+ ** Apply top level substitutions to assertions, rewrite, and store back into
+ ** assertions.
+ **/
+
+#include "preprocessing/passes/apply_substs.h"
+
+#include "context/cdo.h"
+#include "theory/rewriter.h"
+#include "theory/substitutions.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+ApplySubsts::ApplySubsts(PreprocessingPassContext* preprocContext)
+ : PreprocessingPass(preprocContext, "apply-substs")
+{
+}
+
+PreprocessingPassResult ApplySubsts::applyInternal(
+ AssertionPipeline* assertionsToPreprocess)
+{
+ if (!options::unsatCores())
+ {
+ Chat() << "applying substitutions..." << std::endl;
+ Trace("apply-substs") << "SmtEnginePrivate::processAssertions(): "
+ << "applying substitutions" << std::endl;
+ // TODO(#1255): Substitutions in incremental mode should be managed with a
+ // proper data structure.
+
+ // When solving incrementally, all substitutions are piled into the
+ // assertion at d_substitutionsIndex: we don't want to apply substitutions
+ // to this assertion or information will be lost.
+ context::CDO<unsigned>& substs_index =
+ assertionsToPreprocess->getSubstitutionsIndex();
+ unsigned size = assertionsToPreprocess->size();
+ unsigned substitutionAssertion = substs_index > 0 ? substs_index : size;
+ for (unsigned i = 0; i < size; ++i)
+ {
+ if (i == substitutionAssertion)
+ {
+ continue;
+ }
+ Trace("apply-substs") << "applying to " << (*assertionsToPreprocess)[i]
+ << std::endl;
+ d_preprocContext->spendResource(options::preprocessStep());
+ assertionsToPreprocess->replace(
+ i,
+ theory::Rewriter::rewrite(
+ assertionsToPreprocess->getTopLevelSubstitutions().apply(
+ (*assertionsToPreprocess)[i])));
+ Trace("apply-substs") << " got " << (*assertionsToPreprocess)[i]
+ << std::endl;
+ }
+ }
+ return PreprocessingPassResult::NO_CONFLICT;
+}
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
diff --git a/src/preprocessing/passes/apply_substs.h b/src/preprocessing/passes/apply_substs.h
new file mode 100644
index 000000000..f2f77fd0e
--- /dev/null
+++ b/src/preprocessing/passes/apply_substs.h
@@ -0,0 +1,49 @@
+/********************* */
+/*! \file apply_substs.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 Apply substitutions preprocessing pass.
+ **
+ ** Apply top level substitutions to assertions, rewrite, and store back into
+ ** assertions.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H
+#define __CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class ApplySubsts : public PreprocessingPass
+{
+ public:
+ ApplySubsts(PreprocessingPassContext* preprocContext);
+
+ protected:
+ /**
+ * Apply assertionsToPreprocess->getTopLevelSubstitutions() to the
+ * assertions, in assertionsToPreprocess, rewrite, and store back into
+ * given assertion pipeline.
+ */
+ PreprocessingPassResult applyInternal(
+ AssertionPipeline* assertionsToPreprocess) override;
+};
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
+
+#endif
diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp
index 06992dedc..97b05802d 100644
--- a/src/preprocessing/preprocessing_pass.cpp
+++ b/src/preprocessing/preprocessing_pass.cpp
@@ -2,7 +2,7 @@
/*! \file preprocessing_pass.cpp
** \verbatim
** Top contributors (to current version):
- ** Justin Xu
+ ** Justin Xu, Aina Niemetz
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
@@ -24,6 +24,11 @@
namespace CVC4 {
namespace preprocessing {
+AssertionPipeline::AssertionPipeline(context::Context* context)
+ : d_substitutionsIndex(context, 0), d_topLevelSubstitutions(context)
+{
+}
+
void AssertionPipeline::replace(size_t i, Node n) {
PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]););
d_nodes[i] = n;
diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h
index d57484eff..441d1c7cd 100644
--- a/src/preprocessing/preprocessing_pass.h
+++ b/src/preprocessing/preprocessing_pass.h
@@ -2,7 +2,7 @@
/*! \file preprocessing_pass.h
** \verbatim
** Top contributors (to current version):
- ** Justin Xu
+ ** Justin Xu, Aina Niemetz
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
@@ -34,19 +34,24 @@
#include <string>
#include <vector>
+#include "context/cdo.h"
#include "expr/node.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "smt/smt_engine_scope.h"
+#include "theory/substitutions.h"
namespace CVC4 {
namespace preprocessing {
-/* Assertion Pipeline stores a list of assertions modified by preprocessing
- * passes. */
-class AssertionPipeline {
- std::vector<Node> d_nodes;
-
+/**
+ * Assertion Pipeline stores a list of assertions modified by preprocessing
+ * passes.
+ */
+class AssertionPipeline
+{
public:
+ AssertionPipeline(context::Context* context);
+
size_t size() const { return d_nodes.size(); }
void resize(size_t n) { d_nodes.resize(n); }
@@ -80,6 +85,26 @@ class AssertionPipeline {
* dependencies.
*/
void replace(size_t i, const std::vector<Node>& ns);
+
+ context::CDO<unsigned>& getSubstitutionsIndex()
+ {
+ return d_substitutionsIndex;
+ }
+
+ theory::SubstitutionMap& getTopLevelSubstitutions()
+ {
+ return d_topLevelSubstitutions;
+ }
+
+ private:
+ std::vector<Node> d_nodes;
+
+ /* Index for where to store substitutions */
+ context::CDO<unsigned> d_substitutionsIndex;
+
+ /* The top level substitutions */
+ theory::SubstitutionMap d_topLevelSubstitutions;
+
}; /* class AssertionPipeline */
/**
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index d44f24e13..1f3d245d7 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -2,7 +2,7 @@
/*! \file preprocessing_pass_context.cpp
** \verbatim
** Top contributors (to current version):
- ** Justin Xu, Mathias Preiner
+ ** Justin Xu, Mathias Preiner, Aina Niemetz
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
@@ -19,8 +19,11 @@
namespace CVC4 {
namespace preprocessing {
-PreprocessingPassContext::PreprocessingPassContext(SmtEngine* smt)
- : d_smt(smt) {}
+PreprocessingPassContext::PreprocessingPassContext(
+ SmtEngine* smt, ResourceManager* resourceManager)
+ : d_smt(smt), d_resourceManager(resourceManager)
+{
+}
void PreprocessingPassContext::widenLogic(theory::TheoryId id)
{
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index f85f0af7d..9927cd8fb 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -2,7 +2,7 @@
/*! \file preprocessing_pass_context.h
** \verbatim
** Top contributors (to current version):
- ** Justin Xu, Mathias Preiner, Andres Noetzli
+ ** Justin Xu, Aina Niemetz, Mathias Preiner
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
@@ -25,18 +25,24 @@
#include "decision/decision_engine.h"
#include "smt/smt_engine.h"
#include "theory/theory_engine.h"
+#include "util/resource_manager.h"
namespace CVC4 {
namespace preprocessing {
-class PreprocessingPassContext {
+class PreprocessingPassContext
+{
public:
- PreprocessingPassContext(SmtEngine* smt);
+ PreprocessingPassContext(SmtEngine* smt, ResourceManager* resourceManager);
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; }
context::Context* getUserContext() { return d_smt->d_userContext; }
+ void spendResource(unsigned amount)
+ {
+ d_resourceManager->spendResource(amount);
+ }
/* Widen the logic to include the given theory. */
void widenLogic(theory::TheoryId id);
@@ -44,6 +50,7 @@ class PreprocessingPassContext {
private:
/* Pointer to the SmtEngine that this context was created in. */
SmtEngine* d_smt;
+ ResourceManager* d_resourceManager;
}; // class PreprocessingPassContext
} // namespace preprocessing
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback