1 /********************* */
2 /*! \file bv_abstraction.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 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 TheoryPreprocess preprocessing pass
14 ** Calls Theory::preprocess(...) on every assertion of the formula.
17 #include "preprocessing/passes/theory_preprocess.h"
19 #include "preprocessing/preprocessing_pass_registry.h"
20 #include "theory/rewriter.h"
21 #include "theory/theory_engine.h"
24 namespace preprocessing
{
27 using namespace CVC4::theory
;
29 TheoryPreprocess::TheoryPreprocess(PreprocessingPassContext
* preprocContext
)
30 : PreprocessingPass(preprocContext
, "theory-preprocess"){};
32 PreprocessingPassResult
TheoryPreprocess::applyInternal(
33 AssertionPipeline
* assertionsToPreprocess
)
35 TheoryEngine
* te
= d_preprocContext
->getTheoryEngine();
36 te
->preprocessStart();
37 for (size_t i
= 0, size
= assertionsToPreprocess
->size(); i
< size
; ++i
)
39 TNode a
= (*assertionsToPreprocess
)[i
];
40 Assert(Rewriter::rewrite(a
) == a
);
41 assertionsToPreprocess
->replace(i
, te
->preprocess(a
));
42 a
= (*assertionsToPreprocess
)[i
];
43 Assert(Rewriter::rewrite(a
) == a
);
45 return PreprocessingPassResult::NO_CONFLICT
;
48 static RegisterPass
<TheoryPreprocess
> X("theory-preprocess");
51 } // namespace preprocessing