1 /********************* */
2 /*! \file theory_strings.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Tianyi Liang, Tim King
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 Implementation of the theory of strings.
14 ** Implementation of the theory of strings.
17 #include "theory/strings/theory_strings.h"
21 #include "expr/kind.h"
22 #include "options/strings_options.h"
23 #include "smt/logic_exception.h"
24 #include "smt/smt_statistics_registry.h"
25 #include "smt/command.h"
26 #include "theory/rewriter.h"
27 #include "theory/strings/theory_strings_rewriter.h"
28 #include "theory/strings/type_enumerator.h"
29 #include "theory/theory_model.h"
30 #include "theory/valuation.h"
31 #include "theory/quantifiers/term_database.h"
34 using namespace CVC4::context
;
40 Node
TheoryStrings::TermIndex::add( TNode n
, unsigned index
, TheoryStrings
* t
, Node er
, std::vector
< Node
>& c
) {
41 if( index
==n
.getNumChildren() ){
42 if( d_data
.isNull() ){
47 Assert( index
<n
.getNumChildren() );
48 TNode nir
= t
->getRepresentative( n
[index
] );
49 //if it is empty, and doing CONCAT, ignore
50 if( nir
==er
&& n
.getKind()==kind::STRING_CONCAT
){
51 return add( n
, index
+1, t
, er
, c
);
54 return d_children
[nir
].add( n
, index
+1, t
, er
, c
);
60 TheoryStrings::TheoryStrings(context::Context
* c
, context::UserContext
* u
,
61 OutputChannel
& out
, Valuation valuation
,
62 const LogicInfo
& logicInfo
)
63 : Theory(THEORY_STRINGS
, c
, u
, out
, valuation
, logicInfo
),
66 d_equalityEngine(d_notify
, c
, "theory::strings::TheoryStrings", true),
72 d_length_intro_vars(u
),
73 d_pregistered_terms_cache(u
),
74 d_registered_terms_cache(u
),
77 d_extf_infer_cache(c
),
78 d_extf_infer_cache_u(u
),
79 d_ee_disequalities(c
),
82 d_proxy_var_to_length(u
),
85 d_has_extf(c
, false ),
86 d_skolem_cache_ne_reg(u
),
87 d_regexp_memberships(c
),
94 d_processed_memberships(c
),
98 d_cardinality_lits(u
),
99 d_curr_cardinality(c
, 0)
101 // The kinds we are treating as function application in congruence
102 d_equalityEngine
.addFunctionKind(kind::STRING_IN_REGEXP
);
103 d_equalityEngine
.addFunctionKind(kind::STRING_LENGTH
);
104 d_equalityEngine
.addFunctionKind(kind::STRING_CONCAT
);
105 if( options::stringLazyPreproc() ){
106 d_equalityEngine
.addFunctionKind(kind::STRING_STRCTN
);
107 d_equalityEngine
.addFunctionKind(kind::STRING_SUBSTR
);
108 d_equalityEngine
.addFunctionKind(kind::STRING_ITOS
);
109 d_equalityEngine
.addFunctionKind(kind::STRING_STOI
);
110 d_equalityEngine
.addFunctionKind(kind::STRING_U16TOS
);
111 d_equalityEngine
.addFunctionKind(kind::STRING_STOU16
);
112 d_equalityEngine
.addFunctionKind(kind::STRING_U32TOS
);
113 d_equalityEngine
.addFunctionKind(kind::STRING_STOU32
);
114 d_equalityEngine
.addFunctionKind(kind::STRING_STRIDOF
);
115 d_equalityEngine
.addFunctionKind(kind::STRING_STRREPL
);
118 d_zero
= NodeManager::currentNM()->mkConst( Rational( 0 ) );
119 d_one
= NodeManager::currentNM()->mkConst( Rational( 1 ) );
120 d_emptyString
= NodeManager::currentNM()->mkConst( ::CVC4::String("") );
121 std::vector
< Node
> nvec
;
122 d_emptyRegexp
= NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY
, nvec
);
123 d_true
= NodeManager::currentNM()->mkConst( true );
124 d_false
= NodeManager::currentNM()->mkConst( false );
129 TheoryStrings::~TheoryStrings() {
130 for( std::map
< Node
, EqcInfo
* >::iterator it
= d_eqc_info
.begin(); it
!= d_eqc_info
.end(); ++it
){
135 Node
TheoryStrings::getRepresentative( Node t
) {
136 if( d_equalityEngine
.hasTerm( t
) ){
137 return d_equalityEngine
.getRepresentative( t
);
143 bool TheoryStrings::hasTerm( Node a
){
144 return d_equalityEngine
.hasTerm( a
);
147 bool TheoryStrings::areEqual( Node a
, Node b
){
150 }else if( hasTerm( a
) && hasTerm( b
) ){
151 return d_equalityEngine
.areEqual( a
, b
);
157 bool TheoryStrings::areDisequal( Node a
, Node b
){
161 if( a
.getType().isString() ) {
162 for( unsigned i
=0; i
<2; i
++ ) {
163 Node ac
= a
.getKind()==kind::STRING_CONCAT
? a
[i
==0 ? 0 : a
.getNumChildren()-1] : a
;
164 Node bc
= b
.getKind()==kind::STRING_CONCAT
? b
[i
==0 ? 0 : b
.getNumChildren()-1] : b
;
165 if( ac
.isConst() && bc
.isConst() ){
166 CVC4::String as
= ac
.getConst
<String
>();
167 CVC4::String bs
= bc
.getConst
<String
>();
168 int slen
= as
.size() > bs
.size() ? bs
.size() : as
.size();
169 bool flag
= i
== 1 ? as
.rstrncmp(bs
, slen
): as
.strncmp(bs
, slen
);
176 if( hasTerm( a
) && hasTerm( b
) ) {
177 if( d_equalityEngine
.areDisequal( a
, b
, false ) ){
185 Node
TheoryStrings::getLengthExp( Node t
, std::vector
< Node
>& exp
, Node te
){
186 Assert( areEqual( t
, te
) );
187 Node lt
= mkLength( te
);
189 // use own length if it exists, leads to shorter explanation
192 EqcInfo
* ei
= getOrMakeEqcInfo( t
, false );
193 Node length_term
= ei
? ei
->d_length_term
: Node::null();
194 if( length_term
.isNull() ){
195 //typically shouldnt be necessary
198 Debug("strings") << "TheoryStrings::getLengthTerm " << t
<< " is " << length_term
<< std::endl
;
199 addToExplanation( length_term
, te
, exp
);
200 return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, length_term
) );
204 Node
TheoryStrings::getLength( Node t
, std::vector
< Node
>& exp
) {
205 return getLengthExp( t
, exp
, t
);
208 void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine
* eq
) {
209 d_equalityEngine
.setMasterEqualityEngine(eq
);
212 void TheoryStrings::addSharedTerm(TNode t
) {
213 Debug("strings") << "TheoryStrings::addSharedTerm(): "
214 << t
<< " " << t
.getType().isBoolean() << endl
;
215 d_equalityEngine
.addTriggerTerm(t
, THEORY_STRINGS
);
216 Debug("strings") << "TheoryStrings::addSharedTerm() finished" << std::endl
;
219 EqualityStatus
TheoryStrings::getEqualityStatus(TNode a
, TNode b
) {
220 if( d_equalityEngine
.hasTerm(a
) && d_equalityEngine
.hasTerm(b
) ){
221 if (d_equalityEngine
.areEqual(a
, b
)) {
222 // The terms are implied to be equal
223 return EQUALITY_TRUE
;
225 if (d_equalityEngine
.areDisequal(a
, b
, false)) {
226 // The terms are implied to be dis-equal
227 return EQUALITY_FALSE
;
230 return EQUALITY_UNKNOWN
;
233 void TheoryStrings::propagate(Effort e
) {
234 // direct propagation now
237 bool TheoryStrings::propagate(TNode literal
) {
238 Debug("strings-propagate") << "TheoryStrings::propagate(" << literal
<< ")" << std::endl
;
239 // If already in conflict, no more propagation
241 Debug("strings-propagate") << "TheoryStrings::propagate(" << literal
<< "): already in conflict" << std::endl
;
245 bool ok
= d_out
->propagate(literal
);
253 void TheoryStrings::explain(TNode literal
, std::vector
<TNode
>& assumptions
) {
254 Debug("strings-explain") << "Explain " << literal
<< " " << d_conflict
<< std::endl
;
255 bool polarity
= literal
.getKind() != kind::NOT
;
256 TNode atom
= polarity
? literal
: literal
[0];
257 unsigned ps
= assumptions
.size();
258 std::vector
< TNode
> tassumptions
;
259 if (atom
.getKind() == kind::EQUAL
|| atom
.getKind() == kind::IFF
) {
260 if( atom
[0]!=atom
[1] ){
261 d_equalityEngine
.explainEquality(atom
[0], atom
[1], polarity
, tassumptions
);
264 d_equalityEngine
.explainPredicate(atom
, polarity
, tassumptions
);
266 for( unsigned i
=0; i
<tassumptions
.size(); i
++ ){
267 if( std::find( assumptions
.begin(), assumptions
.end(), tassumptions
[i
] )==assumptions
.end() ){
268 assumptions
.push_back( tassumptions
[i
] );
271 Debug("strings-explain-debug") << "Explanation for " << literal
<< " was " << std::endl
;
272 for( unsigned i
=ps
; i
<assumptions
.size(); i
++ ){
273 Debug("strings-explain-debug") << " " << assumptions
[i
] << std::endl
;
277 Node
TheoryStrings::explain( TNode literal
){
278 std::vector
< TNode
> assumptions
;
279 explain( literal
, assumptions
);
280 if( assumptions
.empty() ){
282 }else if( assumptions
.size()==1 ){
283 return assumptions
[0];
285 return NodeManager::currentNM()->mkNode( kind::AND
, assumptions
);
289 /////////////////////////////////////////////////////////////////////////////
291 /////////////////////////////////////////////////////////////////////////////
294 void TheoryStrings::presolve() {
295 Debug("strings-presolve") << "TheoryStrings::Presolving : get fmf options " << (options::stringFMF() ? "true" : "false") << std::endl
;
297 if(!options::stdASCII()) {
303 /////////////////////////////////////////////////////////////////////////////
305 /////////////////////////////////////////////////////////////////////////////
308 void TheoryStrings::collectModelInfo( TheoryModel
* m
, bool fullModel
) {
309 Trace("strings-model") << "TheoryStrings : Collect model info, fullModel = " << fullModel
<< std::endl
;
310 Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl
;
311 m
->assertEqualityEngine( &d_equalityEngine
);
313 std::vector
< Node
> nodes
;
314 getEquivalenceClasses( nodes
);
315 std::map
< Node
, Node
> processed
;
316 std::vector
< std::vector
< Node
> > col
;
317 std::vector
< Node
> lts
;
318 separateByLength( nodes
, col
, lts
);
319 //step 1 : get all values for known lengths
320 std::vector
< Node
> lts_values
;
321 std::map
< unsigned, bool > values_used
;
322 for( unsigned i
=0; i
<col
.size(); i
++ ) {
323 Trace("strings-model") << "Checking length for {";
324 for( unsigned j
=0; j
<col
[i
].size(); j
++ ) {
326 Trace("strings-model") << ", ";
328 Trace("strings-model") << col
[i
][j
];
330 Trace("strings-model") << " } (length is " << lts
[i
] << ")" << std::endl
;
331 if( lts
[i
].isConst() ) {
332 lts_values
.push_back( lts
[i
] );
333 Assert(lts
[i
].getConst
<Rational
>() <= RMAXINT
, "Exceeded LONG_MAX in string model");
334 unsigned lvalue
= lts
[i
].getConst
<Rational
>().getNumerator().toUnsignedInt();
335 values_used
[ lvalue
] = true;
337 //get value for lts[i];
338 if( !lts
[i
].isNull() ){
339 Node v
= d_valuation
.getModelValue(lts
[i
]);
340 Trace("strings-model") << "Model value for " << lts
[i
] << " is " << v
<< std::endl
;
341 lts_values
.push_back( v
);
342 Assert(v
.getConst
<Rational
>() <= RMAXINT
, "Exceeded LONG_MAX in string model");
343 unsigned lvalue
= v
.getConst
<Rational
>().getNumerator().toUnsignedInt();
344 values_used
[ lvalue
] = true;
346 //Trace("strings-model-warn") << "No length for eqc " << col[i][0] << std::endl;
348 lts_values
.push_back( Node::null() );
352 ////step 2 : assign arbitrary values for unknown lengths?
353 // confirmed by calculus invariant, see paper
354 Trace("strings-model") << "Assign to equivalence classes..." << std::endl
;
355 //step 3 : assign values to equivalence classes that are pure variables
356 for( unsigned i
=0; i
<col
.size(); i
++ ){
357 std::vector
< Node
> pure_eq
;
358 Trace("strings-model") << "The equivalence classes ";
359 for( unsigned j
=0; j
<col
[i
].size(); j
++ ) {
360 Trace("strings-model") << col
[i
][j
] << " ";
361 //check if col[i][j] has only variables
362 EqcInfo
* ei
= getOrMakeEqcInfo( col
[i
][j
], false );
363 Node cst
= ei
? ei
->d_const_term
: Node::null();
365 Assert( d_normal_forms
.find( col
[i
][j
] )!=d_normal_forms
.end() );
366 if( d_normal_forms
[col
[i
][j
]].size()==1 ){//&& d_normal_forms[col[i][j]][0]==col[i][j] ){
367 pure_eq
.push_back( col
[i
][j
] );
370 processed
[col
[i
][j
]] = cst
;
373 Trace("strings-model") << "have length " << lts_values
[i
] << std::endl
;
375 //assign a new length if necessary
376 if( !pure_eq
.empty() ){
377 if( lts_values
[i
].isNull() ){
379 while( values_used
.find( lvalue
)!=values_used
.end() ){
382 Trace("strings-model") << "*** Decide to make length of " << lvalue
<< std::endl
;
383 lts_values
[i
] = NodeManager::currentNM()->mkConst( Rational( lvalue
) );
384 values_used
[ lvalue
] = true;
386 Trace("strings-model") << "Need to assign values of length " << lts_values
[i
] << " to equivalence classes ";
387 for( unsigned j
=0; j
<pure_eq
.size(); j
++ ){
388 Trace("strings-model") << pure_eq
[j
] << " ";
390 Trace("strings-model") << std::endl
;
393 //use type enumerator
394 Assert(lts_values
[i
].getConst
<Rational
>() <= RMAXINT
, "Exceeded LONG_MAX in string model");
395 StringEnumeratorLength
sel(lts_values
[i
].getConst
<Rational
>().getNumerator().toUnsignedInt());
396 for( unsigned j
=0; j
<pure_eq
.size(); j
++ ){
397 Assert( !sel
.isFinished() );
399 while( d_equalityEngine
.hasTerm( c
) ){
401 Assert( !sel
.isFinished() );
405 Trace("strings-model") << "*** Assigned constant " << c
<< " for " << pure_eq
[j
] << std::endl
;
406 processed
[pure_eq
[j
]] = c
;
407 m
->assertEquality( pure_eq
[j
], c
, true );
411 Trace("strings-model") << "String Model : Pure Assigned." << std::endl
;
412 //step 4 : assign constants to all other equivalence classes
413 for( unsigned i
=0; i
<nodes
.size(); i
++ ){
414 if( processed
.find( nodes
[i
] )==processed
.end() ){
415 Assert( d_normal_forms
.find( nodes
[i
] )!=d_normal_forms
.end() );
416 Trace("strings-model") << "Construct model for " << nodes
[i
] << " based on normal form ";
417 for( unsigned j
=0; j
<d_normal_forms
[nodes
[i
]].size(); j
++ ) {
418 if( j
>0 ) Trace("strings-model") << " ++ ";
419 Trace("strings-model") << d_normal_forms
[nodes
[i
]][j
];
420 Node r
= getRepresentative( d_normal_forms
[nodes
[i
]][j
] );
421 if( !r
.isConst() && processed
.find( r
)==processed
.end() ){
422 Trace("strings-model") << "(UNPROCESSED)";
425 Trace("strings-model") << std::endl
;
426 std::vector
< Node
> nc
;
427 for( unsigned j
=0; j
<d_normal_forms
[nodes
[i
]].size(); j
++ ) {
428 Node r
= getRepresentative( d_normal_forms
[nodes
[i
]][j
] );
429 Assert( r
.isConst() || processed
.find( r
)!=processed
.end() );
430 nc
.push_back(r
.isConst() ? r
: processed
[r
]);
432 Node cc
= mkConcat( nc
);
433 Assert( cc
.getKind()==kind::CONST_STRING
);
434 Trace("strings-model") << "*** Determined constant " << cc
<< " for " << nodes
[i
] << std::endl
;
435 processed
[nodes
[i
]] = cc
;
436 m
->assertEquality( nodes
[i
], cc
, true );
439 //Trace("strings-model") << "String Model : Assigned." << std::endl;
440 Trace("strings-model") << "String Model : Finished." << std::endl
;
443 /////////////////////////////////////////////////////////////////////////////
445 /////////////////////////////////////////////////////////////////////////////
448 void TheoryStrings::preRegisterTerm(TNode n
) {
449 if( d_pregistered_terms_cache
.find(n
) == d_pregistered_terms_cache
.end() ) {
450 d_pregistered_terms_cache
.insert(n
);
451 //check for logic exceptions
452 if( !options::stringExp() ){
453 if( n
.getKind()==kind::STRING_STRIDOF
||
454 n
.getKind() == kind::STRING_ITOS
|| n
.getKind() == kind::STRING_U16TOS
|| n
.getKind() == kind::STRING_U32TOS
||
455 n
.getKind() == kind::STRING_STOI
|| n
.getKind() == kind::STRING_STOU16
|| n
.getKind() == kind::STRING_STOU32
||
456 n
.getKind() == kind::STRING_STRREPL
|| n
.getKind() == kind::STRING_STRCTN
){
457 std::stringstream ss
;
458 ss
<< "Term of kind " << n
.getKind() << " not supported in default mode, try --strings-exp";
459 throw LogicException(ss
.str());
462 switch( n
.getKind() ) {
464 d_equalityEngine
.addTriggerEquality(n
);
467 case kind::STRING_IN_REGEXP
: {
468 d_out
->requirePhase(n
, true);
469 d_equalityEngine
.addTriggerPredicate(n
);
470 d_equalityEngine
.addTerm(n
[0]);
471 d_equalityEngine
.addTerm(n
[1]);
475 TypeNode tn
= n
.getType();
476 if( tn
.isString() ) {
477 registerTerm( n
, 0 );
479 if( n
.getKind() == kind::VARIABLE
&& options::stringFMF() ){
480 d_input_vars
.insert(n
);
482 d_equalityEngine
.addTerm(n
);
483 } else if (tn
.isBoolean()) {
484 // Get triggered for both equal and dis-equal
485 d_equalityEngine
.addTriggerPredicate(n
);
487 // Function applications/predicates
488 d_equalityEngine
.addTerm(n
);
489 if( options::stringExp() ){
490 //collect extended functions here: some may not be asserted to strings (such as those with return type Int),
491 // but we need to record them so they are treated properly
492 std::map
< Node
, bool > visited
;
493 collectExtendedFuncTerms( n
, visited
);
496 //concat terms do not contribute to theory combination? TODO: verify
497 if( n
.hasOperator() && kindToTheoryId( n
.getKind() )==THEORY_STRINGS
&& n
.getKind()!=kind::STRING_CONCAT
){
498 d_functionsTerms
.push_back( n
);
505 Node
TheoryStrings::expandDefinition(LogicRequest
&logicRequest
, Node node
) {
506 Trace("strings-exp-def") << "TheoryStrings::expandDefinition : " << node
<< std::endl
;
511 void TheoryStrings::check(Effort e
) {
512 if (done() && e
<EFFORT_FULL
) {
516 TimerStat::CodeTimer
checkTimer(d_checkTime
);
521 /*if(getLogicInfo().hasEverything()) {
522 WarningOnce() << "WARNING: strings not supported in default configuration (ALL_SUPPORTED).\n"
523 << "To suppress this warning in the future use proper logic symbol, e.g. (set-logic QF_S)." << std::endl;
527 if( !done() && !hasTerm( d_emptyString
) ) {
528 preRegisterTerm( d_emptyString
);
531 // Trace("strings-process") << "Theory of strings, check : " << e << std::endl;
532 Trace("strings-check") << "Theory of strings, check : " << e
<< std::endl
;
533 while ( !done() && !d_conflict
) {
534 // Get all the assertions
535 Assertion assertion
= get();
536 TNode fact
= assertion
.assertion
;
538 Trace("strings-assertion") << "get assertion: " << fact
<< endl
;
539 polarity
= fact
.getKind() != kind::NOT
;
540 atom
= polarity
? fact
: fact
[0];
542 //assert pending fact
543 assertPendingFact( atom
, polarity
, fact
);
547 if( !d_conflict
&& ( ( e
== EFFORT_FULL
&& !d_valuation
.needCheck() ) || ( e
==EFFORT_STANDARD
&& options::stringEager() ) ) ) {
548 Trace("strings-check") << "Theory of strings full effort check " << std::endl
;
550 if(Trace
.isOn("strings-eqc")) {
551 for( unsigned t
=0; t
<2; t
++ ) {
552 eq::EqClassesIterator eqcs2_i
= eq::EqClassesIterator( &d_equalityEngine
);
553 Trace("strings-eqc") << (t
==0 ? "STRINGS:" : "OTHER:") << std::endl
;
554 while( !eqcs2_i
.isFinished() ){
555 Node eqc
= (*eqcs2_i
);
556 bool print
= (t
==0 && eqc
.getType().isString() ) || (t
==1 && !eqc
.getType().isString() );
558 eq::EqClassIterator eqc2_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
559 Trace("strings-eqc") << "Eqc( " << eqc
<< " ) : { ";
560 while( !eqc2_i
.isFinished() ) {
561 if( (*eqc2_i
)!=eqc
&& (*eqc2_i
).getKind()!=kind::EQUAL
){
562 Trace("strings-eqc") << (*eqc2_i
) << " ";
566 Trace("strings-eqc") << " } " << std::endl
;
567 EqcInfo
* ei
= getOrMakeEqcInfo( eqc
, false );
569 Trace("strings-eqc-debug") << "* Length term : " << ei
->d_length_term
.get() << std::endl
;
570 Trace("strings-eqc-debug") << "* Cardinality lemma k : " << ei
->d_cardinality_lem_k
.get() << std::endl
;
571 Trace("strings-eqc-debug") << "* Normalization length lemma : " << ei
->d_normalized_length
.get() << std::endl
;
576 Trace("strings-eqc") << std::endl
;
578 Trace("strings-eqc") << std::endl
;
581 bool addedLemma
= false;
584 Trace("strings-process") << "----check, next round---" << std::endl
;
586 Trace("strings-process") << "Done check init, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
587 if( !hasProcessed() ){
589 Trace("strings-process") << "Done check extended functions eval, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
590 if( !hasProcessed() ){
592 Trace("strings-process") << "Done check flat forms, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
593 if( !hasProcessed() && e
==EFFORT_FULL
){
595 Trace("strings-process") << "Done check normal forms, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
596 if( !hasProcessed() ){
597 if( options::stringEagerLen() ){
599 Trace("strings-process") << "Done check lengths, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
601 if( !hasProcessed() ){
602 if( options::stringExp() && !options::stringGuessModel() ){
603 checkExtfReductions( 2 );
604 Trace("strings-process") << "Done check extended functions reduction 2, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
606 if( !hasProcessed() ){
608 Trace("strings-process") << "Done check memberships, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
609 if( !hasProcessed() ){
611 Trace("strings-process") << "Done check cardinality, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
620 addedFact
= !d_pending
.empty();
621 addedLemma
= !d_lemma_cache
.empty();
624 }while( !d_conflict
&& !addedLemma
&& addedFact
);
626 Trace("strings-check") << "Theory of strings done full effort check " << addedLemma
<< " " << d_conflict
<< std::endl
;
627 }else if( e
==EFFORT_LAST_CALL
){
628 Assert( !hasProcessed() );
629 Trace("strings-check") << "Theory of strings last call effort check " << std::endl
;
631 checkExtfReductions( 2 );
634 Trace("strings-process") << "Done check extended functions reduction 2, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
636 Trace("strings-check") << "Theory of strings, done check : " << e
<< std::endl
;
637 Assert( d_pending
.empty() );
638 Assert( d_lemma_cache
.empty() );
641 bool TheoryStrings::needsCheckLastEffort() {
642 if( options::stringGuessModel() ){
643 return d_has_extf
.get();
649 void TheoryStrings::checkExtfReductions( int effort
) {
650 Trace("strings-process-debug") << "Checking preprocess at effort " << effort
<< ", #to process=" << d_ext_func_terms
.size() << "..." << std::endl
;
651 for( NodeBoolMap::iterator it
= d_ext_func_terms
.begin(); it
!= d_ext_func_terms
.end(); ++it
){
652 Node n
= (*it
).first
;
653 Trace("strings-process-debug2") << n
<< ", active=" << (*it
).second
<< ", model active=" << d_extf_info_tmp
[n
].d_model_active
<< std::endl
;
654 if( (*it
).second
&& d_extf_info_tmp
[n
].d_model_active
){
655 Assert( d_extf_info_tmp
.find( n
)!=d_extf_info_tmp
.end() );
656 checkExtfReduction( n
, d_extf_info_tmp
[n
].d_pol
, effort
);
657 if( hasProcessed() ){
664 void TheoryStrings::checkExtfReduction( Node atom
, int pol
, int effort
) {
665 //determine the effort level to process the extf at
666 // 0 - at assertion time, 1+ - after no other reduction is applicable
668 if( atom
.getKind()==kind::STRING_STRCTN
){
676 std::vector
< Node
> lexp
;
677 Node lenx
= getLength( x
, lexp
);
678 Node lens
= getLength( s
, lexp
);
679 if( areEqual( lenx
, lens
) ){
680 Trace("strings-extf-debug") << " resolve extf : " << atom
<< " based on equal lengths disequality." << std::endl
;
681 d_ext_func_terms
[atom
] = false;
682 //we can reduce to disequality when lengths are equal
683 if( !areDisequal( x
, s
) ){
684 lexp
.push_back( lenx
.eqNode(lens
) );
685 lexp
.push_back( atom
.negate() );
686 Node xneqs
= x
.eqNode(s
).negate();
687 sendInference( lexp
, xneqs
, "NEG-CTN-EQL", true );
689 }else if( !areDisequal( lenx
, lens
) ){
690 //split on their lenths
691 lenx
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, x
);
692 lens
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, s
);
693 sendSplit( lenx
, lens
, "NEG-CTN-SP" );
700 if( options::stringLazyPreproc() ){
701 if( atom
.getKind()==kind::STRING_SUBSTR
){
703 }else if( atom
.getKind()!=kind::STRING_IN_REGEXP
){
708 if( effort
==r_effort
){
709 Node c_atom
= pol
==-1 ? atom
.negate() : atom
;
710 if( d_preproc_cache
.find( c_atom
)==d_preproc_cache
.end() ){
711 d_preproc_cache
[ c_atom
] = true;
712 Trace("strings-process-debug") << "Process reduction for " << atom
<< ", pol = " << pol
<< std::endl
;
713 if( atom
.getKind()==kind::STRING_STRCTN
&& pol
==1 ){
716 //positive contains reduces to a equality
717 Node sk1
= mkSkolemCached( x
, s
, sk_id_ctn_pre
, "sc1" );
718 Node sk2
= mkSkolemCached( x
, s
, sk_id_ctn_post
, "sc2" );
719 Node eq
= Rewriter::rewrite( x
.eqNode( mkConcat( sk1
, s
, sk2
) ) );
720 std::vector
< Node
> exp_vec
;
721 exp_vec
.push_back( atom
);
722 sendInference( d_empty_vec
, exp_vec
, eq
, "POS-CTN", true );
723 //we've reduced this atom
724 d_ext_func_terms
[ atom
] = false;
725 Trace("strings-extf-debug") << " resolve extf : " << atom
<< " based on positive contain reduction." << std::endl
;
727 // for STRING_SUBSTR, STRING_STRCTN with pol=-1,
728 // STRING_STRIDOF, STRING_ITOS, STRING_U16TOS, STRING_U32TOS, STRING_STOI, STRING_STOU16, STRING_STOU32, STRING_STRREPL
729 std::vector
< Node
> new_nodes
;
730 Node res
= d_preproc
.simplify( atom
, new_nodes
);
732 new_nodes
.push_back( NodeManager::currentNM()->mkNode( res
.getType().isBoolean() ? kind::IFF
: kind::EQUAL
, res
, atom
) );
733 Node nnlem
= new_nodes
.size()==1 ? new_nodes
[0] : NodeManager::currentNM()->mkNode( kind::AND
, new_nodes
);
734 nnlem
= Rewriter::rewrite( nnlem
);
735 Trace("strings-red-lemma") << "Reduction_" << effort
<< " lemma : " << nnlem
<< std::endl
;
736 Trace("strings-red-lemma") << "...from " << atom
<< std::endl
;
737 sendInference( d_empty_vec
, nnlem
, "Reduction", true );
738 //we've reduced this atom
739 d_ext_func_terms
[ atom
] = false;
740 Trace("strings-extf-debug") << " resolve extf : " << atom
<< " based on reduction." << std::endl
;
746 TheoryStrings::EqcInfo::EqcInfo( context::Context
* c
) : d_const_term(c
), d_length_term(c
), d_cardinality_lem_k(c
), d_normalized_length(c
) {
750 TheoryStrings::EqcInfo
* TheoryStrings::getOrMakeEqcInfo( Node eqc
, bool doMake
) {
751 std::map
< Node
, EqcInfo
* >::iterator eqc_i
= d_eqc_info
.find( eqc
);
752 if( eqc_i
==d_eqc_info
.end() ){
754 EqcInfo
* ei
= new EqcInfo( getSatContext() );
755 d_eqc_info
[eqc
] = ei
;
761 return (*eqc_i
).second
;
766 /** Conflict when merging two constants */
767 void TheoryStrings::conflict(TNode a
, TNode b
){
769 Debug("strings-conflict") << "Making conflict..." << std::endl
;
772 if (a
.getKind() == kind::CONST_BOOLEAN
) {
773 conflictNode
= explain( a
.iffNode(b
) );
775 conflictNode
= explain( a
.eqNode(b
) );
777 Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode
<< std::endl
;
778 d_out
->conflict( conflictNode
);
782 /** called when a new equivalance class is created */
783 void TheoryStrings::eqNotifyNewClass(TNode t
){
784 if( t
.getKind() == kind::CONST_STRING
){
785 EqcInfo
* ei
=getOrMakeEqcInfo( t
, true );
786 ei
->d_const_term
= t
;
788 if( t
.getKind() == kind::STRING_LENGTH
){
789 Trace("strings-debug") << "New length eqc : " << t
<< std::endl
;
790 Node r
= d_equalityEngine
.getRepresentative(t
[0]);
791 EqcInfo
* ei
= getOrMakeEqcInfo( r
, true );
792 ei
->d_length_term
= t
[0];
793 //we care about the length of this string
794 registerTerm( t
[0], 1 );
798 /** called when two equivalance classes will merge */
799 void TheoryStrings::eqNotifyPreMerge(TNode t1
, TNode t2
){
800 EqcInfo
* e2
= getOrMakeEqcInfo(t2
, false);
802 EqcInfo
* e1
= getOrMakeEqcInfo( t1
);
803 //add information from e2 to e1
804 if( !e2
->d_const_term
.get().isNull() ){
805 e1
->d_const_term
.set( e2
->d_const_term
);
807 if( !e2
->d_length_term
.get().isNull() ){
808 e1
->d_length_term
.set( e2
->d_length_term
);
810 if( e2
->d_cardinality_lem_k
.get()>e1
->d_cardinality_lem_k
.get() ) {
811 e1
->d_cardinality_lem_k
.set( e2
->d_cardinality_lem_k
);
813 if( !e2
->d_normalized_length
.get().isNull() ){
814 e1
->d_normalized_length
.set( e2
->d_normalized_length
);
819 /** called when two equivalance classes have merged */
820 void TheoryStrings::eqNotifyPostMerge(TNode t1
, TNode t2
) {
824 /** called when two equivalance classes are disequal */
825 void TheoryStrings::eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
) {
826 if( t1
.getType().isString() ){
827 //store disequalities between strings, may need to check if their lengths are equal/disequal
828 d_ee_disequalities
.push_back( t1
.eqNode( t2
) );
832 void TheoryStrings::addCarePairs( quantifiers::TermArgTrie
* t1
, quantifiers::TermArgTrie
* t2
, unsigned arity
, unsigned depth
) {
835 Node f1
= t1
->getNodeData();
836 Node f2
= t2
->getNodeData();
837 if( !d_equalityEngine
.areEqual( f1
, f2
) ){
838 Trace("strings-cg-debug") << "TheoryStrings::computeCareGraph(): checking function " << f1
<< " and " << f2
<< std::endl
;
839 vector
< pair
<TNode
, TNode
> > currentPairs
;
840 for (unsigned k
= 0; k
< f1
.getNumChildren(); ++ k
) {
843 Assert( d_equalityEngine
.hasTerm(x
) );
844 Assert( d_equalityEngine
.hasTerm(y
) );
845 Assert( !d_equalityEngine
.areDisequal( x
, y
, false ) );
846 if( !d_equalityEngine
.areEqual( x
, y
) ){
847 if( d_equalityEngine
.isTriggerTerm(x
, THEORY_STRINGS
) && d_equalityEngine
.isTriggerTerm(y
, THEORY_STRINGS
) ){
848 TNode x_shared
= d_equalityEngine
.getTriggerTermRepresentative(x
, THEORY_STRINGS
);
849 TNode y_shared
= d_equalityEngine
.getTriggerTermRepresentative(y
, THEORY_STRINGS
);
850 EqualityStatus eqStatus
= d_valuation
.getEqualityStatus(x_shared
, y_shared
);
851 if( eqStatus
==EQUALITY_FALSE_AND_PROPAGATED
|| eqStatus
==EQUALITY_FALSE
|| eqStatus
==EQUALITY_FALSE_IN_MODEL
){
852 //an argument is disequal, we are done
855 currentPairs
.push_back(make_pair(x_shared
, y_shared
));
860 for (unsigned c
= 0; c
< currentPairs
.size(); ++ c
) {
861 Trace("strings-cg-pair") << "TheoryStrings::computeCareGraph(): pair : " << currentPairs
[c
].first
<< " " << currentPairs
[c
].second
<< std::endl
;
862 Trace("ajr-temp") << currentPairs
[c
].first
<< ", " << currentPairs
[c
].second
<< std::endl
;
863 addCarePair(currentPairs
[c
].first
, currentPairs
[c
].second
);
869 if( depth
<(arity
-1) ){
870 //add care pairs internal to each child
871 for( std::map
< TNode
, quantifiers::TermArgTrie
>::iterator it
= t1
->d_data
.begin(); it
!= t1
->d_data
.end(); ++it
){
872 addCarePairs( &it
->second
, NULL
, arity
, depth
+1 );
875 //add care pairs based on each pair of non-disequal arguments
876 for( std::map
< TNode
, quantifiers::TermArgTrie
>::iterator it
= t1
->d_data
.begin(); it
!= t1
->d_data
.end(); ++it
){
877 std::map
< TNode
, quantifiers::TermArgTrie
>::iterator it2
= it
;
879 for( ; it2
!= t1
->d_data
.end(); ++it2
){
880 if( !d_equalityEngine
.areDisequal(it
->first
, it2
->first
, false) ){
881 addCarePairs( &it
->second
, &it2
->second
, arity
, depth
+1 );
886 //add care pairs based on product of indices, non-disequal arguments
887 for( std::map
< TNode
, quantifiers::TermArgTrie
>::iterator it
= t1
->d_data
.begin(); it
!= t1
->d_data
.end(); ++it
){
888 for( std::map
< TNode
, quantifiers::TermArgTrie
>::iterator it2
= t2
->d_data
.begin(); it2
!= t2
->d_data
.end(); ++it2
){
889 if( !d_equalityEngine
.areDisequal(it
->first
, it2
->first
, false) ){
890 addCarePairs( &it
->second
, &it2
->second
, arity
, depth
+1 );
898 void TheoryStrings::computeCareGraph(){
899 //computing the care graph here is probably still necessary, due to operators that take non-string arguments TODO: verify
900 Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Build term indices..." << std::endl
;
901 std::map
< Node
, quantifiers::TermArgTrie
> index
;
902 std::map
< Node
, unsigned > arity
;
903 unsigned functionTerms
= d_functionsTerms
.size();
904 for (unsigned i
= 0; i
< functionTerms
; ++ i
) {
905 TNode f1
= d_functionsTerms
[i
];
906 Trace("strings-cg") << "...build for " << f1
<< std::endl
;
907 Node op
= f1
.getOperator();
908 std::vector
< TNode
> reps
;
909 bool has_trigger_arg
= false;
910 for( unsigned j
=0; j
<f1
.getNumChildren(); j
++ ){
911 reps
.push_back( d_equalityEngine
.getRepresentative( f1
[j
] ) );
912 if( d_equalityEngine
.isTriggerTerm( f1
[j
], THEORY_STRINGS
) ){
913 has_trigger_arg
= true;
916 if( has_trigger_arg
){
917 index
[op
].addTerm( f1
, reps
);
918 arity
[op
] = reps
.size();
922 for( std::map
< Node
, quantifiers::TermArgTrie
>::iterator itii
= index
.begin(); itii
!= index
.end(); ++itii
){
923 Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Process index " << itii
->first
<< "..." << std::endl
;
924 addCarePairs( &itii
->second
, NULL
, arity
[ itii
->first
], 0 );
928 void TheoryStrings::assertPendingFact(Node atom
, bool polarity
, Node exp
) {
929 Trace("strings-pending") << "Assert pending fact : " << atom
<< " " << polarity
<< " from " << exp
<< std::endl
;
930 Assert(atom
.getKind() != kind::OR
, "Infer error: a split.");
931 if( atom
.getKind()==kind::EQUAL
){
932 Trace("strings-pending-debug") << " Register term" << std::endl
;
933 for( unsigned j
=0; j
<2; j
++ ) {
934 if( !d_equalityEngine
.hasTerm( atom
[j
] ) && atom
[j
].getType().isString() ) {
935 registerTerm( atom
[j
], 0 );
938 Trace("strings-pending-debug") << " Now assert equality" << std::endl
;
939 d_equalityEngine
.assertEquality( atom
, polarity
, exp
);
940 Trace("strings-pending-debug") << " Finished assert equality" << std::endl
;
942 d_equalityEngine
.assertPredicate( atom
, polarity
, exp
);
944 if( atom
.getKind()==kind::STRING_IN_REGEXP
){
945 addExtendedFuncTerm( atom
);
946 if( polarity
&& atom
[1].getKind()==kind::REGEXP_RANGE
){
947 if( d_extf_infer_cache_u
.find( atom
)==d_extf_infer_cache_u
.end() ){
948 d_extf_infer_cache_u
.insert( atom
);
949 //length of first argument is one
950 Node conc
= d_one
.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, atom
[0] ) );
951 Node lem
= NodeManager::currentNM()->mkNode( kind::OR
, atom
.negate(), conc
);
952 Trace("strings-lemma") << "Strings::Lemma RE-Range-Len : " << lem
<< std::endl
;
958 Trace("strings-pending-debug") << " Now collect terms" << std::endl
;
959 //collect extended function terms in the atom
960 std::map
< Node
, bool > visited
;
961 collectExtendedFuncTerms( atom
, visited
);
962 Trace("strings-pending-debug") << " Finished collect terms" << std::endl
;
965 void TheoryStrings::doPendingFacts() {
967 while( !d_conflict
&& i
<d_pending
.size() ) {
968 Node fact
= d_pending
[i
];
969 Node exp
= d_pending_exp
[ fact
];
970 if(fact
.getKind() == kind::AND
) {
971 for(size_t j
=0; j
<fact
.getNumChildren(); j
++) {
972 bool polarity
= fact
[j
].getKind() != kind::NOT
;
973 TNode atom
= polarity
? fact
[j
] : fact
[j
][0];
974 assertPendingFact(atom
, polarity
, exp
);
977 bool polarity
= fact
.getKind() != kind::NOT
;
978 TNode atom
= polarity
? fact
: fact
[0];
979 assertPendingFact(atom
, polarity
, exp
);
984 d_pending_exp
.clear();
987 void TheoryStrings::doPendingLemmas() {
988 if( !d_conflict
&& !d_lemma_cache
.empty() ){
989 for( unsigned i
=0; i
<d_lemma_cache
.size(); i
++ ){
990 Trace("strings-pending") << "Process pending lemma : " << d_lemma_cache
[i
] << std::endl
;
991 d_out
->lemma( d_lemma_cache
[i
] );
993 for( std::map
< Node
, bool >::iterator it
= d_pending_req_phase
.begin(); it
!= d_pending_req_phase
.end(); ++it
){
994 Trace("strings-pending") << "Require phase : " << it
->first
<< ", polarity = " << it
->second
<< std::endl
;
995 d_out
->requirePhase( it
->first
, it
->second
);
998 d_lemma_cache
.clear();
999 d_pending_req_phase
.clear();
1002 bool TheoryStrings::hasProcessed() {
1003 return d_conflict
|| !d_lemma_cache
.empty() || !d_pending
.empty();
1006 void TheoryStrings::addToExplanation( Node a
, Node b
, std::vector
< Node
>& exp
) {
1008 Debug("strings-explain") << "Add to explanation : " << a
<< " == " << b
<< std::endl
;
1009 Assert( areEqual( a
, b
) );
1010 exp
.push_back( a
.eqNode( b
) );
1014 void TheoryStrings::addToExplanation( Node lit
, std::vector
< Node
>& exp
) {
1015 if( !lit
.isNull() ){
1016 exp
.push_back( lit
);
1020 void TheoryStrings::checkInit() {
1022 d_eqc_to_const
.clear();
1023 d_eqc_to_const_base
.clear();
1024 d_eqc_to_const_exp
.clear();
1025 d_eqc_to_len_term
.clear();
1026 d_term_index
.clear();
1027 d_strings_eqc
.clear();
1029 std::map
< Kind
, unsigned > ncongruent
;
1030 std::map
< Kind
, unsigned > congruent
;
1031 d_emptyString_r
= getRepresentative( d_emptyString
);
1032 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( &d_equalityEngine
);
1033 while( !eqcs_i
.isFinished() ){
1034 Node eqc
= (*eqcs_i
);
1035 TypeNode tn
= eqc
.getType();
1036 if( !tn
.isRegExp() ){
1037 if( tn
.isString() ){
1038 d_strings_eqc
.push_back( eqc
);
1041 eq::EqClassIterator eqc_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
1042 while( !eqc_i
.isFinished() ) {
1044 if( tn
.isInteger() ){
1045 if( n
.getKind()==kind::STRING_LENGTH
){
1046 Node nr
= getRepresentative( n
[0] );
1047 d_eqc_to_len_term
[nr
] = n
[0];
1049 }else if( n
.isConst() ){
1050 d_eqc_to_const
[eqc
] = n
;
1051 d_eqc_to_const_base
[eqc
] = n
;
1052 d_eqc_to_const_exp
[eqc
] = Node::null();
1053 }else if( n
.getNumChildren()>0 ){
1054 Kind k
= n
.getKind();
1055 if( k
!=kind::EQUAL
){
1056 if( d_congruent
.find( n
)==d_congruent
.end() ){
1057 std::vector
< Node
> c
;
1058 Node nc
= d_term_index
[k
].add( n
, 0, this, d_emptyString_r
, c
);
1060 //check if we have inferred a new equality by removal of empty components
1061 if( n
.getKind()==kind::STRING_CONCAT
&& !areEqual( nc
, n
) ){
1062 std::vector
< Node
> exp
;
1063 unsigned count
[2] = { 0, 0 };
1064 while( count
[0]<nc
.getNumChildren() || count
[1]<n
.getNumChildren() ){
1065 //explain empty prefixes
1066 for( unsigned t
=0; t
<2; t
++ ){
1067 Node nn
= t
==0 ? nc
: n
;
1068 while( count
[t
]<nn
.getNumChildren() &&
1069 ( nn
[count
[t
]]==d_emptyString
|| areEqual( nn
[count
[t
]], d_emptyString
) ) ){
1070 if( nn
[count
[t
]]!=d_emptyString
){
1071 exp
.push_back( nn
[count
[t
]].eqNode( d_emptyString
) );
1076 //explain equal components
1077 if( count
[0]<nc
.getNumChildren() ){
1078 Assert( count
[1]<n
.getNumChildren() );
1079 if( nc
[count
[0]]!=n
[count
[1]] ){
1080 exp
.push_back( nc
[count
[0]].eqNode( n
[count
[1]] ) );
1086 //infer the equality
1087 sendInference( exp
, n
.eqNode( nc
), "I_Norm" );
1089 //update the extf map : only process if neither has been reduced
1090 NodeBoolMap::const_iterator it
= d_ext_func_terms
.find( n
);
1091 if( it
!=d_ext_func_terms
.end() ){
1092 if( d_ext_func_terms
.find( nc
)==d_ext_func_terms
.end() ){
1093 d_ext_func_terms
[nc
] = (*it
).second
;
1095 d_ext_func_terms
[nc
] = d_ext_func_terms
[nc
] && (*it
).second
;
1097 d_ext_func_terms
[n
] = false;
1100 //this node is congruent to another one, we can ignore it
1101 Trace("strings-process-debug") << " congruent term : " << n
<< std::endl
;
1102 d_congruent
.insert( n
);
1104 }else if( k
==kind::STRING_CONCAT
&& c
.size()==1 ){
1105 Trace("strings-process-debug") << " congruent term by singular : " << n
<< " " << c
[0] << std::endl
;
1107 if( !areEqual( c
[0], n
) ){
1108 std::vector
< Node
> exp
;
1109 //explain empty components
1110 bool foundNEmpty
= false;
1111 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1112 if( areEqual( n
[i
], d_emptyString
) ){
1113 if( n
[i
]!=d_emptyString
){
1114 exp
.push_back( n
[i
].eqNode( d_emptyString
) );
1117 Assert( !foundNEmpty
);
1119 exp
.push_back( n
[i
].eqNode( c
[0] ) );
1124 AlwaysAssert( foundNEmpty
);
1125 //infer the equality
1126 sendInference( exp
, n
.eqNode( c
[0] ), "I_Norm_S" );
1128 d_congruent
.insert( n
);
1138 if( d_congruent
.find( n
)==d_congruent
.end() ){
1142 Trace("strings-process-debug") << " congruent variable : " << n
<< std::endl
;
1143 d_congruent
.insert( n
);
1152 if( Trace
.isOn("strings-process") ){
1153 for( std::map
< Kind
, TermIndex
>::iterator it
= d_term_index
.begin(); it
!= d_term_index
.end(); ++it
){
1154 Trace("strings-process") << " Terms[" << it
->first
<< "] = " << ncongruent
[it
->first
] << "/" << (congruent
[it
->first
]+ncongruent
[it
->first
]) << std::endl
;
1157 Trace("strings-process") << "Done check init, addedLemma = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
1158 //now, infer constants for equivalence classes
1159 if( !hasProcessed() ){
1163 Trace("strings-process-debug") << "Check constant equivalence classes..." << std::endl
;
1164 prevSize
= d_eqc_to_const
.size();
1165 std::vector
< Node
> vecc
;
1166 checkConstantEquivalenceClasses( &d_term_index
[kind::STRING_CONCAT
], vecc
);
1167 }while( !hasProcessed() && d_eqc_to_const
.size()>prevSize
);
1168 Trace("strings-process") << "Done check constant equivalence classes, addedLemma = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
1172 void TheoryStrings::checkConstantEquivalenceClasses( TermIndex
* ti
, std::vector
< Node
>& vecc
) {
1173 Node n
= ti
->d_data
;
1175 //construct the constant
1176 Node c
= mkConcat( vecc
);
1177 if( !areEqual( n
, c
) ){
1178 Trace("strings-debug") << "Constant eqc : " << c
<< " for " << n
<< std::endl
;
1179 Trace("strings-debug") << " ";
1180 for( unsigned i
=0; i
<vecc
.size(); i
++ ){
1181 Trace("strings-debug") << vecc
[i
] << " ";
1183 Trace("strings-debug") << std::endl
;
1185 unsigned countc
= 0;
1186 std::vector
< Node
> exp
;
1187 while( count
<n
.getNumChildren() ){
1188 while( count
<n
.getNumChildren() && areEqual( n
[count
], d_emptyString
) ){
1189 addToExplanation( n
[count
], d_emptyString
, exp
);
1192 if( count
<n
.getNumChildren() ){
1193 Trace("strings-debug") << "...explain " << n
[count
] << " " << vecc
[countc
] << std::endl
;
1194 if( !areEqual( n
[count
], vecc
[countc
] ) ){
1195 Node nrr
= getRepresentative( n
[count
] );
1196 Assert( !d_eqc_to_const_exp
[nrr
].isNull() );
1197 addToExplanation( n
[count
], d_eqc_to_const_base
[nrr
], exp
);
1198 exp
.push_back( d_eqc_to_const_exp
[nrr
] );
1200 addToExplanation( n
[count
], vecc
[countc
], exp
);
1206 //exp contains an explanation of n==c
1207 Assert( countc
==vecc
.size() );
1209 sendInference( exp
, n
.eqNode( c
), "I_CONST_MERGE" );
1211 }else if( !hasProcessed() ){
1212 Node nr
= getRepresentative( n
);
1213 std::map
< Node
, Node
>::iterator it
= d_eqc_to_const
.find( nr
);
1214 if( it
==d_eqc_to_const
.end() ){
1215 Trace("strings-debug") << "Set eqc const " << n
<< " to " << c
<< std::endl
;
1216 d_eqc_to_const
[nr
] = c
;
1217 d_eqc_to_const_base
[nr
] = n
;
1218 d_eqc_to_const_exp
[nr
] = mkAnd( exp
);
1219 }else if( c
!=it
->second
){
1221 Trace("strings-debug") << "Conflict, other constant was " << it
->second
<< ", this constant was " << c
<< std::endl
;
1222 if( d_eqc_to_const_exp
[nr
].isNull() ){
1223 // n==c ^ n == c' => false
1224 addToExplanation( n
, it
->second
, exp
);
1226 // n==c ^ n == d_eqc_to_const_base[nr] == c' => false
1227 exp
.push_back( d_eqc_to_const_exp
[nr
] );
1228 addToExplanation( n
, d_eqc_to_const_base
[nr
], exp
);
1230 sendInference( exp
, d_false
, "I_CONST_CONFLICT" );
1233 Trace("strings-debug") << "Duplicate constant." << std::endl
;
1238 for( std::map
< TNode
, TermIndex
>::iterator it
= ti
->d_children
.begin(); it
!= ti
->d_children
.end(); ++it
){
1239 std::map
< Node
, Node
>::iterator itc
= d_eqc_to_const
.find( it
->first
);
1240 if( itc
!=d_eqc_to_const
.end() ){
1241 vecc
.push_back( itc
->second
);
1242 checkConstantEquivalenceClasses( &it
->second
, vecc
);
1244 if( hasProcessed() ){
1251 void TheoryStrings::checkExtfEval( int effort
) {
1252 Trace("strings-extf-list") << "Active extended functions, effort=" << effort
<< " : " << std::endl
;
1253 d_extf_info_tmp
.clear();
1254 bool has_nreduce
= false;
1255 Trace("strings-extf-debug") << "Checking " << d_ext_func_terms
.size() << " extended functions." << std::endl
;
1256 for( NodeBoolMap::iterator it
= d_ext_func_terms
.begin(); it
!= d_ext_func_terms
.end(); ++it
){
1257 //if not already reduced
1259 Node n
= (*it
).first
;
1261 //setup information about extf
1262 std::map
< Node
, ExtfInfo
>::iterator iti
= d_extf_info
.find( n
);
1263 Assert( iti
!=d_extf_info
.end() );
1264 d_extf_info_tmp
[n
].init();
1265 std::map
< Node
, ExtfInfoTmp
>::iterator itit
= d_extf_info_tmp
.find( n
);
1267 if( n
.getType().isBoolean() ){
1268 if( areEqual( n
, d_true
) ){
1269 itit
->second
.d_pol
= 1;
1270 }else if( areEqual( n
, d_false
) ){
1271 itit
->second
.d_pol
= -1;
1274 //compute rep vars map
1275 for( unsigned j
=0; j
<iti
->second
.d_vars
.size(); j
++ ){
1276 Node nr
= getRepresentative( iti
->second
.d_vars
[j
] );
1277 itit
->second
.d_rep_vars
[nr
].push_back( iti
->second
.d_vars
[j
] );
1280 Trace("strings-extf-debug") << "Check extf " << n
<< ", pol = " << itit
->second
.d_pol
<< ", effort=" << effort
<< "..." << std::endl
;
1281 //build up a best current substitution for the variables in the term, exp is explanation for substitution
1282 std::vector
< Node
> var
;
1283 std::vector
< Node
> sub
;
1284 for( std::map
< Node
, std::vector
< Node
> >::iterator itv
= itit
->second
.d_rep_vars
.begin(); itv
!= itit
->second
.d_rep_vars
.end(); ++itv
){
1285 Node nr
= itv
->first
;
1291 s
= d_valuation
.getModel()->getRepresentative( nr
);
1293 std::map
< Node
, Node
>::iterator itc
= d_eqc_to_const
.find( nr
);
1294 if( itc
!=d_eqc_to_const
.end() ){
1295 //constant equivalence classes
1296 b
= d_eqc_to_const_base
[nr
];
1298 e
= d_eqc_to_const_exp
[nr
];
1299 }else if( effort
>=1 && effort
<3 ){
1301 b
= d_normal_forms_base
[nr
];
1302 std::vector
< Node
> expt
;
1303 s
= getNormalString( b
, expt
);
1309 for( unsigned i
=0; i
<itv
->second
.size(); i
++ ){
1310 if( itv
->second
[i
]!=s
){
1311 var
.push_back( itv
->second
[i
] );
1314 addToExplanation( itv
->second
[i
], b
, itit
->second
.d_exp
);
1316 Trace("strings-extf-debug") << " " << itv
->second
[i
] << " --> " << s
<< std::endl
;
1320 if( added
&& !e
.isNull() ){
1321 addToExplanation( e
, itit
->second
.d_exp
);
1327 //do substitution, evaluate
1328 Node nr
= n
.substitute( var
.begin(), var
.end(), sub
.begin(), sub
.end() );
1329 Node nrc
= Rewriter::rewrite( nr
);
1330 //if rewrites to a constant, then do the inference and mark as reduced
1331 if( nrc
.isConst() ){
1333 d_ext_func_terms
[n
] = false;
1334 Trace("strings-extf-debug") << " resolvable by evaluation..." << std::endl
;
1335 std::vector
< Node
> exps
;
1336 Trace("strings-extf-debug") << " get symbolic definition..." << std::endl
;
1337 Node nrs
= getSymbolicDefinition( nr
, exps
);
1338 if( !nrs
.isNull() ){
1339 Trace("strings-extf-debug") << " rewrite " << nrs
<< "..." << std::endl
;
1340 nrs
= Rewriter::rewrite( nrs
);
1341 //ensure the symbolic form is non-trivial
1342 if( nrs
.isConst() ){
1343 Trace("strings-extf-debug") << " symbolic definition is trivial..." << std::endl
;
1347 Trace("strings-extf-debug") << " could not infer symbolic definition." << std::endl
;
1350 if( !nrs
.isNull() ){
1351 Trace("strings-extf-debug") << " symbolic def : " << nrs
<< std::endl
;
1352 if( !areEqual( nrs
, nrc
) ){
1353 //infer symbolic unit
1354 if( n
.getType().isBoolean() ){
1355 conc
= nrc
==d_true
? nrs
: nrs
.negate();
1357 conc
= nrs
.eqNode( nrc
);
1359 itit
->second
.d_exp
.clear();
1362 if( !areEqual( n
, nrc
) ){
1363 if( n
.getType().isBoolean() ){
1364 if( areEqual( n
, nrc
==d_true
? d_false
: d_true
) ){
1365 itit
->second
.d_exp
.push_back( nrc
==d_true
? n
.negate() : n
);
1368 conc
= nrc
==d_true
? n
: n
.negate();
1371 conc
= n
.eqNode( nrc
);
1375 if( !conc
.isNull() ){
1376 Trace("strings-extf") << " resolve extf : " << nr
<< " -> " << nrc
<< std::endl
;
1377 sendInference( itit
->second
.d_exp
, conc
, effort
==0 ? "EXTF" : "EXTF-N", true );
1379 Trace("strings-extf-debug") << " conflict, return." << std::endl
;
1384 //check if it is already equal, if so, mark as reduced. Otherwise, do nothing.
1385 if( areEqual( n
, nrc
) ){
1386 Trace("strings-extf") << " resolved extf, since satisfied by model: " << n
<< std::endl
;
1387 itit
->second
.d_model_active
= false;
1390 //if it reduces to a conjunction, infer each and reduce
1391 }else if( ( nrc
.getKind()==kind::OR
&& itit
->second
.d_pol
==-1 ) || ( nrc
.getKind()==kind::AND
&& itit
->second
.d_pol
==1 ) ){
1393 d_ext_func_terms
[n
] = false;
1394 itit
->second
.d_exp
.push_back( itit
->second
.d_pol
==-1 ? n
.negate() : n
);
1395 Trace("strings-extf-debug") << " decomposable..." << std::endl
;
1396 Trace("strings-extf") << " resolve extf : " << nr
<< " -> " << nrc
<< ", pol = " << itit
->second
.d_pol
<< std::endl
;
1397 for( unsigned i
=0; i
<nrc
.getNumChildren(); i
++ ){
1398 sendInference( itit
->second
.d_exp
, itit
->second
.d_pol
==-1 ? nrc
[i
].negate() : nrc
[i
], effort
==0 ? "EXTF_d" : "EXTF_d-N" );
1406 if( !to_reduce
.isNull() ){
1409 Trace("strings-extf") << " cannot rewrite extf : " << to_reduce
<< std::endl
;
1411 checkExtfInference( n
, to_reduce
, itit
->second
, effort
);
1412 if( Trace
.isOn("strings-extf-list") ){
1413 Trace("strings-extf-list") << " * " << to_reduce
;
1414 if( itit
->second
.d_pol
!=0 ){
1415 Trace("strings-extf-list") << ", pol = " << itit
->second
.d_pol
;
1418 Trace("strings-extf-list") << ", from " << n
;
1420 Trace("strings-extf-list") << std::endl
;
1423 if( d_ext_func_terms
[n
] && itit
->second
.d_model_active
){
1427 Trace("strings-extf-debug") << " already reduced " << (*it
).first
<< std::endl
;
1430 d_has_extf
= has_nreduce
;
1433 void TheoryStrings::checkExtfInference( Node n
, Node nr
, ExtfInfoTmp
& in
, int effort
){
1434 //make additional inferences that do not contribute to the reduction of n, but may help show a refutation
1436 //add original to explanation
1437 in
.d_exp
.push_back( in
.d_pol
==1 ? n
: n
.negate() );
1439 //d_extf_infer_cache stores whether we have made the inferences associated with a node n,
1440 // this may need to be generalized if multiple inferences apply
1442 if( nr
.getKind()==kind::STRING_STRCTN
){
1443 if( ( in
.d_pol
==1 && nr
[1].getKind()==kind::STRING_CONCAT
) || ( in
.d_pol
==-1 && nr
[0].getKind()==kind::STRING_CONCAT
) ){
1444 if( d_extf_infer_cache
.find( nr
)==d_extf_infer_cache
.end() ){
1445 d_extf_infer_cache
.insert( nr
);
1447 //one argument does (not) contain each of the components of the other argument
1448 int index
= in
.d_pol
==1 ? 1 : 0;
1449 std::vector
< Node
> children
;
1450 children
.push_back( nr
[0] );
1451 children
.push_back( nr
[1] );
1452 //Node exp_n = mkAnd( exp );
1453 for( unsigned i
=0; i
<nr
[index
].getNumChildren(); i
++ ){
1454 children
[index
] = nr
[index
][i
];
1455 Node conc
= NodeManager::currentNM()->mkNode( kind::STRING_STRCTN
, children
);
1456 //can mark as reduced, since model for n => model for conc
1457 d_ext_func_terms
[conc
] = false;
1458 sendInference( in
.d_exp
, in
.d_pol
==1 ? conc
: conc
.negate(), "CTN_Decompose" );
1463 //store this (reduced) assertion
1464 //Assert( effort==0 || nr[0]==getRepresentative( nr[0] ) );
1465 bool pol
= in
.d_pol
==1;
1466 if( std::find( d_extf_info_tmp
[nr
[0]].d_ctn
[pol
].begin(), d_extf_info_tmp
[nr
[0]].d_ctn
[pol
].end(), nr
[1] )==d_extf_info_tmp
[nr
[0]].d_ctn
[pol
].end() ){
1467 Trace("strings-extf-debug") << " store contains info : " << nr
[0] << " " << pol
<< " " << nr
[1] << std::endl
;
1468 d_extf_info_tmp
[nr
[0]].d_ctn
[pol
].push_back( nr
[1] );
1469 d_extf_info_tmp
[nr
[0]].d_ctn_from
[pol
].push_back( n
);
1470 //transitive closure for contains
1472 for( unsigned i
=0; i
<d_extf_info_tmp
[nr
[0]].d_ctn
[opol
].size(); i
++ ){
1473 Node onr
= d_extf_info_tmp
[nr
[0]].d_ctn
[opol
][i
];
1474 Node conc
= NodeManager::currentNM()->mkNode( kind::STRING_STRCTN
, pol
? nr
[1] : onr
, pol
? onr
: nr
[1] );
1475 conc
= Rewriter::rewrite( conc
);
1476 bool do_infer
= false;
1477 if( conc
.getKind()==kind::EQUAL
){
1478 do_infer
= !areDisequal( conc
[0], conc
[1] );
1480 do_infer
= !areEqual( conc
, d_false
);
1483 conc
= conc
.negate();
1484 std::vector
< Node
> exp_c
;
1485 exp_c
.insert( exp_c
.end(), in
.d_exp
.begin(), in
.d_exp
.end() );
1486 Node ofrom
= d_extf_info_tmp
[nr
[0]].d_ctn_from
[opol
][i
];
1487 Assert( d_extf_info_tmp
.find( ofrom
)!=d_extf_info_tmp
.end() );
1488 exp_c
.insert( exp_c
.end(), d_extf_info_tmp
[ofrom
].d_exp
.begin(), d_extf_info_tmp
[ofrom
].d_exp
.end() );
1489 sendInference( exp_c
, conc
, "CTN_Trans" );
1493 Trace("strings-extf-debug") << " redundant." << std::endl
;
1494 d_ext_func_terms
[n
] = false;
1501 void TheoryStrings::collectVars( Node n
, std::vector
< Node
>& vars
, std::map
< Node
, bool >& visited
) {
1503 if( visited
.find( n
)==visited
.end() ){
1505 if( n
.getNumChildren()>0 ){
1506 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1507 collectVars( n
[i
], vars
, visited
);
1510 //Node nr = getRepresentative( n );
1511 //vars[nr].push_back( n );
1512 vars
.push_back( n
);
1518 Node
TheoryStrings::getSymbolicDefinition( Node n
, std::vector
< Node
>& exp
) {
1519 if( n
.getNumChildren()==0 ){
1520 NodeNodeMap::const_iterator it
= d_proxy_var
.find( n
);
1521 if( it
==d_proxy_var
.end() ){
1522 return Node::null();
1524 Node eq
= n
.eqNode( (*it
).second
);
1525 eq
= Rewriter::rewrite( eq
);
1526 if( std::find( exp
.begin(), exp
.end(), eq
)==exp
.end() ){
1527 exp
.push_back( eq
);
1529 return (*it
).second
;
1532 std::vector
< Node
> children
;
1533 if (n
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
1534 children
.push_back( n
.getOperator() );
1536 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1537 if( n
.getKind()==kind::STRING_IN_REGEXP
&& i
==1 ){
1538 children
.push_back( n
[i
] );
1540 Node ns
= getSymbolicDefinition( n
[i
], exp
);
1542 return Node::null();
1544 children
.push_back( ns
);
1548 return NodeManager::currentNM()->mkNode( n
.getKind(), children
);
1552 Node
TheoryStrings::getConstantEqc( Node eqc
) {
1553 std::map
< Node
, Node
>::iterator it
= d_eqc_to_const
.find( eqc
);
1554 if( it
!=d_eqc_to_const
.end() ){
1557 return Node::null();
1561 void TheoryStrings::debugPrintFlatForms( const char * tc
){
1562 for( unsigned k
=0; k
<d_strings_eqc
.size(); k
++ ){
1563 Node eqc
= d_strings_eqc
[k
];
1564 if( d_eqc
[eqc
].size()>1 ){
1565 Trace( tc
) << "EQC [" << eqc
<< "]" << std::endl
;
1567 Trace( tc
) << "eqc [" << eqc
<< "]";
1569 std::map
< Node
, Node
>::iterator itc
= d_eqc_to_const
.find( eqc
);
1570 if( itc
!=d_eqc_to_const
.end() ){
1571 Trace( tc
) << " C: " << itc
->second
;
1572 if( d_eqc
[eqc
].size()>1 ){
1573 Trace( tc
) << std::endl
;
1576 if( d_eqc
[eqc
].size()>1 ){
1577 for( unsigned i
=0; i
<d_eqc
[eqc
].size(); i
++ ){
1578 Node n
= d_eqc
[eqc
][i
];
1580 for( unsigned j
=0; j
<d_flat_form
[n
].size(); j
++ ){
1581 Node fc
= d_flat_form
[n
][j
];
1582 itc
= d_eqc_to_const
.find( fc
);
1584 if( itc
!=d_eqc_to_const
.end() ){
1585 Trace( tc
) << itc
->second
;
1591 Trace( tc
) << ", from " << n
;
1593 Trace( tc
) << std::endl
;
1596 Trace( tc
) << std::endl
;
1599 Trace( tc
) << std::endl
;
1602 void TheoryStrings::debugPrintNormalForms( const char * tc
) {
1605 struct sortConstLength
{
1606 std::map
< Node
, unsigned > d_const_length
;
1607 bool operator() (Node i
, Node j
) {
1608 std::map
< Node
, unsigned >::iterator it_i
= d_const_length
.find( i
);
1609 std::map
< Node
, unsigned >::iterator it_j
= d_const_length
.find( j
);
1610 if( it_i
==d_const_length
.end() ){
1611 if( it_j
==d_const_length
.end() ){
1617 if( it_j
==d_const_length
.end() ){
1620 return it_i
->second
<it_j
->second
;
1627 void TheoryStrings::checkFlatForms() {
1628 //first check for cycles, while building ordering of equivalence classes
1630 d_flat_form
.clear();
1631 d_flat_form_index
.clear();
1632 Trace("strings-process") << "Check equivalence classes cycles...." << std::endl
;
1633 //rebuild strings eqc based on acyclic ordering
1634 std::vector
< Node
> eqc
;
1635 eqc
.insert( eqc
.end(), d_strings_eqc
.begin(), d_strings_eqc
.end() );
1636 d_strings_eqc
.clear();
1637 if( options::stringBinaryCsp() ){
1638 //sort: process smallest constants first (necessary if doing binary splits)
1639 sortConstLength scl
;
1640 for( unsigned i
=0; i
<eqc
.size(); i
++ ){
1641 std::map
< Node
, Node
>::iterator itc
= d_eqc_to_const
.find( eqc
[i
] );
1642 if( itc
!=d_eqc_to_const
.end() ){
1643 scl
.d_const_length
[eqc
[i
]] = itc
->second
.getConst
<String
>().size();
1646 std::sort( eqc
.begin(), eqc
.end(), scl
);
1648 for( unsigned i
=0; i
<eqc
.size(); i
++ ){
1649 std::vector
< Node
> curr
;
1650 std::vector
< Node
> exp
;
1651 checkCycles( eqc
[i
], curr
, exp
);
1652 if( hasProcessed() ){
1656 Trace("strings-process-debug") << "Done check cycles, lemmas = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << std::endl
;
1657 if( !hasProcessed() ){
1658 //debug print flat forms
1659 if( Trace
.isOn("strings-ff") ){
1660 Trace("strings-ff") << "Flat forms : " << std::endl
;
1661 debugPrintFlatForms( "strings-ff" );
1664 //inferences without recursively expanding flat forms
1666 //(1) approximate equality by containment, infer conflicts
1667 for( unsigned k
=0; k
<d_strings_eqc
.size(); k
++ ){
1668 Node eqc
= d_strings_eqc
[k
];
1669 Node c
= getConstantEqc( eqc
);
1671 //if equivalence class is constant, all component constants in flat forms must be contained in it, in order
1672 std::map
< Node
, std::vector
< Node
> >::iterator it
= d_eqc
.find( eqc
);
1673 if( it
!=d_eqc
.end() ){
1674 for( unsigned i
=0; i
<it
->second
.size(); i
++ ){
1675 Node n
= it
->second
[i
];
1677 if( !TheoryStringsRewriter::canConstantContainList( c
, d_flat_form
[n
], firstc
, lastc
) ){
1678 Trace("strings-ff-debug") << "Flat form for " << n
<< " cannot be contained in constant " << c
<< std::endl
;
1679 Trace("strings-ff-debug") << " indices = " << firstc
<< "/" << lastc
<< std::endl
;
1680 //conflict, explanation is n = base ^ base = c ^ relevant porition of ( n = f[n] )
1681 std::vector
< Node
> exp
;
1682 Assert( d_eqc_to_const_base
.find( eqc
)!=d_eqc_to_const_base
.end() );
1683 addToExplanation( n
, d_eqc_to_const_base
[eqc
], exp
);
1684 Assert( d_eqc_to_const_exp
.find( eqc
)!=d_eqc_to_const_exp
.end() );
1685 if( !d_eqc_to_const_exp
[eqc
].isNull() ){
1686 exp
.push_back( d_eqc_to_const_exp
[eqc
] );
1688 for( int e
=firstc
; e
<=lastc
; e
++ ){
1689 if( d_flat_form
[n
][e
].isConst() ){
1690 Assert( e
>=0 && e
<(int)d_flat_form_index
[n
].size() );
1691 Assert( d_flat_form_index
[n
][e
]>=0 && d_flat_form_index
[n
][e
]<(int)n
.getNumChildren() );
1692 addToExplanation( d_flat_form
[n
][e
], n
[d_flat_form_index
[n
][e
]], exp
);
1695 Node conc
= d_false
;
1696 sendInference( exp
, conc
, "F_NCTN" );
1704 //(2) scan lists, unification to infer conflicts and equalities
1705 for( unsigned k
=0; k
<d_strings_eqc
.size(); k
++ ){
1706 Node eqc
= d_strings_eqc
[k
];
1707 std::map
< Node
, std::vector
< Node
> >::iterator it
= d_eqc
.find( eqc
);
1708 if( it
!=d_eqc
.end() && it
->second
.size()>1 ){
1709 //iterate over start index
1710 for( unsigned start
=0; start
<it
->second
.size()-1; start
++ ){
1711 for( unsigned r
=0; r
<2; r
++ ){
1713 std::vector
< Node
> inelig
;
1714 for( unsigned i
=0; i
<=start
; i
++ ){
1715 inelig
.push_back( it
->second
[start
] );
1717 Node a
= it
->second
[start
];
1720 std::vector
< Node
> exp
;
1721 //std::vector< Node > exp_n;
1724 if( count
==d_flat_form
[a
].size() ){
1725 for( unsigned i
=start
+1; i
<it
->second
.size(); i
++ ){
1727 if( std::find( inelig
.begin(), inelig
.end(), b
)==inelig
.end() ){
1728 if( count
<d_flat_form
[b
].size() ){
1730 std::vector
< Node
> conc_c
;
1731 for( unsigned j
=count
; j
<d_flat_form
[b
].size(); j
++ ){
1732 conc_c
.push_back( b
[d_flat_form_index
[b
][j
]].eqNode( d_emptyString
) );
1734 Assert( !conc_c
.empty() );
1735 conc
= mkAnd( conc_c
);
1738 //swap, will enforce is empty past current
1739 a
= it
->second
[i
]; b
= it
->second
[start
];
1743 inelig
.push_back( it
->second
[i
] );
1747 Node curr
= d_flat_form
[a
][count
];
1748 Node curr_c
= getConstantEqc( curr
);
1749 Node ac
= a
[d_flat_form_index
[a
][count
]];
1750 std::vector
< Node
> lexp
;
1751 Node lcurr
= getLength( ac
, lexp
);
1752 for( unsigned i
=1; i
<it
->second
.size(); i
++ ){
1754 if( std::find( inelig
.begin(), inelig
.end(), b
)==inelig
.end() ){
1755 if( count
==d_flat_form
[b
].size() ){
1756 inelig
.push_back( b
);
1758 std::vector
< Node
> conc_c
;
1759 for( unsigned j
=count
; j
<d_flat_form
[a
].size(); j
++ ){
1760 conc_c
.push_back( a
[d_flat_form_index
[a
][j
]].eqNode( d_emptyString
) );
1762 Assert( !conc_c
.empty() );
1763 conc
= mkAnd( conc_c
);
1769 Node cc
= d_flat_form
[b
][count
];
1771 Node bc
= b
[d_flat_form_index
[b
][count
]];
1772 inelig
.push_back( b
);
1773 Assert( !areEqual( curr
, cc
) );
1774 Node cc_c
= getConstantEqc( cc
);
1775 if( !curr_c
.isNull() && !cc_c
.isNull() ){
1776 //check for constant conflict
1778 Node s
= TheoryStringsRewriter::splitConstant( cc_c
, curr_c
, index
, r
==1 );
1780 addToExplanation( ac
, d_eqc_to_const_base
[curr
], exp
);
1781 addToExplanation( d_eqc_to_const_exp
[curr
], exp
);
1782 addToExplanation( bc
, d_eqc_to_const_base
[cc
], exp
);
1783 addToExplanation( d_eqc_to_const_exp
[cc
], exp
);
1788 }else if( (d_flat_form
[a
].size()-1)==count
&& (d_flat_form
[b
].size()-1)==count
){
1789 conc
= ac
.eqNode( bc
);
1793 //if lengths are the same, apply LengthEq
1794 std::vector
< Node
> lexp2
;
1795 Node lcc
= getLength( bc
, lexp2
);
1796 if( areEqual( lcurr
, lcc
) ){
1797 Trace("strings-ff-debug") << "Infer " << ac
<< " == " << bc
<< " since " << lcurr
<< " == " << lcc
<< std::endl
;
1798 //exp_n.push_back( getLength( curr, true ).eqNode( getLength( cc, true ) ) );
1799 Trace("strings-ff-debug") << "Explanation for " << lcurr
<< " is ";
1800 for( unsigned j
=0; j
<lexp
.size(); j
++ ) { Trace("strings-ff-debug") << lexp
[j
] << std::endl
; }
1801 Trace("strings-ff-debug") << "Explanation for " << lcc
<< " is ";
1802 for( unsigned j
=0; j
<lexp2
.size(); j
++ ) { Trace("strings-ff-debug") << lexp2
[j
] << std::endl
; }
1803 exp
.insert( exp
.end(), lexp
.begin(), lexp
.end() );
1804 exp
.insert( exp
.end(), lexp2
.begin(), lexp2
.end() );
1805 addToExplanation( lcurr
, lcc
, exp
);
1806 conc
= ac
.eqNode( bc
);
1816 if( !conc
.isNull() ){
1817 Trace("strings-ff-debug") << "Found inference : " << conc
<< " based on equality " << a
<< " == " << b
<< " " << r
<< " " << inf_type
<< std::endl
;
1818 addToExplanation( a
, b
, exp
);
1819 //explain why prefixes up to now were the same
1820 for( unsigned j
=0; j
<count
; j
++ ){
1821 Trace("strings-ff-debug") << "Add at " << d_flat_form_index
[a
][j
] << " " << d_flat_form_index
[b
][j
] << std::endl
;
1822 addToExplanation( a
[d_flat_form_index
[a
][j
]], b
[d_flat_form_index
[b
][j
]], exp
);
1824 //explain why other components up to now are empty
1825 for( unsigned t
=0; t
<2; t
++ ){
1826 Node c
= t
==0 ? a
: b
;
1828 if( inf_type
==3 || ( t
==1 && inf_type
==2 ) ){
1829 //explain all the empty components for F_EndpointEq, all for the short end for F_EndpointEmp
1830 jj
= r
==0 ? c
.getNumChildren() : -1;
1832 jj
= t
==0 ? d_flat_form_index
[a
][count
] : d_flat_form_index
[b
][count
];
1835 for( int j
=0; j
<jj
; j
++ ){
1836 if( areEqual( c
[j
], d_emptyString
) ){
1837 addToExplanation( c
[j
], d_emptyString
, exp
);
1841 for( int j
=(c
.getNumChildren()-1); j
>jj
; --j
){
1842 if( areEqual( c
[j
], d_emptyString
) ){
1843 addToExplanation( c
[j
], d_emptyString
, exp
);
1848 //notice that F_EndpointEmp is not typically applied, since strict prefix equality ( a.b = a ) where a,b non-empty
1849 // is conflicting by arithmetic len(a.b)=len(a)+len(b)!=len(a) when len(b)!=0.
1850 sendInference( exp
, conc
, inf_type
==0 ? "F_Const" : ( inf_type
==1 ? "F_Unify" : ( inf_type
==2 ? "F_EndpointEmp" : "F_EndpointEq" ) ) );
1858 }while( inelig
.size()<it
->second
.size() );
1860 for( unsigned i
=0; i
<it
->second
.size(); i
++ ){
1861 std::reverse( d_flat_form
[it
->second
[i
]].begin(), d_flat_form
[it
->second
[i
]].end() );
1862 std::reverse( d_flat_form_index
[it
->second
[i
]].begin(), d_flat_form_index
[it
->second
[i
]].end() );
1868 if( !hasProcessed() ){
1869 // simple extended func reduction
1870 Trace("strings-process") << "Check extended function reduction effort=1..." << std::endl
;
1871 checkExtfReductions( 1 );
1872 Trace("strings-process") << "Done check extended function reduction" << std::endl
;
1877 Node
TheoryStrings::checkCycles( Node eqc
, std::vector
< Node
>& curr
, std::vector
< Node
>& exp
){
1878 if( std::find( curr
.begin(), curr
.end(), eqc
)!=curr
.end() ){
1881 }else if( std::find( d_strings_eqc
.begin(), d_strings_eqc
.end(), eqc
)==d_strings_eqc
.end() ){
1882 curr
.push_back( eqc
);
1883 //look at all terms in this equivalence class
1884 eq::EqClassIterator eqc_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
1885 while( !eqc_i
.isFinished() ) {
1887 if( d_congruent
.find( n
)==d_congruent
.end() ){
1888 if( n
.getKind() == kind::STRING_CONCAT
){
1889 Trace("strings-cycle") << eqc
<< " check term : " << n
<< " in " << eqc
<< std::endl
;
1890 if( eqc
!=d_emptyString_r
){
1891 d_eqc
[eqc
].push_back( n
);
1893 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1894 Node nr
= getRepresentative( n
[i
] );
1895 if( eqc
==d_emptyString_r
){
1896 //for empty eqc, ensure all components are empty
1897 if( nr
!=d_emptyString_r
){
1898 std::vector
< Node
> exp
;
1899 exp
.push_back( n
.eqNode( d_emptyString
) );
1900 sendInference( exp
, n
[i
].eqNode( d_emptyString
), "I_CYCLE_E" );
1901 return Node::null();
1904 if( nr
!=d_emptyString_r
){
1905 d_flat_form
[n
].push_back( nr
);
1906 d_flat_form_index
[n
].push_back( i
);
1908 //for non-empty eqc, recurse and see if we find a loop
1909 Node ncy
= checkCycles( nr
, curr
, exp
);
1910 if( !ncy
.isNull() ){
1911 Trace("strings-cycle") << eqc
<< " cycle: " << ncy
<< " at " << n
<< "[" << i
<< "] : " << n
[i
] << std::endl
;
1912 addToExplanation( n
, eqc
, exp
);
1913 addToExplanation( nr
, n
[i
], exp
);
1915 //can infer all other components must be empty
1916 for( unsigned j
=0; j
<n
.getNumChildren(); j
++ ){
1917 //take first non-empty
1918 if( j
!=i
&& !areEqual( n
[j
], d_emptyString
) ){
1919 sendInference( exp
, n
[j
].eqNode( d_emptyString
), "I_CYCLE" );
1920 return Node::null();
1923 Trace("strings-error") << "Looping term should be congruent : " << n
<< " " << eqc
<< " " << ncy
<< std::endl
;
1924 //should find a non-empty component, otherwise would have been singular congruent (I_Norm_S)
1930 if( hasProcessed() ){
1931 return Node::null();
1941 //now we can add it to the list of equivalence classes
1942 d_strings_eqc
.push_back( eqc
);
1946 return Node::null();
1950 void TheoryStrings::checkNormalForms(){
1951 if( !options::stringEagerLen() ){
1952 for( unsigned i
=0; i
<d_strings_eqc
.size(); i
++ ) {
1953 Node eqc
= d_strings_eqc
[i
];
1954 eq::EqClassIterator eqc_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
1955 while( !eqc_i
.isFinished() ) {
1957 if( d_congruent
.find( n
)==d_congruent
.end() ){
1958 registerTerm( n
, 2 );
1964 if( !hasProcessed() ){
1965 Trace("strings-process") << "Normalize equivalence classes...." << std::endl
;
1966 //calculate normal forms for each equivalence class, possibly adding splitting lemmas
1967 d_normal_forms
.clear();
1968 d_normal_forms_exp
.clear();
1969 std::map
< Node
, Node
> nf_to_eqc
;
1970 std::map
< Node
, Node
> eqc_to_nf
;
1971 std::map
< Node
, Node
> eqc_to_exp
;
1972 for( unsigned i
=0; i
<d_strings_eqc
.size(); i
++ ) {
1973 Node eqc
= d_strings_eqc
[i
];
1974 Trace("strings-process-debug") << "- Verify normal forms are the same for " << eqc
<< std::endl
;
1975 normalizeEquivalenceClass( eqc
);
1976 Trace("strings-debug") << "Finished normalizing eqc..." << std::endl
;
1977 if( hasProcessed() ){
1980 Node nf_term
= mkConcat( d_normal_forms
[eqc
] );
1981 std::map
< Node
, Node
>::iterator itn
= nf_to_eqc
.find( nf_term
);
1982 if( itn
!=nf_to_eqc
.end() ){
1983 //two equivalence classes have same normal form, merge
1984 std::vector
< Node
> nf_exp
;
1985 nf_exp
.push_back( mkAnd( d_normal_forms_exp
[eqc
] ) );
1986 nf_exp
.push_back( eqc_to_exp
[itn
->second
] );
1987 Node eq
= d_normal_forms_base
[eqc
].eqNode( d_normal_forms_base
[itn
->second
] );
1988 sendInference( nf_exp
, eq
, "Normal_Form" );
1990 nf_to_eqc
[nf_term
] = eqc
;
1991 eqc_to_nf
[eqc
] = nf_term
;
1992 eqc_to_exp
[eqc
] = mkAnd( d_normal_forms_exp
[eqc
] );
1995 Trace("strings-process-debug") << "Done verifying normal forms are the same for " << eqc
<< std::endl
;
1997 if( !hasProcessed() ){
1998 if(Trace
.isOn("strings-nf")) {
1999 Trace("strings-nf") << "**** Normal forms are : " << std::endl
;
2000 for( std::map
< Node
, Node
>::iterator it
= eqc_to_exp
.begin(); it
!= eqc_to_exp
.end(); ++it
){
2001 Trace("strings-nf") << " N[" << it
->first
<< "] (base " << d_normal_forms_base
[it
->first
] << ") = " << eqc_to_nf
[it
->first
] << std::endl
;
2002 Trace("strings-nf") << " exp: " << it
->second
<< std::endl
;
2004 Trace("strings-nf") << std::endl
;
2007 Trace("strings-process-debug") << "Done check extended functions re-eval, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
2008 if( !hasProcessed() ){
2009 if( !options::stringEagerLen() ){
2011 if( hasProcessed() ){
2015 //process disequalities between equivalence classes
2017 Trace("strings-process-debug") << "Done check disequalities, addedFact = " << !d_pending
.empty() << " " << !d_lemma_cache
.empty() << ", d_conflict = " << d_conflict
<< std::endl
;
2020 Trace("strings-solve") << "Finished check normal forms, #lemmas = " << d_lemma_cache
.size() << ", conflict = " << d_conflict
<< std::endl
;
2024 //compute d_normal_forms_(base,exp,exp_depend)[eqc]
2025 void TheoryStrings::normalizeEquivalenceClass( Node eqc
) {
2026 Trace("strings-process-debug") << "Process equivalence class " << eqc
<< std::endl
;
2027 if( areEqual( eqc
, d_emptyString
) ) {
2028 #ifdef CVC4_ASSERTIONS
2029 for( unsigned j
=0; j
<d_eqc
[eqc
].size(); j
++ ){
2030 Node n
= d_eqc
[eqc
][j
];
2031 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
2032 Assert( areEqual( n
[i
], d_emptyString
) );
2037 Trace("strings-process-debug") << "Return process equivalence class " << eqc
<< " : empty." << std::endl
;
2038 d_normal_forms_base
[eqc
] = d_emptyString
;
2039 d_normal_forms
[eqc
].clear();
2040 d_normal_forms_exp
[eqc
].clear();
2042 Assert( d_normal_forms
.find(eqc
)==d_normal_forms
.end() );
2043 //phi => t = s1 * ... * sn
2044 // normal form for each non-variable term in this eqc (s1...sn)
2045 std::vector
< std::vector
< Node
> > normal_forms
;
2046 // explanation for each normal form (phi)
2047 std::vector
< std::vector
< Node
> > normal_forms_exp
;
2048 // dependency information
2049 std::vector
< std::map
< Node
, std::map
< bool, int > > > normal_forms_exp_depend
;
2050 // record terms for each normal form (t)
2051 std::vector
< Node
> normal_form_src
;
2053 getNormalForms(eqc
, normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
);
2054 if( hasProcessed() ){
2057 // process the normal forms
2058 processNEqc( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
);
2059 if( hasProcessed() ){
2062 //debugPrintNormalForms( "strings-solve", eqc, normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend );
2064 //construct the normal form
2065 Assert( !normal_forms
.empty() );
2068 std::vector
< Node
>::iterator itn
= std::find( normal_form_src
.begin(), normal_form_src
.end(), eqc
);
2069 if( itn
!=normal_form_src
.end() ){
2070 nf_index
= itn
- normal_form_src
.begin();
2071 Trace("strings-solve-debug2") << "take normal form " << nf_index
<< std::endl
;
2072 Assert( normal_form_src
[nf_index
]==eqc
);
2074 //just take the first normal form
2075 Trace("strings-solve-debug2") << "take the first normal form" << std::endl
;
2077 d_normal_forms
[eqc
].insert( d_normal_forms
[eqc
].end(), normal_forms
[nf_index
].begin(), normal_forms
[nf_index
].end() );
2078 d_normal_forms_exp
[eqc
].insert( d_normal_forms_exp
[eqc
].end(), normal_forms_exp
[nf_index
].begin(), normal_forms_exp
[nf_index
].end() );
2079 Trace("strings-solve-debug2") << "take normal form ... done" << std::endl
;
2080 d_normal_forms_base
[eqc
] = normal_form_src
[nf_index
];
2081 //track dependencies
2082 for( unsigned i
=0; i
<normal_forms_exp
[nf_index
].size(); i
++ ){
2083 Node exp
= normal_forms_exp
[nf_index
][i
];
2084 for( unsigned r
=0; r
<2; r
++ ){
2085 d_normal_forms_exp_depend
[eqc
][exp
][r
==0] = normal_forms_exp_depend
[nf_index
][exp
][r
==0];
2088 Trace("strings-process-debug") << "Return process equivalence class " << eqc
<< " : returned, size = " << d_normal_forms
[eqc
].size() << std::endl
;
2092 void TheoryStrings::getNormalForms( Node
&eqc
, std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
2093 std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
) {
2094 //constant for equivalence class
2095 Node eqc_non_c
= eqc
;
2096 Trace("strings-process-debug") << "Get normal forms " << eqc
<< std::endl
;
2097 eq::EqClassIterator eqc_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
2098 while( !eqc_i
.isFinished() ){
2100 if( d_congruent
.find( n
)==d_congruent
.end() ){
2101 if( n
.getKind() == kind::CONST_STRING
|| n
.getKind() == kind::STRING_CONCAT
){
2102 Trace("strings-process-debug") << "Get Normal Form : Process term " << n
<< " in eqc " << eqc
<< std::endl
;
2103 std::vector
< Node
> nf_n
;
2104 std::vector
< Node
> nf_exp_n
;
2105 std::map
< Node
, std::map
< bool, int > > nf_exp_depend_n
;
2106 if( n
.getKind()==kind::CONST_STRING
){
2107 if( n
!=d_emptyString
) {
2108 nf_n
.push_back( n
);
2110 }else if( n
.getKind()==kind::STRING_CONCAT
){
2111 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ) {
2112 Node nr
= d_equalityEngine
.getRepresentative( n
[i
] );
2113 Trace("strings-process-debug") << "Normalizing subterm " << n
[i
] << " = " << nr
<< std::endl
;
2114 Assert( d_normal_forms
.find( nr
)!=d_normal_forms
.end() );
2115 unsigned orig_size
= nf_n
.size();
2116 unsigned add_size
= d_normal_forms
[nr
].size();
2117 //if not the empty string, add to current normal form
2118 if( !d_normal_forms
[nr
].empty() ){
2119 for( unsigned r
=0; r
<d_normal_forms
[nr
].size(); r
++ ) {
2120 if( Trace
.isOn("strings-error") ) {
2121 if( d_normal_forms
[nr
][r
].getKind()==kind::STRING_CONCAT
){
2122 Trace("strings-error") << "Strings::Error: From eqc = " << eqc
<< ", " << n
<< " index " << i
<< ", bad normal form : ";
2123 for( unsigned rr
=0; rr
<d_normal_forms
[nr
].size(); rr
++ ) {
2124 Trace("strings-error") << d_normal_forms
[nr
][rr
] << " ";
2126 Trace("strings-error") << std::endl
;
2129 Assert( d_normal_forms
[nr
][r
].getKind()!=kind::STRING_CONCAT
);
2131 nf_n
.insert( nf_n
.end(), d_normal_forms
[nr
].begin(), d_normal_forms
[nr
].end() );
2134 for( unsigned j
=0; j
<d_normal_forms_exp
[nr
].size(); j
++ ){
2135 Node exp
= d_normal_forms_exp
[nr
][j
];
2136 nf_exp_n
.push_back( exp
);
2138 for( unsigned k
=0; k
<2; k
++ ){
2139 int prev_dep
= d_normal_forms_exp_depend
[nr
][exp
][k
==1];
2141 nf_exp_depend_n
[exp
][false] = orig_size
+ prev_dep
;
2143 //store forward index (converted back to reverse index below)
2144 nf_exp_depend_n
[exp
][true] = orig_size
+ ( add_size
- prev_dep
);
2148 if( d_normal_forms_base
[nr
]!=n
[i
] ){
2149 Assert( d_normal_forms_base
.find( nr
)!=d_normal_forms_base
.end() );
2150 Node eq
= n
[i
].eqNode( d_normal_forms_base
[nr
] );
2151 nf_exp_n
.push_back( eq
);
2153 nf_exp_depend_n
[eq
][false] = orig_size
;
2154 nf_exp_depend_n
[eq
][true] = orig_size
+ add_size
;
2157 //convert forward indices to reverse indices
2158 int total_size
= nf_n
.size();
2159 for( std::map
< Node
, std::map
< bool, int > >::iterator it
= nf_exp_depend_n
.begin(); it
!= nf_exp_depend_n
.end(); ++it
){
2160 it
->second
[true] = total_size
- it
->second
[true];
2161 Assert( it
->second
[true]>=0 );
2164 //if not equal to self
2165 if( nf_n
.size()>1 || ( nf_n
.size()==1 && nf_n
[0].getKind()==kind::CONST_STRING
) ){
2166 if( nf_n
.size()>1 ) {
2167 for( unsigned i
=0; i
<nf_n
.size(); i
++ ){
2168 if( Trace
.isOn("strings-error") ){
2169 Trace("strings-error") << "Cycle for normal form ";
2170 printConcat(nf_n
,"strings-error");
2171 Trace("strings-error") << "..." << nf_n
[i
] << std::endl
;
2173 Assert( !areEqual( nf_n
[i
], n
) );
2176 normal_forms
.push_back(nf_n
);
2177 normal_form_src
.push_back(n
);
2178 normal_forms_exp
.push_back(nf_exp_n
);
2179 normal_forms_exp_depend
.push_back(nf_exp_depend_n
);
2181 //this was redundant: combination of self + empty string(s)
2182 Node nn
= nf_n
.size()==0 ? d_emptyString
: nf_n
[0];
2183 Assert( areEqual( nn
, eqc
) );
2192 if( normal_forms
.empty() ) {
2193 Trace("strings-solve-debug2") << "construct the normal form" << std::endl
;
2194 //do not choose a concat here use "eqc_non_c" (in this case they have non-trivial explanation why they normalize to self)
2195 std::vector
< Node
> eqc_non_c_nf
;
2196 getConcatVec( eqc_non_c
, eqc_non_c_nf
);
2197 normal_forms
.push_back( eqc_non_c_nf
);
2198 normal_form_src
.push_back( eqc_non_c
);
2199 normal_forms_exp
.push_back( std::vector
< Node
>() );
2200 normal_forms_exp_depend
.push_back( std::map
< Node
, std::map
< bool, int > >() );
2202 if(Trace
.isOn("strings-solve")) {
2203 Trace("strings-solve") << "--- Normal forms for equivlance class " << eqc
<< " : " << std::endl
;
2204 for( unsigned i
=0; i
<normal_forms
.size(); i
++ ) {
2205 Trace("strings-solve") << "#" << i
<< " (from " << normal_form_src
[i
] << ") : ";
2206 for( unsigned j
=0; j
<normal_forms
[i
].size(); j
++ ) {
2208 Trace("strings-solve") << ", ";
2210 Trace("strings-solve") << normal_forms
[i
][j
];
2212 Trace("strings-solve") << std::endl
;
2213 Trace("strings-solve") << " Explanation is : ";
2214 if(normal_forms_exp
[i
].size() == 0) {
2215 Trace("strings-solve") << "NONE";
2217 for( unsigned j
=0; j
<normal_forms_exp
[i
].size(); j
++ ) {
2219 Trace("strings-solve") << " AND ";
2221 Trace("strings-solve") << normal_forms_exp
[i
][j
];
2223 Trace("strings-solve") << std::endl
;
2224 Trace("strings-solve") << "WITH DEPENDENCIES : " << std::endl
;
2225 for( unsigned j
=0; j
<normal_forms_exp
[i
].size(); j
++ ) {
2226 Trace("strings-solve") << " " << normal_forms_exp
[i
][j
] << " -> ";
2227 Trace("strings-solve") << normal_forms_exp_depend
[i
][normal_forms_exp
[i
][j
]][false] << ",";
2228 Trace("strings-solve") << normal_forms_exp_depend
[i
][normal_forms_exp
[i
][j
]][true] << std::endl
;
2231 Trace("strings-solve") << std::endl
;
2235 Trace("strings-solve") << "--- Single normal form for equivalence class " << eqc
<< std::endl
;
2238 //if equivalence class is constant, approximate as containment, infer conflicts
2239 Node c
= getConstantEqc( eqc
);
2241 Trace("strings-solve") << "Eqc is constant " << c
<< std::endl
;
2242 for( unsigned i
=0; i
<normal_forms
.size(); i
++ ) {
2244 if( !TheoryStringsRewriter::canConstantContainList( c
, normal_forms
[i
], firstc
, lastc
) ){
2245 Node n
= normal_form_src
[i
];
2247 Trace("strings-solve") << "Normal form for " << n
<< " cannot be contained in constant " << c
<< std::endl
;
2248 //conflict, explanation is n = base ^ base = c ^ relevant porition of ( n = N[n] )
2249 std::vector
< Node
> exp
;
2250 Assert( d_eqc_to_const_base
.find( eqc
)!=d_eqc_to_const_base
.end() );
2251 addToExplanation( n
, d_eqc_to_const_base
[eqc
], exp
);
2252 Assert( d_eqc_to_const_exp
.find( eqc
)!=d_eqc_to_const_exp
.end() );
2253 if( !d_eqc_to_const_exp
[eqc
].isNull() ){
2254 exp
.push_back( d_eqc_to_const_exp
[eqc
] );
2256 //TODO: this can be minimized based on firstc/lastc, normal_forms_exp_depend
2257 exp
.insert( exp
.end(), normal_forms_exp
[i
].begin(), normal_forms_exp
[i
].end() );
2258 Node conc
= d_false
;
2259 sendInference( exp
, conc
, "N_NCTN" );
2266 void TheoryStrings::getExplanationVectorForPrefix( std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
,
2267 unsigned i
, int index
, bool isRev
, std::vector
< Node
>& curr_exp
) {
2268 if( index
==-1 || !options::stringMinPrefixExplain() ){
2269 curr_exp
.insert(curr_exp
.end(), normal_forms_exp
[i
].begin(), normal_forms_exp
[i
].end() );
2271 for( unsigned k
=0; k
<normal_forms_exp
[i
].size(); k
++ ){
2272 Node exp
= normal_forms_exp
[i
][k
];
2273 int dep
= normal_forms_exp_depend
[i
][exp
][isRev
];
2275 curr_exp
.push_back( exp
);
2276 Trace("strings-explain-prefix-debug") << " include : " << exp
<< std::endl
;
2278 Trace("strings-explain-prefix-debug") << " exclude : " << exp
<< std::endl
;
2284 void TheoryStrings::getExplanationVectorForPrefixEq( std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
2285 std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
,
2286 unsigned i
, unsigned j
, int index_i
, int index_j
, bool isRev
, std::vector
< Node
>& curr_exp
) {
2287 Trace("strings-explain-prefix") << "Get explanation for prefix " << index_i
<< ", " << index_j
<< " of normal forms " << i
<< " and " << j
<< ", reverse = " << isRev
<< std::endl
;
2288 for( unsigned r
=0; r
<2; r
++ ){
2289 getExplanationVectorForPrefix( normal_forms_exp
, normal_forms_exp_depend
, r
==0 ? i
: j
, r
==0 ? index_i
: index_j
, isRev
, curr_exp
);
2291 Trace("strings-explain-prefix") << "Included " << curr_exp
.size() << " / " << ( normal_forms_exp
[i
].size() + normal_forms_exp
[j
].size() ) << std::endl
;
2292 addToExplanation( normal_form_src
[i
], normal_form_src
[j
], curr_exp
);
2296 void TheoryStrings::processNEqc( std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
2297 std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
){
2298 //the possible inferences
2299 std::vector
< InferInfo
> pinfer
;
2300 // loop over all pairs
2301 for(unsigned i
=0; i
<normal_forms
.size()-1; i
++) {
2302 //unify each normalform[j] with normal_forms[i]
2303 for(unsigned j
=i
+1; j
<normal_forms
.size(); j
++ ) {
2304 //ensure that normal_forms[i] and normal_forms[j] are the same modulo equality, add to pinfer if not
2305 Trace("strings-solve") << "Strings: Process normal form #" << i
<< " against #" << j
<< "..." << std::endl
;
2306 if( isNormalFormPair( normal_form_src
[i
], normal_form_src
[j
] ) ) {
2307 Trace("strings-solve") << "Strings: Already cached." << std::endl
;
2309 //process the reverse direction first (check for easy conflicts and inferences)
2310 unsigned rindex
= 0;
2311 processReverseNEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, rindex
, 0, pinfer
);
2312 if( hasProcessed() ){
2315 //AJR: for less aggressive endpoint inference
2319 processSimpleNEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, index
, false, rindex
, pinfer
);
2320 if( hasProcessed() ){
2326 if( !pinfer
.empty() ){
2327 //now, determine which of the possible inferences we want to add
2329 Trace("strings-solve") << "Possible inferences (" << pinfer
.size() << ") : " << std::endl
;
2330 unsigned min_id
= 9;
2331 for( unsigned i
=0; i
<pinfer
.size(); i
++ ){
2332 Trace("strings-solve") << "From " << pinfer
[i
].d_i
<< " / " << pinfer
[i
].d_j
<< " (rev=" << pinfer
[i
].d_rev
<< ") : ";
2333 Trace("strings-solve") << pinfer
[i
].d_conc
<< " by " << pinfer
[i
].getId() << std::endl
;
2334 if( use_index
==-1 || pinfer
[i
].d_id
<min_id
){
2335 min_id
= pinfer
[i
].d_id
;
2339 //send the inference
2340 sendInference( pinfer
[use_index
].d_ant
, pinfer
[use_index
].d_antn
, pinfer
[use_index
].d_conc
, pinfer
[use_index
].getId(), pinfer
[use_index
].sendAsLemma() );
2341 for( unsigned i
=0; i
<pinfer
[use_index
].d_non_emp_vars
.size(); i
++ ){
2342 registerNonEmptySkolem( pinfer
[use_index
].d_non_emp_vars
[i
] );
2347 bool TheoryStrings::InferInfo::sendAsLemma() {
2351 void TheoryStrings::processReverseNEq( std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
2352 std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
,
2353 unsigned i
, unsigned j
, unsigned& index
, unsigned rproc
, std::vector
< InferInfo
>& pinfer
) {
2354 //reverse normal form of i, j
2355 std::reverse( normal_forms
[i
].begin(), normal_forms
[i
].end() );
2356 std::reverse( normal_forms
[j
].begin(), normal_forms
[j
].end() );
2358 processSimpleNEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, index
, true, rproc
, pinfer
);
2360 //reverse normal form of i, j
2361 std::reverse( normal_forms
[i
].begin(), normal_forms
[i
].end() );
2362 std::reverse( normal_forms
[j
].begin(), normal_forms
[j
].end() );
2365 //rproc is the # is the size of suffix that is identical
2366 void TheoryStrings::processSimpleNEq( std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
2367 std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
,
2368 unsigned i
, unsigned j
, unsigned& index
, bool isRev
, unsigned rproc
, std::vector
< InferInfo
>& pinfer
) {
2372 //if we are at the end
2373 if( index
==(normal_forms
[i
].size()-rproc
) || index
==(normal_forms
[j
].size()-rproc
) ){
2374 if( index
==(normal_forms
[i
].size()-rproc
) && index
==(normal_forms
[j
].size()-rproc
) ){
2377 //the remainder must be empty
2378 unsigned k
= index
==(normal_forms
[i
].size()-rproc
) ? j
: i
;
2379 unsigned index_k
= index
;
2380 //Node eq_exp = mkAnd( curr_exp );
2381 std::vector
< Node
> curr_exp
;
2382 getExplanationVectorForPrefixEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, -1, -1, isRev
, curr_exp
);
2383 while( !d_conflict
&& index_k
<(normal_forms
[k
].size()-rproc
) ){
2384 //can infer that this string must be empty
2385 Node eq
= normal_forms
[k
][index_k
].eqNode( d_emptyString
);
2386 //Trace("strings-lemma") << "Strings: Infer " << eq << " from " << eq_exp << std::endl;
2387 Assert( !areEqual( d_emptyString
, normal_forms
[k
][index_k
] ) );
2388 sendInference( curr_exp
, eq
, "N_EndpointEmp" );
2393 Trace("strings-solve-debug") << "Process " << normal_forms
[i
][index
] << " ... " << normal_forms
[j
][index
] << std::endl
;
2394 if( normal_forms
[i
][index
]==normal_forms
[j
][index
] ){
2395 Trace("strings-solve-debug") << "Simple Case 1 : strings are equal" << std::endl
;
2399 Assert( !areEqual(normal_forms
[i
][index
], normal_forms
[j
][index
]) );
2400 std::vector
< Node
> temp_exp
;
2401 Node length_term_i
= getLength( normal_forms
[i
][index
], temp_exp
);
2402 Node length_term_j
= getLength( normal_forms
[j
][index
], temp_exp
);
2403 //check length(normal_forms[i][index]) == length(normal_forms[j][index])
2404 if( areEqual( length_term_i
, length_term_j
) ){
2405 Trace("strings-solve-debug") << "Simple Case 2 : string lengths are equal" << std::endl
;
2406 Node eq
= normal_forms
[i
][index
].eqNode( normal_forms
[j
][index
] );
2407 //eq = Rewriter::rewrite( eq );
2408 Node length_eq
= length_term_i
.eqNode( length_term_j
);
2409 //temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() );
2410 getExplanationVectorForPrefixEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, index
, index
, isRev
, temp_exp
);
2411 temp_exp
.push_back(length_eq
);
2412 sendInference( temp_exp
, eq
, "N_Unify" );
2414 }else if( ( normal_forms
[i
][index
].getKind()!=kind::CONST_STRING
&& index
==normal_forms
[i
].size()-rproc
-1 ) ||
2415 ( normal_forms
[j
][index
].getKind()!=kind::CONST_STRING
&& index
==normal_forms
[j
].size()-rproc
-1 ) ){
2416 Trace("strings-solve-debug") << "Simple Case 3 : at endpoint" << std::endl
;
2418 std::vector
< Node
> antec
;
2419 //antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
2420 getExplanationVectorForPrefixEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, -1, -1, isRev
, antec
);
2421 std::vector
< Node
> eqn
;
2422 for( unsigned r
=0; r
<2; r
++ ) {
2423 int index_k
= index
;
2424 int k
= r
==0 ? i
: j
;
2425 std::vector
< Node
> eqnc
;
2426 for( unsigned index_l
=index_k
; index_l
<(normal_forms
[k
].size()-rproc
); index_l
++ ) {
2428 eqnc
.insert(eqnc
.begin(), normal_forms
[k
][index_l
] );
2430 eqnc
.push_back( normal_forms
[k
][index_l
] );
2433 eqn
.push_back( mkConcat( eqnc
) );
2435 if( !areEqual( eqn
[0], eqn
[1] ) ){
2436 conc
= eqn
[0].eqNode( eqn
[1] );
2437 sendInference( antec
, conc
, "N_EndpointEq", true );
2440 Assert( normal_forms
[i
].size()==normal_forms
[j
].size() );
2441 index
= normal_forms
[i
].size()-rproc
;
2443 }else if( normal_forms
[i
][index
].isConst() && normal_forms
[j
][index
].isConst() ){
2444 Node const_str
= normal_forms
[i
][index
];
2445 Node other_str
= normal_forms
[j
][index
];
2446 Trace("strings-solve-debug") << "Simple Case 3 : Const Split : " << const_str
<< " vs " << other_str
<< " at index " << index
<< ", isRev = " << isRev
<< std::endl
;
2447 unsigned len_short
= const_str
.getConst
<String
>().size() <= other_str
.getConst
<String
>().size() ? const_str
.getConst
<String
>().size() : other_str
.getConst
<String
>().size();
2448 bool isSameFix
= isRev
? const_str
.getConst
<String
>().rstrncmp(other_str
.getConst
<String
>(), len_short
): const_str
.getConst
<String
>().strncmp(other_str
.getConst
<String
>(), len_short
);
2450 //same prefix/suffix
2451 //k is the index of the string that is shorter
2452 int k
= const_str
.getConst
<String
>().size()<other_str
.getConst
<String
>().size() ? i
: j
;
2453 int l
= const_str
.getConst
<String
>().size()<other_str
.getConst
<String
>().size() ? j
: i
;
2454 //update the nf exp dependencies
2455 //notice this is not critical for soundness: not doing the below incrementing will only lead to overapproximating when antecedants are required in explanations
2456 for( std::map
< Node
, std::map
< bool, int > >::iterator itnd
= normal_forms_exp_depend
[l
].begin(); itnd
!= normal_forms_exp_depend
[l
].end(); ++itnd
){
2457 for( std::map
< bool, int >::iterator itnd2
= itnd
->second
.begin(); itnd2
!= itnd
->second
.end(); ++itnd2
){
2458 //see if this can be incremented: it can if it is not relevant to the current index
2459 Assert( itnd2
->second
>=0 && itnd2
->second
<=(int)normal_forms
[l
].size() );
2460 bool increment
= itnd2
->first
==isRev
? itnd2
->second
>(int)index
: ( (int)normal_forms
[l
].size()-1-itnd2
->second
)<(int)index
;
2462 normal_forms_exp_depend
[l
][itnd
->first
][itnd2
->first
] = itnd2
->second
+ 1;
2467 int new_len
= normal_forms
[l
][index
].getConst
<String
>().size() - len_short
;
2468 Node remainderStr
= NodeManager::currentNM()->mkConst( normal_forms
[l
][index
].getConst
<String
>().substr(0, new_len
) );
2469 Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms
[l
][index
] << " into " << normal_forms
[k
][index
] << ", " << remainderStr
<< std::endl
;
2470 normal_forms
[l
].insert( normal_forms
[l
].begin()+index
+ 1, remainderStr
);
2472 Node remainderStr
= NodeManager::currentNM()->mkConst(normal_forms
[l
][index
].getConst
<String
>().substr(len_short
));
2473 Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms
[l
][index
] << " into " << normal_forms
[k
][index
] << ", " << remainderStr
<< std::endl
;
2474 normal_forms
[l
].insert( normal_forms
[l
].begin()+index
+ 1, remainderStr
);
2476 normal_forms
[l
][index
] = normal_forms
[k
][index
];
2481 std::vector
< Node
> antec
;
2482 getExplanationVectorForPrefixEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, index
, index
, isRev
, antec
);
2483 sendInference( antec
, d_false
, "N_Const", true );
2487 //construct the candidate inference "info"
2493 bool info_valid
= false;
2494 Assert( index
<normal_forms
[i
].size()-rproc
&& index
<normal_forms
[j
].size()-rproc
);
2495 std::vector
< Node
> lexp
;
2496 Node length_term_i
= getLength( normal_forms
[i
][index
], lexp
);
2497 Node length_term_j
= getLength( normal_forms
[j
][index
], lexp
);
2498 //check length(normal_forms[i][index]) == length(normal_forms[j][index])
2499 if( !areDisequal(length_term_i
, length_term_j
) && !areEqual(length_term_i
, length_term_j
) &&
2500 normal_forms
[i
][index
].getKind()!=kind::CONST_STRING
&& normal_forms
[j
][index
].getKind()!=kind::CONST_STRING
){ //AJR: remove the latter 2 conditions?
2501 Trace("strings-solve-debug") << "Non-simple Case 1 : string lengths neither equal nor disequal" << std::endl
;
2502 //try to make the lengths equal via splitting on demand
2503 Node length_eq
= NodeManager::currentNM()->mkNode( kind::EQUAL
, length_term_i
, length_term_j
);
2504 length_eq
= Rewriter::rewrite( length_eq
);
2506 info
.d_conc
= NodeManager::currentNM()->mkNode( kind::OR
, length_eq
, length_eq
.negate() );
2507 info
.d_pending_phase
[ length_eq
] = true;
2511 Assert( !areEqual( normal_forms[i][index], normal_forms[j][index] ) );
2512 if( !areDisequal( normal_forms[i][index], normal_forms[j][index] ) ){
2513 Node eq = normal_forms[i][index].eqNode( normal_forms[j][index] );
2514 eq = Rewriter::rewrite( eq );
2515 d_pending_req_phase[ eq ] = true;
2516 Node conc = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
2517 sendInference( d_empty_vec, conc, "Unify-Split", true );
2520 }else if( !isRev
){ //FIXME
2521 Trace("strings-solve-debug") << "Non-simple Case 2 : must compare strings" << std::endl
;
2524 if( detectLoop(normal_forms
, i
, j
, index
, loop_in_i
, loop_in_j
) ){
2525 //FIXME: do for isRev
2526 getExplanationVectorForPrefixEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, -1, -1, false, info
.d_ant
);
2528 if( processLoop( normal_forms
, normal_form_src
, i
, j
, loop_in_i
!=-1 ? i
: j
, loop_in_i
!=-1 ? j
: i
, loop_in_i
!=-1 ? loop_in_i
: loop_in_j
, index
, info
) ){
2533 Trace("strings-solve-debug") << "No loops detected." << std::endl
;
2534 if( normal_forms
[i
][index
].getKind() == kind::CONST_STRING
|| normal_forms
[j
][index
].getKind() == kind::CONST_STRING
){
2535 unsigned const_k
= normal_forms
[i
][index
].getKind() == kind::CONST_STRING
? i
: j
;
2536 unsigned nconst_k
= normal_forms
[i
][index
].getKind() == kind::CONST_STRING
? j
: i
;
2537 Node other_str
= normal_forms
[nconst_k
][index
];
2538 Assert( other_str
.getKind()!=kind::CONST_STRING
, "Other string is not constant." );
2539 Assert( other_str
.getKind()!=kind::STRING_CONCAT
, "Other string is not CONCAT." );
2540 if( !d_equalityEngine
.areDisequal(other_str
, d_emptyString
, true) ){
2541 Node eq
= other_str
.eqNode( d_emptyString
);
2543 info
.d_conc
= NodeManager::currentNM()->mkNode( kind::OR
, eq
, eq
.negate() );
2546 //sendSplit( other_str, d_emptyString, "Len-Split(CST)" );
2548 Node xnz
= other_str
.eqNode( d_emptyString
).negate();
2549 unsigned index_nc_k
= index
+1;
2550 //Node next_const_str = TheoryStringsRewriter::collectConstantStringAt( normal_forms[nconst_k], index_nc_k, false );
2551 unsigned start_index_nc_k
= index
+1;
2552 Node next_const_str
= TheoryStringsRewriter::getNextConstantAt( normal_forms
[nconst_k
], start_index_nc_k
, index_nc_k
, false );
2553 if( !next_const_str
.isNull() ) {
2554 unsigned index_c_k
= index
;
2555 Node const_str
= TheoryStringsRewriter::collectConstantStringAt( normal_forms
[const_k
], index_c_k
, false );
2556 Assert( !const_str
.isNull() );
2557 CVC4::String stra
= const_str
.getConst
<String
>();
2558 CVC4::String strb
= next_const_str
.getConst
<String
>();
2559 //FIXME : make this for isRev
2560 //since non-empty, we start with charecter #1
2561 CVC4::String stra1
= stra
.substr(1);
2562 Trace("strings-csp-debug") << "Compute overlap : " << const_str
<< " " << next_const_str
<< std::endl
;
2563 size_t p
= stra
.size() - stra1
.overlap(strb
);
2564 size_t p2
= stra1
.find(strb
);
2565 p
= p2
==std::string::npos
? p
: ( p
>p2
+1? p2
+1 : p
);
2567 if( start_index_nc_k
==index
+1 ){
2568 info
.d_ant
.push_back( xnz
);
2569 getExplanationVectorForPrefixEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
,
2570 const_k
, nconst_k
, index_c_k
, index_nc_k
, false, info
.d_ant
);
2571 Node prea
= p
==stra
.size()? const_str
: NodeManager::currentNM()->mkConst( stra
.substr(0, p
) );
2572 Node sk
= mkSkolemCached( other_str
, prea
, sk_id_c_spt
, "c_spt" );
2573 Trace("strings-csp") << "Const Split: " << prea
<< " is removed from " << stra
<< " due to " << strb
<< ", p=" << p
<< std::endl
;
2575 info
.d_conc
= other_str
.eqNode( mkConcat(prea
, sk
) );
2580 else if( options::stringLenPropCsp() ){
2581 //propagate length constraint
2582 std::vector< Node > cc;
2583 for( unsigned i=index; i<start_index_nc_k; i++ ){
2584 cc.push_back( normal_forms[nconst_k][i] );
2586 Node lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, mkConcat( cc ) );
2587 conc = NodeManager::currentNM()->mkNode( kind::GEQ, lt, NodeManager::currentNM()->mkConst( Rational(p) ) );
2588 sendInference( ant, conc, "S-Split(CSP-P)-lprop", true );
2594 info
.d_ant
.push_back( xnz
);
2595 Node const_str
= normal_forms
[const_k
][index
];
2596 getExplanationVectorForPrefixEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, index
, index
, false, info
.d_ant
);
2597 CVC4::String stra
= const_str
.getConst
<String
>();
2598 if( options::stringBinaryCsp() && stra
.size()>3 ){
2599 //split string in half
2600 Node c_firstHalf
= NodeManager::currentNM()->mkConst( stra
.substr(0, stra
.size()/2 ) );
2601 Node sk
= mkSkolemCached( other_str
, c_firstHalf
, sk_id_vc_bin_spt
, "c_spt" );
2602 Trace("strings-csp") << "Const Split: " << c_firstHalf
<< " is removed from " << const_str
<< " (binary) " << std::endl
;
2603 info
.d_conc
= NodeManager::currentNM()->mkNode( kind::OR
, other_str
.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, c_firstHalf
, sk
) ),
2604 NodeManager::currentNM()->mkNode( kind::AND
,
2605 sk
.eqNode( d_emptyString
).negate(),
2606 c_firstHalf
.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, other_str
, sk
) ) ));
2611 Node firstChar
= stra
.size() == 1 ? const_str
: NodeManager::currentNM()->mkConst( stra
.substr(0, 1) );
2612 Node sk
= mkSkolemCached( other_str
, firstChar
, sk_id_vc_spt
, "c_spt" );
2613 Trace("strings-csp") << "Const Split: " << firstChar
<< " is removed from " << const_str
<< " (serial) " << std::endl
;
2614 info
.d_conc
= other_str
.eqNode( mkConcat(firstChar
, sk
) );
2621 getExplanationVectorForPrefixEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, index
, index
, false, info
.d_ant
);
2623 for(unsigned xory
=0; xory
<2; xory
++) {
2624 Node x
= xory
==0 ? normal_forms
[i
][index
] : normal_forms
[j
][index
];
2625 Node xgtz
= x
.eqNode( d_emptyString
).negate();
2626 if( d_equalityEngine
.areDisequal( x
, d_emptyString
, true ) ) {
2627 info
.d_ant
.push_back( xgtz
);
2629 info
.d_antn
.push_back( xgtz
);
2632 Node sk
= mkSkolemCached( normal_forms
[i
][index
], normal_forms
[j
][index
], sk_id_v_spt
, "v_spt" );
2633 //must add length requirement
2634 info
.d_non_emp_vars
.push_back( sk
);
2635 Node eq1
= normal_forms
[i
][index
].eqNode( mkConcat(normal_forms
[j
][index
], sk
) );
2636 Node eq2
= normal_forms
[j
][index
].eqNode( mkConcat(normal_forms
[i
][index
], sk
) );
2637 int lentTestSuccess
= -1;
2639 if( options::stringCheckEntailLen() ){
2641 for( unsigned e
=0; e
<2; e
++ ){
2642 Node lt1
= e
==0 ? length_term_i
: length_term_j
;
2643 Node lt2
= e
==0 ? length_term_j
: length_term_i
;
2644 Node ent_lit
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT
, lt1
, lt2
) );
2645 std::pair
<bool, Node
> et
= d_valuation
.entailmentCheck(THEORY_OF_TYPE_BASED
, ent_lit
);
2647 Trace("strings-entail") << "Strings entailment : " << ent_lit
<< " is entailed in the current context." << std::endl
;
2648 Trace("strings-entail") << " explanation was : " << et
.second
<< std::endl
;
2649 lentTestSuccess
= e
;
2650 lentTestExp
= et
.second
;
2655 if( lentTestSuccess
!=-1 ){
2656 info
.d_antn
.push_back( lentTestExp
);
2657 info
.d_conc
= lentTestSuccess
==0 ? eq1
: eq2
;
2661 Node ldeq
= NodeManager::currentNM()->mkNode( kind::EQUAL
, length_term_i
, length_term_j
).negate();
2662 if( d_equalityEngine
.areDisequal( length_term_i
, length_term_j
, true ) ){
2663 info
.d_ant
.push_back( ldeq
);
2665 info
.d_antn
.push_back(ldeq
);
2668 info
.d_conc
= Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::OR
, eq1
, eq2
));
2676 pinfer
.push_back( info
);
2688 bool TheoryStrings::detectLoop( std::vector
< std::vector
< Node
> > &normal_forms
, int i
, int j
, int index
, int &loop_in_i
, int &loop_in_j
) {
2689 int has_loop
[2] = { -1, -1 };
2690 if( options::stringLB() != 2 ) {
2691 for( unsigned r
=0; r
<2; r
++ ) {
2692 int n_index
= (r
==0 ? i
: j
);
2693 int other_n_index
= (r
==0 ? j
: i
);
2694 if( normal_forms
[other_n_index
][index
].getKind() != kind::CONST_STRING
) {
2695 for( unsigned lp
= index
+1; lp
<normal_forms
[n_index
].size(); lp
++ ){
2696 if( normal_forms
[n_index
][lp
]==normal_forms
[other_n_index
][index
] ){
2704 if( has_loop
[0]!=-1 || has_loop
[1]!=-1 ) {
2705 loop_in_i
= has_loop
[0];
2706 loop_in_j
= has_loop
[1];
2714 bool TheoryStrings::processLoop( std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
2715 int i
, int j
, int loop_n_index
, int other_n_index
, int loop_index
, int index
, InferInfo
& info
){
2716 if( options::stringAbortLoop() ){
2717 Message() << "Looping word equation encountered." << std::endl
;
2721 Trace("strings-loop") << "Detected possible loop for " << normal_forms
[loop_n_index
][loop_index
] << std::endl
;
2722 Trace("strings-loop") << " ... (X)= " << normal_forms
[other_n_index
][index
] << std::endl
;
2724 Trace("strings-loop") << " ... T(Y.Z)= ";
2725 std::vector
< Node
> vec_t
;
2726 for(int lp
=index
; lp
<loop_index
; ++lp
) {
2727 if(lp
!= index
) Trace("strings-loop") << " ++ ";
2728 Trace("strings-loop") << normal_forms
[loop_n_index
][lp
];
2729 vec_t
.push_back( normal_forms
[loop_n_index
][lp
] );
2731 Node t_yz
= mkConcat( vec_t
);
2732 Trace("strings-loop") << " (" << t_yz
<< ")" << std::endl
;
2733 Trace("strings-loop") << " ... S(Z.Y)= ";
2734 std::vector
< Node
> vec_s
;
2735 for(int lp
=index
+1; lp
<(int)normal_forms
[other_n_index
].size(); ++lp
) {
2736 if(lp
!= index
+1) Trace("strings-loop") << " ++ ";
2737 Trace("strings-loop") << normal_forms
[other_n_index
][lp
];
2738 vec_s
.push_back( normal_forms
[other_n_index
][lp
] );
2740 Node s_zy
= mkConcat( vec_s
);
2741 Trace("strings-loop") << " (" << s_zy
<< ")" << std::endl
;
2742 Trace("strings-loop") << " ... R= ";
2743 std::vector
< Node
> vec_r
;
2744 for(int lp
=loop_index
+1; lp
<(int)normal_forms
[loop_n_index
].size(); ++lp
) {
2745 if(lp
!= loop_index
+1) Trace("strings-loop") << " ++ ";
2746 Trace("strings-loop") << normal_forms
[loop_n_index
][lp
];
2747 vec_r
.push_back( normal_forms
[loop_n_index
][lp
] );
2749 Node r
= mkConcat( vec_r
);
2750 Trace("strings-loop") << " (" << r
<< ")" << std::endl
;
2752 //Trace("strings-loop") << "Lemma Cache: " << normal_form_src[i] << " vs " << normal_form_src[j] << std::endl;
2753 //TODO: can be more general
2754 if( s_zy
.isConst() && r
.isConst() && r
!=d_emptyString
) {
2757 if(s_zy
.getConst
<String
>().tailcmp( r
.getConst
<String
>(), c
) ) {
2759 s_zy
= NodeManager::currentNM()->mkConst( s_zy
.getConst
<String
>().substr(0, c
) );
2762 Trace("strings-loop") << "Strings::Loop: Refactor S(Z.Y)= " << s_zy
<< ", c=" << c
<< std::endl
;
2767 Trace("strings-loop") << "Strings::Loop: tails are different." << std::endl
;
2768 sendInference( info
.d_ant
, conc
, "Loop Conflict", true );
2773 //require that x is non-empty
2775 if( !areDisequal( normal_forms
[loop_n_index
][loop_index
], d_emptyString
) ){
2776 //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop
2777 split_eq
= normal_forms
[loop_n_index
][loop_index
].eqNode( d_emptyString
);
2778 }else if( !areDisequal( t_yz
, d_emptyString
) && t_yz
.getKind()!=kind::CONST_STRING
) {
2779 //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop
2780 split_eq
= t_yz
.eqNode( d_emptyString
);
2782 if( !split_eq
.isNull() ){
2783 info
.d_conc
= NodeManager::currentNM()->mkNode( kind::OR
, split_eq
, split_eq
.negate() );
2788 info
.d_ant
.push_back( normal_forms
[loop_n_index
][loop_index
].eqNode( d_emptyString
).negate() );
2789 if( t_yz
.getKind()!=kind::CONST_STRING
) {
2790 info
.d_ant
.push_back( t_yz
.eqNode( d_emptyString
).negate() );
2792 Node ant
= mkExplain( info
.d_ant
);
2793 if( d_loop_antec
.find( ant
) == d_loop_antec
.end() ){
2794 d_loop_antec
.insert( ant
);
2796 info
.d_antn
.push_back( ant
);
2800 r
== d_emptyString
&&
2802 s_zy
.getConst
<String
>().isRepeated()
2804 Node rep_c
= NodeManager::currentNM()->mkConst( s_zy
.getConst
<String
>().substr(0, 1) );
2805 Trace("strings-loop") << "Special case (X)=" << normal_forms
[other_n_index
][index
] << " " << std::endl
;
2806 Trace("strings-loop") << "... (C)=" << rep_c
<< " " << std::endl
;
2808 str_in_re
= NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP
, normal_forms
[other_n_index
][index
],
2809 NodeManager::currentNM()->mkNode( kind::REGEXP_STAR
,
2810 NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, rep_c
) ) );
2812 } else if(t_yz
.isConst()) {
2813 Trace("strings-loop") << "Strings::Loop: Const Normal Breaking." << std::endl
;
2814 CVC4::String s
= t_yz
.getConst
< CVC4::String
>();
2815 unsigned size
= s
.size();
2816 std::vector
< Node
> vconc
;
2817 for(unsigned len
=1; len
<=size
; len
++) {
2818 Node y
= NodeManager::currentNM()->mkConst(s
.substr(0, len
));
2819 Node z
= NodeManager::currentNM()->mkConst(s
.substr(len
, size
- len
));
2822 if(r
!= d_emptyString
) {
2823 std::vector
< Node
> v2(vec_r
);
2824 v2
.insert(v2
.begin(), y
);
2825 v2
.insert(v2
.begin(), z
);
2826 restr
= mkConcat( z
, y
);
2827 cc
= Rewriter::rewrite(s_zy
.eqNode( mkConcat( v2
) ));
2829 cc
= Rewriter::rewrite(s_zy
.eqNode( mkConcat( z
, y
) ));
2834 Node conc2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, normal_forms
[other_n_index
][index
],
2835 NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
,
2836 NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, y
),
2837 NodeManager::currentNM()->mkNode(kind::REGEXP_STAR
,
2838 NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, restr
))));
2839 cc
= cc
==d_true
? conc2
: NodeManager::currentNM()->mkNode( kind::AND
, cc
, conc2
);
2840 d_regexp_ant
[conc2
] = ant
;
2841 vconc
.push_back(cc
);
2843 conc
= vconc
.size()==0 ? Node::null() : vconc
.size()==1 ? vconc
[0] : NodeManager::currentNM()->mkNode(kind::OR
, vconc
);
2845 Trace("strings-loop") << "Strings::Loop: Normal Loop Breaking." << std::endl
;
2847 Node sk_w
= mkSkolemS( "w_loop" );
2848 Node sk_y
= mkSkolemS( "y_loop", 1 );
2849 Node sk_z
= mkSkolemS( "z_loop" );
2850 //t1 * ... * tn = y * z
2851 Node conc1
= t_yz
.eqNode( mkConcat( sk_y
, sk_z
) );
2852 // s1 * ... * sk = z * y * r
2853 vec_r
.insert(vec_r
.begin(), sk_y
);
2854 vec_r
.insert(vec_r
.begin(), sk_z
);
2855 Node conc2
= s_zy
.eqNode( mkConcat( vec_r
) );
2856 Node conc3
= normal_forms
[other_n_index
][index
].eqNode( mkConcat( sk_y
, sk_w
) );
2857 Node restr
= r
== d_emptyString
? s_zy
: mkConcat( sk_z
, sk_y
);
2858 str_in_re
= NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP
, sk_w
,
2859 NodeManager::currentNM()->mkNode( kind::REGEXP_STAR
,
2860 NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, restr
) ) );
2862 std::vector
< Node
> vec_conc
;
2863 vec_conc
.push_back(conc1
); vec_conc
.push_back(conc2
); vec_conc
.push_back(conc3
);
2864 vec_conc
.push_back(str_in_re
);
2865 //vec_conc.push_back(sk_y.eqNode(d_emptyString).negate());//by mkskolems
2866 conc
= NodeManager::currentNM()->mkNode( kind::AND
, vec_conc
);
2869 //set its antecedant to ant, to say when it is relevant
2870 if(!str_in_re
.isNull()) {
2871 d_regexp_ant
[str_in_re
] = ant
;
2874 addNormalFormPair( normal_form_src
[i
], normal_form_src
[j
] );
2875 if( options::stringProcessLoop() ){
2880 d_out
->setIncomplete();
2883 Trace("strings-loop") << "Strings::Loop: loop lemma for " << ant
<< " has already added." << std::endl
;
2884 addNormalFormPair( normal_form_src
[i
], normal_form_src
[j
] );
2891 //return true for lemma, false if we succeed
2892 bool TheoryStrings::processDeq( Node ni
, Node nj
) {
2893 //Assert( areDisequal( ni, nj ) );
2894 if( d_normal_forms
[ni
].size()>1 || d_normal_forms
[nj
].size()>1 ){
2895 std::vector
< Node
> nfi
;
2896 nfi
.insert( nfi
.end(), d_normal_forms
[ni
].begin(), d_normal_forms
[ni
].end() );
2897 std::vector
< Node
> nfj
;
2898 nfj
.insert( nfj
.end(), d_normal_forms
[nj
].begin(), d_normal_forms
[nj
].end() );
2900 int revRet
= processReverseDeq( nfi
, nfj
, ni
, nj
);
2906 nfi
.insert( nfi
.end(), d_normal_forms
[ni
].begin(), d_normal_forms
[ni
].end() );
2908 nfj
.insert( nfj
.end(), d_normal_forms
[nj
].begin(), d_normal_forms
[nj
].end() );
2911 while( index
<nfi
.size() || index
<nfj
.size() ){
2912 int ret
= processSimpleDeq( nfi
, nfj
, ni
, nj
, index
, false );
2916 Assert( index
<nfi
.size() && index
<nfj
.size() );
2917 Node i
= nfi
[index
];
2918 Node j
= nfj
[index
];
2919 Trace("strings-solve-debug") << "...Processing(DEQ) " << i
<< " " << j
<< std::endl
;
2920 if( !areEqual( i
, j
) ) {
2921 Assert( i
.getKind()!=kind::CONST_STRING
|| j
.getKind()!=kind::CONST_STRING
);
2922 std::vector
< Node
> lexp
;
2923 Node li
= getLength( i
, lexp
);
2924 Node lj
= getLength( j
, lexp
);
2925 if( areDisequal(li
, lj
) ){
2926 //if( i.getKind()==kind::CONST_STRING || j.getKind()==kind::CONST_STRING ){
2928 Trace("strings-solve") << "Non-Simple Case 1 : add lemma " << std::endl
;
2930 std::vector
< Node
> antec
;
2931 std::vector
< Node
> antec_new_lits
;
2932 antec
.insert( antec
.end(), d_normal_forms_exp
[ni
].begin(), d_normal_forms_exp
[ni
].end() );
2933 antec
.insert( antec
.end(), d_normal_forms_exp
[nj
].begin(), d_normal_forms_exp
[nj
].end() );
2935 if( areDisequal( ni
, nj
) ){
2936 antec
.push_back( ni
.eqNode( nj
).negate() );
2938 antec_new_lits
.push_back( ni
.eqNode( nj
).negate() );
2940 antec_new_lits
.push_back( li
.eqNode( lj
).negate() );
2941 std::vector
< Node
> conc
;
2942 Node sk1
= mkSkolemCached( i
, j
, sk_id_deq_x
, "x_dsplit" );
2943 Node sk2
= mkSkolemCached( i
, j
, sk_id_deq_y
, "y_dsplit" );
2944 Node sk3
= mkSkolemCached( i
, j
, sk_id_deq_z
, "z_dsplit", 1 );
2945 //Node nemp = sk3.eqNode(d_emptyString).negate();
2946 //conc.push_back(nemp);
2947 Node lsk1
= mkLength( sk1
);
2948 conc
.push_back( lsk1
.eqNode( li
) );
2949 Node lsk2
= mkLength( sk2
);
2950 conc
.push_back( lsk2
.eqNode( lj
) );
2951 conc
.push_back( NodeManager::currentNM()->mkNode( kind::OR
, j
.eqNode( mkConcat( sk1
, sk3
) ), i
.eqNode( mkConcat( sk2
, sk3
) ) ) );
2952 sendInference( antec
, antec_new_lits
, NodeManager::currentNM()->mkNode( kind::AND
, conc
), "D-DISL-Split" );
2953 ++(d_statistics
.d_deq_splits
);
2955 }else if( areEqual( li
, lj
) ){
2956 Assert( !areDisequal( i
, j
) );
2957 //splitting on demand : try to make them disequal
2958 Node eq
= i
.eqNode( j
);
2959 sendSplit( i
, j
, "S-Split(DEQL)" );
2960 eq
= Rewriter::rewrite( eq
);
2961 d_pending_req_phase
[ eq
] = false;
2964 //splitting on demand : try to make lengths equal
2965 Node eq
= li
.eqNode( lj
);
2966 sendSplit( li
, lj
, "D-Split" );
2967 eq
= Rewriter::rewrite( eq
);
2968 d_pending_req_phase
[ eq
] = true;
2980 int TheoryStrings::processReverseDeq( std::vector
< Node
>& nfi
, std::vector
< Node
>& nfj
, Node ni
, Node nj
) {
2981 //reverse normal form of i, j
2982 std::reverse( nfi
.begin(), nfi
.end() );
2983 std::reverse( nfj
.begin(), nfj
.end() );
2986 int ret
= processSimpleDeq( nfi
, nfj
, ni
, nj
, index
, true );
2988 //reverse normal form of i, j
2989 std::reverse( nfi
.begin(), nfi
.end() );
2990 std::reverse( nfj
.begin(), nfj
.end() );
2995 int TheoryStrings::processSimpleDeq( std::vector
< Node
>& nfi
, std::vector
< Node
>& nfj
, Node ni
, Node nj
, unsigned& index
, bool isRev
) {
2996 while( index
<nfi
.size() || index
<nfj
.size() ) {
2997 if( index
>=nfi
.size() || index
>=nfj
.size() ){
2998 Trace("strings-solve-debug") << "Disequality normalize empty" << std::endl
;
2999 std::vector
< Node
> ant
;
3000 //we have a conflict : because the lengths are equal, the remainder needs to be empty, which will lead to a conflict
3001 Node lni
= getLengthExp( ni
, ant
, d_normal_forms_base
[ni
] );
3002 Node lnj
= getLengthExp( nj
, ant
, d_normal_forms_base
[nj
] );
3003 ant
.push_back( lni
.eqNode( lnj
) );
3004 ant
.insert( ant
.end(), d_normal_forms_exp
[ni
].begin(), d_normal_forms_exp
[ni
].end() );
3005 ant
.insert( ant
.end(), d_normal_forms_exp
[nj
].begin(), d_normal_forms_exp
[nj
].end() );
3006 std::vector
< Node
> cc
;
3007 std::vector
< Node
>& nfk
= index
>=nfi
.size() ? nfj
: nfi
;
3008 for( unsigned index_k
=index
; index_k
<nfk
.size(); index_k
++ ){
3009 cc
.push_back( nfk
[index_k
].eqNode( d_emptyString
) );
3011 Node conc
= cc
.size()==1 ? cc
[0] : NodeManager::currentNM()->mkNode( kind::AND
, cc
);
3012 conc
= Rewriter::rewrite( conc
);
3013 sendInference( ant
, conc
, "Disequality Normalize Empty", true);
3016 Node i
= nfi
[index
];
3017 Node j
= nfj
[index
];
3018 Trace("strings-solve-debug") << "...Processing(QED) " << i
<< " " << j
<< std::endl
;
3019 if( !areEqual( i
, j
) ) {
3020 if( i
.getKind()==kind::CONST_STRING
&& j
.getKind()==kind::CONST_STRING
) {
3021 unsigned int len_short
= i
.getConst
<String
>().size() < j
.getConst
<String
>().size() ? i
.getConst
<String
>().size() : j
.getConst
<String
>().size();
3022 bool isSameFix
= isRev
? i
.getConst
<String
>().rstrncmp(j
.getConst
<String
>(), len_short
): i
.getConst
<String
>().strncmp(j
.getConst
<String
>(), len_short
);
3024 //same prefix/suffix
3025 //k is the index of the string that is shorter
3026 Node nk
= i
.getConst
<String
>().size() < j
.getConst
<String
>().size() ? i
: j
;
3027 Node nl
= i
.getConst
<String
>().size() < j
.getConst
<String
>().size() ? j
: i
;
3030 int new_len
= nl
.getConst
<String
>().size() - len_short
;
3031 remainderStr
= NodeManager::currentNM()->mkConst( nl
.getConst
<String
>().substr(0, new_len
) );
3032 Trace("strings-solve-debug-test") << "Rev. Break normal form of " << nl
<< " into " << nk
<< ", " << remainderStr
<< std::endl
;
3034 remainderStr
= NodeManager::currentNM()->mkConst( nl
.getConst
<String
>().substr( len_short
) );
3035 Trace("strings-solve-debug-test") << "Break normal form of " << nl
<< " into " << nk
<< ", " << remainderStr
<< std::endl
;
3037 if( i
.getConst
<String
>().size() < j
.getConst
<String
>().size() ) {
3038 nfj
.insert( nfj
.begin() + index
+ 1, remainderStr
);
3039 nfj
[index
] = nfi
[index
];
3041 nfi
.insert( nfi
.begin() + index
+ 1, remainderStr
);
3042 nfi
[index
] = nfj
[index
];
3048 std::vector
< Node
> lexp
;
3049 Node li
= getLength( i
, lexp
);
3050 Node lj
= getLength( j
, lexp
);
3051 if( areEqual( li
, lj
) && areDisequal( i
, j
) ) {
3052 Trace("strings-solve") << "Simple Case 2 : found equal length disequal sub strings " << i
<< " " << j
<< std::endl
;
3053 //we are done: D-Remove
3066 void TheoryStrings::addNormalFormPair( Node n1
, Node n2
){
3067 if( !isNormalFormPair( n1
, n2
) ){
3069 NodeIntMap::const_iterator it
= d_nf_pairs
.find( n1
);
3070 if( it
!=d_nf_pairs
.end() ){
3071 index
= (*it
).second
;
3073 d_nf_pairs
[n1
] = index
+ 1;
3074 if( index
<(int)d_nf_pairs_data
[n1
].size() ){
3075 d_nf_pairs_data
[n1
][index
] = n2
;
3077 d_nf_pairs_data
[n1
].push_back( n2
);
3079 Assert( isNormalFormPair( n1
, n2
) );
3081 Trace("strings-nf-debug") << "Already a normal form pair " << n1
<< " " << n2
<< std::endl
;
3085 bool TheoryStrings::isNormalFormPair( Node n1
, Node n2
) {
3086 //TODO: modulo equality?
3087 return isNormalFormPair2( n1
, n2
) || isNormalFormPair2( n2
, n1
);
3090 bool TheoryStrings::isNormalFormPair2( Node n1
, Node n2
) {
3091 //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl;
3092 NodeIntMap::const_iterator it
= d_nf_pairs
.find( n1
);
3093 if( it
!=d_nf_pairs
.end() ){
3094 Assert( d_nf_pairs_data
.find( n1
)!=d_nf_pairs_data
.end() );
3095 for( int i
=0; i
<(*it
).second
; i
++ ){
3096 Assert( i
<(int)d_nf_pairs_data
[n1
].size() );
3097 if( d_nf_pairs_data
[n1
][i
]==n2
){
3105 void TheoryStrings::registerTerm( Node n
, int effort
) {
3106 // 0 : upon preregistration or internal assertion
3107 // 1 : upon occurrence in length term
3108 // 2 : before normal form computation
3109 // 3 : called on normal form terms
3110 bool do_register
= false;
3111 if( options::stringEagerLen() ){
3112 do_register
= effort
==0;
3114 do_register
= effort
>0 || n
.getKind()!=kind::STRING_CONCAT
;
3117 if(d_registered_terms_cache
.find(n
) == d_registered_terms_cache
.end()) {
3118 d_registered_terms_cache
.insert(n
);
3119 Debug("strings-register") << "TheoryStrings::registerTerm() " << n
<< ", effort = " << effort
<< std::endl
;
3120 if(n
.getType().isString()) {
3121 //register length information:
3122 // for variables, split on empty vs positive length
3123 // for concat/const, introduce proxy var and state length relation
3124 if( n
.getKind()!=kind::STRING_CONCAT
&& n
.getKind()!=kind::CONST_STRING
) {
3125 if( d_length_intro_vars
.find(n
)==d_length_intro_vars
.end() ) {
3126 sendLengthLemma( n
);
3127 ++(d_statistics
.d_splits
);
3130 Node sk
= mkSkolemS("lsym", 2);
3131 StringsProxyVarAttribute spva
;
3132 sk
.setAttribute(spva
,true);
3133 Node eq
= Rewriter::rewrite( sk
.eqNode(n
) );
3134 Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq
<< std::endl
;
3135 d_proxy_var
[n
] = sk
;
3136 Trace("strings-assert") << "(assert " << eq
<< ")" << std::endl
;
3138 Node skl
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, sk
);
3140 if( n
.getKind() == kind::STRING_CONCAT
) {
3141 std::vector
<Node
> node_vec
;
3142 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ) {
3143 if( n
[i
].getAttribute(StringsProxyVarAttribute()) ){
3144 Assert( d_proxy_var_to_length
.find( n
[i
] )!=d_proxy_var_to_length
.end() );
3145 node_vec
.push_back( d_proxy_var_to_length
[n
[i
]] );
3147 Node lni
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, n
[i
] );
3148 node_vec
.push_back(lni
);
3151 lsum
= NodeManager::currentNM()->mkNode( kind::PLUS
, node_vec
);
3152 } else if( n
.getKind() == kind::CONST_STRING
) {
3153 lsum
= NodeManager::currentNM()->mkConst( ::CVC4::Rational( n
.getConst
<String
>().size() ) );
3155 lsum
= Rewriter::rewrite( lsum
);
3156 d_proxy_var_to_length
[sk
] = lsum
;
3157 Node ceq
= Rewriter::rewrite( skl
.eqNode( lsum
) );
3158 Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq
<< std::endl
;
3159 Trace("strings-lemma-debug") << " prerewrite : " << skl
.eqNode( lsum
) << std::endl
;
3160 Trace("strings-assert") << "(assert " << ceq
<< ")" << std::endl
;
3165 AlwaysAssert(false, "String Terms only in registerTerm.");
3171 void TheoryStrings::sendInference( std::vector
< Node
>& exp
, std::vector
< Node
>& exp_n
, Node eq
, const char * c
, bool asLemma
) {
3172 eq
= eq
.isNull() ? d_false
: Rewriter::rewrite( eq
);
3174 if( Trace
.isOn("strings-infer-debug") ){
3175 Trace("strings-infer-debug") << "By " << c
<< ", infer : " << eq
<< " from: " << std::endl
;
3176 for( unsigned i
=0; i
<exp
.size(); i
++ ){
3177 Trace("strings-infer-debug") << " " << exp
[i
] << std::endl
;
3179 for( unsigned i
=0; i
<exp_n
.size(); i
++ ){
3180 Trace("strings-infer-debug") << " N:" << exp_n
[i
] << std::endl
;
3182 //Trace("strings-infer-debug") << "as lemma : " << asLemma << std::endl;
3184 //check if we should send a lemma or an inference
3185 if( asLemma
|| eq
==d_false
|| eq
.getKind()==kind::OR
|| !exp_n
.empty() || options::stringInferAsLemmas() ){
3187 if( options::stringRExplainLemmas() ){
3188 eq_exp
= mkExplain( exp
, exp_n
);
3191 eq_exp
= mkAnd( exp_n
);
3192 }else if( exp_n
.empty() ){
3193 eq_exp
= mkAnd( exp
);
3195 std::vector
< Node
> ev
;
3196 ev
.insert( ev
.end(), exp
.begin(), exp
.end() );
3197 ev
.insert( ev
.end(), exp_n
.begin(), exp_n
.end() );
3198 eq_exp
= NodeManager::currentNM()->mkNode( kind::AND
, ev
);
3201 sendLemma( eq_exp
, eq
, c
);
3203 sendInfer( mkAnd( exp
), eq
, c
);
3208 void TheoryStrings::sendInference( std::vector
< Node
>& exp
, Node eq
, const char * c
, bool asLemma
) {
3209 std::vector
< Node
> exp_n
;
3210 sendInference( exp
, exp_n
, eq
, c
, asLemma
);
3213 void TheoryStrings::sendLemma( Node ant
, Node conc
, const char * c
) {
3214 if( conc
.isNull() || conc
== d_false
) {
3215 d_out
->conflict(ant
);
3216 Trace("strings-conflict") << "Strings::Conflict : " << c
<< " : " << ant
<< std::endl
;
3217 Trace("strings-lemma") << "Strings::Conflict : " << c
<< " : " << ant
<< std::endl
;
3218 Trace("strings-assert") << "(assert (not " << ant
<< ")) ; conflict " << c
<< std::endl
;
3222 if( ant
== d_true
) {
3225 lem
= NodeManager::currentNM()->mkNode( kind::IMPLIES
, ant
, conc
);
3227 Trace("strings-lemma") << "Strings::Lemma " << c
<< " : " << lem
<< std::endl
;
3228 Trace("strings-assert") << "(assert " << lem
<< ") ; lemma " << c
<< std::endl
;
3229 d_lemma_cache
.push_back( lem
);
3233 void TheoryStrings::sendInfer( Node eq_exp
, Node eq
, const char * c
) {
3234 if( options::stringInferSym() ){
3235 std::vector
< Node
> vars
;
3236 std::vector
< Node
> subs
;
3237 std::vector
< Node
> unproc
;
3238 inferSubstitutionProxyVars( eq_exp
, vars
, subs
, unproc
);
3239 if( unproc
.empty() ){
3240 Trace("strings-lemma-debug") << "Strings::Infer " << eq
<< " from " << eq_exp
<< " by " << c
<< std::endl
;
3241 Node eqs
= eq
.substitute( vars
.begin(), vars
.end(), subs
.begin(), subs
.end() );
3242 Trace("strings-lemma-debug") << "Strings::Infer Alternate : " << eqs
<< std::endl
;
3243 for( unsigned i
=0; i
<vars
.size(); i
++ ){
3244 Trace("strings-lemma-debug") << " " << vars
[i
] << " -> " << subs
[i
] << std::endl
;
3246 sendLemma( d_true
, eqs
, c
);
3249 for( unsigned i
=0; i
<unproc
.size(); i
++ ){
3250 Trace("strings-lemma-debug") << " non-trivial exp : " << unproc
[i
] << std::endl
;
3254 Trace("strings-lemma") << "Strings::Infer " << eq
<< " from " << eq_exp
<< " by " << c
<< std::endl
;
3255 Trace("strings-assert") << "(assert (=> " << eq_exp
<< " " << eq
<< ")) ; infer " << c
<< std::endl
;
3256 d_pending
.push_back( eq
);
3257 d_pending_exp
[eq
] = eq_exp
;
3258 d_infer
.push_back( eq
);
3259 d_infer_exp
.push_back( eq_exp
);
3263 void TheoryStrings::sendSplit( Node a
, Node b
, const char * c
, bool preq
) {
3264 Node eq
= a
.eqNode( b
);
3265 eq
= Rewriter::rewrite( eq
);
3266 Node neq
= NodeManager::currentNM()->mkNode( kind::NOT
, eq
);
3267 Node lemma_or
= NodeManager::currentNM()->mkNode( kind::OR
, eq
, neq
);
3268 Trace("strings-lemma") << "Strings::Lemma " << c
<< " SPLIT : " << lemma_or
<< std::endl
;
3269 d_lemma_cache
.push_back(lemma_or
);
3270 d_pending_req_phase
[eq
] = preq
;
3271 ++(d_statistics
.d_splits
);
3275 void TheoryStrings::sendLengthLemma( Node n
){
3276 Node n_len
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, n
);
3277 if( options::stringSplitEmp() || !options::stringLenGeqZ() ){
3278 Node n_len_eq_z
= n_len
.eqNode( d_zero
);
3279 Node n_len_eq_z_2
= n
.eqNode( d_emptyString
);
3280 n_len_eq_z
= Rewriter::rewrite( n_len_eq_z
);
3281 n_len_eq_z_2
= Rewriter::rewrite( n_len_eq_z_2
);
3282 Node n_len_geq_zero
= NodeManager::currentNM()->mkNode( kind::OR
, NodeManager::currentNM()->mkNode( kind::AND
, n_len_eq_z
, n_len_eq_z_2
),
3283 NodeManager::currentNM()->mkNode( kind::GT
, n_len
, d_zero
) );
3284 Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero
<< std::endl
;
3285 d_out
->lemma(n_len_geq_zero
);
3286 d_out
->requirePhase( n_len_eq_z
, true );
3287 d_out
->requirePhase( n_len_eq_z_2
, true );
3289 //AJR: probably a good idea
3290 if( options::stringLenGeqZ() ){
3291 Node n_len_geq
= NodeManager::currentNM()->mkNode( kind::GEQ
, n_len
, d_zero
);
3292 n_len_geq
= Rewriter::rewrite( n_len_geq
);
3293 d_out
->lemma( n_len_geq
);
3297 void TheoryStrings::inferSubstitutionProxyVars( Node n
, std::vector
< Node
>& vars
, std::vector
< Node
>& subs
, std::vector
< Node
>& unproc
) {
3298 if( n
.getKind()==kind::AND
){
3299 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
3300 inferSubstitutionProxyVars( n
[i
], vars
, subs
, unproc
);
3303 }else if( n
.getKind()==kind::EQUAL
){
3304 Node ns
= n
.substitute( vars
.begin(), vars
.end(), subs
.begin(), subs
.end() );
3305 ns
= Rewriter::rewrite( ns
);
3306 if( ns
.getKind()==kind::EQUAL
){
3309 for( unsigned i
=0; i
<2; i
++ ){
3311 if( ns
[i
].getAttribute(StringsProxyVarAttribute()) ){
3313 }else if( ns
[i
].isConst() ){
3314 NodeNodeMap::const_iterator it
= d_proxy_var
.find( ns
[i
] );
3315 if( it
!=d_proxy_var
.end() ){
3321 if( v
.getNumChildren()==0 ){
3325 //both sides involved in proxy var
3336 subs
.push_back( s
);
3337 vars
.push_back( v
);
3345 unproc
.push_back( n
);
3350 Node
TheoryStrings::mkConcat( Node n1
, Node n2
) {
3351 return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, n1
, n2
) );
3354 Node
TheoryStrings::mkConcat( Node n1
, Node n2
, Node n3
) {
3355 return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, n1
, n2
, n3
) );
3358 Node
TheoryStrings::mkConcat( const std::vector
< Node
>& c
) {
3359 return Rewriter::rewrite( c
.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, c
) : ( c
.size()==1 ? c
[0] : d_emptyString
) );
3362 Node
TheoryStrings::mkLength( Node t
) {
3363 return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, t
) );
3366 Node
TheoryStrings::mkSkolemCached( Node a
, Node b
, int id
, const char * c
, int isLenSplit
){
3367 //return mkSkolemS( c, isLenSplit );
3368 std::map
< int, Node
>::iterator it
= d_skolem_cache
[a
][b
].find( id
);
3369 if( it
==d_skolem_cache
[a
][b
].end() ){
3370 Node sk
= mkSkolemS( c
, isLenSplit
);
3371 d_skolem_cache
[a
][b
][id
] = sk
;
3378 //isLenSplit: 0-yes, 1-no, 2-ignore
3379 Node
TheoryStrings::mkSkolemS( const char *c
, int isLenSplit
) {
3380 Node n
= NodeManager::currentNM()->mkSkolem( c
, NodeManager::currentNM()->stringType(), "string sko" );
3381 d_length_intro_vars
.insert(n
);
3382 ++(d_statistics
.d_new_skolems
);
3383 if(isLenSplit
== 0) {
3384 sendLengthLemma( n
);
3385 ++(d_statistics
.d_splits
);
3386 } else if(isLenSplit
== 1) {
3387 registerNonEmptySkolem( n
);
3392 void TheoryStrings::registerNonEmptySkolem( Node n
) {
3393 if( d_skolem_cache_ne_reg
.find( n
)==d_skolem_cache_ne_reg
.end() ){
3394 d_skolem_cache_ne_reg
.insert( n
);
3395 d_equalityEngine
.assertEquality(n
.eqNode(d_emptyString
), false, d_true
);
3396 Node len_n_gt_z
= NodeManager::currentNM()->mkNode(kind::GT
,
3397 NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, n
), d_zero
);
3398 Trace("strings-lemma") << "Strings::Lemma SK-NON-ZERO : " << len_n_gt_z
<< std::endl
;
3399 Trace("strings-assert") << "(assert " << len_n_gt_z
<< ")" << std::endl
;
3400 d_out
->lemma(len_n_gt_z
);
3404 Node
TheoryStrings::mkExplain( std::vector
< Node
>& a
) {
3405 std::vector
< Node
> an
;
3406 return mkExplain( a
, an
);
3409 Node
TheoryStrings::mkExplain( std::vector
< Node
>& a
, std::vector
< Node
>& an
) {
3410 std::vector
< TNode
> antec_exp
;
3411 for( unsigned i
=0; i
<a
.size(); i
++ ) {
3412 if( std::find( a
.begin(), a
.begin() + i
, a
[i
] )==a
.begin() + i
) {
3414 Debug("strings-explain") << "Ask for explanation of " << a
[i
] << std::endl
;
3416 if(a
[i
].getKind() == kind::EQUAL
) {
3417 //assert( hasTerm(a[i][0]) );
3418 //assert( hasTerm(a[i][1]) );
3419 Assert( areEqual(a
[i
][0], a
[i
][1]) );
3420 if( a
[i
][0]==a
[i
][1] ){
3423 } else if( a
[i
].getKind()==kind::NOT
&& a
[i
][0].getKind()==kind::EQUAL
) {
3424 Assert( hasTerm(a
[i
][0][0]) );
3425 Assert( hasTerm(a
[i
][0][1]) );
3426 AlwaysAssert( d_equalityEngine
.areDisequal(a
[i
][0][0], a
[i
][0][1], true) );
3427 }else if( a
[i
].getKind() == kind::AND
){
3428 for( unsigned j
=0; j
<a
[i
].getNumChildren(); j
++ ){
3429 a
.push_back( a
[i
][j
] );
3434 unsigned ps
= antec_exp
.size();
3435 explain(a
[i
], antec_exp
);
3436 Debug("strings-explain") << "Done, explanation was : " << std::endl
;
3437 for( unsigned j
=ps
; j
<antec_exp
.size(); j
++ ) {
3438 Debug("strings-explain") << " " << antec_exp
[j
] << std::endl
;
3440 Debug("strings-explain") << std::endl
;
3444 for( unsigned i
=0; i
<an
.size(); i
++ ) {
3445 if( std::find( an
.begin(), an
.begin() + i
, an
[i
] )==an
.begin() + i
){
3446 Debug("strings-explain") << "Add to explanation (new literal) " << an
[i
] << std::endl
;
3447 antec_exp
.push_back(an
[i
]);
3451 if( antec_exp
.empty() ) {
3453 } else if( antec_exp
.size()==1 ) {
3456 ant
= NodeManager::currentNM()->mkNode( kind::AND
, antec_exp
);
3458 ant
= Rewriter::rewrite( ant
);
3462 Node
TheoryStrings::mkAnd( std::vector
< Node
>& a
) {
3463 std::vector
< Node
> au
;
3464 for( unsigned i
=0; i
<a
.size(); i
++ ){
3465 if( std::find( au
.begin(), au
.end(), a
[i
] )==au
.end() ){
3466 au
.push_back( a
[i
] );
3471 } else if( au
.size() == 1 ) {
3474 return NodeManager::currentNM()->mkNode( kind::AND
, au
);
3478 void TheoryStrings::getConcatVec( Node n
, std::vector
< Node
>& c
) {
3479 if( n
.getKind()==kind::STRING_CONCAT
) {
3480 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ) {
3481 if( !areEqual( n
[i
], d_emptyString
) ) {
3482 c
.push_back( n
[i
] );
3490 void TheoryStrings::checkDeqNF() {
3491 std::vector
< std::vector
< Node
> > cols
;
3492 std::vector
< Node
> lts
;
3493 std::map
< Node
, std::map
< Node
, bool > > processed
;
3495 //for each pair of disequal strings, must determine whether their lengths are equal or disequal
3496 for( NodeList::const_iterator id
= d_ee_disequalities
.begin(); id
!= d_ee_disequalities
.end(); ++id
) {
3499 for( unsigned i
=0; i
<2; i
++ ){
3500 n
[i
] = d_equalityEngine
.getRepresentative( eq
[i
] );
3502 if( processed
[n
[0]].find( n
[1] )==processed
[n
[0]].end() ){
3503 processed
[n
[0]][n
[1]] = true;
3505 for( unsigned i
=0; i
<2; i
++ ){
3506 EqcInfo
* ei
= getOrMakeEqcInfo( n
[i
], false );
3507 lt
[i
] = ei
? ei
->d_length_term
: Node::null();
3508 if( lt
[i
].isNull() ){
3511 lt
[i
] = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, lt
[i
] );
3513 if( !areEqual( lt
[0], lt
[1] ) && !areDisequal( lt
[0], lt
[1] ) ){
3514 sendSplit( lt
[0], lt
[1], "DEQ-LENGTH-SP" );
3519 if( !hasProcessed() ){
3520 separateByLength( d_strings_eqc
, cols
, lts
);
3521 for( unsigned i
=0; i
<cols
.size(); i
++ ){
3522 if( cols
[i
].size()>1 && d_lemma_cache
.empty() ){
3523 Trace("strings-solve") << "- Verify disequalities are processed for " << cols
[i
][0] << ", normal form : ";
3524 printConcat( d_normal_forms
[cols
[i
][0]], "strings-solve" );
3525 Trace("strings-solve") << "... #eql = " << cols
[i
].size() << std::endl
;
3526 //must ensure that normal forms are disequal
3527 for( unsigned j
=0; j
<cols
[i
].size(); j
++ ){
3528 for( unsigned k
=(j
+1); k
<cols
[i
].size(); k
++ ){
3529 //for strings that are disequal, but have the same length
3530 if( areDisequal( cols
[i
][j
], cols
[i
][k
] ) ){
3531 Assert( !d_conflict
);
3532 Trace("strings-solve") << "- Compare " << cols
[i
][j
] << " ";
3533 printConcat( d_normal_forms
[cols
[i
][j
]], "strings-solve" );
3534 Trace("strings-solve") << " against " << cols
[i
][k
] << " ";
3535 printConcat( d_normal_forms
[cols
[i
][k
]], "strings-solve" );
3536 Trace("strings-solve") << "..." << std::endl
;
3537 if( processDeq( cols
[i
][j
], cols
[i
][k
] ) ){
3548 void TheoryStrings::checkLengthsEqc() {
3549 if( options::stringLenNorm() ){
3550 for( unsigned i
=0; i
<d_strings_eqc
.size(); i
++ ){
3551 //if( d_normal_forms[nodes[i]].size()>1 ) {
3552 Trace("strings-process-debug") << "Process length constraints for " << d_strings_eqc
[i
] << std::endl
;
3553 //check if there is a length term for this equivalence class
3554 EqcInfo
* ei
= getOrMakeEqcInfo( d_strings_eqc
[i
], false );
3555 Node lt
= ei
? ei
->d_length_term
: Node::null();
3556 if( !lt
.isNull() ) {
3557 Node llt
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, lt
);
3558 //now, check if length normalization has occurred
3559 if( ei
->d_normalized_length
.get().isNull() ) {
3560 Node nf
= mkConcat( d_normal_forms
[d_strings_eqc
[i
]] );
3561 if( Trace
.isOn("strings-process-debug") ){
3562 Trace("strings-process-debug") << " normal form is " << nf
<< " from base " << d_normal_forms_base
[d_strings_eqc
[i
]] << std::endl
;
3563 Trace("strings-process-debug") << " normal form exp is: " << std::endl
;
3564 for( unsigned j
=0; j
<d_normal_forms_exp
[d_strings_eqc
[i
]].size(); j
++ ){
3565 Trace("strings-process-debug") << " " << d_normal_forms_exp
[d_strings_eqc
[i
]][j
] << std::endl
;
3569 //if not, add the lemma
3570 std::vector
< Node
> ant
;
3571 ant
.insert( ant
.end(), d_normal_forms_exp
[d_strings_eqc
[i
]].begin(), d_normal_forms_exp
[d_strings_eqc
[i
]].end() );
3572 ant
.push_back( d_normal_forms_base
[d_strings_eqc
[i
]].eqNode( lt
) );
3573 Node lc
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, nf
);
3574 Node lcr
= Rewriter::rewrite( lc
);
3575 Trace("strings-process-debug") << "Rewrote length " << lc
<< " to " << lcr
<< std::endl
;
3576 Node eq
= llt
.eqNode( lcr
);
3578 ei
->d_normalized_length
.set( eq
);
3579 sendInference( ant
, eq
, "LEN-NORM", true );
3583 Trace("strings-process-debug") << "No length term for eqc " << d_strings_eqc
[i
] << " " << d_eqc_to_len_term
[d_strings_eqc
[i
]] << std::endl
;
3584 if( !options::stringEagerLen() ){
3585 Node c
= mkConcat( d_normal_forms
[d_strings_eqc
[i
]] );
3586 registerTerm( c
, 3 );
3589 NodeNodeMap::const_iterator it = d_proxy_var.find( c );
3590 if( it!=d_proxy_var.end() ){
3591 Node pv = (*it).second;
3592 Assert( d_proxy_var_to_length.find( pv )!=d_proxy_var_to_length.end() );
3593 Node pvl = d_proxy_var_to_length[pv];
3594 Node ceq = Rewriter::rewrite( mkLength( pv ).eqNode( pvl ) );
3595 sendInference( d_empty_vec, ceq, "LEN-NORM-I", true );
3602 // Trace("strings-process-debug") << "Do not process length constraints for " << nodes[i] << " " << d_normal_forms[nodes[i]].size() << std::endl;
3608 void TheoryStrings::checkCardinality() {
3609 //int cardinality = options::stringCharCardinality();
3610 //Trace("strings-solve-debug2") << "get cardinality: " << cardinality << endl;
3612 //AJR: this will create a partition of eqc, where each collection has length that are pairwise propagated to be equal.
3613 // we do not require disequalities between the lengths of each collection, since we split on disequalities between lengths of string terms that are disequal (DEQ-LENGTH-SP).
3614 // TODO: revisit this?
3615 std::vector
< std::vector
< Node
> > cols
;
3616 std::vector
< Node
> lts
;
3617 separateByLength( d_strings_eqc
, cols
, lts
);
3619 for( unsigned i
= 0; i
<cols
.size(); ++i
) {
3621 Trace("strings-card") << "Number of strings with length equal to " << lr
<< " is " << cols
[i
].size() << std::endl
;
3622 if( cols
[i
].size() > 1 ) {
3624 unsigned card_need
= 1;
3625 double curr
= (double)cols
[i
].size();
3626 while( curr
>d_card_size
){
3627 curr
= curr
/(double)d_card_size
;
3630 Trace("strings-card") << "Need length " << card_need
<< " for this number of strings (where alphabet size is " << d_card_size
<< ")." << std::endl
;
3631 Node cmp
= NodeManager::currentNM()->mkNode( kind::GEQ
, lr
, NodeManager::currentNM()->mkConst( Rational( card_need
) ) );
3632 cmp
= Rewriter::rewrite( cmp
);
3634 unsigned int int_k
= (unsigned int)card_need
;
3635 for( std::vector
< Node
>::iterator itr1
= cols
[i
].begin();
3636 itr1
!= cols
[i
].end(); ++itr1
) {
3637 for( std::vector
< Node
>::iterator itr2
= itr1
+ 1;
3638 itr2
!= cols
[i
].end(); ++itr2
) {
3639 if(!areDisequal( *itr1
, *itr2
)) {
3641 sendSplit( *itr1
, *itr2
, "CARD-SP" );
3646 EqcInfo
* ei
= getOrMakeEqcInfo( lr
, true );
3647 Trace("strings-card") << "Previous cardinality used for " << lr
<< " is " << ((int)ei
->d_cardinality_lem_k
.get()-1) << std::endl
;
3648 if( int_k
+1 > ei
->d_cardinality_lem_k
.get() ){
3649 Node k_node
= NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k
) );
3650 //add cardinality lemma
3651 Node dist
= NodeManager::currentNM()->mkNode( kind::DISTINCT
, cols
[i
] );
3652 std::vector
< Node
> vec_node
;
3653 vec_node
.push_back( dist
);
3654 for( std::vector
< Node
>::iterator itr1
= cols
[i
].begin();
3655 itr1
!= cols
[i
].end(); ++itr1
) {
3656 Node len
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, *itr1
);
3658 Node len_eq_lr
= len
.eqNode(lr
);
3659 vec_node
.push_back( len_eq_lr
);
3662 Node len
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, cols
[i
][0] );
3663 Node cons
= NodeManager::currentNM()->mkNode( kind::GEQ
, len
, k_node
);
3664 cons
= Rewriter::rewrite( cons
);
3665 ei
->d_cardinality_lem_k
.set( int_k
+1 );
3667 sendInference( d_empty_vec
, vec_node
, cons
, "CARDINALITY", true );
3676 void TheoryStrings::getEquivalenceClasses( std::vector
< Node
>& eqcs
) {
3677 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( &d_equalityEngine
);
3678 while( !eqcs_i
.isFinished() ) {
3679 Node eqc
= (*eqcs_i
);
3680 //if eqc.getType is string
3681 if (eqc
.getType().isString()) {
3682 eqcs
.push_back( eqc
);
3688 void TheoryStrings::separateByLength(std::vector
< Node
>& n
,
3689 std::vector
< std::vector
< Node
> >& cols
,
3690 std::vector
< Node
>& lts
) {
3691 unsigned leqc_counter
= 0;
3692 std::map
< Node
, unsigned > eqc_to_leqc
;
3693 std::map
< unsigned, Node
> leqc_to_eqc
;
3694 std::map
< unsigned, std::vector
< Node
> > eqc_to_strings
;
3695 for( unsigned i
=0; i
<n
.size(); i
++ ) {
3697 Assert( d_equalityEngine
.getRepresentative(eqc
)==eqc
);
3698 EqcInfo
* ei
= getOrMakeEqcInfo( eqc
, false );
3699 Node lt
= ei
? ei
->d_length_term
: Node::null();
3701 lt
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, lt
);
3702 Node r
= d_equalityEngine
.getRepresentative( lt
);
3703 if( eqc_to_leqc
.find( r
)==eqc_to_leqc
.end() ){
3704 eqc_to_leqc
[r
] = leqc_counter
;
3705 leqc_to_eqc
[leqc_counter
] = r
;
3708 eqc_to_strings
[ eqc_to_leqc
[r
] ].push_back( eqc
);
3710 eqc_to_strings
[leqc_counter
].push_back( eqc
);
3714 for( std::map
< unsigned, std::vector
< Node
> >::iterator it
= eqc_to_strings
.begin(); it
!= eqc_to_strings
.end(); ++it
){
3715 cols
.push_back( std::vector
< Node
>() );
3716 cols
.back().insert( cols
.back().end(), it
->second
.begin(), it
->second
.end() );
3717 lts
.push_back( leqc_to_eqc
[it
->first
] );
3721 void TheoryStrings::printConcat( std::vector
< Node
>& n
, const char * c
) {
3722 for( unsigned i
=0; i
<n
.size(); i
++ ){
3723 if( i
>0 ) Trace(c
) << " ++ ";
3730 //// Finite Model Finding
3732 Node
TheoryStrings::getNextDecisionRequest() {
3733 if( options::stringFMF() && !d_conflict
){
3734 Node in_var_lsum
= d_input_var_lsum
.get();
3735 //Trace("strings-fmf-debug") << "Strings::FMF: Assertion Level = " << d_valuation.getAssertionLevel() << std::endl;
3736 //initialize the term we will minimize
3737 if( in_var_lsum
.isNull() && !d_input_vars
.empty() ){
3738 Trace("strings-fmf-debug") << "Input variables: ";
3739 std::vector
< Node
> ll
;
3740 for(NodeSet::key_iterator itr
= d_input_vars
.key_begin();
3741 itr
!= d_input_vars
.key_end(); ++itr
) {
3742 Trace("strings-fmf-debug") << " " << (*itr
) ;
3743 ll
.push_back( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, *itr
) );
3745 Trace("strings-fmf-debug") << std::endl
;
3746 in_var_lsum
= ll
.size()==1 ? ll
[0] : NodeManager::currentNM()->mkNode( kind::PLUS
, ll
);
3747 in_var_lsum
= Rewriter::rewrite( in_var_lsum
);
3748 d_input_var_lsum
.set( in_var_lsum
);
3750 if( !in_var_lsum
.isNull() ){
3751 //Trace("strings-fmf") << "Get next decision request." << std::endl;
3752 //check if we need to decide on something
3753 int decideCard
= d_curr_cardinality
.get();
3754 if( d_cardinality_lits
.find( decideCard
)!=d_cardinality_lits
.end() ){
3756 Node cnode
= d_cardinality_lits
[ d_curr_cardinality
.get() ];
3757 if( d_valuation
.hasSatValue( cnode
, value
) ) {
3759 d_curr_cardinality
.set( d_curr_cardinality
.get() + 1 );
3760 decideCard
= d_curr_cardinality
.get();
3761 Trace("strings-fmf-debug") << "Has false SAT value, increment and decide." << std::endl
;
3764 Trace("strings-fmf-debug") << "Has true SAT value, do not decide." << std::endl
;
3767 Trace("strings-fmf-debug") << "No SAT value, decide." << std::endl
;
3770 if( decideCard
!=-1 ){
3771 if( d_cardinality_lits
.find( decideCard
)==d_cardinality_lits
.end() ){
3772 Node lit
= NodeManager::currentNM()->mkNode( kind::LEQ
, in_var_lsum
, NodeManager::currentNM()->mkConst( Rational( decideCard
) ) );
3773 lit
= Rewriter::rewrite( lit
);
3774 d_cardinality_lits
[decideCard
] = lit
;
3775 Node lem
= NodeManager::currentNM()->mkNode( kind::OR
, lit
, lit
.negate() );
3776 Trace("strings-fmf") << "Strings::FMF: Add decision lemma " << lem
<< ", decideCard = " << decideCard
<< std::endl
;
3777 d_out
->lemma( lem
);
3778 d_out
->requirePhase( lit
, true );
3780 Node lit
= d_cardinality_lits
[ decideCard
];
3781 Trace("strings-fmf") << "Strings::FMF: Decide positive on " << lit
<< std::endl
;
3786 return Node::null();
3789 Node
TheoryStrings::ppRewrite(TNode atom
) {
3790 Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom
<< std::endl
;
3791 if( !options::stringLazyPreproc() ){
3792 //eager preprocess here
3793 std::vector
< Node
> new_nodes
;
3794 Node ret
= d_preproc
.processAssertion( atom
, new_nodes
);
3796 Trace("strings-ppr") << " rewrote " << atom
<< " -> " << ret
<< ", with " << new_nodes
.size() << " lemmas." << std::endl
;
3797 for( unsigned i
=0; i
<new_nodes
.size(); i
++ ){
3798 Trace("strings-ppr") << " lemma : " << new_nodes
[i
] << std::endl
;
3799 d_out
->lemma( new_nodes
[i
] );
3803 Assert( new_nodes
.empty() );
3809 void TheoryStrings::collectExtendedFuncTerms( Node n
, std::map
< Node
, bool >& visited
) {
3810 if( visited
.find( n
)==visited
.end() ){
3812 if( n
.getKind()==kind::STRING_SUBSTR
|| n
.getKind()==kind::STRING_STRIDOF
||
3813 n
.getKind() == kind::STRING_ITOS
|| n
.getKind() == kind::STRING_U16TOS
|| n
.getKind() == kind::STRING_U32TOS
||
3814 n
.getKind() == kind::STRING_STOI
|| n
.getKind() == kind::STRING_STOU16
|| n
.getKind() == kind::STRING_STOU32
||
3815 n
.getKind() == kind::STRING_STRREPL
|| n
.getKind() == kind::STRING_STRCTN
){
3816 addExtendedFuncTerm( n
);
3818 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
3819 collectExtendedFuncTerms( n
[i
], visited
);
3824 void TheoryStrings::addExtendedFuncTerm( Node n
) {
3825 if( d_ext_func_terms
.find( n
)==d_ext_func_terms
.end() ){
3826 Trace("strings-extf-debug2") << "Found extended function : " << n
<< std::endl
;
3827 Assert( n
.getKind()==kind::STRING_IN_REGEXP
|| options::stringLazyPreproc() );
3828 d_ext_func_terms
[n
] = true;
3830 std::map
< Node
, bool > visited
;
3831 collectVars( n
, d_extf_info
[n
].d_vars
, visited
);
3836 TheoryStrings::Statistics::Statistics():
3837 d_splits("TheoryStrings::NumOfSplitOnDemands", 0),
3838 d_eq_splits("TheoryStrings::NumOfEqSplits", 0),
3839 d_deq_splits("TheoryStrings::NumOfDiseqSplits", 0),
3840 d_loop_lemmas("TheoryStrings::NumOfLoops", 0),
3841 d_new_skolems("TheoryStrings::NumOfNewSkolems", 0)
3843 smtStatisticsRegistry()->registerStat(&d_splits
);
3844 smtStatisticsRegistry()->registerStat(&d_eq_splits
);
3845 smtStatisticsRegistry()->registerStat(&d_deq_splits
);
3846 smtStatisticsRegistry()->registerStat(&d_loop_lemmas
);
3847 smtStatisticsRegistry()->registerStat(&d_new_skolems
);
3850 TheoryStrings::Statistics::~Statistics(){
3851 smtStatisticsRegistry()->unregisterStat(&d_splits
);
3852 smtStatisticsRegistry()->unregisterStat(&d_eq_splits
);
3853 smtStatisticsRegistry()->unregisterStat(&d_deq_splits
);
3854 smtStatisticsRegistry()->unregisterStat(&d_loop_lemmas
);
3855 smtStatisticsRegistry()->unregisterStat(&d_new_skolems
);
3877 //// Regular Expressions
3880 unsigned TheoryStrings::getNumMemberships( Node n
, bool isPos
) {
3882 NodeIntMap::const_iterator it
= d_pos_memberships
.find( n
);
3883 if( it
!=d_pos_memberships
.end() ){
3884 return (*it
).second
;
3887 NodeIntMap::const_iterator it
= d_neg_memberships
.find( n
);
3888 if( it
!=d_neg_memberships
.end() ){
3889 return (*it
).second
;
3895 Node
TheoryStrings::getMembership( Node n
, bool isPos
, unsigned i
) {
3896 return isPos
? d_pos_memberships_data
[n
][i
] : d_neg_memberships_data
[n
][i
];
3899 Node
TheoryStrings::mkRegExpAntec(Node atom
, Node ant
) {
3900 if(d_regexp_ant
.find(atom
) == d_regexp_ant
.end()) {
3901 return Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND
, ant
, atom
) );
3903 Node n
= d_regexp_ant
[atom
];
3904 return Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND
, ant
, n
) );
3908 Node
TheoryStrings::normalizeRegexp(Node r
) {
3910 if(d_nf_regexps
.find(r
) != d_nf_regexps
.end()) {
3911 nf_r
= d_nf_regexps
[r
];
3913 std::vector
< Node
> nf_exp
;
3914 if(!d_regexp_opr
.checkConstRegExp(r
)) {
3915 switch( r
.getKind() ) {
3916 case kind::REGEXP_EMPTY
:
3917 case kind::REGEXP_SIGMA
: {
3920 case kind::STRING_TO_REGEXP
: {
3921 if(r
[0].isConst()) {
3924 if(d_normal_forms
.find( r
[0] ) != d_normal_forms
.end()) {
3925 nf_r
= mkConcat( d_normal_forms
[r
[0]] );
3926 Debug("regexp-nf") << "Term: " << r
[0] << " has a normal form " << nf_r
<< std::endl
;
3927 nf_exp
.insert(nf_exp
.end(), d_normal_forms_exp
[r
[0]].begin(), d_normal_forms_exp
[r
[0]].end());
3928 nf_r
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, nf_r
) );
3932 case kind::REGEXP_CONCAT
:
3933 case kind::REGEXP_UNION
:
3934 case kind::REGEXP_INTER
: {
3936 std::vector
< Node
> vec_nodes
;
3937 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
3938 Node rtmp
= normalizeRegexp(r
[i
]);
3939 vec_nodes
.push_back(rtmp
);
3945 Node rtmp
= vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode(r
.getKind(), vec_nodes
);
3946 nf_r
= Rewriter::rewrite( rtmp
);
3949 case kind::REGEXP_STAR
: {
3950 Node rtmp
= normalizeRegexp(r
[0]);
3952 rtmp
= NodeManager::currentNM()->mkNode(kind::REGEXP_STAR
, rtmp
);
3953 nf_r
= Rewriter::rewrite( rtmp
);
3961 d_nf_regexps
[r
] = nf_r
;
3962 d_nf_regexps_exp
[r
] = nf_exp
;
3967 bool TheoryStrings::normalizePosMemberships(std::map
< Node
, std::vector
< Node
> > &memb_with_exps
) {
3968 std::map
< Node
, std::vector
< Node
> > unprocessed_x_exps
;
3969 std::map
< Node
, std::vector
< Node
> > unprocessed_memberships
;
3970 std::map
< Node
, std::vector
< Node
> > unprocessed_memberships_bases
;
3971 bool addLemma
= false;
3973 Trace("regexp-check") << "Normalizing Positive Memberships ... " << std::endl
;
3975 for( NodeIntMap::const_iterator itr_xr
= d_pos_memberships
.begin(); itr_xr
!= d_pos_memberships
.end(); ++itr_xr
){
3976 Node x
= (*itr_xr
).first
;
3978 std::vector
< Node
> nf_x_exp
;
3979 if(d_normal_forms
.find( x
) != d_normal_forms
.end()) {
3980 //nf_x = mkConcat( d_normal_forms[x] );
3981 nf_x_exp
.insert(nf_x_exp
.end(), d_normal_forms_exp
[x
].begin(), d_normal_forms_exp
[x
].end());
3982 //Debug("regexp-nf") << "Term: " << x << " has a normal form " << ret << std::endl;
3986 Trace("regexp-nf") << "Checking Memberships for N(" << x
<< ") = " << nf_x
<< " :" << std::endl
;
3988 std::vector
< Node
> vec_x
;
3989 std::vector
< Node
> vec_r
;
3990 unsigned n_pmem
= (*itr_xr
).second
;
3991 Assert( getNumMemberships( x
, true )==n_pmem
);
3992 for( unsigned k
=0; k
<n_pmem
; k
++ ){
3993 Node r
= getMembership( x
, true, k
);
3994 Node nf_r
= normalizeRegexp( r
); //AJR: fixed (was normalizing mem #0 always)
3995 Node memb
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, nf_x
, nf_r
);
3996 if(d_processed_memberships
.find(memb
) == d_processed_memberships
.end()) {
3997 if(d_regexp_opr
.checkConstRegExp(nf_r
)) {
4001 Trace("regexp-nf") << "Handling Symbolic Regexp for N(" << r
<< ") = " << nf_r
<< std::endl
;
4002 //TODO: handle symbolic ones
4005 d_processed_memberships
.insert(memb
);
4008 if(!vec_x
.empty()) {
4009 if(unprocessed_x_exps
.find(nf_x
) == unprocessed_x_exps
.end()) {
4010 unprocessed_x_exps
[nf_x
] = nf_x_exp
;
4011 unprocessed_memberships
[nf_x
] = vec_r
;
4012 unprocessed_memberships_bases
[nf_x
] = vec_x
;
4014 unprocessed_x_exps
[nf_x
].insert(unprocessed_x_exps
[nf_x
].end(), nf_x_exp
.begin(), nf_x_exp
.end());
4015 unprocessed_memberships
[nf_x
].insert(unprocessed_memberships
[nf_x
].end(), vec_r
.begin(), vec_r
.end());
4016 unprocessed_memberships_bases
[nf_x
].insert(unprocessed_memberships_bases
[nf_x
].end(), vec_x
.begin(), vec_x
.end());
4021 for(std::map
< Node
, std::vector
< Node
> >::const_iterator itr
= unprocessed_memberships
.begin();
4022 itr
!= unprocessed_memberships
.end(); ++itr
) {
4023 Node nf_x
= itr
->first
;
4024 std::vector
< Node
> exp( unprocessed_x_exps
[nf_x
] );
4025 Node r
= itr
->second
[0];
4027 Node inter_r
= d_nf_regexps
[r
];
4028 exp
.insert(exp
.end(), d_nf_regexps_exp
[r
].begin(), d_nf_regexps_exp
[r
].end());
4029 Node x
= unprocessed_memberships_bases
[itr
->first
][0];
4030 Node memb
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, x
, r
);
4031 exp
.push_back(memb
);
4032 for(std::size_t i
=1; i
< itr
->second
.size(); i
++) {
4034 Node r2
= itr
->second
[i
];
4035 Node inter_r2
= d_nf_regexps
[r2
];
4036 exp
.insert(exp
.end(), d_nf_regexps_exp
[r2
].begin(), d_nf_regexps_exp
[r2
].end());
4037 Node x2
= unprocessed_memberships_bases
[itr
->first
][i
];
4038 memb
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, x2
, r2
);
4039 exp
.push_back(memb
);
4041 bool spflag
= false;
4042 inter_r
= d_regexp_opr
.intersect(inter_r
, inter_r2
, spflag
);
4043 if(inter_r
== d_emptyRegexp
) {
4046 sendInference( d_empty_vec
, exp
, conc
, "INTERSECT CONFLICT", true );
4053 memb
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, nf_x
, inter_r
) );
4054 memb_with_exps
[memb
] = exp
;
4063 bool TheoryStrings::applyRConsume( CVC4::String
&s
, Node
&r
) {
4064 Trace("regexp-derivative") << "TheoryStrings::derivative: s=" << s
<< ", r= " << r
<< std::endl
;
4065 Assert( d_regexp_opr
.checkConstRegExp(r
) );
4067 if( !s
.isEmptyString() ) {
4070 for(unsigned i
=0; i
<s
.size(); ++i
) {
4071 CVC4::String c
= s
.substr(i
, 1);
4073 int rt
= d_regexp_opr
.derivativeS(dc
, c
, dc2
);
4077 } else if(rt
== 2) {
4087 Node
TheoryStrings::applyRSplit(Node s1
, Node s2
, Node r
) {
4088 Assert(d_regexp_opr
.checkConstRegExp(r
));
4090 std::vector
< std::pair
< Node
, Node
> > vec_can
;
4091 d_regexp_opr
.splitRegExp(r
, vec_can
);
4092 //TODO: lazy cache or eager?
4093 std::vector
< Node
> vec_or
;
4095 for(unsigned int i
=0; i
<vec_can
.size(); i
++) {
4096 Node m1
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s1
, vec_can
[i
].first
);
4097 Node m2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s2
, vec_can
[i
].second
);
4098 Node c
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND
, m1
, m2
) );
4099 vec_or
.push_back( c
);
4101 Node conc
= vec_or
.size()==0? Node::null() : vec_or
.size()==1 ? vec_or
[0] : Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::OR
, vec_or
) );
4105 bool TheoryStrings::applyRLen(std::map
< Node
, std::vector
< Node
> > &XinR_with_exps
) {
4106 if(XinR_with_exps
.size() > 0) {
4107 //TODO: get vector, var, store.
4114 bool TheoryStrings::checkMembershipsWithoutLength(
4115 std::map
< Node
, std::vector
< Node
> > &memb_with_exps
,
4116 std::map
< Node
, std::vector
< Node
> > &XinR_with_exps
) {
4117 for(std::map
< Node
, std::vector
< Node
> >::iterator itr
= memb_with_exps
.begin(); itr
!= memb_with_exps
.end(); ++itr
) {
4118 Node memb
= itr
->first
;
4122 memb
= Rewriter::rewrite( memb
);
4123 if(memb
== d_false
) {
4125 sendInference(d_empty_vec
, itr
->second
, conc
, "MEMBERSHIP CONFLICT", true);
4129 Assert(memb
== d_true
);
4131 } else if(s
.getKind() == kind::VARIABLE
) {
4133 XinR_with_exps
[itr
->first
] = itr
->second
;
4135 Assert(s
.getKind() == kind::STRING_CONCAT
);
4137 for( unsigned i
=0; i
<s
.getNumChildren(); i
++ ) {
4138 if(s
[i
].isConst()) {
4139 CVC4::String
str( s
[0].getConst
< String
>() );
4140 //R-Consume, see Tianyi's thesis
4141 if(!applyRConsume(str
, r
)) {
4142 sendInference(d_empty_vec
, itr
->second
, conc
, "R-Consume CONFLICT", true);
4147 //R-Split, see Tianyi's thesis
4148 if(i
== s
.getNumChildren() - 1) {
4150 Node memb2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
[i
], r
);
4151 XinR_with_exps
[itr
->first
] = itr
->second
;
4154 std::vector
< Node
> vec_s2
;
4155 for( unsigned j
=i
+1; j
<s
.getNumChildren(); j
++ ) {
4156 vec_s2
.push_back(s
[j
]);
4158 Node s2
= mkConcat(vec_s2
);
4159 conc
= applyRSplit(s1
, s2
, r
);
4160 if(conc
== d_true
) {
4162 } else if(conc
.isNull() || conc
== d_false
) {
4163 conc
= Node::null();
4164 sendInference(d_empty_vec
, itr
->second
, conc
, "R-Split Conflict", true);
4168 sendInference(d_empty_vec
, itr
->second
, conc
, "R-Split", true);
4180 bool TheoryStrings::checkMemberships2() {
4181 bool addedLemma
= false;
4182 d_nf_regexps
.clear();
4183 d_nf_regexps_exp
.clear();
4184 std::map
< Node
, std::vector
< Node
> > memb_with_exps
;
4185 std::map
< Node
, std::vector
< Node
> > XinR_with_exps
;
4187 addedLemma
= normalizePosMemberships( memb_with_exps
);
4190 addedLemma
|= checkMembershipsWithoutLength( memb_with_exps
, XinR_with_exps
);
4191 //TODO: check addlemma
4192 if (!addedLemma
&& !d_conflict
) {
4193 for(std::map
< Node
, std::vector
< Node
> >::const_iterator itr
= XinR_with_exps
.begin();
4194 itr
!= XinR_with_exps
.end(); ++itr
) {
4195 std::vector
<Node
> vec_or
;
4196 d_regexp_opr
.disjunctRegExp( itr
->first
, vec_or
);
4197 Node tmp
= NodeManager::currentNM()->mkNode(kind::REGEXP_UNION
, vec_or
);
4198 Trace("regexp-process") << "Got r: " << itr
->first
<< " to " << tmp
<< std::endl
;
4200 if(r.getKind() == kind::REGEXP_STAR) {
4202 addedLemma = applyRLen(XinR_with_exps);
4208 Assert(false); //TODO:tmp
4215 void TheoryStrings::checkMemberships() {
4216 //add the memberships
4217 for( NodeBoolMap::iterator it
= d_ext_func_terms
.begin(); it
!= d_ext_func_terms
.end(); ++it
){
4219 Node n
= (*it
).first
;
4220 if( n
.getKind()==kind::STRING_IN_REGEXP
) {
4221 Assert( d_extf_info_tmp
.find( n
)!=d_extf_info_tmp
.end() );
4222 Assert( d_extf_info_tmp
[n
].d_pol
==1 || d_extf_info_tmp
[n
].d_pol
==-1 );
4223 bool pol
= d_extf_info_tmp
[n
].d_pol
==1;
4224 Trace("strings-process-debug") << " add membership : " << n
<< ", pol = " << pol
<< std::endl
;
4225 addMembership( pol
? n
: n
.negate() );
4231 bool addedLemma
= false;
4232 bool changed
= false;
4233 std::vector
< Node
> processed
;
4234 std::vector
< Node
> cprocessed
;
4236 Trace("regexp-debug") << "Checking Memberships ... " << std::endl
;
4237 //if(options::stringEIT()) {
4238 //TODO: Opt for normal forms
4239 for( NodeIntMap::const_iterator itr_xr
= d_pos_memberships
.begin(); itr_xr
!= d_pos_memberships
.end(); ++itr_xr
){
4240 bool spflag
= false;
4241 Node x
= (*itr_xr
).first
;
4242 Trace("regexp-debug") << "Checking Memberships for " << x
<< std::endl
;
4243 if(d_inter_index
.find(x
) == d_inter_index
.end()) {
4244 d_inter_index
[x
] = 0;
4246 int cur_inter_idx
= d_inter_index
[x
];
4247 unsigned n_pmem
= (*itr_xr
).second
;
4248 Assert( getNumMemberships( x
, true )==n_pmem
);
4249 if( cur_inter_idx
!= (int)n_pmem
) {
4251 d_inter_cache
[x
] = getMembership( x
, true, 0 );
4252 d_inter_index
[x
] = 1;
4253 Trace("regexp-debug") << "... only one choice " << std::endl
;
4254 } else if(n_pmem
> 1) {
4256 if(d_inter_cache
.find(x
) != d_inter_cache
.end()) {
4257 r
= d_inter_cache
[x
];
4260 r
= getMembership( x
, true, 0 );
4264 unsigned k_start
= cur_inter_idx
;
4265 Trace("regexp-debug") << "... staring from : " << cur_inter_idx
<< ", we have " << n_pmem
<< std::endl
;
4266 for(unsigned k
= k_start
; k
<n_pmem
; k
++) {
4267 Node r2
= getMembership( x
, true, k
);
4268 r
= d_regexp_opr
.intersect(r
, r2
, spflag
);
4271 } else if(r
== d_emptyRegexp
) {
4272 std::vector
< Node
> vec_nodes
;
4273 for( unsigned kk
=0; kk
<=k
; kk
++ ){
4274 Node rr
= getMembership( x
, true, kk
);
4275 Node n
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, x
, rr
);
4276 vec_nodes
.push_back( n
);
4279 sendInference(vec_nodes
, conc
, "INTERSECT CONFLICT", true);
4288 if(!d_conflict
&& !spflag
) {
4289 d_inter_cache
[x
] = r
;
4290 d_inter_index
[x
] = (int)n_pmem
;
4297 Trace("regexp-debug") << "... No Intersect Conflict in Memberships, addedLemma: " << addedLemma
<< std::endl
;
4299 for( unsigned i
=0; i
<d_regexp_memberships
.size(); i
++ ) {
4300 //check regular expression membership
4301 Node assertion
= d_regexp_memberships
[i
];
4302 if( d_regexp_ucached
.find(assertion
) == d_regexp_ucached
.end()
4303 && d_regexp_ccached
.find(assertion
) == d_regexp_ccached
.end() ) {
4304 Trace("strings-regexp") << "We have regular expression assertion : " << assertion
<< std::endl
;
4305 Node atom
= assertion
.getKind()==kind::NOT
? assertion
[0] : assertion
;
4306 bool polarity
= assertion
.getKind()!=kind::NOT
;
4310 std::vector
< Node
> rnfexp
;
4312 //if(options::stringOpt1()) {
4315 x
= getNormalString( x
, rnfexp
);
4318 if(!d_regexp_opr
.checkConstRegExp(r
)) {
4319 r
= getNormalSymRegExp(r
, rnfexp
);
4322 Trace("strings-regexp-nf") << "Term " << atom
<< " is normalized to " << x
<< " IN " << r
<< std::endl
;
4324 Node tmp
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, x
, r
) );
4329 d_regexp_ccached
.insert(assertion
);
4331 } else if(tmp
== d_false
) {
4332 Node antec
= mkRegExpAntec(assertion
, mkExplain(rnfexp
));
4333 Node conc
= Node::null();
4334 sendLemma(antec
, conc
, "REGEXP NF Conflict");
4342 flag
= checkPDerivative(x
, r
, atom
, addedLemma
, processed
, cprocessed
, rnfexp
);
4343 if(options::stringOpt2() && flag
) {
4344 if(d_regexp_opr
.checkConstRegExp(r
) && x
.getKind()==kind::STRING_CONCAT
) {
4345 std::vector
< std::pair
< Node
, Node
> > vec_can
;
4346 d_regexp_opr
.splitRegExp(r
, vec_can
);
4347 //TODO: lazy cache or eager?
4348 std::vector
< Node
> vec_or
;
4349 std::vector
< Node
> vec_s2
;
4350 for(unsigned int s2i
=1; s2i
<x
.getNumChildren(); s2i
++) {
4351 vec_s2
.push_back(x
[s2i
]);
4354 Node s2
= mkConcat(vec_s2
);
4355 for(unsigned int i
=0; i
<vec_can
.size(); i
++) {
4356 Node m1
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s1
, vec_can
[i
].first
);
4357 Node m2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s2
, vec_can
[i
].second
);
4358 Node c
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND
, m1
, m2
) );
4359 vec_or
.push_back( c
);
4361 Node conc
= vec_or
.size()==1 ? vec_or
[0] : Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::OR
, vec_or
) );
4362 //Trace("regexp-split") << "R " << r << " to " << conc << std::endl;
4363 Node antec
= mkRegExpAntec(atom
, mkExplain(rnfexp
));
4364 if(conc
== d_true
) {
4366 cprocessed
.push_back( assertion
);
4368 processed
.push_back( assertion
);
4371 sendLemma(antec
, conc
, "RegExp-CST-SP");
4378 if(! options::stringExp()) {
4379 throw LogicException("Strings Incomplete (due to Negative Membership) by default, try --strings-exp option.");
4383 //check if the term is atomic
4384 Node xr
= getRepresentative( x
);
4385 //Trace("strings-regexp") << xr << " is rep of " << x << std::endl;
4386 //Assert( d_normal_forms.find( xr )!=d_normal_forms.end() );
4388 if( true || r
.getKind()!=kind::REGEXP_STAR
|| ( d_normal_forms
[xr
].size()==1 && x
.getKind()!=kind::STRING_CONCAT
) ){
4389 Trace("strings-regexp") << "Unroll/simplify membership of atomic term " << xr
<< std::endl
;
4390 //if so, do simple unrolling
4391 std::vector
< Node
> nvec
;
4393 /*if(xr.isConst()) {
4394 Node tmp = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, xr, r) );
4395 if(tmp==d_true || tmp==d_false) {
4397 tmp = tmp==d_true? d_false : d_true;
4399 nvec.push_back( tmp );
4404 d_regexp_opr
.simplify(atom
, nvec
, polarity
);
4406 Node antec
= assertion
;
4407 if(d_regexp_ant
.find(assertion
) != d_regexp_ant
.end()) {
4408 antec
= d_regexp_ant
[assertion
];
4409 for(std::vector
< Node
>::const_iterator itr
=nvec
.begin(); itr
<nvec
.end(); itr
++) {
4410 if(itr
->getKind() == kind::STRING_IN_REGEXP
) {
4411 if(d_regexp_ant
.find( *itr
) == d_regexp_ant
.end()) {
4412 d_regexp_ant
[ *itr
] = antec
;
4417 antec
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND
, antec
, mkExplain(rnfexp
)) );
4418 Node conc
= nvec
.size()==1 ? nvec
[0] : NodeManager::currentNM()->mkNode(kind::AND
, nvec
);
4419 conc
= Rewriter::rewrite(conc
);
4420 sendLemma( antec
, conc
, "REGEXP_Unfold" );
4423 cprocessed
.push_back( assertion
);
4425 processed
.push_back( assertion
);
4427 //d_regexp_ucached[assertion] = true;
4429 Trace("strings-regexp") << "Unroll/simplify membership of non-atomic term " << xr
<< " = ";
4430 for( unsigned j
=0; j
<d_normal_forms
[xr
].size(); j
++ ){
4431 Trace("strings-regexp") << d_normal_forms
[xr
][j
] << " ";
4433 Trace("strings-regexp") << ", polarity = " << polarity
<< std::endl
;
4434 //otherwise, distribute unrolling over parts
4437 if( d_normal_forms
[xr
].size()>1 ){
4438 p1
= d_normal_forms
[xr
][0];
4439 std::vector
< Node
> cc
;
4440 cc
.insert( cc
.begin(), d_normal_forms
[xr
].begin() + 1, d_normal_forms
[xr
].end() );
4441 p2
= mkConcat( cc
);
4444 Trace("strings-regexp-debug") << "Construct antecedant..." << std::endl
;
4445 std::vector
< Node
> antec
;
4446 std::vector
< Node
> antecn
;
4447 antec
.insert( antec
.begin(), d_normal_forms_exp
[xr
].begin(), d_normal_forms_exp
[xr
].end() );
4449 antec
.push_back( x
.eqNode( xr
) );
4451 antecn
.push_back( assertion
);
4452 Node ant
= mkExplain( antec
, antecn
);
4453 Trace("strings-regexp-debug") << "Construct conclusion..." << std::endl
;
4456 if( d_normal_forms
[xr
].size()==0 ){
4458 }else if( d_normal_forms
[xr
].size()==1 ){
4459 Trace("strings-regexp-debug") << "Case 1\n";
4460 conc
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, d_normal_forms
[xr
][0], r
);
4462 Trace("strings-regexp-debug") << "Case 2\n";
4463 std::vector
< Node
> conc_c
;
4464 Node s11
= mkSkolemS( "s11" );
4465 Node s12
= mkSkolemS( "s12" );
4466 Node s21
= mkSkolemS( "s21" );
4467 Node s22
= mkSkolemS( "s22" );
4468 conc
= p1
.eqNode( mkConcat(s11
, s12
) );
4469 conc_c
.push_back(conc
);
4470 conc
= p2
.eqNode( mkConcat(s21
, s22
) );
4471 conc_c
.push_back(conc
);
4472 conc
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s11
, r
);
4473 conc_c
.push_back(conc
);
4474 conc
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, mkConcat(s12
, s21
), r
[0]);
4475 conc_c
.push_back(conc
);
4476 conc
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s22
, r
);
4477 conc_c
.push_back(conc
);
4478 conc
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND
, conc_c
));
4479 Node eqz
= Rewriter::rewrite(x
.eqNode(d_emptyString
));
4480 conc
= NodeManager::currentNM()->mkNode(kind::OR
, eqz
, conc
);
4481 d_pending_req_phase
[eqz
] = true;
4484 if( d_normal_forms
[xr
].size()==0 ){
4486 }else if( d_normal_forms
[xr
].size()==1 ){
4487 Trace("strings-regexp-debug") << "Case 3\n";
4488 conc
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, d_normal_forms
[xr
][0], r
).negate();
4490 Trace("strings-regexp-debug") << "Case 4\n";
4491 Node len1
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, p1
);
4492 Node len2
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, p2
);
4493 Node bi
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
4494 Node bj
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
4495 Node b1v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, bi
, bj
);
4496 Node g1
= NodeManager::currentNM()->mkNode(kind::AND
,
4497 NodeManager::currentNM()->mkNode(kind::GEQ
, bi
, d_zero
),
4498 NodeManager::currentNM()->mkNode(kind::GEQ
, len1
, bi
),
4499 NodeManager::currentNM()->mkNode(kind::GEQ
, bj
, d_zero
),
4500 NodeManager::currentNM()->mkNode(kind::GEQ
, len2
, bj
));
4501 Node s11
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR
, p1
, d_zero
, bi
);
4502 Node s12
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR
, p1
, bi
, NodeManager::currentNM()->mkNode(kind::MINUS
, len1
, bi
));
4503 Node s21
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR
, p2
, d_zero
, bj
);
4504 Node s22
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR
, p2
, bj
, NodeManager::currentNM()->mkNode(kind::MINUS
, len2
, bj
));
4505 Node cc1
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s11
, r
).negate();
4506 Node cc2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, mkConcat(s12
, s21
), r
[0]).negate();
4507 Node cc3
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s22
, r
).negate();
4508 conc
= NodeManager::currentNM()->mkNode(kind::OR
, cc1
, cc2
, cc3
);
4509 conc
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, g1
, conc
);
4510 conc
= NodeManager::currentNM()->mkNode(kind::FORALL
, b1v
, conc
);
4511 conc
= NodeManager::currentNM()->mkNode(kind::AND
, x
.eqNode(d_emptyString
).negate(), conc
);
4515 ant
= mkRegExpAntec(assertion
, ant
);
4516 sendLemma(ant
, conc
, "REGEXP CSTAR");
4518 if( conc
==d_false
){
4519 d_regexp_ccached
.insert( assertion
);
4521 cprocessed
.push_back( assertion
);
4524 d_regexp_ccached
.insert(assertion
);
4536 for( unsigned i
=0; i
<processed
.size(); i
++ ) {
4537 d_regexp_ucached
.insert(processed
[i
]);
4539 for( unsigned i
=0; i
<cprocessed
.size(); i
++ ) {
4540 d_regexp_ccached
.insert(cprocessed
[i
]);
4546 bool TheoryStrings::checkPDerivative(Node x
, Node r
, Node atom
, bool &addedLemma
,
4547 std::vector
< Node
> &processed
, std::vector
< Node
> &cprocessed
, std::vector
< Node
> &nf_exp
) {
4549 Node antnf
= mkExplain(nf_exp
);
4551 if(areEqual(x
, d_emptyString
)) {
4553 switch(d_regexp_opr
.delta(r
, exp
)) {
4555 Node antec
= mkRegExpAntec(atom
, x
.eqNode(d_emptyString
));
4556 antec
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND
, antec
, antnf
));
4557 sendLemma(antec
, exp
, "RegExp Delta");
4559 d_regexp_ccached
.insert(atom
);
4563 d_regexp_ccached
.insert(atom
);
4567 Node antec
= mkRegExpAntec(atom
, x
.eqNode(d_emptyString
));
4568 antec
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND
, antec
, antnf
));
4569 Node conc
= Node::null();
4570 sendLemma(antec
, conc
, "RegExp Delta CONFLICT");
4572 d_regexp_ccached
.insert(atom
);
4580 /*Node xr = getRepresentative( x );
4582 Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, xr, r);
4583 Node nn = Rewriter::rewrite( n );
4585 d_regexp_ccached.insert(atom);
4587 } else if(nn == d_false) {
4588 Node antec = mkRegExpAntec(atom, x.eqNode(xr));
4589 Node conc = Node::null();
4590 sendLemma(antec, conc, "RegExp Delta CONFLICT");
4592 d_regexp_ccached.insert(atom);
4596 Node sREant
= mkRegExpAntec(atom
, d_true
);
4597 sREant
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND
, sREant
, antnf
));
4598 if(deriveRegExp( x
, r
, sREant
)) {
4600 processed
.push_back( atom
);
4607 CVC4::String
TheoryStrings::getHeadConst( Node x
) {
4609 return x
.getConst
< String
>();
4610 } else if( x
.getKind() == kind::STRING_CONCAT
) {
4611 if( x
[0].isConst() ) {
4612 return x
[0].getConst
< String
>();
4614 return d_emptyString
.getConst
< String
>();
4617 return d_emptyString
.getConst
< String
>();
4621 bool TheoryStrings::deriveRegExp( Node x
, Node r
, Node ant
) {
4623 Assert(x
!= d_emptyString
);
4624 Trace("regexp-derive") << "TheoryStrings::deriveRegExp: x=" << x
<< ", r= " << r
<< std::endl
;
4626 // Node n = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, r );
4627 // Node r = Rewriter::rewrite( n );
4629 // sendLemma(ant, r, "REGEXP REWRITE");
4633 CVC4::String s
= getHeadConst( x
);
4634 if( !s
.isEmptyString() && d_regexp_opr
.checkConstRegExp( r
) ) {
4635 Node conc
= Node::null();
4638 for(unsigned i
=0; i
<s
.size(); ++i
) {
4639 CVC4::String c
= s
.substr(i
, 1);
4641 int rt
= d_regexp_opr
.derivativeS(dc
, c
, dc2
);
4645 } else if(rt
== 2) {
4654 Assert(false, "Impossible: TheoryStrings::deriveRegExp: const string in const regular expression.");
4657 Assert( x
.getKind() == kind::STRING_CONCAT
);
4658 std::vector
< Node
> vec_nodes
;
4659 for(unsigned int i
=1; i
<x
.getNumChildren(); ++i
) {
4660 vec_nodes
.push_back( x
[i
] );
4662 Node left
= mkConcat( vec_nodes
);
4663 left
= Rewriter::rewrite( left
);
4664 conc
= NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP
, left
, dc
);
4666 /*std::vector< Node > sdc;
4667 d_regexp_opr.simplify(conc, sdc, true);
4668 if(sdc.size() == 1) {
4671 conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, conc));
4675 sendLemma(ant
, conc
, "RegExp-Derive");
4682 void TheoryStrings::addMembership(Node assertion
) {
4683 bool polarity
= assertion
.getKind() != kind::NOT
;
4684 TNode atom
= polarity
? assertion
: assertion
[0];
4689 NodeIntMap::const_iterator it
= d_pos_memberships
.find( x
);
4690 if( it
!=d_nf_pairs
.end() ){
4691 index
= (*it
).second
;
4692 for( int k
=0; k
<index
; k
++ ){
4693 if( k
<(int)d_pos_memberships_data
[x
].size() ){
4694 if( d_pos_memberships_data
[x
][k
]==r
){
4702 d_pos_memberships
[x
] = index
+ 1;
4703 if( index
<(int)d_pos_memberships_data
[x
].size() ){
4704 d_pos_memberships_data
[x
][index
] = r
;
4706 d_pos_memberships_data
[x
].push_back( r
);
4708 } else if(!options::stringIgnNegMembership()) {
4709 /*if(options::stringEIT() && d_regexp_opr.checkConstRegExp(r)) {
4711 Node r2 = d_regexp_opr.complement(r, rt);
4712 Node a = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r2);
4715 NodeIntMap::const_iterator it
= d_neg_memberships
.find( x
);
4716 if( it
!=d_nf_pairs
.end() ){
4717 index
= (*it
).second
;
4718 for( int k
=0; k
<index
; k
++ ){
4719 if( k
<(int)d_neg_memberships_data
[x
].size() ){
4720 if( d_neg_memberships_data
[x
][k
]==r
){
4728 d_neg_memberships
[x
] = index
+ 1;
4729 if( index
<(int)d_neg_memberships_data
[x
].size() ){
4730 d_neg_memberships_data
[x
][index
] = r
;
4732 d_neg_memberships_data
[x
].push_back( r
);
4736 if(polarity
|| !options::stringIgnNegMembership()) {
4737 d_regexp_memberships
.push_back( assertion
);
4741 Node
TheoryStrings::getNormalString( Node x
, std::vector
<Node
> &nf_exp
){
4743 Node xr
= getRepresentative( x
);
4744 if( d_normal_forms
.find( xr
) != d_normal_forms
.end() ){
4745 Node ret
= mkConcat( d_normal_forms
[xr
] );
4746 nf_exp
.insert( nf_exp
.end(), d_normal_forms_exp
[xr
].begin(), d_normal_forms_exp
[xr
].end() );
4747 addToExplanation( x
, d_normal_forms_base
[xr
], nf_exp
);
4748 Trace("strings-debug") << "Term: " << x
<< " has a normal form " << ret
<< std::endl
;
4751 if(x
.getKind() == kind::STRING_CONCAT
) {
4752 std::vector
< Node
> vec_nodes
;
4753 for(unsigned i
=0; i
<x
.getNumChildren(); i
++) {
4754 Node nc
= getNormalString( x
[i
], nf_exp
);
4755 vec_nodes
.push_back( nc
);
4757 return mkConcat( vec_nodes
);
4764 Node
TheoryStrings::getNormalSymRegExp(Node r
, std::vector
<Node
> &nf_exp
) {
4766 switch( r
.getKind() ) {
4767 case kind::REGEXP_EMPTY
:
4768 case kind::REGEXP_SIGMA
:
4770 case kind::STRING_TO_REGEXP
: {
4771 if(!r
[0].isConst()) {
4772 Node tmp
= getNormalString( r
[0], nf_exp
);
4774 ret
= NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, tmp
);
4779 case kind::REGEXP_CONCAT
: {
4780 std::vector
< Node
> vec_nodes
;
4781 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
4782 vec_nodes
.push_back( getNormalSymRegExp(r
[i
], nf_exp
) );
4784 ret
= mkConcat(vec_nodes
);
4787 case kind::REGEXP_UNION
: {
4788 std::vector
< Node
> vec_nodes
;
4789 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
4790 vec_nodes
.push_back( getNormalSymRegExp(r
[i
], nf_exp
) );
4792 ret
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_UNION
, vec_nodes
) );
4795 case kind::REGEXP_INTER
: {
4796 std::vector
< Node
> vec_nodes
;
4797 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
4798 vec_nodes
.push_back( getNormalSymRegExp(r
[i
], nf_exp
) );
4800 ret
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_INTER
, vec_nodes
) );
4803 case kind::REGEXP_STAR
: {
4804 ret
= getNormalSymRegExp( r
[0], nf_exp
);
4805 ret
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_STAR
, ret
) );
4808 //case kind::REGEXP_PLUS:
4809 //case kind::REGEXP_OPT:
4810 //case kind::REGEXP_RANGE:
4812 Trace("strings-error") << "Unsupported term: " << r
<< " in normalization SymRegExp." << std::endl
;
4814 //return Node::null();
4820 }/* CVC4::theory::strings namespace */
4821 }/* CVC4::theory namespace */
4822 }/* CVC4 namespace */