a8cbcfac07d2eb64a5b3eb502bab2166b2997f2d
1 /********************* */
2 /*! \file theory_strings_preprocess.cpp
4 ** Original author: Tianyi Liang
5 ** Major contributors: none
6 ** Minor contributors (to current version): Morgan Deters
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Strings Preprocess
14 ** Strings Preprocess.
17 #include "theory/strings/theory_strings_preprocess.h"
18 #include "expr/kind.h"
19 #include "theory/strings/options.h"
20 #include "smt/logic_exception.h"
27 StringsPreprocess::StringsPreprocess() {
29 d_zero
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
32 void StringsPreprocess::processRegExp( Node s
, Node r
, std::vector
< Node
> &ret
) {
35 case kind::REGEXP_EMPTY
: {
36 Node eq
= NodeManager::currentNM()->mkConst( false );
40 case kind::REGEXP_SIGMA
: {
41 Node one
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
42 Node eq
= one
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
));
46 case kind::REGEXP_RANGE
: {
47 Node one
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
48 Node eq
= one
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
));
50 eq
= NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP
, s
, r
);
54 case kind::STRING_TO_REGEXP
: {
55 Node eq
= s
.eqNode( r
[0] );
59 case kind::REGEXP_CONCAT
: {
61 std::vector
< Node
> cc
;
62 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
63 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
64 cc
.push_back( r
[i
][0] );
71 Node eq
= s
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, cc
));
74 Node eq
= NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP
, s
, r
);
79 case kind::REGEXP_UNION
: {
80 std::vector
< Node
> c_or
;
81 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
82 std::vector
< Node
> ntmp
;
83 processRegExp( s
, r
[i
], ntmp
);
84 Node lem
= ntmp
.size()==1 ? ntmp
[0] : NodeManager::currentNM()->mkNode(kind::AND
, ntmp
);
85 c_or
.push_back( lem
);
87 Node eq
= NodeManager::currentNM()->mkNode(kind::OR
, c_or
);
91 case kind::REGEXP_INTER
: {
92 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
93 processRegExp( s
, r
[i
], ret
);
97 case kind::REGEXP_STAR
: {
98 if(r
[0].getKind() == kind::REGEXP_SIGMA
) {
99 ret
.push_back(NodeManager::currentNM()->mkConst(true));
101 Node eq
= NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP
, s
, r
);
106 case kind::REGEXP_LOOP
: {
107 Node eq
= NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP
, s
, r
);
112 Trace("strings-error") << "Unsupported term: " << r
<< " in simplifyRegExp." << std::endl
;
113 Assert( false, "Unsupported Term" );
118 bool StringsPreprocess::checkStarPlus( Node t
) {
119 if( t
.getKind() != kind::REGEXP_STAR
&& t
.getKind() != kind::REGEXP_PLUS
) {
120 for( unsigned i
= 0; i
<t
.getNumChildren(); ++i
) {
121 if( checkStarPlus(t
[i
]) ) return true;
128 int StringsPreprocess::checkFixLenVar( Node t
) {
130 if(t
.getKind() == kind::EQUAL
) {
131 if(t
[0].getType().isInteger() && t
[0].isConst() && t
[1].getKind() == kind::STRING_LENGTH
) {
132 if(t
[1][0].getKind() == kind::VARIABLE
) {
135 } else if(t
[1].getType().isInteger() && t
[1].isConst() && t
[0].getKind() == kind::STRING_LENGTH
) {
136 if(t
[0][0].getKind() == kind::VARIABLE
) {
142 unsigned len
= t
[ret
].getConst
<Rational
>().getNumerator().toUnsignedInt();
147 if(!options::stringExp()) {
152 Node
StringsPreprocess::simplify( Node t
, std::vector
< Node
> &new_nodes
) {
153 std::hash_map
<TNode
, Node
, TNodeHashFunction
>::const_iterator i
= d_cache
.find(t
);
154 if(i
!= d_cache
.end()) {
155 return (*i
).second
.isNull() ? t
: (*i
).second
;
158 Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t
<< std::endl
;
160 /*int c_id = checkFixLenVar(t);
163 int len = t[c_id].getConst<Rational>().getNumerator().toUnsignedInt();
165 Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
166 std::vector< Node > vec;
167 for(int i=0; i<len; i++) {
168 Node num = NodeManager::currentNM()->mkConst( ::CVC4::Rational(i) );
169 //Node sk = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, t[v_id][0], num);
170 Node sk = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, t[v_id][0], num, one);
172 Node cc = one.eqNode(NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ));
173 new_nodes.push_back( cc );
175 Node lem = t[v_id][0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, vec ) );
176 lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, t, lem );
177 new_nodes.push_back( lem );
182 if( t
.getKind() == kind::STRING_IN_REGEXP
) {
183 Node t0
= simplify( t
[0], new_nodes
);
186 std::vector
< Node
> ret
;
187 processRegExp( t0
, t
[1], ret
);
189 Node n
= ret
.size() == 1 ? ret
[0] : NodeManager::currentNM()->mkNode( kind::AND
, ret
);
190 n
= Rewriter::rewrite(n
);
191 d_cache
[t
] = (t
== n
) ? Node::null() : n
;
193 } else if( t
.getKind() == kind::STRING_SUBSTR_TOTAL
) {
194 Node lenxgti
= NodeManager::currentNM()->mkNode( kind::GEQ
,
195 NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, t
[0] ),
196 NodeManager::currentNM()->mkNode( kind::PLUS
, t
[1], t
[2] ) );
197 Node t1geq0
= NodeManager::currentNM()->mkNode(kind::GEQ
, t
[1], d_zero
);
198 Node t2geq0
= NodeManager::currentNM()->mkNode(kind::GEQ
, t
[2], d_zero
);
199 Node cond
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND
, lenxgti
, t1geq0
, t2geq0
));
200 Node sk1
= NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for charat/substr" );
201 Node sk3
= NodeManager::currentNM()->mkSkolem( "ss3", NodeManager::currentNM()->stringType(), "created for charat/substr" );
202 Node x_eq_123
= t
[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, sk1
, t
, sk3
) );
203 Node len_sk1_eq_i
= t
[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, sk1
) );
204 Node lemma
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE
, cond
,
205 NodeManager::currentNM()->mkNode( kind::AND
, x_eq_123
, len_sk1_eq_i
),
206 t
.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") )) ));
207 new_nodes
.push_back( lemma
);
210 } else if( t
.getKind() == kind::STRING_STRIDOF
) {
211 if(options::stringExp()) {
212 Node sk1
= NodeManager::currentNM()->mkSkolem( "io1", NodeManager::currentNM()->stringType(), "created for indexof" );
213 Node sk2
= NodeManager::currentNM()->mkSkolem( "io2", NodeManager::currentNM()->stringType(), "created for indexof" );
214 Node sk3
= NodeManager::currentNM()->mkSkolem( "io3", NodeManager::currentNM()->stringType(), "created for indexof" );
215 Node sk4
= NodeManager::currentNM()->mkSkolem( "io4", NodeManager::currentNM()->stringType(), "created for indexof" );
216 Node skk
= NodeManager::currentNM()->mkSkolem( "iok", NodeManager::currentNM()->integerType(), "created for indexof" );
217 Node eq
= t
[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, sk1
, sk2
, sk3
, sk4
) );
218 new_nodes
.push_back( eq
);
219 Node negone
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
220 Node krange
= NodeManager::currentNM()->mkNode( kind::GEQ
, skk
, negone
);
221 new_nodes
.push_back( krange
);
222 krange
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT
,
223 NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, t
[0] ), skk
) );
224 new_nodes
.push_back( krange
);
225 krange
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT
,
226 NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, t
[1] ), d_zero
) );
227 new_nodes
.push_back( krange
);
228 krange
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GEQ
,
230 new_nodes
.push_back( krange
);
232 //str.len(s1) < y + str.len(s2)
233 Node c1
= Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::GT
,
234 NodeManager::currentNM()->mkNode( kind::PLUS
, t
[2], NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, t
[1] )),
235 NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, t
[0] )));
237 Node c2
= t
[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, sk1
) );
239 Node c3
= Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::STRING_STRCTN
,
240 NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, sk2
, sk3
, sk4
), t
[1] ).negate());
242 Node left
= NodeManager::currentNM()->mkNode( kind::OR
, c1
, NodeManager::currentNM()->mkNode( kind::AND
, c2
, c3
) );
244 Node c4
= t
[1].eqNode( sk3
);
246 Node c5
= NodeManager::currentNM()->mkNode( kind::STRING_STRCTN
,
247 NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, sk2
,
248 NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL
, t
[1], d_zero
,
249 NodeManager::currentNM()->mkNode(kind::MINUS
,
250 NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, t
[1]),
251 NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) )))),
254 Node c6
= skk
.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
,
255 NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, sk1
, sk2
)));
257 Node right
= Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::AND
, c2
, c4
, c5
, c6
));
258 Node cond
= skk
.eqNode( negone
);
259 Node rr
= NodeManager::currentNM()->mkNode( kind::ITE
, cond
, left
, right
);
260 new_nodes
.push_back( rr
);
264 throw LogicException("string indexof not supported in default mode, try --strings-exp");
266 } else if( t
.getKind() == kind::STRING_ITOS
|| t
.getKind() == kind::STRING_U16TOS
|| t
.getKind() == kind::STRING_U32TOS
) {
267 if(options::stringExp()) {
268 //Node num = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE,
269 // NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero),
270 // t[0], NodeManager::currentNM()->mkNode(kind::UMINUS, t[0])));
272 Node pret
= NodeManager::currentNM()->mkNode(kind::STRING_ITOS
, num
);
273 Node lenp
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, pret
);
275 Node nonneg
= NodeManager::currentNM()->mkNode(kind::GEQ
, t
[0], d_zero
);
276 if(t
.getKind()==kind::STRING_U16TOS
) {
277 nonneg
= NodeManager::currentNM()->mkNode(kind::AND
, nonneg
, NodeManager::currentNM()->mkNode(kind::GEQ
, NodeManager::currentNM()->mkConst( ::CVC4::Rational(UINT16_MAX
) ), t
[0]));
278 Node lencond
= NodeManager::currentNM()->mkNode(kind::GEQ
, NodeManager::currentNM()->mkConst( ::CVC4::Rational(5) ), lenp
);
279 new_nodes
.push_back(lencond
);
280 } else if(t
.getKind()==kind::STRING_U32TOS
) {
281 nonneg
= NodeManager::currentNM()->mkNode(kind::AND
, nonneg
, NodeManager::currentNM()->mkNode(kind::GEQ
, NodeManager::currentNM()->mkConst( ::CVC4::Rational(UINT32_MAX
) ), t
[0]));
282 Node lencond
= NodeManager::currentNM()->mkNode(kind::GEQ
, NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) ), lenp
);
283 new_nodes
.push_back(lencond
);
286 Node lem
= NodeManager::currentNM()->mkNode(kind::IFF
, nonneg
.negate(),
287 pret
.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") ))//lenp.eqNode(d_zero)
289 new_nodes
.push_back(lem
);
292 Node b1
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
293 Node b1v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, b1
);
294 Node g1
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND
, NodeManager::currentNM()->mkNode( kind::GEQ
, b1
, d_zero
),
295 NodeManager::currentNM()->mkNode( kind::GT
, lenp
, b1
) ) );
296 Node one
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
297 Node nine
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) );
298 Node ten
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) );
300 std::vector
< TypeNode
> argTypes
;
301 argTypes
.push_back(NodeManager::currentNM()->integerType());
302 Node ufP
= NodeManager::currentNM()->mkSkolem("ufP",
303 NodeManager::currentNM()->mkFunctionType(
304 argTypes
, NodeManager::currentNM()->integerType()),
306 Node ufM
= NodeManager::currentNM()->mkSkolem("ufM",
307 NodeManager::currentNM()->mkFunctionType(
308 argTypes
, NodeManager::currentNM()->integerType()),
311 lem
= num
.eqNode(NodeManager::currentNM()->mkNode(kind::APPLY_UF
, ufP
, d_zero
));
312 new_nodes
.push_back( lem
);
314 Node ufx
= NodeManager::currentNM()->mkNode(kind::APPLY_UF
, ufP
, b1
);
315 Node ufx1
= NodeManager::currentNM()->mkNode(kind::APPLY_UF
, ufP
, NodeManager::currentNM()->mkNode(kind::MINUS
,b1
,one
));
316 Node ufMx
= NodeManager::currentNM()->mkNode(kind::APPLY_UF
, ufM
, b1
);
317 Node b1gtz
= NodeManager::currentNM()->mkNode(kind::GT
, b1
, d_zero
);
318 Node cc1
= ufx1
.eqNode( NodeManager::currentNM()->mkNode(kind::PLUS
,
319 NodeManager::currentNM()->mkNode(kind::MULT
, ufx
, ten
),
320 NodeManager::currentNM()->mkNode(kind::APPLY_UF
, ufM
, NodeManager::currentNM()->mkNode(kind::MINUS
,b1
,one
)) ));
321 cc1
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, b1gtz
, cc1
);
322 Node lstx
= lenp
.eqNode(NodeManager::currentNM()->mkNode(kind::PLUS
, b1
, one
));
323 Node cc2
= ufx
.eqNode(ufMx
);
324 cc2
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, lstx
, cc2
);
326 Node cl
= NodeManager::currentNM()->mkNode(kind::AND
, lstx
, d_zero
.eqNode(b1
).negate());
327 Node cc21
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, cl
, NodeManager::currentNM()->mkNode(kind::GT
, ufMx
, d_zero
));
329 Node cc3
= NodeManager::currentNM()->mkNode(kind::GEQ
, ufMx
, d_zero
);
330 Node cc4
= NodeManager::currentNM()->mkNode(kind::GEQ
, nine
, ufMx
);
332 Node b21
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
333 Node b22
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
334 Node b2v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, b21
, b22
);
336 Node c21
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, b21
).eqNode(
337 NodeManager::currentNM()->mkNode(kind::MINUS
, lenp
, NodeManager::currentNM()->mkNode(kind::PLUS
, b1
, one
) ));
339 NodeManager::currentNM()->mkNode(kind::ITE
, ufMx
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(0))),
340 NodeManager::currentNM()->mkConst(::CVC4::String("0")),
341 NodeManager::currentNM()->mkNode(kind::ITE
, ufMx
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(1))),
342 NodeManager::currentNM()->mkConst(::CVC4::String("1")),
343 NodeManager::currentNM()->mkNode(kind::ITE
, ufMx
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(2))),
344 NodeManager::currentNM()->mkConst(::CVC4::String("2")),
345 NodeManager::currentNM()->mkNode(kind::ITE
, ufMx
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(3))),
346 NodeManager::currentNM()->mkConst(::CVC4::String("3")),
347 NodeManager::currentNM()->mkNode(kind::ITE
, ufMx
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(4))),
348 NodeManager::currentNM()->mkConst(::CVC4::String("4")),
349 NodeManager::currentNM()->mkNode(kind::ITE
, ufMx
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(5))),
350 NodeManager::currentNM()->mkConst(::CVC4::String("5")),
351 NodeManager::currentNM()->mkNode(kind::ITE
, ufMx
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(6))),
352 NodeManager::currentNM()->mkConst(::CVC4::String("6")),
353 NodeManager::currentNM()->mkNode(kind::ITE
, ufMx
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(7))),
354 NodeManager::currentNM()->mkConst(::CVC4::String("7")),
355 NodeManager::currentNM()->mkNode(kind::ITE
, ufMx
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(8))),
356 NodeManager::currentNM()->mkConst(::CVC4::String("8")),
357 NodeManager::currentNM()->mkConst(::CVC4::String("9")))))))))));
358 Node c22
= pret
.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, b21
, ch
, b22
) );
359 Node cc5
= NodeManager::currentNM()->mkNode(kind::EXISTS
, b2v
, NodeManager::currentNM()->mkNode(kind::AND
, c21
, c22
));
360 std::vector
< Node
> svec
;
361 svec
.push_back(cc1
);svec
.push_back(cc2
);
362 svec
.push_back(cc21
);
363 svec
.push_back(cc3
);svec
.push_back(cc4
);svec
.push_back(cc5
);
364 Node conc
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND
, svec
) );
365 conc
= NodeManager::currentNM()->mkNode( kind::IMPLIES
, g1
, conc
);
366 conc
= NodeManager::currentNM()->mkNode( kind::FORALL
, b1v
, conc
);
367 conc
= NodeManager::currentNM()->mkNode( kind::IMPLIES
, nonneg
, conc
);
368 new_nodes
.push_back( conc
);
370 /*conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::IMPLIES,
371 NodeManager::currentNM()->mkNode(kind::LT, t[0], d_zero),
372 t.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT,
373 NodeManager::currentNM()->mkConst(::CVC4::String("-")), pret))));
374 new_nodes.push_back( conc );*/
378 d_cache
[pret
] = pret
;
382 throw LogicException("string int.to.str not supported in default mode, try --strings-exp");
384 } else if( t
.getKind() == kind::STRING_STOI
|| t
.getKind() == kind::STRING_STOU16
|| t
.getKind() == kind::STRING_STOU32
) {
385 if(options::stringExp()) {
387 Node pret
= NodeManager::currentNM()->mkNode(kind::STRING_STOI
, str
);
388 Node lenp
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, str
);
390 Node negone
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
391 Node one
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
392 Node nine
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) );
393 Node ten
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) );
394 std::vector
< TypeNode
> argTypes
;
395 argTypes
.push_back(NodeManager::currentNM()->integerType());
396 Node ufP
= NodeManager::currentNM()->mkSkolem("ufP",
397 NodeManager::currentNM()->mkFunctionType(
398 argTypes
, NodeManager::currentNM()->integerType()),
400 Node ufM
= NodeManager::currentNM()->mkSkolem("ufM",
401 NodeManager::currentNM()->mkFunctionType(
402 argTypes
, NodeManager::currentNM()->integerType()),
405 //Node ufP0 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero);
406 //new_nodes.push_back(pret.eqNode(ufP0));
408 Node lem
= NodeManager::currentNM()->mkNode(kind::IMPLIES
,
409 str
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(""))),
410 pret
.eqNode(negone
));
411 new_nodes
.push_back(lem
);
412 /*lem = NodeManager::currentNM()->mkNode(kind::IFF,
413 t[0].eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("0"))),
415 new_nodes.push_back(lem);*/
416 if(t
.getKind()==kind::STRING_U16TOS
) {
417 lem
= NodeManager::currentNM()->mkNode(kind::GEQ
, NodeManager::currentNM()->mkConst(::CVC4::String("5")), lenp
);
418 new_nodes
.push_back(lem
);
419 } else if(t
.getKind()==kind::STRING_U32TOS
) {
420 lem
= NodeManager::currentNM()->mkNode(kind::GEQ
, NodeManager::currentNM()->mkConst(::CVC4::String("9")), lenp
);
421 new_nodes
.push_back(lem
);
424 Node cc1
= str
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("")));
425 //cc1 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(negone), cc1);
427 std::vector
< Node
> vec_n
;
428 Node p
= NodeManager::currentNM()->mkSkolem("p", NodeManager::currentNM()->integerType());
429 Node g
= NodeManager::currentNM()->mkNode(kind::GEQ
, p
, d_zero
);
431 g
= NodeManager::currentNM()->mkNode(kind::GT
, lenp
, p
);
433 Node z2
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL
, str
, p
, one
);
436 for(unsigned i
=0; i
<=9; i
++) {
438 std::string
stmp(chtmp
);
439 g
= z2
.eqNode( NodeManager::currentNM()->mkConst(::CVC4::String(stmp
)) ).negate();
442 Node cc2
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND
, vec_n
));
444 Node b2
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
445 Node b2v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, b2
);
446 Node g2
= NodeManager::currentNM()->mkNode(kind::AND
,
447 NodeManager::currentNM()->mkNode(kind::GEQ
, b2
, d_zero
),
448 NodeManager::currentNM()->mkNode(kind::GT
, lenp
, b2
));
449 Node ufx
= NodeManager::currentNM()->mkNode(kind::APPLY_UF
, ufP
, b2
);
450 Node ufx1
= NodeManager::currentNM()->mkNode(kind::APPLY_UF
, ufP
, NodeManager::currentNM()->mkNode(kind::MINUS
,b2
,one
));
451 Node ufMx
= NodeManager::currentNM()->mkNode(kind::APPLY_UF
, ufM
, b2
);
452 std::vector
< Node
> vec_c3
;
453 std::vector
< Node
> vec_c3b
;
455 Node c3cc
= NodeManager::currentNM()->mkNode(kind::GEQ
, ufMx
, d_zero
);
456 vec_c3b
.push_back(c3cc
);
457 c3cc
= NodeManager::currentNM()->mkNode(kind::GEQ
, nine
, ufMx
);
458 vec_c3b
.push_back(c3cc
);
459 Node sx
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL
, str
, b2
, one
);
460 for(unsigned i
=0; i
<=9; i
++) {
462 std::string
stmp(chtmp
);
463 c3cc
= NodeManager::currentNM()->mkNode(kind::IFF
,
464 ufMx
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(i
))),
465 sx
.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(stmp
))));
466 vec_c3b
.push_back(c3cc
);
469 Node b2gtz
= NodeManager::currentNM()->mkNode(kind::GT
, b2
, d_zero
);
470 c3cc
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, b2gtz
,
471 ufx
.eqNode(NodeManager::currentNM()->mkNode(kind::PLUS
,
472 NodeManager::currentNM()->mkNode(kind::MULT
, ufx1
, ten
),
474 vec_c3b
.push_back(c3cc
);
475 c3cc
= NodeManager::currentNM()->mkNode(kind::AND
, vec_c3b
);
476 c3cc
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::IMPLIES
, g2
, c3cc
) );
477 c3cc
= NodeManager::currentNM()->mkNode(kind::FORALL
, b2v
, c3cc
);
478 vec_c3
.push_back(c3cc
);
480 c3cc
= NodeManager::currentNM()->mkNode(kind::APPLY_UF
, ufP
, d_zero
).eqNode(NodeManager::currentNM()->mkNode(kind::APPLY_UF
, ufM
, d_zero
));
481 vec_c3
.push_back(c3cc
);
482 Node lstx
= NodeManager::currentNM()->mkNode(kind::MINUS
, lenp
, one
);
483 Node upflstx
= NodeManager::currentNM()->mkNode(kind::APPLY_UF
, ufP
, lstx
);
484 c3cc
= upflstx
.eqNode(pret
);
485 vec_c3
.push_back(c3cc
);
486 Node cc3
= NodeManager::currentNM()->mkNode(kind::AND
, vec_c3
);
487 Node conc
= NodeManager::currentNM()->mkNode(kind::ITE
, pret
.eqNode(negone
),
488 NodeManager::currentNM()->mkNode(kind::OR
, cc1
, cc2
), cc3
);
489 new_nodes
.push_back( conc
);
493 d_cache
[pret
] = pret
;
497 throw LogicException("string int.to.str not supported in default mode, try --strings-exp");
499 } else if( t
.getKind() == kind::STRING_STRREPL
) {
500 if(options::stringExp()) {
504 Node sk1
= NodeManager::currentNM()->mkSkolem( "rp1", t
[0].getType(), "created for replace" );
505 Node sk2
= NodeManager::currentNM()->mkSkolem( "rp2", t
[0].getType(), "created for replace" );
506 Node skw
= NodeManager::currentNM()->mkSkolem( "rpw", t
[0].getType(), "created for replace" );
507 Node cond
= NodeManager::currentNM()->mkNode( kind::STRING_STRCTN
, x
, y
);
508 Node c1
= x
.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, sk1
, y
, sk2
) );
509 Node c2
= skw
.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, sk1
, z
, sk2
) );
510 Node c3
= NodeManager::currentNM()->mkNode(kind::STRING_STRCTN
,
511 NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, sk1
,
512 NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL
, y
, d_zero
,
513 NodeManager::currentNM()->mkNode(kind::MINUS
,
514 NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, y
),
515 NodeManager::currentNM()->mkConst(::CVC4::Rational(1))))), y
).negate();
516 Node rr
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE
, cond
,
517 NodeManager::currentNM()->mkNode( kind::AND
, c1
, c2
, c3
),
519 new_nodes
.push_back( rr
);
520 rr
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::GT
, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, y
), d_zero
) );
521 new_nodes
.push_back( rr
);
526 throw LogicException("string replace not supported in default mode, try --strings-exp");
529 d_cache
[t
] = Node::null();
533 /*if( t.getNumChildren()>0 ) {
534 std::vector< Node > cc;
535 if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {
536 cc.push_back(t.getOperator());
538 bool changed = false;
539 for( unsigned i=0; i<t.getNumChildren(); i++ ){
540 Node tn = simplify( t[i], new_nodes );
542 changed = changed || tn!=t[i];
545 Node n = NodeManager::currentNM()->mkNode( t.getKind(), cc );
549 d_cache[t] = Node::null();
554 Trace("strings-preprocess") << "StringsPreprocess::simplify returns: " << retNode
<< std::endl
;
555 if(!new_nodes
.empty()) {
556 Trace("strings-preprocess") << " ... new nodes (" << new_nodes
.size() << "):\n";
557 for(unsigned int i
=0; i
<new_nodes
.size(); ++i
) {
558 Trace("strings-preprocess") << "\t" << new_nodes
[i
] << "\n";
565 Node
StringsPreprocess::decompose(Node t
, std::vector
< Node
> & new_nodes
) {
566 std::hash_map
<TNode
, Node
, TNodeHashFunction
>::const_iterator i
= d_cache
.find(t
);
567 if(i
!= d_cache
.end()) {
568 return (*i
).second
.isNull() ? t
: (*i
).second
;
571 unsigned num
= t
.getNumChildren();
573 return simplify(t
, new_nodes
);
575 bool changed
= false;
576 std::vector
< Node
> cc
;
577 if (t
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
578 cc
.push_back(t
.getOperator());
580 for(unsigned i
=0; i
<t
.getNumChildren(); i
++) {
581 Node s
= decompose(t
[i
], new_nodes
);
588 Node tmp
= NodeManager::currentNM()->mkNode( t
.getKind(), cc
);
589 return simplify(tmp
, new_nodes
);
591 return simplify(t
, new_nodes
);
596 void StringsPreprocess::simplify(std::vector
< Node
> &vec_node
, std::vector
< Node
> &new_nodes
) {
597 for( unsigned i
=0; i
<vec_node
.size(); i
++ ){
598 vec_node
[i
] = decompose( vec_node
[i
], new_nodes
);
602 void StringsPreprocess::simplify(std::vector
< Node
> &vec_node
) {
603 std::vector
< Node
> new_nodes
;
604 simplify(vec_node
, new_nodes
);
605 vec_node
.insert( vec_node
.end(), new_nodes
.begin(), new_nodes
.end() );
608 }/* CVC4::theory::strings namespace */
609 }/* CVC4::theory namespace */
610 }/* CVC4 namespace */