From 5b8a3fe89cd4b10f7bdc69dd5b1a66ebcbb823db Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Tue, 1 Oct 2013 20:03:30 -0500 Subject: [PATCH] adds partial function substr. the use of this function should be guarded, especially for disequalities --- src/parser/smt2/Smt2.g | 7 +- src/theory/strings/kinds | 3 + src/theory/strings/theory_strings.cpp | 105 +++++++++--------- .../strings/theory_strings_preprocess.cpp | 31 +++++- .../strings/theory_strings_preprocess.h | 2 +- .../strings/theory_strings_rewriter.cpp | 15 ++- .../strings/theory_strings_type_rules.h | 22 ++++ test/regress/regress0/strings/Makefile.am | 1 + test/regress/regress0/strings/substr001.smt2 | 14 +++ 9 files changed, 135 insertions(+), 65 deletions(-) create mode 100644 test/regress/regress0/strings/substr001.smt2 diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index c0365ab55..885a7c487 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -870,10 +870,6 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] expr = MK_EXPR(kind, args); } } - //| /* substring */ - //LPAREN_TOK STRSUB_TOK n1=INTEGER_LITERAL n2=INTEGER_LITERAL RPAREN_TOK - //{ - //} | /* A non-built-in function application */ LPAREN_TOK functionName[name, CHECK_DECLARED] @@ -1250,6 +1246,7 @@ builtinOp[CVC4::Kind& kind] | STRCON_TOK { $kind = CVC4::kind::STRING_CONCAT; } | STRLEN_TOK { $kind = CVC4::kind::STRING_LENGTH; } + | STRSUB_TOK { $kind = CVC4::kind::STRING_SUBSTR; } | STRINRE_TOK { $kind = CVC4::kind::STRING_IN_REGEXP; } | STRTORE_TOK { $kind = CVC4::kind::STRING_TO_REGEXP; } | RECON_TOK { $kind = CVC4::kind::REGEXP_CONCAT; } @@ -1622,7 +1619,7 @@ INT2BV_TOK : 'int2bv'; //STRCST_TOK : 'str.cst'; STRCON_TOK : 'str.++'; STRLEN_TOK : 'str.len'; -//STRSUB_TOK : 'str.sub' ; +STRSUB_TOK : 'str.sub' ; STRINRE_TOK : 'str.in.re'; STRTORE_TOK : 'str.to.re'; RECON_TOK : 're.++'; diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 814276a7c..fe7b9b3d9 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -16,6 +16,8 @@ operator STRING_IN_REGEXP 2 "membership" operator STRING_LENGTH 1 "string length" +operator STRING_SUBSTR 3 "string substr" + #sort CHAR_TYPE \ # Cardinality::INTEGERS \ # well-founded \ @@ -99,6 +101,7 @@ 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_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index bf61d3852..291af408b 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -364,7 +364,7 @@ void TheoryStrings::check(Effort e) { bool addedLemma = false; if( e == EFFORT_FULL && !d_conflict ) { eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); - while( !eqcs_i.isFinished() ){ + while( !eqcs_i.isFinished() ) { Node eqc = (*eqcs_i); //if eqc.getType is string if (eqc.getType().isString()) { @@ -372,60 +372,59 @@ void TheoryStrings::check(Effort e) { //get the constant for the equivalence class //int c_len = ...; eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); - while( !eqc_i.isFinished() ){ - Node n = (*eqc_i); - - //if n is concat, and - //if n has not instantiatied the concat..length axiom - //then, add lemma - if( n.getKind() == kind::STRING_CONCAT || n.getKind() == kind::CONST_STRING ){ - if( d_length_inst.find(n)==d_length_inst.end() ){ - d_length_inst[n] = true; - Trace("strings-debug") << "get n: " << n << endl; - Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" ); - d_length_intro_vars.push_back( sk ); - Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n ); - eq = Rewriter::rewrite(eq); - Trace("strings-lemma") << "Strings: Add lemma " << eq << std::endl; - d_out->lemma(eq); - Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); - Node lsum; - if( n.getKind() == kind::STRING_CONCAT ){ - //add lemma - std::vector node_vec; - for( unsigned i=0; imkNode( kind::STRING_LENGTH, n[i] ); - node_vec.push_back(lni); - } - lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec ); - }else{ - //add lemma - lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst().size() ) ); - } - Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum ); - ceq = Rewriter::rewrite(ceq); - Trace("strings-lemma") << "Strings: Add lemma " << ceq << std::endl; - d_out->lemma(ceq); - addedLemma = true; - } - } - ++eqc_i; - } + while( !eqc_i.isFinished() ){ + Node n = (*eqc_i); + //if n is concat, and + //if n has not instantiatied the concat..length axiom + //then, add lemma + if( n.getKind() == kind::STRING_CONCAT || n.getKind() == kind::CONST_STRING ){ + if( d_length_inst.find(n)==d_length_inst.end() ){ + d_length_inst[n] = true; + Trace("strings-debug") << "get n: " << n << endl; + Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" ); + d_length_intro_vars.push_back( sk ); + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n ); + eq = Rewriter::rewrite(eq); + Trace("strings-lemma") << "Strings: Add term lemma " << eq << std::endl; + d_out->lemma(eq); + Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); + Node lsum; + if( n.getKind() == kind::STRING_CONCAT ){ + //add lemma + std::vector node_vec; + for( unsigned i=0; imkNode( kind::STRING_LENGTH, n[i] ); + node_vec.push_back(lni); + } + lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec ); + }else{ + //add lemma + lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst().size() ) ); + } + Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum ); + ceq = Rewriter::rewrite(ceq); + Trace("strings-lemma") << "Strings: Add length lemma " << ceq << std::endl; + d_out->lemma(ceq); + addedLemma = true; + } + } + ++eqc_i; + } } ++eqcs_i; - } - if( !addedLemma ){ - addedLemma = checkNormalForms(); - Trace("strings-process") << "Done check normal forms, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; - if(!d_conflict && !addedLemma) { - addedLemma = checkCardinality(); - Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; - if( !d_conflict && !addedLemma ){ - addedLemma = checkInductiveEquations(); - Trace("strings-process") << "Done check inductive equations, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; - } - } - } + } + if( !addedLemma ){ + addedLemma = checkNormalForms(); + Trace("strings-process") << "Done check normal forms, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + if(!d_conflict && !addedLemma) { + addedLemma = checkCardinality(); + Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + if( !d_conflict && !addedLemma ){ + addedLemma = checkInductiveEquations(); + Trace("strings-process") << "Done check inductive equations, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + } + } + } } Trace("strings-check") << "Theory of strings, done check : " << e << std::endl; Trace("strings-process") << "Theory of strings, done check : " << e << std::endl; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 8fa4345e5..f303fd333 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -84,7 +84,8 @@ void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret } } -Node StringsPreprocess::simplify( Node t ) { + +Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { std::hash_map::const_iterator i = d_cache.find(t); if(i != d_cache.end()) { return (*i).second.isNull() ? t : (*i).second; @@ -92,21 +93,39 @@ Node StringsPreprocess::simplify( Node t ) { if( t.getKind() == kind::STRING_IN_REGEXP ){ // t0 in t1 + Node t0 = simplify( t[0], new_nodes ); //rewrite it std::vector< Node > ret; - simplifyRegExp( t[0], t[1], ret ); + simplifyRegExp( t0, t[1], ret ); Node n = ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret ); d_cache[t] = (t == n) ? Node::null() : n; return n; - }else if( t.getNumChildren()>0 ){ + }else if( t.getKind() == kind::STRING_SUBSTR ){ + Node sk1 = NodeManager::currentNM()->mkSkolem( "st1sym_$$", t.getType(), "created for substr" ); + Node sk2 = NodeManager::currentNM()->mkSkolem( "st2sym_$$", t.getType(), "created for substr" ); + Node sk3 = NodeManager::currentNM()->mkSkolem( "st3sym_$$", 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 ); + + d_cache[t] = sk2; + return sk2; + } else if( t.getNumChildren()>0 ){ std::vector< Node > cc; if (t.getMetaKind() == kind::metakind::PARAMETERIZED) { cc.push_back(t.getOperator()); } bool changed = false; for( unsigned i=0; i &vec_node) { + std::vector< Node > new_nodes; for( unsigned i=0; i d_cache; private: void simplifyRegExp( Node s, Node r, std::vector< Node > &ret ); - Node simplify( Node t ); + Node simplify( Node t, std::vector< Node > &new_nodes ); public: void simplify(std::vector< Node > &vec_node); }; diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 412135675..3a7ad1ee0 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -137,7 +137,20 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec); } } - } + } else if(node.getKind() == kind::STRING_SUBSTR) { + if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) { + int i = node[1].getConst().getNumerator().toUnsignedInt(); + int j = node[2].getConst().getNumerator().toUnsignedInt(); + if( node[0].getConst().size() >= (unsigned) (i + j) ) { + retNode = NodeManager::currentNM()->mkConst( node[0].getConst().substr(i, j) ); + } else { + // TODO: some issues, must be guarded by users + retNode = NodeManager::currentNM()->mkConst( false ); + } + } else { + //handled by preprocess + } + } Trace("strings-postrewrite") << "Strings::postRewrite returning " << node << std::endl; return RewriteResponse(REWRITE_DONE, retNode); diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 8fc630206..ef8f58f80 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -61,6 +61,28 @@ public: } }; +class StringSubstrTypeRule { +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 string terms in substr"); + } + t = n[1].getType(check); + if (!t.isInteger()) { + throw TypeCheckingExceptionPrivate(n, "expecting start int terms in substr"); + } + t = n[2].getType(check); + if (!t.isInteger()) { + throw TypeCheckingExceptionPrivate(n, "expecting length int terms in substr"); + } + } + return nodeManager->stringType(); + } +}; + class RegExpConstantTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 90872cf4d..9b9fdef7a 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -26,6 +26,7 @@ TESTS = \ str004.smt2 \ str005.smt2 \ model001.smt2 \ + substr001.smt2 \ loop001.smt2 \ loop002.smt2 \ loop003.smt2 \ diff --git a/test/regress/regress0/strings/substr001.smt2 b/test/regress/regress0/strings/substr001.smt2 new file mode 100644 index 000000000..b5ff587b2 --- /dev/null +++ b/test/regress/regress0/strings/substr001.smt2 @@ -0,0 +1,14 @@ +(set-logic QF_S) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun i1 () Int) +(declare-fun i2 () Int) +(declare-fun i3 () Int) +(declare-fun i4 () Int) + +(assert (= "efg" (str.sub x i1 i2) ) ) +(assert (= "bef" (str.sub x i3 i4) ) ) +(assert (> (str.len x) 5)) + +(check-sat) -- 2.30.2