Updates not related to creation for eliminating Expr-level datatype (#4838)
[cvc5.git] / src / preprocessing / passes / extended_rewriter_pass.h
1 /********************* */
2 /*! \file extended_rewriter_pass.h
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Haniel Barbosa, Mathias Preiner
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
11 **
12 ** \brief The ExtRewPre preprocessing pass
13 **
14 ** Applies the extended rewriter to assertions
15 **/
16
17 #include "cvc4_private.h"
18
19 #ifndef CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H
20 #define CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H
21
22 #include "preprocessing/preprocessing_pass.h"
23 #include "preprocessing/preprocessing_pass_context.h"
24
25 namespace CVC4 {
26 namespace preprocessing {
27 namespace passes {
28
29 class ExtRewPre : public PreprocessingPass
30 {
31 public:
32 ExtRewPre(PreprocessingPassContext* preprocContext);
33
34 protected:
35 PreprocessingPassResult applyInternal(
36 AssertionPipeline* assertionsToPreprocess) override;
37 };
38
39 } // namespace passes
40 } // namespace preprocessing
41 } // namespace CVC4
42
43 #endif /* CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H */