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 "theory/rewriter.h"
20 #include "theory/theory_engine.h"
23 namespace preprocessing
{
26 using namespace CVC4::theory
;
28 TheoryPreprocess::TheoryPreprocess(PreprocessingPassContext
* preprocContext
)
29 : PreprocessingPass(preprocContext
, "theory-preprocess"){};
31 PreprocessingPassResult
TheoryPreprocess::applyInternal(
32 AssertionPipeline
* assertionsToPreprocess
)
34 TheoryEngine
* te
= d_preprocContext
->getTheoryEngine();
35 te
->preprocessStart();
36 for (size_t i
= 0, size
= assertionsToPreprocess
->size(); i
< size
; ++i
)
38 TNode a
= (*assertionsToPreprocess
)[i
];
39 Assert(Rewriter::rewrite(a
) == a
);
40 assertionsToPreprocess
->replace(i
, te
->preprocess(a
));
41 a
= (*assertionsToPreprocess
)[i
];
42 Assert(Rewriter::rewrite(a
) == a
);
44 return PreprocessingPassResult::NO_CONFLICT
;
49 } // namespace preprocessing