summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/parser/smt2/Smt2.g4
-rw-r--r--src/printer/smt2/smt2_printer.cpp2
-rw-r--r--src/theory/strings/kinds4
-rw-r--r--src/theory/strings/theory_strings.cpp5
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp36
-rw-r--r--src/theory/strings/theory_strings_type_rules.h36
6 files changed, 85 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 497705cb6..1bfae498a 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1256,6 +1256,8 @@ builtinOp[CVC4::Kind& kind]
| STRCAT_TOK { $kind = CVC4::kind::STRING_CHARAT; }
| STRIDOF_TOK { $kind = CVC4::kind::STRING_STRIDOF; }
| STRREPL_TOK { $kind = CVC4::kind::STRING_STRREPL; }
+ | STRPREF_TOK { $kind = CVC4::kind::STRING_PREFIX; }
+ | STRSUFF_TOK { $kind = CVC4::kind::STRING_SUFFIX; }
| STRINRE_TOK { $kind = CVC4::kind::STRING_IN_REGEXP; }
| STRTORE_TOK { $kind = CVC4::kind::STRING_TO_REGEXP; }
| RECON_TOK { $kind = CVC4::kind::REGEXP_CONCAT; }
@@ -1634,6 +1636,8 @@ STRCTN_TOK : 'str.contain' ;
STRCAT_TOK : 'str.at' ;
STRIDOF_TOK : 'str.indexof' ;
STRREPL_TOK : 'str.replace' ;
+STRPREF_TOK : 'str.prefixof' ;
+STRSUFF_TOK : 'str.suffixof' ;
STRINRE_TOK : 'str.in.re';
STRTORE_TOK : 'str.to.re';
RECON_TOK : 're.++';
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index aae9938b7..d97c07063 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -283,6 +283,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
case kind::STRING_STRCTN: out << "str.contain "; break;
case kind::STRING_STRIDOF: out << "str.indexof "; break;
case kind::STRING_STRREPL: out << "str.replace "; break;
+ case kind::STRING_PREFIX: out << "str.prefixof "; break;
+ case kind::STRING_SUFFIX: out << "str.suffixof "; break;
case kind::STRING_TO_REGEXP: out << "str.to.re "; break;
case kind::REGEXP_CONCAT: out << "re.++ "; break;
case kind::REGEXP_OR: out << "re.or "; break;
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index e55891ec2..b3a75a560 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -18,6 +18,8 @@ operator STRING_CHARAT 2 "string charat (user symbol)"
operator STRING_STRCTN 2 "string contains"
operator STRING_STRIDOF 3 "string indexof"
operator STRING_STRREPL 3 "string replace"
+operator STRING_PREFIX 2 "string prefixof"
+operator STRING_SUFFIX 2 "string suffixof"
#sort CHAR_TYPE \
# Cardinality::INTEGERS \
@@ -109,6 +111,8 @@ typerule STRING_CHARAT ::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
+typerule STRING_PREFIX ::CVC4::theory::strings::StringPrefixOfTypeRule
+typerule STRING_SUFFIX ::CVC4::theory::strings::StringSuffixOfTypeRule
typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 0a8781abb..3209a92ec 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1758,8 +1758,9 @@ bool TheoryStrings::checkSimple() {
Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, n[1], d_zero);
Node x_eq_123 = n[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk, sk3 ) );
Node len_sk1_eq_i = n[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
+ Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 ));
Node lemma = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i );
- lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, lenxgti, lemma ) );
+ lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, lemma ) );
Trace("strings-lemma") << "Strings::Lemma CHARAT : " << lemma << std::endl;
d_out->lemma(lemma);
} else if( n.getKind() == kind::STRING_SUBSTR ) {
@@ -1776,7 +1777,7 @@ bool TheoryStrings::checkSimple() {
NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
Node lemma = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i );
- Node cond = NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 );
+ Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, lemma ) );
Trace("strings-lemma") << "Strings::Lemma SUBSTR : " << lemma << std::endl;
d_out->lemma(lemma);
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index ddfe1a39c..7bf016d29 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -414,6 +414,42 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
}
}
}
+ } else if(node.getKind() == kind::STRING_PREFIX) {
+ if(node[0].isConst() && node[1].isConst()) {
+ CVC4::String s = node[1].getConst<String>();
+ CVC4::String t = node[0].getConst<String>();
+ retNode = NodeManager::currentNM()->mkConst( false );
+ if(s.size() >= t.size()) {
+ if(t == s.substr(0, t.size())) {
+ retNode = NodeManager::currentNM()->mkConst( true );
+ }
+ }
+ } else {
+ Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[0]);
+ Node lent = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]);
+ retNode = NodeManager::currentNM()->mkNode(kind::AND,
+ NodeManager::currentNM()->mkNode(kind::GEQ, lent, lens),
+ node[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, node[1],
+ NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ), lens)));
+ }
+ } else if(node.getKind() == kind::STRING_SUFFIX) {
+ if(node[0].isConst() && node[1].isConst()) {
+ CVC4::String s = node[1].getConst<String>();
+ CVC4::String t = node[0].getConst<String>();
+ retNode = NodeManager::currentNM()->mkConst( false );
+ if(s.size() >= t.size()) {
+ if(t == s.substr(s.size() - t.size(), t.size())) {
+ retNode = NodeManager::currentNM()->mkConst( true );
+ }
+ }
+ } else {
+ Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[0]);
+ Node lent = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]);
+ retNode = NodeManager::currentNM()->mkNode(kind::AND,
+ NodeManager::currentNM()->mkNode(kind::GEQ, lent, lens),
+ node[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, node[1],
+ NodeManager::currentNM()->mkNode(kind::MINUS, lent, lens), lens)));
+ }
} else if(node.getKind() == kind::STRING_IN_REGEXP) {
retNode = rewriteMembership(node);
}
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 29fdf27a6..2b198892b 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -168,6 +168,42 @@ public:
}
};
+class StringPrefixOfTypeRule {
+public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ if( check ) {
+ TypeNode t = n[0].getType(check);
+ if (!t.isString()) {
+ throw TypeCheckingExceptionPrivate(n, "expecting a string term in string prefixof 0");
+ }
+ t = n[1].getType(check);
+ if (!t.isString()) {
+ throw TypeCheckingExceptionPrivate(n, "expecting a string term in string prefixof 1");
+ }
+ }
+ return nodeManager->booleanType();
+ }
+};
+
+class StringSuffixOfTypeRule {
+public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ if( check ) {
+ TypeNode t = n[0].getType(check);
+ if (!t.isString()) {
+ throw TypeCheckingExceptionPrivate(n, "expecting a string term in string suffixof 0");
+ }
+ t = n[1].getType(check);
+ if (!t.isString()) {
+ throw TypeCheckingExceptionPrivate(n, "expecting a string term in string suffixof 1");
+ }
+ }
+ return nodeManager->booleanType();
+ }
+};
+
class RegExpConstantTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback