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 |
57568 |
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 |
57568 |
d_secondBound(c) |
36 |
|
{ |
37 |
57568 |
} |
38 |
|
|
39 |
116275 |
Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf) |
40 |
|
{ |
41 |
|
// check conflict |
42 |
232550 |
Node prev = isSuf ? d_secondBound : d_firstBound; |
43 |
116275 |
if (!prev.isNull()) |
44 |
|
{ |
45 |
203168 |
Trace("strings-eager-pconf-debug") << "Check conflict " << prev << ", " << t |
46 |
101584 |
<< " post=" << isSuf << std::endl; |
47 |
101735 |
Node prevC = utils::getConstantEndpoint(prev, isSuf); |
48 |
101584 |
Assert(!prevC.isNull()); |
49 |
101584 |
Assert(prevC.isConst()); |
50 |
101584 |
if (c.isNull()) |
51 |
|
{ |
52 |
100089 |
c = utils::getConstantEndpoint(t, isSuf); |
53 |
100089 |
Assert(!c.isNull()); |
54 |
|
} |
55 |
101584 |
Assert(c.isConst()); |
56 |
101584 |
bool conflict = false; |
57 |
|
// if the constant prefixes are different |
58 |
101584 |
if (c != prevC) |
59 |
|
{ |
60 |
|
// conflicts between constants should be handled by equality engine |
61 |
24439 |
Assert(!t.isConst() || !prev.isConst()); |
62 |
48878 |
Trace("strings-eager-pconf-debug") |
63 |
24439 |
<< "Check conflict constants " << prevC << ", " << c << std::endl; |
64 |
24439 |
size_t pvs = Word::getLength(prevC); |
65 |
24439 |
size_t cvs = Word::getLength(c); |
66 |
48724 |
if (pvs == cvs || (pvs > cvs && t.isConst()) |
67 |
48724 |
|| (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 |
349 |
conflict = true; |
73 |
|
} |
74 |
|
else |
75 |
|
{ |
76 |
48180 |
Node larges = pvs > cvs ? prevC : c; |
77 |
48180 |
Node smalls = pvs > cvs ? c : prevC; |
78 |
24090 |
if (isSuf) |
79 |
|
{ |
80 |
13553 |
conflict = !Word::hasSuffix(larges, smalls); |
81 |
|
} |
82 |
|
else |
83 |
|
{ |
84 |
10537 |
conflict = !Word::hasPrefix(larges, smalls); |
85 |
|
} |
86 |
|
} |
87 |
24439 |
if (!conflict && (pvs > cvs || prev.isConst())) |
88 |
|
{ |
89 |
|
// current is subsumed, either shorter prefix or the other is a full |
90 |
|
// constant |
91 |
23723 |
return Node::null(); |
92 |
|
} |
93 |
|
} |
94 |
77145 |
else if (!t.isConst()) |
95 |
|
{ |
96 |
|
// current is subsumed since the other may be a full constant |
97 |
77145 |
return Node::null(); |
98 |
|
} |
99 |
716 |
if (conflict) |
100 |
|
{ |
101 |
1130 |
Trace("strings-eager-pconf") |
102 |
565 |
<< "Conflict for " << prevC << ", " << c << std::endl; |
103 |
1130 |
Node ret = mkMergeConflict(t, prev); |
104 |
1130 |
Trace("strings-eager-pconf") |
105 |
565 |
<< "String: eager prefix conflict: " << ret << std::endl; |
106 |
565 |
return ret; |
107 |
|
} |
108 |
|
} |
109 |
14842 |
if (isSuf) |
110 |
|
{ |
111 |
7417 |
d_secondBound = t; |
112 |
|
} |
113 |
|
else |
114 |
|
{ |
115 |
7425 |
d_firstBound = t; |
116 |
|
} |
117 |
14842 |
return Node::null(); |
118 |
|
} |
119 |
|
|
120 |
841 |
Node EqcInfo::mkMergeConflict(Node t, Node prev) |
121 |
|
{ |
122 |
1682 |
std::vector<Node> ccs; |
123 |
1682 |
Node r[2]; |
124 |
2523 |
for (unsigned i = 0; i < 2; i++) |
125 |
|
{ |
126 |
3364 |
Node tp = i == 0 ? t : prev; |
127 |
1682 |
if (tp.getKind() == STRING_IN_REGEXP) |
128 |
|
{ |
129 |
354 |
ccs.push_back(tp); |
130 |
354 |
r[i] = tp[0]; |
131 |
|
} |
132 |
|
else |
133 |
|
{ |
134 |
1328 |
r[i] = tp; |
135 |
|
} |
136 |
|
} |
137 |
841 |
if (r[0] != r[1]) |
138 |
|
{ |
139 |
841 |
ccs.push_back(r[0].eqNode(r[1])); |
140 |
|
} |
141 |
841 |
Assert(!ccs.empty()); |
142 |
1682 |
return NodeManager::currentNM()->mkAnd(ccs); |
143 |
|
} |
144 |
|
|
145 |
|
} // namespace strings |
146 |
|
} // namespace theory |
147 |
31137 |
} // namespace cvc5 |