From 650bb8fecf03c2af1da83177c3ad3f6c1b532294 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Thu, 16 Jan 2014 15:37:58 -0600 Subject: [PATCH] adds partial functions --- src/printer/smt2/smt2_printer.cpp | 8 +- src/smt/smt_engine.cpp | 62 +++++++++++++ src/theory/strings/kinds | 10 ++- .../strings/theory_strings_preprocess.cpp | 86 ++++++++++--------- .../strings/theory_strings_preprocess.h | 1 + .../strings/theory_strings_rewriter.cpp | 10 +-- test/regress/regress0/strings/Makefile.am | 1 + test/regress/regress0/strings/at001.smt2 | 12 +++ test/regress/regress0/strings/substr001.smt2 | 1 - 9 files changed, 136 insertions(+), 55 deletions(-) create mode 100644 test/regress/regress0/strings/at001.smt2 diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 409c9b4dd..09de0d378 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -277,9 +277,13 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::STRING_CONCAT: out << "str.++ "; break; case kind::STRING_IN_REGEXP: out << "str.in.re "; break; case kind::STRING_LENGTH: out << "str.len "; break; - case kind::STRING_SUBSTR: out << "str.substr "; break; + case kind::STRING_SUBSTR: + case kind::STRING_SUBSTR_TOTAL: + out << "str.substr "; break; + case kind::STRING_CHARAT: + case kind::STRING_CHARAT_TOTAL: + out << "str.at "; break; case kind::STRING_STRCTN: out << "str.contain "; break; - case kind::STRING_CHARAT: out << "str.at "; break; case kind::STRING_STRIDOF: out << "str.indexof "; break; case kind::STRING_STRREPL: out << "str.replace "; break; case kind::STRING_TO_REGEXP: out << "str.to.re "; break; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3c3bbe971..761348890 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -305,6 +305,13 @@ class SmtEnginePrivate : public NodeManagerListener { */ hash_map d_abstractValues; + /** + * Function symbol used to implement uninterpreted undefined string + * semantics. Needed to deal with partial charat/substr function. + */ + Node d_charAtUndef; + Node d_substrUndef; + /** * Function symbol used to implement uninterpreted division-by-zero * semantics. Needed to deal with partial division function ("/"). @@ -433,6 +440,8 @@ public: d_fakeContext(), d_abstractValueMap(&d_fakeContext), d_abstractValues(), + d_charAtUndef(), + d_substrUndef(), d_divByZero(), d_intDivByZero(), d_modZero(), @@ -1525,6 +1534,59 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map argTypes; + argTypes.push_back(NodeManager::currentNM()->stringType()); + argTypes.push_back(NodeManager::currentNM()->integerType()); + d_charAtUndef = NodeManager::currentNM()->mkSkolem("charAt_undef", + NodeManager::currentNM()->mkFunctionType( + argTypes, + NodeManager::currentNM()->stringType()), + "partial charat undef", + NodeManager::SKOLEM_EXACT_NAME); + if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) { + d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); + d_smt.d_logic.enableTheory(THEORY_UF); + d_smt.d_logic.lock(); + } + } + TNode str = n[0], num = n[1]; + Node lenx = nm->mkNode(kind::STRING_LENGTH, str); + Node cond = nm->mkNode(kind::GT, lenx, num); + Node total = nm->mkNode(kind::STRING_CHARAT_TOTAL, str, num); + Node undef = nm->mkNode(kind::APPLY_UF, d_charAtUndef, str, num); + node = nm->mkNode(kind::ITE, cond, total, undef); + } + break; + case kind::STRING_SUBSTR: { + if(d_substrUndef.isNull()) { + std::vector< TypeNode > argTypes; + argTypes.push_back(NodeManager::currentNM()->stringType()); + argTypes.push_back(NodeManager::currentNM()->integerType()); + argTypes.push_back(NodeManager::currentNM()->integerType()); + d_substrUndef = NodeManager::currentNM()->mkSkolem("substr_undef", + NodeManager::currentNM()->mkFunctionType( + argTypes, + NodeManager::currentNM()->stringType()), + "partial substring undef", + NodeManager::SKOLEM_EXACT_NAME); + if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) { + d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); + d_smt.d_logic.enableTheory(THEORY_UF); + d_smt.d_logic.lock(); + } + } + TNode str = n[0]; + Node lenx = nm->mkNode(kind::STRING_LENGTH, str); + Node num = nm->mkNode(kind::PLUS, n[1], n[2]); + Node cond = nm->mkNode(kind::GEQ, lenx, num); + Node total = nm->mkNode(kind::STRING_SUBSTR_TOTAL, str, n[1], n[2]); + Node undef = nm->mkNode(kind::APPLY_UF, d_substrUndef, str, n[1], n[2]); + node = nm->mkNode(kind::ITE, cond, total, undef); + } + break; + case kind::DIVISION: { // partial function: division if(d_divByZero.isNull()) { 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().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 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().getNumerator().toUnsignedInt(); if( node[0].getConst().size() > (unsigned) i ) { retNode = NodeManager::currentNM()->mkConst( node[0].getConst().substr(i, 1) ); - } else { - // TODO: some issues, must be guarded by users - retNode = NodeManager::currentNM()->mkConst( false ); } } } else if(node.getKind() == kind::STRING_STRIDOF) { diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index a5c6ae2f4..a2142eeb3 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -19,6 +19,7 @@ MAKEFLAGS = -k # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" TESTS = \ + at001.smt2 \ cardinality.smt2 \ str001.smt2 \ str002.smt2 \ diff --git a/test/regress/regress0/strings/at001.smt2 b/test/regress/regress0/strings/at001.smt2 new file mode 100644 index 000000000..855957430 --- /dev/null +++ b/test/regress/regress0/strings/at001.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_S) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun i () Int) + +(assert (= (str.at x i) "b")) +(assert (> i 5)) +(assert (< (str.len x) 4)) +(assert (> (str.len x) 2)) + +(check-sat) diff --git a/test/regress/regress0/strings/substr001.smt2 b/test/regress/regress0/strings/substr001.smt2 index c0554c481..476b82699 100644 --- a/test/regress/regress0/strings/substr001.smt2 +++ b/test/regress/regress0/strings/substr001.smt2 @@ -1,5 +1,4 @@ (set-logic QF_S) -(set-option :strings-exp true) (set-info :status sat) (declare-fun x () String) -- 2.30.2