1 /********************* */
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2021 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
12 ** \brief The rewrite preprocessing pass
14 ** Calls the rewriter on every assertion
17 #include "preprocessing/passes/rewrite.h"
19 #include "preprocessing/assertion_pipeline.h"
20 #include "theory/rewriter.h"
23 namespace preprocessing
{
26 using namespace CVC4::theory
;
29 Rewrite::Rewrite(PreprocessingPassContext
* preprocContext
)
30 : PreprocessingPass(preprocContext
, "rewrite"){};
33 PreprocessingPassResult
Rewrite::applyInternal(
34 AssertionPipeline
* assertionsToPreprocess
)
36 for (unsigned i
= 0; i
< assertionsToPreprocess
->size(); ++i
) {
37 assertionsToPreprocess
->replace(i
, Rewriter::rewrite((*assertionsToPreprocess
)[i
]));
40 return PreprocessingPassResult::NO_CONFLICT
;
45 } // namespace preprocessing