1 /********************* */
2 /*! \file theory_strings.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Tianyi Liang, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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/command.h"
24 #include "smt/logic_exception.h"
25 #include "smt/smt_statistics_registry.h"
26 #include "theory/ext_theory.h"
27 #include "theory/rewriter.h"
28 #include "theory/strings/theory_strings_rewriter.h"
29 #include "theory/strings/type_enumerator.h"
30 #include "theory/theory_model.h"
31 #include "theory/valuation.h"
34 using namespace CVC4::context
;
35 using namespace CVC4::kind
;
41 std::ostream
& operator<<(std::ostream
& out
, Inference i
)
45 case INFER_SSPLIT_CST_PROP
: out
<< "S-Split(CST-P)-prop"; break;
46 case INFER_SSPLIT_VAR_PROP
: out
<< "S-Split(VAR)-prop"; break;
47 case INFER_LEN_SPLIT
: out
<< "Len-Split(Len)"; break;
48 case INFER_LEN_SPLIT_EMP
: out
<< "Len-Split(Emp)"; break;
49 case INFER_SSPLIT_CST_BINARY
: out
<< "S-Split(CST-P)-binary"; break;
50 case INFER_SSPLIT_CST
: out
<< "S-Split(CST-P)"; break;
51 case INFER_SSPLIT_VAR
: out
<< "S-Split(VAR)"; break;
52 case INFER_FLOOP
: out
<< "F-Loop"; break;
53 default: out
<< "?"; break;
58 std::ostream
& operator<<(std::ostream
& out
, InferStep s
)
62 case BREAK
: out
<< "break"; break;
63 case CHECK_INIT
: out
<< "check_init"; break;
64 case CHECK_CONST_EQC
: out
<< "check_const_eqc"; break;
65 case CHECK_EXTF_EVAL
: out
<< "check_extf_eval"; break;
66 case CHECK_CYCLES
: out
<< "check_cycles"; break;
67 case CHECK_FLAT_FORMS
: out
<< "check_flat_forms"; break;
68 case CHECK_NORMAL_FORMS_EQ
: out
<< "check_normal_forms_eq"; break;
69 case CHECK_NORMAL_FORMS_DEQ
: out
<< "check_normal_forms_deq"; break;
70 case CHECK_CODES
: out
<< "check_codes"; break;
71 case CHECK_LENGTH_EQC
: out
<< "check_length_eqc"; break;
72 case CHECK_EXTF_REDUCTION
: out
<< "check_extf_reduction"; break;
73 case CHECK_MEMBERSHIP
: out
<< "check_membership"; break;
74 case CHECK_CARDINALITY
: out
<< "check_cardinality"; break;
75 default: out
<< "?"; break;
80 Node
TheoryStrings::TermIndex::add( TNode n
, unsigned index
, TheoryStrings
* t
, Node er
, std::vector
< Node
>& c
) {
81 if( index
==n
.getNumChildren() ){
82 if( d_data
.isNull() ){
87 Assert( index
<n
.getNumChildren() );
88 TNode nir
= t
->getRepresentative( n
[index
] );
89 //if it is empty, and doing CONCAT, ignore
90 if( nir
==er
&& n
.getKind()==kind::STRING_CONCAT
){
91 return add( n
, index
+1, t
, er
, c
);
94 return d_children
[nir
].add( n
, index
+1, t
, er
, c
);
99 TheoryStrings::TheoryStrings(context::Context
* c
,
100 context::UserContext
* u
,
103 const LogicInfo
& logicInfo
)
104 : Theory(THEORY_STRINGS
, c
, u
, out
, valuation
, logicInfo
),
106 d_equalityEngine(d_notify
, c
, "theory::strings", true),
107 d_conflict(c
, false),
111 d_pregistered_terms_cache(u
),
112 d_registered_terms_cache(u
),
113 d_length_lemma_terms_cache(u
),
114 d_preproc(&d_sk_cache
, u
),
115 d_extf_infer_cache(c
),
116 d_extf_infer_cache_u(u
),
117 d_ee_disequalities(c
),
120 d_proxy_var_to_length(u
),
122 d_has_extf(c
, false),
123 d_has_str_code(false),
124 d_regexp_solver(*this, c
, u
),
127 d_cardinality_lits(u
),
128 d_curr_cardinality(c
, 0),
130 d_strategy_init(false)
133 getExtTheory()->addFunctionKind(kind::STRING_SUBSTR
);
134 getExtTheory()->addFunctionKind(kind::STRING_STRIDOF
);
135 getExtTheory()->addFunctionKind(kind::STRING_ITOS
);
136 getExtTheory()->addFunctionKind(kind::STRING_STOI
);
137 getExtTheory()->addFunctionKind(kind::STRING_STRREPL
);
138 getExtTheory()->addFunctionKind(kind::STRING_STRREPLALL
);
139 getExtTheory()->addFunctionKind(kind::STRING_STRCTN
);
140 getExtTheory()->addFunctionKind(kind::STRING_IN_REGEXP
);
141 getExtTheory()->addFunctionKind(kind::STRING_LEQ
);
142 getExtTheory()->addFunctionKind(kind::STRING_CODE
);
144 // The kinds we are treating as function application in congruence
145 d_equalityEngine
.addFunctionKind(kind::STRING_LENGTH
);
146 d_equalityEngine
.addFunctionKind(kind::STRING_CONCAT
);
147 d_equalityEngine
.addFunctionKind(kind::STRING_IN_REGEXP
);
148 d_equalityEngine
.addFunctionKind(kind::STRING_CODE
);
149 if( options::stringLazyPreproc() ){
150 d_equalityEngine
.addFunctionKind(kind::STRING_STRCTN
);
151 d_equalityEngine
.addFunctionKind(kind::STRING_LEQ
);
152 d_equalityEngine
.addFunctionKind(kind::STRING_SUBSTR
);
153 d_equalityEngine
.addFunctionKind(kind::STRING_ITOS
);
154 d_equalityEngine
.addFunctionKind(kind::STRING_STOI
);
155 d_equalityEngine
.addFunctionKind(kind::STRING_STRIDOF
);
156 d_equalityEngine
.addFunctionKind(kind::STRING_STRREPL
);
157 d_equalityEngine
.addFunctionKind(kind::STRING_STRREPLALL
);
160 d_zero
= NodeManager::currentNM()->mkConst( Rational( 0 ) );
161 d_one
= NodeManager::currentNM()->mkConst( Rational( 1 ) );
162 d_neg_one
= NodeManager::currentNM()->mkConst(Rational(-1));
163 d_emptyString
= NodeManager::currentNM()->mkConst( ::CVC4::String("") );
164 d_true
= NodeManager::currentNM()->mkConst( true );
165 d_false
= NodeManager::currentNM()->mkConst( false );
167 d_card_size
= TheoryStringsRewriter::getAlphabetCardinality();
170 TheoryStrings::~TheoryStrings() {
171 for( std::map
< Node
, EqcInfo
* >::iterator it
= d_eqc_info
.begin(); it
!= d_eqc_info
.end(); ++it
){
176 Node
TheoryStrings::getRepresentative( Node t
) {
177 if( d_equalityEngine
.hasTerm( t
) ){
178 return d_equalityEngine
.getRepresentative( t
);
184 bool TheoryStrings::hasTerm( Node a
){
185 return d_equalityEngine
.hasTerm( a
);
188 bool TheoryStrings::areEqual( Node a
, Node b
){
191 }else if( hasTerm( a
) && hasTerm( b
) ){
192 return d_equalityEngine
.areEqual( a
, b
);
198 bool TheoryStrings::areDisequal( Node a
, Node b
){
202 if( hasTerm( a
) && hasTerm( b
) ) {
203 Node ar
= d_equalityEngine
.getRepresentative( a
);
204 Node br
= d_equalityEngine
.getRepresentative( b
);
205 return ( ar
!=br
&& ar
.isConst() && br
.isConst() ) || d_equalityEngine
.areDisequal( ar
, br
, false );
207 Node ar
= getRepresentative( a
);
208 Node br
= getRepresentative( b
);
209 return ar
!=br
&& ar
.isConst() && br
.isConst();
214 bool TheoryStrings::areCareDisequal( TNode x
, TNode y
) {
215 Assert( d_equalityEngine
.hasTerm(x
) );
216 Assert( d_equalityEngine
.hasTerm(y
) );
217 if( d_equalityEngine
.isTriggerTerm(x
, THEORY_STRINGS
) && d_equalityEngine
.isTriggerTerm(y
, THEORY_STRINGS
) ){
218 TNode x_shared
= d_equalityEngine
.getTriggerTermRepresentative(x
, THEORY_STRINGS
);
219 TNode y_shared
= d_equalityEngine
.getTriggerTermRepresentative(y
, THEORY_STRINGS
);
220 EqualityStatus eqStatus
= d_valuation
.getEqualityStatus(x_shared
, y_shared
);
221 if( eqStatus
==EQUALITY_FALSE_AND_PROPAGATED
|| eqStatus
==EQUALITY_FALSE
|| eqStatus
==EQUALITY_FALSE_IN_MODEL
){
228 Node
TheoryStrings::getLengthExp( Node t
, std::vector
< Node
>& exp
, Node te
){
229 Assert( areEqual( t
, te
) );
230 Node lt
= mkLength( te
);
232 // use own length if it exists, leads to shorter explanation
235 EqcInfo
* ei
= getOrMakeEqcInfo( t
, false );
236 Node length_term
= ei
? ei
->d_length_term
: Node::null();
237 if( length_term
.isNull() ){
238 //typically shouldnt be necessary
241 Debug("strings") << "TheoryStrings::getLengthTerm " << t
<< " is " << length_term
<< std::endl
;
242 addToExplanation( length_term
, te
, exp
);
243 return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, length_term
) );
247 Node
TheoryStrings::getLength( Node t
, std::vector
< Node
>& exp
) {
248 return getLengthExp( t
, exp
, t
);
251 Node
TheoryStrings::getNormalString(Node x
, std::vector
<Node
>& nf_exp
)
255 Node xr
= getRepresentative(x
);
256 if (d_normal_forms
.find(xr
) != d_normal_forms
.end())
258 Node ret
= mkConcat(d_normal_forms
[xr
]);
259 nf_exp
.insert(nf_exp
.end(),
260 d_normal_forms_exp
[xr
].begin(),
261 d_normal_forms_exp
[xr
].end());
262 addToExplanation(x
, d_normal_forms_base
[xr
], nf_exp
);
263 Trace("strings-debug")
264 << "Term: " << x
<< " has a normal form " << ret
<< std::endl
;
267 // if x does not have a normal form, then it should not occur in the
268 // equality engine and hence should be its own representative.
270 if (x
.getKind() == kind::STRING_CONCAT
)
272 std::vector
<Node
> vec_nodes
;
273 for (unsigned i
= 0; i
< x
.getNumChildren(); i
++)
275 Node nc
= getNormalString(x
[i
], nf_exp
);
276 vec_nodes
.push_back(nc
);
278 return mkConcat(vec_nodes
);
284 void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine
* eq
) {
285 d_equalityEngine
.setMasterEqualityEngine(eq
);
288 void TheoryStrings::addSharedTerm(TNode t
) {
289 Debug("strings") << "TheoryStrings::addSharedTerm(): "
290 << t
<< " " << t
.getType().isBoolean() << endl
;
291 d_equalityEngine
.addTriggerTerm(t
, THEORY_STRINGS
);
292 if (options::stringExp())
294 getExtTheory()->registerTermRec(t
);
296 Debug("strings") << "TheoryStrings::addSharedTerm() finished" << std::endl
;
299 EqualityStatus
TheoryStrings::getEqualityStatus(TNode a
, TNode b
) {
300 if( d_equalityEngine
.hasTerm(a
) && d_equalityEngine
.hasTerm(b
) ){
301 if (d_equalityEngine
.areEqual(a
, b
)) {
302 // The terms are implied to be equal
303 return EQUALITY_TRUE
;
305 if (d_equalityEngine
.areDisequal(a
, b
, false)) {
306 // The terms are implied to be dis-equal
307 return EQUALITY_FALSE
;
310 return EQUALITY_UNKNOWN
;
313 void TheoryStrings::propagate(Effort e
) {
314 // direct propagation now
317 bool TheoryStrings::propagate(TNode literal
) {
318 Debug("strings-propagate") << "TheoryStrings::propagate(" << literal
<< ")" << std::endl
;
319 // If already in conflict, no more propagation
321 Debug("strings-propagate") << "TheoryStrings::propagate(" << literal
<< "): already in conflict" << std::endl
;
325 bool ok
= d_out
->propagate(literal
);
333 void TheoryStrings::explain(TNode literal
, std::vector
<TNode
>& assumptions
) {
334 Debug("strings-explain") << "Explain " << literal
<< " " << d_conflict
<< std::endl
;
335 bool polarity
= literal
.getKind() != kind::NOT
;
336 TNode atom
= polarity
? literal
: literal
[0];
337 unsigned ps
= assumptions
.size();
338 std::vector
< TNode
> tassumptions
;
339 if (atom
.getKind() == kind::EQUAL
) {
340 if( atom
[0]!=atom
[1] ){
341 Assert( hasTerm( atom
[0] ) );
342 Assert( hasTerm( atom
[1] ) );
343 d_equalityEngine
.explainEquality(atom
[0], atom
[1], polarity
, tassumptions
);
346 d_equalityEngine
.explainPredicate(atom
, polarity
, tassumptions
);
348 for( unsigned i
=0; i
<tassumptions
.size(); i
++ ){
349 if( std::find( assumptions
.begin(), assumptions
.end(), tassumptions
[i
] )==assumptions
.end() ){
350 assumptions
.push_back( tassumptions
[i
] );
353 if (Debug
.isOn("strings-explain-debug"))
355 Debug("strings-explain-debug") << "Explanation for " << literal
<< " was "
357 for (unsigned i
= ps
; i
< assumptions
.size(); i
++)
359 Debug("strings-explain-debug") << " " << assumptions
[i
] << std::endl
;
364 Node
TheoryStrings::explain( TNode literal
){
365 Debug("strings-explain") << "explain called on " << literal
<< std::endl
;
366 std::vector
< TNode
> assumptions
;
367 explain( literal
, assumptions
);
368 if( assumptions
.empty() ){
370 }else if( assumptions
.size()==1 ){
371 return assumptions
[0];
373 return NodeManager::currentNM()->mkNode( kind::AND
, assumptions
);
377 bool TheoryStrings::getCurrentSubstitution( int effort
, std::vector
< Node
>& vars
,
378 std::vector
< Node
>& subs
, std::map
< Node
, std::vector
< Node
> >& exp
) {
379 Trace("strings-subs") << "getCurrentSubstitution, effort = " << effort
<< std::endl
;
380 for( unsigned i
=0; i
<vars
.size(); i
++ ){
382 Trace("strings-subs") << " get subs for " << n
<< "..." << std::endl
;
385 Node mv
= d_valuation
.getModel()->getRepresentative( n
);
386 Trace("strings-subs") << " model val : " << mv
<< std::endl
;
387 subs
.push_back( mv
);
389 Node nr
= getRepresentative( n
);
390 std::map
< Node
, Node
>::iterator itc
= d_eqc_to_const
.find( nr
);
391 if( itc
!=d_eqc_to_const
.end() ){
392 //constant equivalence classes
393 Trace("strings-subs") << " constant eqc : " << d_eqc_to_const_exp
[nr
] << " " << d_eqc_to_const_base
[nr
] << " " << nr
<< std::endl
;
394 subs
.push_back( itc
->second
);
395 if( !d_eqc_to_const_exp
[nr
].isNull() ){
396 exp
[n
].push_back( d_eqc_to_const_exp
[nr
] );
398 if( !d_eqc_to_const_base
[nr
].isNull() ){
399 addToExplanation( n
, d_eqc_to_const_base
[nr
], exp
[n
] );
401 }else if( effort
>=1 && effort
<3 && n
.getType().isString() ){
403 Node ns
= getNormalString( d_normal_forms_base
[nr
], exp
[n
] );
404 subs
.push_back( ns
);
405 Trace("strings-subs") << " normal eqc : " << ns
<< " " << d_normal_forms_base
[nr
] << " " << nr
<< std::endl
;
406 if( !d_normal_forms_base
[nr
].isNull() ) {
407 addToExplanation( n
, d_normal_forms_base
[nr
], exp
[n
] );
411 //Trace("strings-subs") << " representative : " << nr << std::endl;
412 //addToExplanation( n, nr, exp[n] );
413 //subs.push_back( nr );
421 bool TheoryStrings::doReduction(int effort
, Node n
, bool& isCd
)
423 Assert(d_extf_info_tmp
.find(n
) != d_extf_info_tmp
.end());
424 if (!d_extf_info_tmp
[n
].d_model_active
)
426 // n is not active in the model, no need to reduce
429 //determine the effort level to process the extf at
430 // 0 - at assertion time, 1+ - after no other reduction is applicable
432 // polarity : 1 true, -1 false, 0 neither
434 Kind k
= n
.getKind();
435 if (n
.getType().isBoolean() && !d_extf_info_tmp
[n
].d_const
.isNull())
437 pol
= d_extf_info_tmp
[n
].d_const
.getConst
<bool>() ? 1 : -1;
439 if (k
== STRING_STRCTN
)
451 std::vector
<Node
> lexp
;
452 Node lenx
= getLength(x
, lexp
);
453 Node lens
= getLength(s
, lexp
);
454 if (areEqual(lenx
, lens
))
456 Trace("strings-extf-debug")
457 << " resolve extf : " << n
458 << " based on equal lengths disequality." << std::endl
;
459 // We can reduce negative contains to a disequality when lengths are
460 // equal. In other words, len( x ) = len( s ) implies
461 // ~contains( x, s ) reduces to x != s.
462 if (!areDisequal(x
, s
))
464 // len( x ) = len( s ) ^ ~contains( x, s ) => x != s
465 lexp
.push_back(lenx
.eqNode(lens
));
466 lexp
.push_back(n
.negate());
467 Node xneqs
= x
.eqNode(s
).negate();
468 sendInference(lexp
, xneqs
, "NEG-CTN-EQL", true);
470 // this depends on the current assertions, so we set that this
471 // inference is context-dependent.
484 if (options::stringLazyPreproc())
486 if (k
== STRING_SUBSTR
)
490 else if (k
!= STRING_IN_REGEXP
)
496 if (effort
!= r_effort
)
498 // not the right effort level to reduce
501 Node c_n
= pol
== -1 ? n
.negate() : n
;
502 Trace("strings-process-debug")
503 << "Process reduction for " << n
<< ", pol = " << pol
<< std::endl
;
504 if (k
== STRING_STRCTN
&& pol
== 1)
508 // positive contains reduces to a equality
510 d_sk_cache
.mkSkolemCached(x
, s
, SkolemCache::SK_FIRST_CTN_PRE
, "sc1");
512 d_sk_cache
.mkSkolemCached(x
, s
, SkolemCache::SK_FIRST_CTN_POST
, "sc2");
513 Node eq
= Rewriter::rewrite(x
.eqNode(mkConcat(sk1
, s
, sk2
)));
514 std::vector
<Node
> exp_vec
;
515 exp_vec
.push_back(n
);
516 sendInference(d_empty_vec
, exp_vec
, eq
, "POS-CTN", true);
517 Trace("strings-extf-debug")
518 << " resolve extf : " << n
<< " based on positive contain reduction."
520 Trace("strings-red-lemma") << "Reduction (positive contains) lemma : " << n
521 << " => " << eq
<< std::endl
;
522 // context-dependent because it depends on the polarity of n itself
525 else if (k
!= kind::STRING_CODE
)
527 NodeManager
* nm
= NodeManager::currentNM();
528 Assert(k
== STRING_SUBSTR
|| k
== STRING_STRCTN
|| k
== STRING_STRIDOF
529 || k
== STRING_ITOS
|| k
== STRING_STOI
|| k
== STRING_STRREPL
530 || k
== STRING_STRREPLALL
|| k
== STRING_LEQ
);
531 std::vector
<Node
> new_nodes
;
532 Node res
= d_preproc
.simplify(n
, new_nodes
);
534 new_nodes
.push_back(res
.eqNode(n
));
536 new_nodes
.size() == 1 ? new_nodes
[0] : nm
->mkNode(AND
, new_nodes
);
537 nnlem
= Rewriter::rewrite(nnlem
);
538 Trace("strings-red-lemma")
539 << "Reduction_" << effort
<< " lemma : " << nnlem
<< std::endl
;
540 Trace("strings-red-lemma") << "...from " << n
<< std::endl
;
541 sendInference(d_empty_vec
, nnlem
, "Reduction", true);
542 Trace("strings-extf-debug")
543 << " resolve extf : " << n
<< " based on reduction." << std::endl
;
549 /////////////////////////////////////////////////////////////////////////////
551 /////////////////////////////////////////////////////////////////////////////
554 void TheoryStrings::presolve() {
555 Debug("strings-presolve") << "TheoryStrings::Presolving : get fmf options " << (options::stringFMF() ? "true" : "false") << std::endl
;
556 initializeStrategy();
558 // if strings fmf is enabled, register the strategy
559 if (options::stringFMF())
561 d_sslds
.reset(new StringSumLengthDecisionStrategy(
562 getSatContext(), getUserContext(), d_valuation
));
563 Trace("strings-dstrat-reg")
564 << "presolve: register decision strategy." << std::endl
;
565 std::vector
<Node
> inputVars
;
566 for (NodeSet::const_iterator itr
= d_input_vars
.begin();
567 itr
!= d_input_vars
.end();
570 inputVars
.push_back(*itr
);
572 d_sslds
->initialize(inputVars
);
573 getDecisionManager()->registerStrategy(
574 DecisionManager::STRAT_STRINGS_SUM_LENGTHS
, d_sslds
.get());
579 /////////////////////////////////////////////////////////////////////////////
581 /////////////////////////////////////////////////////////////////////////////
583 bool TheoryStrings::collectModelInfo(TheoryModel
* m
)
585 Trace("strings-model") << "TheoryStrings : Collect model info" << std::endl
;
586 Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl
;
588 std::set
<Node
> termSet
;
590 // Compute terms appearing in assertions and shared terms
591 computeRelevantTerms(termSet
);
592 // assert the (relevant) portion of the equality engine to the model
593 if (!m
->assertEqualityEngine(&d_equalityEngine
, &termSet
))
598 std::unordered_set
<Node
, NodeHashFunction
> repSet
;
599 NodeManager
* nm
= NodeManager::currentNM();
601 // get the relevant string equivalence classes
602 for (const Node
& s
: termSet
)
604 if (s
.getType().isString())
606 Node r
= getRepresentative(s
);
610 std::vector
<Node
> nodes(repSet
.begin(), repSet
.end());
611 std::map
< Node
, Node
> processed
;
612 std::vector
< std::vector
< Node
> > col
;
613 std::vector
< Node
> lts
;
614 separateByLength( nodes
, col
, lts
);
615 //step 1 : get all values for known lengths
616 std::vector
< Node
> lts_values
;
617 std::map
<unsigned, Node
> values_used
;
618 std::vector
<Node
> len_splits
;
619 for( unsigned i
=0; i
<col
.size(); i
++ ) {
620 Trace("strings-model") << "Checking length for {";
621 for( unsigned j
=0; j
<col
[i
].size(); j
++ ) {
623 Trace("strings-model") << ", ";
625 Trace("strings-model") << col
[i
][j
];
627 Trace("strings-model") << " } (length is " << lts
[i
] << ")" << std::endl
;
629 if( lts
[i
].isConst() ) {
632 else if (!lts
[i
].isNull())
634 // get the model value for lts[i]
635 len_value
= d_valuation
.getModelValue(lts
[i
]);
637 if (len_value
.isNull())
639 lts_values
.push_back(Node::null());
643 Assert(len_value
.getConst
<Rational
>() <= Rational(String::maxSize()),
644 "Exceeded UINT32_MAX in string model");
646 len_value
.getConst
<Rational
>().getNumerator().toUnsignedInt();
647 std::map
<unsigned, Node
>::iterator itvu
= values_used
.find(lvalue
);
648 if (itvu
== values_used
.end())
650 values_used
[lvalue
] = lts
[i
];
654 len_splits
.push_back(lts
[i
].eqNode(itvu
->second
));
656 lts_values
.push_back(len_value
);
659 ////step 2 : assign arbitrary values for unknown lengths?
660 // confirmed by calculus invariant, see paper
661 Trace("strings-model") << "Assign to equivalence classes..." << std::endl
;
662 std::map
<Node
, Node
> pure_eq_assign
;
663 //step 3 : assign values to equivalence classes that are pure variables
664 for( unsigned i
=0; i
<col
.size(); i
++ ){
665 std::vector
< Node
> pure_eq
;
666 Trace("strings-model") << "The (" << col
[i
].size()
667 << ") equivalence classes ";
668 for (const Node
& eqc
: col
[i
])
670 Trace("strings-model") << eqc
<< " ";
671 //check if col[i][j] has only variables
674 Assert(d_normal_forms
.find(eqc
) != d_normal_forms
.end());
675 if (d_normal_forms
[eqc
].size() == 1)
677 // does it have a code and the length of these equivalence classes are
679 if (d_has_str_code
&& lts_values
[i
] == d_one
)
681 EqcInfo
* eip
= getOrMakeEqcInfo(eqc
, false);
682 if (eip
&& !eip
->d_code_term
.get().isNull())
684 // its value must be equal to its code
685 Node ct
= nm
->mkNode(kind::STRING_CODE
, eip
->d_code_term
.get());
686 Node ctv
= d_valuation
.getModelValue(ct
);
688 ctv
.getConst
<Rational
>().getNumerator().toUnsignedInt();
689 Trace("strings-model") << "(code: " << cvalue
<< ") ";
690 std::vector
<unsigned> vec
;
691 vec
.push_back(String::convertCodeToUnsignedInt(cvalue
));
692 Node mv
= nm
->mkConst(String(vec
));
693 pure_eq_assign
[eqc
] = mv
;
694 m
->getEqualityEngine()->addTerm(mv
);
697 pure_eq
.push_back(eqc
);
702 processed
[eqc
] = eqc
;
705 Trace("strings-model") << "have length " << lts_values
[i
] << std::endl
;
707 //assign a new length if necessary
708 if( !pure_eq
.empty() ){
709 if( lts_values
[i
].isNull() ){
710 // start with length two (other lengths have special precendence)
712 while( values_used
.find( lvalue
)!=values_used
.end() ){
715 Trace("strings-model") << "*** Decide to make length of " << lvalue
<< std::endl
;
716 lts_values
[i
] = nm
->mkConst(Rational(lvalue
));
717 values_used
[lvalue
] = Node::null();
719 Trace("strings-model") << "Need to assign values of length " << lts_values
[i
] << " to equivalence classes ";
720 for( unsigned j
=0; j
<pure_eq
.size(); j
++ ){
721 Trace("strings-model") << pure_eq
[j
] << " ";
723 Trace("strings-model") << std::endl
;
725 //use type enumerator
726 Assert(lts_values
[i
].getConst
<Rational
>() <= Rational(String::maxSize()),
727 "Exceeded UINT32_MAX in string model");
728 StringEnumeratorLength
sel(lts_values
[i
].getConst
<Rational
>().getNumerator().toUnsignedInt());
729 for (const Node
& eqc
: pure_eq
)
732 std::map
<Node
, Node
>::iterator itp
= pure_eq_assign
.find(eqc
);
733 if (itp
== pure_eq_assign
.end())
735 Assert( !sel
.isFinished() );
737 while (m
->hasTerm(c
))
740 if (sel
.isFinished())
742 // We are in a case where model construction is impossible due to
743 // an insufficient number of constants of a given length.
745 // Consider an integer equivalence class E whose value is assigned
746 // n in the model. Let { S_1, ..., S_m } be the set of string
747 // equivalence classes such that len( x ) is a member of E for
748 // some member x of each class S1, ...,Sm. Since our calculus is
749 // saturated with respect to cardinality inference (see Liang
750 // et al, Figure 6, CAV 2014), we have that m <= A^n, where A is
751 // the cardinality of our alphabet.
753 // Now, consider the case where there exists two integer
754 // equivalence classes E1 and E2 that are assigned n, and moreover
755 // we did not received notification from arithmetic that E1 = E2.
756 // This typically should never happen, but assume in the following
759 // Now, it may be the case that there are string equivalence
760 // classes { S_1, ..., S_m1 } whose lengths are in E1,
761 // and classes { S'_1, ..., S'_m2 } whose lengths are in E2, where
762 // m1 + m2 > A^n. In this case, we have insufficient strings to
763 // assign to { S_1, ..., S_m1, S'_1, ..., S'_m2 }. If this
764 // happens, we add a split on len( u1 ) = len( u2 ) for some
765 // len( u1 ) in E1, len( u2 ) in E2. We do this for each pair of
766 // integer equivalence classes that are assigned to the same value
768 AlwaysAssert(!len_splits
.empty());
769 for (const Node
& sl
: len_splits
)
771 Node spl
= nm
->mkNode(OR
, sl
, sl
.negate());
784 Trace("strings-model") << "*** Assigned constant " << c
<< " for "
787 if (!m
->assertEquality(eqc
, c
, true))
794 Trace("strings-model") << "String Model : Pure Assigned." << std::endl
;
795 //step 4 : assign constants to all other equivalence classes
796 for( unsigned i
=0; i
<nodes
.size(); i
++ ){
797 if( processed
.find( nodes
[i
] )==processed
.end() ){
798 Assert( d_normal_forms
.find( nodes
[i
] )!=d_normal_forms
.end() );
799 Trace("strings-model") << "Construct model for " << nodes
[i
] << " based on normal form ";
800 for( unsigned j
=0; j
<d_normal_forms
[nodes
[i
]].size(); j
++ ) {
801 if( j
>0 ) Trace("strings-model") << " ++ ";
802 Trace("strings-model") << d_normal_forms
[nodes
[i
]][j
];
803 Node r
= getRepresentative( d_normal_forms
[nodes
[i
]][j
] );
804 if( !r
.isConst() && processed
.find( r
)==processed
.end() ){
805 Trace("strings-model") << "(UNPROCESSED)";
808 Trace("strings-model") << std::endl
;
809 std::vector
< Node
> nc
;
810 for( unsigned j
=0; j
<d_normal_forms
[nodes
[i
]].size(); j
++ ) {
811 Node r
= getRepresentative( d_normal_forms
[nodes
[i
]][j
] );
812 Assert( r
.isConst() || processed
.find( r
)!=processed
.end() );
813 nc
.push_back(r
.isConst() ? r
: processed
[r
]);
815 Node cc
= mkConcat( nc
);
816 Assert( cc
.getKind()==kind::CONST_STRING
);
817 Trace("strings-model") << "*** Determined constant " << cc
<< " for " << nodes
[i
] << std::endl
;
818 processed
[nodes
[i
]] = cc
;
819 if (!m
->assertEquality(nodes
[i
], cc
, true))
825 //Trace("strings-model") << "String Model : Assigned." << std::endl;
826 Trace("strings-model") << "String Model : Finished." << std::endl
;
830 /////////////////////////////////////////////////////////////////////////////
832 /////////////////////////////////////////////////////////////////////////////
835 void TheoryStrings::preRegisterTerm(TNode n
) {
836 if( d_pregistered_terms_cache
.find(n
) == d_pregistered_terms_cache
.end() ) {
837 d_pregistered_terms_cache
.insert(n
);
838 Trace("strings-preregister")
839 << "TheoryString::preregister : " << n
<< std::endl
;
840 //check for logic exceptions
841 Kind k
= n
.getKind();
842 if( !options::stringExp() ){
843 if (k
== kind::STRING_STRIDOF
|| k
== kind::STRING_ITOS
844 || k
== kind::STRING_STOI
|| k
== kind::STRING_STRREPL
845 || k
== kind::STRING_STRREPLALL
|| k
== kind::STRING_STRCTN
848 std::stringstream ss
;
849 ss
<< "Term of kind " << k
850 << " not supported in default mode, try --strings-exp";
851 throw LogicException(ss
.str());
857 d_equalityEngine
.addTriggerEquality(n
);
860 case kind::STRING_IN_REGEXP
: {
861 d_out
->requirePhase(n
, true);
862 d_equalityEngine
.addTriggerPredicate(n
);
863 d_equalityEngine
.addTerm(n
[0]);
864 d_equalityEngine
.addTerm(n
[1]);
869 TypeNode tn
= n
.getType();
870 if (tn
.isRegExp() && n
.isVar())
872 std::stringstream ss
;
873 ss
<< "Regular expression variables are not supported.";
874 throw LogicException(ss
.str());
876 if( tn
.isString() ) {
877 // all characters of constants should fall in the alphabet
880 std::vector
<unsigned> vec
= n
.getConst
<String
>().getVec();
881 for (unsigned u
: vec
)
883 if (u
>= d_card_size
)
885 std::stringstream ss
;
886 ss
<< "Characters in string \"" << n
887 << "\" are outside of the given alphabet.";
888 throw LogicException(ss
.str());
892 // if finite model finding is enabled,
893 // then we minimize the length of this term if it is a variable
894 // but not an internally generated Skolem, or a term that does
895 // not belong to this theory.
896 if (options::stringFMF()
897 && (n
.isVar() ? !d_sk_cache
.isSkolem(n
)
898 : kindToTheoryId(k
) != THEORY_STRINGS
))
900 d_input_vars
.insert(n
);
901 Trace("strings-dstrat-reg") << "input variable: " << n
<< std::endl
;
903 d_equalityEngine
.addTerm(n
);
904 } else if (tn
.isBoolean()) {
905 // Get triggered for both equal and dis-equal
906 d_equalityEngine
.addTriggerPredicate(n
);
908 // Function applications/predicates
909 d_equalityEngine
.addTerm(n
);
911 // Set d_functionsTerms stores all function applications that are
912 // relevant to theory combination. Notice that this is a subset of
913 // the applications whose kinds are function kinds in the equality
914 // engine. This means it does not include applications of operators
915 // like re.++, which is not a function kind in the equality engine.
916 // Concatenation terms do not need to be considered here because
917 // their arguments have string type and do not introduce any shared
919 if (n
.hasOperator() && d_equalityEngine
.isFunctionKind(k
)
920 && k
!= kind::STRING_CONCAT
)
922 d_functionsTerms
.push_back( n
);
929 Node
TheoryStrings::expandDefinition(LogicRequest
&logicRequest
, Node node
) {
930 Trace("strings-exp-def") << "TheoryStrings::expandDefinition : " << node
<< std::endl
;
934 void TheoryStrings::check(Effort e
) {
935 if (done() && e
<EFFORT_FULL
) {
939 TimerStat::CodeTimer
checkTimer(d_checkTime
);
944 if( !done() && !hasTerm( d_emptyString
) ) {
945 preRegisterTerm( d_emptyString
);
948 // Trace("strings-process") << "Theory of strings, check : " << e << std::endl;
949 Trace("strings-check") << "Theory of strings, check : " << e
<< std::endl
;
950 while ( !done() && !d_conflict
) {
951 // Get all the assertions
952 Assertion assertion
= get();
953 TNode fact
= assertion
.assertion
;
955 Trace("strings-assertion") << "get assertion: " << fact
<< endl
;
956 polarity
= fact
.getKind() != kind::NOT
;
957 atom
= polarity
? fact
: fact
[0];
959 //assert pending fact
960 assertPendingFact( atom
, polarity
, fact
);
964 Assert(d_strategy_init
);
965 std::map
<Effort
, std::pair
<unsigned, unsigned> >::iterator itsr
=
966 d_strat_steps
.find(e
);
967 if (!d_conflict
&& !d_valuation
.needCheck() && itsr
!= d_strat_steps
.end())
969 Trace("strings-check") << "Theory of strings " << e
<< " effort check "
971 if(Trace
.isOn("strings-eqc")) {
972 for( unsigned t
=0; t
<2; t
++ ) {
973 eq::EqClassesIterator eqcs2_i
= eq::EqClassesIterator( &d_equalityEngine
);
974 Trace("strings-eqc") << (t
==0 ? "STRINGS:" : "OTHER:") << std::endl
;
975 while( !eqcs2_i
.isFinished() ){
976 Node eqc
= (*eqcs2_i
);
977 bool print
= (t
==0 && eqc
.getType().isString() ) || (t
==1 && !eqc
.getType().isString() );
979 eq::EqClassIterator eqc2_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
980 Trace("strings-eqc") << "Eqc( " << eqc
<< " ) : { ";
981 while( !eqc2_i
.isFinished() ) {
982 if( (*eqc2_i
)!=eqc
&& (*eqc2_i
).getKind()!=kind::EQUAL
){
983 Trace("strings-eqc") << (*eqc2_i
) << " ";
987 Trace("strings-eqc") << " } " << std::endl
;
988 EqcInfo
* ei
= getOrMakeEqcInfo( eqc
, false );
990 Trace("strings-eqc-debug") << "* Length term : " << ei
->d_length_term
.get() << std::endl
;
991 Trace("strings-eqc-debug") << "* Cardinality lemma k : " << ei
->d_cardinality_lem_k
.get() << std::endl
;
992 Trace("strings-eqc-debug") << "* Normalization length lemma : " << ei
->d_normalized_length
.get() << std::endl
;
997 Trace("strings-eqc") << std::endl
;
999 Trace("strings-eqc") << std::endl
;
1001 unsigned sbegin
= itsr
->second
.first
;
1002 unsigned send
= itsr
->second
.second
;
1003 bool addedLemma
= false;
1006 runStrategy(sbegin
, send
);
1008 addedFact
= !d_pending
.empty();
1009 addedLemma
= !d_lemma_cache
.empty();
1012 // repeat if we did not add a lemma or conflict
1013 }while( !d_conflict
&& !addedLemma
&& addedFact
);
1015 Trace("strings-check") << "Theory of strings done full effort check " << addedLemma
<< " " << d_conflict
<< std::endl
;
1017 Trace("strings-check") << "Theory of strings, done check : " << e
<< std::endl
;
1018 Assert( d_pending
.empty() );
1019 Assert( d_lemma_cache
.empty() );
1022 bool TheoryStrings::needsCheckLastEffort() {
1023 if( options::stringGuessModel() ){
1024 return d_has_extf
.get();
1030 void TheoryStrings::checkExtfReductions( int effort
) {
1031 // Notice we don't make a standard call to ExtTheory::doReductions here,
1032 // since certain optimizations like context-dependent reductions and
1033 // stratifying effort levels are done in doReduction below.
1034 std::vector
< Node
> extf
= getExtTheory()->getActive();
1035 Trace("strings-process") << " checking " << extf
.size() << " active extf"
1037 for( unsigned i
=0; i
<extf
.size(); i
++ ){
1038 Assert(!d_conflict
);
1040 Trace("strings-process") << " check " << n
<< ", active in model="
1041 << d_extf_info_tmp
[n
].d_model_active
<< std::endl
;
1042 // whether the reduction was context-dependent
1044 bool ret
= doReduction(effort
, n
, isCd
);
1047 getExtTheory()->markReduced(extf
[i
], isCd
);
1056 void TheoryStrings::checkMemberships()
1058 // add the memberships
1059 std::vector
<Node
> mems
= getExtTheory()->getActive(kind::STRING_IN_REGEXP
);
1060 for (unsigned i
= 0; i
< mems
.size(); i
++)
1063 Assert(d_extf_info_tmp
.find(n
) != d_extf_info_tmp
.end());
1064 if (!d_extf_info_tmp
[n
].d_const
.isNull())
1066 bool pol
= d_extf_info_tmp
[n
].d_const
.getConst
<bool>();
1067 Trace("strings-process-debug")
1068 << " add membership : " << n
<< ", pol = " << pol
<< std::endl
;
1069 d_regexp_solver
.addMembership(pol
? n
: n
.negate());
1073 Trace("strings-process-debug")
1074 << " irrelevant (non-asserted) membership : " << n
<< std::endl
;
1077 d_regexp_solver
.check();
1080 TheoryStrings::EqcInfo::EqcInfo(context::Context
* c
)
1083 d_cardinality_lem_k(c
),
1084 d_normalized_length(c
)
1088 TheoryStrings::EqcInfo
* TheoryStrings::getOrMakeEqcInfo( Node eqc
, bool doMake
) {
1089 std::map
< Node
, EqcInfo
* >::iterator eqc_i
= d_eqc_info
.find( eqc
);
1090 if( eqc_i
==d_eqc_info
.end() ){
1092 EqcInfo
* ei
= new EqcInfo( getSatContext() );
1093 d_eqc_info
[eqc
] = ei
;
1099 return (*eqc_i
).second
;
1104 /** Conflict when merging two constants */
1105 void TheoryStrings::conflict(TNode a
, TNode b
){
1107 Debug("strings-conflict") << "Making conflict..." << std::endl
;
1110 conflictNode
= explain( a
.eqNode(b
) );
1111 Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode
<< std::endl
;
1112 d_out
->conflict( conflictNode
);
1116 /** called when a new equivalance class is created */
1117 void TheoryStrings::eqNotifyNewClass(TNode t
){
1118 Kind k
= t
.getKind();
1119 if (k
== kind::STRING_LENGTH
|| k
== kind::STRING_CODE
)
1121 Trace("strings-debug") << "New length eqc : " << t
<< std::endl
;
1122 Node r
= d_equalityEngine
.getRepresentative(t
[0]);
1123 EqcInfo
* ei
= getOrMakeEqcInfo( r
, true );
1124 if (k
== kind::STRING_LENGTH
)
1126 ei
->d_length_term
= t
[0];
1130 ei
->d_code_term
= t
[0];
1132 //we care about the length of this string
1133 registerTerm( t
[0], 1 );
1135 //getExtTheory()->registerTerm( t );
1139 /** called when two equivalance classes will merge */
1140 void TheoryStrings::eqNotifyPreMerge(TNode t1
, TNode t2
){
1141 EqcInfo
* e2
= getOrMakeEqcInfo(t2
, false);
1143 EqcInfo
* e1
= getOrMakeEqcInfo( t1
);
1144 //add information from e2 to e1
1145 if( !e2
->d_length_term
.get().isNull() ){
1146 e1
->d_length_term
.set( e2
->d_length_term
);
1148 if (!e2
->d_code_term
.get().isNull())
1150 e1
->d_code_term
.set(e2
->d_code_term
);
1152 if( e2
->d_cardinality_lem_k
.get()>e1
->d_cardinality_lem_k
.get() ) {
1153 e1
->d_cardinality_lem_k
.set( e2
->d_cardinality_lem_k
);
1155 if( !e2
->d_normalized_length
.get().isNull() ){
1156 e1
->d_normalized_length
.set( e2
->d_normalized_length
);
1161 /** called when two equivalance classes have merged */
1162 void TheoryStrings::eqNotifyPostMerge(TNode t1
, TNode t2
) {
1166 /** called when two equivalance classes are disequal */
1167 void TheoryStrings::eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
) {
1168 if( t1
.getType().isString() ){
1169 //store disequalities between strings, may need to check if their lengths are equal/disequal
1170 d_ee_disequalities
.push_back( t1
.eqNode( t2
) );
1174 void TheoryStrings::addCarePairs(TNodeTrie
* t1
,
1181 Node f1
= t1
->getData();
1182 Node f2
= t2
->getData();
1183 if( !d_equalityEngine
.areEqual( f1
, f2
) ){
1184 Trace("strings-cg-debug") << "TheoryStrings::computeCareGraph(): checking function " << f1
<< " and " << f2
<< std::endl
;
1185 vector
< pair
<TNode
, TNode
> > currentPairs
;
1186 for (unsigned k
= 0; k
< f1
.getNumChildren(); ++ k
) {
1189 Assert( d_equalityEngine
.hasTerm(x
) );
1190 Assert( d_equalityEngine
.hasTerm(y
) );
1191 Assert( !d_equalityEngine
.areDisequal( x
, y
, false ) );
1192 Assert( !areCareDisequal( x
, y
) );
1193 if( !d_equalityEngine
.areEqual( x
, y
) ){
1194 if( d_equalityEngine
.isTriggerTerm(x
, THEORY_STRINGS
) && d_equalityEngine
.isTriggerTerm(y
, THEORY_STRINGS
) ){
1195 TNode x_shared
= d_equalityEngine
.getTriggerTermRepresentative(x
, THEORY_STRINGS
);
1196 TNode y_shared
= d_equalityEngine
.getTriggerTermRepresentative(y
, THEORY_STRINGS
);
1197 currentPairs
.push_back(make_pair(x_shared
, y_shared
));
1201 for (unsigned c
= 0; c
< currentPairs
.size(); ++ c
) {
1202 Trace("strings-cg-pair") << "TheoryStrings::computeCareGraph(): pair : " << currentPairs
[c
].first
<< " " << currentPairs
[c
].second
<< std::endl
;
1203 addCarePair(currentPairs
[c
].first
, currentPairs
[c
].second
);
1209 if( depth
<(arity
-1) ){
1210 //add care pairs internal to each child
1211 for (std::pair
<const TNode
, TNodeTrie
>& tt
: t1
->d_data
)
1213 addCarePairs(&tt
.second
, nullptr, arity
, depth
+ 1);
1216 //add care pairs based on each pair of non-disequal arguments
1217 for (std::map
<TNode
, TNodeTrie
>::iterator it
= t1
->d_data
.begin();
1218 it
!= t1
->d_data
.end();
1221 std::map
<TNode
, TNodeTrie
>::iterator it2
= it
;
1223 for( ; it2
!= t1
->d_data
.end(); ++it2
){
1224 if( !d_equalityEngine
.areDisequal(it
->first
, it2
->first
, false) ){
1225 if( !areCareDisequal(it
->first
, it2
->first
) ){
1226 addCarePairs( &it
->second
, &it2
->second
, arity
, depth
+1 );
1232 //add care pairs based on product of indices, non-disequal arguments
1233 for (std::pair
<const TNode
, TNodeTrie
>& tt1
: t1
->d_data
)
1235 for (std::pair
<const TNode
, TNodeTrie
>& tt2
: t2
->d_data
)
1237 if (!d_equalityEngine
.areDisequal(tt1
.first
, tt2
.first
, false))
1239 if (!areCareDisequal(tt1
.first
, tt2
.first
))
1241 addCarePairs(&tt1
.second
, &tt2
.second
, arity
, depth
+ 1);
1250 void TheoryStrings::computeCareGraph(){
1251 //computing the care graph here is probably still necessary, due to operators that take non-string arguments TODO: verify
1252 Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Build term indices..." << std::endl
;
1253 std::map
<Node
, TNodeTrie
> index
;
1254 std::map
< Node
, unsigned > arity
;
1255 unsigned functionTerms
= d_functionsTerms
.size();
1256 for (unsigned i
= 0; i
< functionTerms
; ++ i
) {
1257 TNode f1
= d_functionsTerms
[i
];
1258 Trace("strings-cg") << "...build for " << f1
<< std::endl
;
1259 Node op
= f1
.getOperator();
1260 std::vector
< TNode
> reps
;
1261 bool has_trigger_arg
= false;
1262 for( unsigned j
=0; j
<f1
.getNumChildren(); j
++ ){
1263 reps
.push_back( d_equalityEngine
.getRepresentative( f1
[j
] ) );
1264 if( d_equalityEngine
.isTriggerTerm( f1
[j
], THEORY_STRINGS
) ){
1265 has_trigger_arg
= true;
1268 if( has_trigger_arg
){
1269 index
[op
].addTerm( f1
, reps
);
1270 arity
[op
] = reps
.size();
1274 for (std::pair
<const Node
, TNodeTrie
>& tt
: index
)
1276 Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Process index "
1277 << tt
.first
<< "..." << std::endl
;
1278 addCarePairs(&tt
.second
, nullptr, arity
[tt
.first
], 0);
1282 void TheoryStrings::assertPendingFact(Node atom
, bool polarity
, Node exp
) {
1283 Trace("strings-pending") << "Assert pending fact : " << atom
<< " " << polarity
<< " from " << exp
<< std::endl
;
1284 Assert(atom
.getKind() != kind::OR
, "Infer error: a split.");
1285 if( atom
.getKind()==kind::EQUAL
){
1286 Trace("strings-pending-debug") << " Register term" << std::endl
;
1287 for( unsigned j
=0; j
<2; j
++ ) {
1288 if( !d_equalityEngine
.hasTerm( atom
[j
] ) && atom
[j
].getType().isString() ) {
1289 registerTerm( atom
[j
], 0 );
1292 Trace("strings-pending-debug") << " Now assert equality" << std::endl
;
1293 d_equalityEngine
.assertEquality( atom
, polarity
, exp
);
1294 Trace("strings-pending-debug") << " Finished assert equality" << std::endl
;
1296 d_equalityEngine
.assertPredicate( atom
, polarity
, exp
);
1298 if( atom
.getKind()==kind::STRING_IN_REGEXP
){
1299 if( polarity
&& atom
[1].getKind()==kind::REGEXP_RANGE
){
1300 if( d_extf_infer_cache_u
.find( atom
)==d_extf_infer_cache_u
.end() ){
1301 d_extf_infer_cache_u
.insert( atom
);
1302 //length of first argument is one
1303 Node conc
= d_one
.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, atom
[0] ) );
1304 Node lem
= NodeManager::currentNM()->mkNode( kind::OR
, atom
.negate(), conc
);
1305 Trace("strings-lemma") << "Strings::Lemma RE-Range-Len : " << lem
<< std::endl
;
1306 d_out
->lemma( lem
);
1310 //register the atom here, since it may not create a new equivalence class
1311 //getExtTheory()->registerTerm( atom );
1313 Trace("strings-pending-debug") << " Now collect terms" << std::endl
;
1314 // Collect extended function terms in the atom. Notice that we must register
1315 // all extended functions occurring in assertions and shared terms. We
1316 // make a similar call to registerTermRec in addSharedTerm.
1317 getExtTheory()->registerTermRec( atom
);
1318 Trace("strings-pending-debug") << " Finished collect terms" << std::endl
;
1321 void TheoryStrings::doPendingFacts() {
1323 while( !d_conflict
&& i
<d_pending
.size() ) {
1324 Node fact
= d_pending
[i
];
1325 Node exp
= d_pending_exp
[ fact
];
1326 if(fact
.getKind() == kind::AND
) {
1327 for(size_t j
=0; j
<fact
.getNumChildren(); j
++) {
1328 bool polarity
= fact
[j
].getKind() != kind::NOT
;
1329 TNode atom
= polarity
? fact
[j
] : fact
[j
][0];
1330 assertPendingFact(atom
, polarity
, exp
);
1333 bool polarity
= fact
.getKind() != kind::NOT
;
1334 TNode atom
= polarity
? fact
: fact
[0];
1335 assertPendingFact(atom
, polarity
, exp
);
1340 d_pending_exp
.clear();
1343 void TheoryStrings::doPendingLemmas() {
1344 if( !d_conflict
&& !d_lemma_cache
.empty() ){
1345 for( unsigned i
=0; i
<d_lemma_cache
.size(); i
++ ){
1346 Trace("strings-pending") << "Process pending lemma : " << d_lemma_cache
[i
] << std::endl
;
1347 d_out
->lemma( d_lemma_cache
[i
] );
1349 for( std::map
< Node
, bool >::iterator it
= d_pending_req_phase
.begin(); it
!= d_pending_req_phase
.end(); ++it
){
1350 Trace("strings-pending") << "Require phase : " << it
->first
<< ", polarity = " << it
->second
<< std::endl
;
1351 d_out
->requirePhase( it
->first
, it
->second
);
1354 d_lemma_cache
.clear();
1355 d_pending_req_phase
.clear();
1358 bool TheoryStrings::hasProcessed() {
1359 return d_conflict
|| !d_lemma_cache
.empty() || !d_pending
.empty();
1362 void TheoryStrings::addToExplanation( Node a
, Node b
, std::vector
< Node
>& exp
) {
1364 Debug("strings-explain") << "Add to explanation : " << a
<< " == " << b
<< std::endl
;
1365 Assert( areEqual( a
, b
) );
1366 exp
.push_back( a
.eqNode( b
) );
1370 void TheoryStrings::addToExplanation( Node lit
, std::vector
< Node
>& exp
) {
1371 if( !lit
.isNull() ){
1372 exp
.push_back( lit
);
1376 void TheoryStrings::checkInit() {
1378 d_eqc_to_const
.clear();
1379 d_eqc_to_const_base
.clear();
1380 d_eqc_to_const_exp
.clear();
1381 d_eqc_to_len_term
.clear();
1382 d_term_index
.clear();
1383 d_strings_eqc
.clear();
1385 std::map
< Kind
, unsigned > ncongruent
;
1386 std::map
< Kind
, unsigned > congruent
;
1387 d_emptyString_r
= getRepresentative( d_emptyString
);
1388 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( &d_equalityEngine
);
1389 while( !eqcs_i
.isFinished() ){
1390 Node eqc
= (*eqcs_i
);
1391 TypeNode tn
= eqc
.getType();
1392 if( !tn
.isRegExp() ){
1393 if( tn
.isString() ){
1394 d_strings_eqc
.push_back( eqc
);
1397 eq::EqClassIterator eqc_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
1398 while( !eqc_i
.isFinished() ) {
1401 d_eqc_to_const
[eqc
] = n
;
1402 d_eqc_to_const_base
[eqc
] = n
;
1403 d_eqc_to_const_exp
[eqc
] = Node::null();
1404 }else if( tn
.isInteger() ){
1405 if( n
.getKind()==kind::STRING_LENGTH
){
1406 Node nr
= getRepresentative( n
[0] );
1407 d_eqc_to_len_term
[nr
] = n
[0];
1409 }else if( n
.getNumChildren()>0 ){
1410 Kind k
= n
.getKind();
1411 if( k
!=kind::EQUAL
){
1412 if( d_congruent
.find( n
)==d_congruent
.end() ){
1413 std::vector
< Node
> c
;
1414 Node nc
= d_term_index
[k
].add( n
, 0, this, d_emptyString_r
, c
);
1416 //check if we have inferred a new equality by removal of empty components
1417 if( n
.getKind()==kind::STRING_CONCAT
&& !areEqual( nc
, n
) ){
1418 std::vector
< Node
> exp
;
1419 unsigned count
[2] = { 0, 0 };
1420 while( count
[0]<nc
.getNumChildren() || count
[1]<n
.getNumChildren() ){
1421 //explain empty prefixes
1422 for( unsigned t
=0; t
<2; t
++ ){
1423 Node nn
= t
==0 ? nc
: n
;
1424 while( count
[t
]<nn
.getNumChildren() &&
1425 ( nn
[count
[t
]]==d_emptyString
|| areEqual( nn
[count
[t
]], d_emptyString
) ) ){
1426 if( nn
[count
[t
]]!=d_emptyString
){
1427 exp
.push_back( nn
[count
[t
]].eqNode( d_emptyString
) );
1432 //explain equal components
1433 if( count
[0]<nc
.getNumChildren() ){
1434 Assert( count
[1]<n
.getNumChildren() );
1435 if( nc
[count
[0]]!=n
[count
[1]] ){
1436 exp
.push_back( nc
[count
[0]].eqNode( n
[count
[1]] ) );
1442 //infer the equality
1443 sendInference( exp
, n
.eqNode( nc
), "I_Norm" );
1444 }else if( getExtTheory()->hasFunctionKind( n
.getKind() ) ){
1445 //mark as congruent : only process if neither has been reduced
1446 getExtTheory()->markCongruent( nc
, n
);
1448 //this node is congruent to another one, we can ignore it
1449 Trace("strings-process-debug") << " congruent term : " << n
<< std::endl
;
1450 d_congruent
.insert( n
);
1452 }else if( k
==kind::STRING_CONCAT
&& c
.size()==1 ){
1453 Trace("strings-process-debug") << " congruent term by singular : " << n
<< " " << c
[0] << std::endl
;
1455 if( !areEqual( c
[0], n
) ){
1456 std::vector
< Node
> exp
;
1457 //explain empty components
1458 bool foundNEmpty
= false;
1459 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1460 if( areEqual( n
[i
], d_emptyString
) ){
1461 if( n
[i
]!=d_emptyString
){
1462 exp
.push_back( n
[i
].eqNode( d_emptyString
) );
1465 Assert( !foundNEmpty
);
1467 exp
.push_back( n
[i
].eqNode( c
[0] ) );
1472 AlwaysAssert( foundNEmpty
);
1473 //infer the equality
1474 sendInference( exp
, n
.eqNode( c
[0] ), "I_Norm_S" );
1476 d_congruent
.insert( n
);
1486 if( d_congruent
.find( n
)==d_congruent
.end() ){
1490 Trace("strings-process-debug") << " congruent variable : " << n
<< std::endl
;
1491 d_congruent
.insert( n
);
1500 if( Trace
.isOn("strings-process") ){
1501 for( std::map
< Kind
, TermIndex
>::iterator it
= d_term_index
.begin(); it
!= d_term_index
.end(); ++it
){
1502 Trace("strings-process") << " Terms[" << it
->first
<< "] = " << ncongruent
[it
->first
] << "/" << (congruent
[it
->first
]+ncongruent
[it
->first
]) << std::endl
;
1507 void TheoryStrings::checkConstantEquivalenceClasses()
1511 std::vector
<Node
> vecc
;
1515 Trace("strings-process-debug") << "Check constant equivalence classes..."
1517 prevSize
= d_eqc_to_const
.size();
1518 checkConstantEquivalenceClasses(&d_term_index
[kind::STRING_CONCAT
], vecc
);
1519 } while (!hasProcessed() && d_eqc_to_const
.size() > prevSize
);
1522 void TheoryStrings::checkConstantEquivalenceClasses( TermIndex
* ti
, std::vector
< Node
>& vecc
) {
1523 Node n
= ti
->d_data
;
1525 //construct the constant
1526 Node c
= mkConcat( vecc
);
1527 if( !areEqual( n
, c
) ){
1528 Trace("strings-debug") << "Constant eqc : " << c
<< " for " << n
<< std::endl
;
1529 Trace("strings-debug") << " ";
1530 for( unsigned i
=0; i
<vecc
.size(); i
++ ){
1531 Trace("strings-debug") << vecc
[i
] << " ";
1533 Trace("strings-debug") << std::endl
;
1535 unsigned countc
= 0;
1536 std::vector
< Node
> exp
;
1537 while( count
<n
.getNumChildren() ){
1538 while( count
<n
.getNumChildren() && areEqual( n
[count
], d_emptyString
) ){
1539 addToExplanation( n
[count
], d_emptyString
, exp
);
1542 if( count
<n
.getNumChildren() ){
1543 Trace("strings-debug") << "...explain " << n
[count
] << " " << vecc
[countc
] << std::endl
;
1544 if( !areEqual( n
[count
], vecc
[countc
] ) ){
1545 Node nrr
= getRepresentative( n
[count
] );
1546 Assert( !d_eqc_to_const_exp
[nrr
].isNull() );
1547 addToExplanation( n
[count
], d_eqc_to_const_base
[nrr
], exp
);
1548 exp
.push_back( d_eqc_to_const_exp
[nrr
] );
1550 addToExplanation( n
[count
], vecc
[countc
], exp
);
1556 //exp contains an explanation of n==c
1557 Assert( countc
==vecc
.size() );
1559 sendInference( exp
, n
.eqNode( c
), "I_CONST_MERGE" );
1561 }else if( !hasProcessed() ){
1562 Node nr
= getRepresentative( n
);
1563 std::map
< Node
, Node
>::iterator it
= d_eqc_to_const
.find( nr
);
1564 if( it
==d_eqc_to_const
.end() ){
1565 Trace("strings-debug") << "Set eqc const " << n
<< " to " << c
<< std::endl
;
1566 d_eqc_to_const
[nr
] = c
;
1567 d_eqc_to_const_base
[nr
] = n
;
1568 d_eqc_to_const_exp
[nr
] = mkAnd( exp
);
1569 }else if( c
!=it
->second
){
1571 Trace("strings-debug") << "Conflict, other constant was " << it
->second
<< ", this constant was " << c
<< std::endl
;
1572 if( d_eqc_to_const_exp
[nr
].isNull() ){
1573 // n==c ^ n == c' => false
1574 addToExplanation( n
, it
->second
, exp
);
1576 // n==c ^ n == d_eqc_to_const_base[nr] == c' => false
1577 exp
.push_back( d_eqc_to_const_exp
[nr
] );
1578 addToExplanation( n
, d_eqc_to_const_base
[nr
], exp
);
1580 sendInference( exp
, d_false
, "I_CONST_CONFLICT" );
1583 Trace("strings-debug") << "Duplicate constant." << std::endl
;
1588 for( std::map
< TNode
, TermIndex
>::iterator it
= ti
->d_children
.begin(); it
!= ti
->d_children
.end(); ++it
){
1589 std::map
< Node
, Node
>::iterator itc
= d_eqc_to_const
.find( it
->first
);
1590 if( itc
!=d_eqc_to_const
.end() ){
1591 vecc
.push_back( itc
->second
);
1592 checkConstantEquivalenceClasses( &it
->second
, vecc
);
1594 if( hasProcessed() ){
1601 void TheoryStrings::checkExtfEval( int effort
) {
1602 Trace("strings-extf-list") << "Active extended functions, effort=" << effort
<< " : " << std::endl
;
1603 d_extf_info_tmp
.clear();
1604 bool has_nreduce
= false;
1605 std::vector
< Node
> terms
= getExtTheory()->getActive();
1606 std::vector
< Node
> sterms
;
1607 std::vector
< std::vector
< Node
> > exp
;
1608 getExtTheory()->getSubstitutedTerms( effort
, terms
, sterms
, exp
);
1609 for( unsigned i
=0; i
<terms
.size(); i
++ ){
1611 Node sn
= sterms
[i
];
1612 //setup information about extf
1613 ExtfInfoTmp
& einfo
= d_extf_info_tmp
[n
];
1614 Node r
= getRepresentative(n
);
1615 std::map
<Node
, Node
>::iterator itcit
= d_eqc_to_const
.find(r
);
1616 if (itcit
!= d_eqc_to_const
.end())
1618 einfo
.d_const
= itcit
->second
;
1620 Trace("strings-extf-debug") << "Check extf " << n
<< " == " << sn
1621 << ", constant = " << einfo
.d_const
1622 << ", effort=" << effort
<< "..." << std::endl
;
1626 einfo
.d_exp
.insert(einfo
.d_exp
.end(), exp
[i
].begin(), exp
[i
].end());
1627 // inference is rewriting the substituted node
1628 Node nrc
= Rewriter::rewrite( sn
);
1629 //if rewrites to a constant, then do the inference and mark as reduced
1630 if( nrc
.isConst() ){
1632 getExtTheory()->markReduced( n
);
1633 Trace("strings-extf-debug") << " resolvable by evaluation..." << std::endl
;
1634 std::vector
< Node
> exps
;
1635 // The following optimization gets the "symbolic definition" of
1636 // an extended term. The symbolic definition of a term t is a term
1637 // t' where constants are replaced by their corresponding proxy
1639 // For example, if lsym is a proxy variable for "", then
1640 // str.replace( lsym, lsym, lsym ) is the symbolic definition for
1641 // str.replace( "", "", "" ). It is generally better to use symbolic
1642 // definitions when doing cd-rewriting for the purpose of minimizing
1643 // clauses, e.g. we infer the unit equality:
1644 // str.replace( lsym, lsym, lsym ) == ""
1645 // instead of making this inference multiple times:
1646 // x = "" => str.replace( x, x, x ) == ""
1647 // y = "" => str.replace( y, y, y ) == ""
1648 Trace("strings-extf-debug") << " get symbolic definition..." << std::endl
;
1649 Node nrs
= getSymbolicDefinition( sn
, exps
);
1650 if( !nrs
.isNull() ){
1651 Trace("strings-extf-debug") << " rewrite " << nrs
<< "..." << std::endl
;
1652 Node nrsr
= Rewriter::rewrite(nrs
);
1653 // ensure the symbolic form is not rewritable
1656 // we cannot use the symbolic definition if it rewrites
1657 Trace("strings-extf-debug") << " symbolic definition is trivial..." << std::endl
;
1661 Trace("strings-extf-debug") << " could not infer symbolic definition." << std::endl
;
1664 if( !nrs
.isNull() ){
1665 Trace("strings-extf-debug") << " symbolic def : " << nrs
<< std::endl
;
1666 if( !areEqual( nrs
, nrc
) ){
1667 //infer symbolic unit
1668 if( n
.getType().isBoolean() ){
1669 conc
= nrc
==d_true
? nrs
: nrs
.negate();
1671 conc
= nrs
.eqNode( nrc
);
1673 einfo
.d_exp
.clear();
1676 if( !areEqual( n
, nrc
) ){
1677 if( n
.getType().isBoolean() ){
1678 if( areEqual( n
, nrc
==d_true
? d_false
: d_true
) ){
1679 einfo
.d_exp
.push_back(nrc
== d_true
? n
.negate() : n
);
1682 conc
= nrc
==d_true
? n
: n
.negate();
1685 conc
= n
.eqNode( nrc
);
1689 if( !conc
.isNull() ){
1690 Trace("strings-extf") << " resolve extf : " << sn
<< " -> " << nrc
<< std::endl
;
1692 einfo
.d_exp
, conc
, effort
== 0 ? "EXTF" : "EXTF-N", true);
1694 Trace("strings-extf-debug") << " conflict, return." << std::endl
;
1699 //check if it is already equal, if so, mark as reduced. Otherwise, do nothing.
1700 if( areEqual( n
, nrc
) ){
1701 Trace("strings-extf") << " resolved extf, since satisfied by model: " << n
<< std::endl
;
1702 einfo
.d_model_active
= false;
1708 // if this was a predicate which changed after substitution + rewriting
1709 if (!einfo
.d_const
.isNull() && nrc
.getType().isBoolean() && nrc
!= n
)
1711 bool pol
= einfo
.d_const
== d_true
;
1712 Node nrcAssert
= pol
? nrc
: nrc
.negate();
1713 Node nAssert
= pol
? n
: n
.negate();
1715 einfo
.d_exp
.push_back(nAssert
);
1716 Trace("strings-extf-debug") << " decomposable..." << std::endl
;
1717 Trace("strings-extf") << " resolve extf : " << sn
<< " -> " << nrc
1718 << ", const = " << einfo
.d_const
<< std::endl
;
1719 // We send inferences internal here, which may help show unsat.
1720 // However, we do not make a determination whether n can be marked
1721 // reduced since this argument may be circular: we may infer than n
1722 // can be reduced to something else, but that thing may argue that it
1723 // can be reduced to n, in theory.
1724 sendInternalInference(
1725 einfo
.d_exp
, nrcAssert
, effort
== 0 ? "EXTF_d" : "EXTF_d-N");
1730 to_reduce
= sterms
[i
];
1733 if( !to_reduce
.isNull() ){
1736 Trace("strings-extf") << " cannot rewrite extf : " << to_reduce
<< std::endl
;
1738 checkExtfInference(n
, to_reduce
, einfo
, effort
);
1739 if( Trace
.isOn("strings-extf-list") ){
1740 Trace("strings-extf-list") << " * " << to_reduce
;
1741 if (!einfo
.d_const
.isNull())
1743 Trace("strings-extf-list") << ", const = " << einfo
.d_const
;
1746 Trace("strings-extf-list") << ", from " << n
;
1748 Trace("strings-extf-list") << std::endl
;
1750 if (getExtTheory()->isActive(n
) && einfo
.d_model_active
)
1756 d_has_extf
= has_nreduce
;
1759 void TheoryStrings::checkExtfInference( Node n
, Node nr
, ExtfInfoTmp
& in
, int effort
){
1760 if (in
.d_const
.isNull())
1764 NodeManager
* nm
= NodeManager::currentNM();
1765 Trace("strings-extf-infer") << "checkExtfInference: " << n
<< " : " << nr
1766 << " == " << in
.d_const
<< std::endl
;
1768 // add original to explanation
1769 if (n
.getType().isBoolean())
1771 // if Boolean, it's easy
1772 in
.d_exp
.push_back(in
.d_const
.getConst
<bool>() ? n
: n
.negate());
1776 // otherwise, must explain via base node
1777 Node r
= getRepresentative(n
);
1779 // d_eqc_to_const_exp[r] => d_eqc_to_const_base[r] = in.d_const
1781 // n = d_eqc_to_const_base[r] ^ d_eqc_to_const_exp[r] => n = in.d_const
1782 Assert(d_eqc_to_const_base
.find(r
) != d_eqc_to_const_base
.end());
1783 addToExplanation(n
, d_eqc_to_const_base
[r
], in
.d_exp
);
1784 Assert(d_eqc_to_const_exp
.find(r
) != d_eqc_to_const_exp
.end());
1785 in
.d_exp
.insert(in
.d_exp
.end(),
1786 d_eqc_to_const_exp
[r
].begin(),
1787 d_eqc_to_const_exp
[r
].end());
1790 // d_extf_infer_cache stores whether we have made the inferences associated
1792 // this may need to be generalized if multiple inferences apply
1794 if (nr
.getKind() == STRING_STRCTN
)
1796 Assert(in
.d_const
.isConst());
1797 bool pol
= in
.d_const
.getConst
<bool>();
1798 if ((pol
&& nr
[1].getKind() == STRING_CONCAT
)
1799 || (!pol
&& nr
[0].getKind() == STRING_CONCAT
))
1801 // If str.contains( x, str.++( y1, ..., yn ) ),
1802 // we may infer str.contains( x, y1 ), ..., str.contains( x, yn )
1803 // The following recognizes two situations related to the above reasoning:
1804 // (1) If ~str.contains( x, yi ) holds for some i, we are in conflict,
1805 // (2) If str.contains( x, yj ) already holds for some j, then the term
1806 // str.contains( x, yj ) is irrelevant since it is satisfied by all models
1807 // for str.contains( x, str.++( y1, ..., yn ) ).
1809 // Notice that the dual of the above reasoning also holds, i.e.
1810 // If ~str.contains( str.++( x1, ..., xn ), y ),
1811 // we may infer ~str.contains( x1, y ), ..., ~str.contains( xn, y )
1812 // This is also handled here.
1813 if (d_extf_infer_cache
.find(nr
) == d_extf_infer_cache
.end())
1815 d_extf_infer_cache
.insert(nr
);
1817 int index
= pol
? 1 : 0;
1818 std::vector
<Node
> children
;
1819 children
.push_back(nr
[0]);
1820 children
.push_back(nr
[1]);
1821 for (const Node
& nrc
: nr
[index
])
1823 children
[index
] = nrc
;
1824 Node conc
= nm
->mkNode(STRING_STRCTN
, children
);
1825 conc
= Rewriter::rewrite(pol
? conc
: conc
.negate());
1826 // check if it already (does not) hold
1829 if (areEqual(conc
, d_false
))
1831 // we are in conflict
1832 sendInference(in
.d_exp
, conc
, "CTN_Decompose");
1834 else if (getExtTheory()->hasFunctionKind(conc
.getKind()))
1836 // can mark as reduced, since model for n implies model for conc
1837 getExtTheory()->markReduced(conc
);
1845 if (std::find(d_extf_info_tmp
[nr
[0]].d_ctn
[pol
].begin(),
1846 d_extf_info_tmp
[nr
[0]].d_ctn
[pol
].end(),
1848 == d_extf_info_tmp
[nr
[0]].d_ctn
[pol
].end())
1850 Trace("strings-extf-debug") << " store contains info : " << nr
[0]
1851 << " " << pol
<< " " << nr
[1] << std::endl
;
1852 // Store s (does not) contains t, since nr = (~)contains( s, t ) holds.
1853 d_extf_info_tmp
[nr
[0]].d_ctn
[pol
].push_back(nr
[1]);
1854 d_extf_info_tmp
[nr
[0]].d_ctn_from
[pol
].push_back(n
);
1855 // Do transistive closure on contains, e.g.
1856 // if contains( s, t ) and ~contains( s, r ), then ~contains( t, r ).
1858 // The following infers new (negative) contains based on the above
1859 // reasoning, provided that ~contains( t, r ) does not
1860 // already hold in the current context. We test this by checking that
1861 // contains( t, r ) is not already asserted false in the current
1862 // context. We also handle the case where contains( t, r ) is equivalent
1863 // to t = r, in which case we check that t != r does not already hold
1864 // in the current context.
1866 // Notice that form of the above inference is enough to find
1867 // conflicts purely due to contains predicates. For example, if we
1868 // have only positive occurrences of contains, then no conflicts due to
1869 // contains predicates are possible and this schema does nothing. For
1870 // example, note that contains( s, t ) and contains( t, r ) implies
1871 // contains( s, r ), which we could but choose not to infer. Instead,
1872 // we prefer being lazy: only if ~contains( s, r ) appears later do we
1873 // infer ~contains( t, r ), which suffices to show a conflict.
1875 for (unsigned i
= 0, size
= d_extf_info_tmp
[nr
[0]].d_ctn
[opol
].size();
1879 Node onr
= d_extf_info_tmp
[nr
[0]].d_ctn
[opol
][i
];
1881 nm
->mkNode(STRING_STRCTN
, pol
? nr
[1] : onr
, pol
? onr
: nr
[1]);
1882 conc
= Rewriter::rewrite(conc
);
1883 conc
= conc
.negate();
1884 bool do_infer
= false;
1885 bool pol
= conc
.getKind() != NOT
;
1886 Node lit
= pol
? conc
: conc
[0];
1887 if (lit
.getKind() == EQUAL
)
1889 do_infer
= pol
? !areEqual(lit
[0], lit
[1])
1890 : !areDisequal(lit
[0], lit
[1]);
1894 do_infer
= !areEqual(lit
, pol
? d_true
: d_false
);
1898 std::vector
<Node
> exp_c
;
1899 exp_c
.insert(exp_c
.end(), in
.d_exp
.begin(), in
.d_exp
.end());
1900 Node ofrom
= d_extf_info_tmp
[nr
[0]].d_ctn_from
[opol
][i
];
1901 Assert(d_extf_info_tmp
.find(ofrom
) != d_extf_info_tmp
.end());
1902 exp_c
.insert(exp_c
.end(),
1903 d_extf_info_tmp
[ofrom
].d_exp
.begin(),
1904 d_extf_info_tmp
[ofrom
].d_exp
.end());
1905 sendInference(exp_c
, conc
, "CTN_Trans");
1911 // If we already know that s (does not) contain t, then n is redundant.
1912 // For example, if str.contains( x, y ), str.contains( z, y ), and x=z
1913 // are asserted in the current context, then str.contains( z, y ) is
1914 // satisfied by all models of str.contains( x, y ) ^ x=z and thus can
1916 Trace("strings-extf-debug") << " redundant." << std::endl
;
1917 getExtTheory()->markReduced(n
);
1923 // If it's not a predicate, see if we can solve the equality n = c, where c
1924 // is the constant that extended term n is equal to.
1925 Node inferEq
= nr
.eqNode(in
.d_const
);
1926 Node inferEqr
= Rewriter::rewrite(inferEq
);
1927 Node inferEqrr
= inferEqr
;
1928 if (inferEqr
.getKind() == EQUAL
)
1930 // try to use the extended rewriter for equalities
1931 inferEqrr
= TheoryStringsRewriter::rewriteEqualityExt(inferEqr
);
1933 if (inferEqrr
!= inferEqr
)
1935 inferEqrr
= Rewriter::rewrite(inferEqrr
);
1936 Trace("strings-extf-infer") << "checkExtfInference: " << inferEq
1937 << " ...reduces to " << inferEqrr
<< std::endl
;
1938 sendInternalInference(in
.d_exp
, inferEqrr
, "EXTF_equality_rew");
1942 Node
TheoryStrings::getSymbolicDefinition( Node n
, std::vector
< Node
>& exp
) {
1943 if( n
.getNumChildren()==0 ){
1944 NodeNodeMap::const_iterator it
= d_proxy_var
.find( n
);
1945 if( it
==d_proxy_var
.end() ){
1946 return Node::null();
1948 Node eq
= n
.eqNode( (*it
).second
);
1949 eq
= Rewriter::rewrite( eq
);
1950 if( std::find( exp
.begin(), exp
.end(), eq
)==exp
.end() ){
1951 exp
.push_back( eq
);
1953 return (*it
).second
;
1956 std::vector
< Node
> children
;
1957 if (n
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
1958 children
.push_back( n
.getOperator() );
1960 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1961 if( n
.getKind()==kind::STRING_IN_REGEXP
&& i
==1 ){
1962 children
.push_back( n
[i
] );
1964 Node ns
= getSymbolicDefinition( n
[i
], exp
);
1966 return Node::null();
1968 children
.push_back( ns
);
1972 return NodeManager::currentNM()->mkNode( n
.getKind(), children
);
1976 Node
TheoryStrings::getConstantEqc( Node eqc
) {
1977 std::map
< Node
, Node
>::iterator it
= d_eqc_to_const
.find( eqc
);
1978 if( it
!=d_eqc_to_const
.end() ){
1981 return Node::null();
1985 void TheoryStrings::debugPrintFlatForms( const char * tc
){
1986 for( unsigned k
=0; k
<d_strings_eqc
.size(); k
++ ){
1987 Node eqc
= d_strings_eqc
[k
];
1988 if( d_eqc
[eqc
].size()>1 ){
1989 Trace( tc
) << "EQC [" << eqc
<< "]" << std::endl
;
1991 Trace( tc
) << "eqc [" << eqc
<< "]";
1993 std::map
< Node
, Node
>::iterator itc
= d_eqc_to_const
.find( eqc
);
1994 if( itc
!=d_eqc_to_const
.end() ){
1995 Trace( tc
) << " C: " << itc
->second
;
1996 if( d_eqc
[eqc
].size()>1 ){
1997 Trace( tc
) << std::endl
;
2000 if( d_eqc
[eqc
].size()>1 ){
2001 for( unsigned i
=0; i
<d_eqc
[eqc
].size(); i
++ ){
2002 Node n
= d_eqc
[eqc
][i
];
2004 for( unsigned j
=0; j
<d_flat_form
[n
].size(); j
++ ){
2005 Node fc
= d_flat_form
[n
][j
];
2006 itc
= d_eqc_to_const
.find( fc
);
2008 if( itc
!=d_eqc_to_const
.end() ){
2009 Trace( tc
) << itc
->second
;
2015 Trace( tc
) << ", from " << n
;
2017 Trace( tc
) << std::endl
;
2020 Trace( tc
) << std::endl
;
2023 Trace( tc
) << std::endl
;
2026 void TheoryStrings::debugPrintNormalForms( const char * tc
) {
2029 struct sortConstLength
{
2030 std::map
< Node
, unsigned > d_const_length
;
2031 bool operator() (Node i
, Node j
) {
2032 std::map
< Node
, unsigned >::iterator it_i
= d_const_length
.find( i
);
2033 std::map
< Node
, unsigned >::iterator it_j
= d_const_length
.find( j
);
2034 if( it_i
==d_const_length
.end() ){
2035 if( it_j
==d_const_length
.end() ){
2041 if( it_j
==d_const_length
.end() ){
2044 return it_i
->second
<it_j
->second
;
2050 void TheoryStrings::checkCycles()
2052 // first check for cycles, while building ordering of equivalence classes
2053 d_flat_form
.clear();
2054 d_flat_form_index
.clear();
2056 //rebuild strings eqc based on acyclic ordering
2057 std::vector
< Node
> eqc
;
2058 eqc
.insert( eqc
.end(), d_strings_eqc
.begin(), d_strings_eqc
.end() );
2059 d_strings_eqc
.clear();
2060 if( options::stringBinaryCsp() ){
2061 //sort: process smallest constants first (necessary if doing binary splits)
2062 sortConstLength scl
;
2063 for( unsigned i
=0; i
<eqc
.size(); i
++ ){
2064 std::map
< Node
, Node
>::iterator itc
= d_eqc_to_const
.find( eqc
[i
] );
2065 if( itc
!=d_eqc_to_const
.end() ){
2066 scl
.d_const_length
[eqc
[i
]] = itc
->second
.getConst
<String
>().size();
2069 std::sort( eqc
.begin(), eqc
.end(), scl
);
2071 for( unsigned i
=0; i
<eqc
.size(); i
++ ){
2072 std::vector
< Node
> curr
;
2073 std::vector
< Node
> exp
;
2074 checkCycles( eqc
[i
], curr
, exp
);
2075 if( hasProcessed() ){
2081 void TheoryStrings::checkFlatForms()
2083 // debug print flat forms
2084 if (Trace
.isOn("strings-ff"))
2086 Trace("strings-ff") << "Flat forms : " << std::endl
;
2087 debugPrintFlatForms("strings-ff");
2090 // inferences without recursively expanding flat forms
2092 //(1) approximate equality by containment, infer conflicts
2093 for (const Node
& eqc
: d_strings_eqc
)
2095 Node c
= getConstantEqc(eqc
);
2098 // if equivalence class is constant, all component constants in flat forms
2099 // must be contained in it, in order
2100 std::map
<Node
, std::vector
<Node
> >::iterator it
= d_eqc
.find(eqc
);
2101 if (it
!= d_eqc
.end())
2103 for (const Node
& n
: it
->second
)
2106 if (!TheoryStringsRewriter::canConstantContainList(
2107 c
, d_flat_form
[n
], firstc
, lastc
))
2109 Trace("strings-ff-debug") << "Flat form for " << n
2110 << " cannot be contained in constant "
2112 Trace("strings-ff-debug") << " indices = " << firstc
<< "/"
2113 << lastc
<< std::endl
;
2114 // conflict, explanation is n = base ^ base = c ^ relevant portion
2116 std::vector
<Node
> exp
;
2117 Assert(d_eqc_to_const_base
.find(eqc
) != d_eqc_to_const_base
.end());
2118 addToExplanation(n
, d_eqc_to_const_base
[eqc
], exp
);
2119 Assert(d_eqc_to_const_exp
.find(eqc
) != d_eqc_to_const_exp
.end());
2120 if (!d_eqc_to_const_exp
[eqc
].isNull())
2122 exp
.push_back(d_eqc_to_const_exp
[eqc
]);
2124 for (int e
= firstc
; e
<= lastc
; e
++)
2126 if (d_flat_form
[n
][e
].isConst())
2128 Assert(e
>= 0 && e
< (int)d_flat_form_index
[n
].size());
2129 Assert(d_flat_form_index
[n
][e
] >= 0
2130 && d_flat_form_index
[n
][e
] < (int)n
.getNumChildren());
2132 d_flat_form
[n
][e
], n
[d_flat_form_index
[n
][e
]], exp
);
2135 Node conc
= d_false
;
2136 sendInference(exp
, conc
, "F_NCTN");
2144 //(2) scan lists, unification to infer conflicts and equalities
2145 for (const Node
& eqc
: d_strings_eqc
)
2147 std::map
<Node
, std::vector
<Node
> >::iterator it
= d_eqc
.find(eqc
);
2148 if (it
== d_eqc
.end() || it
->second
.size() <= 1)
2152 // iterate over start index
2153 for (unsigned start
= 0; start
< it
->second
.size() - 1; start
++)
2155 for (unsigned r
= 0; r
< 2; r
++)
2157 bool isRev
= r
== 1;
2158 checkFlatForm(it
->second
, start
, isRev
);
2168 void TheoryStrings::checkFlatForm(std::vector
<Node
>& eqc
,
2173 std::vector
<Node
> inelig
;
2174 for (unsigned i
= 0; i
<= start
; i
++)
2176 inelig
.push_back(eqc
[start
]);
2178 Node a
= eqc
[start
];
2182 std::vector
<Node
> exp
;
2185 unsigned eqc_size
= eqc
.size();
2186 unsigned asize
= d_flat_form
[a
].size();
2189 for (unsigned i
= start
+ 1; i
< eqc_size
; i
++)
2192 if (std::find(inelig
.begin(), inelig
.end(), b
) == inelig
.end())
2194 unsigned bsize
= d_flat_form
[b
].size();
2198 std::vector
<Node
> conc_c
;
2199 for (unsigned j
= count
; j
< bsize
; j
++)
2202 b
[d_flat_form_index
[b
][j
]].eqNode(d_emptyString
));
2204 Assert(!conc_c
.empty());
2205 conc
= mkAnd(conc_c
);
2208 // swap, will enforce is empty past current
2214 inelig
.push_back(eqc
[i
]);
2220 Node curr
= d_flat_form
[a
][count
];
2221 Node curr_c
= getConstantEqc(curr
);
2222 Node ac
= a
[d_flat_form_index
[a
][count
]];
2223 std::vector
<Node
> lexp
;
2224 Node lcurr
= getLength(ac
, lexp
);
2225 for (unsigned i
= 1; i
< eqc_size
; i
++)
2228 if (std::find(inelig
.begin(), inelig
.end(), b
) == inelig
.end())
2230 if (count
== d_flat_form
[b
].size())
2232 inelig
.push_back(b
);
2234 std::vector
<Node
> conc_c
;
2235 for (unsigned j
= count
; j
< asize
; j
++)
2238 a
[d_flat_form_index
[a
][j
]].eqNode(d_emptyString
));
2240 Assert(!conc_c
.empty());
2241 conc
= mkAnd(conc_c
);
2249 Node cc
= d_flat_form
[b
][count
];
2252 Node bc
= b
[d_flat_form_index
[b
][count
]];
2253 inelig
.push_back(b
);
2254 Assert(!areEqual(curr
, cc
));
2255 Node cc_c
= getConstantEqc(cc
);
2256 if (!curr_c
.isNull() && !cc_c
.isNull())
2258 // check for constant conflict
2260 Node s
= TheoryStringsRewriter::splitConstant(
2261 cc_c
, curr_c
, index
, isRev
);
2264 addToExplanation(ac
, d_eqc_to_const_base
[curr
], exp
);
2265 addToExplanation(d_eqc_to_const_exp
[curr
], exp
);
2266 addToExplanation(bc
, d_eqc_to_const_base
[cc
], exp
);
2267 addToExplanation(d_eqc_to_const_exp
[cc
], exp
);
2273 else if ((d_flat_form
[a
].size() - 1) == count
2274 && (d_flat_form
[b
].size() - 1) == count
)
2276 conc
= ac
.eqNode(bc
);
2282 // if lengths are the same, apply LengthEq
2283 std::vector
<Node
> lexp2
;
2284 Node lcc
= getLength(bc
, lexp2
);
2285 if (areEqual(lcurr
, lcc
))
2287 Trace("strings-ff-debug") << "Infer " << ac
<< " == " << bc
2288 << " since " << lcurr
2289 << " == " << lcc
<< std::endl
;
2290 // exp_n.push_back( getLength( curr, true ).eqNode(
2291 // getLength( cc, true ) ) );
2292 Trace("strings-ff-debug") << "Explanation for " << lcurr
2294 for (unsigned j
= 0; j
< lexp
.size(); j
++)
2296 Trace("strings-ff-debug") << lexp
[j
] << std::endl
;
2298 Trace("strings-ff-debug") << "Explanation for " << lcc
2300 for (unsigned j
= 0; j
< lexp2
.size(); j
++)
2302 Trace("strings-ff-debug") << lexp2
[j
] << std::endl
;
2304 exp
.insert(exp
.end(), lexp
.begin(), lexp
.end());
2305 exp
.insert(exp
.end(), lexp2
.begin(), lexp2
.end());
2306 addToExplanation(lcurr
, lcc
, exp
);
2307 conc
= ac
.eqNode(bc
);
2319 Trace("strings-ff-debug")
2320 << "Found inference : " << conc
<< " based on equality " << a
2321 << " == " << b
<< ", " << isRev
<< " " << inf_type
<< std::endl
;
2322 addToExplanation(a
, b
, exp
);
2323 // explain why prefixes up to now were the same
2324 for (unsigned j
= 0; j
< count
; j
++)
2326 Trace("strings-ff-debug") << "Add at " << d_flat_form_index
[a
][j
] << " "
2327 << d_flat_form_index
[b
][j
] << std::endl
;
2329 a
[d_flat_form_index
[a
][j
]], b
[d_flat_form_index
[b
][j
]], exp
);
2331 // explain why other components up to now are empty
2332 for (unsigned t
= 0; t
< 2; t
++)
2334 Node c
= t
== 0 ? a
: b
;
2336 if (inf_type
== 3 || (t
== 1 && inf_type
== 2))
2338 // explain all the empty components for F_EndpointEq, all for
2339 // the short end for F_EndpointEmp
2340 jj
= isRev
? -1 : c
.getNumChildren();
2344 jj
= t
== 0 ? d_flat_form_index
[a
][count
]
2345 : d_flat_form_index
[b
][count
];
2347 int startj
= isRev
? jj
+ 1 : 0;
2348 int endj
= isRev
? c
.getNumChildren() : jj
;
2349 for (int j
= startj
; j
< endj
; j
++)
2351 if (areEqual(c
[j
], d_emptyString
))
2353 addToExplanation(c
[j
], d_emptyString
, exp
);
2357 // notice that F_EndpointEmp is not typically applied, since
2358 // strict prefix equality ( a.b = a ) where a,b non-empty
2359 // is conflicting by arithmetic len(a.b)=len(a)+len(b)!=len(a)
2366 : (inf_type
== 1 ? "F_Unify" : (inf_type
== 2 ? "F_EndpointEmp"
2367 : "F_EndpointEq")));
2375 } while (inelig
.size() < eqc
.size());
2377 for (const Node
& n
: eqc
)
2379 std::reverse(d_flat_form
[n
].begin(), d_flat_form
[n
].end());
2380 std::reverse(d_flat_form_index
[n
].begin(), d_flat_form_index
[n
].end());
2384 Node
TheoryStrings::checkCycles( Node eqc
, std::vector
< Node
>& curr
, std::vector
< Node
>& exp
){
2385 if( std::find( curr
.begin(), curr
.end(), eqc
)!=curr
.end() ){
2388 }else if( std::find( d_strings_eqc
.begin(), d_strings_eqc
.end(), eqc
)==d_strings_eqc
.end() ){
2389 curr
.push_back( eqc
);
2390 //look at all terms in this equivalence class
2391 eq::EqClassIterator eqc_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
2392 while( !eqc_i
.isFinished() ) {
2394 if( d_congruent
.find( n
)==d_congruent
.end() ){
2395 if( n
.getKind() == kind::STRING_CONCAT
){
2396 Trace("strings-cycle") << eqc
<< " check term : " << n
<< " in " << eqc
<< std::endl
;
2397 if( eqc
!=d_emptyString_r
){
2398 d_eqc
[eqc
].push_back( n
);
2400 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
2401 Node nr
= getRepresentative( n
[i
] );
2402 if( eqc
==d_emptyString_r
){
2403 //for empty eqc, ensure all components are empty
2404 if( nr
!=d_emptyString_r
){
2405 std::vector
< Node
> exp
;
2406 exp
.push_back( n
.eqNode( d_emptyString
) );
2407 sendInference( exp
, n
[i
].eqNode( d_emptyString
), "I_CYCLE_E" );
2408 return Node::null();
2411 if( nr
!=d_emptyString_r
){
2412 d_flat_form
[n
].push_back( nr
);
2413 d_flat_form_index
[n
].push_back( i
);
2415 //for non-empty eqc, recurse and see if we find a loop
2416 Node ncy
= checkCycles( nr
, curr
, exp
);
2417 if( !ncy
.isNull() ){
2418 Trace("strings-cycle") << eqc
<< " cycle: " << ncy
<< " at " << n
<< "[" << i
<< "] : " << n
[i
] << std::endl
;
2419 addToExplanation( n
, eqc
, exp
);
2420 addToExplanation( nr
, n
[i
], exp
);
2422 //can infer all other components must be empty
2423 for( unsigned j
=0; j
<n
.getNumChildren(); j
++ ){
2424 //take first non-empty
2425 if( j
!=i
&& !areEqual( n
[j
], d_emptyString
) ){
2426 sendInference( exp
, n
[j
].eqNode( d_emptyString
), "I_CYCLE" );
2427 return Node::null();
2430 Trace("strings-error") << "Looping term should be congruent : " << n
<< " " << eqc
<< " " << ncy
<< std::endl
;
2431 //should find a non-empty component, otherwise would have been singular congruent (I_Norm_S)
2437 if( hasProcessed() ){
2438 return Node::null();
2448 //now we can add it to the list of equivalence classes
2449 d_strings_eqc
.push_back( eqc
);
2453 return Node::null();
2456 void TheoryStrings::checkNormalFormsEq()
2458 if( !options::stringEagerLen() ){
2459 for( unsigned i
=0; i
<d_strings_eqc
.size(); i
++ ) {
2460 Node eqc
= d_strings_eqc
[i
];
2461 eq::EqClassIterator eqc_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
2462 while( !eqc_i
.isFinished() ) {
2464 if( d_congruent
.find( n
)==d_congruent
.end() ){
2465 registerTerm( n
, 2 );
2476 // calculate normal forms for each equivalence class, possibly adding
2478 d_normal_forms
.clear();
2479 d_normal_forms_exp
.clear();
2480 std::map
<Node
, Node
> nf_to_eqc
;
2481 std::map
<Node
, Node
> eqc_to_nf
;
2482 std::map
<Node
, Node
> eqc_to_exp
;
2483 for (const Node
& eqc
: d_strings_eqc
)
2485 Trace("strings-process-debug") << "- Verify normal forms are the same for "
2486 << eqc
<< std::endl
;
2487 normalizeEquivalenceClass(eqc
);
2488 Trace("strings-debug") << "Finished normalizing eqc..." << std::endl
;
2493 Node nf_term
= mkConcat(d_normal_forms
[eqc
]);
2494 std::map
<Node
, Node
>::iterator itn
= nf_to_eqc
.find(nf_term
);
2495 if (itn
!= nf_to_eqc
.end())
2497 // two equivalence classes have same normal form, merge
2498 std::vector
<Node
> nf_exp
;
2499 nf_exp
.push_back(mkAnd(d_normal_forms_exp
[eqc
]));
2500 nf_exp
.push_back(eqc_to_exp
[itn
->second
]);
2502 d_normal_forms_base
[eqc
].eqNode(d_normal_forms_base
[itn
->second
]);
2503 sendInference(nf_exp
, eq
, "Normal_Form");
2504 if( hasProcessed() ){
2510 nf_to_eqc
[nf_term
] = eqc
;
2511 eqc_to_nf
[eqc
] = nf_term
;
2512 eqc_to_exp
[eqc
] = mkAnd(d_normal_forms_exp
[eqc
]);
2514 Trace("strings-process-debug")
2515 << "Done verifying normal forms are the same for " << eqc
<< std::endl
;
2517 if (Trace
.isOn("strings-nf"))
2519 Trace("strings-nf") << "**** Normal forms are : " << std::endl
;
2520 for (std::map
<Node
, Node
>::iterator it
= eqc_to_exp
.begin();
2521 it
!= eqc_to_exp
.end();
2524 Trace("strings-nf") << " N[" << it
->first
<< "] (base "
2525 << d_normal_forms_base
[it
->first
]
2526 << ") = " << eqc_to_nf
[it
->first
] << std::endl
;
2527 Trace("strings-nf") << " exp: " << it
->second
<< std::endl
;
2529 Trace("strings-nf") << std::endl
;
2533 void TheoryStrings::checkCodes()
2535 // ensure that lemmas regarding str.code been added for each constant string
2539 NodeManager
* nm
= NodeManager::currentNM();
2540 // str.code applied to the code term for each equivalence class that has a
2541 // code term but is not a constant
2542 std::vector
<Node
> nconst_codes
;
2543 // str.code applied to the proxy variables for each equivalence classes that
2544 // are constants of size one
2545 std::vector
<Node
> const_codes
;
2546 for (const Node
& eqc
: d_strings_eqc
)
2548 if (d_normal_forms
[eqc
].size() == 1 && d_normal_forms
[eqc
][0].isConst())
2550 Node c
= d_normal_forms
[eqc
][0];
2551 Trace("strings-code-debug") << "Get proxy variable for " << c
2553 Node cc
= nm
->mkNode(kind::STRING_CODE
, c
);
2554 cc
= Rewriter::rewrite(cc
);
2555 Assert(cc
.isConst());
2556 NodeNodeMap::const_iterator it
= d_proxy_var
.find(c
);
2557 AlwaysAssert(it
!= d_proxy_var
.end());
2558 Node vc
= nm
->mkNode(kind::STRING_CODE
, (*it
).second
);
2559 if (!areEqual(cc
, vc
))
2561 sendInference(d_empty_vec
, cc
.eqNode(vc
), "Code_Proxy");
2563 const_codes
.push_back(vc
);
2567 EqcInfo
* ei
= getOrMakeEqcInfo(eqc
, false);
2568 if (ei
&& !ei
->d_code_term
.get().isNull())
2570 Node vc
= nm
->mkNode(kind::STRING_CODE
, ei
->d_code_term
.get());
2571 nconst_codes
.push_back(vc
);
2579 // now, ensure that str.code is injective
2580 std::vector
<Node
> cmps
;
2581 cmps
.insert(cmps
.end(), const_codes
.rbegin(), const_codes
.rend());
2582 cmps
.insert(cmps
.end(), nconst_codes
.rbegin(), nconst_codes
.rend());
2583 for (unsigned i
= 0, num_ncc
= nconst_codes
.size(); i
< num_ncc
; i
++)
2585 Node c1
= nconst_codes
[i
];
2587 for (const Node
& c2
: cmps
)
2589 Trace("strings-code-debug")
2590 << "Compare codes : " << c1
<< " " << c2
<< std::endl
;
2591 if (!areDisequal(c1
, c2
) && !areEqual(c1
, d_neg_one
))
2593 Node eq_no
= c1
.eqNode(d_neg_one
);
2594 Node deq
= c1
.eqNode(c2
).negate();
2595 Node eqn
= c1
[0].eqNode(c2
[0]);
2596 // str.code(x)==-1 V str.code(x)!=str.code(y) V x==y
2597 Node inj_lem
= nm
->mkNode(kind::OR
, eq_no
, deq
, eqn
);
2598 sendInference(d_empty_vec
, inj_lem
, "Code_Inj");
2605 //compute d_normal_forms_(base,exp,exp_depend)[eqc]
2606 void TheoryStrings::normalizeEquivalenceClass( Node eqc
) {
2607 Trace("strings-process-debug") << "Process equivalence class " << eqc
<< std::endl
;
2608 if( areEqual( eqc
, d_emptyString
) ) {
2609 #ifdef CVC4_ASSERTIONS
2610 for( unsigned j
=0; j
<d_eqc
[eqc
].size(); j
++ ){
2611 Node n
= d_eqc
[eqc
][j
];
2612 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
2613 Assert( areEqual( n
[i
], d_emptyString
) );
2618 Trace("strings-process-debug") << "Return process equivalence class " << eqc
<< " : empty." << std::endl
;
2619 d_normal_forms_base
[eqc
] = d_emptyString
;
2620 d_normal_forms
[eqc
].clear();
2621 d_normal_forms_exp
[eqc
].clear();
2623 Assert( d_normal_forms
.find(eqc
)==d_normal_forms
.end() );
2624 //phi => t = s1 * ... * sn
2625 // normal form for each non-variable term in this eqc (s1...sn)
2626 std::vector
< std::vector
< Node
> > normal_forms
;
2627 // explanation for each normal form (phi)
2628 std::vector
< std::vector
< Node
> > normal_forms_exp
;
2629 // dependency information
2630 std::vector
< std::map
< Node
, std::map
< bool, int > > > normal_forms_exp_depend
;
2631 // record terms for each normal form (t)
2632 std::vector
< Node
> normal_form_src
;
2634 getNormalForms(eqc
, normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
);
2635 if( hasProcessed() ){
2638 // process the normal forms
2639 processNEqc( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
);
2640 if( hasProcessed() ){
2643 //debugPrintNormalForms( "strings-solve", eqc, normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend );
2645 //construct the normal form
2646 Assert( !normal_forms
.empty() );
2649 std::vector
< Node
>::iterator itn
= std::find( normal_form_src
.begin(), normal_form_src
.end(), eqc
);
2650 if( itn
!=normal_form_src
.end() ){
2651 nf_index
= itn
- normal_form_src
.begin();
2652 Trace("strings-solve-debug2") << "take normal form " << nf_index
<< std::endl
;
2653 Assert( normal_form_src
[nf_index
]==eqc
);
2655 //just take the first normal form
2656 Trace("strings-solve-debug2") << "take the first normal form" << std::endl
;
2658 d_normal_forms
[eqc
].insert( d_normal_forms
[eqc
].end(), normal_forms
[nf_index
].begin(), normal_forms
[nf_index
].end() );
2659 d_normal_forms_exp
[eqc
].insert( d_normal_forms_exp
[eqc
].end(), normal_forms_exp
[nf_index
].begin(), normal_forms_exp
[nf_index
].end() );
2660 Trace("strings-solve-debug2") << "take normal form ... done" << std::endl
;
2661 d_normal_forms_base
[eqc
] = normal_form_src
[nf_index
];
2662 //track dependencies
2663 for( unsigned i
=0; i
<normal_forms_exp
[nf_index
].size(); i
++ ){
2664 Node exp
= normal_forms_exp
[nf_index
][i
];
2665 for( unsigned r
=0; r
<2; r
++ ){
2666 d_normal_forms_exp_depend
[eqc
][exp
][r
==0] = normal_forms_exp_depend
[nf_index
][exp
][r
==0];
2669 Trace("strings-process-debug") << "Return process equivalence class " << eqc
<< " : returned, size = " << d_normal_forms
[eqc
].size() << std::endl
;
2673 void trackNfExpDependency( std::vector
< Node
>& nf_exp_n
, std::map
< Node
, std::map
< bool, int > >& nf_exp_depend_n
, Node exp
, int new_val
, int new_rev_val
){
2674 if( std::find( nf_exp_n
.begin(), nf_exp_n
.end(), exp
)==nf_exp_n
.end() ){
2675 nf_exp_n
.push_back( exp
);
2677 for( unsigned k
=0; k
<2; k
++ ){
2678 int val
= k
==0 ? new_val
: new_rev_val
;
2679 std::map
< bool, int >::iterator itned
= nf_exp_depend_n
[exp
].find( k
==1 );
2680 if( itned
==nf_exp_depend_n
[exp
].end() ){
2681 Trace("strings-process-debug") << "Deps : set dependency on " << exp
<< " to " << val
<< " isRev=" << (k
==0) << std::endl
;
2682 nf_exp_depend_n
[exp
][k
==1] = val
;
2684 Trace("strings-process-debug") << "Deps : Multiple dependencies on " << exp
<< " : " << itned
->second
<< " " << val
<< " isRev=" << (k
==0) << std::endl
;
2685 //if we already have a dependency (in the case of non-linear string equalities), it is min/max
2686 bool cmp
= val
> itned
->second
;
2688 nf_exp_depend_n
[exp
][k
==1] = val
;
2694 void TheoryStrings::getNormalForms( Node
&eqc
, std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
2695 std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
) {
2696 //constant for equivalence class
2697 Node eqc_non_c
= eqc
;
2698 Trace("strings-process-debug") << "Get normal forms " << eqc
<< std::endl
;
2699 eq::EqClassIterator eqc_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
2700 while( !eqc_i
.isFinished() ){
2702 if( d_congruent
.find( n
)==d_congruent
.end() ){
2703 if( n
.getKind() == kind::CONST_STRING
|| n
.getKind() == kind::STRING_CONCAT
){
2704 Trace("strings-process-debug") << "Get Normal Form : Process term " << n
<< " in eqc " << eqc
<< std::endl
;
2705 std::vector
< Node
> nf_n
;
2706 std::vector
< Node
> nf_exp_n
;
2707 std::map
< Node
, std::map
< bool, int > > nf_exp_depend_n
;
2708 if( n
.getKind()==kind::CONST_STRING
){
2709 if( n
!=d_emptyString
) {
2710 nf_n
.push_back( n
);
2712 }else if( n
.getKind()==kind::STRING_CONCAT
){
2713 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ) {
2714 Node nr
= d_equalityEngine
.getRepresentative( n
[i
] );
2715 Trace("strings-process-debug") << "Normalizing subterm " << n
[i
] << " = " << nr
<< std::endl
;
2716 Assert( d_normal_forms
.find( nr
)!=d_normal_forms
.end() );
2717 unsigned orig_size
= nf_n
.size();
2718 unsigned add_size
= d_normal_forms
[nr
].size();
2719 //if not the empty string, add to current normal form
2720 if( !d_normal_forms
[nr
].empty() ){
2721 for( unsigned r
=0; r
<d_normal_forms
[nr
].size(); r
++ ) {
2722 if( Trace
.isOn("strings-error") ) {
2723 if( d_normal_forms
[nr
][r
].getKind()==kind::STRING_CONCAT
){
2724 Trace("strings-error") << "Strings::Error: From eqc = " << eqc
<< ", " << n
<< " index " << i
<< ", bad normal form : ";
2725 for( unsigned rr
=0; rr
<d_normal_forms
[nr
].size(); rr
++ ) {
2726 Trace("strings-error") << d_normal_forms
[nr
][rr
] << " ";
2728 Trace("strings-error") << std::endl
;
2731 Assert( d_normal_forms
[nr
][r
].getKind()!=kind::STRING_CONCAT
);
2733 nf_n
.insert( nf_n
.end(), d_normal_forms
[nr
].begin(), d_normal_forms
[nr
].end() );
2736 for( unsigned j
=0; j
<d_normal_forms_exp
[nr
].size(); j
++ ){
2737 Node exp
= d_normal_forms_exp
[nr
][j
];
2739 trackNfExpDependency( nf_exp_n
, nf_exp_depend_n
, exp
,
2740 orig_size
+ d_normal_forms_exp_depend
[nr
][exp
][false],
2741 orig_size
+ ( add_size
- d_normal_forms_exp_depend
[nr
][exp
][true] ) );
2743 if( d_normal_forms_base
[nr
]!=n
[i
] ){
2744 Assert( d_normal_forms_base
.find( nr
)!=d_normal_forms_base
.end() );
2745 Node eq
= n
[i
].eqNode( d_normal_forms_base
[nr
] );
2746 //track depends : entire current segment is dependent upon base equality
2747 trackNfExpDependency( nf_exp_n
, nf_exp_depend_n
, eq
, orig_size
, orig_size
+ add_size
);
2750 //convert forward indices to reverse indices
2751 int total_size
= nf_n
.size();
2752 for( std::map
< Node
, std::map
< bool, int > >::iterator it
= nf_exp_depend_n
.begin(); it
!= nf_exp_depend_n
.end(); ++it
){
2753 it
->second
[true] = total_size
- it
->second
[true];
2754 Assert( it
->second
[true]>=0 );
2757 //if not equal to self
2758 if( nf_n
.size()>1 || ( nf_n
.size()==1 && nf_n
[0].getKind()==kind::CONST_STRING
) ){
2759 if( nf_n
.size()>1 ) {
2760 for( unsigned i
=0; i
<nf_n
.size(); i
++ ){
2761 if( Trace
.isOn("strings-error") ){
2762 Trace("strings-error") << "Cycle for normal form ";
2763 printConcat(nf_n
,"strings-error");
2764 Trace("strings-error") << "..." << nf_n
[i
] << std::endl
;
2766 Assert( !areEqual( nf_n
[i
], n
) );
2769 normal_forms
.push_back(nf_n
);
2770 normal_form_src
.push_back(n
);
2771 normal_forms_exp
.push_back(nf_exp_n
);
2772 normal_forms_exp_depend
.push_back(nf_exp_depend_n
);
2774 //this was redundant: combination of self + empty string(s)
2775 Node nn
= nf_n
.size()==0 ? d_emptyString
: nf_n
[0];
2776 Assert( areEqual( nn
, eqc
) );
2785 if( normal_forms
.empty() ) {
2786 Trace("strings-solve-debug2") << "construct the normal form" << std::endl
;
2787 //do not choose a concat here use "eqc_non_c" (in this case they have non-trivial explanation why they normalize to self)
2788 std::vector
< Node
> eqc_non_c_nf
;
2789 getConcatVec( eqc_non_c
, eqc_non_c_nf
);
2790 normal_forms
.push_back( eqc_non_c_nf
);
2791 normal_form_src
.push_back( eqc_non_c
);
2792 normal_forms_exp
.push_back( std::vector
< Node
>() );
2793 normal_forms_exp_depend
.push_back( std::map
< Node
, std::map
< bool, int > >() );
2795 if(Trace
.isOn("strings-solve")) {
2796 Trace("strings-solve") << "--- Normal forms for equivalance class " << eqc
<< " : " << std::endl
;
2797 for( unsigned i
=0; i
<normal_forms
.size(); i
++ ) {
2798 Trace("strings-solve") << "#" << i
<< " (from " << normal_form_src
[i
] << ") : ";
2799 for( unsigned j
=0; j
<normal_forms
[i
].size(); j
++ ) {
2801 Trace("strings-solve") << ", ";
2803 Trace("strings-solve") << normal_forms
[i
][j
];
2805 Trace("strings-solve") << std::endl
;
2806 Trace("strings-solve") << " Explanation is : ";
2807 if(normal_forms_exp
[i
].size() == 0) {
2808 Trace("strings-solve") << "NONE";
2810 for( unsigned j
=0; j
<normal_forms_exp
[i
].size(); j
++ ) {
2812 Trace("strings-solve") << " AND ";
2814 Trace("strings-solve") << normal_forms_exp
[i
][j
];
2816 Trace("strings-solve") << std::endl
;
2817 Trace("strings-solve") << "WITH DEPENDENCIES : " << std::endl
;
2818 for( unsigned j
=0; j
<normal_forms_exp
[i
].size(); j
++ ) {
2819 Trace("strings-solve") << " " << normal_forms_exp
[i
][j
] << " -> ";
2820 Trace("strings-solve") << normal_forms_exp_depend
[i
][normal_forms_exp
[i
][j
]][false] << ",";
2821 Trace("strings-solve") << normal_forms_exp_depend
[i
][normal_forms_exp
[i
][j
]][true] << std::endl
;
2824 Trace("strings-solve") << std::endl
;
2828 Trace("strings-solve") << "--- Single normal form for equivalence class " << eqc
<< std::endl
;
2831 //if equivalence class is constant, approximate as containment, infer conflicts
2832 Node c
= getConstantEqc( eqc
);
2834 Trace("strings-solve") << "Eqc is constant " << c
<< std::endl
;
2835 for( unsigned i
=0; i
<normal_forms
.size(); i
++ ) {
2837 if( !TheoryStringsRewriter::canConstantContainList( c
, normal_forms
[i
], firstc
, lastc
) ){
2838 Node n
= normal_form_src
[i
];
2840 Trace("strings-solve") << "Normal form for " << n
<< " cannot be contained in constant " << c
<< std::endl
;
2841 //conflict, explanation is n = base ^ base = c ^ relevant porition of ( n = N[n] )
2842 std::vector
< Node
> exp
;
2843 Assert( d_eqc_to_const_base
.find( eqc
)!=d_eqc_to_const_base
.end() );
2844 addToExplanation( n
, d_eqc_to_const_base
[eqc
], exp
);
2845 Assert( d_eqc_to_const_exp
.find( eqc
)!=d_eqc_to_const_exp
.end() );
2846 if( !d_eqc_to_const_exp
[eqc
].isNull() ){
2847 exp
.push_back( d_eqc_to_const_exp
[eqc
] );
2849 //TODO: this can be minimized based on firstc/lastc, normal_forms_exp_depend
2850 exp
.insert( exp
.end(), normal_forms_exp
[i
].begin(), normal_forms_exp
[i
].end() );
2851 Node conc
= d_false
;
2852 sendInference( exp
, conc
, "N_NCTN" );
2859 void TheoryStrings::getExplanationVectorForPrefix( std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
,
2860 unsigned i
, int index
, bool isRev
, std::vector
< Node
>& curr_exp
) {
2861 if( index
==-1 || !options::stringMinPrefixExplain() ){
2862 curr_exp
.insert(curr_exp
.end(), normal_forms_exp
[i
].begin(), normal_forms_exp
[i
].end() );
2864 for( unsigned k
=0; k
<normal_forms_exp
[i
].size(); k
++ ){
2865 Node exp
= normal_forms_exp
[i
][k
];
2866 int dep
= normal_forms_exp_depend
[i
][exp
][isRev
];
2868 curr_exp
.push_back( exp
);
2869 Trace("strings-explain-prefix-debug") << " include : " << exp
<< std::endl
;
2871 Trace("strings-explain-prefix-debug") << " exclude : " << exp
<< std::endl
;
2877 void TheoryStrings::getExplanationVectorForPrefixEq( std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
2878 std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
,
2879 unsigned i
, unsigned j
, int index_i
, int index_j
, bool isRev
, std::vector
< Node
>& curr_exp
) {
2880 Trace("strings-explain-prefix") << "Get explanation for prefix " << index_i
<< ", " << index_j
<< " of normal forms " << i
<< " and " << j
<< ", reverse = " << isRev
<< std::endl
;
2881 for( unsigned r
=0; r
<2; r
++ ){
2882 getExplanationVectorForPrefix( normal_forms_exp
, normal_forms_exp_depend
, r
==0 ? i
: j
, r
==0 ? index_i
: index_j
, isRev
, curr_exp
);
2884 Trace("strings-explain-prefix") << "Included " << curr_exp
.size() << " / " << ( normal_forms_exp
[i
].size() + normal_forms_exp
[j
].size() ) << std::endl
;
2885 addToExplanation( normal_form_src
[i
], normal_form_src
[j
], curr_exp
);
2889 void TheoryStrings::processNEqc( std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
2890 std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
){
2891 //the possible inferences
2892 std::vector
< InferInfo
> pinfer
;
2893 // loop over all pairs
2894 for(unsigned i
=0; i
<normal_forms
.size()-1; i
++) {
2895 //unify each normalform[j] with normal_forms[i]
2896 for(unsigned j
=i
+1; j
<normal_forms
.size(); j
++ ) {
2897 //ensure that normal_forms[i] and normal_forms[j] are the same modulo equality, add to pinfer if not
2898 Trace("strings-solve") << "Strings: Process normal form #" << i
<< " against #" << j
<< "..." << std::endl
;
2899 if( isNormalFormPair( normal_form_src
[i
], normal_form_src
[j
] ) ) {
2900 Trace("strings-solve") << "Strings: Already cached." << std::endl
;
2902 //process the reverse direction first (check for easy conflicts and inferences)
2903 unsigned rindex
= 0;
2904 processReverseNEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, rindex
, 0, pinfer
);
2905 if( hasProcessed() ){
2907 }else if( !pinfer
.empty() && pinfer
.back().d_id
==1 ){
2910 //AJR: for less aggressive endpoint inference
2914 processSimpleNEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, index
, false, rindex
, pinfer
);
2915 if( hasProcessed() ){
2917 }else if( !pinfer
.empty() && pinfer
.back().d_id
==1 ){
2927 // now, determine which of the possible inferences we want to add
2928 unsigned use_index
= 0;
2929 bool set_use_index
= false;
2930 Trace("strings-solve") << "Possible inferences (" << pinfer
.size()
2931 << ") : " << std::endl
;
2932 unsigned min_id
= 9;
2933 unsigned max_index
= 0;
2934 for (unsigned i
= 0, size
= pinfer
.size(); i
< size
; i
++)
2936 Trace("strings-solve") << "From " << pinfer
[i
].d_i
<< " / " << pinfer
[i
].d_j
2937 << " (rev=" << pinfer
[i
].d_rev
<< ") : ";
2938 Trace("strings-solve") << pinfer
[i
].d_conc
<< " by " << pinfer
[i
].d_id
2940 if (!set_use_index
|| pinfer
[i
].d_id
< min_id
2941 || (pinfer
[i
].d_id
== min_id
&& pinfer
[i
].d_index
> max_index
))
2943 min_id
= pinfer
[i
].d_id
;
2944 max_index
= pinfer
[i
].d_index
;
2946 set_use_index
= true;
2949 // send the inference
2950 if (!pinfer
[use_index
].d_nf_pair
[0].isNull())
2952 Assert(!pinfer
[use_index
].d_nf_pair
[1].isNull());
2953 addNormalFormPair(pinfer
[use_index
].d_nf_pair
[0],
2954 pinfer
[use_index
].d_nf_pair
[1]);
2956 std::stringstream ssi
;
2957 ssi
<< pinfer
[use_index
].d_id
;
2958 sendInference(pinfer
[use_index
].d_ant
,
2959 pinfer
[use_index
].d_antn
,
2960 pinfer
[use_index
].d_conc
,
2962 pinfer
[use_index
].sendAsLemma());
2963 // Register the new skolems from this inference. We register them here
2964 // (lazily), since the code above has now decided to use the inference
2965 // at use_index that involves them.
2966 for (const std::pair
<const LengthStatus
, std::vector
<Node
> >& sks
:
2967 pinfer
[use_index
].d_new_skolem
)
2969 for (const Node
& n
: sks
.second
)
2971 registerLength(n
, sks
.first
);
2976 bool TheoryStrings::InferInfo::sendAsLemma() {
2980 void TheoryStrings::processReverseNEq( std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
2981 std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
,
2982 unsigned i
, unsigned j
, unsigned& index
, unsigned rproc
, std::vector
< InferInfo
>& pinfer
) {
2983 //reverse normal form of i, j
2984 std::reverse( normal_forms
[i
].begin(), normal_forms
[i
].end() );
2985 std::reverse( normal_forms
[j
].begin(), normal_forms
[j
].end() );
2987 processSimpleNEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, index
, true, rproc
, pinfer
);
2989 //reverse normal form of i, j
2990 std::reverse( normal_forms
[i
].begin(), normal_forms
[i
].end() );
2991 std::reverse( normal_forms
[j
].begin(), normal_forms
[j
].end() );
2994 //rproc is the # is the size of suffix that is identical
2995 void TheoryStrings::processSimpleNEq( std::vector
< std::vector
< Node
> > &normal_forms
, std::vector
< Node
> &normal_form_src
,
2996 std::vector
< std::vector
< Node
> > &normal_forms_exp
, std::vector
< std::map
< Node
, std::map
< bool, int > > >& normal_forms_exp_depend
,
2997 unsigned i
, unsigned j
, unsigned& index
, bool isRev
, unsigned rproc
, std::vector
< InferInfo
>& pinfer
) {
2998 Assert( rproc
<=normal_forms
[i
].size() && rproc
<=normal_forms
[j
].size() );
3002 //if we are at the end
3003 if( index
==(normal_forms
[i
].size()-rproc
) || index
==(normal_forms
[j
].size()-rproc
) ){
3004 if( index
==(normal_forms
[i
].size()-rproc
) && index
==(normal_forms
[j
].size()-rproc
) ){
3007 //the remainder must be empty
3008 unsigned k
= index
==(normal_forms
[i
].size()-rproc
) ? j
: i
;
3009 unsigned index_k
= index
;
3010 //Node eq_exp = mkAnd( curr_exp );
3011 std::vector
< Node
> curr_exp
;
3012 getExplanationVectorForPrefixEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, -1, -1, isRev
, curr_exp
);
3013 while( !d_conflict
&& index_k
<(normal_forms
[k
].size()-rproc
) ){
3014 //can infer that this string must be empty
3015 Node eq
= normal_forms
[k
][index_k
].eqNode( d_emptyString
);
3016 //Trace("strings-lemma") << "Strings: Infer " << eq << " from " << eq_exp << std::endl;
3017 Assert( !areEqual( d_emptyString
, normal_forms
[k
][index_k
] ) );
3018 sendInference( curr_exp
, eq
, "N_EndpointEmp" );
3023 Trace("strings-solve-debug") << "Process " << normal_forms
[i
][index
] << " ... " << normal_forms
[j
][index
] << std::endl
;
3024 if( normal_forms
[i
][index
]==normal_forms
[j
][index
] ){
3025 Trace("strings-solve-debug") << "Simple Case 1 : strings are equal" << std::endl
;
3029 Assert( !areEqual(normal_forms
[i
][index
], normal_forms
[j
][index
]) );
3030 std::vector
< Node
> temp_exp
;
3031 Node length_term_i
= getLength( normal_forms
[i
][index
], temp_exp
);
3032 Node length_term_j
= getLength( normal_forms
[j
][index
], temp_exp
);
3033 //check length(normal_forms[i][index]) == length(normal_forms[j][index])
3034 if( areEqual( length_term_i
, length_term_j
) ){
3035 Trace("strings-solve-debug") << "Simple Case 2 : string lengths are equal" << std::endl
;
3036 Node eq
= normal_forms
[i
][index
].eqNode( normal_forms
[j
][index
] );
3037 //eq = Rewriter::rewrite( eq );
3038 Node length_eq
= length_term_i
.eqNode( length_term_j
);
3039 //temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() );
3040 getExplanationVectorForPrefixEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, index
, index
, isRev
, temp_exp
);
3041 temp_exp
.push_back(length_eq
);
3042 sendInference( temp_exp
, eq
, "N_Unify" );
3044 }else if( ( normal_forms
[i
][index
].getKind()!=kind::CONST_STRING
&& index
==normal_forms
[i
].size()-rproc
-1 ) ||
3045 ( normal_forms
[j
][index
].getKind()!=kind::CONST_STRING
&& index
==normal_forms
[j
].size()-rproc
-1 ) ){
3046 Trace("strings-solve-debug") << "Simple Case 3 : at endpoint" << std::endl
;
3047 std::vector
< Node
> antec
;
3048 //antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
3049 getExplanationVectorForPrefixEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, -1, -1, isRev
, antec
);
3050 std::vector
< Node
> eqn
;
3051 for( unsigned r
=0; r
<2; r
++ ) {
3052 int index_k
= index
;
3053 int k
= r
==0 ? i
: j
;
3054 std::vector
< Node
> eqnc
;
3055 for( unsigned index_l
=index_k
; index_l
<(normal_forms
[k
].size()-rproc
); index_l
++ ) {
3057 eqnc
.insert(eqnc
.begin(), normal_forms
[k
][index_l
] );
3059 eqnc
.push_back( normal_forms
[k
][index_l
] );
3062 eqn
.push_back( mkConcat( eqnc
) );
3064 if( !areEqual( eqn
[0], eqn
[1] ) ){
3065 sendInference( antec
, eqn
[0].eqNode( eqn
[1] ), "N_EndpointEq", true );
3068 Assert( normal_forms
[i
].size()==normal_forms
[j
].size() );
3069 index
= normal_forms
[i
].size()-rproc
;
3071 }else if( normal_forms
[i
][index
].isConst() && normal_forms
[j
][index
].isConst() ){
3072 Node const_str
= normal_forms
[i
][index
];
3073 Node other_str
= normal_forms
[j
][index
];
3074 Trace("strings-solve-debug") << "Simple Case 3 : Const Split : " << const_str
<< " vs " << other_str
<< " at index " << index
<< ", isRev = " << isRev
<< std::endl
;
3075 unsigned len_short
= const_str
.getConst
<String
>().size() <= other_str
.getConst
<String
>().size() ? const_str
.getConst
<String
>().size() : other_str
.getConst
<String
>().size();
3076 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
);
3078 //same prefix/suffix
3079 //k is the index of the string that is shorter
3080 int k
= const_str
.getConst
<String
>().size()<other_str
.getConst
<String
>().size() ? i
: j
;
3081 int l
= const_str
.getConst
<String
>().size()<other_str
.getConst
<String
>().size() ? j
: i
;
3082 //update the nf exp dependencies
3083 //notice this is not critical for soundness: not doing the below incrementing will only lead to overapproximating when antecedants are required in explanations
3084 for( std::map
< Node
, std::map
< bool, int > >::iterator itnd
= normal_forms_exp_depend
[l
].begin(); itnd
!= normal_forms_exp_depend
[l
].end(); ++itnd
){
3085 for( std::map
< bool, int >::iterator itnd2
= itnd
->second
.begin(); itnd2
!= itnd
->second
.end(); ++itnd2
){
3086 //see if this can be incremented: it can if it is not relevant to the current index
3087 Assert( itnd2
->second
>=0 && itnd2
->second
<=(int)normal_forms
[l
].size() );
3088 bool increment
= (itnd2
->first
==isRev
) ? itnd2
->second
>(int)index
: ( (int)normal_forms
[l
].size()-1-itnd2
->second
)<(int)index
;
3090 normal_forms_exp_depend
[l
][itnd
->first
][itnd2
->first
] = itnd2
->second
+ 1;
3095 int new_len
= normal_forms
[l
][index
].getConst
<String
>().size() - len_short
;
3096 Node remainderStr
= NodeManager::currentNM()->mkConst( normal_forms
[l
][index
].getConst
<String
>().substr(0, new_len
) );
3097 Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms
[l
][index
] << " into " << normal_forms
[k
][index
] << ", " << remainderStr
<< std::endl
;
3098 normal_forms
[l
].insert( normal_forms
[l
].begin()+index
+ 1, remainderStr
);
3100 Node remainderStr
= NodeManager::currentNM()->mkConst(normal_forms
[l
][index
].getConst
<String
>().substr(len_short
));
3101 Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms
[l
][index
] << " into " << normal_forms
[k
][index
] << ", " << remainderStr
<< std::endl
;
3102 normal_forms
[l
].insert( normal_forms
[l
].begin()+index
+ 1, remainderStr
);
3104 normal_forms
[l
][index
] = normal_forms
[k
][index
];
3109 std::vector
< Node
> antec
;
3110 getExplanationVectorForPrefixEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, index
, index
, isRev
, antec
);
3111 sendInference( antec
, d_false
, "N_Const", true );
3115 //construct the candidate inference "info"
3117 info
.d_index
= index
;
3122 bool info_valid
= false;
3123 Assert( index
<normal_forms
[i
].size()-rproc
&& index
<normal_forms
[j
].size()-rproc
);
3124 std::vector
< Node
> lexp
;
3125 Node length_term_i
= getLength( normal_forms
[i
][index
], lexp
);
3126 Node length_term_j
= getLength( normal_forms
[j
][index
], lexp
);
3127 //split on equality between string lengths (note that splitting on equality between strings is worse since it is harder to process)
3128 if( !areDisequal( length_term_i
, length_term_j
) && !areEqual( length_term_i
, length_term_j
) &&
3129 normal_forms
[i
][index
].getKind()!=kind::CONST_STRING
&& normal_forms
[j
][index
].getKind()!=kind::CONST_STRING
){ //AJR: remove the latter 2 conditions?
3130 Trace("strings-solve-debug") << "Non-simple Case 1 : string lengths neither equal nor disequal" << std::endl
;
3131 //try to make the lengths equal via splitting on demand
3132 Node length_eq
= NodeManager::currentNM()->mkNode( kind::EQUAL
, length_term_i
, length_term_j
);
3133 length_eq
= Rewriter::rewrite( length_eq
);
3135 info
.d_conc
= NodeManager::currentNM()->mkNode( kind::OR
, length_eq
, length_eq
.negate() );
3136 info
.d_pending_phase
[ length_eq
] = true;
3137 info
.d_id
= INFER_LEN_SPLIT
;
3140 Trace("strings-solve-debug") << "Non-simple Case 2 : must compare strings" << std::endl
;
3143 ProcessLoopResult plr
= ProcessLoopResult::SKIPPED
;
3144 if( detectLoop( normal_forms
, i
, j
, index
, loop_in_i
, loop_in_j
, rproc
) ){
3145 if( !isRev
){ //FIXME
3146 getExplanationVectorForPrefixEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, -1, -1, isRev
, info
.d_ant
);
3148 plr
= processLoop(normal_forms
,
3152 loop_in_i
!= -1 ? i
: j
,
3153 loop_in_i
!= -1 ? j
: i
,
3154 loop_in_i
!= -1 ? loop_in_i
: loop_in_j
,
3157 if (plr
== ProcessLoopResult::INFERENCE
)
3164 if (plr
== ProcessLoopResult::SKIPPED
)
3166 //AJR: length entailment here?
3167 if( normal_forms
[i
][index
].getKind() == kind::CONST_STRING
|| normal_forms
[j
][index
].getKind() == kind::CONST_STRING
){
3168 unsigned const_k
= normal_forms
[i
][index
].getKind() == kind::CONST_STRING
? i
: j
;
3169 unsigned nconst_k
= normal_forms
[i
][index
].getKind() == kind::CONST_STRING
? j
: i
;
3170 Node other_str
= normal_forms
[nconst_k
][index
];
3171 Assert( other_str
.getKind()!=kind::CONST_STRING
, "Other string is not constant." );
3172 Assert( other_str
.getKind()!=kind::STRING_CONCAT
, "Other string is not CONCAT." );
3173 if( !d_equalityEngine
.areDisequal( other_str
, d_emptyString
, true ) ){
3174 Node eq
= other_str
.eqNode( d_emptyString
);
3176 info
.d_conc
= NodeManager::currentNM()->mkNode( kind::OR
, eq
, eq
.negate() );
3177 info
.d_id
= INFER_LEN_SPLIT_EMP
;
3180 if( !isRev
){ //FIXME
3181 Node xnz
= other_str
.eqNode( d_emptyString
).negate();
3182 unsigned index_nc_k
= index
+1;
3183 //Node next_const_str = TheoryStringsRewriter::collectConstantStringAt( normal_forms[nconst_k], index_nc_k, false );
3184 unsigned start_index_nc_k
= index
+1;
3185 Node next_const_str
= TheoryStringsRewriter::getNextConstantAt( normal_forms
[nconst_k
], start_index_nc_k
, index_nc_k
, false );
3186 if( !next_const_str
.isNull() ) {
3187 unsigned index_c_k
= index
;
3188 Node const_str
= TheoryStringsRewriter::collectConstantStringAt( normal_forms
[const_k
], index_c_k
, false );
3189 Assert( !const_str
.isNull() );
3190 CVC4::String stra
= const_str
.getConst
<String
>();
3191 CVC4::String strb
= next_const_str
.getConst
<String
>();
3192 //since non-empty, we start with charecter #1
3195 CVC4::String stra1
= stra
.prefix( stra
.size()-1 );
3196 p
= stra
.size() - stra1
.roverlap(strb
);
3197 Trace("strings-csp-debug") << "Compute roverlap : " << const_str
<< " " << next_const_str
<< std::endl
;
3198 size_t p2
= stra1
.rfind(strb
);
3199 p
= p2
==std::string::npos
? p
: ( p
>p2
+1? p2
+1 : p
);
3200 Trace("strings-csp-debug") << "overlap : " << stra1
<< " " << strb
<< " returned " << p
<< " " << p2
<< " " << (p2
==std::string::npos
) << std::endl
;
3202 CVC4::String stra1
= stra
.substr( 1 );
3203 p
= stra
.size() - stra1
.overlap(strb
);
3204 Trace("strings-csp-debug") << "Compute overlap : " << const_str
<< " " << next_const_str
<< std::endl
;
3205 size_t p2
= stra1
.find(strb
);
3206 p
= p2
==std::string::npos
? p
: ( p
>p2
+1? p2
+1 : p
);
3207 Trace("strings-csp-debug") << "overlap : " << stra1
<< " " << strb
<< " returned " << p
<< " " << p2
<< " " << (p2
==std::string::npos
) << std::endl
;
3210 if( start_index_nc_k
==index
+1 ){
3211 info
.d_ant
.push_back( xnz
);
3212 getExplanationVectorForPrefixEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
,
3213 const_k
, nconst_k
, index_c_k
, index_nc_k
, isRev
, info
.d_ant
);
3214 Node prea
= p
==stra
.size() ? const_str
: NodeManager::currentNM()->mkConst( isRev
? stra
.suffix( p
) : stra
.prefix( p
) );
3215 Node sk
= d_sk_cache
.mkSkolemCached(
3218 isRev
? SkolemCache::SK_ID_C_SPT_REV
3219 : SkolemCache::SK_ID_C_SPT
,
3221 Trace("strings-csp") << "Const Split: " << prea
<< " is removed from " << stra
<< " due to " << strb
<< ", p=" << p
<< std::endl
;
3223 info
.d_conc
= other_str
.eqNode( isRev
? mkConcat( sk
, prea
) : mkConcat(prea
, sk
) );
3224 info
.d_new_skolem
[LENGTH_SPLIT
].push_back(sk
);
3225 info
.d_id
= INFER_SSPLIT_CST_PROP
;
3228 /* FIXME for isRev, speculative
3229 else if( options::stringLenPropCsp() ){
3230 //propagate length constraint
3231 std::vector< Node > cc;
3232 for( unsigned i=index; i<start_index_nc_k; i++ ){
3233 cc.push_back( normal_forms[nconst_k][i] );
3235 Node lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, mkConcat( cc ) );
3236 conc = NodeManager::currentNM()->mkNode( kind::GEQ, lt, NodeManager::currentNM()->mkConst( Rational(p) ) );
3237 sendInference( ant, conc, "S-Split(CSP-P)-lprop", true );
3243 info
.d_ant
.push_back( xnz
);
3244 Node const_str
= normal_forms
[const_k
][index
];
3245 getExplanationVectorForPrefixEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, index
, index
, isRev
, info
.d_ant
);
3246 CVC4::String stra
= const_str
.getConst
<String
>();
3247 if( options::stringBinaryCsp() && stra
.size()>3 ){
3248 //split string in half
3249 Node c_firstHalf
= NodeManager::currentNM()->mkConst( isRev
? stra
.substr( stra
.size()/2 ) : stra
.substr(0, stra
.size()/2 ) );
3250 Node sk
= d_sk_cache
.mkSkolemCached(
3253 isRev
? SkolemCache::SK_ID_VC_BIN_SPT_REV
3254 : SkolemCache::SK_ID_VC_BIN_SPT
,
3256 Trace("strings-csp") << "Const Split: " << c_firstHalf
<< " is removed from " << const_str
<< " (binary) " << std::endl
;
3257 info
.d_conc
= NodeManager::currentNM()->mkNode( kind::OR
, other_str
.eqNode( isRev
? mkConcat( sk
, c_firstHalf
) : mkConcat( c_firstHalf
, sk
) ),
3258 NodeManager::currentNM()->mkNode( kind::AND
,
3259 sk
.eqNode( d_emptyString
).negate(),
3260 c_firstHalf
.eqNode( isRev
? mkConcat( sk
, other_str
) : mkConcat( other_str
, sk
) ) ) );
3261 info
.d_new_skolem
[LENGTH_SPLIT
].push_back(sk
);
3262 info
.d_id
= INFER_SSPLIT_CST_BINARY
;
3266 Node firstChar
= stra
.size() == 1 ? const_str
: NodeManager::currentNM()->mkConst( isRev
? stra
.suffix( 1 ) : stra
.prefix( 1 ) );
3267 Node sk
= d_sk_cache
.mkSkolemCached(
3270 isRev
? SkolemCache::SK_ID_VC_SPT_REV
3271 : SkolemCache::SK_ID_VC_SPT
,
3273 Trace("strings-csp") << "Const Split: " << firstChar
<< " is removed from " << const_str
<< " (serial) " << std::endl
;
3274 info
.d_conc
= other_str
.eqNode( isRev
? mkConcat( sk
, firstChar
) : mkConcat(firstChar
, sk
) );
3275 info
.d_new_skolem
[LENGTH_SPLIT
].push_back(sk
);
3276 info
.d_id
= INFER_SSPLIT_CST
;
3283 int lentTestSuccess
= -1;
3285 if( options::stringCheckEntailLen() ){
3287 for( unsigned e
=0; e
<2; e
++ ){
3288 Node t
= e
==0 ? normal_forms
[i
][index
] : normal_forms
[j
][index
];
3289 //do not infer constants are larger than variables
3290 if( t
.getKind()!=kind::CONST_STRING
){
3291 Node lt1
= e
==0 ? length_term_i
: length_term_j
;
3292 Node lt2
= e
==0 ? length_term_j
: length_term_i
;
3293 Node ent_lit
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT
, lt1
, lt2
) );
3294 std::pair
<bool, Node
> et
= d_valuation
.entailmentCheck( THEORY_OF_TYPE_BASED
, ent_lit
);
3296 Trace("strings-entail") << "Strings entailment : " << ent_lit
<< " is entailed in the current context." << std::endl
;
3297 Trace("strings-entail") << " explanation was : " << et
.second
<< std::endl
;
3298 lentTestSuccess
= e
;
3299 lentTestExp
= et
.second
;
3306 getExplanationVectorForPrefixEq( normal_forms
, normal_form_src
, normal_forms_exp
, normal_forms_exp_depend
, i
, j
, index
, index
, isRev
, info
.d_ant
);
3308 for(unsigned xory
=0; xory
<2; xory
++) {
3309 Node x
= xory
==0 ? normal_forms
[i
][index
] : normal_forms
[j
][index
];
3310 Node xgtz
= x
.eqNode( d_emptyString
).negate();
3311 if( d_equalityEngine
.areDisequal( x
, d_emptyString
, true ) ) {
3312 info
.d_ant
.push_back( xgtz
);
3314 info
.d_antn
.push_back( xgtz
);
3317 Node sk
= d_sk_cache
.mkSkolemCached(
3318 normal_forms
[i
][index
],
3319 normal_forms
[j
][index
],
3320 isRev
? SkolemCache::SK_ID_V_SPT_REV
3321 : SkolemCache::SK_ID_V_SPT
,
3323 // must add length requirement
3324 info
.d_new_skolem
[LENGTH_GEQ_ONE
].push_back(sk
);
3325 Node eq1
= normal_forms
[i
][index
].eqNode( isRev
? mkConcat(sk
, normal_forms
[j
][index
]) : mkConcat(normal_forms
[j
][index
], sk
) );
3326 Node eq2
= normal_forms
[j
][index
].eqNode( isRev
? mkConcat(sk
, normal_forms
[i
][index
]) : mkConcat(normal_forms
[i
][index
], sk
) );
3328 if( lentTestSuccess
!=-1 ){
3329 info
.d_antn
.push_back( lentTestExp
);
3330 info
.d_conc
= lentTestSuccess
==0 ? eq1
: eq2
;
3331 info
.d_id
= INFER_SSPLIT_VAR_PROP
;
3334 Node ldeq
= NodeManager::currentNM()->mkNode( kind::EQUAL
, length_term_i
, length_term_j
).negate();
3335 if( d_equalityEngine
.areDisequal( length_term_i
, length_term_j
, true ) ){
3336 info
.d_ant
.push_back( ldeq
);
3338 info
.d_antn
.push_back(ldeq
);
3341 info
.d_conc
= NodeManager::currentNM()->mkNode( kind::OR
, eq1
, eq2
);
3342 info
.d_id
= INFER_SSPLIT_VAR
;
3349 pinfer
.push_back( info
);
3358 bool TheoryStrings::detectLoop( std::vector
< std::vector
< Node
> > &normal_forms
, int i
, int j
, int index
, int &loop_in_i
, int &loop_in_j
, unsigned rproc
){
3359 int has_loop
[2] = { -1, -1 };
3360 if( options::stringLB() != 2 ) {
3361 for( unsigned r
=0; r
<2; r
++ ) {
3362 int n_index
= (r
==0 ? i
: j
);
3363 int other_n_index
= (r
==0 ? j
: i
);
3364 if( normal_forms
[other_n_index
][index
].getKind() != kind::CONST_STRING
) {
3365 for( unsigned lp
= index
+1; lp
<normal_forms
[n_index
].size()-rproc
; lp
++ ){
3366 if( normal_forms
[n_index
][lp
]==normal_forms
[other_n_index
][index
] ){
3374 if( has_loop
[0]!=-1 || has_loop
[1]!=-1 ) {
3375 loop_in_i
= has_loop
[0];
3376 loop_in_j
= has_loop
[1];
3379 Trace("strings-solve-debug") << "No loops detected." << std::endl
;
3385 TheoryStrings::ProcessLoopResult
TheoryStrings::processLoop(
3386 const std::vector
<std::vector
<Node
> >& normal_forms
,
3387 const std::vector
<Node
>& normal_form_src
,
3396 if (options::stringProcessLoopMode() == ProcessLoopMode::ABORT
)
3398 throw LogicException("Looping word equation encountered.");
3400 else if (options::stringProcessLoopMode() == ProcessLoopMode::NONE
)
3402 d_out
->setIncomplete();
3403 return ProcessLoopResult::SKIPPED
;
3406 NodeManager
* nm
= NodeManager::currentNM();
3408 Trace("strings-loop") << "Detected possible loop for "
3409 << normal_forms
[loop_n_index
][loop_index
] << std::endl
;
3410 Trace("strings-loop") << " ... (X)= " << normal_forms
[other_n_index
][index
]
3413 Trace("strings-loop") << " ... T(Y.Z)= ";
3414 const std::vector
<Node
>& veci
= normal_forms
[loop_n_index
];
3415 std::vector
<Node
> vec_t(veci
.begin() + index
, veci
.begin() + loop_index
);
3416 Node t_yz
= mkConcat(vec_t
);
3417 Trace("strings-loop") << " (" << t_yz
<< ")" << std::endl
;
3418 Trace("strings-loop") << " ... S(Z.Y)= ";
3419 const std::vector
<Node
>& vecoi
= normal_forms
[other_n_index
];
3420 std::vector
<Node
> vec_s(vecoi
.begin() + index
+ 1, vecoi
.end());
3421 Node s_zy
= mkConcat(vec_s
);
3422 Trace("strings-loop") << s_zy
<< std::endl
;
3423 Trace("strings-loop") << " ... R= ";
3424 std::vector
<Node
> vec_r(veci
.begin() + loop_index
+ 1, veci
.end());
3425 Node r
= mkConcat(vec_r
);
3426 Trace("strings-loop") << r
<< std::endl
;
3428 if (s_zy
.isConst() && r
.isConst() && r
!= d_emptyString
)
3432 if (s_zy
.getConst
<String
>().tailcmp(r
.getConst
<String
>(), c
))
3436 s_zy
= nm
->mkConst(s_zy
.getConst
<String
>().substr(0, c
));
3439 Trace("strings-loop") << "Strings::Loop: Refactor S(Z.Y)= " << s_zy
3440 << ", c=" << c
<< std::endl
;
3446 Trace("strings-loop") << "Strings::Loop: tails are different."
3448 sendInference(info
.d_ant
, conc
, "Loop Conflict", true);
3449 return ProcessLoopResult::CONFLICT
;
3454 for (unsigned r
= 0; r
< 2; r
++)
3456 Node t
= r
== 0 ? normal_forms
[loop_n_index
][loop_index
] : t_yz
;
3457 split_eq
= t
.eqNode(d_emptyString
);
3458 Node split_eqr
= Rewriter::rewrite(split_eq
);
3459 // the equality could rewrite to false
3460 if (!split_eqr
.isConst())
3462 if (!areDisequal(t
, d_emptyString
))
3464 // try to make t equal to empty to avoid loop
3465 info
.d_conc
= nm
->mkNode(kind::OR
, split_eq
, split_eq
.negate());
3466 info
.d_id
= INFER_LEN_SPLIT_EMP
;
3467 return ProcessLoopResult::INFERENCE
;
3471 info
.d_ant
.push_back(split_eq
.negate());
3476 Assert(!split_eqr
.getConst
<bool>());
3480 Node ant
= mkExplain(info
.d_ant
);
3482 info
.d_antn
.push_back(ant
);
3485 if (s_zy
== t_yz
&& r
== d_emptyString
&& s_zy
.isConst()
3486 && s_zy
.getConst
<String
>().isRepeated())
3488 Node rep_c
= nm
->mkConst(s_zy
.getConst
<String
>().substr(0, 1));
3489 Trace("strings-loop") << "Special case (X)="
3490 << normal_forms
[other_n_index
][index
] << " "
3492 Trace("strings-loop") << "... (C)=" << rep_c
<< " " << std::endl
;
3495 nm
->mkNode(kind::STRING_IN_REGEXP
,
3496 normal_forms
[other_n_index
][index
],
3497 nm
->mkNode(kind::REGEXP_STAR
,
3498 nm
->mkNode(kind::STRING_TO_REGEXP
, rep_c
)));
3501 else if (t_yz
.isConst())
3503 Trace("strings-loop") << "Strings::Loop: Const Normal Breaking."
3505 CVC4::String s
= t_yz
.getConst
<CVC4::String
>();
3506 unsigned size
= s
.size();
3507 std::vector
<Node
> vconc
;
3508 for (unsigned len
= 1; len
<= size
; len
++)
3510 Node y
= nm
->mkConst(s
.substr(0, len
));
3511 Node z
= nm
->mkConst(s
.substr(len
, size
- len
));
3514 if (r
!= d_emptyString
)
3516 std::vector
<Node
> v2(vec_r
);
3517 v2
.insert(v2
.begin(), y
);
3518 v2
.insert(v2
.begin(), z
);
3519 restr
= mkConcat(z
, y
);
3520 cc
= Rewriter::rewrite(s_zy
.eqNode(mkConcat(v2
)));
3524 cc
= Rewriter::rewrite(s_zy
.eqNode(mkConcat(z
, y
)));
3530 Node conc2
= nm
->mkNode(
3531 kind::STRING_IN_REGEXP
,
3532 normal_forms
[other_n_index
][index
],
3533 nm
->mkNode(kind::REGEXP_CONCAT
,
3534 nm
->mkNode(kind::STRING_TO_REGEXP
, y
),
3535 nm
->mkNode(kind::REGEXP_STAR
,
3536 nm
->mkNode(kind::STRING_TO_REGEXP
, restr
))));
3537 cc
= cc
== d_true
? conc2
: nm
->mkNode(kind::AND
, cc
, conc2
);
3538 vconc
.push_back(cc
);
3540 conc
= vconc
.size() == 0 ? Node::null() : vconc
.size() == 1
3542 : nm
->mkNode(kind::OR
, vconc
);
3546 if (options::stringProcessLoopMode() == ProcessLoopMode::SIMPLE_ABORT
)
3548 throw LogicException("Normal looping word equation encountered.");
3550 else if (options::stringProcessLoopMode() == ProcessLoopMode::SIMPLE
)
3552 d_out
->setIncomplete();
3553 return ProcessLoopResult::SKIPPED
;
3556 Trace("strings-loop") << "Strings::Loop: Normal Loop Breaking."
3559 Node sk_w
= d_sk_cache
.mkSkolem("w_loop");
3560 Node sk_y
= d_sk_cache
.mkSkolem("y_loop");
3561 registerLength(sk_y
, LENGTH_GEQ_ONE
);
3562 Node sk_z
= d_sk_cache
.mkSkolem("z_loop");
3563 // t1 * ... * tn = y * z
3564 Node conc1
= t_yz
.eqNode(mkConcat(sk_y
, sk_z
));
3565 // s1 * ... * sk = z * y * r
3566 vec_r
.insert(vec_r
.begin(), sk_y
);
3567 vec_r
.insert(vec_r
.begin(), sk_z
);
3568 Node conc2
= s_zy
.eqNode(mkConcat(vec_r
));
3570 normal_forms
[other_n_index
][index
].eqNode(mkConcat(sk_y
, sk_w
));
3571 Node restr
= r
== d_emptyString
? s_zy
: mkConcat(sk_z
, sk_y
);
3573 nm
->mkNode(kind::STRING_IN_REGEXP
,
3575 nm
->mkNode(kind::REGEXP_STAR
,
3576 nm
->mkNode(kind::STRING_TO_REGEXP
, restr
)));
3578 std::vector
<Node
> vec_conc
;
3579 vec_conc
.push_back(conc1
);
3580 vec_conc
.push_back(conc2
);
3581 vec_conc
.push_back(conc3
);
3582 vec_conc
.push_back(str_in_re
);
3583 // vec_conc.push_back(sk_y.eqNode(d_emptyString).negate());//by mkskolems
3584 conc
= nm
->mkNode(kind::AND
, vec_conc
);
3589 info
.d_id
= INFER_FLOOP
;
3590 info
.d_nf_pair
[0] = normal_form_src
[i
];
3591 info
.d_nf_pair
[1] = normal_form_src
[j
];
3592 return ProcessLoopResult::INFERENCE
;
3595 //return true for lemma, false if we succeed
3596 void TheoryStrings::processDeq( Node ni
, Node nj
) {
3597 //Assert( areDisequal( ni, nj ) );
3598 if( d_normal_forms
[ni
].size()>1 || d_normal_forms
[nj
].size()>1 ){
3599 std::vector
< Node
> nfi
;
3600 nfi
.insert( nfi
.end(), d_normal_forms
[ni
].begin(), d_normal_forms
[ni
].end() );
3601 std::vector
< Node
> nfj
;
3602 nfj
.insert( nfj
.end(), d_normal_forms
[nj
].begin(), d_normal_forms
[nj
].end() );
3604 int revRet
= processReverseDeq( nfi
, nfj
, ni
, nj
);
3610 nfi
.insert( nfi
.end(), d_normal_forms
[ni
].begin(), d_normal_forms
[ni
].end() );
3612 nfj
.insert( nfj
.end(), d_normal_forms
[nj
].begin(), d_normal_forms
[nj
].end() );
3615 while( index
<nfi
.size() || index
<nfj
.size() ){
3616 int ret
= processSimpleDeq( nfi
, nfj
, ni
, nj
, index
, false );
3620 Assert( index
<nfi
.size() && index
<nfj
.size() );
3621 Node i
= nfi
[index
];
3622 Node j
= nfj
[index
];
3623 Trace("strings-solve-debug") << "...Processing(DEQ) " << i
<< " " << j
<< std::endl
;
3624 if( !areEqual( i
, j
) ){
3625 Assert( i
.getKind()!=kind::CONST_STRING
|| j
.getKind()!=kind::CONST_STRING
);
3626 std::vector
< Node
> lexp
;
3627 Node li
= getLength( i
, lexp
);
3628 Node lj
= getLength( j
, lexp
);
3629 if( areDisequal( li
, lj
) ){
3630 if( i
.getKind()==kind::CONST_STRING
|| j
.getKind()==kind::CONST_STRING
){
3632 Node const_k
= i
.getKind() == kind::CONST_STRING
? i
: j
;
3633 Node nconst_k
= i
.getKind() == kind::CONST_STRING
? j
: i
;
3634 Node lnck
= i
.getKind() == kind::CONST_STRING
? lj
: li
;
3635 if( !d_equalityEngine
.areDisequal( nconst_k
, d_emptyString
, true ) ){
3636 Node eq
= nconst_k
.eqNode( d_emptyString
);
3637 Node conc
= NodeManager::currentNM()->mkNode( kind::OR
, eq
, eq
.negate() );
3638 sendInference( d_empty_vec
, conc
, "D-DISL-Emp-Split" );
3641 //split on first character
3642 CVC4::String str
= const_k
.getConst
<String
>();
3643 Node firstChar
= str
.size() == 1 ? const_k
: NodeManager::currentNM()->mkConst( str
.prefix( 1 ) );
3644 if( areEqual( lnck
, d_one
) ){
3645 if( areDisequal( firstChar
, nconst_k
) ){
3647 }else if( !areEqual( firstChar
, nconst_k
) ){
3648 //splitting on demand : try to make them disequal
3650 firstChar
, nconst_k
, "S-Split(DEQL-Const)", false))
3656 Node sk
= d_sk_cache
.mkSkolemCached(
3657 nconst_k
, firstChar
, SkolemCache::SK_ID_DC_SPT
, "dc_spt");
3658 registerLength(sk
, LENGTH_ONE
);
3660 d_sk_cache
.mkSkolemCached(nconst_k
,
3662 SkolemCache::SK_ID_DC_SPT_REM
,
3664 Node eq1
= nconst_k
.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, sk
, skr
) );
3665 eq1
= Rewriter::rewrite( eq1
);
3666 Node eq2
= nconst_k
.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, firstChar
, skr
) );
3667 std::vector
< Node
> antec
;
3668 antec
.insert( antec
.end(), d_normal_forms_exp
[ni
].begin(), d_normal_forms_exp
[ni
].end() );
3669 antec
.insert( antec
.end(), d_normal_forms_exp
[nj
].begin(), d_normal_forms_exp
[nj
].end() );
3670 antec
.push_back( nconst_k
.eqNode( d_emptyString
).negate() );
3671 sendInference( antec
, NodeManager::currentNM()->mkNode( kind::OR
,
3672 NodeManager::currentNM()->mkNode( kind::AND
, eq1
, sk
.eqNode( firstChar
).negate() ), eq2
), "D-DISL-CSplit" );
3673 d_pending_req_phase
[ eq1
] = true;
3678 Trace("strings-solve") << "Non-Simple Case 1 : add lemma " << std::endl
;
3680 std::vector
< Node
> antec
;
3681 std::vector
< Node
> antec_new_lits
;
3682 antec
.insert( antec
.end(), d_normal_forms_exp
[ni
].begin(), d_normal_forms_exp
[ni
].end() );
3683 antec
.insert( antec
.end(), d_normal_forms_exp
[nj
].begin(), d_normal_forms_exp
[nj
].end() );
3685 if( areDisequal( ni
, nj
) ){
3686 antec
.push_back( ni
.eqNode( nj
).negate() );
3688 antec_new_lits
.push_back( ni
.eqNode( nj
).negate() );
3690 antec_new_lits
.push_back( li
.eqNode( lj
).negate() );
3691 std::vector
< Node
> conc
;
3692 Node sk1
= d_sk_cache
.mkSkolemCached(
3693 i
, j
, SkolemCache::SK_ID_DEQ_X
, "x_dsplit");
3694 Node sk2
= d_sk_cache
.mkSkolemCached(
3695 i
, j
, SkolemCache::SK_ID_DEQ_Y
, "y_dsplit");
3696 Node sk3
= d_sk_cache
.mkSkolemCached(
3697 i
, j
, SkolemCache::SK_ID_DEQ_Z
, "z_dsplit");
3698 registerLength(sk3
, LENGTH_GEQ_ONE
);
3699 //Node nemp = sk3.eqNode(d_emptyString).negate();
3700 //conc.push_back(nemp);
3701 Node lsk1
= mkLength( sk1
);
3702 conc
.push_back( lsk1
.eqNode( li
) );
3703 Node lsk2
= mkLength( sk2
);
3704 conc
.push_back( lsk2
.eqNode( lj
) );
3705 conc
.push_back( NodeManager::currentNM()->mkNode( kind::OR
, j
.eqNode( mkConcat( sk1
, sk3
) ), i
.eqNode( mkConcat( sk2
, sk3
) ) ) );
3706 sendInference( antec
, antec_new_lits
, NodeManager::currentNM()->mkNode( kind::AND
, conc
), "D-DISL-Split" );
3707 ++(d_statistics
.d_deq_splits
);
3710 }else if( areEqual( li
, lj
) ){
3711 Assert( !areDisequal( i
, j
) );
3712 //splitting on demand : try to make them disequal
3713 if (sendSplit(i
, j
, "S-Split(DEQL)", false))
3718 //splitting on demand : try to make lengths equal
3719 if (sendSplit(li
, lj
, "D-Split"))
3732 int TheoryStrings::processReverseDeq( std::vector
< Node
>& nfi
, std::vector
< Node
>& nfj
, Node ni
, Node nj
) {
3733 //reverse normal form of i, j
3734 std::reverse( nfi
.begin(), nfi
.end() );
3735 std::reverse( nfj
.begin(), nfj
.end() );
3738 int ret
= processSimpleDeq( nfi
, nfj
, ni
, nj
, index
, true );
3740 //reverse normal form of i, j
3741 std::reverse( nfi
.begin(), nfi
.end() );
3742 std::reverse( nfj
.begin(), nfj
.end() );
3747 int TheoryStrings::processSimpleDeq( std::vector
< Node
>& nfi
, std::vector
< Node
>& nfj
, Node ni
, Node nj
, unsigned& index
, bool isRev
){
3748 // See if one side is constant, if so, the disequality ni != nj is satisfied
3749 // since ni does not contain nj or vice versa.
3750 // This is only valid when isRev is false, since when isRev=true, the contents
3751 // of normal form vectors nfi and nfj are reversed.
3754 for (unsigned i
= 0; i
< 2; i
++)
3756 Node c
= getConstantEqc(i
== 0 ? ni
: nj
);
3760 if (!TheoryStringsRewriter::canConstantContainList(
3761 c
, i
== 0 ? nfj
: nfi
, findex
, lindex
))
3763 Trace("strings-solve-debug")
3764 << "Disequality: constant cannot contain list" << std::endl
;
3770 while( index
<nfi
.size() || index
<nfj
.size() ) {
3771 if( index
>=nfi
.size() || index
>=nfj
.size() ){
3772 Trace("strings-solve-debug") << "Disequality normalize empty" << std::endl
;
3773 std::vector
< Node
> ant
;
3774 //we have a conflict : because the lengths are equal, the remainder needs to be empty, which will lead to a conflict
3775 Node lni
= getLengthExp( ni
, ant
, d_normal_forms_base
[ni
] );
3776 Node lnj
= getLengthExp( nj
, ant
, d_normal_forms_base
[nj
] );
3777 ant
.push_back( lni
.eqNode( lnj
) );
3778 ant
.insert( ant
.end(), d_normal_forms_exp
[ni
].begin(), d_normal_forms_exp
[ni
].end() );
3779 ant
.insert( ant
.end(), d_normal_forms_exp
[nj
].begin(), d_normal_forms_exp
[nj
].end() );
3780 std::vector
< Node
> cc
;
3781 std::vector
< Node
>& nfk
= index
>=nfi
.size() ? nfj
: nfi
;
3782 for( unsigned index_k
=index
; index_k
<nfk
.size(); index_k
++ ){
3783 cc
.push_back( nfk
[index_k
].eqNode( d_emptyString
) );
3785 Node conc
= cc
.size()==1 ? cc
[0] : NodeManager::currentNM()->mkNode( kind::AND
, cc
);
3786 conc
= Rewriter::rewrite( conc
);
3787 sendInference( ant
, conc
, "Disequality Normalize Empty", true);
3790 Node i
= nfi
[index
];
3791 Node j
= nfj
[index
];
3792 Trace("strings-solve-debug") << "...Processing(QED) " << i
<< " " << j
<< std::endl
;
3793 if( !areEqual( i
, j
) ) {
3794 if( i
.getKind()==kind::CONST_STRING
&& j
.getKind()==kind::CONST_STRING
) {
3795 unsigned int len_short
= i
.getConst
<String
>().size() < j
.getConst
<String
>().size() ? i
.getConst
<String
>().size() : j
.getConst
<String
>().size();
3796 bool isSameFix
= isRev
? i
.getConst
<String
>().rstrncmp(j
.getConst
<String
>(), len_short
): i
.getConst
<String
>().strncmp(j
.getConst
<String
>(), len_short
);
3798 //same prefix/suffix
3799 //k is the index of the string that is shorter
3800 Node nk
= i
.getConst
<String
>().size() < j
.getConst
<String
>().size() ? i
: j
;
3801 Node nl
= i
.getConst
<String
>().size() < j
.getConst
<String
>().size() ? j
: i
;
3804 int new_len
= nl
.getConst
<String
>().size() - len_short
;
3805 remainderStr
= NodeManager::currentNM()->mkConst( nl
.getConst
<String
>().substr(0, new_len
) );
3806 Trace("strings-solve-debug-test") << "Rev. Break normal form of " << nl
<< " into " << nk
<< ", " << remainderStr
<< std::endl
;
3808 remainderStr
= NodeManager::currentNM()->mkConst( nl
.getConst
<String
>().substr( len_short
) );
3809 Trace("strings-solve-debug-test") << "Break normal form of " << nl
<< " into " << nk
<< ", " << remainderStr
<< std::endl
;
3811 if( i
.getConst
<String
>().size() < j
.getConst
<String
>().size() ) {
3812 nfj
.insert( nfj
.begin() + index
+ 1, remainderStr
);
3813 nfj
[index
] = nfi
[index
];
3815 nfi
.insert( nfi
.begin() + index
+ 1, remainderStr
);
3816 nfi
[index
] = nfj
[index
];
3822 std::vector
< Node
> lexp
;
3823 Node li
= getLength( i
, lexp
);
3824 Node lj
= getLength( j
, lexp
);
3825 if( areEqual( li
, lj
) && areDisequal( i
, j
) ){
3826 Trace("strings-solve") << "Simple Case 2 : found equal length disequal sub strings " << i
<< " " << j
<< std::endl
;
3827 //we are done: D-Remove
3840 void TheoryStrings::addNormalFormPair( Node n1
, Node n2
){
3841 if( !isNormalFormPair( n1
, n2
) ){
3843 NodeIntMap::const_iterator it
= d_nf_pairs
.find( n1
);
3844 if( it
!=d_nf_pairs
.end() ){
3845 index
= (*it
).second
;
3847 d_nf_pairs
[n1
] = index
+ 1;
3848 if( index
<(int)d_nf_pairs_data
[n1
].size() ){
3849 d_nf_pairs_data
[n1
][index
] = n2
;
3851 d_nf_pairs_data
[n1
].push_back( n2
);
3853 Assert( isNormalFormPair( n1
, n2
) );
3855 Trace("strings-nf-debug") << "Already a normal form pair " << n1
<< " " << n2
<< std::endl
;
3859 bool TheoryStrings::isNormalFormPair( Node n1
, Node n2
) {
3860 //TODO: modulo equality?
3861 return isNormalFormPair2( n1
, n2
) || isNormalFormPair2( n2
, n1
);
3864 bool TheoryStrings::isNormalFormPair2( Node n1
, Node n2
) {
3865 //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl;
3866 NodeIntMap::const_iterator it
= d_nf_pairs
.find( n1
);
3867 if( it
!=d_nf_pairs
.end() ){
3868 Assert( d_nf_pairs_data
.find( n1
)!=d_nf_pairs_data
.end() );
3869 for( int i
=0; i
<(*it
).second
; i
++ ){
3870 Assert( i
<(int)d_nf_pairs_data
[n1
].size() );
3871 if( d_nf_pairs_data
[n1
][i
]==n2
){
3879 void TheoryStrings::registerTerm( Node n
, int effort
) {
3880 TypeNode tn
= n
.getType();
3881 bool do_register
= true;
3884 if (options::stringEagerLen())
3886 do_register
= effort
== 0;
3890 do_register
= effort
> 0 || n
.getKind() != STRING_CONCAT
;
3897 if (d_registered_terms_cache
.find(n
) != d_registered_terms_cache
.end())
3901 d_registered_terms_cache
.insert(n
);
3902 NodeManager
* nm
= NodeManager::currentNM();
3903 Debug("strings-register") << "TheoryStrings::registerTerm() " << n
3904 << ", effort = " << effort
<< std::endl
;
3907 // register length information:
3908 // for variables, split on empty vs positive length
3909 // for concat/const/replace, introduce proxy var and state length relation
3911 if (n
.getKind() != STRING_CONCAT
&& n
.getKind() != CONST_STRING
)
3913 Node lsumb
= nm
->mkNode(STRING_LENGTH
, n
);
3914 lsum
= Rewriter::rewrite(lsumb
);
3915 // can register length term if it does not rewrite
3918 registerLength(n
, LENGTH_SPLIT
);
3922 Node sk
= d_sk_cache
.mkSkolemCached(n
, SkolemCache::SK_PURIFY
, "lsym");
3923 StringsProxyVarAttribute spva
;
3924 sk
.setAttribute(spva
, true);
3925 Node eq
= Rewriter::rewrite(sk
.eqNode(n
));
3926 Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq
3928 d_proxy_var
[n
] = sk
;
3929 Trace("strings-assert") << "(assert " << eq
<< ")" << std::endl
;
3931 Node skl
= nm
->mkNode(STRING_LENGTH
, sk
);
3932 if (n
.getKind() == STRING_CONCAT
)
3934 std::vector
<Node
> node_vec
;
3935 for (unsigned i
= 0; i
< n
.getNumChildren(); i
++)
3937 if (n
[i
].getAttribute(StringsProxyVarAttribute()))
3939 Assert(d_proxy_var_to_length
.find(n
[i
])
3940 != d_proxy_var_to_length
.end());
3941 node_vec
.push_back(d_proxy_var_to_length
[n
[i
]]);
3945 Node lni
= nm
->mkNode(STRING_LENGTH
, n
[i
]);
3946 node_vec
.push_back(lni
);
3949 lsum
= nm
->mkNode(PLUS
, node_vec
);
3950 lsum
= Rewriter::rewrite(lsum
);
3952 else if (n
.getKind() == CONST_STRING
)
3954 lsum
= nm
->mkConst(Rational(n
.getConst
<String
>().size()));
3956 Assert(!lsum
.isNull());
3957 d_proxy_var_to_length
[sk
] = lsum
;
3958 Node ceq
= Rewriter::rewrite(skl
.eqNode(lsum
));
3959 Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq
<< std::endl
;
3960 Trace("strings-lemma-debug")
3961 << " prerewrite : " << skl
.eqNode(lsum
) << std::endl
;
3962 Trace("strings-assert") << "(assert " << ceq
<< ")" << std::endl
;
3965 else if (n
.getKind() == STRING_CODE
)
3967 d_has_str_code
= true;
3968 // ite( str.len(s)==1, 0 <= str.code(s) < num_codes, str.code(s)=-1 )
3969 Node code_len
= mkLength(n
[0]).eqNode(d_one
);
3970 Node code_eq_neg1
= n
.eqNode(d_neg_one
);
3971 Node code_range
= nm
->mkNode(
3973 nm
->mkNode(GEQ
, n
, d_zero
),
3974 nm
->mkNode(LT
, n
, nm
->mkConst(Rational(CVC4::String::num_codes()))));
3975 Node lem
= nm
->mkNode(ITE
, code_len
, code_range
, code_eq_neg1
);
3976 Trace("strings-lemma") << "Strings::Lemma CODE : " << lem
<< std::endl
;
3977 Trace("strings-assert") << "(assert " << lem
<< ")" << std::endl
;
3982 bool TheoryStrings::sendInternalInference(std::vector
<Node
>& exp
,
3986 if (conc
.getKind() == AND
3987 || (conc
.getKind() == NOT
&& conc
[0].getKind() == OR
))
3989 Node conj
= conc
.getKind() == AND
? conc
: conc
[0];
3990 bool pol
= conc
.getKind() == AND
;
3992 for (const Node
& cc
: conj
)
3994 bool retc
= sendInternalInference(exp
, pol
? cc
: cc
.negate(), c
);
3999 bool pol
= conc
.getKind() != NOT
;
4000 Node lit
= pol
? conc
: conc
[0];
4001 if (lit
.getKind() == EQUAL
)
4003 for (unsigned i
= 0; i
< 2; i
++)
4005 if (!lit
[i
].isConst() && !hasTerm(lit
[i
]))
4007 // introduces a new non-constant term, do not infer
4011 // does it already hold?
4012 if (pol
? areEqual(lit
[0], lit
[1]) : areDisequal(lit
[0], lit
[1]))
4017 else if (lit
.isConst())
4019 if (lit
.getConst
<bool>())
4026 else if (!hasTerm(lit
))
4028 // introduces a new non-constant term, do not infer
4031 else if (areEqual(lit
, pol
? d_true
: d_false
))
4036 sendInference(exp
, conc
, c
);
4040 void TheoryStrings::sendInference( std::vector
< Node
>& exp
, std::vector
< Node
>& exp_n
, Node eq
, const char * c
, bool asLemma
) {
4041 eq
= eq
.isNull() ? d_false
: Rewriter::rewrite( eq
);
4043 if( Trace
.isOn("strings-infer-debug") ){
4044 Trace("strings-infer-debug") << "By " << c
<< ", infer : " << eq
<< " from: " << std::endl
;
4045 for( unsigned i
=0; i
<exp
.size(); i
++ ){
4046 Trace("strings-infer-debug") << " " << exp
[i
] << std::endl
;
4048 for( unsigned i
=0; i
<exp_n
.size(); i
++ ){
4049 Trace("strings-infer-debug") << " N:" << exp_n
[i
] << std::endl
;
4051 //Trace("strings-infer-debug") << "as lemma : " << asLemma << std::endl;
4053 //check if we should send a lemma or an inference
4054 if( asLemma
|| eq
==d_false
|| eq
.getKind()==kind::OR
|| !exp_n
.empty() || options::stringInferAsLemmas() ){
4056 if( options::stringRExplainLemmas() ){
4057 eq_exp
= mkExplain( exp
, exp_n
);
4060 eq_exp
= mkAnd( exp_n
);
4061 }else if( exp_n
.empty() ){
4062 eq_exp
= mkAnd( exp
);
4064 std::vector
< Node
> ev
;
4065 ev
.insert( ev
.end(), exp
.begin(), exp
.end() );
4066 ev
.insert( ev
.end(), exp_n
.begin(), exp_n
.end() );
4067 eq_exp
= NodeManager::currentNM()->mkNode( kind::AND
, ev
);
4070 // if we have unexplained literals, this lemma is not a conflict
4071 if (eq
== d_false
&& !exp_n
.empty())
4073 eq
= eq_exp
.negate();
4076 sendLemma( eq_exp
, eq
, c
);
4078 sendInfer( mkAnd( exp
), eq
, c
);
4083 void TheoryStrings::sendInference( std::vector
< Node
>& exp
, Node eq
, const char * c
, bool asLemma
) {
4084 std::vector
< Node
> exp_n
;
4085 sendInference( exp
, exp_n
, eq
, c
, asLemma
);
4088 void TheoryStrings::sendLemma( Node ant
, Node conc
, const char * c
) {
4089 if( conc
.isNull() || conc
== d_false
) {
4090 Trace("strings-conflict") << "Strings::Conflict : " << c
<< " : " << ant
<< std::endl
;
4091 Trace("strings-lemma") << "Strings::Conflict : " << c
<< " : " << ant
<< std::endl
;
4092 Trace("strings-assert") << "(assert (not " << ant
<< ")) ; conflict " << c
<< std::endl
;
4093 d_out
->conflict(ant
);
4097 if( ant
== d_true
) {
4100 lem
= NodeManager::currentNM()->mkNode( kind::IMPLIES
, ant
, conc
);
4102 Trace("strings-lemma") << "Strings::Lemma " << c
<< " : " << lem
<< std::endl
;
4103 Trace("strings-assert") << "(assert " << lem
<< ") ; lemma " << c
<< std::endl
;
4104 d_lemma_cache
.push_back( lem
);
4108 void TheoryStrings::sendInfer( Node eq_exp
, Node eq
, const char * c
) {
4109 if( options::stringInferSym() ){
4110 std::vector
< Node
> vars
;
4111 std::vector
< Node
> subs
;
4112 std::vector
< Node
> unproc
;
4113 inferSubstitutionProxyVars( eq_exp
, vars
, subs
, unproc
);
4114 if( unproc
.empty() ){
4115 Trace("strings-lemma-debug") << "Strings::Infer " << eq
<< " from " << eq_exp
<< " by " << c
<< std::endl
;
4116 Node eqs
= eq
.substitute( vars
.begin(), vars
.end(), subs
.begin(), subs
.end() );
4117 Trace("strings-lemma-debug") << "Strings::Infer Alternate : " << eqs
<< std::endl
;
4118 for( unsigned i
=0; i
<vars
.size(); i
++ ){
4119 Trace("strings-lemma-debug") << " " << vars
[i
] << " -> " << subs
[i
] << std::endl
;
4121 sendLemma( d_true
, eqs
, c
);
4124 for( unsigned i
=0; i
<unproc
.size(); i
++ ){
4125 Trace("strings-lemma-debug") << " non-trivial exp : " << unproc
[i
] << std::endl
;
4129 Trace("strings-lemma") << "Strings::Infer " << eq
<< " from " << eq_exp
<< " by " << c
<< std::endl
;
4130 Trace("strings-assert") << "(assert (=> " << eq_exp
<< " " << eq
<< ")) ; infer " << c
<< std::endl
;
4131 d_pending
.push_back( eq
);
4132 d_pending_exp
[eq
] = eq_exp
;
4133 d_infer
.push_back( eq
);
4134 d_infer_exp
.push_back( eq_exp
);
4137 bool TheoryStrings::sendSplit(Node a
, Node b
, const char* c
, bool preq
)
4139 Node eq
= a
.eqNode( b
);
4140 eq
= Rewriter::rewrite( eq
);
4143 Node neq
= NodeManager::currentNM()->mkNode(kind::NOT
, eq
);
4144 Node lemma_or
= NodeManager::currentNM()->mkNode(kind::OR
, eq
, neq
);
4145 Trace("strings-lemma") << "Strings::Lemma " << c
<< " SPLIT : " << lemma_or
4147 d_lemma_cache
.push_back(lemma_or
);
4148 d_pending_req_phase
[eq
] = preq
;
4149 ++(d_statistics
.d_splits
);
4155 void TheoryStrings::registerLength(Node n
, LengthStatus s
)
4157 if (d_length_lemma_terms_cache
.find(n
) != d_length_lemma_terms_cache
.end())
4161 d_length_lemma_terms_cache
.insert(n
);
4163 NodeManager
* nm
= NodeManager::currentNM();
4164 Node n_len
= nm
->mkNode(kind::STRING_LENGTH
, n
);
4166 if (s
== LENGTH_GEQ_ONE
)
4168 Node neq_empty
= n
.eqNode(d_emptyString
).negate();
4169 Node len_n_gt_z
= nm
->mkNode(GT
, n_len
, d_zero
);
4170 Node len_geq_one
= nm
->mkNode(AND
, neq_empty
, len_n_gt_z
);
4171 Trace("strings-lemma") << "Strings::Lemma SK-GEQ-ONE : " << len_geq_one
4173 Trace("strings-assert") << "(assert " << len_geq_one
<< ")" << std::endl
;
4174 d_out
->lemma(len_geq_one
);
4178 if (s
== LENGTH_ONE
)
4180 Node len_one
= n_len
.eqNode(d_one
);
4181 Trace("strings-lemma") << "Strings::Lemma SK-ONE : " << len_one
4183 Trace("strings-assert") << "(assert " << len_one
<< ")" << std::endl
;
4184 d_out
->lemma(len_one
);
4187 Assert(s
== LENGTH_SPLIT
);
4189 if( options::stringSplitEmp() || !options::stringLenGeqZ() ){
4190 Node n_len_eq_z
= n_len
.eqNode( d_zero
);
4191 Node n_len_eq_z_2
= n
.eqNode( d_emptyString
);
4192 Node case_empty
= nm
->mkNode(AND
, n_len_eq_z
, n_len_eq_z_2
);
4193 case_empty
= Rewriter::rewrite(case_empty
);
4194 Node case_nempty
= nm
->mkNode(GT
, n_len
, d_zero
);
4195 if (!case_empty
.isConst())
4197 Node lem
= nm
->mkNode(OR
, case_empty
, case_nempty
);
4199 Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << lem
4201 // prefer trying the empty case first
4202 // notice that requirePhase must only be called on rewritten literals that
4203 // occur in the CNF stream.
4204 n_len_eq_z
= Rewriter::rewrite(n_len_eq_z
);
4205 Assert(!n_len_eq_z
.isConst());
4206 d_out
->requirePhase(n_len_eq_z
, true);
4207 n_len_eq_z_2
= Rewriter::rewrite(n_len_eq_z_2
);
4208 Assert(!n_len_eq_z_2
.isConst());
4209 d_out
->requirePhase(n_len_eq_z_2
, true);
4211 else if (!case_empty
.getConst
<bool>())
4213 // the rewriter knows that n is non-empty
4214 Trace("strings-lemma")
4215 << "Strings::Lemma LENGTH > 0 (non-empty): " << case_nempty
4217 d_out
->lemma(case_nempty
);
4221 // If n = "" ---> true or len( n ) = 0 ----> true, then we expect that
4222 // n ---> "". Since this method is only called on non-constants n, it must
4223 // be that n = "" ^ len( n ) = 0 does not rewrite to true.
4228 // additionally add len( x ) >= 0 ?
4229 if( options::stringLenGeqZ() ){
4230 Node n_len_geq
= nm
->mkNode(kind::GEQ
, n_len
, d_zero
);
4231 n_len_geq
= Rewriter::rewrite( n_len_geq
);
4232 d_out
->lemma( n_len_geq
);
4236 void TheoryStrings::inferSubstitutionProxyVars( Node n
, std::vector
< Node
>& vars
, std::vector
< Node
>& subs
, std::vector
< Node
>& unproc
) {
4237 if( n
.getKind()==kind::AND
){
4238 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
4239 inferSubstitutionProxyVars( n
[i
], vars
, subs
, unproc
);
4242 }else if( n
.getKind()==kind::EQUAL
){
4243 Node ns
= n
.substitute( vars
.begin(), vars
.end(), subs
.begin(), subs
.end() );
4244 ns
= Rewriter::rewrite( ns
);
4245 if( ns
.getKind()==kind::EQUAL
){
4248 for( unsigned i
=0; i
<2; i
++ ){
4250 if( ns
[i
].getAttribute(StringsProxyVarAttribute()) ){
4252 }else if( ns
[i
].isConst() ){
4253 NodeNodeMap::const_iterator it
= d_proxy_var
.find( ns
[i
] );
4254 if( it
!=d_proxy_var
.end() ){
4260 if( v
.getNumChildren()==0 ){
4264 //both sides involved in proxy var
4275 subs
.push_back( s
);
4276 vars
.push_back( v
);
4284 unproc
.push_back( n
);
4289 Node
TheoryStrings::mkConcat( Node n1
, Node n2
) {
4290 return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, n1
, n2
) );
4293 Node
TheoryStrings::mkConcat( Node n1
, Node n2
, Node n3
) {
4294 return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, n1
, n2
, n3
) );
4297 Node
TheoryStrings::mkConcat( const std::vector
< Node
>& c
) {
4298 return Rewriter::rewrite( c
.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT
, c
) : ( c
.size()==1 ? c
[0] : d_emptyString
) );
4301 Node
TheoryStrings::mkLength( Node t
) {
4302 return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, t
) );
4305 Node
TheoryStrings::mkExplain( std::vector
< Node
>& a
) {
4306 std::vector
< Node
> an
;
4307 return mkExplain( a
, an
);
4310 Node
TheoryStrings::mkExplain( std::vector
< Node
>& a
, std::vector
< Node
>& an
) {
4311 std::vector
< TNode
> antec_exp
;
4312 for( unsigned i
=0; i
<a
.size(); i
++ ) {
4313 if( std::find( a
.begin(), a
.begin() + i
, a
[i
] )==a
.begin() + i
) {
4315 Debug("strings-explain") << "Ask for explanation of " << a
[i
] << std::endl
;
4317 if(a
[i
].getKind() == kind::EQUAL
) {
4318 //Assert( hasTerm(a[i][0]) );
4319 //Assert( hasTerm(a[i][1]) );
4320 Assert( areEqual(a
[i
][0], a
[i
][1]) );
4321 if( a
[i
][0]==a
[i
][1] ){
4324 } else if( a
[i
].getKind()==kind::NOT
&& a
[i
][0].getKind()==kind::EQUAL
) {
4325 Assert( hasTerm(a
[i
][0][0]) );
4326 Assert( hasTerm(a
[i
][0][1]) );
4327 AlwaysAssert( d_equalityEngine
.areDisequal(a
[i
][0][0], a
[i
][0][1], true) );
4328 }else if( a
[i
].getKind() == kind::AND
){
4329 for( unsigned j
=0; j
<a
[i
].getNumChildren(); j
++ ){
4330 a
.push_back( a
[i
][j
] );
4335 unsigned ps
= antec_exp
.size();
4336 explain(a
[i
], antec_exp
);
4337 Debug("strings-explain") << "Done, explanation was : " << std::endl
;
4338 for( unsigned j
=ps
; j
<antec_exp
.size(); j
++ ) {
4339 Debug("strings-explain") << " " << antec_exp
[j
] << std::endl
;
4341 Debug("strings-explain") << std::endl
;
4345 for( unsigned i
=0; i
<an
.size(); i
++ ) {
4346 if( std::find( an
.begin(), an
.begin() + i
, an
[i
] )==an
.begin() + i
){
4347 Debug("strings-explain") << "Add to explanation (new literal) " << an
[i
] << std::endl
;
4348 antec_exp
.push_back(an
[i
]);
4352 if( antec_exp
.empty() ) {
4354 } else if( antec_exp
.size()==1 ) {
4357 ant
= NodeManager::currentNM()->mkNode( kind::AND
, antec_exp
);
4359 //ant = Rewriter::rewrite( ant );
4363 Node
TheoryStrings::mkAnd( std::vector
< Node
>& a
) {
4364 std::vector
< Node
> au
;
4365 for( unsigned i
=0; i
<a
.size(); i
++ ){
4366 if( std::find( au
.begin(), au
.end(), a
[i
] )==au
.end() ){
4367 au
.push_back( a
[i
] );
4372 } else if( au
.size() == 1 ) {
4375 return NodeManager::currentNM()->mkNode( kind::AND
, au
);
4379 void TheoryStrings::getConcatVec( Node n
, std::vector
< Node
>& c
) {
4380 if( n
.getKind()==kind::STRING_CONCAT
) {
4381 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ) {
4382 if( !areEqual( n
[i
], d_emptyString
) ) {
4383 c
.push_back( n
[i
] );
4391 void TheoryStrings::checkNormalFormsDeq()
4393 std::vector
< std::vector
< Node
> > cols
;
4394 std::vector
< Node
> lts
;
4395 std::map
< Node
, std::map
< Node
, bool > > processed
;
4397 //for each pair of disequal strings, must determine whether their lengths are equal or disequal
4398 for( NodeList::const_iterator id
= d_ee_disequalities
.begin(); id
!= d_ee_disequalities
.end(); ++id
) {
4401 for( unsigned i
=0; i
<2; i
++ ){
4402 n
[i
] = d_equalityEngine
.getRepresentative( eq
[i
] );
4404 if( processed
[n
[0]].find( n
[1] )==processed
[n
[0]].end() ){
4405 processed
[n
[0]][n
[1]] = true;
4407 for( unsigned i
=0; i
<2; i
++ ){
4408 EqcInfo
* ei
= getOrMakeEqcInfo( n
[i
], false );
4409 lt
[i
] = ei
? ei
->d_length_term
: Node::null();
4410 if( lt
[i
].isNull() ){
4413 lt
[i
] = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, lt
[i
] );
4415 if( !areEqual( lt
[0], lt
[1] ) && !areDisequal( lt
[0], lt
[1] ) ){
4416 sendSplit( lt
[0], lt
[1], "DEQ-LENGTH-SP" );
4421 if( !hasProcessed() ){
4422 separateByLength( d_strings_eqc
, cols
, lts
);
4423 for( unsigned i
=0; i
<cols
.size(); i
++ ){
4424 if( cols
[i
].size()>1 && d_lemma_cache
.empty() ){
4425 Trace("strings-solve") << "- Verify disequalities are processed for " << cols
[i
][0] << ", normal form : ";
4426 printConcat( d_normal_forms
[cols
[i
][0]], "strings-solve" );
4427 Trace("strings-solve") << "... #eql = " << cols
[i
].size() << std::endl
;
4428 //must ensure that normal forms are disequal
4429 for( unsigned j
=0; j
<cols
[i
].size(); j
++ ){
4430 for( unsigned k
=(j
+1); k
<cols
[i
].size(); k
++ ){
4431 //for strings that are disequal, but have the same length
4432 if( areDisequal( cols
[i
][j
], cols
[i
][k
] ) ){
4433 Assert( !d_conflict
);
4434 Trace("strings-solve") << "- Compare " << cols
[i
][j
] << " ";
4435 printConcat( d_normal_forms
[cols
[i
][j
]], "strings-solve" );
4436 Trace("strings-solve") << " against " << cols
[i
][k
] << " ";
4437 printConcat( d_normal_forms
[cols
[i
][k
]], "strings-solve" );
4438 Trace("strings-solve") << "..." << std::endl
;
4439 processDeq( cols
[i
][j
], cols
[i
][k
] );
4440 if( hasProcessed() ){
4451 void TheoryStrings::checkLengthsEqc() {
4452 if( options::stringLenNorm() ){
4453 for( unsigned i
=0; i
<d_strings_eqc
.size(); i
++ ){
4454 //if( d_normal_forms[nodes[i]].size()>1 ) {
4455 Trace("strings-process-debug") << "Process length constraints for " << d_strings_eqc
[i
] << std::endl
;
4456 //check if there is a length term for this equivalence class
4457 EqcInfo
* ei
= getOrMakeEqcInfo( d_strings_eqc
[i
], false );
4458 Node lt
= ei
? ei
->d_length_term
: Node::null();
4459 if( !lt
.isNull() ) {
4460 Node llt
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, lt
);
4461 //now, check if length normalization has occurred
4462 if( ei
->d_normalized_length
.get().isNull() ) {
4463 Node nf
= mkConcat( d_normal_forms
[d_strings_eqc
[i
]] );
4464 if( Trace
.isOn("strings-process-debug") ){
4465 Trace("strings-process-debug") << " normal form is " << nf
<< " from base " << d_normal_forms_base
[d_strings_eqc
[i
]] << std::endl
;
4466 Trace("strings-process-debug") << " normal form exp is: " << std::endl
;
4467 for( unsigned j
=0; j
<d_normal_forms_exp
[d_strings_eqc
[i
]].size(); j
++ ){
4468 Trace("strings-process-debug") << " " << d_normal_forms_exp
[d_strings_eqc
[i
]][j
] << std::endl
;
4472 //if not, add the lemma
4473 std::vector
< Node
> ant
;
4474 ant
.insert( ant
.end(), d_normal_forms_exp
[d_strings_eqc
[i
]].begin(), d_normal_forms_exp
[d_strings_eqc
[i
]].end() );
4475 ant
.push_back( d_normal_forms_base
[d_strings_eqc
[i
]].eqNode( lt
) );
4476 Node lc
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, nf
);
4477 Node lcr
= Rewriter::rewrite( lc
);
4478 Trace("strings-process-debug") << "Rewrote length " << lc
<< " to " << lcr
<< std::endl
;
4479 Node eq
= llt
.eqNode( lcr
);
4481 ei
->d_normalized_length
.set( eq
);
4482 sendInference( ant
, eq
, "LEN-NORM", true );
4486 Trace("strings-process-debug") << "No length term for eqc " << d_strings_eqc
[i
] << " " << d_eqc_to_len_term
[d_strings_eqc
[i
]] << std::endl
;
4487 if( !options::stringEagerLen() ){
4488 Node c
= mkConcat( d_normal_forms
[d_strings_eqc
[i
]] );
4489 registerTerm( c
, 3 );
4492 NodeNodeMap::const_iterator it = d_proxy_var.find( c );
4493 if( it!=d_proxy_var.end() ){
4494 Node pv = (*it).second;
4495 Assert( d_proxy_var_to_length.find( pv )!=d_proxy_var_to_length.end() );
4496 Node pvl = d_proxy_var_to_length[pv];
4497 Node ceq = Rewriter::rewrite( mkLength( pv ).eqNode( pvl ) );
4498 sendInference( d_empty_vec, ceq, "LEN-NORM-I", true );
4505 // Trace("strings-process-debug") << "Do not process length constraints for " << nodes[i] << " " << d_normal_forms[nodes[i]].size() << std::endl;
4511 void TheoryStrings::checkCardinality() {
4512 //int cardinality = options::stringCharCardinality();
4513 //Trace("strings-solve-debug2") << "get cardinality: " << cardinality << endl;
4515 //AJR: this will create a partition of eqc, where each collection has length that are pairwise propagated to be equal.
4516 // 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).
4517 // TODO: revisit this?
4518 std::vector
< std::vector
< Node
> > cols
;
4519 std::vector
< Node
> lts
;
4520 separateByLength( d_strings_eqc
, cols
, lts
);
4522 Trace("strings-card") << "Check cardinality...." << std::endl
;
4523 for( unsigned i
= 0; i
<cols
.size(); ++i
) {
4525 Trace("strings-card") << "Number of strings with length equal to " << lr
<< " is " << cols
[i
].size() << std::endl
;
4526 if( cols
[i
].size() > 1 ) {
4528 unsigned card_need
= 1;
4529 double curr
= (double)cols
[i
].size();
4530 while( curr
>d_card_size
){
4531 curr
= curr
/(double)d_card_size
;
4534 Trace("strings-card") << "Need length " << card_need
<< " for this number of strings (where alphabet size is " << d_card_size
<< ")." << std::endl
;
4535 //check if we need to split
4536 bool needsSplit
= true;
4538 // if constant, compare
4539 Node cmp
= NodeManager::currentNM()->mkNode( kind::GEQ
, lr
, NodeManager::currentNM()->mkConst( Rational( card_need
) ) );
4540 cmp
= Rewriter::rewrite( cmp
);
4541 needsSplit
= cmp
!=d_true
;
4543 // find the minimimum constant that we are unknown to be disequal from, or otherwise stop if we increment such that cardinality does not apply
4545 bool success
= true;
4546 while( r
<card_need
&& success
){
4547 Node rr
= NodeManager::currentNM()->mkConst
<Rational
>( Rational(r
) );
4548 if( areDisequal( rr
, lr
) ){
4555 Trace("strings-card") << "Symbolic length " << lr
<< " must be at least " << r
<< " due to constant disequalities." << std::endl
;
4557 needsSplit
= r
<card_need
;
4561 unsigned int int_k
= (unsigned int)card_need
;
4562 for( std::vector
< Node
>::iterator itr1
= cols
[i
].begin();
4563 itr1
!= cols
[i
].end(); ++itr1
) {
4564 for( std::vector
< Node
>::iterator itr2
= itr1
+ 1;
4565 itr2
!= cols
[i
].end(); ++itr2
) {
4566 if(!areDisequal( *itr1
, *itr2
)) {
4568 if (sendSplit(*itr1
, *itr2
, "CARD-SP"))
4575 EqcInfo
* ei
= getOrMakeEqcInfo( lr
, true );
4576 Trace("strings-card") << "Previous cardinality used for " << lr
<< " is " << ((int)ei
->d_cardinality_lem_k
.get()-1) << std::endl
;
4577 if( int_k
+1 > ei
->d_cardinality_lem_k
.get() ){
4578 Node k_node
= NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k
) );
4579 //add cardinality lemma
4580 Node dist
= NodeManager::currentNM()->mkNode( kind::DISTINCT
, cols
[i
] );
4581 std::vector
< Node
> vec_node
;
4582 vec_node
.push_back( dist
);
4583 for( std::vector
< Node
>::iterator itr1
= cols
[i
].begin();
4584 itr1
!= cols
[i
].end(); ++itr1
) {
4585 Node len
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, *itr1
);
4587 Node len_eq_lr
= len
.eqNode(lr
);
4588 vec_node
.push_back( len_eq_lr
);
4591 Node len
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, cols
[i
][0] );
4592 Node cons
= NodeManager::currentNM()->mkNode( kind::GEQ
, len
, k_node
);
4593 cons
= Rewriter::rewrite( cons
);
4594 ei
->d_cardinality_lem_k
.set( int_k
+1 );
4596 sendInference( d_empty_vec
, vec_node
, cons
, "CARDINALITY", true );
4603 Trace("strings-card") << "...end check cardinality" << std::endl
;
4606 void TheoryStrings::getEquivalenceClasses( std::vector
< Node
>& eqcs
) {
4607 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( &d_equalityEngine
);
4608 while( !eqcs_i
.isFinished() ) {
4609 Node eqc
= (*eqcs_i
);
4610 //if eqc.getType is string
4611 if (eqc
.getType().isString()) {
4612 eqcs
.push_back( eqc
);
4618 void TheoryStrings::separateByLength(std::vector
< Node
>& n
,
4619 std::vector
< std::vector
< Node
> >& cols
,
4620 std::vector
< Node
>& lts
) {
4621 unsigned leqc_counter
= 0;
4622 std::map
< Node
, unsigned > eqc_to_leqc
;
4623 std::map
< unsigned, Node
> leqc_to_eqc
;
4624 std::map
< unsigned, std::vector
< Node
> > eqc_to_strings
;
4625 for( unsigned i
=0; i
<n
.size(); i
++ ) {
4627 Assert( d_equalityEngine
.getRepresentative(eqc
)==eqc
);
4628 EqcInfo
* ei
= getOrMakeEqcInfo( eqc
, false );
4629 Node lt
= ei
? ei
->d_length_term
: Node::null();
4631 lt
= NodeManager::currentNM()->mkNode( kind::STRING_LENGTH
, lt
);
4632 Node r
= d_equalityEngine
.getRepresentative( lt
);
4633 if( eqc_to_leqc
.find( r
)==eqc_to_leqc
.end() ){
4634 eqc_to_leqc
[r
] = leqc_counter
;
4635 leqc_to_eqc
[leqc_counter
] = r
;
4638 eqc_to_strings
[ eqc_to_leqc
[r
] ].push_back( eqc
);
4640 eqc_to_strings
[leqc_counter
].push_back( eqc
);
4644 for( std::map
< unsigned, std::vector
< Node
> >::iterator it
= eqc_to_strings
.begin(); it
!= eqc_to_strings
.end(); ++it
){
4645 cols
.push_back( std::vector
< Node
>() );
4646 cols
.back().insert( cols
.back().end(), it
->second
.begin(), it
->second
.end() );
4647 lts
.push_back( leqc_to_eqc
[it
->first
] );
4651 void TheoryStrings::printConcat( std::vector
< Node
>& n
, const char * c
) {
4652 for( unsigned i
=0; i
<n
.size(); i
++ ){
4653 if( i
>0 ) Trace(c
) << " ++ ";
4659 //// Finite Model Finding
4661 TheoryStrings::StringSumLengthDecisionStrategy::StringSumLengthDecisionStrategy(
4662 context::Context
* c
, context::UserContext
* u
, Valuation valuation
)
4663 : DecisionStrategyFmf(c
, valuation
), d_input_var_lsum(u
)
4667 bool TheoryStrings::StringSumLengthDecisionStrategy::isInitialized()
4669 return !d_input_var_lsum
.get().isNull();
4672 void TheoryStrings::StringSumLengthDecisionStrategy::initialize(
4673 const std::vector
<Node
>& vars
)
4675 if (d_input_var_lsum
.get().isNull() && !vars
.empty())
4677 NodeManager
* nm
= NodeManager::currentNM();
4678 std::vector
<Node
> sum
;
4679 for (const Node
& v
: vars
)
4681 sum
.push_back(nm
->mkNode(STRING_LENGTH
, v
));
4683 Node sumn
= sum
.size() == 1 ? sum
[0] : nm
->mkNode(PLUS
, sum
);
4684 d_input_var_lsum
.set(sumn
);
4688 Node
TheoryStrings::StringSumLengthDecisionStrategy::mkLiteral(unsigned i
)
4690 if (d_input_var_lsum
.get().isNull())
4692 return Node::null();
4694 NodeManager
* nm
= NodeManager::currentNM();
4695 Node lit
= nm
->mkNode(LEQ
, d_input_var_lsum
.get(), nm
->mkConst(Rational(i
)));
4696 Trace("strings-fmf") << "StringsFMF::mkLiteral: " << lit
<< std::endl
;
4699 std::string
TheoryStrings::StringSumLengthDecisionStrategy::identify() const
4701 return std::string("string_sum_len");
4704 Node
TheoryStrings::ppRewrite(TNode atom
) {
4705 Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom
<< std::endl
;
4707 if (options::regExpElim() && atom
.getKind() == STRING_IN_REGEXP
)
4709 // aggressive elimination of regular expression membership
4710 atomElim
= d_regexp_elim
.eliminate(atom
);
4711 if (!atomElim
.isNull())
4713 Trace("strings-ppr") << " rewrote " << atom
<< " -> " << atomElim
4714 << " via regular expression elimination."
4719 if( !options::stringLazyPreproc() ){
4720 //eager preprocess here
4721 std::vector
< Node
> new_nodes
;
4722 Node ret
= d_preproc
.processAssertion( atom
, new_nodes
);
4724 Trace("strings-ppr") << " rewrote " << atom
<< " -> " << ret
<< ", with " << new_nodes
.size() << " lemmas." << std::endl
;
4725 for( unsigned i
=0; i
<new_nodes
.size(); i
++ ){
4726 Trace("strings-ppr") << " lemma : " << new_nodes
[i
] << std::endl
;
4727 d_out
->lemma( new_nodes
[i
] );
4731 Assert( new_nodes
.empty() );
4738 TheoryStrings::Statistics::Statistics()
4739 : d_splits("theory::strings::NumOfSplitOnDemands", 0),
4740 d_eq_splits("theory::strings::NumOfEqSplits", 0),
4741 d_deq_splits("theory::strings::NumOfDiseqSplits", 0),
4742 d_loop_lemmas("theory::strings::NumOfLoops", 0)
4744 smtStatisticsRegistry()->registerStat(&d_splits
);
4745 smtStatisticsRegistry()->registerStat(&d_eq_splits
);
4746 smtStatisticsRegistry()->registerStat(&d_deq_splits
);
4747 smtStatisticsRegistry()->registerStat(&d_loop_lemmas
);
4750 TheoryStrings::Statistics::~Statistics(){
4751 smtStatisticsRegistry()->unregisterStat(&d_splits
);
4752 smtStatisticsRegistry()->unregisterStat(&d_eq_splits
);
4753 smtStatisticsRegistry()->unregisterStat(&d_deq_splits
);
4754 smtStatisticsRegistry()->unregisterStat(&d_loop_lemmas
);
4757 /** run the given inference step */
4758 void TheoryStrings::runInferStep(InferStep s
, int effort
)
4760 Trace("strings-process") << "Run " << s
;
4763 Trace("strings-process") << ", effort = " << effort
;
4765 Trace("strings-process") << "..." << std::endl
;
4768 case CHECK_INIT
: checkInit(); break;
4769 case CHECK_CONST_EQC
: checkConstantEquivalenceClasses(); break;
4770 case CHECK_EXTF_EVAL
: checkExtfEval(effort
); break;
4771 case CHECK_CYCLES
: checkCycles(); break;
4772 case CHECK_FLAT_FORMS
: checkFlatForms(); break;
4773 case CHECK_NORMAL_FORMS_EQ
: checkNormalFormsEq(); break;
4774 case CHECK_NORMAL_FORMS_DEQ
: checkNormalFormsDeq(); break;
4775 case CHECK_CODES
: checkCodes(); break;
4776 case CHECK_LENGTH_EQC
: checkLengthsEqc(); break;
4777 case CHECK_EXTF_REDUCTION
: checkExtfReductions(effort
); break;
4778 case CHECK_MEMBERSHIP
: checkMemberships(); break;
4779 case CHECK_CARDINALITY
: checkCardinality(); break;
4780 default: Unreachable(); break;
4782 Trace("strings-process") << "Done " << s
4783 << ", addedFact = " << !d_pending
.empty() << " "
4784 << !d_lemma_cache
.empty()
4785 << ", d_conflict = " << d_conflict
<< std::endl
;
4788 bool TheoryStrings::hasStrategyEffort(Effort e
) const
4790 return d_strat_steps
.find(e
) != d_strat_steps
.end();
4793 void TheoryStrings::addStrategyStep(InferStep s
, int effort
, bool addBreak
)
4795 // must run check init first
4796 Assert((s
== CHECK_INIT
)==d_infer_steps
.empty());
4797 // must use check cycles when using flat forms
4798 Assert(s
!= CHECK_FLAT_FORMS
4799 || std::find(d_infer_steps
.begin(), d_infer_steps
.end(), CHECK_CYCLES
)
4800 != d_infer_steps
.end());
4801 d_infer_steps
.push_back(s
);
4802 d_infer_step_effort
.push_back(effort
);
4805 d_infer_steps
.push_back(BREAK
);
4806 d_infer_step_effort
.push_back(0);
4810 void TheoryStrings::initializeStrategy()
4812 // initialize the strategy if not already done so
4813 if (!d_strategy_init
)
4815 std::map
<Effort
, unsigned> step_begin
;
4816 std::map
<Effort
, unsigned> step_end
;
4817 d_strategy_init
= true;
4818 // beginning indices
4819 step_begin
[EFFORT_FULL
] = 0;
4820 if (options::stringEager())
4822 step_begin
[EFFORT_STANDARD
] = 0;
4824 // add the inference steps
4825 addStrategyStep(CHECK_INIT
);
4826 addStrategyStep(CHECK_CONST_EQC
);
4827 addStrategyStep(CHECK_EXTF_EVAL
, 0);
4828 addStrategyStep(CHECK_CYCLES
);
4829 if (options::stringFlatForms())
4831 addStrategyStep(CHECK_FLAT_FORMS
);
4833 addStrategyStep(CHECK_EXTF_REDUCTION
, 1);
4834 if (options::stringEager())
4836 // do only the above inferences at standard effort, if applicable
4837 step_end
[EFFORT_STANDARD
] = d_infer_steps
.size() - 1;
4839 addStrategyStep(CHECK_NORMAL_FORMS_EQ
);
4840 addStrategyStep(CHECK_EXTF_EVAL
, 1);
4841 if (!options::stringEagerLen())
4843 addStrategyStep(CHECK_LENGTH_EQC
);
4845 addStrategyStep(CHECK_NORMAL_FORMS_DEQ
);
4846 addStrategyStep(CHECK_CODES
);
4847 if (options::stringEagerLen())
4849 addStrategyStep(CHECK_LENGTH_EQC
);
4851 if (options::stringExp() && !options::stringGuessModel())
4853 addStrategyStep(CHECK_EXTF_REDUCTION
, 2);
4855 addStrategyStep(CHECK_MEMBERSHIP
);
4856 addStrategyStep(CHECK_CARDINALITY
);
4857 step_end
[EFFORT_FULL
] = d_infer_steps
.size() - 1;
4858 if (options::stringExp() && options::stringGuessModel())
4860 step_begin
[EFFORT_LAST_CALL
] = d_infer_steps
.size();
4861 // these two steps are run in parallel
4862 addStrategyStep(CHECK_EXTF_REDUCTION
, 2, false);
4863 addStrategyStep(CHECK_EXTF_EVAL
, 3);
4864 step_end
[EFFORT_LAST_CALL
] = d_infer_steps
.size() - 1;
4866 // set the beginning/ending ranges
4867 for (const std::pair
<const Effort
, unsigned>& it_begin
: step_begin
)
4869 Effort e
= it_begin
.first
;
4870 std::map
<Effort
, unsigned>::iterator it_end
= step_end
.find(e
);
4871 Assert(it_end
!= step_end
.end());
4873 std::pair
<unsigned, unsigned>(it_begin
.second
, it_end
->second
);
4878 void TheoryStrings::runStrategy(unsigned sbegin
, unsigned send
)
4880 Trace("strings-process") << "----check, next round---" << std::endl
;
4881 for (unsigned i
= sbegin
; i
<= send
; i
++)
4883 InferStep curr
= d_infer_steps
[i
];
4893 runInferStep(curr
, d_infer_step_effort
[i
]);
4900 Trace("strings-process") << "----finished round---" << std::endl
;
4903 }/* CVC4::theory::strings namespace */
4904 }/* CVC4::theory namespace */
4905 }/* CVC4 namespace */