diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/parser/smt2/Smt2.g | 4 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 2 | ||||
-rw-r--r-- | src/smt/options_handlers.h | 7 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 66 | ||||
-rw-r--r-- | src/theory/arith/options | 2 | ||||
-rw-r--r-- | src/theory/strings/kinds | 4 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 23 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.h | 3 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 215 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.h | 1 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 26 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_type_rules.h | 28 | ||||
-rw-r--r-- | src/util/regexp.h | 21 |
13 files changed, 363 insertions, 39 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..5dc3043af 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -286,6 +286,8 @@ 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: 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/options_handlers.h b/src/smt/options_handlers.h index 51ad7b6ca..c9c3d6345 100644 --- a/src/smt/options_handlers.h +++ b/src/smt/options_handlers.h @@ -83,9 +83,9 @@ assertions\n\ + Output the assertions after preprocessing and before clausification.\n\ Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\ where PASS is one of the preprocessing passes: definition-expansion\n\ - boolean-terms constrain-subtypes substitution skolem-quant simplify\n\ - static-learning ite-removal repeat-simplify rewrite-apply-to-const\n\ - theory-preprocessing.\n\ + boolean-terms constrain-subtypes substitution strings-pp skolem-quant\n\ + simplify static-learning ite-removal repeat-simplify\n\ + rewrite-apply-to-const theory-preprocessing.\n\ PASS can also be the special value \"everything\", in which case the\n\ assertions are printed before any preprocessing (with\n\ \"assertions:pre-everything\") or after all preprocessing completes\n\ @@ -181,6 +181,7 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) { } else if(!strcmp(p, "boolean-terms")) { } else if(!strcmp(p, "constrain-subtypes")) { } else if(!strcmp(p, "substitution")) { + } else if(!strcmp(p, "strings-pp")) { } else if(!strcmp(p, "skolem-quant")) { } else if(!strcmp(p, "simplify")) { } else if(!strcmp(p, "static-learning")) { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ef4f01cd1..7ada9d350 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -313,6 +313,12 @@ class SmtEnginePrivate : public NodeManagerListener { Node d_ufSubstr; /** + * Function symbol used to implement uninterpreted undefined string + * semantics. Needed to deal with partial str2int function. + */ + Node d_ufS2I; + + /** * Function symbol used to implement uninterpreted division-by-zero * semantics. Needed to deal with partial division function ("/"). */ @@ -787,6 +793,34 @@ void SmtEngine::finalOptionsAreSet() { return; } + // for strings + if(options::stringExp()) { + if( !d_logic.isQuantified() ) { + d_logic = d_logic.getUnlockedCopy(); + d_logic.enableQuantifiers(); + Trace("smt") << "turning on quantifier logic, for strings-exp" << std::endl; + } + if(! options::finiteModelFind.wasSetByUser()) { + options::finiteModelFind.set( true ); + Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl; + } + if(! options::fmfBoundInt.wasSetByUser()) { + 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; + } + */ + } + if(options::bitvectorEagerBitblast()) { // Eager solver should use the internal decision strategy options::decisionMode.set(DECISION_STRATEGY_INTERNAL); @@ -937,29 +971,6 @@ void SmtEngine::setLogicInternal() throw() { } } - - // for strings - if(options::stringExp()) { - if( !d_logic.isQuantified() ) { - d_logic = d_logic.getUnlockedCopy(); - d_logic.enableQuantifiers(); - d_logic.lock(); - Trace("smt") << "turning on quantifier logic, for strings-exp" << std::endl; - } - if(! options::finiteModelFind.wasSetByUser()) { - options::finiteModelFind.set( true ); - Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl; - } - if(! options::fmfBoundInt.wasSetByUser()) { - options::fmfBoundInt.set( true ); - Trace("smt") << "turning on fmf-bound-int, 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 if(! options::ufSymmetryBreaker.wasSetByUser()) { bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified(); @@ -3118,11 +3129,18 @@ void SmtEnginePrivate::processAssertions() { // Assertions ARE guaranteed to be rewritten by this point if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) { + dumpAssertions("pre-strings-pp", d_assertionsToPreprocess); CVC4::theory::strings::StringsPreprocess sp; - sp.simplify( d_assertionsToPreprocess ); + std::vector<Node> newNodes; + newNodes.push_back(d_assertionsToPreprocess[d_realAssertionsEnd - 1]); + sp.simplify( d_assertionsToPreprocess, newNodes ); + if(newNodes.size() > 1) { + d_assertionsToPreprocess[d_realAssertionsEnd - 1] = NodeManager::currentNM()->mkNode(kind::AND, newNodes); + } for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] ); } + dumpAssertions("post-strings-pp", d_assertionsToPreprocess); } if( d_smt.d_logic.isQuantified() ){ dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess); 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..7fbefe251 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -21,6 +21,8 @@ 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 (total function)" #sort CHAR_TYPE \ # Cardinality::INTEGERS \ @@ -115,6 +117,8 @@ 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_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 367f3fe4f..d8b20d890 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); d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); @@ -404,8 +407,14 @@ void TheoryStrings::preRegisterTerm(TNode n) { case kind::CONST_STRING: case kind::STRING_CONCAT: case kind::STRING_SUBSTR_TOTAL: + case kind::STRING_ITOS: + case kind::STRING_STOI: 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 +1766,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 +2373,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 +2445,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 <Node, int>, 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..43e7829bb 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -230,7 +230,206 @@ 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 type conv P"); + Node ufM = NodeManager::currentNM()->mkSkolem("ufM_$$", + NodeManager::currentNM()->mkFunctionType( + argTypes, NodeManager::currentNM()->integerType()), + "uf type conv 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_STOI ) { + if(options::stringExp()) { + Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) ); + 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 type conv P"); + Node ufM = NodeManager::currentNM()->mkSkolem("ufM_$$", + NodeManager::currentNM()->mkFunctionType( + argTypes, NodeManager::currentNM()->integerType()), + "uf type conv M"); + + Node ufP0 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero); + new_nodes.push_back(t.eqNode(ufP0)); + //cc1 + Node cc1 = t[0].eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(""))); + cc1 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(negone), cc1); + //cc2 + Node b1 = NodeManager::currentNM()->mkBoundVar("x", NodeManager::currentNM()->integerType()); + Node z1 = NodeManager::currentNM()->mkBoundVar("z1", NodeManager::currentNM()->stringType()); + Node z2 = NodeManager::currentNM()->mkBoundVar("z2", NodeManager::currentNM()->stringType()); + Node z3 = NodeManager::currentNM()->mkBoundVar("z3", NodeManager::currentNM()->stringType()); + Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1, z1, z2, z3); + std::vector< Node > vec_n; + Node g = NodeManager::currentNM()->mkNode(kind::GEQ, b1, d_zero); + vec_n.push_back(g); + g = NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, t[0]), b1); + vec_n.push_back(g); + g = b1.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, z1) ); + vec_n.push_back(g); + g = one.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, z2) ); + vec_n.push_back(g); + g = t[0].eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, z1, z2, z3) ); + vec_n.push_back(g); + char chtmp[2]; + chtmp[1] = '\0'; + for(unsigned i=0; i<=9; i++) { + chtmp[0] = i + '0'; + std::string stmp(chtmp); + g = z2.eqNode( NodeManager::currentNM()->mkConst(::CVC4::String(stmp)) ).negate(); + vec_n.push_back(g); + } + Node cc2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, vec_n)); + cc2 = NodeManager::currentNM()->mkNode(kind::EXISTS, b1v, cc2); + cc2 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(negone), cc2); + //cc3 + Node b2 = NodeManager::currentNM()->mkBoundVar("y", NodeManager::currentNM()->integerType()); + Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2); + Node g2 = NodeManager::currentNM()->mkNode(kind::AND, + NodeManager::currentNM()->mkNode(kind::GEQ, b2, d_zero), + NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, t[0]), b2)); + Node ufx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, b2); + Node ufx1 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, NodeManager::currentNM()->mkNode(kind::MINUS,b2,one)); + Node ufMx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, b2); + Node w1 = NodeManager::currentNM()->mkBoundVar("w1", NodeManager::currentNM()->stringType()); + Node w2 = NodeManager::currentNM()->mkBoundVar("w2", NodeManager::currentNM()->stringType()); + Node b3v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, w1, w2); + Node b2gtz = NodeManager::currentNM()->mkNode(kind::GT, b2, d_zero); + Node c3c1 = 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,b2,one)) )); + c3c1 = NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::GT, ufx, d_zero), c3c1); + c3c1 = NodeManager::currentNM()->mkNode(kind::IMPLIES, b2gtz, c3c1); + Node lstx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH,t[0]).eqNode(NodeManager::currentNM()->mkNode(kind::PLUS, b2, one)); + Node c3c2 = ufx.eqNode(ufMx); + c3c2 = NodeManager::currentNM()->mkNode(kind::IMPLIES, lstx, c3c2); + Node c3c3 = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero); + Node c3c4 = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx); + Node rev = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, w1).eqNode( + NodeManager::currentNM()->mkNode(kind::MINUS, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH,t[0]), + NodeManager::currentNM()->mkNode(kind::PLUS, b2, 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 c3c5 = t[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, w1, ch, w2)); + c3c5 = NodeManager::currentNM()->mkNode(kind::AND, rev, c3c5); + c3c5 = NodeManager::currentNM()->mkNode(kind::EXISTS, b3v, c3c5); + Node cc3 = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, c3c1, c3c2, c3c3, c3c4, c3c5) ); + cc3 = NodeManager::currentNM()->mkNode(kind::IMPLIES, g2, cc3); + cc3 = NodeManager::currentNM()->mkNode(kind::FORALL, b2v, cc3); + //conc + Node conc = NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2, cc3); + 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 +445,7 @@ 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 ); + d_cache[t] = skw; retNode = skw; } else { @@ -277,21 +477,24 @@ 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<new_nodes.size(); ++i) { - Trace("strings-preprocess") << " " << new_nodes[i]; + Trace("strings-preprocess") << "\t" << new_nodes[i] << "\n"; } - Trace("strings-preprocess") << std::endl; } return retNode; } -void StringsPreprocess::simplify(std::vector< Node > &vec_node) { - std::vector< Node > new_nodes; +void StringsPreprocess::simplify(std::vector< Node > &vec_node, std::vector< Node > &new_nodes) { for( unsigned i=0; i<vec_node.size(); i++ ){ vec_node[i] = simplify( vec_node[i], new_nodes ); } +} + +void StringsPreprocess::simplify(std::vector< Node > &vec_node) { + std::vector< Node > new_nodes; + simplify(vec_node, new_nodes); vec_node.insert( vec_node.end(), new_nodes.begin(), new_nodes.end() ); } diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index 7aa0a2af8..c2d5d656a 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -39,6 +39,7 @@ private: void simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn ); Node simplify( Node t, std::vector< Node > &new_nodes ); public: + void simplify(std::vector< Node > &vec_node, std::vector< Node > &new_nodes); void simplify(std::vector< Node > &vec_node); StringsPreprocess(); }; diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 84f58a16d..660b7aafe 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -353,7 +353,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } else if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) { int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt(); int j = node[2].getConst<Rational>().getNumerator().toUnsignedInt(); - if( node[0].getConst<String>().size() >= (unsigned) (i + j) && i>=0 && j>=0 ) { + if( i>=0 && j>=0 && node[0].getConst<String>().size() >= (unsigned) (i + j) ) { retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().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,28 @@ 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<Rational>().getNumerator().toUnsignedInt(); + std::string stmp = static_cast<std::ostringstream*>( &(std::ostringstream() << i) )->str(); + retNode = NodeManager::currentNM()->mkConst( ::CVC4::String(stmp) ); + } + } else if(node.getKind() == kind::STRING_STOI) { + if(node[0].isConst()) { + CVC4::String s = node[0].getConst<String>(); + int rt = s.toNumber(); + retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(rt)); + } else if(node[0].getKind() == kind::STRING_CONCAT) { + for(unsigned i=0; i<node[0].getNumChildren(); ++i) { + if(node[0][i].isConst()) { + CVC4::String t = node[0][i].getConst<String>(); + if(!t.isNumber()) { + retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(-1)); + break; + } + } + } + } } 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) diff --git a/src/util/regexp.h b/src/util/regexp.h index 4c69592d4..4d12803ff 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -354,6 +354,27 @@ public: ret_vec.insert( ret_vec.end(), itr, itr + j ); return String(ret_vec); } + bool isNumber() const { + for(unsigned int i=0; i<d_str.size(); ++i) { + char c = convertUnsignedIntToChar( d_str[i] ); + if(c<'0' || c>'9') { + return false; + } + } + return true; + } + int toNumber() const { + if(isNumber()) { + int ret=0; + for(unsigned int i=0; i<d_str.size(); ++i) { + char c = convertUnsignedIntToChar( d_str[i] ); + ret = ret * 10 + (int)c - (int)'0'; + } + return ret; + } else { + return -1; + } + } };/* class String */ namespace strings { |