diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-11 23:25:15 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-11 23:25:15 -0500 |
commit | d4c7b0b250a419ec149f973abcb1c1bf3886cef3 (patch) | |
tree | b376444a53e3657c60241980b37be0ec345167f4 /src/theory/theory_preprocessor.h | |
parent | d7847d052eb45695f24b2d534d3b6fb1551302ea (diff) |
(proof-new) Split TheoryEngine (#4558)
This PR splits two classes from TheoryEngine (EngineOutputChannel and TheoryPreprocess) that will be undergoing further refactoring for proofs.
This PR does not change their behavior and is code-move only modulo a few cosmetic changes.
Diffstat (limited to 'src/theory/theory_preprocessor.h')
-rw-r--r-- | src/theory/theory_preprocessor.h | 81 |
1 files changed, 81 insertions, 0 deletions
diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h new file mode 100644 index 000000000..f6caa10ec --- /dev/null +++ b/src/theory/theory_preprocessor.h @@ -0,0 +1,81 @@ +/********************* */ +/*! \file theory_preprocessor.h + ** \verbatim + ** Top contributors (to current version): + ** Dejan Jovanovic, Morgan Deters, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 theory preprocessor. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__THEORY_PREPROCESSOR_H +#define CVC4__THEORY__THEORY_PREPROCESSOR_H + +#include <unordered_map> + +#include "expr/node.h" +#include "preprocessing/assertion_pipeline.h" + +namespace CVC4 { + +class LogicInfo; +class TheoryEngine; +class RemoveTermFormulas; +class LazyCDProof; + +namespace theory { + +/** + * The preprocessor used in TheoryEngine. + */ +class TheoryPreprocessor +{ + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; + + public: + /** Constructs a theory preprocessor */ + TheoryPreprocessor(TheoryEngine& engine, RemoveTermFormulas& tfr); + /** Destroys a theory preprocessor */ + ~TheoryPreprocessor(); + /** Clear the cache of this class */ + void clearCache(); + /** + * Preprocesses node and stores it along with lemmas generated by + * preprocessing into the assertion pipeline lemmas. The (optional) argument + * lcp is the proof that stores a proof of all top-level formulas in lemmas, + * assuming that lcp initially contains a proof of node. The flag + * doTheoryPreprocess is whether we should run theory-specific preprocessing. + */ + void preprocess(TNode node, + preprocessing::AssertionPipeline& lemmas, + bool doTheoryPreprocess); + /** + * Runs theory specific preprocessing on the non-Boolean parts of + * the formula. This is only called on input assertions, after ITEs + * have been removed. + */ + Node theoryPreprocess(TNode node); + + private: + /** Reference to owning theory engine */ + TheoryEngine& d_engine; + /** Logic info of theory engine */ + const LogicInfo& d_logicInfo; + /** Cache for theory-preprocessing of assertions */ + NodeMap d_ppCache; + /** The term formula remover */ + RemoveTermFormulas& d_tfr; + /** Helper for theoryPreprocess */ + Node ppTheoryRewrite(TNode term); +}; + +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__THEORY_PREPROCESSOR_H */ |