diff options
Diffstat (limited to 'src/preprocessing/preprocessing_pass.h')
-rw-r--r-- | src/preprocessing/preprocessing_pass.h | 37 |
1 files changed, 31 insertions, 6 deletions
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 */ /** |