1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, 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 |
|
* Sequences solver for seq.nth/seq.update. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/strings/array_solver.h" |
17 |
|
|
18 |
|
#include "theory/strings/arith_entail.h" |
19 |
|
#include "theory/strings/theory_strings_utils.h" |
20 |
|
#include "util/rational.h" |
21 |
|
|
22 |
|
using namespace cvc5::context; |
23 |
|
using namespace cvc5::kind; |
24 |
|
|
25 |
|
namespace cvc5 { |
26 |
|
namespace theory { |
27 |
|
namespace strings { |
28 |
|
|
29 |
|
ArraySolver::ArraySolver(Env& env, |
30 |
|
SolverState& s, |
31 |
|
InferenceManager& im, |
32 |
|
TermRegistry& tr, |
33 |
|
CoreSolver& cs, |
34 |
|
ExtfSolver& es, |
35 |
|
ExtTheory& extt) |
36 |
|
: EnvObj(env), |
37 |
|
d_state(s), |
38 |
|
d_im(im), |
39 |
|
d_termReg(tr), |
40 |
|
d_csolver(cs), |
41 |
|
d_esolver(es), |
42 |
|
d_eqProc(context()) |
43 |
|
{ |
44 |
|
NodeManager* nm = NodeManager::currentNM(); |
45 |
|
d_zero = nm->mkConst(Rational(0)); |
46 |
|
} |
47 |
|
|
48 |
|
ArraySolver::~ArraySolver() {} |
49 |
|
|
50 |
|
void ArraySolver::checkArrayConcat() |
51 |
|
{ |
52 |
|
if (!d_termReg.hasSeqUpdate()) |
53 |
|
{ |
54 |
|
Trace("seq-array") << "No seq.update/seq.nth terms, skipping check..." |
55 |
|
<< std::endl; |
56 |
|
return; |
57 |
|
} |
58 |
|
d_currTerms.clear(); |
59 |
|
Trace("seq-array") << "ArraySolver::checkArrayConcat..." << std::endl; |
60 |
|
checkTerms(STRING_UPDATE); |
61 |
|
checkTerms(SEQ_NTH); |
62 |
|
} |
63 |
|
|
64 |
|
void ArraySolver::checkTerms(Kind k) |
65 |
|
{ |
66 |
|
Assert(k == STRING_UPDATE || k == SEQ_NTH); |
67 |
|
NodeManager* nm = NodeManager::currentNM(); |
68 |
|
// get all the active update terms that have not been reduced in the |
69 |
|
// current context by context-dependent simplification |
70 |
|
std::vector<Node> terms = d_esolver.getActive(k); |
71 |
|
for (const Node& t : terms) |
72 |
|
{ |
73 |
|
Trace("seq-array-debug") << "check term " << t << "..." << std::endl; |
74 |
|
Assert(t.getKind() == k); |
75 |
|
if (k == STRING_UPDATE && !d_termReg.isHandledUpdate(t)) |
76 |
|
{ |
77 |
|
// not handled by procedure |
78 |
|
Trace("seq-array-debug") << "...unhandled" << std::endl; |
79 |
|
continue; |
80 |
|
} |
81 |
|
Node r = d_state.getRepresentative(t[0]); |
82 |
|
NormalForm& nf = d_csolver.getNormalForm(r); |
83 |
|
Trace("seq-array-debug") << "...normal form " << nf.d_nf << std::endl; |
84 |
|
if (nf.d_nf.empty()) |
85 |
|
{ |
86 |
|
// updates should have been reduced (UPD_EMPTYSTR) |
87 |
|
Assert(k != STRING_UPDATE); |
88 |
|
Trace("seq-array-debug") << "...empty" << std::endl; |
89 |
|
continue; |
90 |
|
} |
91 |
|
else if (nf.d_nf.size() == 1) |
92 |
|
{ |
93 |
|
Trace("seq-array-debug") << "...norm form size 1" << std::endl; |
94 |
|
// NOTE: could split on n=0 if needed, do not introduce ITE |
95 |
|
if (nf.d_nf[0].getKind() == SEQ_UNIT) |
96 |
|
{ |
97 |
|
// do we know whether n = 0 ? |
98 |
|
// x = (seq.unit m) => (seq.update x n z) = ite(n=0, z, (seq.unit m)) |
99 |
|
// x = (seq.unit m) => (seq.nth x n) = ite(n=0, m, Uf(x, n)) |
100 |
|
Node thenBranch; |
101 |
|
Node elseBranch; |
102 |
|
InferenceId iid; |
103 |
|
if (k == STRING_UPDATE) |
104 |
|
{ |
105 |
|
thenBranch = t[2]; |
106 |
|
elseBranch = nf.d_nf[0]; |
107 |
|
iid = InferenceId::STRINGS_ARRAY_UPDATE_UNIT; |
108 |
|
} |
109 |
|
else |
110 |
|
{ |
111 |
|
Assert(k == SEQ_NTH); |
112 |
|
thenBranch = nf.d_nf[0][0]; |
113 |
|
Node uf = SkolemCache::mkSkolemSeqNth(t[0].getType(), "Uf"); |
114 |
|
elseBranch = nm->mkNode(APPLY_UF, uf, t[0], t[1]); |
115 |
|
iid = InferenceId::STRINGS_ARRAY_NTH_UNIT; |
116 |
|
} |
117 |
|
std::vector<Node> exp; |
118 |
|
d_im.addToExplanation(t[0], nf.d_nf[0], exp); |
119 |
|
d_im.addToExplanation(r, t[0], exp); |
120 |
|
Node eq = nm->mkNode(ITE, |
121 |
|
t[1].eqNode(d_zero), |
122 |
|
t.eqNode(thenBranch), |
123 |
|
t.eqNode(elseBranch)); |
124 |
|
if (d_eqProc.find(eq) == d_eqProc.end()) |
125 |
|
{ |
126 |
|
d_eqProc.insert(eq); |
127 |
|
d_im.sendInference(exp, eq, iid); |
128 |
|
} |
129 |
|
} |
130 |
|
// otherwise, the equivalence class is pure wrt concatenation |
131 |
|
d_currTerms[k].push_back(t); |
132 |
|
continue; |
133 |
|
} |
134 |
|
// otherwise, we are the concatenation of the components |
135 |
|
// NOTE: for nth, split on index vs component lengths, do not introduce ITE |
136 |
|
std::vector<Node> cond; |
137 |
|
std::vector<Node> cchildren; |
138 |
|
std::vector<Node> lacc; |
139 |
|
for (const Node& c : nf.d_nf) |
140 |
|
{ |
141 |
|
Trace("seq-array-debug") << "...process " << c << std::endl; |
142 |
|
Node clen = nm->mkNode(STRING_LENGTH, c); |
143 |
|
Node currIndex = t[1]; |
144 |
|
if (!lacc.empty()) |
145 |
|
{ |
146 |
|
Node currSum = lacc.size() == 1 ? lacc[0] : nm->mkNode(PLUS, lacc); |
147 |
|
currIndex = nm->mkNode(MINUS, currIndex, currSum); |
148 |
|
} |
149 |
|
if (k == STRING_UPDATE) |
150 |
|
{ |
151 |
|
Node cc = nm->mkNode(STRING_UPDATE, c, currIndex, t[2]); |
152 |
|
Trace("seq-array-debug") << "......component " << cc << std::endl; |
153 |
|
cchildren.push_back(cc); |
154 |
|
} |
155 |
|
else |
156 |
|
{ |
157 |
|
Assert(k == SEQ_NTH); |
158 |
|
Node cc = nm->mkNode(SEQ_NTH, c, currIndex); |
159 |
|
Trace("seq-array-debug") << "......component " << cc << std::endl; |
160 |
|
cchildren.push_back(cc); |
161 |
|
} |
162 |
|
lacc.push_back(clen); |
163 |
|
if (k == SEQ_NTH) |
164 |
|
{ |
165 |
|
Node currSumPost = lacc.size() == 1 ? lacc[0] : nm->mkNode(PLUS, lacc); |
166 |
|
Node cc = nm->mkNode(LT, t[1], currSumPost); |
167 |
|
Trace("seq-array-debug") << "......condition " << cc << std::endl; |
168 |
|
cond.push_back(cc); |
169 |
|
} |
170 |
|
} |
171 |
|
// z = (seq.++ x y) => |
172 |
|
// (seq.update z n l) = |
173 |
|
// (seq.++ (seq.update x n 1) (seq.update y (- n len(x)) 1)) |
174 |
|
// z = (seq.++ x y) => |
175 |
|
// (seq.nth z n) = |
176 |
|
// (ite (or (< n 0) (>= n (+ (str.len x) (str.len y)))) (Uf z n) |
177 |
|
// (ite (< n (str.len x)) (seq.nth x n) |
178 |
|
// (seq.nth y (- n (str.len x))))) |
179 |
|
InferenceId iid; |
180 |
|
Node eq; |
181 |
|
if (k == STRING_UPDATE) |
182 |
|
{ |
183 |
|
Node finalc = utils::mkConcat(cchildren, t.getType()); |
184 |
|
eq = t.eqNode(finalc); |
185 |
|
iid = InferenceId::STRINGS_ARRAY_UPDATE_CONCAT; |
186 |
|
} |
187 |
|
else |
188 |
|
{ |
189 |
|
std::reverse(cchildren.begin(), cchildren.end()); |
190 |
|
std::reverse(cond.begin(), cond.end()); |
191 |
|
Node uf = SkolemCache::mkSkolemSeqNth(t[0].getType(), "Uf"); |
192 |
|
eq = t.eqNode(cchildren[0]); |
193 |
|
for (size_t i = 1, ncond = cond.size(); i < ncond; i++) |
194 |
|
{ |
195 |
|
eq = nm->mkNode(ITE, cond[i], t.eqNode(cchildren[i]), eq); |
196 |
|
} |
197 |
|
Node ufa = nm->mkNode(APPLY_UF, uf, t[0], t[1]); |
198 |
|
Node oobCond = |
199 |
|
nm->mkNode(OR, nm->mkNode(LT, t[1], d_zero), cond[0].notNode()); |
200 |
|
eq = nm->mkNode(ITE, oobCond, t.eqNode(ufa), eq); |
201 |
|
iid = InferenceId::STRINGS_ARRAY_NTH_CONCAT; |
202 |
|
} |
203 |
|
std::vector<Node> exp; |
204 |
|
d_im.addToExplanation(r, t[0], exp); |
205 |
|
exp.insert(exp.end(), nf.d_exp.begin(), nf.d_exp.end()); |
206 |
|
exp.push_back(t[0].eqNode(nf.d_base)); |
207 |
|
if (d_eqProc.find(eq) == d_eqProc.end()) |
208 |
|
{ |
209 |
|
d_eqProc.insert(eq); |
210 |
|
Trace("seq-array") << "- send lemma - " << eq << std::endl; |
211 |
|
d_im.sendInference(exp, eq, iid); |
212 |
|
} |
213 |
|
} |
214 |
|
} |
215 |
|
|
216 |
|
} // namespace strings |
217 |
|
} // namespace theory |
218 |
31137 |
} // namespace cvc5 |