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 |
|
* Implementation of equivalence class info for the theory of strings. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/strings/eqc_info.h" |
17 |
|
|
18 |
|
#include "theory/strings/theory_strings_utils.h" |
19 |
|
#include "theory/strings/word.h" |
20 |
|
|
21 |
|
using namespace std; |
22 |
|
using namespace cvc5::context; |
23 |
|
using namespace cvc5::kind; |
24 |
|
|
25 |
|
namespace cvc5 { |
26 |
|
namespace theory { |
27 |
|
namespace strings { |
28 |
|
|
29 |
56279 |
EqcInfo::EqcInfo(context::Context* c) |
30 |
|
: d_lengthTerm(c), |
31 |
|
d_codeTerm(c), |
32 |
|
d_cardinalityLemK(c), |
33 |
|
d_normalizedLength(c), |
34 |
|
d_firstBound(c), |
35 |
56279 |
d_secondBound(c) |
36 |
|
{ |
37 |
56279 |
} |
38 |
|
|
39 |
93055 |
Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf) |
40 |
|
{ |
41 |
|
// check conflict |
42 |
186110 |
Node prev = isSuf ? d_secondBound : d_firstBound; |
43 |
93055 |
if (!prev.isNull()) |
44 |
|
{ |
45 |
158478 |
Trace("strings-eager-pconf-debug") << "Check conflict " << prev << ", " << t |
46 |
79239 |
<< " post=" << isSuf << std::endl; |
47 |
79364 |
Node prevC = utils::getConstantEndpoint(prev, isSuf); |
48 |
79239 |
Assert(!prevC.isNull()); |
49 |
79239 |
Assert(prevC.isConst()); |
50 |
79239 |
if (c.isNull()) |
51 |
|
{ |
52 |
78382 |
c = utils::getConstantEndpoint(t, isSuf); |
53 |
78382 |
Assert(!c.isNull()); |
54 |
|
} |
55 |
79239 |
Assert(c.isConst()); |
56 |
79239 |
bool conflict = false; |
57 |
|
// if the constant prefixes are different |
58 |
79239 |
if (c != prevC) |
59 |
|
{ |
60 |
|
// conflicts between constants should be handled by equality engine |
61 |
20917 |
Assert(!t.isConst() || !prev.isConst()); |
62 |
41834 |
Trace("strings-eager-pconf-debug") |
63 |
20917 |
<< "Check conflict constants " << prevC << ", " << c << std::endl; |
64 |
20917 |
size_t pvs = Word::getLength(prevC); |
65 |
20917 |
size_t cvs = Word::getLength(c); |
66 |
41692 |
if (pvs == cvs || (pvs > cvs && t.isConst()) |
67 |
41692 |
|| (cvs > pvs && prev.isConst())) |
68 |
|
{ |
69 |
|
// If equal length, cannot be equal due to node check above. |
70 |
|
// If one is fully constant and has less length than the other, then the |
71 |
|
// other will not fit and we are in conflict. |
72 |
325 |
conflict = true; |
73 |
|
} |
74 |
|
else |
75 |
|
{ |
76 |
41184 |
Node larges = pvs > cvs ? prevC : c; |
77 |
41184 |
Node smalls = pvs > cvs ? c : prevC; |
78 |
20592 |
if (isSuf) |
79 |
|
{ |
80 |
11082 |
conflict = !Word::hasSuffix(larges, smalls); |
81 |
|
} |
82 |
|
else |
83 |
|
{ |
84 |
9510 |
conflict = !Word::hasPrefix(larges, smalls); |
85 |
|
} |
86 |
|
} |
87 |
20917 |
if (!conflict && (pvs > cvs || prev.isConst())) |
88 |
|
{ |
89 |
|
// current is subsumed, either shorter prefix or the other is a full |
90 |
|
// constant |
91 |
20271 |
return Node::null(); |
92 |
|
} |
93 |
|
} |
94 |
58322 |
else if (!t.isConst()) |
95 |
|
{ |
96 |
|
// current is subsumed since the other may be a full constant |
97 |
58322 |
return Node::null(); |
98 |
|
} |
99 |
646 |
if (conflict) |
100 |
|
{ |
101 |
1042 |
Trace("strings-eager-pconf") |
102 |
521 |
<< "Conflict for " << prevC << ", " << c << std::endl; |
103 |
1042 |
Node ret = mkMergeConflict(t, prev); |
104 |
1042 |
Trace("strings-eager-pconf") |
105 |
521 |
<< "String: eager prefix conflict: " << ret << std::endl; |
106 |
521 |
return ret; |
107 |
|
} |
108 |
|
} |
109 |
13941 |
if (isSuf) |
110 |
|
{ |
111 |
6983 |
d_secondBound = t; |
112 |
|
} |
113 |
|
else |
114 |
|
{ |
115 |
6958 |
d_firstBound = t; |
116 |
|
} |
117 |
13941 |
return Node::null(); |
118 |
|
} |
119 |
|
|
120 |
796 |
Node EqcInfo::mkMergeConflict(Node t, Node prev) |
121 |
|
{ |
122 |
1592 |
std::vector<Node> ccs; |
123 |
1592 |
Node r[2]; |
124 |
2388 |
for (unsigned i = 0; i < 2; i++) |
125 |
|
{ |
126 |
3184 |
Node tp = i == 0 ? t : prev; |
127 |
1592 |
if (tp.getKind() == STRING_IN_REGEXP) |
128 |
|
{ |
129 |
311 |
ccs.push_back(tp); |
130 |
311 |
r[i] = tp[0]; |
131 |
|
} |
132 |
|
else |
133 |
|
{ |
134 |
1281 |
r[i] = tp; |
135 |
|
} |
136 |
|
} |
137 |
796 |
if (r[0] != r[1]) |
138 |
|
{ |
139 |
796 |
ccs.push_back(r[0].eqNode(r[1])); |
140 |
|
} |
141 |
796 |
Assert(!ccs.empty()); |
142 |
1592 |
return NodeManager::currentNM()->mkAnd(ccs); |
143 |
|
} |
144 |
|
|
145 |
|
} // namespace strings |
146 |
|
} // namespace theory |
147 |
31137 |
} // namespace cvc5 |