diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/kinds | 4 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 5 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 36 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_type_rules.h | 36 |
4 files changed, 79 insertions, 2 deletions
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) |