diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-05 09:19:23 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-11 16:36:27 -0600 |
| commit | af120ba0b8565ec1d49b69924d3ebc4a81d5fbe1 (patch) | |
| tree | bd7199d5afef1232df8d3ba01605fca914e141a2 /src/theory/strings | |
| parent | 9fc5c9d2c52b22cd3246f78dff7e1027675f288e (diff) | |
minor fix for merge
Diffstat (limited to 'src/theory/strings')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 18 |
1 files 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.size() && index<nfj.size() ); Node i = nfi[index]; Node j = nfj[index]; - Trace("strings-solve-debug") << "...Processing " << i << " " << j << std::endl; + Trace("strings-solve-debug") << "...Processing(DEQ) " << i << " " << j << std::endl; if( !areEqual( i, j ) ) { Assert( i.getKind()!=kind::CONST_STRING || j.getKind()!=kind::CONST_STRING ); Node li = getLength( i ); @@ -1521,7 +1521,7 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& 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<String>().size() < j.getConst<String>().size() ? i.getConst<String>().size() : j.getConst<String>().size(); @@ -2049,11 +2049,10 @@ bool TheoryStrings::checkCardinality() { for( unsigned i = 0; i<cols.size(); ++i ){ Node lr = lts[i]; - Trace("string-cardinality") << "Number of strings with length equal to " << lr << " is " << cols[i].size() << std::endl; + Trace("strings-card") << "Number of strings with length equal to " << lr << " is " << cols[i].size() << std::endl; // size > 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 ); } } |