diff options
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 1 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 11 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 5 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 12 |
4 files changed, 17 insertions, 12 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index d97c07063..0afe29ccc 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -278,6 +278,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::STRING_CONCAT: out << "str.++ "; break; case kind::STRING_IN_REGEXP: out << "str.in.re "; break; case kind::STRING_LENGTH: out << "str.len "; break; + case kind::STRING_SUBSTR_TOTAL: case kind::STRING_SUBSTR: out << "str.substr "; break; case kind::STRING_CHARAT: out << "str.at "; break; case kind::STRING_STRCTN: out << "str.contain "; break; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 0b4fe80c5..367f3fe4f 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1785,17 +1785,18 @@ bool TheoryStrings::checkSimple() { //add lemma lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) ); } else if( n.getKind() == kind::STRING_SUBSTR_TOTAL ) { - lsum = n[2];/* - Node sk1 = NodeManager::currentNM()->mkSkolem( "st1_$$", NodeManager::currentNM()->stringType(), "created for substr" ); - Node sk3 = NodeManager::currentNM()->mkSkolem( "st3_$$", NodeManager::currentNM()->stringType(), "created for substr" ); - d_statistics.d_new_skolems += 2; Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ), NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) ); Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], d_zero); Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[2], d_zero); - Node x_eq_123 = n[0].eqNode(NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk, sk3 )); Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 )); + lsum = NodeManager::currentNM()->mkNode( kind::ITE, cond, n[2], d_zero ); + /* + Node sk1 = NodeManager::currentNM()->mkSkolem( "st1_$$", NodeManager::currentNM()->stringType(), "created for substr" ); + Node sk3 = NodeManager::currentNM()->mkSkolem( "st3_$$", NodeManager::currentNM()->stringType(), "created for substr" ); + d_statistics.d_new_skolems += 2; + Node x_eq_123 = n[0].eqNode(NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk, sk3 )); Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, n[1], NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); Node lemma = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i ); diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 1e2eb2572..7bdacb92d 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -180,8 +180,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node x_eq_123 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, t, sk3 ) ); Node len_sk1_eq_i = t[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); //Node len_uf_eq_j = t[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, uf ) ); - Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, - NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i )) ); + Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, + NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i ), + t.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") )) )); new_nodes.push_back( lemma ); retNode = t; d_cache[t] = t; diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index b08994927..84f58a16d 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -323,15 +323,15 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } else if(node.getKind() == kind::STRING_LENGTH) { if(node[0].isConst()) { retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst<String>().size() ) ); - } else if(node[0].getKind() == kind::STRING_SUBSTR_TOTAL) { + } /*else if(node[0].getKind() == kind::STRING_SUBSTR_TOTAL) { retNode = node[0][2]; - } else if(node[0].getKind() == kind::STRING_CONCAT) { + }*/ else if(node[0].getKind() == kind::STRING_CONCAT) { Node tmpNode = rewriteConcatString(node[0]); if(tmpNode.isConst()) { retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode.getConst<String>().size() ) ); - } else if(tmpNode.getKind() == kind::STRING_SUBSTR_TOTAL) { + } /*else if(tmpNode.getKind() == kind::STRING_SUBSTR_TOTAL) { retNode = tmpNode[2]; - } else { + }*/ else { // it has to be string concat std::vector<Node> node_vec; for(unsigned int i=0; i<tmpNode.getNumChildren(); ++i) { @@ -353,8 +353,10 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } else if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) { int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt(); int j = node[2].getConst<Rational>().getNumerator().toUnsignedInt(); - if( node[0].getConst<String>().size() >= (unsigned) (i + j) ) { + if( node[0].getConst<String>().size() >= (unsigned) (i + j) && i>=0 && j>=0 ) { retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, j) ); + } else { + retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); } } } else if(node.getKind() == kind::STRING_STRCTN) { |