1 /********************* */
2 /*! \file strings_eager_pp.cpp
4 ** Top contributors (to current version):
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
12 ** \brief The strings eager preprocess utility
15 #include "preprocessing/passes/strings_eager_pp.h"
17 #include "theory/strings/theory_strings_preprocess.h"
18 #include "theory/rewriter.h"
20 using namespace CVC4::theory
;
23 namespace preprocessing
{
26 StringsEagerPp::StringsEagerPp(PreprocessingPassContext
* preprocContext
)
27 : PreprocessingPass(preprocContext
, "strings-eager-pp"){};
29 PreprocessingPassResult
StringsEagerPp::applyInternal(
30 AssertionPipeline
* assertionsToPreprocess
)
32 NodeManager
* nm
= NodeManager::currentNM();
33 theory::strings::SkolemCache
skc(false);
34 theory::strings::StringsPreprocess
pp(&skc
);
35 for (size_t i
= 0, nasserts
= assertionsToPreprocess
->size(); i
< nasserts
;
38 Node prev
= (*assertionsToPreprocess
)[i
];
39 std::vector
<Node
> asserts
;
40 Node rew
= pp
.processAssertion(prev
, asserts
);
43 std::vector
<Node
> conj
;
45 conj
.insert(conj
.end(), asserts
.begin(), asserts
.end());
46 rew
= nm
->mkAnd(conj
);
50 assertionsToPreprocess
->replace(i
, theory::Rewriter::rewrite(rew
));
54 return PreprocessingPassResult::NO_CONFLICT
;
58 } // namespace preprocessing