- if( !hasProcessed() ){
- //get equivalence classes
- //std::vector< Node > eqcs;
- //getEquivalenceClasses( eqcs );
- Trace("strings-process") << "Normalize equivalence classes...." << std::endl;
- //calculate normal forms for each equivalence class, possibly adding splitting lemmas
- d_normal_forms.clear();
- d_normal_forms_exp.clear();
- std::map< Node, Node > nf_to_eqc;
- std::map< Node, Node > eqc_to_exp;
- for( unsigned i=0; i<eqcs.size(); i++ ) {
- Node eqc = eqcs[i];
- Trace("strings-process-debug") << "- Verify normal forms are the same for " << eqc << std::endl;
- std::vector< Node > visited;
- std::vector< Node > nf;
- std::vector< Node > nf_exp;
- normalizeEquivalenceClass(eqc, visited, nf, nf_exp);
- Trace("strings-debug") << "Finished normalizing eqc..." << std::endl;
- if( d_conflict ) {
- return;
- } else if ( d_pending.empty() && d_lemma_cache.empty() ) {
- Node nf_term;
- if( nf.size()==0 ){
- nf_term = d_emptyString;
- }else if( nf.size()==1 ) {
- nf_term = nf[0];
- } else {
- nf_term = mkConcat( nf );
- }
- nf_term = Rewriter::rewrite( nf_term );
- Trace("strings-debug") << "Make nf_term_exp..." << std::endl;
- Node nf_term_exp = nf_exp.empty() ? d_true : nf_exp.size()==1 ? nf_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, nf_exp );
- if( nf_to_eqc.find(nf_term)!=nf_to_eqc.end() ) {
- //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl;
- //two equivalence classes have same normal form, merge
- Node eq_exp = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, nf_term_exp, eqc_to_exp[nf_to_eqc[nf_term]] ) );
- Node eq = eqc.eqNode( nf_to_eqc[nf_term] );
- sendInfer( eq_exp, eq, "Normal_Form" );
- //d_equalityEngine.assertEquality( eq, true, eq_exp );
- } else {
- nf_to_eqc[nf_term] = eqc;
- eqc_to_exp[eqc] = nf_term_exp;
+ //inferences without recursively expanding flat forms (TODO)
+ /*
+ for( unsigned k=0; k<d_eqcs.size(); k++ ){
+ Node eqc = d_eqcs[k];
+ Node c;
+ std::map< Node, Node >::iterator itc = d_eqc_to_const.find( eqc );
+ if( itc!=d_eqc_to_const.end() ){
+ c = itc->second;
+ }
+ std::map< Node, std::vector< Node > >::iterator it = d_eqc.find( eqc );
+ if( it!=d_eqc.end() && it->second.size()>1 ){
+ for( unsigned r=0; r<2; r++ ){
+ bool success;
+ int count = 0;
+ do{
+ success = true;
+ Node curr = d_flat_form[it->second[0]][count];
+ Node lcurr = getLength( curr );
+ for( unsigned i=1; i<it->second.size(); i++ ){
+ Node cc = d_flat_form[it->second[i]][count];
+ if( cc!=curr ){
+ //constant conflict? TODO
+ //if lengths are the same, apply LengthEq
+ Node lcc = getLength( cc );
+ if( areEqual( lcurr, lcc ) ){
+ std::vector< Node > exp;
+ Node a = it->second[0];
+ Node b = it->second[i];
+ addToExplanation( a, b, exp );
+ //explain why prefixes up to now were the same
+ for( unsigned j=0; j<count; j++ ){
+ addToExplanation( a[d_flat_form_index[a][j]], b[d_flat_form_index[b][j]], exp );
+ }
+ //explain why components are empty
+ //TODO
+ addToExplanation( lcurr, lcc, exp );
+ sendInfer( mkAnd( exp ), curr.eqNode( cc ), "F-LengthEq" );
+ return;
+ }
+ success = false;
+ }
+ }
+ count++;
+ //check if we are at the endpoint of any string
+ for( unsigned i=0; i<it->second.size(); i++ ){
+ if( count==d_flat_form[it->second[i]].size() ){
+ Node a = it->second[i];
+ for( unsigned j=0; j<it->second.size(); j++ ){
+ if( i!=j ){
+ //remainder must be empty
+ if( count<d_flat_form[it->second[j]].size() ){
+ Node b = it->second[j];
+ std::vector< Node > exp;
+ addToExplanation( a, b, exp );
+ for( unsigned j=0; j<count; j++ ){
+ addToExplanation( a[d_flat_form_index[a][j]], b[d_flat_form_index[b][j]], exp );
+ }
+
+ }
+ }
+ }
+ }
+ }
+ }while( success && );
+
+ if( r==1 ){
+ for( unsigned i=0; i<it->second.size(); i++ ){
+ std::reverse( d_flat_form[it->second].begin(), d_flat_form[it->second].end() );
+ std::reverse( d_flat_form_index[it->second].begin(), d_flat_form_index[it->second].end() );
+ }
+ }