From: Tianyi Liang Date: Wed, 29 Jan 2014 16:32:17 +0000 (-0600) Subject: add prefixof, suffixof X-Git-Tag: cvc5-1.0.0~7116 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8c4a79a1dfc47572e81506cc1de9372370199f74;p=cvc5.git add prefixof, suffixof --- 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(); + CVC4::String t = node[0].getConst(); + 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(); + CVC4::String t = node[0].getConst(); + 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)