summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/strings/kinds10
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp86
-rw-r--r--src/theory/strings/theory_strings_preprocess.h1
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp10
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) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback