1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Tianyi Liang, Andres Noetzli |
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 eager solver. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/strings/eager_solver.h" |
17 |
|
|
18 |
|
#include "theory/strings/theory_strings_utils.h" |
19 |
|
|
20 |
|
using namespace cvc5::kind; |
21 |
|
|
22 |
|
namespace cvc5 { |
23 |
|
namespace theory { |
24 |
|
namespace strings { |
25 |
|
|
26 |
9853 |
EagerSolver::EagerSolver(SolverState& state) : d_state(state) {} |
27 |
|
|
28 |
9853 |
EagerSolver::~EagerSolver() {} |
29 |
|
|
30 |
119502 |
void EagerSolver::eqNotifyNewClass(TNode t) |
31 |
|
{ |
32 |
119502 |
Kind k = t.getKind(); |
33 |
119502 |
if (k == STRING_LENGTH || k == STRING_TO_CODE) |
34 |
|
{ |
35 |
34023 |
eq::EqualityEngine* ee = d_state.getEqualityEngine(); |
36 |
68046 |
Node r = ee->getRepresentative(t[0]); |
37 |
34023 |
EqcInfo* ei = d_state.getOrMakeEqcInfo(r); |
38 |
34023 |
if (k == STRING_LENGTH) |
39 |
|
{ |
40 |
31637 |
ei->d_lengthTerm = t[0]; |
41 |
|
} |
42 |
|
else |
43 |
|
{ |
44 |
2386 |
ei->d_codeTerm = t[0]; |
45 |
34023 |
} |
46 |
|
} |
47 |
85479 |
else if (t.isConst()) |
48 |
|
{ |
49 |
24976 |
if (t.getType().isStringLike()) |
50 |
|
{ |
51 |
10353 |
EqcInfo* ei = d_state.getOrMakeEqcInfo(t); |
52 |
10353 |
ei->d_prefixC = t; |
53 |
10353 |
ei->d_suffixC = t; |
54 |
|
} |
55 |
|
} |
56 |
60503 |
else if (k == STRING_CONCAT) |
57 |
|
{ |
58 |
10118 |
addEndpointsToEqcInfo(t, t, t); |
59 |
|
} |
60 |
119502 |
} |
61 |
|
|
62 |
1283956 |
void EagerSolver::eqNotifyMerge(TNode t1, TNode t2) |
63 |
|
{ |
64 |
1283956 |
EqcInfo* e2 = d_state.getOrMakeEqcInfo(t2, false); |
65 |
1283956 |
if (e2 == nullptr) |
66 |
|
{ |
67 |
949171 |
return; |
68 |
|
} |
69 |
334785 |
Assert(t1.getType().isStringLike()); |
70 |
334785 |
EqcInfo* e1 = d_state.getOrMakeEqcInfo(t1); |
71 |
|
// add information from e2 to e1 |
72 |
334785 |
if (!e2->d_lengthTerm.get().isNull()) |
73 |
|
{ |
74 |
334611 |
e1->d_lengthTerm.set(e2->d_lengthTerm); |
75 |
|
} |
76 |
334785 |
if (!e2->d_codeTerm.get().isNull()) |
77 |
|
{ |
78 |
10899 |
e1->d_codeTerm.set(e2->d_codeTerm); |
79 |
|
} |
80 |
334785 |
if (!e2->d_prefixC.get().isNull()) |
81 |
|
{ |
82 |
69152 |
d_state.setPendingPrefixConflictWhen( |
83 |
69152 |
e1->addEndpointConst(e2->d_prefixC, Node::null(), false)); |
84 |
|
} |
85 |
334785 |
if (!e2->d_suffixC.get().isNull()) |
86 |
|
{ |
87 |
99334 |
d_state.setPendingPrefixConflictWhen( |
88 |
99334 |
e1->addEndpointConst(e2->d_suffixC, Node::null(), true)); |
89 |
|
} |
90 |
334785 |
if (e2->d_cardinalityLemK.get() > e1->d_cardinalityLemK.get()) |
91 |
|
{ |
92 |
|
e1->d_cardinalityLemK.set(e2->d_cardinalityLemK); |
93 |
|
} |
94 |
334785 |
if (!e2->d_normalizedLength.get().isNull()) |
95 |
|
{ |
96 |
106 |
e1->d_normalizedLength.set(e2->d_normalizedLength); |
97 |
|
} |
98 |
|
} |
99 |
|
|
100 |
181108 |
void EagerSolver::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) |
101 |
|
{ |
102 |
181108 |
if (t1.getType().isStringLike()) |
103 |
|
{ |
104 |
|
// store disequalities between strings, may need to check if their lengths |
105 |
|
// are equal/disequal |
106 |
73265 |
d_state.addDisequality(t1, t2); |
107 |
|
} |
108 |
181108 |
} |
109 |
|
|
110 |
15185 |
void EagerSolver::addEndpointsToEqcInfo(Node t, Node concat, Node eqc) |
111 |
|
{ |
112 |
15185 |
Assert(concat.getKind() == STRING_CONCAT |
113 |
|
|| concat.getKind() == REGEXP_CONCAT); |
114 |
15185 |
EqcInfo* ei = nullptr; |
115 |
|
// check each side |
116 |
45555 |
for (unsigned r = 0; r < 2; r++) |
117 |
|
{ |
118 |
30370 |
unsigned index = r == 0 ? 0 : concat.getNumChildren() - 1; |
119 |
60740 |
Node c = utils::getConstantComponent(concat[index]); |
120 |
30370 |
if (!c.isNull()) |
121 |
|
{ |
122 |
9217 |
if (ei == nullptr) |
123 |
|
{ |
124 |
7416 |
ei = d_state.getOrMakeEqcInfo(eqc); |
125 |
|
} |
126 |
18434 |
Trace("strings-eager-pconf-debug") |
127 |
9217 |
<< "New term: " << concat << " for " << t << " with prefix " << c |
128 |
9217 |
<< " (" << (r == 1) << ")" << std::endl; |
129 |
9217 |
d_state.setPendingPrefixConflictWhen(ei->addEndpointConst(t, c, r == 1)); |
130 |
|
} |
131 |
|
} |
132 |
15185 |
} |
133 |
|
|
134 |
946267 |
void EagerSolver::notifyFact(TNode atom, |
135 |
|
bool polarity, |
136 |
|
TNode fact, |
137 |
|
bool isInternal) |
138 |
|
{ |
139 |
946267 |
if (atom.getKind() == STRING_IN_REGEXP) |
140 |
|
{ |
141 |
23941 |
if (polarity && atom[1].getKind() == REGEXP_CONCAT) |
142 |
|
{ |
143 |
5067 |
eq::EqualityEngine* ee = d_state.getEqualityEngine(); |
144 |
10134 |
Node eqc = ee->getRepresentative(atom[0]); |
145 |
5067 |
addEndpointsToEqcInfo(atom, atom[1], eqc); |
146 |
|
} |
147 |
|
} |
148 |
946267 |
} |
149 |
|
|
150 |
|
} // namespace strings |
151 |
|
} // namespace theory |
152 |
29340 |
} // namespace cvc5 |