diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/kinds | 10 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 86 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.h | 1 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 10 |
4 files changed, 55 insertions, 52 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 9e0897c00..b30bf8f36 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -13,9 +13,11 @@ typechecker "theory/strings/theory_strings_type_rules.h" operator STRING_CONCAT 2: "string concat" operator STRING_IN_REGEXP 2 "membership" operator STRING_LENGTH 1 "string length" -operator STRING_SUBSTR 3 "string substr" +operator STRING_SUBSTR 3 "string substr (user symbol)" +operator STRING_SUBSTR_TOTAL 3 "string substr (internal symbol)" +operator STRING_CHARAT 2 "string charat (user symbol)" +operator STRING_CHARAT_TOTAL 2 "string charat (internal symbol)" operator STRING_STRCTN 2 "string contains" -operator STRING_CHARAT 2 "string charat" operator STRING_STRIDOF 3 "string indexof" operator STRING_STRREPL 3 "string replace" @@ -105,8 +107,10 @@ typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule -typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule +typerule STRING_SUBSTR_TOTAL ::CVC4::theory::strings::StringSubstrTypeRule typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule +typerule STRING_CHARAT_TOTAL ::CVC4::theory::strings::StringCharAtTypeRule +typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 543238d31..11e206eeb 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -23,6 +23,9 @@ namespace CVC4 { namespace theory { namespace strings { +StringsPreprocess::StringsPreprocess() { +} + void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn ) { int k = r.getKind(); switch( k ) { @@ -115,48 +118,47 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // TODO // return (t0 == t[0]) ? t : NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, t0, t[1] ); //} - } else if( t.getKind() == kind::STRING_SUBSTR ){ - if(options::stringExp()) { - Node sk1 = NodeManager::currentNM()->mkSkolem( "st1_$$", t.getType(), "created for substr" ); - Node sk2 = NodeManager::currentNM()->mkSkolem( "st2_$$", t.getType(), "created for substr" ); - Node sk3 = NodeManager::currentNM()->mkSkolem( "st3_$$", t.getType(), "created for substr" ); - Node x = simplify( t[0], new_nodes ); - Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x ); - new_nodes.push_back( x_eq_123 ); - Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1], - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); - new_nodes.push_back( len_sk1_eq_i ); - Node len_sk2_eq_j = NodeManager::currentNM()->mkNode( kind::EQUAL, t[2], - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) ); - new_nodes.push_back( len_sk2_eq_j ); + } else if( t.getKind() == kind::STRING_SUBSTR_TOTAL ){ + Node sk1 = NodeManager::currentNM()->mkSkolem( "st1_$$", t.getType(), "created for substr" ); + Node sk2 = NodeManager::currentNM()->mkSkolem( "st2_$$", t.getType(), "created for substr" ); + Node sk3 = NodeManager::currentNM()->mkSkolem( "st3_$$", t.getType(), "created for substr" ); + Node x = simplify( t[0], new_nodes ); + Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ), + NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ) ); + Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x ); + Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1], + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); + Node len_sk2_eq_j = NodeManager::currentNM()->mkNode( kind::EQUAL, t[2], + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) ); - d_cache[t] = sk2; - retNode = sk2; - } else { - throw LogicException("substring not supported in this release"); - } - } else if( t.getKind() == kind::STRING_CHARAT ){ - if(options::stringExp()) { - Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", t.getType(), "created for charat" ); - Node sk2 = NodeManager::currentNM()->mkSkolem( "ca2_$$", t.getType(), "created for charat" ); - Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3_$$", t.getType(), "created for charat" ); - Node x = simplify( t[0], new_nodes ); - Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x ); - new_nodes.push_back( x_eq_123 ); - Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1], - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); - new_nodes.push_back( len_sk1_eq_i ); - Node len_sk2_eq_1 = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkConst( Rational( 1 ) ), - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) ); - new_nodes.push_back( len_sk2_eq_1 ); + Node tp = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, len_sk2_eq_j ); + tp = NodeManager::currentNM()->mkNode( kind::IMPLIES, lenxgti, tp ); + new_nodes.push_back( tp ); - d_cache[t] = sk2; - retNode = sk2; - } else { - throw LogicException("string char at not supported in this release"); - } + d_cache[t] = sk2; + retNode = sk2; + } else if( t.getKind() == kind::STRING_CHARAT_TOTAL ){ + Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", t.getType(), "created for charat" ); + Node sk2 = NodeManager::currentNM()->mkSkolem( "ca2_$$", t.getType(), "created for charat" ); + Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3_$$", t.getType(), "created for charat" ); + Node x = simplify( t[0], new_nodes ); + Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ), t[1] ); + Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x ); + Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1], + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); + Node len_sk2_eq_1 = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkConst( Rational( 1 ) ), + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) ); + + Node tp = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, len_sk2_eq_1 ); + tp = NodeManager::currentNM()->mkNode( kind::IMPLIES, lenxgti, tp ); + new_nodes.push_back( tp ); + + d_cache[t] = sk2; + retNode = sk2; } else if( t.getKind() == kind::STRING_STRIDOF ){ if(options::stringExp()) { Node sk1 = NodeManager::currentNM()->mkSkolem( "io1_$$", t[0].getType(), "created for indexof" ); @@ -224,7 +226,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { } else { throw LogicException("string replace not supported in this release"); } - } else if( t.getNumChildren()>0 ){ + } else if(t.getKind() == kind::STRING_CHARAT || t.getKind() == kind::STRING_SUBSTR) { + InternalError("CharAt and Substr should not be reached here."); + } else if( t.getNumChildren()>0 ) { std::vector< Node > cc; if (t.getMetaKind() == kind::metakind::PARAMETERIZED) { cc.push_back(t.getOperator()); diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index 698ef6ba1..6d278cc7a 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -36,6 +36,7 @@ private: Node simplify( Node t, std::vector< Node > &new_nodes ); public: void simplify(std::vector< Node > &vec_node); + StringsPreprocess(); }; }/* CVC4::theory::strings namespace */ diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index d21754820..9f278aac2 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -340,15 +340,12 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec); } } - } else if(node.getKind() == kind::STRING_SUBSTR) { + } else if(node.getKind() == kind::STRING_SUBSTR_TOTAL) { 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) ) { retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, j) ); - } else { - // TODO: some issues, must be guarded by users - retNode = NodeManager::currentNM()->mkConst( false ); } } } else if(node.getKind() == kind::STRING_STRCTN) { @@ -363,14 +360,11 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { retNode = NodeManager::currentNM()->mkConst( false ); } } - } else if(node.getKind() == kind::STRING_CHARAT) { + } else if(node.getKind() == kind::STRING_CHARAT_TOTAL) { if( node[0].isConst() && node[1].isConst() ) { int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt(); if( node[0].getConst<String>().size() > (unsigned) i ) { retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, 1) ); - } else { - // TODO: some issues, must be guarded by users - retNode = NodeManager::currentNM()->mkConst( false ); } } } else if(node.getKind() == kind::STRING_STRIDOF) { |