1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* The strings eager preprocess utility. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "preprocessing/passes/strings_eager_pp.h" |
17 |
|
|
18 |
|
#include "preprocessing/assertion_pipeline.h" |
19 |
|
#include "theory/rewriter.h" |
20 |
|
#include "theory/strings/theory_strings_preprocess.h" |
21 |
|
|
22 |
|
using namespace cvc5::theory; |
23 |
|
|
24 |
|
namespace cvc5 { |
25 |
|
namespace preprocessing { |
26 |
|
namespace passes { |
27 |
|
|
28 |
9459 |
StringsEagerPp::StringsEagerPp(PreprocessingPassContext* preprocContext) |
29 |
9459 |
: PreprocessingPass(preprocContext, "strings-eager-pp"){}; |
30 |
|
|
31 |
36 |
PreprocessingPassResult StringsEagerPp::applyInternal( |
32 |
|
AssertionPipeline* assertionsToPreprocess) |
33 |
|
{ |
34 |
36 |
NodeManager* nm = NodeManager::currentNM(); |
35 |
72 |
theory::strings::SkolemCache skc(false); |
36 |
72 |
theory::strings::StringsPreprocess pp(&skc); |
37 |
127 |
for (size_t i = 0, nasserts = assertionsToPreprocess->size(); i < nasserts; |
38 |
|
++i) |
39 |
|
{ |
40 |
182 |
Node prev = (*assertionsToPreprocess)[i]; |
41 |
182 |
std::vector<Node> asserts; |
42 |
182 |
Node rew = pp.processAssertion(prev, asserts); |
43 |
91 |
if (!asserts.empty()) |
44 |
|
{ |
45 |
62 |
std::vector<Node> conj; |
46 |
31 |
conj.push_back(rew); |
47 |
31 |
conj.insert(conj.end(), asserts.begin(), asserts.end()); |
48 |
31 |
rew = nm->mkAnd(conj); |
49 |
|
} |
50 |
91 |
if (prev != rew) |
51 |
|
{ |
52 |
31 |
assertionsToPreprocess->replace(i, theory::Rewriter::rewrite(rew)); |
53 |
|
} |
54 |
|
} |
55 |
|
|
56 |
72 |
return PreprocessingPassResult::NO_CONFLICT; |
57 |
|
} |
58 |
|
|
59 |
|
} // namespace passes |
60 |
|
} // namespace preprocessing |
61 |
28191 |
} // namespace cvc5 |