1 /********************* */
2 /*! \file theory_strings_preprocess.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Tianyi Liang, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 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.\endverbatim
12 ** \brief Strings Preprocess
14 ** Strings Preprocess.
17 #include "theory/strings/theory_strings_preprocess.h"
21 #include "expr/kind.h"
22 #include "options/strings_options.h"
23 #include "proof/proof_manager.h"
24 #include "smt/logic_exception.h"
31 StringsPreprocess::StringsPreprocess( context::UserContext
* u
) : d_cache( u
){
33 d_zero
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
36 StringsPreprocess::~StringsPreprocess(){
41 int StringsPreprocess::checkFixLenVar( Node t ) {
43 if(t.getKind() == kind::EQUAL) {
44 if(t[0].getType().isInteger() && t[0].isConst() && t[1].getKind() == kind::STRING_LENGTH) {
45 if(t[1][0].getKind() == kind::VARIABLE) {
48 } else if(t[1].getType().isInteger() && t[1].isConst() && t[0].getKind() == kind::STRING_LENGTH) {
49 if(t[0][0].getKind() == kind::VARIABLE) {
55 unsigned len = t[ret].getConst<Rational>().getNumerator().toUnsignedInt();
60 if(!options::stringExp()) {
66 Node
StringsPreprocess::simplify( Node t
, std::vector
< Node
> &new_nodes
) {
67 NodeNodeMap::const_iterator i
= d_cache
.find(t
);
68 if(i
!= d_cache
.end()) {
69 return (*i
).second
.isNull() ? t
: (*i
).second
;
72 Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t
<< std::endl
;
75 /*int c_id = checkFixLenVar(t);
78 int len = t[c_id].getConst<Rational>().getNumerator().toUnsignedInt();
80 Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
81 std::vector< Node > vec;
82 for(int i=0; i<len; i++) {
83 Node num = NodeManager::currentNM()->mkConst( ::CVC4::Rational(i) );
84 //Node sk = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, t[v_id][0], num);
85 Node sk = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, t[v_id][0], num, one);
87 Node cc = one.eqNode(NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ));
88 new_nodes.push_back( cc );
90 Node lem = t[v_id][0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, vec ) );
91 lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, t, lem );
92 new_nodes.push_back( lem );
97 if( t
.getKind() == kind::STRING_SUBSTR
) {
99 Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
100 NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ),
101 NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ) );
102 Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[1], d_zero);
103 Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GT, t[2], d_zero);
104 Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
105 Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for charat/substr" );
106 Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3", NodeManager::currentNM()->stringType(), "created for charat/substr" );
107 Node x_eq_123 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, t, sk3 ) );
108 Node len_sk1_eq_i = t[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
109 Node lenc = t[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t ) );
110 Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond,
111 NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, lenc ),
112 t.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") )) ));
114 Node t12
= NodeManager::currentNM()->mkNode( kind::PLUS
, t
[1], t
[2] );
115 Node lt0
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, t
[0] );
116 //start point is greater than or equal zero
117 Node c1
= NodeManager::currentNM()->mkNode( kind::GEQ
, t
[1], d_zero
);
118 //start point is less than end of string
119 Node c2
= NodeManager::currentNM()->mkNode( kind::GT
, lt0
, t
[1] );
121 Node c3
= NodeManager::currentNM()->mkNode( kind::GT
, t
[2], d_zero
);
122 Node cond
= NodeManager::currentNM()->mkNode( kind::AND
, c1
, c2
, c3
);
124 Node sk1
= NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for substr" );
125 Node sk2
= NodeManager::currentNM()->mkSkolem( "ss2", NodeManager::currentNM()->stringType(), "created for substr" );
126 Node b11
= t
[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, sk1
, t
, sk2
) );
127 //length of first skolem is second argument
128 Node b12
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, sk1
).eqNode( t
[1] );
129 //length of second skolem is abs difference between end point and end of string
130 Node b13
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, sk2
).eqNode(
131 NodeManager::currentNM()->mkNode( kind::ITE
, NodeManager::currentNM()->mkNode( kind::GEQ
, lt0
, t12
),
132 NodeManager::currentNM()->mkNode( kind::MINUS
, lt0
, t12
), d_zero
) );
134 Node b1
= NodeManager::currentNM()->mkNode( kind::AND
, b11
, b12
, b13
);
135 Node b2
= t
.eqNode( NodeManager::currentNM()->mkConst( ::CVC4::String("") ) );
137 Node lemma
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE
, cond
, b1
, b2
) );
138 new_nodes
.push_back( lemma
);
140 } else if( t
.getKind() == kind::STRING_STRIDOF
) {
141 Node sk2
= NodeManager::currentNM()->mkSkolem( "io2", NodeManager::currentNM()->stringType(), "created for indexof" );
142 Node sk3
= NodeManager::currentNM()->mkSkolem( "io3", NodeManager::currentNM()->stringType(), "created for indexof" );
143 Node sk4
= NodeManager::currentNM()->mkSkolem( "io4", NodeManager::currentNM()->stringType(), "created for indexof" );
144 Node skk
= NodeManager::currentNM()->mkSkolem( "iok", NodeManager::currentNM()->integerType(), "created for indexof" );
145 Node st
= NodeManager::currentNM()->mkNode( kind::STRING_SUBSTR
, t
[0], t
[2], NodeManager::currentNM()->mkNode( kind::MINUS
, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, t
[0] ), t
[2] ) );
146 Node eq
= st
.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, sk2
, sk3
, sk4
) );
147 new_nodes
.push_back( eq
);
148 Node negone
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
149 Node krange
= NodeManager::currentNM()->mkNode( kind::GEQ
, skk
, negone
);
150 new_nodes
.push_back( krange
);
151 krange
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT
, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, t
[0] ), skk
) );
152 new_nodes
.push_back( krange
);
153 krange
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT
, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, t
[1] ), d_zero
) );
154 new_nodes
.push_back( krange
);
155 Node start_valid
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GEQ
, t
[2], d_zero
) );
157 //str.len(s1) < y + str.len(s2)
158 Node c1
= Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::GT
,
159 NodeManager::currentNM()->mkNode( kind::PLUS
, t
[2], NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, t
[1] )),
160 NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, t
[0] )));
162 Node c3
= Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::STRING_STRCTN
, st
, t
[1] ).negate());
164 Node left
= NodeManager::currentNM()->mkNode( kind::OR
, c1
, c3
, start_valid
.negate() );
166 Node c4
= t
[1].eqNode( sk3
);
168 Node c5
= NodeManager::currentNM()->mkNode( kind::STRING_STRCTN
,
169 NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, sk2
,
170 NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR
, t
[1], d_zero
,
171 NodeManager::currentNM()->mkNode(kind::MINUS
,
172 NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, t
[1]),
173 NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) )))),
176 Node c6
= skk
.eqNode( NodeManager::currentNM()->mkNode( kind::PLUS
, t
[2],
177 NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, sk2
)) );
179 Node right
= Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::AND
, c4
, c5
, c6
, start_valid
));
180 Node cond
= skk
.eqNode( negone
);
181 Node rr
= NodeManager::currentNM()->mkNode( kind::ITE
, cond
, left
, right
);
182 new_nodes
.push_back( rr
);
183 if( options::stringLazyPreproc() ){
184 new_nodes
.push_back( t
.eqNode( skk
) );
185 d_cache
[t
] = Node::null();
190 } else if( t
.getKind() == kind::STRING_ITOS
|| t
.getKind() == kind::STRING_U16TOS
|| t
.getKind() == kind::STRING_U32TOS
) {
191 //Node num = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE,
192 // NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero),
193 // t[0], NodeManager::currentNM()->mkNode(kind::UMINUS, t[0])));
195 Node pret
= NodeManager::currentNM()->mkNode(kind::STRING_ITOS
, num
);
196 Node lenp
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, pret
);
198 Node nonneg
= NodeManager::currentNM()->mkNode(kind::GEQ
, t
[0], d_zero
);
199 if(t
.getKind()==kind::STRING_U16TOS
) {
200 nonneg
= NodeManager::currentNM()->mkNode(kind::AND
, nonneg
, NodeManager::currentNM()->mkNode(kind::GEQ
, NodeManager::currentNM()->mkConst( ::CVC4::Rational(UINT16_MAX
) ), t
[0]));
201 Node lencond
= NodeManager::currentNM()->mkNode(kind::GEQ
, NodeManager::currentNM()->mkConst( ::CVC4::Rational(5) ), lenp
);
202 new_nodes
.push_back(lencond
);
203 } else if(t
.getKind()==kind::STRING_U32TOS
) {
204 nonneg
= NodeManager::currentNM()->mkNode(kind::AND
, nonneg
, NodeManager::currentNM()->mkNode(kind::GEQ
, NodeManager::currentNM()->mkConst( ::CVC4::Rational(UINT32_MAX
) ), t
[0]));
205 Node lencond
= NodeManager::currentNM()->mkNode(kind::GEQ
, NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) ), lenp
);
206 new_nodes
.push_back(lencond
);
209 Node lem
= NodeManager::currentNM()->mkNode(kind::IFF
, nonneg
.negate(),
210 pret
.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") ))//lenp.eqNode(d_zero)
212 new_nodes
.push_back(lem
);
215 Node b1
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
216 Node b1v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, b1
);
217 Node g1
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND
, NodeManager::currentNM()->mkNode( kind::GEQ
, b1
, d_zero
),
218 NodeManager::currentNM()->mkNode( kind::GT
, lenp
, b1
) ) );
219 Node one
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
220 Node nine
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) );
221 Node ten
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) );
223 std::vector
< TypeNode
> argTypes
;
224 argTypes
.push_back(NodeManager::currentNM()->integerType());
225 Node ufP
= NodeManager::currentNM()->mkSkolem("ufP",
226 NodeManager::currentNM()->mkFunctionType(
227 argTypes
, NodeManager::currentNM()->integerType()),
229 Node ufM
= NodeManager::currentNM()->mkSkolem("ufM",
230 NodeManager::currentNM()->mkFunctionType(
231 argTypes
, NodeManager::currentNM()->integerType()),
234 lem
= num
.eqNode(NodeManager::currentNM()->mkNode(kind::APPLY_UF
, ufP
, d_zero
));
235 new_nodes
.push_back( lem
);
237 Node ufx
= NodeManager::currentNM()->mkNode(kind::APPLY_UF
, ufP
, b1
);
238 Node ufx1
= NodeManager::currentNM()->mkNode(kind::APPLY_UF
, ufP
, NodeManager::currentNM()->mkNode(kind::MINUS
,b1
,one
));
239 Node ufMx
= NodeManager::currentNM()->mkNode(kind::APPLY_UF
, ufM
, b1
);
240 Node b1gtz
= NodeManager::currentNM()->mkNode(kind::GT
, b1
, d_zero
);
241 Node cc1
= ufx1
.eqNode( NodeManager::currentNM()->mkNode(kind::PLUS
,
242 NodeManager::currentNM()->mkNode(kind::MULT
, ufx
, ten
),
243 NodeManager::currentNM()->mkNode(kind::APPLY_UF
, ufM
, NodeManager::currentNM()->mkNode(kind::MINUS
,b1
,one
)) ));
244 cc1
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, b1gtz
, cc1
);
245 Node lstx
= lenp
.eqNode(NodeManager::currentNM()->mkNode(kind::PLUS
, b1
, one
));
246 Node cc2
= ufx
.eqNode(ufMx
);
247 cc2
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, lstx
, cc2
);
249 Node cl
= NodeManager::currentNM()->mkNode(kind::AND
, lstx
, d_zero
.eqNode(b1
).negate());
250 Node cc21
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, cl
, NodeManager::currentNM()->mkNode(kind::GT
, ufMx
, d_zero
));
252 Node cc3
= NodeManager::currentNM()->mkNode(kind::GEQ
, ufMx
, d_zero
);
253 Node cc4
= NodeManager::currentNM()->mkNode(kind::GEQ
, nine
, ufMx
);
255 Node b21
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
256 Node b22
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
257 Node b2v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, b21
, b22
);
259 Node c21
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, b21
).eqNode(
260 NodeManager::currentNM()->mkNode(kind::MINUS
, lenp
, NodeManager::currentNM()->mkNode(kind::PLUS
, b1
, one
) ));
262 NodeManager::currentNM()->mkNode(kind::ITE
, ufMx
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(0))),
263 NodeManager::currentNM()->mkConst(::CVC4::String("0")),
264 NodeManager::currentNM()->mkNode(kind::ITE
, ufMx
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(1))),
265 NodeManager::currentNM()->mkConst(::CVC4::String("1")),
266 NodeManager::currentNM()->mkNode(kind::ITE
, ufMx
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(2))),
267 NodeManager::currentNM()->mkConst(::CVC4::String("2")),
268 NodeManager::currentNM()->mkNode(kind::ITE
, ufMx
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(3))),
269 NodeManager::currentNM()->mkConst(::CVC4::String("3")),
270 NodeManager::currentNM()->mkNode(kind::ITE
, ufMx
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(4))),
271 NodeManager::currentNM()->mkConst(::CVC4::String("4")),
272 NodeManager::currentNM()->mkNode(kind::ITE
, ufMx
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(5))),
273 NodeManager::currentNM()->mkConst(::CVC4::String("5")),
274 NodeManager::currentNM()->mkNode(kind::ITE
, ufMx
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(6))),
275 NodeManager::currentNM()->mkConst(::CVC4::String("6")),
276 NodeManager::currentNM()->mkNode(kind::ITE
, ufMx
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(7))),
277 NodeManager::currentNM()->mkConst(::CVC4::String("7")),
278 NodeManager::currentNM()->mkNode(kind::ITE
, ufMx
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(8))),
279 NodeManager::currentNM()->mkConst(::CVC4::String("8")),
280 NodeManager::currentNM()->mkConst(::CVC4::String("9")))))))))));
281 Node c22
= pret
.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, b21
, ch
, b22
) );
282 Node cc5
= NodeManager::currentNM()->mkNode(kind::EXISTS
, b2v
, NodeManager::currentNM()->mkNode(kind::AND
, c21
, c22
));
283 std::vector
< Node
> svec
;
284 svec
.push_back(cc1
);svec
.push_back(cc2
);
285 svec
.push_back(cc21
);
286 svec
.push_back(cc3
);svec
.push_back(cc4
);svec
.push_back(cc5
);
287 Node conc
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND
, svec
) );
288 conc
= NodeManager::currentNM()->mkNode( kind::IMPLIES
, g1
, conc
);
289 conc
= NodeManager::currentNM()->mkNode( kind::FORALL
, b1v
, conc
);
290 conc
= NodeManager::currentNM()->mkNode( kind::IMPLIES
, nonneg
, conc
);
291 new_nodes
.push_back( conc
);
293 /*conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::IMPLIES,
294 NodeManager::currentNM()->mkNode(kind::LT, t[0], d_zero),
295 t.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT,
296 NodeManager::currentNM()->mkConst(::CVC4::String("-")), pret))));
297 new_nodes.push_back( conc );*/
298 if( options::stringLazyPreproc() && t
!=pret
){
299 new_nodes
.push_back( t
.eqNode( pret
) );
300 d_cache
[t
] = Node::null();
305 //don't rewrite processed
307 d_cache
[pret
] = pret
;
309 } else if( t
.getKind() == kind::STRING_STOI
|| t
.getKind() == kind::STRING_STOU16
|| t
.getKind() == kind::STRING_STOU32
) {
311 Node pret
= NodeManager::currentNM()->mkNode(kind::STRING_STOI
, str
);
312 Node lenp
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, str
);
314 Node negone
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
315 Node one
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
316 Node nine
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) );
317 Node ten
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) );
318 std::vector
< TypeNode
> argTypes
;
319 argTypes
.push_back(NodeManager::currentNM()->integerType());
320 Node ufP
= NodeManager::currentNM()->mkSkolem("ufP",
321 NodeManager::currentNM()->mkFunctionType(
322 argTypes
, NodeManager::currentNM()->integerType()),
324 Node ufM
= NodeManager::currentNM()->mkSkolem("ufM",
325 NodeManager::currentNM()->mkFunctionType(
326 argTypes
, NodeManager::currentNM()->integerType()),
329 //Node ufP0 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero);
330 //new_nodes.push_back(pret.eqNode(ufP0));
332 Node lem
= NodeManager::currentNM()->mkNode(kind::IMPLIES
,
333 str
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(""))),
334 pret
.eqNode(negone
));
335 new_nodes
.push_back(lem
);
336 /*lem = NodeManager::currentNM()->mkNode(kind::IFF,
337 t[0].eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("0"))),
339 new_nodes.push_back(lem);*/
340 if(t
.getKind()==kind::STRING_U16TOS
) {
341 lem
= NodeManager::currentNM()->mkNode(kind::GEQ
, NodeManager::currentNM()->mkConst(::CVC4::String("5")), lenp
);
342 new_nodes
.push_back(lem
);
343 } else if(t
.getKind()==kind::STRING_U32TOS
) {
344 lem
= NodeManager::currentNM()->mkNode(kind::GEQ
, NodeManager::currentNM()->mkConst(::CVC4::String("9")), lenp
);
345 new_nodes
.push_back(lem
);
348 Node cc1
= str
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("")));
349 //cc1 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(negone), cc1);
351 std::vector
< Node
> vec_n
;
352 Node p
= NodeManager::currentNM()->mkSkolem("p", NodeManager::currentNM()->integerType());
353 Node g
= NodeManager::currentNM()->mkNode(kind::GEQ
, p
, d_zero
);
355 g
= NodeManager::currentNM()->mkNode(kind::GT
, lenp
, p
);
357 Node z2
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR
, str
, p
, one
);
360 for(unsigned i
=0; i
<=9; i
++) {
362 std::string
stmp(chtmp
);
363 g
= z2
.eqNode( NodeManager::currentNM()->mkConst(::CVC4::String(stmp
)) ).negate();
366 Node cc2
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND
, vec_n
));
368 Node b2
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
369 Node b2v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, b2
);
370 Node g2
= NodeManager::currentNM()->mkNode(kind::AND
,
371 NodeManager::currentNM()->mkNode(kind::GEQ
, b2
, d_zero
),
372 NodeManager::currentNM()->mkNode(kind::GT
, lenp
, b2
));
373 Node ufx
= NodeManager::currentNM()->mkNode(kind::APPLY_UF
, ufP
, b2
);
374 Node ufx1
= NodeManager::currentNM()->mkNode(kind::APPLY_UF
, ufP
, NodeManager::currentNM()->mkNode(kind::MINUS
,b2
,one
));
375 Node ufMx
= NodeManager::currentNM()->mkNode(kind::APPLY_UF
, ufM
, b2
);
376 std::vector
< Node
> vec_c3
;
377 std::vector
< Node
> vec_c3b
;
379 Node c3cc
= NodeManager::currentNM()->mkNode(kind::GEQ
, ufMx
, d_zero
);
380 vec_c3b
.push_back(c3cc
);
381 c3cc
= NodeManager::currentNM()->mkNode(kind::GEQ
, nine
, ufMx
);
382 vec_c3b
.push_back(c3cc
);
383 Node sx
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR
, str
, b2
, one
);
384 for(unsigned i
=0; i
<=9; i
++) {
386 std::string
stmp(chtmp
);
387 c3cc
= NodeManager::currentNM()->mkNode(kind::IFF
,
388 ufMx
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(i
))),
389 sx
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(stmp
))));
390 vec_c3b
.push_back(c3cc
);
393 Node b2gtz
= NodeManager::currentNM()->mkNode(kind::GT
, b2
, d_zero
);
394 c3cc
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, b2gtz
,
395 ufx
.eqNode(NodeManager::currentNM()->mkNode(kind::PLUS
,
396 NodeManager::currentNM()->mkNode(kind::MULT
, ufx1
, ten
),
398 vec_c3b
.push_back(c3cc
);
399 c3cc
= NodeManager::currentNM()->mkNode(kind::AND
, vec_c3b
);
400 c3cc
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::IMPLIES
, g2
, c3cc
) );
401 c3cc
= NodeManager::currentNM()->mkNode(kind::FORALL
, b2v
, c3cc
);
402 vec_c3
.push_back(c3cc
);
404 c3cc
= NodeManager::currentNM()->mkNode(kind::APPLY_UF
, ufP
, d_zero
).eqNode(NodeManager::currentNM()->mkNode(kind::APPLY_UF
, ufM
, d_zero
));
405 vec_c3
.push_back(c3cc
);
406 Node lstx
= NodeManager::currentNM()->mkNode(kind::MINUS
, lenp
, one
);
407 Node upflstx
= NodeManager::currentNM()->mkNode(kind::APPLY_UF
, ufP
, lstx
);
408 c3cc
= upflstx
.eqNode(pret
);
409 vec_c3
.push_back(c3cc
);
410 Node cc3
= NodeManager::currentNM()->mkNode(kind::AND
, vec_c3
);
411 Node conc
= NodeManager::currentNM()->mkNode(kind::ITE
, pret
.eqNode(negone
),
412 NodeManager::currentNM()->mkNode(kind::OR
, cc1
, cc2
), cc3
);
413 new_nodes
.push_back( conc
);
414 if( options::stringLazyPreproc() && t
!=pret
){
415 new_nodes
.push_back( t
.eqNode( pret
) );
416 d_cache
[t
] = Node::null();
422 d_cache
[pret
] = pret
;
424 } else if( t
.getKind() == kind::STRING_STRREPL
) {
428 Node sk1
= NodeManager::currentNM()->mkSkolem( "rp1", t
[0].getType(), "created for replace" );
429 Node sk2
= NodeManager::currentNM()->mkSkolem( "rp2", t
[0].getType(), "created for replace" );
430 Node skw
= NodeManager::currentNM()->mkSkolem( "rpw", t
[0].getType(), "created for replace" );
431 Node cond
= NodeManager::currentNM()->mkNode( kind::STRING_STRCTN
, x
, y
);
432 Node c1
= x
.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, sk1
, y
, sk2
) );
433 Node c2
= skw
.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, sk1
, z
, sk2
) );
434 Node c3
= NodeManager::currentNM()->mkNode(kind::STRING_STRCTN
,
435 NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, sk1
,
436 NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR
, y
, d_zero
,
437 NodeManager::currentNM()->mkNode(kind::MINUS
,
438 NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, y
),
439 NodeManager::currentNM()->mkConst(::CVC4::Rational(1))))), y
).negate();
440 Node rr
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE
, cond
,
441 NodeManager::currentNM()->mkNode( kind::AND
, c1
, c2
, c3
),
443 new_nodes
.push_back( rr
);
444 rr
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::GT
, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, y
), d_zero
) );
445 new_nodes
.push_back( rr
);
446 if( options::stringLazyPreproc() ){
447 new_nodes
.push_back( t
.eqNode( skw
) );
448 d_cache
[t
] = Node::null();
453 } else if( t
.getKind() == kind::STRING_STRCTN
){
455 d_cache
[t
] = Node::null();
457 d_cache
[t
] = Node::null();
460 /*if( t.getNumChildren()>0 ) {
461 std::vector< Node > cc;
462 if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {
463 cc.push_back(t.getOperator());
465 bool changed = false;
466 for( unsigned i=0; i<t.getNumChildren(); i++ ){
467 Node tn = simplify( t[i], new_nodes );
469 changed = changed || tn!=t[i];
472 Node n = NodeManager::currentNM()->mkNode( t.getKind(), cc );
476 d_cache[t] = Node::null();
481 Trace("strings-preprocess-debug") << "StringsPreprocess::simplify: " << t
<< " -> " << retNode
<< std::endl
;
482 if(!new_nodes
.empty()) {
483 Trace("strings-preprocess-debug") << " ... new nodes (" << new_nodes
.size() << "):\n";
484 for(unsigned int i
=0; i
<new_nodes
.size(); ++i
) {
485 Trace("strings-preprocess-debug") << "\t" << new_nodes
[i
] << "\n";
492 Node
StringsPreprocess::decompose(Node t
, std::vector
< Node
> & new_nodes
) {
493 NodeNodeMap::const_iterator i
= d_cache
.find(t
);
494 if(i
!= d_cache
.end()) {
495 return (*i
).second
.isNull() ? t
: (*i
).second
;
498 unsigned num
= t
.getNumChildren();
500 return simplify(t
, new_nodes
);
502 bool changed
= false;
503 std::vector
< Node
> cc
;
504 if (t
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
505 cc
.push_back(t
.getOperator());
507 for(unsigned i
=0; i
<t
.getNumChildren(); i
++) {
508 Node s
= decompose(t
[i
], new_nodes
);
515 Node tmp
= NodeManager::currentNM()->mkNode( t
.getKind(), cc
);
516 return simplify(tmp
, new_nodes
);
518 return simplify(t
, new_nodes
);
523 void StringsPreprocess::simplify(std::vector
< Node
> &vec_node
) {
524 for( unsigned i
=0; i
<vec_node
.size(); i
++ ){
525 std::vector
< Node
> new_nodes
;
526 Node curr
= decompose( vec_node
[i
], new_nodes
);
527 if( !new_nodes
.empty() ){
528 new_nodes
.insert( new_nodes
.begin(), curr
);
529 curr
= NodeManager::currentNM()->mkNode( kind::AND
, new_nodes
);
531 if( curr
!=vec_node
[i
] ){
532 curr
= Rewriter::rewrite( curr
);
533 PROOF( ProofManager::currentPM()->addDependence(curr
, vec_node
[i
]); );
539 }/* CVC4::theory::strings namespace */
540 }/* CVC4::theory namespace */
541 }/* CVC4 namespace */