From 12794a1a7daae3abe713e77d41bb58d59b061830 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Mon, 17 Feb 2014 19:59:03 -0600 Subject: [PATCH] add str2int --- src/smt/smt_engine.cpp | 127 +++++++++++++----- src/theory/strings/theory_strings.cpp | 3 +- .../strings/theory_strings_preprocess.cpp | 122 +++++++++++++++-- .../strings/theory_strings_rewriter.cpp | 17 ++- src/util/regexp.h | 21 +++ 5 files changed, 241 insertions(+), 49 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 08568f8da..c1aff6f4b 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -312,6 +312,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,34 +793,6 @@ 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); @@ -965,6 +943,35 @@ 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::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 if(! options::ufSymmetryBreaker.wasSetByUser()) { bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified(); @@ -1607,6 +1614,61 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_mapmkNode( kind::ITE, cond, totalf, uf ); break; } + case kind::STRING_STOI: { + if(d_ufS2I.isNull()) { + std::vector< TypeNode > argTypes; + argTypes.push_back(NodeManager::currentNM()->stringType()); + d_ufS2I = NodeManager::currentNM()->mkSkolem("__ufS2I", + NodeManager::currentNM()->mkFunctionType( + argTypes, NodeManager::currentNM()->integerType()), + "uf str2int", + NodeManager::SKOLEM_EXACT_NAME); + } + Node cond; + if(n[0].isConst()) { + CVC4::String s = n[0].getConst(); + if(s.isNumber()) { + cond = NodeManager::currentNM()->mkConst( false ); + } else { + cond = NodeManager::currentNM()->mkConst( true ); + } + } else { + Node cc1 = n[0].eqNode(nm->mkConst(::CVC4::String(""))); + Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); + Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); + 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, zero); + vec_n.push_back(g); + g = NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n[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 = n[0].eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, z1, z2, z3) ); + vec_n.push_back(g); + for(unsigned i=0; i<=9; i++) { + char ch[2]; + ch[0] = i + '0'; ch[1] = '\0'; + std::string stmp(ch); + g = z2.eqNode( nm->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); + cond = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2)); + } + Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_STOI_TOTAL, n[0]); + Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufS2I, n[0]); + node = NodeManager::currentNM()->mkNode( kind::ITE, cond, uf, totalf ); + + break; + } case kind::DIVISION: { // partial function: division if(d_divByZero.isNull()) { @@ -3123,18 +3185,11 @@ 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; - std::vector 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); - } + sp.simplify( d_assertionsToPreprocess ); 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/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index cd583c144..056cd9eb5 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -57,7 +57,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu 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_equalityEngine.addFunctionKind(kind::STRING_STOI_TOTAL); d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); @@ -408,6 +408,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { case kind::STRING_CONCAT: case kind::STRING_SUBSTR_TOTAL: case kind::STRING_ITOS: + case kind::STRING_STOI_TOTAL: d_equalityEngine.addTerm(n); break; //case kind::STRING_ITOS: diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index b2fa3dcd3..2b8aeddcc 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -249,11 +249,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node ufP = NodeManager::currentNM()->mkSkolem("ufP_$$", NodeManager::currentNM()->mkFunctionType( argTypes, NodeManager::currentNM()->integerType()), - "uf itos assist P"); + "uf type conv P"); Node ufM = NodeManager::currentNM()->mkSkolem("ufM_$$", NodeManager::currentNM()->mkFunctionType( argTypes, NodeManager::currentNM()->integerType()), - "uf itos assist M"); + "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) ); @@ -314,6 +314,114 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { 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_TOTAL ) { + if(options::stringExp()) { + 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(d_zero), 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); + for(unsigned i=0; i<=9; i++) { + char ch[2]; + ch[0] = i + '0'; ch[1] = '\0'; + std::string stmp(ch); + 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(d_zero), 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 { @@ -335,8 +443,6 @@ 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; @@ -378,15 +484,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { 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) { - 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_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 112f5eb4f..c3f63f803 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -451,8 +451,21 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { retNode = NodeManager::currentNM()->mkConst( ::CVC4::String(stmp) ); } } else if(node.getKind() == kind::STRING_STOI_TOTAL) { - //TODO - Assert(false, "stoi not supported."); + if(node[0].isConst()) { + CVC4::String s = node[0].getConst(); + int rt = s.toNumber(); + retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(rt)); + } else if(node[0].getKind() == kind::STRING_CONCAT) { + for(unsigned i=0; i(); + if(!t.isNumber()) { + retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(0)); + break; + } + } + } + } } else if(node.getKind() == kind::STRING_IN_REGEXP) { retNode = rewriteMembership(node); } diff --git a/src/util/regexp.h b/src/util/regexp.h index 4c69592d4..4891998e5 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'9') { + return false; + } + } + return true; + } + int toNumber() const { + if(isNumber()) { + int ret=0; + for(unsigned int i=0; i