From 856cc3f45a1b2da648a6b85a5e774c260a83c596 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Mon, 17 Feb 2014 14:22:26 -0600 Subject: [PATCH] type conversion --- src/parser/smt2/Smt2.g | 4 + src/printer/smt2/smt2_printer.cpp | 3 + src/smt/smt_engine.cpp | 8 +- src/theory/arith/options | 2 +- src/theory/strings/kinds | 6 ++ src/theory/strings/theory_strings.cpp | 22 ++++- src/theory/strings/theory_strings.h | 3 + .../strings/theory_strings_preprocess.cpp | 99 ++++++++++++++++++- .../strings/theory_strings_rewriter.cpp | 13 ++- .../strings/theory_strings_type_rules.h | 28 ++++++ 10 files changed, 177 insertions(+), 11 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 9c2ac4c1b..6e8e9ea00 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1280,6 +1280,8 @@ builtinOp[CVC4::Kind& kind] | STRREPL_TOK { $kind = CVC4::kind::STRING_STRREPL; } | STRPREF_TOK { $kind = CVC4::kind::STRING_PREFIX; } | STRSUFF_TOK { $kind = CVC4::kind::STRING_SUFFIX; } + | STRITOS_TOK { $kind = CVC4::kind::STRING_ITOS; } + | STRSTOI_TOK { $kind = CVC4::kind::STRING_STOI; } | STRINRE_TOK { $kind = CVC4::kind::STRING_IN_REGEXP; } | STRTORE_TOK { $kind = CVC4::kind::STRING_TO_REGEXP; } | RECON_TOK { $kind = CVC4::kind::REGEXP_CONCAT; } @@ -1660,6 +1662,8 @@ STRIDOF_TOK : 'str.indexof' ; STRREPL_TOK : 'str.replace' ; STRPREF_TOK : 'str.prefixof' ; STRSUFF_TOK : 'str.suffixof' ; +STRITOS_TOK : 'int.to.str' ; +STRSTOI_TOK : 'str.to.int' ; 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 0afe29ccc..5ac56e027 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -286,6 +286,9 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, 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_ITOS: out << "int.to.str "; break; + case kind::STRING_STOI_TOTAL: + case kind::STRING_STOI: out << "str.to.int "; 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/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ef4f01cd1..dcca1624d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -954,10 +954,16 @@ void SmtEngine::setLogicInternal() throw() { options::fmfBoundInt.set( true ); Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl; } + if(! options::rewriteDivk.wasSetByUser()) { + options::rewriteDivk.set( true ); + Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl; + } + + /* if(! options::stringFMF.wasSetByUser()) { options::stringFMF.set( true ); Trace("smt") << "turning on strings-fmf, for strings-exp" << std::endl; - } + }*/ } // by default, symmetry breaker is on only for QF_UF diff --git a/src/theory/arith/options b/src/theory/arith/options index 43b582bc8..3fc08e18e 100644 --- a/src/theory/arith/options +++ b/src/theory/arith/options @@ -100,7 +100,7 @@ option arithPropAsLemmaLength --arith-prop-clauses uint16_t :default 8 :read-wri option soiQuickExplain --soi-qe bool :default false :read-write use quick explain to minimize the sum of infeasibility conflicts -option rewriteDivk rewrite-divk --rewrite-divk bool :default false +option rewriteDivk rewrite-divk --rewrite-divk bool :default false :read-write rewrite division and mod when by a constant into linear terms endmodule diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 7d631e826..09f536b15 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -21,6 +21,9 @@ operator STRING_STRIDOF 3 "string indexof" operator STRING_STRREPL 3 "string replace" operator STRING_PREFIX 2 "string prefixof" operator STRING_SUFFIX 2 "string suffixof" +operator STRING_ITOS 1 "integer to string" +operator STRING_STOI 1 "string to integer (user symbol)" +operator STRING_STOI_TOTAL 1 "string to integer (internal symbol)" #sort CHAR_TYPE \ # Cardinality::INTEGERS \ @@ -115,6 +118,9 @@ 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_ITOS ::CVC4::theory::strings::StringIntToStrTypeRule +typerule STRING_STOI ::CVC4::theory::strings::StringStrToIntTypeRule +typerule STRING_STOI_TOTAL ::CVC4::theory::strings::StringStrToIntTypeRule 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 367f3fe4f..cd583c144 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -46,6 +46,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu //d_var_lmax( c ), d_str_pos_ctn( c ), d_str_neg_ctn( c ), + d_int_to_str( c ), d_reg_exp_mem( c ), d_curr_cardinality( c, 0 ) { @@ -55,6 +56,8 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_equalityEngine.addFunctionKind(kind::STRING_CONCAT); d_equalityEngine.addFunctionKind(kind::STRING_STRCTN); d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL); + d_equalityEngine.addFunctionKind(kind::STRING_ITOS); + //d_equalityEngine.addFunctionKind(kind::STRING_STOI_TOTAL); d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); @@ -404,8 +407,13 @@ void TheoryStrings::preRegisterTerm(TNode n) { case kind::CONST_STRING: case kind::STRING_CONCAT: case kind::STRING_SUBSTR_TOTAL: + case kind::STRING_ITOS: d_equalityEngine.addTerm(n); break; + //case kind::STRING_ITOS: + //d_int_to_str; + //d_equalityEngine.addTerm(n); + //break; default: if(n.getType().isString() ) { if( std::find( d_length_intro_vars.begin(), d_length_intro_vars.end(), n )==d_length_intro_vars.end() ) { @@ -1757,7 +1765,8 @@ bool TheoryStrings::checkSimple() { //if n is concat, and //if n has not instantiatied the concat..length axiom //then, add lemma - if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT || n.getKind()==kind::STRING_SUBSTR_TOTAL ) { + if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT + || n.getKind() == kind::STRING_SUBSTR_TOTAL ) { if( d_length_nodes.find(n)==d_length_nodes.end() ) { if( d_length_inst.find(n)==d_length_inst.end() ) { //Node nr = d_equalityEngine.getRepresentative( n ); @@ -2363,7 +2372,7 @@ bool TheoryStrings::checkContains() { Trace("strings-process") << "Done check positive contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; if(!d_conflict && !addedLemma) { addedLemma = checkNegContains(); - Trace("strings-process") << "Done check positive contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + Trace("strings-process") << "Done check negative contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; } return addedLemma; } @@ -2435,8 +2444,13 @@ bool TheoryStrings::checkNegContains() { addedLemma = true; } } else if(!areDisequal(lenx, lens)) { - sendSplit(lenx, lens, "NEG-CTN-SP"); - addedLemma = true; + Node s = lenx < lens ? lenx : lens; + Node eq = s.eqNode( lenx < lens ? lens : lenx ); + if(d_str_neg_ctn_ulen.find(eq) == d_str_neg_ctn_ulen.end()) { + d_str_neg_ctn_ulen[ eq ] = true; + sendSplit(lenx, lens, "NEG-CTN-SP"); + addedLemma = true; + } } else { if(d_str_neg_ctn_rewritten.find(atom) == d_str_neg_ctn_rewritten.end()) { Node b1 = NodeManager::currentNM()->mkBoundVar("bi", NodeManager::currentNM()->integerType()); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 73d7619db..87cc3330a 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -290,9 +290,12 @@ private: // Special String Functions NodeList d_str_pos_ctn; NodeList d_str_neg_ctn; + NodeList d_int_to_str; std::map< Node, bool > d_str_ctn_eqlen; + std::map< Node, bool > d_str_neg_ctn_ulen; std::map< Node, bool > d_str_pos_ctn_rewritten; std::map< Node, bool > d_str_neg_ctn_rewritten; + std::map< std::pair , bool > d_int_to_str_rewritten; // Regular Expression private: diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 7bdacb92d..2b0cedd07 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -230,7 +230,96 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { } else { throw LogicException("string indexof not supported in this release"); } - } else if( t.getKind() == kind::STRING_STRREPL ){ + } else if( t.getKind() == kind::STRING_ITOS ) { + if(options::stringExp()) { + Node num = t[0];//NodeManager::currentNM()->mkNode(kind::ABS, t[0]); + Node pret = NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num); + Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret); + + Node b1 = NodeManager::currentNM()->mkBoundVar("x", NodeManager::currentNM()->integerType()); + Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1); + Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ), + NodeManager::currentNM()->mkNode( kind::GT, lenp, b1 ) ) ); + Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); + Node nine = NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) ); + Node ten = NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) ); + + std::vector< TypeNode > argTypes; + argTypes.push_back(NodeManager::currentNM()->integerType()); + Node ufP = NodeManager::currentNM()->mkSkolem("ufP_$$", + NodeManager::currentNM()->mkFunctionType( + argTypes, NodeManager::currentNM()->integerType()), + "uf itos assist P"); + Node ufM = NodeManager::currentNM()->mkSkolem("ufM_$$", + NodeManager::currentNM()->mkFunctionType( + argTypes, NodeManager::currentNM()->integerType()), + "uf itos assist M"); + + new_nodes.push_back( num.eqNode(NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero)) ); + new_nodes.push_back( NodeManager::currentNM()->mkNode(kind::GT, lenp, d_zero) ); + + Node ufx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, b1); + Node ufx1 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, NodeManager::currentNM()->mkNode(kind::MINUS,b1,one)); + Node ufMx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, b1); + Node b1gtz = NodeManager::currentNM()->mkNode(kind::GT, b1, d_zero); + Node cc1 = ufx1.eqNode( NodeManager::currentNM()->mkNode(kind::PLUS, + NodeManager::currentNM()->mkNode(kind::MULT, ufx, ten), + NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, NodeManager::currentNM()->mkNode(kind::MINUS,b1,one)) )); + cc1 = NodeManager::currentNM()->mkNode(kind::IMPLIES, b1gtz, cc1); + Node lstx = lenp.eqNode(NodeManager::currentNM()->mkNode(kind::PLUS, b1, one)); + Node cc2 = ufx.eqNode(ufMx); + cc2 = NodeManager::currentNM()->mkNode(kind::IMPLIES, lstx, cc2); + Node cc3 = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero); + Node cc4 = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx); + + Node b21 = NodeManager::currentNM()->mkBoundVar("y", NodeManager::currentNM()->stringType()); + Node b22 = NodeManager::currentNM()->mkBoundVar("z", NodeManager::currentNM()->stringType()); + Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b21, b22); + + Node c21 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, b21).eqNode( + NodeManager::currentNM()->mkNode(kind::MINUS, lenp, NodeManager::currentNM()->mkNode(kind::PLUS, b1, one) )); + Node ch = + NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(0))), + NodeManager::currentNM()->mkConst(::CVC4::String("0")), + NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(1))), + NodeManager::currentNM()->mkConst(::CVC4::String("1")), + NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(2))), + NodeManager::currentNM()->mkConst(::CVC4::String("2")), + NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(3))), + NodeManager::currentNM()->mkConst(::CVC4::String("3")), + NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(4))), + NodeManager::currentNM()->mkConst(::CVC4::String("4")), + NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(5))), + NodeManager::currentNM()->mkConst(::CVC4::String("5")), + NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(6))), + NodeManager::currentNM()->mkConst(::CVC4::String("6")), + NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(7))), + NodeManager::currentNM()->mkConst(::CVC4::String("7")), + NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(8))), + NodeManager::currentNM()->mkConst(::CVC4::String("8")), + NodeManager::currentNM()->mkConst(::CVC4::String("9"))))))))))); + Node c22 = pret.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, b21, ch, b22) ); + Node cc5 = NodeManager::currentNM()->mkNode(kind::EXISTS, b2v, NodeManager::currentNM()->mkNode(kind::AND, c21, c22)); + //Node pos = NodeManager::currentNM()->mkNode(kind::MINUS, lenp, NodeManager::currentNM()->mkNode(kind::PLUS, b1, one)); + //Node cc5 = ch.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, pret, pos, one) ); + Node conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, cc1, cc2, cc3, cc4, cc5) ); + conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc ); + conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc ); + new_nodes.push_back( conc ); + /* + Node sign = NodeManager::currentNM()->mkNode(kind::ITE, + NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero), + NodeManager::currentNM()->mkConst(::CVC4::String("")), + NodeManager::currentNM()->mkConst(::CVC4::String("-"))); + conc = t.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sign, pret) ); + new_nodes.push_back( conc );*/ + + d_cache[t] = t; + retNode = t; + } else { + throw LogicException("string int.to.str not supported in this release"); + } + } else if( t.getKind() == kind::STRING_STRREPL ) { if(options::stringExp()) { Node x = t[0]; Node y = t[1]; @@ -246,6 +335,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3 ), skw.eqNode(x) ) ); new_nodes.push_back( rr ); + //rr = cond.negate(); + //new_nodes.push_back( rr ); + d_cache[t] = skw; retNode = skw; } else { @@ -277,11 +369,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Trace("strings-preprocess") << "StringsPreprocess::simplify returns: " << retNode << std::endl; if(!new_nodes.empty()) { - Trace("strings-preprocess") << " ... new nodes:"; + Trace("strings-preprocess") << " ... new nodes (" << new_nodes.size() << "):\n"; for(unsigned int i=0; i().getNumerator().toUnsignedInt(); int j = node[2].getConst().getNumerator().toUnsignedInt(); - if( node[0].getConst().size() >= (unsigned) (i + j) && i>=0 && j>=0 ) { + if( i>=0 && j>=0 && node[0].getConst().size() >= (unsigned) (i + j) ) { retNode = NodeManager::currentNM()->mkConst( node[0].getConst().substr(i, j) ); } else { retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); @@ -405,6 +405,8 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { retNode = node[0]; } } + } else { + retNode = node[0]; } } else if(node.getKind() == kind::STRING_PREFIX) { if(node[0].isConst() && node[1].isConst()) { @@ -442,6 +444,15 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { node[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[1], NodeManager::currentNM()->mkNode(kind::MINUS, lent, lens), lens))); } + } else if(node.getKind() == kind::STRING_ITOS) { + if(node[0].isConst()) { + int i = node[0].getConst().getNumerator().toUnsignedInt(); + std::string stmp = static_cast( &(std::ostringstream() << i) )->str(); + retNode = NodeManager::currentNM()->mkConst( ::CVC4::String(stmp) ); + } + } else if(node.getKind() == kind::STRING_STOI_TOTAL) { + //TODO + Assert(false, "stoi not supported."); } 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 2b198892b..0c365e993 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -204,6 +204,34 @@ public: } }; +class StringIntToStrTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + if( check ) { + TypeNode t = n[0].getType(check); + if (!t.isInteger()) { + throw TypeCheckingExceptionPrivate(n, "expecting an integer term in int to string 0"); + } + } + return nodeManager->stringType(); + } +}; + +class StringStrToIntTypeRule { +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 to int 0"); + } + } + return nodeManager->integerType(); + } +}; + class RegExpConstantTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) -- 2.30.2