diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-07 12:39:50 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-07 12:39:50 -0600 |
| commit | b4c7be882b88c6741212ecd9c6be4e91fec76087 (patch) | |
| tree | 0f96427e0e6f84ff6ac60ac81ff6f13459515295 /src/theory/strings | |
| parent | ea514f2aa787998ac31f8546bd202890f6bac056 (diff) | |
Minor change to F-Length inference in strings. No internal tracking of cardinality assertions in uf. Change fullModel false array collectModelInfo to assign constants.
Diffstat (limited to 'src/theory/strings')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 9f474a3ca..634c1b130 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1417,8 +1417,9 @@ void TheoryStrings::checkFlatForms() { }else{ Node curr = d_flat_form[a][count]; Node curr_c = d_eqc_to_const[curr]; + Node ac = a[d_flat_form_index[a][count]]; std::vector< Node > lexp; - Node lcurr = getLength( curr, lexp ); + Node lcurr = getLength( ac, lexp ); for( unsigned i=1; i<it->second.size(); i++ ){ b = it->second[i]; if( std::find( inelig.begin(), inelig.end(), b )==inelig.end() ){ @@ -1438,7 +1439,6 @@ void TheoryStrings::checkFlatForms() { }else{ Node cc = d_flat_form[b][count]; if( cc!=curr ){ - Node ac = a[d_flat_form_index[a][count]]; Node bc = b[d_flat_form_index[b][count]]; inelig.push_back( b ); Assert( !areEqual( curr, cc ) ); @@ -1463,10 +1463,14 @@ void TheoryStrings::checkFlatForms() { }else{ //if lengths are the same, apply LengthEq std::vector< Node > lexp2; - Node lcc = getLength( cc, lexp2 ); + Node lcc = getLength( bc, lexp2 ); if( areEqual( lcurr, lcc ) ){ Trace("strings-ff-debug") << "Infer " << ac << " == " << bc << " since " << lcurr << " == " << lcc << std::endl; //exp_n.push_back( getLength( curr, true ).eqNode( getLength( cc, true ) ) ); + Trace("strings-ff-debug") << "Explanation for " << lcurr << " is "; + for( unsigned j=0; j<lexp.size(); j++ ) { Trace("strings-ff-debug") << lexp[j] << std::endl; } + Trace("strings-ff-debug") << "Explanation for " << lcc << " is "; + for( unsigned j=0; j<lexp2.size(); j++ ) { Trace("strings-ff-debug") << lexp2[j] << std::endl; } exp.insert( exp.end(), lexp.begin(), lexp.end() ); exp.insert( exp.end(), lexp2.begin(), lexp2.end() ); addToExplanation( lcurr, lcc, exp ); @@ -2755,6 +2759,7 @@ void TheoryStrings::sendInference( std::vector< Node >& exp, std::vector< Node > for( unsigned i=0; i<exp_n.size(); i++ ){ Trace("strings-infer-debug") << " N:" << exp_n[i] << std::endl; } + //Trace("strings-infer-debug") << "as lemma : " << asLemma << std::endl; } bool doSendLemma = ( asLemma || eq==d_false || eq.getKind()==kind::OR || options::stringInferAsLemmas() ); if( doSendLemma ){ |