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 |
21602 |
EqcInfo::EqcInfo(context::Context* c) |
30 |
|
: d_lengthTerm(c), |
31 |
|
d_codeTerm(c), |
32 |
|
d_cardinalityLemK(c), |
33 |
|
d_normalizedLength(c), |
34 |
|
d_prefixC(c), |
35 |
21602 |
d_suffixC(c) |
36 |
|
{ |
37 |
21602 |
} |
38 |
|
|
39 |
45415 |
Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf) |
40 |
|
{ |
41 |
|
// check conflict |
42 |
90830 |
Node prev = isSuf ? d_suffixC : d_prefixC; |
43 |
45415 |
if (!prev.isNull()) |
44 |
|
{ |
45 |
79630 |
Trace("strings-eager-pconf-debug") << "Check conflict " << prev << ", " << t |
46 |
39815 |
<< " post=" << isSuf << std::endl; |
47 |
39959 |
Node prevC = utils::getConstantEndpoint(prev, isSuf); |
48 |
39815 |
Assert(!prevC.isNull()); |
49 |
39815 |
Assert(prevC.isConst()); |
50 |
39815 |
if (c.isNull()) |
51 |
|
{ |
52 |
39607 |
c = utils::getConstantEndpoint(t, isSuf); |
53 |
39607 |
Assert(!c.isNull()); |
54 |
|
} |
55 |
39815 |
Assert(c.isConst()); |
56 |
39815 |
bool conflict = false; |
57 |
|
// if the constant prefixes are different |
58 |
39815 |
if (c != prevC) |
59 |
|
{ |
60 |
|
// conflicts between constants should be handled by equality engine |
61 |
11678 |
Assert(!t.isConst() || !prev.isConst()); |
62 |
23356 |
Trace("strings-eager-pconf-debug") |
63 |
11678 |
<< "Check conflict constants " << prevC << ", " << c << std::endl; |
64 |
11678 |
size_t pvs = Word::getLength(prevC); |
65 |
11678 |
size_t cvs = Word::getLength(c); |
66 |
23288 |
if (pvs == cvs || (pvs > cvs && t.isConst()) |
67 |
23288 |
|| (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 |
229 |
conflict = true; |
73 |
|
} |
74 |
|
else |
75 |
|
{ |
76 |
22898 |
Node larges = pvs > cvs ? prevC : c; |
77 |
22898 |
Node smalls = pvs > cvs ? c : prevC; |
78 |
11449 |
if (isSuf) |
79 |
|
{ |
80 |
7018 |
conflict = !Word::hasSuffix(larges, smalls); |
81 |
|
} |
82 |
|
else |
83 |
|
{ |
84 |
4431 |
conflict = !Word::hasPrefix(larges, smalls); |
85 |
|
} |
86 |
|
} |
87 |
11678 |
if (!conflict && (pvs > cvs || prev.isConst())) |
88 |
|
{ |
89 |
|
// current is subsumed, either shorter prefix or the other is a full |
90 |
|
// constant |
91 |
11189 |
return Node::null(); |
92 |
|
} |
93 |
|
} |
94 |
28137 |
else if (!t.isConst()) |
95 |
|
{ |
96 |
|
// current is subsumed since the other may be a full constant |
97 |
28137 |
return Node::null(); |
98 |
|
} |
99 |
489 |
if (conflict) |
100 |
|
{ |
101 |
690 |
Trace("strings-eager-pconf") |
102 |
345 |
<< "Conflict for " << prevC << ", " << c << std::endl; |
103 |
690 |
std::vector<Node> ccs; |
104 |
690 |
Node r[2]; |
105 |
1035 |
for (unsigned i = 0; i < 2; i++) |
106 |
|
{ |
107 |
1380 |
Node tp = i == 0 ? t : prev; |
108 |
690 |
if (tp.getKind() == STRING_IN_REGEXP) |
109 |
|
{ |
110 |
208 |
ccs.push_back(tp); |
111 |
208 |
r[i] = tp[0]; |
112 |
|
} |
113 |
|
else |
114 |
|
{ |
115 |
482 |
r[i] = tp; |
116 |
|
} |
117 |
|
} |
118 |
345 |
if (r[0] != r[1]) |
119 |
|
{ |
120 |
345 |
ccs.push_back(r[0].eqNode(r[1])); |
121 |
|
} |
122 |
345 |
Assert(!ccs.empty()); |
123 |
|
Node ret = |
124 |
690 |
ccs.size() == 1 ? ccs[0] : NodeManager::currentNM()->mkNode(AND, ccs); |
125 |
690 |
Trace("strings-eager-pconf") |
126 |
345 |
<< "String: eager prefix conflict: " << ret << std::endl; |
127 |
345 |
return ret; |
128 |
|
} |
129 |
|
} |
130 |
5744 |
if (isSuf) |
131 |
|
{ |
132 |
3237 |
d_suffixC = t; |
133 |
|
} |
134 |
|
else |
135 |
|
{ |
136 |
2507 |
d_prefixC = t; |
137 |
|
} |
138 |
5744 |
return Node::null(); |
139 |
|
} |
140 |
|
|
141 |
|
} // namespace strings |
142 |
|
} // namespace theory |
143 |
28194 |
} // namespace cvc5 |