From 6440e0675e5a9906fb9f21d1c1c119299e1cc2be Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 5 Feb 2014 09:19:23 -0600 Subject: minor fix for merge --- src/theory/strings/theory_strings.cpp | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 58344964c..3435d8f58 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1403,7 +1403,7 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) { Assert( index& nfi, std::vector< Node } else { Node i = nfi[index]; Node j = nfj[index]; - Trace("strings-solve-debug") << "...Processing " << i << " " << j << std::endl; + Trace("strings-solve-debug") << "...Processing(QED) " << i << " " << j << std::endl; if( !areEqual( i, j ) ) { if( i.getKind()==kind::CONST_STRING && j.getKind()==kind::CONST_STRING ) { unsigned int len_short = i.getConst().size() < j.getConst().size() ? i.getConst().size() : j.getConst().size(); @@ -2032,11 +2032,10 @@ bool TheoryStrings::checkCardinality() { for( unsigned i = 0; i c^k - double k = std::log( cols[i].size() ) / log((double) cardinality); - unsigned int int_k = (unsigned int)k; - Node k_node = NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k ) ); + double k = cols[i].size()==1 ? 0.0 : std::log( cols[i].size() - 1) / log((double) cardinality); + unsigned int int_k = (unsigned int) k; //double c_k = pow ( (double)cardinality, (double)lr ); if( cols[i].size() > 1 ) { bool allDisequal = true; @@ -2055,9 +2054,10 @@ bool TheoryStrings::checkCardinality() { } if(allDisequal) { EqcInfo* ei = getOrMakeEqcInfo( lr, true ); - Trace("string-cardinality") << "Previous cardinality used for " << lr << " is " << ((int)ei->d_cardinality_lem_k.get()-1) << std::endl; + Trace("strings-card") << "Previous cardinality used for " << lr << " is " << ((int)ei->d_cardinality_lem_k.get()-1) << std::endl; if( int_k+1 > ei->d_cardinality_lem_k.get() ){ - //add cardinality lemma + Node k_node = NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k ) ); + //add cardinality lemma Node dist = NodeManager::currentNM()->mkNode( kind::DISTINCT, cols[i] ); std::vector< Node > vec_node; vec_node.push_back( dist ); @@ -2065,7 +2065,7 @@ bool TheoryStrings::checkCardinality() { itr1 != cols[i].end(); ++itr1) { Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, *itr1 ); if( len!=lr ){ - Node len_eq_lr = NodeManager::currentNM()->mkNode( kind::EQUAL, lr, len ); + Node len_eq_lr = len.eqNode(lr); vec_node.push_back( len_eq_lr ); } } -- cgit v1.2.3 From 1d79a34e64be03b02339468e1d173a3f35948667 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 5 Feb 2014 09:19:23 -0600 Subject: minor fix for merge --- src/theory/strings/theory_strings.cpp | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 4fa37a732..5822192a8 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1420,7 +1420,7 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) { Assert( index& nfi, std::vector< Node } else { Node i = nfi[index]; Node j = nfj[index]; - Trace("strings-solve-debug") << "...Processing " << i << " " << j << std::endl; + Trace("strings-solve-debug") << "...Processing(QED) " << i << " " << j << std::endl; if( !areEqual( i, j ) ) { if( i.getKind()==kind::CONST_STRING && j.getKind()==kind::CONST_STRING ) { unsigned int len_short = i.getConst().size() < j.getConst().size() ? i.getConst().size() : j.getConst().size(); @@ -2049,11 +2049,10 @@ bool TheoryStrings::checkCardinality() { for( unsigned i = 0; i c^k - double k = std::log( cols[i].size() ) / log((double) cardinality); - unsigned int int_k = (unsigned int)k; - Node k_node = NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k ) ); + double k = cols[i].size()==1 ? 0.0 : std::log( cols[i].size() - 1) / log((double) cardinality); + unsigned int int_k = (unsigned int) k; //double c_k = pow ( (double)cardinality, (double)lr ); if( cols[i].size() > 1 ) { bool allDisequal = true; @@ -2072,9 +2071,10 @@ bool TheoryStrings::checkCardinality() { } if(allDisequal) { EqcInfo* ei = getOrMakeEqcInfo( lr, true ); - Trace("string-cardinality") << "Previous cardinality used for " << lr << " is " << ((int)ei->d_cardinality_lem_k.get()-1) << std::endl; + Trace("strings-card") << "Previous cardinality used for " << lr << " is " << ((int)ei->d_cardinality_lem_k.get()-1) << std::endl; if( int_k+1 > ei->d_cardinality_lem_k.get() ){ - //add cardinality lemma + Node k_node = NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k ) ); + //add cardinality lemma Node dist = NodeManager::currentNM()->mkNode( kind::DISTINCT, cols[i] ); std::vector< Node > vec_node; vec_node.push_back( dist ); @@ -2082,7 +2082,7 @@ bool TheoryStrings::checkCardinality() { itr1 != cols[i].end(); ++itr1) { Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, *itr1 ); if( len!=lr ){ - Node len_eq_lr = NodeManager::currentNM()->mkNode( kind::EQUAL, lr, len ); + Node len_eq_lr = len.eqNode(lr); vec_node.push_back( len_eq_lr ); } } -- cgit v1.2.3 From c4a9bdc1c8b166180320a9d7a126ba8d8606351d Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Thu, 6 Feb 2014 11:22:43 -0600 Subject: minor cleanup for merge --- src/theory/strings/theory_strings.cpp | 184 +++++++++++++++++----------------- 1 file changed, 92 insertions(+), 92 deletions(-) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 5822192a8..00688a95d 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -673,34 +673,34 @@ void TheoryStrings::doPendingLemmas() { bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< std::vector< Node > > &normal_forms, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src) { Trace("strings-process-debug") << "Get normal forms " << eqc << std::endl; - // EqcItr - eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); - while( !eqc_i.isFinished() ) { - Node n = (*eqc_i); - if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) { - Trace("strings-process-debug") << "Get Normal Form : Process term " << n << " in eqc " << eqc << std::endl; - std::vector nf_n; - std::vector nf_exp_n; + // EqcItr + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ) { + Node n = (*eqc_i); + if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) { + Trace("strings-process-debug") << "Get Normal Form : Process term " << n << " in eqc " << eqc << std::endl; + std::vector nf_n; + std::vector nf_exp_n; bool result = true; - if( n.getKind() == kind::CONST_STRING ){ - if( n!=d_emptyString ) { - nf_n.push_back( n ); - } - } else if( n.getKind() == kind::STRING_CONCAT ) { - for( unsigned i=0; i nf_temp; - std::vector< Node > nf_exp_temp; - Trace("strings-process-debug") << "Normalizing subterm " << n[i] << " = " << nr << std::endl; - bool nresult = false; - if( nr==eqc ){ - nf_temp.push_back( nr ); - }else{ - nresult = normalizeEquivalenceClass( nr, visited, nf_temp, nf_exp_temp ); - if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) { - return true; - } - } + if( n.getKind() == kind::CONST_STRING ) { + if( n!=d_emptyString ) { + nf_n.push_back( n ); + } + } else if( n.getKind() == kind::STRING_CONCAT ) { + for( unsigned i=0; i nf_temp; + std::vector< Node > nf_exp_temp; + Trace("strings-process-debug") << "Normalizing subterm " << n[i] << " = " << nr << std::endl; + bool nresult = false; + if( nr==eqc ) { + nf_temp.push_back( nr ); + } else { + nresult = normalizeEquivalenceClass( nr, visited, nf_temp, nf_exp_temp ); + if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) { + return true; + } + } //successfully computed normal form if( nf.size()!=1 || nf[0]!=d_emptyString ) { for( unsigned r=0; r & visited, std if( nr!=n[i] ) { nf_exp_n.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n[i], nr ) ); } - if( !nresult ){ + if( !nresult ) { //Trace("strings-process-debug") << "....Caused already asserted - for( unsigned j=i+1; j1 ){ + if( nf_n.size()>1 ) { result = false; break; } } - } - } - //if not equal to self - //if( nf_n.size()!=1 || (nf_n.size()>1 && nf_n[0]!=eqc ) ){ - if( nf_n.size()>1 || ( nf_n.size()==1 && nf_n[0].getKind()==kind::CONST_STRING ) ) { - if( nf_n.size()>1 ){ - Trace("strings-process-debug") << "Check for cycle lemma for normal form "; - printConcat(nf_n,"strings-process-debug"); - Trace("strings-process-debug") << "..." << std::endl; - for( unsigned i=0; i ant; - if( nf_n[i]!=n ){ - ant.push_back( nf_n[i].eqNode( n ) ); - } - ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() ); - std::vector< Node > cc; - for( unsigned j=0; j empty_vec; - Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc ); - sendLemma( mkExplain( ant ), conc, "CYCLE" ); - return true; - } - } - } - if( !result ) { - Trace("strings-process-debug") << "Will have cycle lemma at higher level!!!!!!!!!!!!!!!!" << std::endl; - //we have a normal form that will cause a component lemma at a higher level - normal_forms.clear(); - normal_forms_exp.clear(); - normal_form_src.clear(); - } - normal_forms.push_back(nf_n); - normal_forms_exp.push_back(nf_exp_n); - normal_form_src.push_back(n); - if( !result ){ - return false; - } - } else { - Node nn = nf_n.size()==0 ? d_emptyString : nf_n[0]; - //Assert( areEqual( nf_n[0], eqc ) ); - if( !areEqual( nn, eqc ) ){ - std::vector< Node > ant; - ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() ); - ant.push_back( n.eqNode( eqc ) ); - Node conc = nn.eqNode( eqc ); - sendLemma( mkExplain( ant ), conc, "CYCLE-T" ); - return true; - } - } - //} - } - ++eqc_i; - } + } + } + //if not equal to self + //if( nf_n.size()!=1 || (nf_n.size()>1 && nf_n[0]!=eqc ) ){ + if( nf_n.size()>1 || ( nf_n.size()==1 && nf_n[0].getKind()==kind::CONST_STRING ) ) { + if( nf_n.size()>1 ) { + Trace("strings-process-debug") << "Check for cycle lemma for normal form "; + printConcat(nf_n,"strings-process-debug"); + Trace("strings-process-debug") << "..." << std::endl; + for( unsigned i=0; i ant; + if( nf_n[i]!=n ){ + ant.push_back( nf_n[i].eqNode( n ) ); + } + ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() ); + std::vector< Node > cc; + for( unsigned j=0; j empty_vec; + Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc ); + sendLemma( mkExplain( ant ), conc, "CYCLE" ); + return true; + } + } + } + if( !result ) { + Trace("strings-process-debug") << "Will have cycle lemma at higher level!!!!!!!!!!!!!!!!" << std::endl; + //we have a normal form that will cause a component lemma at a higher level + normal_forms.clear(); + normal_forms_exp.clear(); + normal_form_src.clear(); + } + normal_forms.push_back(nf_n); + normal_forms_exp.push_back(nf_exp_n); + normal_form_src.push_back(n); + if( !result ){ + return false; + } + } else { + Node nn = nf_n.size()==0 ? d_emptyString : nf_n[0]; + //Assert( areEqual( nf_n[0], eqc ) ); + if( !areEqual( nn, eqc ) ){ + std::vector< Node > ant; + ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() ); + ant.push_back( n.eqNode( eqc ) ); + Node conc = nn.eqNode( eqc ); + sendLemma( mkExplain( ant ), conc, "CYCLE-T" ); + return true; + } + } + //} + } + ++eqc_i; + } // Test the result if( !normal_forms.empty() ) { @@ -2051,7 +2051,7 @@ bool TheoryStrings::checkCardinality() { Node lr = lts[i]; Trace("strings-card") << "Number of strings with length equal to " << lr << " is " << cols[i].size() << std::endl; // size > c^k - double k = cols[i].size()==1 ? 0.0 : std::log( cols[i].size() - 1) / log((double) cardinality); + double k = std::log( cols[i].size() ) / log((double) cardinality); unsigned int int_k = (unsigned int) k; //double c_k = pow ( (double)cardinality, (double)lr ); if( cols[i].size() > 1 ) { -- cgit v1.2.3 From d13964bd1acb6c8fd1bfaa1dca5fe1e8799fa3ab Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 5 Feb 2014 09:19:23 -0600 Subject: minor fix for merge --- src/theory/strings/theory_strings.cpp | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 4fa37a732..5822192a8 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1420,7 +1420,7 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) { Assert( index& nfi, std::vector< Node } else { Node i = nfi[index]; Node j = nfj[index]; - Trace("strings-solve-debug") << "...Processing " << i << " " << j << std::endl; + Trace("strings-solve-debug") << "...Processing(QED) " << i << " " << j << std::endl; if( !areEqual( i, j ) ) { if( i.getKind()==kind::CONST_STRING && j.getKind()==kind::CONST_STRING ) { unsigned int len_short = i.getConst().size() < j.getConst().size() ? i.getConst().size() : j.getConst().size(); @@ -2049,11 +2049,10 @@ bool TheoryStrings::checkCardinality() { for( unsigned i = 0; i c^k - double k = std::log( cols[i].size() ) / log((double) cardinality); - unsigned int int_k = (unsigned int)k; - Node k_node = NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k ) ); + double k = cols[i].size()==1 ? 0.0 : std::log( cols[i].size() - 1) / log((double) cardinality); + unsigned int int_k = (unsigned int) k; //double c_k = pow ( (double)cardinality, (double)lr ); if( cols[i].size() > 1 ) { bool allDisequal = true; @@ -2072,9 +2071,10 @@ bool TheoryStrings::checkCardinality() { } if(allDisequal) { EqcInfo* ei = getOrMakeEqcInfo( lr, true ); - Trace("string-cardinality") << "Previous cardinality used for " << lr << " is " << ((int)ei->d_cardinality_lem_k.get()-1) << std::endl; + Trace("strings-card") << "Previous cardinality used for " << lr << " is " << ((int)ei->d_cardinality_lem_k.get()-1) << std::endl; if( int_k+1 > ei->d_cardinality_lem_k.get() ){ - //add cardinality lemma + Node k_node = NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k ) ); + //add cardinality lemma Node dist = NodeManager::currentNM()->mkNode( kind::DISTINCT, cols[i] ); std::vector< Node > vec_node; vec_node.push_back( dist ); @@ -2082,7 +2082,7 @@ bool TheoryStrings::checkCardinality() { itr1 != cols[i].end(); ++itr1) { Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, *itr1 ); if( len!=lr ){ - Node len_eq_lr = NodeManager::currentNM()->mkNode( kind::EQUAL, lr, len ); + Node len_eq_lr = len.eqNode(lr); vec_node.push_back( len_eq_lr ); } } -- cgit v1.2.3 From edca72439ae37bc7a8b2b3faa44c353a3491c6cb Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Thu, 6 Feb 2014 11:22:43 -0600 Subject: minor cleanup for merge --- src/theory/strings/theory_strings.cpp | 184 +++++++++++++++++----------------- 1 file changed, 92 insertions(+), 92 deletions(-) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 5822192a8..00688a95d 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -673,34 +673,34 @@ void TheoryStrings::doPendingLemmas() { bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< std::vector< Node > > &normal_forms, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src) { Trace("strings-process-debug") << "Get normal forms " << eqc << std::endl; - // EqcItr - eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); - while( !eqc_i.isFinished() ) { - Node n = (*eqc_i); - if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) { - Trace("strings-process-debug") << "Get Normal Form : Process term " << n << " in eqc " << eqc << std::endl; - std::vector nf_n; - std::vector nf_exp_n; + // EqcItr + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ) { + Node n = (*eqc_i); + if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) { + Trace("strings-process-debug") << "Get Normal Form : Process term " << n << " in eqc " << eqc << std::endl; + std::vector nf_n; + std::vector nf_exp_n; bool result = true; - if( n.getKind() == kind::CONST_STRING ){ - if( n!=d_emptyString ) { - nf_n.push_back( n ); - } - } else if( n.getKind() == kind::STRING_CONCAT ) { - for( unsigned i=0; i nf_temp; - std::vector< Node > nf_exp_temp; - Trace("strings-process-debug") << "Normalizing subterm " << n[i] << " = " << nr << std::endl; - bool nresult = false; - if( nr==eqc ){ - nf_temp.push_back( nr ); - }else{ - nresult = normalizeEquivalenceClass( nr, visited, nf_temp, nf_exp_temp ); - if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) { - return true; - } - } + if( n.getKind() == kind::CONST_STRING ) { + if( n!=d_emptyString ) { + nf_n.push_back( n ); + } + } else if( n.getKind() == kind::STRING_CONCAT ) { + for( unsigned i=0; i nf_temp; + std::vector< Node > nf_exp_temp; + Trace("strings-process-debug") << "Normalizing subterm " << n[i] << " = " << nr << std::endl; + bool nresult = false; + if( nr==eqc ) { + nf_temp.push_back( nr ); + } else { + nresult = normalizeEquivalenceClass( nr, visited, nf_temp, nf_exp_temp ); + if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) { + return true; + } + } //successfully computed normal form if( nf.size()!=1 || nf[0]!=d_emptyString ) { for( unsigned r=0; r & visited, std if( nr!=n[i] ) { nf_exp_n.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n[i], nr ) ); } - if( !nresult ){ + if( !nresult ) { //Trace("strings-process-debug") << "....Caused already asserted - for( unsigned j=i+1; j1 ){ + if( nf_n.size()>1 ) { result = false; break; } } - } - } - //if not equal to self - //if( nf_n.size()!=1 || (nf_n.size()>1 && nf_n[0]!=eqc ) ){ - if( nf_n.size()>1 || ( nf_n.size()==1 && nf_n[0].getKind()==kind::CONST_STRING ) ) { - if( nf_n.size()>1 ){ - Trace("strings-process-debug") << "Check for cycle lemma for normal form "; - printConcat(nf_n,"strings-process-debug"); - Trace("strings-process-debug") << "..." << std::endl; - for( unsigned i=0; i ant; - if( nf_n[i]!=n ){ - ant.push_back( nf_n[i].eqNode( n ) ); - } - ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() ); - std::vector< Node > cc; - for( unsigned j=0; j empty_vec; - Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc ); - sendLemma( mkExplain( ant ), conc, "CYCLE" ); - return true; - } - } - } - if( !result ) { - Trace("strings-process-debug") << "Will have cycle lemma at higher level!!!!!!!!!!!!!!!!" << std::endl; - //we have a normal form that will cause a component lemma at a higher level - normal_forms.clear(); - normal_forms_exp.clear(); - normal_form_src.clear(); - } - normal_forms.push_back(nf_n); - normal_forms_exp.push_back(nf_exp_n); - normal_form_src.push_back(n); - if( !result ){ - return false; - } - } else { - Node nn = nf_n.size()==0 ? d_emptyString : nf_n[0]; - //Assert( areEqual( nf_n[0], eqc ) ); - if( !areEqual( nn, eqc ) ){ - std::vector< Node > ant; - ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() ); - ant.push_back( n.eqNode( eqc ) ); - Node conc = nn.eqNode( eqc ); - sendLemma( mkExplain( ant ), conc, "CYCLE-T" ); - return true; - } - } - //} - } - ++eqc_i; - } + } + } + //if not equal to self + //if( nf_n.size()!=1 || (nf_n.size()>1 && nf_n[0]!=eqc ) ){ + if( nf_n.size()>1 || ( nf_n.size()==1 && nf_n[0].getKind()==kind::CONST_STRING ) ) { + if( nf_n.size()>1 ) { + Trace("strings-process-debug") << "Check for cycle lemma for normal form "; + printConcat(nf_n,"strings-process-debug"); + Trace("strings-process-debug") << "..." << std::endl; + for( unsigned i=0; i ant; + if( nf_n[i]!=n ){ + ant.push_back( nf_n[i].eqNode( n ) ); + } + ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() ); + std::vector< Node > cc; + for( unsigned j=0; j empty_vec; + Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc ); + sendLemma( mkExplain( ant ), conc, "CYCLE" ); + return true; + } + } + } + if( !result ) { + Trace("strings-process-debug") << "Will have cycle lemma at higher level!!!!!!!!!!!!!!!!" << std::endl; + //we have a normal form that will cause a component lemma at a higher level + normal_forms.clear(); + normal_forms_exp.clear(); + normal_form_src.clear(); + } + normal_forms.push_back(nf_n); + normal_forms_exp.push_back(nf_exp_n); + normal_form_src.push_back(n); + if( !result ){ + return false; + } + } else { + Node nn = nf_n.size()==0 ? d_emptyString : nf_n[0]; + //Assert( areEqual( nf_n[0], eqc ) ); + if( !areEqual( nn, eqc ) ){ + std::vector< Node > ant; + ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() ); + ant.push_back( n.eqNode( eqc ) ); + Node conc = nn.eqNode( eqc ); + sendLemma( mkExplain( ant ), conc, "CYCLE-T" ); + return true; + } + } + //} + } + ++eqc_i; + } // Test the result if( !normal_forms.empty() ) { @@ -2051,7 +2051,7 @@ bool TheoryStrings::checkCardinality() { Node lr = lts[i]; Trace("strings-card") << "Number of strings with length equal to " << lr << " is " << cols[i].size() << std::endl; // size > c^k - double k = cols[i].size()==1 ? 0.0 : std::log( cols[i].size() - 1) / log((double) cardinality); + double k = std::log( cols[i].size() ) / log((double) cardinality); unsigned int int_k = (unsigned int) k; //double c_k = pow ( (double)cardinality, (double)lr ); if( cols[i].size() > 1 ) { -- cgit v1.2.3 From ff739bd2e4227ec3254226de86df3b39e2fa23a9 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Tue, 11 Feb 2014 16:35:17 -0600 Subject: escaped characters, having an issue with smt-lib defintion, further repair is needed. --- src/util/regexp.h | 147 ++++++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 126 insertions(+), 21 deletions(-) diff --git a/src/util/regexp.h b/src/util/regexp.h index 82b838315..4942c2652 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -22,7 +22,8 @@ #include #include -//#include "util/cvc4_assert.h" +#include +#include "util/exception.h" //#include "util/integer.h" #include "util/hash.h" @@ -30,6 +31,21 @@ namespace CVC4 { class CVC4_PUBLIC String { +public: + static unsigned int convertCharToUnsignedInt( char c ) { + int i = (int)c; + i = i-65; + return (unsigned int)(i<0 ? i+256 : i); + } + static char convertUnsignedIntToChar( unsigned int i ){ + int ii = i+65; + return (char)(ii>=256 ? ii-256 : ii); + } + static bool isPrintable( unsigned int i ){ + char c = convertUnsignedIntToChar( i ); + return isprint( (int)c ); + } + private: std::vector d_str; @@ -42,19 +58,99 @@ private: } } + //guarded + char hexToDec(char c) { + if(isdigit(c)) { + return c - '0'; + } else if (c >= 'a' && c >= 'f') { + return c - 'a' + 10; + } else { + return c - 'A' + 10; + } + } + + void toInternal(const std::string &s) { + d_str.clear(); + unsigned i=0; + while(i < s.size()) { + if(s[i] == '\\') { + i++; + if(i < s.size()) { + switch(s[i]) { + case 'n': {d_str.push_back( convertCharToUnsignedInt('\n') );i++;} break; + case 't': {d_str.push_back( convertCharToUnsignedInt('\t') );i++;} break; + case 'v': {d_str.push_back( convertCharToUnsignedInt('\v') );i++;} break; + case 'b': {d_str.push_back( convertCharToUnsignedInt('\b') );i++;} break; + case 'r': {d_str.push_back( convertCharToUnsignedInt('\r') );i++;} break; + case 'f': {d_str.push_back( convertCharToUnsignedInt('\f') );i++;} break; + case 'a': {d_str.push_back( convertCharToUnsignedInt('\a') );i++;} break; + case '\\': {d_str.push_back( convertCharToUnsignedInt('\\') );i++;} break; + case 'x': { + if(i + 2 < s.size()) { + if((isdigit(s[i+1]) || (s[i+1] >= 'a' && s[i+1] >= 'f') || (s[i+1] >= 'A' && s[i+1] >= 'F')) && + (isdigit(s[i+2]) || (s[i+2] >= 'a' && s[i+2] >= 'f') || (s[i+2] >= 'A' && s[i+2] >= 'F'))) { + d_str.push_back( convertCharToUnsignedInt( hexToDec(s[i+1]) * 16 + hexToDec(s[i+2]) ) ); + i += 3; + } else { + throw CVC4::Exception( "Error String Literal: \"" + s + "\"" ); + } + } else { + throw CVC4::Exception( "Error String Literal: \"" + s + "\"" ); + } + } + break; + default: { + if(isdigit(s[i])) { + int num = (int)s[i] - (int)'0'; + bool flag = num < 4; + if(i+1 < s.size() && num < 8 && isdigit(s[i+1]) && s[i+1] < '8') { + num = num * 8 + (int)s[i+1] - (int)'0'; + if(flag && i+2 < s.size() && isdigit(s[i+2]) && s[i+2] < '8') { + num = num * 8 + (int)s[i+2] - (int)'0'; + d_str.push_back( convertCharToUnsignedInt((char)num) ); + i += 3; + } else { + d_str.push_back( convertCharToUnsignedInt((char)num) ); + i += 2; + } + } else { + d_str.push_back( convertCharToUnsignedInt((char)num) ); + i++; + } + } else { + d_str.push_back( convertCharToUnsignedInt(s[i]) ); + i++; + } + } + } + } else { + throw CVC4::Exception( "Error String Literal: \"" + s + "\"" ); + } + } else { + d_str.push_back( convertCharToUnsignedInt(s[i]) ); + i++; + } + } + } + public: String() {} String(const std::string &s) { + toInternal(s); + /* for(unsigned int i=0; i( &(std::ostringstream() << (int)c) )->str(); + s = "\\x" + s2; + } + } + str += s; + } } return str; } @@ -237,22 +358,6 @@ public: ret_vec.insert( ret_vec.end(), itr, itr + j ); return String(ret_vec); } - -public: - static unsigned int convertCharToUnsignedInt( char c ) { - int i = (int)c; - i = i-65; - return (unsigned int)(i<0 ? i+256 : i); - } - static char convertUnsignedIntToChar( unsigned int i ){ - int ii = i+65; - return (char)(ii>=256 ? ii-256 : ii); - } - static bool isPrintable( unsigned int i ){ - char c = convertUnsignedIntToChar( i ); - return isprint( (int)c ); - } - };/* class String */ namespace strings { -- cgit v1.2.3