diff options
Diffstat (limited to 'src/theory/strings')
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 35 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 6 |
2 files changed, 23 insertions, 18 deletions
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index d53382c82..105f8dac3 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -113,6 +113,12 @@ int StringsPreprocess::checkFixLenVar( Node t ) { } } } + if(ret != 2) { + int len = t[ret].getConst<Rational>().getNumerator().toUnsignedInt(); + if(len < 2) { + ret = 2; + } + } return ret; } Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { @@ -127,22 +133,21 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { if( c_id != 2 ) { int v_id = 1 - c_id; int len = t[c_id].getConst<Rational>().getNumerator().toUnsignedInt(); - Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); - std::vector< Node > vec; - for(int i=0; i<len; i++) { - //Node sk = NodeManager::currentNM()->mkSkolem( "fl_$$", NodeManager::currentNM()->stringType(), "created for fixed length" ); - Node num = NodeManager::currentNM()->mkConst( ::CVC4::Rational(i) ); - Node sk = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, t[v_id][0], num); - vec.push_back(sk); - Node lem = one.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ) ); - new_nodes.push_back( lem ); + if(len > 1) { + Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); + std::vector< Node > vec; + for(int i=0; i<len; i++) { + Node num = NodeManager::currentNM()->mkConst( ::CVC4::Rational(i) ); + Node sk = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, t[v_id][0], num); + vec.push_back(sk); + Node lem = one.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ) ); + new_nodes.push_back( lem ); + } + Node lem = t[v_id][0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, vec ) ); + lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, t, lem ); + d_cache[t] = t; + retNode = t; } - Node lem = t[v_id][0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, vec ) ); - lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, t, lem ); - new_nodes.push_back( lem ); - - d_cache[t] = t; - retNode = t; } else if( t.getKind() == kind::STRING_IN_REGEXP ) { // t0 in t1 Node t0 = simplify( t[0], new_nodes ); diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index a4c12dfdc..78731d469 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -295,9 +295,9 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { } RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { - Trace("strings-postrewrite") << "Strings::postRewrite start " << node << std::endl; - Node retNode = node; - Node orig = retNode; + Trace("strings-postrewrite") << "Strings::postRewrite start " << node << std::endl; + Node retNode = node; + Node orig = retNode; if(node.getKind() == kind::STRING_CONCAT) { retNode = rewriteConcatString(node); |