diff options
19 files changed, 1122 insertions, 750 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 7e31d1494..c35a14800 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -679,18 +679,20 @@ libcvc4_add_sources( theory/strings/regexp_operation.h theory/strings/regexp_solver.cpp theory/strings/regexp_solver.h + theory/strings/sequences_rewriter.cpp + theory/strings/sequences_rewriter.h theory/strings/skolem_cache.cpp theory/strings/skolem_cache.h theory/strings/solver_state.cpp theory/strings/solver_state.h theory/strings/strings_fmf.cpp theory/strings/strings_fmf.h + theory/strings/strings_rewriter.cpp + theory/strings/strings_rewriter.h theory/strings/theory_strings.cpp theory/strings/theory_strings.h theory/strings/theory_strings_preprocess.cpp theory/strings/theory_strings_preprocess.h - theory/strings/theory_strings_rewriter.cpp - theory/strings/theory_strings_rewriter.h theory/strings/theory_strings_type_rules.h theory/strings/theory_strings_utils.cpp theory/strings/theory_strings_utils.h diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index 44d3666e8..7920ecbeb 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -20,7 +20,7 @@ #include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -#include "theory/strings/theory_strings_rewriter.h" +#include "theory/strings/sequences_rewriter.h" using namespace CVC4::kind; using namespace std; @@ -1692,7 +1692,7 @@ Node ExtendedRewriter::extendedRewriteStrings(Node ret) if (ret.getKind() == EQUAL) { - new_ret = strings::TheoryStringsRewriter::rewriteEqualityExt(ret); + new_ret = strings::SequencesRewriter::rewriteEqualityExt(ret); } return new_ret; diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index c23041914..6958d2528 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -16,7 +16,6 @@ #include "theory/strings/base_solver.h" #include "options/strings_options.h" -#include "theory/strings/theory_strings_rewriter.h" #include "theory/strings/theory_strings_utils.h" using namespace std; diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index 723a8c08e..2a95b41ba 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -17,7 +17,7 @@ #include "theory/strings/core_solver.h" #include "options/strings_options.h" -#include "theory/strings/theory_strings_rewriter.h" +#include "theory/strings/sequences_rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" @@ -155,7 +155,7 @@ void CoreSolver::checkFlatForms() for (const Node& n : it->second) { int firstc, lastc; - if (!TheoryStringsRewriter::canConstantContainList( + if (!SequencesRewriter::canConstantContainList( c, d_flat_form[n], firstc, lastc)) { Trace("strings-ff-debug") << "Flat form for " << n @@ -348,8 +348,8 @@ void CoreSolver::checkFlatForm(std::vector<Node>& eqc, { // check for constant conflict int index; - Node s = TheoryStringsRewriter::splitConstant( - cc_c, curr_c, index, isRev); + Node s = + SequencesRewriter::splitConstant(cc_c, curr_c, index, isRev); if (s.isNull()) { d_bsolver.explainConstantEqc(ac,curr,exp); @@ -905,7 +905,7 @@ void CoreSolver::getNormalForms(Node eqc, { NormalForm& nf = normal_forms[i]; int firstc, lastc; - if (!TheoryStringsRewriter::canConstantContainList( + if (!SequencesRewriter::canConstantContainList( c, nf.d_nf, firstc, lastc)) { Node n = nf.d_base; @@ -1910,7 +1910,7 @@ int CoreSolver::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& if (!c.isNull()) { int findex, lindex; - if (!TheoryStringsRewriter::canConstantContainList( + if (!SequencesRewriter::canConstantContainList( c, i == 0 ? nfj : nfi, findex, lindex)) { Trace("strings-solve-debug") diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index af114e361..c586df6dd 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -15,8 +15,8 @@ #include "theory/strings/extf_solver.h" #include "options/strings_options.h" +#include "theory/strings/sequences_rewriter.h" #include "theory/strings/theory_strings_preprocess.h" -#include "theory/strings/theory_strings_rewriter.h" #include "theory/strings/theory_strings_utils.h" using namespace std; @@ -617,7 +617,7 @@ void ExtfSolver::checkExtfInference(Node n, if (inferEqr.getKind() == EQUAL) { // try to use the extended rewriter for equalities - inferEqrr = TheoryStringsRewriter::rewriteEqualityExt(inferEqr); + inferEqrr = SequencesRewriter::rewriteEqualityExt(inferEqr); } if (inferEqrr != inferEqr) { diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 67ba2d5a3..389c4e7bf 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -19,7 +19,6 @@ #include "theory/ext_theory.h" #include "theory/rewriter.h" #include "theory/strings/theory_strings.h" -#include "theory/strings/theory_strings_rewriter.h" #include "theory/strings/theory_strings_utils.h" using namespace std; diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 6c7846737..5b988061b 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -8,7 +8,7 @@ theory THEORY_STRINGS ::CVC4::theory::strings::TheoryStrings "theory/strings/the properties check parametric propagate presolve -rewriter ::CVC4::theory::strings::TheoryStringsRewriter "theory/strings/theory_strings_rewriter.h" +rewriter ::CVC4::theory::strings::SequencesRewriter "theory/strings/sequences_rewriter.h" typechecker "theory/strings/theory_strings_type_rules.h" diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index 86995736e..976efad3c 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -17,7 +17,7 @@ #include "options/strings_options.h" #include "theory/rewriter.h" -#include "theory/strings/theory_strings_rewriter.h" +#include "theory/strings/sequences_rewriter.h" #include "theory/strings/theory_strings_utils.h" using namespace CVC4; @@ -70,7 +70,7 @@ Node RegExpElimination::eliminateConcat(Node atom) for (unsigned i = 0, size = children.size(); i < size; i++) { Node c = children[i]; - Node fl = TheoryStringsRewriter::getFixedLengthForRegexp(c); + Node fl = SequencesRewriter::getFixedLengthForRegexp(c); if (fl.isNull()) { if (!hasPivotIndex && c.getKind() == REGEXP_STAR diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index f91b59834..d5105a489 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -18,7 +18,7 @@ #include "expr/kind.h" #include "options/strings_options.h" -#include "theory/strings/theory_strings_rewriter.h" +#include "theory/strings/sequences_rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" @@ -920,12 +920,12 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes // all strings in the language of R1 have the same length, say n, // then the conclusion of the reduction is quantifier-free: // ~( substr(s,0,n) in R1 ) OR ~( substr(s,n,len(s)-n) in R2) - Node reLength = TheoryStringsRewriter::getFixedLengthForRegexp(r[0]); + Node reLength = SequencesRewriter::getFixedLengthForRegexp(r[0]); if (reLength.isNull()) { // try from the opposite end unsigned indexE = r.getNumChildren() - 1; - reLength = TheoryStringsRewriter::getFixedLengthForRegexp(r[indexE]); + reLength = SequencesRewriter::getFixedLengthForRegexp(r[indexE]); if (!reLength.isNull()) { indexRm = indexE; diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 9d9c66ec2..cd66c0ebf 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -21,7 +21,6 @@ #include "options/strings_options.h" #include "theory/ext_theory.h" #include "theory/strings/theory_strings.h" -#include "theory/strings/theory_strings_rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/theory_model.h" diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 95f537878..f4a1cd411 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file theory_strings_rewriter.cpp +/*! \file sequences_rewriter.cpp ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds, Andres Noetzli, Tianyi Liang @@ -14,7 +14,7 @@ ** Implementation of the theory of strings. **/ -#include "theory/strings/theory_strings_rewriter.h" +#include "theory/strings/sequences_rewriter.h" #include <stdint.h> #include <algorithm> @@ -24,6 +24,7 @@ #include "smt/logic_exception.h" #include "theory/arith/arith_msum.h" #include "theory/strings/regexp_operation.h" +#include "theory/strings/strings_rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" #include "theory/theory.h" @@ -36,55 +37,75 @@ using namespace CVC4::kind; using namespace CVC4::theory; using namespace CVC4::theory::strings; -Node TheoryStringsRewriter::simpleRegexpConsume( std::vector< Node >& mchildren, std::vector< Node >& children, int dir ){ +Node SequencesRewriter::simpleRegexpConsume(std::vector<Node>& mchildren, + std::vector<Node>& children, + int dir) +{ Trace("regexp-ext-rewrite-debug") << "Simple reg exp consume, dir=" << dir << ":" << std::endl; Trace("regexp-ext-rewrite-debug") << " mchildren : " << mchildren << std::endl; Trace("regexp-ext-rewrite-debug") << " children : " << children << std::endl; NodeManager* nm = NodeManager::currentNM(); - unsigned tmin = dir<0 ? 0 : dir; - unsigned tmax = dir<0 ? 1 : dir; - //try to remove off front and back - for( unsigned t=0; t<2; t++ ){ - if( tmin<=t && t<=tmax ){ + unsigned tmin = dir < 0 ? 0 : dir; + unsigned tmax = dir < 0 ? 1 : dir; + // try to remove off front and back + for (unsigned t = 0; t < 2; t++) + { + if (tmin <= t && t <= tmax) + { bool do_next = true; - while( !children.empty() && !mchildren.empty() && do_next ){ + while (!children.empty() && !mchildren.empty() && do_next) + { do_next = false; - Node xc = mchildren[mchildren.size()-1]; - Node rc = children[children.size()-1]; + Node xc = mchildren[mchildren.size() - 1]; + Node rc = children[children.size() - 1]; Assert(rc.getKind() != kind::REGEXP_CONCAT); Assert(xc.getKind() != kind::STRING_CONCAT); - if( rc.getKind() == kind::STRING_TO_REGEXP ){ - if( xc==rc[0] ){ + if (rc.getKind() == kind::STRING_TO_REGEXP) + { + if (xc == rc[0]) + { children.pop_back(); mchildren.pop_back(); do_next = true; Trace("regexp-ext-rewrite-debug") << "...strip equal" << std::endl; - }else if( xc.isConst() && rc[0].isConst() ){ - //split the constant + } + else if (xc.isConst() && rc[0].isConst()) + { + // split the constant int index; - Node s = splitConstant( xc, rc[0], index, t==0 ); - Trace("regexp-ext-rewrite-debug") << "CRE: Regexp const split : " << xc << " " << rc[0] << " -> " << s << " " << index << " " << t << std::endl; - if( s.isNull() ){ + Node s = splitConstant(xc, rc[0], index, t == 0); + Trace("regexp-ext-rewrite-debug") + << "CRE: Regexp const split : " << xc << " " << rc[0] << " -> " + << s << " " << index << " " << t << std::endl; + if (s.isNull()) + { Trace("regexp-ext-rewrite-debug") << "...return false" << std::endl; - return NodeManager::currentNM()->mkConst( false ); - }else{ + return NodeManager::currentNM()->mkConst(false); + } + else + { Trace("regexp-ext-rewrite-debug") << "...strip equal const" << std::endl; children.pop_back(); mchildren.pop_back(); - if( index==0 ){ - mchildren.push_back( s ); - }else{ + if (index == 0) + { + mchildren.push_back(s); + } + else + { children.push_back(nm->mkNode(STRING_TO_REGEXP, s)); } } do_next = true; } - }else if( xc.isConst() ){ - //check for constants + } + else if (xc.isConst()) + { + // check for constants CVC4::String s = xc.getConst<String>(); if (Word::isEmpty(xc)) { @@ -99,101 +120,145 @@ Node TheoryStringsRewriter::simpleRegexpConsume( std::vector< Node >& mchildren, std::vector<unsigned> ssVec; ssVec.push_back(t == 0 ? s.back() : s.front()); CVC4::String ss(ssVec); - if( testConstStringInRegExp( ss, 0, rc ) ){ - //strip off one character + if (testConstStringInRegExp(ss, 0, rc)) + { + // strip off one character mchildren.pop_back(); - if( s.size()>1 ){ - if( t==0 ){ - mchildren.push_back( NodeManager::currentNM()->mkConst(s.substr( 0, s.size()-1 )) ); - }else{ - mchildren.push_back( NodeManager::currentNM()->mkConst(s.substr( 1 )) ); + if (s.size() > 1) + { + if (t == 0) + { + mchildren.push_back(NodeManager::currentNM()->mkConst( + s.substr(0, s.size() - 1))); + } + else + { + mchildren.push_back( + NodeManager::currentNM()->mkConst(s.substr(1))); } } children.pop_back(); do_next = true; - }else{ - return NodeManager::currentNM()->mkConst( false ); } - }else if( rc.getKind()==kind::REGEXP_INTER || rc.getKind()==kind::REGEXP_UNION ){ - //see if any/each child does not work + else + { + return NodeManager::currentNM()->mkConst(false); + } + } + else if (rc.getKind() == kind::REGEXP_INTER + || rc.getKind() == kind::REGEXP_UNION) + { + // see if any/each child does not work bool result_valid = true; Node result; - Node emp_s = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); - for( unsigned i=0; i<rc.getNumChildren(); i++ ){ - std::vector< Node > mchildren_s; - std::vector< Node > children_s; - mchildren_s.push_back( xc ); + Node emp_s = NodeManager::currentNM()->mkConst(::CVC4::String("")); + for (unsigned i = 0; i < rc.getNumChildren(); i++) + { + std::vector<Node> mchildren_s; + std::vector<Node> children_s; + mchildren_s.push_back(xc); utils::getConcat(rc[i], children_s); - Node ret = simpleRegexpConsume( mchildren_s, children_s, t ); - if( !ret.isNull() ){ + Node ret = simpleRegexpConsume(mchildren_s, children_s, t); + if (!ret.isNull()) + { // one conjunct cannot be satisfied, return false - if( rc.getKind()==kind::REGEXP_INTER ){ + if (rc.getKind() == kind::REGEXP_INTER) + { return ret; } - }else{ - if( children_s.empty() ){ - //if we were able to fully consume, store the result + } + else + { + if (children_s.empty()) + { + // if we were able to fully consume, store the result Assert(mchildren_s.size() <= 1); - if( mchildren_s.empty() ){ - mchildren_s.push_back( emp_s ); + if (mchildren_s.empty()) + { + mchildren_s.push_back(emp_s); } - if( result.isNull() ){ + if (result.isNull()) + { result = mchildren_s[0]; - }else if( result!=mchildren_s[0] ){ + } + else if (result != mchildren_s[0]) + { result_valid = false; } - }else{ + } + else + { result_valid = false; } } } - if( result_valid ){ - if( result.isNull() ){ - //all disjuncts cannot be satisfied, return false + if (result_valid) + { + if (result.isNull()) + { + // all disjuncts cannot be satisfied, return false Assert(rc.getKind() == kind::REGEXP_UNION); - return NodeManager::currentNM()->mkConst( false ); - }else{ - //all branches led to the same result + return NodeManager::currentNM()->mkConst(false); + } + else + { + // all branches led to the same result children.pop_back(); mchildren.pop_back(); - if( result!=emp_s ){ - mchildren.push_back( result ); + if (result != emp_s) + { + mchildren.push_back(result); } do_next = true; } } - }else if( rc.getKind()==kind::REGEXP_STAR ){ - //check if there is no way that this star can be unrolled even once - std::vector< Node > mchildren_s; - mchildren_s.insert( mchildren_s.end(), mchildren.begin(), mchildren.end() ); - if( t==1 ){ - std::reverse( mchildren_s.begin(), mchildren_s.end() ); + } + else if (rc.getKind() == kind::REGEXP_STAR) + { + // check if there is no way that this star can be unrolled even once + std::vector<Node> mchildren_s; + mchildren_s.insert( + mchildren_s.end(), mchildren.begin(), mchildren.end()); + if (t == 1) + { + std::reverse(mchildren_s.begin(), mchildren_s.end()); } - std::vector< Node > children_s; + std::vector<Node> children_s; utils::getConcat(rc[0], children_s); Trace("regexp-ext-rewrite-debug") << "...recursive call on body of star" << std::endl; - Node ret = simpleRegexpConsume( mchildren_s, children_s, t ); - if( !ret.isNull() ){ - Trace("regexp-ext-rewrite-debug") << "CRE : regexp star infeasable " << xc << " " << rc << std::endl; + Node ret = simpleRegexpConsume(mchildren_s, children_s, t); + if (!ret.isNull()) + { + Trace("regexp-ext-rewrite-debug") + << "CRE : regexp star infeasable " << xc << " " << rc + << std::endl; children.pop_back(); if (!children.empty()) { Trace("regexp-ext-rewrite-debug") << "...continue" << std::endl; do_next = true; } - }else{ - if( children_s.empty() ){ - //check if beyond this, we can't do it or there is nothing left, if so, repeat + } + else + { + if (children_s.empty()) + { + // check if beyond this, we can't do it or there is nothing + // left, if so, repeat bool can_skip = false; - if( children.size()>1 ){ - std::vector< Node > mchildren_ss; - mchildren_ss.insert( mchildren_ss.end(), mchildren.begin(), mchildren.end() ); - std::vector< Node > children_ss; - children_ss.insert( children_ss.end(), children.begin(), children.end()-1 ); - if( t==1 ){ - std::reverse( mchildren_ss.begin(), mchildren_ss.end() ); - std::reverse( children_ss.begin(), children_ss.end() ); + if (children.size() > 1) + { + std::vector<Node> mchildren_ss; + mchildren_ss.insert( + mchildren_ss.end(), mchildren.begin(), mchildren.end()); + std::vector<Node> children_ss; + children_ss.insert( + children_ss.end(), children.begin(), children.end() - 1); + if (t == 1) + { + std::reverse(mchildren_ss.begin(), mchildren_ss.end()); + std::reverse(children_ss.begin(), children_ss.end()); } if (simpleRegexpConsume(mchildren_ss, children_ss, t) .isNull()) @@ -201,17 +266,22 @@ Node TheoryStringsRewriter::simpleRegexpConsume( std::vector< Node >& mchildren, can_skip = true; } } - if( !can_skip ){ + if (!can_skip) + { Trace("regexp-ext-rewrite-debug") << "...can't skip" << std::endl; - //take the result of fully consuming once - if( t==1 ){ - std::reverse( mchildren_s.begin(), mchildren_s.end() ); + // take the result of fully consuming once + if (t == 1) + { + std::reverse(mchildren_s.begin(), mchildren_s.end()); } mchildren.clear(); - mchildren.insert( mchildren.end(), mchildren_s.begin(), mchildren_s.end() ); + mchildren.insert( + mchildren.end(), mchildren_s.begin(), mchildren_s.end()); do_next = true; - }else{ + } + else + { Trace("regexp-ext-rewrite-debug") << "...can skip " << rc << " from " << xc << std::endl; } @@ -219,20 +289,23 @@ Node TheoryStringsRewriter::simpleRegexpConsume( std::vector< Node >& mchildren, } } } - if( !do_next ){ - Trace("regexp-ext-rewrite") << "Cannot consume : " << xc << " " << rc << std::endl; + if (!do_next) + { + Trace("regexp-ext-rewrite") + << "Cannot consume : " << xc << " " << rc << std::endl; } } } - if( dir!=0 ){ - std::reverse( children.begin(), children.end() ); - std::reverse( mchildren.begin(), mchildren.end() ); + if (dir != 0) + { + std::reverse(children.begin(), children.end()); + std::reverse(mchildren.begin(), mchildren.end()); } } return Node::null(); } -Node TheoryStringsRewriter::rewriteEquality(Node node) +Node SequencesRewriter::rewriteEquality(Node node) { Assert(node.getKind() == kind::EQUAL); if (node[0] == node[1]) @@ -320,7 +393,7 @@ Node TheoryStringsRewriter::rewriteEquality(Node node) return node; } -Node TheoryStringsRewriter::rewriteEqualityExt(Node node) +Node SequencesRewriter::rewriteEqualityExt(Node node) { Assert(node.getKind() == EQUAL); if (node[0].getType().isInteger()) @@ -334,7 +407,7 @@ Node TheoryStringsRewriter::rewriteEqualityExt(Node node) return node; } -Node TheoryStringsRewriter::rewriteStrEqualityExt(Node node) +Node SequencesRewriter::rewriteStrEqualityExt(Node node) { Assert(node.getKind() == EQUAL && node[0].getType().isString()); @@ -708,7 +781,7 @@ Node TheoryStringsRewriter::rewriteStrEqualityExt(Node node) return node; } -Node TheoryStringsRewriter::rewriteArithEqualityExt(Node node) +Node SequencesRewriter::rewriteArithEqualityExt(Node node) { Assert(node.getKind() == EQUAL && node[0].getType().isInteger()); @@ -722,7 +795,7 @@ Node TheoryStringsRewriter::rewriteArithEqualityExt(Node node) // TODO (#1180) add rewrite // str.++( str.substr( x, n1, n2 ), str.substr( x, n1+n2, n3 ) ) ---> // str.substr( x, n1, n2+n3 ) -Node TheoryStringsRewriter::rewriteConcat(Node node) +Node SequencesRewriter::rewriteConcat(Node node) { Assert(node.getKind() == kind::STRING_CONCAT); Trace("strings-rewrite-debug") @@ -761,19 +834,26 @@ Node TheoryStringsRewriter::rewriteConcat(Node node) // take the last term as the current tmpNode = tmpNode[tmpNode.getNumChildren() - 1]; } - if(!tmpNode.isConst()) { - if(!preNode.isNull()) { + if (!tmpNode.isConst()) + { + if (!preNode.isNull()) + { if (preNode.isConst() && !Word::isEmpty(preNode)) { - node_vec.push_back( preNode ); + node_vec.push_back(preNode); } preNode = Node::null(); } - node_vec.push_back( tmpNode ); - }else{ - if( preNode.isNull() ){ + node_vec.push_back(tmpNode); + } + else + { + if (preNode.isNull()) + { preNode = tmpNode; - }else{ + } + else + { std::vector<Node> vec; vec.push_back(preNode); vec.push_back(tmpNode); @@ -783,7 +863,7 @@ Node TheoryStringsRewriter::rewriteConcat(Node node) } if (!preNode.isNull() && (!preNode.isConst() || !Word::isEmpty(preNode))) { - node_vec.push_back( preNode ); + node_vec.push_back(preNode); } // Sort adjacent operands in str.++ that all result in the same string or the @@ -817,7 +897,7 @@ Node TheoryStringsRewriter::rewriteConcat(Node node) return retNode; } -Node TheoryStringsRewriter::rewriteConcatRegExp(TNode node) +Node SequencesRewriter::rewriteConcatRegExp(TNode node) { Assert(node.getKind() == kind::REGEXP_CONCAT); NodeManager* nm = NodeManager::currentNM(); @@ -957,7 +1037,7 @@ Node TheoryStringsRewriter::rewriteConcatRegExp(TNode node) if (cvec[i].getKind() == REGEXP_STAR && cvec[i][0] == cvec[i + 1]) { // by convention, flip the order (a*)++a ---> a++(a*) - std::swap(cvec[i], cvec[i+1]); + std::swap(cvec[i], cvec[i + 1]); changed = true; } } @@ -969,7 +1049,7 @@ Node TheoryStringsRewriter::rewriteConcatRegExp(TNode node) return node; } -Node TheoryStringsRewriter::rewriteStarRegExp(TNode node) +Node SequencesRewriter::rewriteStarRegExp(TNode node) { Assert(node.getKind() == REGEXP_STAR); NodeManager* nm = NodeManager::currentNM(); @@ -1025,7 +1105,7 @@ Node TheoryStringsRewriter::rewriteStarRegExp(TNode node) return node; } -Node TheoryStringsRewriter::rewriteAndOrRegExp(TNode node) +Node SequencesRewriter::rewriteAndOrRegExp(TNode node) { Kind nk = node.getKind(); Assert(nk == REGEXP_UNION || nk == REGEXP_INTER); @@ -1091,7 +1171,7 @@ Node TheoryStringsRewriter::rewriteAndOrRegExp(TNode node) return node; } -Node TheoryStringsRewriter::rewriteLoopRegExp(TNode node) +Node SequencesRewriter::rewriteLoopRegExp(TNode node) { Assert(node.getKind() == REGEXP_LOOP); Node retNode = node; @@ -1164,16 +1244,22 @@ Node TheoryStringsRewriter::rewriteLoopRegExp(TNode node) return node; } -bool TheoryStringsRewriter::isConstRegExp( TNode t ) { - if( t.getKind()==kind::STRING_TO_REGEXP ) { +bool SequencesRewriter::isConstRegExp(TNode t) +{ + if (t.getKind() == kind::STRING_TO_REGEXP) + { return t[0].isConst(); } else if (t.isVar()) { return false; - }else{ - for( unsigned i = 0; i<t.getNumChildren(); ++i ) { - if( !isConstRegExp(t[i]) ){ + } + else + { + for (unsigned i = 0; i < t.getNumChildren(); ++i) + { + if (!isConstRegExp(t[i])) + { return false; } } @@ -1181,17 +1267,23 @@ bool TheoryStringsRewriter::isConstRegExp( TNode t ) { } } -bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned int index_start, TNode r ) { +bool SequencesRewriter::testConstStringInRegExp(CVC4::String& s, + unsigned int index_start, + TNode r) +{ Assert(index_start <= s.size()); - Trace("regexp-debug") << "Checking " << s << " in " << r << ", starting at " << index_start << std::endl; + Trace("regexp-debug") << "Checking " << s << " in " << r << ", starting at " + << index_start << std::endl; Assert(!r.isVar()); Kind k = r.getKind(); - switch( k ) { - case kind::STRING_TO_REGEXP: { - CVC4::String s2 = s.substr( index_start, s.size() - index_start ); + switch (k) + { + case kind::STRING_TO_REGEXP: + { + CVC4::String s2 = s.substr(index_start, s.size() - index_start); if (r[0].isConst()) { - return ( s2 == r[0].getConst<String>() ); + return (s2 == r[0].getConst<String>()); } else { @@ -1199,64 +1291,91 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i return false; } } - case kind::REGEXP_CONCAT: { - if( s.size() != index_start ) { - std::vector<int> vec_k( r.getNumChildren(), -1 ); + case kind::REGEXP_CONCAT: + { + if (s.size() != index_start) + { + std::vector<int> vec_k(r.getNumChildren(), -1); int start = 0; - int left = (int) s.size() - index_start; - int i=0; - while( i<(int) r.getNumChildren() ) { + int left = (int)s.size() - index_start; + int i = 0; + while (i < (int)r.getNumChildren()) + { bool flag = true; - if( i == (int) r.getNumChildren() - 1 ) { - if( testConstStringInRegExp( s, index_start + start, r[i] ) ) { + if (i == (int)r.getNumChildren() - 1) + { + if (testConstStringInRegExp(s, index_start + start, r[i])) + { return true; } - } else if( i == -1 ) { + } + else if (i == -1) + { return false; - } else { - for(vec_k[i] = vec_k[i] + 1; vec_k[i] <= left; ++vec_k[i]) { + } + else + { + for (vec_k[i] = vec_k[i] + 1; vec_k[i] <= left; ++vec_k[i]) + { CVC4::String t = s.substr(index_start + start, vec_k[i]); - if( testConstStringInRegExp( t, 0, r[i] ) ) { - start += vec_k[i]; left -= vec_k[i]; flag = false; - ++i; vec_k[i] = -1; + if (testConstStringInRegExp(t, 0, r[i])) + { + start += vec_k[i]; + left -= vec_k[i]; + flag = false; + ++i; + vec_k[i] = -1; break; } } } - if(flag) { + if (flag) + { --i; - if(i >= 0) { - start -= vec_k[i]; left += vec_k[i]; + if (i >= 0) + { + start -= vec_k[i]; + left += vec_k[i]; } } } return false; - } else { - for(unsigned i=0; i<r.getNumChildren(); ++i) { - if(!testConstStringInRegExp( s, index_start, r[i] )) return false; + } + else + { + for (unsigned i = 0; i < r.getNumChildren(); ++i) + { + if (!testConstStringInRegExp(s, index_start, r[i])) return false; } return true; } } - case kind::REGEXP_UNION: { - for(unsigned i=0; i<r.getNumChildren(); ++i) { - if(testConstStringInRegExp( s, index_start, r[i] )) return true; + case kind::REGEXP_UNION: + { + for (unsigned i = 0; i < r.getNumChildren(); ++i) + { + if (testConstStringInRegExp(s, index_start, r[i])) return true; } return false; } - case kind::REGEXP_INTER: { - for(unsigned i=0; i<r.getNumChildren(); ++i) { - if(!testConstStringInRegExp( s, index_start, r[i] )) return false; + case kind::REGEXP_INTER: + { + for (unsigned i = 0; i < r.getNumChildren(); ++i) + { + if (!testConstStringInRegExp(s, index_start, r[i])) return false; } return true; } - case kind::REGEXP_STAR: { - if( s.size() != index_start ) { + case kind::REGEXP_STAR: + { + if (s.size() != index_start) + { for (unsigned i = s.size() - index_start; i > 0; --i) { CVC4::String t = s.substr(index_start, i); - if( testConstStringInRegExp( t, 0, r[0] ) ) { + if (testConstStringInRegExp(t, 0, r[0])) + { if (index_start + i == s.size() || testConstStringInRegExp(s, index_start + i, r)) { @@ -1265,22 +1384,29 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i } } return false; - } else { + } + else + { return true; } } - case kind::REGEXP_EMPTY: { - return false; + case kind::REGEXP_EMPTY: { return false; } - case kind::REGEXP_SIGMA: { - if(s.size() == index_start + 1) { + case kind::REGEXP_SIGMA: + { + if (s.size() == index_start + 1) + { return true; - } else { + } + else + { return false; } } - case kind::REGEXP_RANGE: { - if(s.size() == index_start + 1) { + case kind::REGEXP_RANGE: + { + if (s.size() == index_start + 1) + { unsigned a = r[0].getConst<String>().front(); a = String::convertUnsignedIntToCode(a); unsigned b = r[1].getConst<String>().front(); @@ -1288,54 +1414,82 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i unsigned c = s.back(); c = String::convertUnsignedIntToCode(c); return (a <= c && c <= b); - } else { + } + else + { return false; } } - case kind::REGEXP_LOOP: { + case kind::REGEXP_LOOP: + { uint32_t l = r[1].getConst<Rational>().getNumerator().toUnsignedInt(); - if(s.size() == index_start) { - return l==0? true : testConstStringInRegExp(s, index_start, r[0]); - } else if(l==0 && r[1]==r[2]) { + if (s.size() == index_start) + { + return l == 0 ? true : testConstStringInRegExp(s, index_start, r[0]); + } + else if (l == 0 && r[1] == r[2]) + { return false; - } else { + } + else + { Assert(r.getNumChildren() == 3) << "String rewriter error: LOOP has 2 children"; - if(l==0) { - //R{0,u} + if (l == 0) + { + // R{0,u} uint32_t u = r[2].getConst<Rational>().getNumerator().toUnsignedInt(); - for(unsigned len=s.size() - index_start; len>=1; len--) { + for (unsigned len = s.size() - index_start; len >= 1; len--) + { CVC4::String t = s.substr(index_start, len); - if(testConstStringInRegExp(t, 0, r[0])) { - if(len + index_start == s.size()) { + if (testConstStringInRegExp(t, 0, r[0])) + { + if (len + index_start == s.size()) + { return true; - } else { - Node num2 = NodeManager::currentNM()->mkConst( CVC4::Rational(u - 1) ); - Node r2 = NodeManager::currentNM()->mkNode(kind::REGEXP_LOOP, r[0], r[1], num2); - if(testConstStringInRegExp(s, index_start+len, r2)) { + } + else + { + Node num2 = + NodeManager::currentNM()->mkConst(CVC4::Rational(u - 1)); + Node r2 = NodeManager::currentNM()->mkNode( + kind::REGEXP_LOOP, r[0], r[1], num2); + if (testConstStringInRegExp(s, index_start + len, r2)) + { return true; } } } } return false; - } else { - //R{l,l} + } + else + { + // R{l,l} Assert(r[1] == r[2]) << "String rewriter error: LOOP nums are not equal"; - if(l>s.size() - index_start) { - if(testConstStringInRegExp(s, s.size(), r[0])) { + if (l > s.size() - index_start) + { + if (testConstStringInRegExp(s, s.size(), r[0])) + { l = s.size() - index_start; - } else { + } + else + { return false; } } - for(unsigned len=1; len<=s.size() - index_start; len++) { + for (unsigned len = 1; len <= s.size() - index_start; len++) + { CVC4::String t = s.substr(index_start, len); - if(testConstStringInRegExp(t, 0, r[0])) { - Node num2 = NodeManager::currentNM()->mkConst( CVC4::Rational(l - 1) ); - Node r2 = NodeManager::currentNM()->mkNode(kind::REGEXP_LOOP, r[0], num2, num2); - if(testConstStringInRegExp(s, index_start+len, r2)) { + if (testConstStringInRegExp(t, 0, r[0])) + { + Node num2 = + NodeManager::currentNM()->mkConst(CVC4::Rational(l - 1)); + Node r2 = NodeManager::currentNM()->mkNode( + kind::REGEXP_LOOP, r[0], num2, num2); + if (testConstStringInRegExp(s, index_start + len, r2)) + { return true; } } @@ -1349,27 +1503,31 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i return !testConstStringInRegExp(s, index_start, r[0]); break; } - default: { + default: + { Assert(!RegExpOpr::isRegExpKind(k)); return false; } } } -Node TheoryStringsRewriter::rewriteMembership(TNode node) { +Node SequencesRewriter::rewriteMembership(TNode node) +{ NodeManager* nm = NodeManager::currentNM(); Node retNode = node; Node x = node[0]; Node r = node[1]; - if(r.getKind() == kind::REGEXP_EMPTY) { - retNode = NodeManager::currentNM()->mkConst( false ); + if (r.getKind() == kind::REGEXP_EMPTY) + { + retNode = NodeManager::currentNM()->mkConst(false); } else if (x.isConst() && isConstRegExp(r)) { - //test whether x in node[1] + // test whether x in node[1] CVC4::String s = x.getConst<String>(); - retNode = NodeManager::currentNM()->mkConst( testConstStringInRegExp( s, 0, r ) ); + retNode = + NodeManager::currentNM()->mkConst(testConstStringInRegExp(s, 0, r)); } else if (r.getKind() == kind::REGEXP_SIGMA) { @@ -1420,7 +1578,7 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { } if (r[0].getKind() == kind::REGEXP_SIGMA) { - retNode = NodeManager::currentNM()->mkConst( true ); + retNode = NodeManager::currentNM()->mkConst(true); return returnRewrite(node, retNode, "re-in-sigma-star"); } } @@ -1485,11 +1643,14 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { else if (r.getKind() == kind::REGEXP_INTER || r.getKind() == kind::REGEXP_UNION) { - std::vector< Node > mvec; - for( unsigned i=0; i<r.getNumChildren(); i++ ){ - mvec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, r[i] ) ); + std::vector<Node> mvec; + for (unsigned i = 0; i < r.getNumChildren(); i++) + { + mvec.push_back( + NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r[i])); } - retNode = NodeManager::currentNM()->mkNode( r.getKind()==kind::REGEXP_INTER ? kind::AND : kind::OR, mvec ); + retNode = NodeManager::currentNM()->mkNode( + r.getKind() == kind::REGEXP_INTER ? kind::AND : kind::OR, mvec); } else if (r.getKind() == kind::STRING_TO_REGEXP) { @@ -1510,30 +1671,42 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { } else if (x != node[0] || r != node[1]) { - retNode = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, r ); + retNode = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r); } - //do simple consumes - if( retNode==node ){ - if( r.getKind()==kind::REGEXP_STAR ){ - for( unsigned dir=0; dir<=1; dir++ ){ - std::vector< Node > mchildren; + // do simple consumes + if (retNode == node) + { + if (r.getKind() == kind::REGEXP_STAR) + { + for (unsigned dir = 0; dir <= 1; dir++) + { + std::vector<Node> mchildren; utils::getConcat(x, mchildren); bool success = true; - while( success ){ + while (success) + { success = false; - std::vector< Node > children; + std::vector<Node> children; utils::getConcat(r[0], children); - Node scn = simpleRegexpConsume( mchildren, children, dir ); - if( !scn.isNull() ){ - Trace("regexp-ext-rewrite") << "Regexp star : const conflict : " << node << std::endl; + Node scn = simpleRegexpConsume(mchildren, children, dir); + if (!scn.isNull()) + { + Trace("regexp-ext-rewrite") + << "Regexp star : const conflict : " << node << std::endl; return scn; - }else if( children.empty() ){ - //fully consumed one copy of the STAR - if( mchildren.empty() ){ - Trace("regexp-ext-rewrite") << "Regexp star : full consume : " << node << std::endl; - return NodeManager::currentNM()->mkConst( true ); - }else{ + } + else if (children.empty()) + { + // fully consumed one copy of the STAR + if (mchildren.empty()) + { + Trace("regexp-ext-rewrite") + << "Regexp star : full consume : " << node << std::endl; + return NodeManager::currentNM()->mkConst(true); + } + else + { retNode = nm->mkNode(STRING_IN_REGEXP, utils::mkConcat(STRING_CONCAT, mchildren), r); @@ -1541,39 +1714,52 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { } } } - if( retNode!=node ){ - Trace("regexp-ext-rewrite") << "Regexp star : rewrite " << node << " -> " << retNode << std::endl; + if (retNode != node) + { + Trace("regexp-ext-rewrite") << "Regexp star : rewrite " << node + << " -> " << retNode << std::endl; break; } } - }else{ - std::vector< Node > children; + } + else + { + std::vector<Node> children; utils::getConcat(r, children); - std::vector< Node > mchildren; + std::vector<Node> mchildren; utils::getConcat(x, mchildren); unsigned prevSize = children.size() + mchildren.size(); - Node scn = simpleRegexpConsume( mchildren, children ); - if( !scn.isNull() ){ - Trace("regexp-ext-rewrite") << "Regexp : const conflict : " << node << std::endl; + Node scn = simpleRegexpConsume(mchildren, children); + if (!scn.isNull()) + { + Trace("regexp-ext-rewrite") + << "Regexp : const conflict : " << node << std::endl; return scn; - }else{ - if( (children.size() + mchildren.size())!=prevSize ){ + } + else + { + if ((children.size() + mchildren.size()) != prevSize) + { // Given a membership (str.++ x1 ... xn) in (re.++ r1 ... rm), // above, we strip components to construct an equivalent membership: // (str.++ xi .. xj) in (re.++ rk ... rl). Node xn = utils::mkConcat(STRING_CONCAT, mchildren); Node emptyStr = nm->mkConst(String("")); - if( children.empty() ){ + if (children.empty()) + { // If we stripped all components on the right, then the left is // equal to the empty string. // e.g. (str.++ "a" x) in (re.++ (str.to.re "a")) ---> (= x "") retNode = xn.eqNode(emptyStr); - }else{ + } + else + { // otherwise, construct the updated regular expression retNode = nm->mkNode( STRING_IN_REGEXP, xn, utils::mkConcat(REGEXP_CONCAT, children)); } - Trace("regexp-ext-rewrite") << "Regexp : rewrite : " << node << " -> " << retNode << std::endl; + Trace("regexp-ext-rewrite") << "Regexp : rewrite : " << node << " -> " + << retNode << std::endl; return returnRewrite(node, retNode, "re-simple-consume"); } } @@ -1582,8 +1768,10 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { return retNode; } -RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { - Trace("strings-postrewrite") << "Strings::postRewrite start " << node << std::endl; +RewriteResponse SequencesRewriter::postRewrite(TNode node) +{ + Trace("strings-postrewrite") + << "Strings::postRewrite start " << node << std::endl; NodeManager* nm = NodeManager::currentNM(); Node retNode = node; Node orig = retNode; @@ -1599,22 +1787,31 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { else if (nk == kind::STRING_LENGTH) { Kind nk0 = node[0].getKind(); - if( node[0].isConst() ){ + if (node[0].isConst()) + { retNode = nm->mkConst(Rational(Word::getLength(node[0]))); } else if (nk0 == kind::STRING_CONCAT) { Node tmpNode = node[0]; - if(tmpNode.isConst()) { + if (tmpNode.isConst()) + { retNode = nm->mkConst(Rational(Word::getLength(tmpNode))); - }else if( tmpNode.getKind()==kind::STRING_CONCAT ){ + } + else if (tmpNode.getKind() == kind::STRING_CONCAT) + { std::vector<Node> node_vec; - for(unsigned int i=0; i<tmpNode.getNumChildren(); ++i) { - if(tmpNode[i].isConst()) { + for (unsigned int i = 0; i < tmpNode.getNumChildren(); ++i) + { + if (tmpNode[i].isConst()) + { node_vec.push_back( nm->mkConst(Rational(Word::getLength(tmpNode[i])))); - } else { - node_vec.push_back( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, tmpNode[i]) ); + } + else + { + node_vec.push_back(NodeManager::currentNM()->mkNode( + kind::STRING_LENGTH, tmpNode[i])); } } retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec); @@ -1639,8 +1836,9 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } else if (nk == kind::STRING_CHARAT) { - Node one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); - retNode = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, node[0], node[1], one); + Node one = NodeManager::currentNM()->mkConst(Rational(1)); + retNode = NodeManager::currentNM()->mkNode( + kind::STRING_SUBSTR, node[0], node[1], one); } else if (nk == kind::STRING_SUBSTR) { @@ -1648,7 +1846,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } else if (nk == kind::STRING_STRCTN) { - retNode = rewriteContains( node ); + retNode = rewriteContains(node); } else if (nk == kind::STRING_LT) { @@ -1659,15 +1857,15 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } else if (nk == kind::STRING_LEQ) { - retNode = rewriteStringLeq(node); + retNode = StringsRewriter::rewriteStringLeq(node); } else if (nk == kind::STRING_STRIDOF) { - retNode = rewriteIndexof( node ); + retNode = rewriteIndexof(node); } else if (nk == kind::STRING_STRREPL) { - retNode = rewriteReplace( node ); + retNode = rewriteReplace(node); } else if (nk == kind::STRING_STRREPLALL) { @@ -1675,7 +1873,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } else if (nk == STRING_TOLOWER || nk == STRING_TOUPPER) { - retNode = rewriteStrConvert(node); + retNode = StringsRewriter::rewriteStrConvert(node); } else if (nk == STRING_REV) { @@ -1695,36 +1893,11 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } else if (nk == kind::STRING_ITOS) { - if(node[0].isConst()) { - if( node[0].getConst<Rational>().sgn()==-1 ){ - retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); - }else{ - std::string stmp = node[0].getConst<Rational>().getNumerator().toString(); - Assert(stmp[0] != '-'); - retNode = NodeManager::currentNM()->mkConst( ::CVC4::String(stmp) ); - } - } + retNode = StringsRewriter::rewriteIntToStr(node); } else if (nk == kind::STRING_STOI) { - if(node[0].isConst()) { - CVC4::String s = node[0].getConst<String>(); - if(s.isNumber()) { - retNode = nm->mkConst(s.toNumber()); - } else { - retNode = nm->mkConst(Rational(-1)); - } - } 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; - } - } - } - } + retNode = StringsRewriter::rewriteStrToInt(node); } else if (nk == kind::STRING_IN_REGEXP) { @@ -1732,7 +1905,11 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } else if (nk == STRING_TO_CODE) { - retNode = rewriteStringToCode(node); + retNode = StringsRewriter::rewriteStringToCode(node); + } + else if (nk == STRING_FROM_CODE) + { + retNode = StringsRewriter::rewriteStringFromCode(node); } else if (nk == REGEXP_CONCAT) { @@ -1744,7 +1921,8 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } else if (nk == REGEXP_DIFF) { - retNode = nm->mkNode(REGEXP_INTER, node[0],nm->mkNode(REGEXP_COMPLEMENT, node[1])); + retNode = nm->mkNode( + REGEXP_INTER, node[0], nm->mkNode(REGEXP_COMPLEMENT, node[1])); } else if (nk == REGEXP_STAR) { @@ -1773,15 +1951,21 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { retNode = rewriteLoopRegExp(node); } - Trace("strings-postrewrite") << "Strings::postRewrite returning " << retNode << std::endl; - if( orig!=retNode ){ - Trace("strings-rewrite-debug") << "Strings: post-rewrite " << orig << " to " << retNode << std::endl; + Trace("strings-postrewrite") + << "Strings::postRewrite returning " << retNode << std::endl; + if (orig != retNode) + { + Trace("strings-rewrite-debug") + << "Strings: post-rewrite " << orig << " to " << retNode << std::endl; } - return RewriteResponse(orig==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode); + return RewriteResponse(orig == retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, + retNode); } -bool TheoryStringsRewriter::hasEpsilonNode(TNode node) { - for(unsigned int i=0; i<node.getNumChildren(); i++) { +bool SequencesRewriter::hasEpsilonNode(TNode node) +{ + for (unsigned int i = 0; i < node.getNumChildren(); i++) + { if (node[i].getKind() == kind::STRING_TO_REGEXP && node[i][0].isConst() && Word::isEmpty(node[i][0])) { @@ -1791,11 +1975,12 @@ bool TheoryStringsRewriter::hasEpsilonNode(TNode node) { return false; } -RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { +RewriteResponse SequencesRewriter::preRewrite(TNode node) +{ return RewriteResponse(REWRITE_DONE, node); } -Node TheoryStringsRewriter::rewriteSubstr(Node node) +Node SequencesRewriter::rewriteSubstr(Node node) { Assert(node.getKind() == kind::STRING_SUBSTR); @@ -2086,11 +2271,13 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) return node; } -Node TheoryStringsRewriter::rewriteContains( Node node ) { +Node SequencesRewriter::rewriteContains(Node node) +{ Assert(node.getKind() == kind::STRING_STRCTN); NodeManager* nm = NodeManager::currentNM(); - if( node[0] == node[1] ){ + if (node[0] == node[1]) + { Node ret = NodeManager::currentNM()->mkConst(true); return returnRewrite(node, ret, "ctn-eq"); } @@ -2101,7 +2288,9 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { { Node ret = nm->mkConst(Word::find(node[0], node[1]) != std::string::npos); return returnRewrite(node, ret, "ctn-const"); - }else{ + } + else + { Node t = node[1]; if (Word::isEmpty(node[0])) { @@ -2302,7 +2491,8 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { // splitting if (node[0].getKind() == kind::STRING_CONCAT) { - if( node[1].isConst() ){ + if (node[1].isConst()) + { CVC4::String t = node[1].getConst<String>(); // Below, we are looking for a constant component of node[0] // has no overlap with node[1], which means we can split. @@ -2312,8 +2502,9 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { // Hence, we consider only the inner children. for (unsigned i = 1; i < (node[0].getNumChildren() - 1); i++) { - //constant contains - if( node[0][i].isConst() ){ + // constant contains + if (node[0][i].isConst()) + { CVC4::String s = node[0][i].getConst<String>(); // if no overlap, we can split into disjunction if (s.noOverlapWith(t)) @@ -2440,7 +2631,8 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { return node; } -Node TheoryStringsRewriter::rewriteIndexof( Node node ) { +Node SequencesRewriter::rewriteIndexof(Node node) +{ Assert(node.getKind() == kind::STRING_STRIDOF); NodeManager* nm = NodeManager::currentNM(); @@ -2632,7 +2824,7 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) { } } - if (node[2].isConst() && node[2].getConst<Rational>().sgn()==0) + if (node[2].isConst() && node[2].getConst<Rational>().sgn() == 0) { std::vector<Node> cb; std::vector<Node> ce; @@ -2650,7 +2842,8 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) { return node; } -Node TheoryStringsRewriter::rewriteReplace( Node node ) { +Node SequencesRewriter::rewriteReplace(Node node) +{ Assert(node.getKind() == kind::STRING_STRREPL); NodeManager* nm = NodeManager::currentNM(); @@ -3134,7 +3327,7 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { return node; } -Node TheoryStringsRewriter::rewriteReplaceAll(Node node) +Node SequencesRewriter::rewriteReplaceAll(Node node) { Assert(node.getKind() == STRING_STRREPLALL); @@ -3185,7 +3378,7 @@ Node TheoryStringsRewriter::rewriteReplaceAll(Node node) return node; } -Node TheoryStringsRewriter::rewriteReplaceInternal(Node node) +Node SequencesRewriter::rewriteReplaceInternal(Node node) { Kind nk = node.getKind(); Assert(nk == STRING_STRREPL || nk == STRING_STRREPLALL); @@ -3207,68 +3400,7 @@ Node TheoryStringsRewriter::rewriteReplaceInternal(Node node) return Node::null(); } -Node TheoryStringsRewriter::rewriteStrConvert(Node node) -{ - Kind nk = node.getKind(); - Assert(nk == STRING_TOLOWER || nk == STRING_TOUPPER); - NodeManager* nm = NodeManager::currentNM(); - if (node[0].isConst()) - { - std::vector<unsigned> nvec = node[0].getConst<String>().getVec(); - for (unsigned i = 0, nvsize = nvec.size(); i < nvsize; i++) - { - unsigned newChar = CVC4::String::convertUnsignedIntToCode(nvec[i]); - // transform it - // upper 65 ... 90 - // lower 97 ... 122 - if (nk == STRING_TOUPPER) - { - if (newChar >= 97 && newChar <= 122) - { - newChar = newChar - 32; - } - } - else if (nk == STRING_TOLOWER) - { - if (newChar >= 65 && newChar <= 90) - { - newChar = newChar + 32; - } - } - newChar = CVC4::String::convertCodeToUnsignedInt(newChar); - nvec[i] = newChar; - } - Node retNode = nm->mkConst(String(nvec)); - return returnRewrite(node, retNode, "str-conv-const"); - } - else if (node[0].getKind() == STRING_CONCAT) - { - NodeBuilder<> concatBuilder(STRING_CONCAT); - for (const Node& nc : node[0]) - { - concatBuilder << nm->mkNode(nk, nc); - } - // tolower( x1 ++ x2 ) --> tolower( x1 ) ++ tolower( x2 ) - Node retNode = concatBuilder.constructNode(); - return returnRewrite(node, retNode, "str-conv-minscope-concat"); - } - else if (node[0].getKind() == STRING_TOLOWER - || node[0].getKind() == STRING_TOUPPER) - { - // tolower( tolower( x ) ) --> tolower( x ) - // tolower( toupper( x ) ) --> tolower( x ) - Node retNode = nm->mkNode(nk, node[0][0]); - return returnRewrite(node, retNode, "str-conv-idem"); - } - else if (node[0].getKind() == STRING_ITOS) - { - // tolower( str.from.int( x ) ) --> str.from.int( x ) - return returnRewrite(node, node[0], "str-conv-itos"); - } - return node; -} - -Node TheoryStringsRewriter::rewriteStrReverse(Node node) +Node SequencesRewriter::rewriteStrReverse(Node node) { Assert(node.getKind() == STRING_REV); NodeManager* nm = NodeManager::currentNM(); @@ -3301,61 +3433,7 @@ Node TheoryStringsRewriter::rewriteStrReverse(Node node) return node; } -Node TheoryStringsRewriter::rewriteStringLeq(Node n) -{ - Assert(n.getKind() == kind::STRING_LEQ); - NodeManager* nm = NodeManager::currentNM(); - if (n[0] == n[1]) - { - Node ret = nm->mkConst(true); - return returnRewrite(n, ret, "str-leq-id"); - } - if (n[0].isConst() && n[1].isConst()) - { - String s = n[0].getConst<String>(); - String t = n[1].getConst<String>(); - Node ret = nm->mkConst(s.isLeq(t)); - return returnRewrite(n, ret, "str-leq-eval"); - } - // empty strings - for (unsigned i = 0; i < 2; i++) - { - if (n[i].isConst() && n[i].getConst<String>().isEmptyString()) - { - Node ret = i == 0 ? nm->mkConst(true) : n[0].eqNode(n[1]); - return returnRewrite(n, ret, "str-leq-empty"); - } - } - - std::vector<Node> n1; - utils::getConcat(n[0], n1); - std::vector<Node> n2; - utils::getConcat(n[1], n2); - Assert(!n1.empty() && !n2.empty()); - - // constant prefixes - if (n1[0].isConst() && n2[0].isConst() && n1[0] != n2[0]) - { - String s = n1[0].getConst<String>(); - String t = n2[0].getConst<String>(); - // only need to truncate if s is longer - if (s.size() > t.size()) - { - s = s.prefix(t.size()); - } - // if prefix is not leq, then entire string is not leq - if (!s.isLeq(t)) - { - Node ret = nm->mkConst(false); - return returnRewrite(n, ret, "str-leq-cprefix"); - } - } - - Trace("strings-rewrite-nf") << "No rewrites for : " << n << std::endl; - return n; -} - -Node TheoryStringsRewriter::rewritePrefixSuffix(Node n) +Node SequencesRewriter::rewritePrefixSuffix(Node n) { Assert(n.getKind() == kind::STRING_PREFIX || n.getKind() == kind::STRING_SUFFIX); @@ -3434,67 +3512,26 @@ Node TheoryStringsRewriter::rewritePrefixSuffix(Node n) return retNode; } -Node TheoryStringsRewriter::rewriteStringFromCode(Node n) +Node SequencesRewriter::splitConstant(Node a, Node b, int& index, bool isRev) { - Assert(n.getKind() == kind::STRING_FROM_CODE); - NodeManager* nm = NodeManager::currentNM(); - - if (n[0].isConst()) - { - Integer i = n[0].getConst<Rational>().getNumerator(); - Node ret; - if (i >= 0 && i < strings::utils::getAlphabetCardinality()) - { - std::vector<unsigned> svec = {i.toUnsignedInt()}; - ret = nm->mkConst(String(svec)); - } - else - { - ret = nm->mkConst(String("")); - } - return returnRewrite(n, ret, "from-code-eval"); - } - - return n; -} - -Node TheoryStringsRewriter::rewriteStringToCode(Node n) -{ - Assert(n.getKind() == kind::STRING_TO_CODE); - if (n[0].isConst()) - { - CVC4::String s = n[0].getConst<String>(); - Node ret; - if (s.size() == 1) - { - std::vector<unsigned> vec = s.getVec(); - Assert(vec.size() == 1); - ret = NodeManager::currentNM()->mkConst( - Rational(CVC4::String::convertUnsignedIntToCode(vec[0]))); - } - else - { - ret = NodeManager::currentNM()->mkConst(Rational(-1)); - } - return returnRewrite(n, ret, "to-code-eval"); - } - - return n; -} - -Node TheoryStringsRewriter::splitConstant( Node a, Node b, int& index, bool isRev ) { Assert(a.isConst() && b.isConst()); size_t lenA = Word::getLength(a); size_t lenB = Word::getLength(b); index = lenA <= lenB ? 1 : 0; size_t len_short = index == 1 ? lenA : lenB; - bool cmp = isRev ? a.getConst<String>().rstrncmp(b.getConst<String>(), len_short): a.getConst<String>().strncmp(b.getConst<String>(), len_short); - if( cmp ) { - Node l = index==0 ? a : b; - if( isRev ){ + bool cmp = + isRev ? a.getConst<String>().rstrncmp(b.getConst<String>(), len_short) + : a.getConst<String>().strncmp(b.getConst<String>(), len_short); + if (cmp) + { + Node l = index == 0 ? a : b; + if (isRev) + { int new_len = l.getConst<String>().size() - len_short; return Word::substr(l, 0, new_len); - }else{ + } + else + { return Word::substr(l, len_short); } } @@ -3502,24 +3539,33 @@ Node TheoryStringsRewriter::splitConstant( Node a, Node b, int& index, bool isRe return Node::null(); } -bool TheoryStringsRewriter::canConstantContainConcat( Node c, Node n, int& firstc, int& lastc ) { +bool SequencesRewriter::canConstantContainConcat(Node c, + Node n, + int& firstc, + int& lastc) +{ Assert(c.isConst()); CVC4::String t = c.getConst<String>(); const std::vector<unsigned>& tvec = t.getVec(); Assert(n.getKind() == kind::STRING_CONCAT); - //must find constant components in order + // must find constant components in order size_t pos = 0; firstc = -1; lastc = -1; - for(unsigned i=0; i<n.getNumChildren(); i++) { - if( n[i].isConst() ){ - firstc = firstc==-1 ? i : firstc; + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + if (n[i].isConst()) + { + firstc = firstc == -1 ? i : firstc; lastc = i; CVC4::String s = n[i].getConst<String>(); - size_t new_pos = t.find(s,pos); - if( new_pos==std::string::npos ) { + size_t new_pos = t.find(s, pos); + if (new_pos == std::string::npos) + { return false; - }else{ + } + else + { pos = new_pos + s.size(); } } @@ -3541,20 +3587,29 @@ bool TheoryStringsRewriter::canConstantContainConcat( Node c, Node n, int& first return true; } -bool TheoryStringsRewriter::canConstantContainList( Node c, std::vector< Node >& l, int& firstc, int& lastc ) { +bool SequencesRewriter::canConstantContainList(Node c, + std::vector<Node>& l, + int& firstc, + int& lastc) +{ Assert(c.isConst()); - //must find constant components in order + // must find constant components in order size_t pos = 0; firstc = -1; lastc = -1; - for(unsigned i=0; i<l.size(); i++) { - if( l[i].isConst() ){ - firstc = firstc==-1 ? i : firstc; + for (unsigned i = 0; i < l.size(); i++) + { + if (l[i].isConst()) + { + firstc = firstc == -1 ? i : firstc; lastc = i; size_t new_pos = Word::find(c, l[i], pos); - if( new_pos==std::string::npos ) { + if (new_pos == std::string::npos) + { return false; - }else{ + } + else + { pos = new_pos + Word::getLength(l[i]); } } @@ -3562,10 +3617,10 @@ bool TheoryStringsRewriter::canConstantContainList( Node c, std::vector< Node >& return true; } -bool TheoryStringsRewriter::stripSymbolicLength(std::vector<Node>& n1, - std::vector<Node>& nr, - int dir, - Node& curr) +bool SequencesRewriter::stripSymbolicLength(std::vector<Node>& n1, + std::vector<Node>& nr, + int dir, + Node& curr) { Assert(dir == 1 || dir == -1); Assert(nr.empty()); @@ -3676,12 +3731,12 @@ bool TheoryStringsRewriter::stripSymbolicLength(std::vector<Node>& n1, return ret; } -int TheoryStringsRewriter::componentContains(std::vector<Node>& n1, - std::vector<Node>& n2, - std::vector<Node>& nb, - std::vector<Node>& ne, - bool computeRemainder, - int remainderDir) +int SequencesRewriter::componentContains(std::vector<Node>& n1, + std::vector<Node>& n2, + std::vector<Node>& nb, + std::vector<Node>& ne, + bool computeRemainder, + int remainderDir) { Assert(nb.empty()); Assert(ne.empty()); @@ -3803,7 +3858,7 @@ int TheoryStringsRewriter::componentContains(std::vector<Node>& n1, return -1; } -bool TheoryStringsRewriter::componentContainsBase( +bool SequencesRewriter::componentContainsBase( Node n1, Node n2, Node& n1rb, Node& n1re, int dir, bool computeRemainder) { Assert(n1rb.isNull()); @@ -3942,11 +3997,11 @@ bool TheoryStringsRewriter::componentContainsBase( return false; } -bool TheoryStringsRewriter::stripConstantEndpoints(std::vector<Node>& n1, - std::vector<Node>& n2, - std::vector<Node>& nb, - std::vector<Node>& ne, - int dir) +bool SequencesRewriter::stripConstantEndpoints(std::vector<Node>& n1, + std::vector<Node>& n2, + std::vector<Node>& nb, + std::vector<Node>& ne, + int dir) { Assert(nb.empty()); Assert(ne.empty()); @@ -4123,7 +4178,7 @@ bool TheoryStringsRewriter::stripConstantEndpoints(std::vector<Node>& n1, return changed; } -Node TheoryStringsRewriter::canonicalStrForSymbolicLength(Node len) +Node SequencesRewriter::canonicalStrForSymbolicLength(Node len) { NodeManager* nm = NodeManager::currentNM(); @@ -4179,7 +4234,7 @@ Node TheoryStringsRewriter::canonicalStrForSymbolicLength(Node len) return res; } -Node TheoryStringsRewriter::lengthPreserveRewrite(Node n) +Node SequencesRewriter::lengthPreserveRewrite(Node n) { NodeManager* nm = NodeManager::currentNM(); Node len = Rewriter::rewrite(nm->mkNode(kind::STRING_LENGTH, n)); @@ -4187,9 +4242,7 @@ Node TheoryStringsRewriter::lengthPreserveRewrite(Node n) return res.isNull() ? n : res; } -Node TheoryStringsRewriter::checkEntailContains(Node a, - Node b, - bool fullRewriter) +Node SequencesRewriter::checkEntailContains(Node a, Node b, bool fullRewriter) { NodeManager* nm = NodeManager::currentNM(); Node ctn = nm->mkNode(kind::STRING_STRCTN, a, b); @@ -4212,14 +4265,14 @@ Node TheoryStringsRewriter::checkEntailContains(Node a, return ctn.isConst() ? ctn : Node::null(); } -bool TheoryStringsRewriter::checkEntailNonEmpty(Node a) +bool SequencesRewriter::checkEntailNonEmpty(Node a) { Node len = NodeManager::currentNM()->mkNode(STRING_LENGTH, a); len = Rewriter::rewrite(len); return checkEntailArith(len, true); } -bool TheoryStringsRewriter::checkEntailLengthOne(Node s, bool strict) +bool SequencesRewriter::checkEntailLengthOne(Node s, bool strict) { NodeManager* nm = NodeManager::currentNM(); Node one = nm->mkConst(Rational(1)); @@ -4228,7 +4281,7 @@ bool TheoryStringsRewriter::checkEntailLengthOne(Node s, bool strict) return checkEntailArith(one, len) && (!strict || checkEntailArith(len, true)); } -bool TheoryStringsRewriter::checkEntailArithEq(Node a, Node b) +bool SequencesRewriter::checkEntailArithEq(Node a, Node b) { if (a == b) { @@ -4242,7 +4295,7 @@ bool TheoryStringsRewriter::checkEntailArithEq(Node a, Node b) } } -bool TheoryStringsRewriter::checkEntailArith(Node a, Node b, bool strict) +bool SequencesRewriter::checkEntailArith(Node a, Node b, bool strict) { if (a == b) { @@ -4266,7 +4319,7 @@ typedef expr::Attribute<StrCheckEntailArithTag, bool> StrCheckEntailArithAttr; typedef expr::Attribute<StrCheckEntailArithComputedTag, bool> StrCheckEntailArithComputedAttr; -bool TheoryStringsRewriter::checkEntailArith(Node a, bool strict) +bool SequencesRewriter::checkEntailArith(Node a, bool strict) { if (a.isConst()) { @@ -4297,7 +4350,7 @@ bool TheoryStringsRewriter::checkEntailArith(Node a, bool strict) return ret; } -bool TheoryStringsRewriter::checkEntailArithApprox(Node ar) +bool SequencesRewriter::checkEntailArithApprox(Node ar) { Assert(Rewriter::rewrite(ar) == ar); NodeManager* nm = NodeManager::currentNM(); @@ -4572,9 +4625,9 @@ bool TheoryStringsRewriter::checkEntailArithApprox(Node ar) return false; } -void TheoryStringsRewriter::getArithApproximations(Node a, - std::vector<Node>& approx, - bool isOverApprox) +void SequencesRewriter::getArithApproximations(Node a, + std::vector<Node>& approx, + bool isOverApprox) { NodeManager* nm = NodeManager::currentNM(); // We do not handle PLUS here since this leads to exponential behavior. @@ -4760,7 +4813,7 @@ void TheoryStringsRewriter::getArithApproximations(Node a, Trace("strings-ent-approx-debug") << "Return " << approx.size() << std::endl; } -bool TheoryStringsRewriter::checkEntailMultisetSubset(Node a, Node b) +bool SequencesRewriter::checkEntailMultisetSubset(Node a, Node b) { NodeManager* nm = NodeManager::currentNM(); @@ -4846,7 +4899,7 @@ bool TheoryStringsRewriter::checkEntailMultisetSubset(Node a, Node b) return false; } -Node TheoryStringsRewriter::checkEntailHomogeneousString(Node a) +Node SequencesRewriter::checkEntailHomogeneousString(Node a) { NodeManager* nm = NodeManager::currentNM(); @@ -4890,7 +4943,7 @@ Node TheoryStringsRewriter::checkEntailHomogeneousString(Node a) return nm->mkConst(String(cv)); } -Node TheoryStringsRewriter::getMultisetApproximation(Node a) +Node SequencesRewriter::getMultisetApproximation(Node a) { NodeManager* nm = NodeManager::currentNM(); if (a.getKind() == STRING_SUBSTR) @@ -4916,9 +4969,9 @@ Node TheoryStringsRewriter::getMultisetApproximation(Node a) } } -bool TheoryStringsRewriter::checkEntailArithWithEqAssumption(Node assumption, - Node a, - bool strict) +bool SequencesRewriter::checkEntailArithWithEqAssumption(Node assumption, + Node a, + bool strict) { Assert(assumption.getKind() == kind::EQUAL); Assert(Rewriter::rewrite(assumption) == assumption); @@ -4987,10 +5040,10 @@ bool TheoryStringsRewriter::checkEntailArithWithEqAssumption(Node assumption, return checkEntailArith(a, strict); } -bool TheoryStringsRewriter::checkEntailArithWithAssumption(Node assumption, - Node a, - Node b, - bool strict) +bool SequencesRewriter::checkEntailArithWithAssumption(Node assumption, + Node a, + Node b, + bool strict) { Assert(Rewriter::rewrite(assumption) == assumption); @@ -5043,7 +5096,7 @@ bool TheoryStringsRewriter::checkEntailArithWithAssumption(Node assumption, return res; } -bool TheoryStringsRewriter::checkEntailArithWithAssumptions( +bool SequencesRewriter::checkEntailArithWithAssumptions( std::vector<Node> assumptions, Node a, Node b, bool strict) { // TODO: We currently try to show the entailment with each assumption @@ -5063,7 +5116,7 @@ bool TheoryStringsRewriter::checkEntailArithWithAssumptions( return res; } -Node TheoryStringsRewriter::getConstantArithBound(Node a, bool isLower) +Node SequencesRewriter::getConstantArithBound(Node a, bool isLower) { Assert(Rewriter::rewrite(a) == a); Node ret; @@ -5146,7 +5199,7 @@ Node TheoryStringsRewriter::getConstantArithBound(Node a, bool isLower) return ret; } -Node TheoryStringsRewriter::getFixedLengthForRegexp(Node n) +Node SequencesRewriter::getFixedLengthForRegexp(Node n) { NodeManager* nm = NodeManager::currentNM(); if (n.getKind() == STRING_TO_REGEXP) @@ -5199,7 +5252,7 @@ Node TheoryStringsRewriter::getFixedLengthForRegexp(Node n) return Node::null(); } -bool TheoryStringsRewriter::checkEntailArithInternal(Node a) +bool SequencesRewriter::checkEntailArithInternal(Node a) { Assert(Rewriter::rewrite(a) == a); // check whether a >= 0 @@ -5228,9 +5281,9 @@ bool TheoryStringsRewriter::checkEntailArithInternal(Node a) return false; } -Node TheoryStringsRewriter::decomposeSubstrChain(Node s, - std::vector<Node>& ss, - std::vector<Node>& ls) +Node SequencesRewriter::decomposeSubstrChain(Node s, + std::vector<Node>& ss, + std::vector<Node>& ls) { Assert(ss.empty()); Assert(ls.empty()); @@ -5245,9 +5298,9 @@ Node TheoryStringsRewriter::decomposeSubstrChain(Node s, return s; } -Node TheoryStringsRewriter::mkSubstrChain(Node base, - const std::vector<Node>& ss, - const std::vector<Node>& ls) +Node SequencesRewriter::mkSubstrChain(Node base, + const std::vector<Node>& ss, + const std::vector<Node>& ls) { NodeManager* nm = NodeManager::currentNM(); for (unsigned i = 0, size = ss.size(); i < size; i++) @@ -5257,7 +5310,7 @@ Node TheoryStringsRewriter::mkSubstrChain(Node base, return base; } -Node TheoryStringsRewriter::getStringOrEmpty(Node n) +Node SequencesRewriter::getStringOrEmpty(Node n) { NodeManager* nm = NodeManager::currentNM(); Node res; @@ -5294,7 +5347,7 @@ Node TheoryStringsRewriter::getStringOrEmpty(Node n) break; } res = n; - break; + break; } default: { @@ -5306,9 +5359,9 @@ Node TheoryStringsRewriter::getStringOrEmpty(Node n) return res; } -bool TheoryStringsRewriter::inferZerosInSumGeq(Node x, - std::vector<Node>& ys, - std::vector<Node>& zeroYs) +bool SequencesRewriter::inferZerosInSumGeq(Node x, + std::vector<Node>& ys, + std::vector<Node>& zeroYs) { Assert(zeroYs.empty()); @@ -5354,7 +5407,7 @@ bool TheoryStringsRewriter::inferZerosInSumGeq(Node x, return true; } -Node TheoryStringsRewriter::inferEqsFromContains(Node x, Node y) +Node SequencesRewriter::inferEqsFromContains(Node x, Node y) { NodeManager* nm = NodeManager::currentNM(); Node emp = nm->mkConst(String("")); @@ -5441,8 +5494,7 @@ Node TheoryStringsRewriter::inferEqsFromContains(Node x, Node y) return nb.constructNode(); } -std::pair<bool, std::vector<Node> > TheoryStringsRewriter::collectEmptyEqs( - Node x) +std::pair<bool, std::vector<Node> > SequencesRewriter::collectEmptyEqs(Node x) { NodeManager* nm = NodeManager::currentNM(); Node empty = nm->mkConst(::CVC4::String("")); @@ -5496,7 +5548,7 @@ std::pair<bool, std::vector<Node> > TheoryStringsRewriter::collectEmptyEqs( allEmptyEqs, std::vector<Node>(emptyNodes.begin(), emptyNodes.end())); } -Node TheoryStringsRewriter::returnRewrite(Node node, Node ret, const char* c) +Node SequencesRewriter::returnRewrite(Node node, Node ret, const char* c) { Trace("strings-rewrite") << "Rewrite " << node << " to " << ret << " by " << c << "." << std::endl; diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/sequences_rewriter.h index 4accfca39..5aba4ab6f 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/sequences_rewriter.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file theory_strings_rewriter.h +/*! \file sequences_rewriter.h ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds, Andres Noetzli, Tianyi Liang @@ -9,14 +9,14 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Rewriter for the theory of strings + ** \brief Rewriter for the theory of strings and sequences ** **/ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__THEORY_STRINGS_REWRITER_H -#define CVC4__THEORY__STRINGS__THEORY_STRINGS_REWRITER_H +#ifndef CVC4__THEORY__STRINGS__SEQUENCES_REWRITER_H +#define CVC4__THEORY__STRINGS__SEQUENCES_REWRITER_H #include <climits> #include <utility> @@ -30,9 +30,9 @@ namespace CVC4 { namespace theory { namespace strings { -class TheoryStringsRewriter : public TheoryRewriter +class SequencesRewriter : public TheoryRewriter { - private: + protected: /** simple regular expression consume * * This method is called when we are rewriting a membership of the form @@ -88,9 +88,13 @@ class TheoryStringsRewriter : public TheoryRewriter * "bb" ++ x in ( "b" ++ ("a")* )* * is equivalent to false. */ - static Node simpleRegexpConsume( std::vector< Node >& mchildren, std::vector< Node >& children, int dir = -1 ); - static bool isConstRegExp( TNode t ); - static bool testConstStringInRegExp( CVC4::String &s, unsigned int index_start, TNode r ); + static Node simpleRegexpConsume(std::vector<Node>& mchildren, + std::vector<Node>& children, + int dir = -1); + static bool isConstRegExp(TNode t); + static bool testConstStringInRegExp(CVC4::String& s, + unsigned int index_start, + TNode r); /** rewrite regular expression concatenation * @@ -178,38 +182,38 @@ class TheoryStringsRewriter : public TheoryRewriter */ static Node rewriteEqualityExt(Node node); /** rewrite concat - * This is the entry point for post-rewriting terms node of the form - * str.++( t1, .., tn ) - * Returns the rewritten form of node. - */ + * This is the entry point for post-rewriting terms node of the form + * str.++( t1, .., tn ) + * Returns the rewritten form of node. + */ static Node rewriteConcat(Node node); /** rewrite substr - * This is the entry point for post-rewriting terms node of the form - * str.substr( s, i1, i2 ) - * Returns the rewritten form of node. - */ + * This is the entry point for post-rewriting terms node of the form + * str.substr( s, i1, i2 ) + * Returns the rewritten form of node. + */ static Node rewriteSubstr(Node node); /** rewrite contains - * This is the entry point for post-rewriting terms node of the form - * str.contains( t, s ) - * Returns the rewritten form of node. - * - * For details on some of the basic rewrites done in this function, see Figure - * 7 of Reynolds et al "Scaling Up DPLL(T) String Solvers Using - * Context-Dependent Rewriting", CAV 2017. - */ + * This is the entry point for post-rewriting terms node of the form + * str.contains( t, s ) + * Returns the rewritten form of node. + * + * For details on some of the basic rewrites done in this function, see Figure + * 7 of Reynolds et al "Scaling Up DPLL(T) String Solvers Using + * Context-Dependent Rewriting", CAV 2017. + */ static Node rewriteContains(Node node); /** rewrite indexof - * This is the entry point for post-rewriting terms n of the form - * str.indexof( s, t, n ) - * Returns the rewritten form of node. - */ + * This is the entry point for post-rewriting terms n of the form + * str.indexof( s, t, n ) + * Returns the rewritten form of node. + */ static Node rewriteIndexof(Node node); /** rewrite replace - * This is the entry point for post-rewriting terms n of the form - * str.replace( s, t, r ) - * Returns the rewritten form of node. - */ + * This is the entry point for post-rewriting terms n of the form + * str.replace( s, t, r ) + * Returns the rewritten form of node. + */ static Node rewriteReplace(Node node); /** rewrite replace all * This is the entry point for post-rewriting terms n of the form @@ -223,13 +227,6 @@ class TheoryStringsRewriter : public TheoryRewriter * str.replaceall. If it returns a non-null ret, then node rewrites to ret. */ static Node rewriteReplaceInternal(Node node); - /** rewrite string convert - * - * This is the entry point for post-rewriting terms n of the form - * str.tolower( s ) and str.toupper( s ) - * Returns the rewritten form of node. - */ - static Node rewriteStrConvert(Node node); /** rewrite string reverse * * This is the entry point for post-rewriting terms n of the form @@ -237,25 +234,12 @@ class TheoryStringsRewriter : public TheoryRewriter * Returns the rewritten form of node. */ static Node rewriteStrReverse(Node node); - /** rewrite string less than or equal - * This is the entry point for post-rewriting terms n of the form - * str.<=( t, s ) - * Returns the rewritten form of n. - */ - static Node rewriteStringLeq(Node n); /** rewrite prefix/suffix - * This is the entry point for post-rewriting terms n of the form - * str.prefixof( s, t ) / str.suffixof( s, t ) - * Returns the rewritten form of node. - */ - static Node rewritePrefixSuffix(Node node); - - /** rewrite str.from_code * This is the entry point for post-rewriting terms n of the form - * str.from_code( t ) + * str.prefixof( s, t ) / str.suffixof( s, t ) * Returns the rewritten form of node. */ - static Node rewriteStringFromCode(Node node); + static Node rewritePrefixSuffix(Node node); /** rewrite str.to_code * This is the entry point for post-rewriting terms n of the form @@ -264,7 +248,7 @@ class TheoryStringsRewriter : public TheoryRewriter */ static Node rewriteStringToCode(Node node); - static Node splitConstant( Node a, Node b, int& index, bool isRev ); + static Node splitConstant(Node a, Node b, int& index, bool isRev); /** can constant contain list * return true if constant c can contain the list l in order * firstc/lastc store which indices in l were used to determine the return @@ -277,17 +261,20 @@ class TheoryStringsRewriter : public TheoryRewriter * firstc/lastc are updated to 1/1 * canConstantContainList( "abc", { x, "d", y } ) returns false * firstc/lastc are updated to 1/1 - * canConstantContainList( "abcdef", { x, "b", y, "a", z, "c", w } + * canConstantContainList( "abcdef", { x, "b", y, "a", z, "c", w } * returns false * firstc/lastc are updated to 1/3 - * canConstantContainList( "abcdef", { x, "b", y, "e", z, "c", w } + * canConstantContainList( "abcdef", { x, "b", y, "e", z, "c", w } * returns false * firstc/lastc are updated to 1/5 */ - static bool canConstantContainList( Node c, std::vector< Node >& l, int& firstc, int& lastc ); + static bool canConstantContainList(Node c, + std::vector<Node>& l, + int& firstc, + int& lastc); /** can constant contain concat - * same as above but with n = str.++( l ) instead of l - */ + * same as above but with n = str.++( l ) instead of l + */ static bool canConstantContainConcat(Node c, Node n, int& firstc, int& lastc); /** strip symbolic length @@ -334,54 +321,54 @@ class TheoryStringsRewriter : public TheoryRewriter int dir, Node& curr); /** component contains - * This function is used when rewriting str.contains( t1, t2 ), where - * n1 is the vector form of t1 - * n2 is the vector form of t2 - * - * If this function returns n>=0 for some n, then - * n1 = { x1...x{n-1} xn...x{n+s} x{n+s+1}...xm }, - * n2 = { y1...ys }, - * y1 is a suffix of xn, - * y2...y{s-1} = x{n+1}...x{n+s-1}, and - * ys is a prefix of x{n+s} - * Otherwise it returns -1. - * - * This function may update n1 if computeRemainder = true. - * We maintain the invariant that the resulting value n1' - * of n1 after this function is such that: - * n1 = str.++( nb, n1', ne ) - * The vectors nb and ne have the following properties. - * If computeRemainder = true, then - * If remainderDir != -1, then - * ne is { x{n+s}' x{n+s+1}...xm } - * where x{n+s} = str.++( ys, x{n+s}' ). - * If remainderDir != 1, then - * nb is { x1, ..., x{n-1}, xn' } - * where xn = str.++( xn', y1 ). - * - * For example: - * - * componentContains({ x, "abc", x }, { "b" }, {}, true, 0) - * returns 1, - * n1 is updated to { "b" }, - * nb is updated to { x, "a" }, - * ne is updated to { "c", x } - * - * componentContains({ x, "abc", x }, { "b" }, {}, true, 1) - * returns 1, - * n1 is updated to { x, "ab" }, - * ne is updated to { "c", x } - * - * componentContains({ y, z, "abc", x, "def" }, { "c", x, "de" }, {}, true, 1) - * returns 2, - * n1 is updated to { y, z, "abc", x, "de" }, - * ne is updated to { "f" } - * - * componentContains({ y, "abc", x, "def" }, { "c", x, "de" }, {}, true, -1) - * returns 1, - * n1 is updated to { "c", x, "def" }, - * nb is updated to { y, "ab" } - */ + * This function is used when rewriting str.contains( t1, t2 ), where + * n1 is the vector form of t1 + * n2 is the vector form of t2 + * + * If this function returns n>=0 for some n, then + * n1 = { x1...x{n-1} xn...x{n+s} x{n+s+1}...xm }, + * n2 = { y1...ys }, + * y1 is a suffix of xn, + * y2...y{s-1} = x{n+1}...x{n+s-1}, and + * ys is a prefix of x{n+s} + * Otherwise it returns -1. + * + * This function may update n1 if computeRemainder = true. + * We maintain the invariant that the resulting value n1' + * of n1 after this function is such that: + * n1 = str.++( nb, n1', ne ) + * The vectors nb and ne have the following properties. + * If computeRemainder = true, then + * If remainderDir != -1, then + * ne is { x{n+s}' x{n+s+1}...xm } + * where x{n+s} = str.++( ys, x{n+s}' ). + * If remainderDir != 1, then + * nb is { x1, ..., x{n-1}, xn' } + * where xn = str.++( xn', y1 ). + * + * For example: + * + * componentContains({ x, "abc", x }, { "b" }, {}, true, 0) + * returns 1, + * n1 is updated to { "b" }, + * nb is updated to { x, "a" }, + * ne is updated to { "c", x } + * + * componentContains({ x, "abc", x }, { "b" }, {}, true, 1) + * returns 1, + * n1 is updated to { x, "ab" }, + * ne is updated to { "c", x } + * + * componentContains({ y, z, "abc", x, "def" }, { "c", x, "de" }, {}, true, 1) + * returns 2, + * n1 is updated to { y, z, "abc", x, "de" }, + * ne is updated to { "f" } + * + * componentContains({ y, "abc", x, "def" }, { "c", x, "de" }, {}, true, -1) + * returns 1, + * n1 is updated to { "c", x, "def" }, + * nb is updated to { y, "ab" } + */ static int componentContains(std::vector<Node>& n1, std::vector<Node>& n2, std::vector<Node>& nb, @@ -443,37 +430,37 @@ class TheoryStringsRewriter : public TheoryRewriter static bool componentContainsBase( Node n1, Node n2, Node& n1rb, Node& n1re, int dir, bool computeRemainder); /** strip constant endpoints - * This function is used when rewriting str.contains( t1, t2 ), where - * n1 is the vector form of t1 - * n2 is the vector form of t2 - * - * It modifies n1 to a new vector n1' such that: - * (1) str.contains( str.++( n1 ), str.++( n2 ) ) is equivalent to - * str.contains( str.++( n1' ), str.++( n2 ) ) - * (2) str.++( n1 ) = str.++( nb, n1', ne ) - * - * "dir" is the direction in which we can modify n1: - * if dir = 1, then we allow dropping components from the front of n1, - * if dir = -1, then we allow dropping components from the back of n1, - * if dir = 0, then we allow dropping components from either. - * - * It returns true if n1 is modified. - * - * For example: - * stripConstantEndpoints({ "ab", x, "de" }, { "c" }, {}, {}, 1) - * returns true, - * n1 is updated to { x, "de" } - * nb is updated to { "ab" } - * stripConstantEndpoints({ "ab", x, "de" }, { "bd" }, {}, {}, 0) - * returns true, - * n1 is updated to { "b", x, "d" } - * nb is updated to { "a" } - * ne is updated to { "e" } - * stripConstantEndpoints({ "ad", substr("ccc",x,y) }, { "d" }, {}, {}, -1) - * returns true, - * n1 is updated to {"ad"} - * ne is updated to { substr("ccc",x,y) } - */ + * This function is used when rewriting str.contains( t1, t2 ), where + * n1 is the vector form of t1 + * n2 is the vector form of t2 + * + * It modifies n1 to a new vector n1' such that: + * (1) str.contains( str.++( n1 ), str.++( n2 ) ) is equivalent to + * str.contains( str.++( n1' ), str.++( n2 ) ) + * (2) str.++( n1 ) = str.++( nb, n1', ne ) + * + * "dir" is the direction in which we can modify n1: + * if dir = 1, then we allow dropping components from the front of n1, + * if dir = -1, then we allow dropping components from the back of n1, + * if dir = 0, then we allow dropping components from either. + * + * It returns true if n1 is modified. + * + * For example: + * stripConstantEndpoints({ "ab", x, "de" }, { "c" }, {}, {}, 1) + * returns true, + * n1 is updated to { x, "de" } + * nb is updated to { "ab" } + * stripConstantEndpoints({ "ab", x, "de" }, { "bd" }, {}, {}, 0) + * returns true, + * n1 is updated to { "b", x, "d" } + * nb is updated to { "a" } + * ne is updated to { "e" } + * stripConstantEndpoints({ "ad", substr("ccc",x,y) }, { "d" }, {}, {}, -1) + * returns true, + * n1 is updated to {"ad"} + * ne is updated to { substr("ccc",x,y) } + */ static bool stripConstantEndpoints(std::vector<Node>& n1, std::vector<Node>& n2, std::vector<Node>& nb, @@ -779,10 +766,10 @@ class TheoryStringsRewriter : public TheoryRewriter * and the list of nodes that are compared to the empty string */ static std::pair<bool, std::vector<Node> > collectEmptyEqs(Node x); -}; /* class TheoryStringsRewriter */ +}; /* class SequencesRewriter */ -}/* CVC4::theory::strings namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace strings +} // namespace theory +} // namespace CVC4 -#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_REWRITER_H */ +#endif /* CVC4__THEORY__STRINGS__SEQUENCES_REWRITER_H */ diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index b4e1c74ea..7396a5013 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -15,7 +15,7 @@ #include "theory/strings/skolem_cache.h" #include "theory/rewriter.h" -#include "theory/strings/theory_strings_rewriter.h" +#include "theory/strings/sequences_rewriter.h" #include "util/rational.h" using namespace CVC4::kind; @@ -163,8 +163,8 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b) a = s; b = m; } - else if (TheoryStringsRewriter::checkEntailArith( - nm->mkNode(PLUS, n, m), nm->mkNode(STRING_LENGTH, s))) + else if (SequencesRewriter::checkEntailArith(nm->mkNode(PLUS, n, m), + nm->mkNode(STRING_LENGTH, s))) { // SK_PURIFY((str.substr x n m)) ---> SK_SUFFIX_REM(x, n) // if n + m >= (str.len x) diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp new file mode 100644 index 000000000..75dfe7432 --- /dev/null +++ b/src/theory/strings/strings_rewriter.cpp @@ -0,0 +1,247 @@ +/********************* */ +/*! \file strings_rewriter.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Andres Noetzli, Tianyi Liang + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of rewrite rules for string-specific operators in + ** theory of strings. + **/ + +#include "theory/strings/strings_rewriter.h" + +#include "expr/node_builder.h" +#include "theory/strings/theory_strings_utils.h" +#include "util/rational.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace strings { + +Node StringsRewriter::rewriteStrToInt(Node node) +{ + Assert(node.getKind() == STRING_STOI); + NodeManager* nm = NodeManager::currentNM(); + if (node[0].isConst()) + { + Node ret; + String s = node[0].getConst<String>(); + if (s.isNumber()) + { + ret = nm->mkConst(s.toNumber()); + } + else + { + ret = nm->mkConst(Rational(-1)); + } + return returnRewrite(node, ret, "stoi-eval"); + } + else if (node[0].getKind() == STRING_CONCAT) + { + for (TNode nc : node[0]) + { + if (nc.isConst()) + { + String t = nc.getConst<String>(); + if (!t.isNumber()) + { + Node ret = nm->mkConst(Rational(-1)); + return returnRewrite(node, ret, "stoi-concat-nonnum"); + } + } + } + } + return node; +} + +Node StringsRewriter::rewriteIntToStr(Node node) +{ + Assert(node.getKind() == STRING_ITOS); + NodeManager* nm = NodeManager::currentNM(); + if (node[0].isConst()) + { + Node ret; + if (node[0].getConst<Rational>().sgn() == -1) + { + ret = nm->mkConst(String("")); + } + else + { + std::string stmp = node[0].getConst<Rational>().getNumerator().toString(); + Assert(stmp[0] != '-'); + ret = nm->mkConst(String(stmp)); + } + return returnRewrite(node, ret, "itos-eval"); + } + return node; +} + +Node StringsRewriter::rewriteStrConvert(Node node) +{ + Kind nk = node.getKind(); + Assert(nk == STRING_TOLOWER || nk == STRING_TOUPPER); + NodeManager* nm = NodeManager::currentNM(); + if (node[0].isConst()) + { + std::vector<unsigned> nvec = node[0].getConst<String>().getVec(); + for (unsigned i = 0, nvsize = nvec.size(); i < nvsize; i++) + { + unsigned newChar = String::convertUnsignedIntToCode(nvec[i]); + // transform it + // upper 65 ... 90 + // lower 97 ... 122 + if (nk == STRING_TOUPPER) + { + if (newChar >= 97 && newChar <= 122) + { + newChar = newChar - 32; + } + } + else if (nk == STRING_TOLOWER) + { + if (newChar >= 65 && newChar <= 90) + { + newChar = newChar + 32; + } + } + newChar = String::convertCodeToUnsignedInt(newChar); + nvec[i] = newChar; + } + Node retNode = nm->mkConst(String(nvec)); + return returnRewrite(node, retNode, "str-conv-const"); + } + else if (node[0].getKind() == STRING_CONCAT) + { + NodeBuilder<> concatBuilder(STRING_CONCAT); + for (const Node& nc : node[0]) + { + concatBuilder << nm->mkNode(nk, nc); + } + // tolower( x1 ++ x2 ) --> tolower( x1 ) ++ tolower( x2 ) + Node retNode = concatBuilder.constructNode(); + return returnRewrite(node, retNode, "str-conv-minscope-concat"); + } + else if (node[0].getKind() == STRING_TOLOWER + || node[0].getKind() == STRING_TOUPPER) + { + // tolower( tolower( x ) ) --> tolower( x ) + // tolower( toupper( x ) ) --> tolower( x ) + Node retNode = nm->mkNode(nk, node[0][0]); + return returnRewrite(node, retNode, "str-conv-idem"); + } + else if (node[0].getKind() == STRING_ITOS) + { + // tolower( str.from.int( x ) ) --> str.from.int( x ) + return returnRewrite(node, node[0], "str-conv-itos"); + } + return node; +} + +Node StringsRewriter::rewriteStringLeq(Node n) +{ + Assert(n.getKind() == kind::STRING_LEQ); + NodeManager* nm = NodeManager::currentNM(); + if (n[0] == n[1]) + { + Node ret = nm->mkConst(true); + return returnRewrite(n, ret, "str-leq-id"); + } + if (n[0].isConst() && n[1].isConst()) + { + String s = n[0].getConst<String>(); + String t = n[1].getConst<String>(); + Node ret = nm->mkConst(s.isLeq(t)); + return returnRewrite(n, ret, "str-leq-eval"); + } + // empty strings + for (unsigned i = 0; i < 2; i++) + { + if (n[i].isConst() && n[i].getConst<String>().isEmptyString()) + { + Node ret = i == 0 ? nm->mkConst(true) : n[0].eqNode(n[1]); + return returnRewrite(n, ret, "str-leq-empty"); + } + } + + std::vector<Node> n1; + utils::getConcat(n[0], n1); + std::vector<Node> n2; + utils::getConcat(n[1], n2); + Assert(!n1.empty() && !n2.empty()); + + // constant prefixes + if (n1[0].isConst() && n2[0].isConst() && n1[0] != n2[0]) + { + String s = n1[0].getConst<String>(); + String t = n2[0].getConst<String>(); + // only need to truncate if s is longer + if (s.size() > t.size()) + { + s = s.prefix(t.size()); + } + // if prefix is not leq, then entire string is not leq + if (!s.isLeq(t)) + { + Node ret = nm->mkConst(false); + return returnRewrite(n, ret, "str-leq-cprefix"); + } + } + return n; +} + +Node StringsRewriter::rewriteStringFromCode(Node n) +{ + Assert(n.getKind() == kind::STRING_FROM_CODE); + NodeManager* nm = NodeManager::currentNM(); + + if (n[0].isConst()) + { + Integer i = n[0].getConst<Rational>().getNumerator(); + Node ret; + if (i >= 0 && i < strings::utils::getAlphabetCardinality()) + { + std::vector<unsigned> svec = {i.toUnsignedInt()}; + ret = nm->mkConst(String(svec)); + } + else + { + ret = nm->mkConst(String("")); + } + return returnRewrite(n, ret, "from-code-eval"); + } + return n; +} + +Node StringsRewriter::rewriteStringToCode(Node n) +{ + Assert(n.getKind() == kind::STRING_TO_CODE); + if (n[0].isConst()) + { + NodeManager* nm = NodeManager::currentNM(); + String s = n[0].getConst<String>(); + Node ret; + if (s.size() == 1) + { + std::vector<unsigned> vec = s.getVec(); + Assert(vec.size() == 1); + ret = nm->mkConst(Rational(String::convertUnsignedIntToCode(vec[0]))); + } + else + { + ret = nm->mkConst(Rational(-1)); + } + return returnRewrite(n, ret, "to-code-eval"); + } + return n; +} + +} // namespace strings +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/strings/strings_rewriter.h b/src/theory/strings/strings_rewriter.h new file mode 100644 index 000000000..e6a6b0693 --- /dev/null +++ b/src/theory/strings/strings_rewriter.h @@ -0,0 +1,88 @@ +/********************* */ +/*! \file strings_rewriter.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Andres Noetzli, Tianyi Liang + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Rewrite rules for string-specific operators in theory of strings + ** + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__STRINGS__STRINGS_REWRITER_H +#define CVC4__THEORY__STRINGS__STRINGS_REWRITER_H + +#include "expr/node.h" +#include "theory/strings/sequences_rewriter.h" + +namespace CVC4 { +namespace theory { +namespace strings { + +/** + * An extension of SequencesRewriter that handles operators that + * are specific to strings (and cannot be applied to sequences). + */ +class StringsRewriter : public SequencesRewriter +{ + public: + /** rewrite string to integer + * + * This is the entry point for post-rewriting terms n of the form + * str.to_int( s ) + * Returns the rewritten form of n. + */ + static Node rewriteStrToInt(Node n); + + /** rewrite integer to string + * + * This is the entry point for post-rewriting terms n of the form + * str.from_int( i ) + * Returns the rewritten form of n. + */ + static Node rewriteIntToStr(Node n); + + /** rewrite string convert + * + * This is the entry point for post-rewriting terms n of the form + * str.tolower( s ) and str.toupper( s ) + * Returns the rewritten form of n. + */ + static Node rewriteStrConvert(Node n); + + /** rewrite string less than or equal + * + * This is the entry point for post-rewriting terms n of the form + * str.<=( t, s ) + * Returns the rewritten form of n. + */ + static Node rewriteStringLeq(Node n); + + /** rewrite str.from_code + * + * This is the entry point for post-rewriting terms n of the form + * str.from_code( t ) + * Returns the rewritten form of n. + */ + static Node rewriteStringFromCode(Node n); + + /** rewrite str.to_code + * + * This is the entry point for post-rewriting terms n of the form + * str.to_code( t ) + * Returns the rewritten form of n. + */ + static Node rewriteStringToCode(Node n); +}; + +} // namespace strings +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__STRINGS__STRINGS_REWRITER_H */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index c0dc561f6..e6e0f8557 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -26,7 +26,6 @@ #include "smt/smt_statistics_registry.h" #include "theory/ext_theory.h" #include "theory/rewriter.h" -#include "theory/strings/theory_strings_rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/type_enumerator.h" #include "theory/strings/word.h" diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index a4b0a6705..d4183700d 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -22,7 +22,7 @@ #include "options/strings_options.h" #include "proof/proof_manager.h" #include "smt/logic_exception.h" -#include "theory/strings/theory_strings_rewriter.h" +#include "theory/strings/sequences_rewriter.h" using namespace CVC4; using namespace CVC4::kind; @@ -71,7 +71,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node sk1 = n == d_zero ? d_empty_str : d_sc->mkSkolemCached( s, n, SkolemCache::SK_PREFIX, "sspre"); - Node sk2 = TheoryStringsRewriter::checkEntailArith(t12, lt0) + Node sk2 = SequencesRewriter::checkEntailArith(t12, lt0) ? d_empty_str : d_sc->mkSkolemCached( s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr"); diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 35f2f7bfa..d6a6b701c 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -2,6 +2,7 @@ cvc4_add_unit_test_black(regexp_operation_black theory) cvc4_add_unit_test_black(theory_black theory) cvc4_add_unit_test_white(evaluator_white theory) cvc4_add_unit_test_white(logic_info_white theory) +cvc4_add_unit_test_white(sequences_rewriter_white theory) cvc4_add_unit_test_white(theory_arith_white theory) cvc4_add_unit_test_white(theory_bv_rewriter_white theory) cvc4_add_unit_test_white(theory_bv_white theory) @@ -9,7 +10,6 @@ cvc4_add_unit_test_white(theory_engine_white theory) cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory) cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white theory) cvc4_add_unit_test_white(theory_sets_type_enumerator_white theory) -cvc4_add_unit_test_white(theory_strings_rewriter_white theory) cvc4_add_unit_test_white(theory_strings_skolem_cache_black theory) cvc4_add_unit_test_white(theory_strings_word_white theory) cvc4_add_unit_test_white(theory_white theory) diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/sequences_rewriter_white.h index af8b24a0b..200a36d0b 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/sequences_rewriter_white.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file theory_strings_rewriter_white.h +/*! \file sequences_rewriter_white.h ** \verbatim ** Top contributors (to current version): ** Andres Noetzli @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Unit tests for the strings rewriter + ** \brief Unit tests for the strings/sequences rewriter ** - ** Unit tests for the strings rewriter. + ** Unit tests for the strings/sequences rewriter. **/ #include "expr/node.h" @@ -20,7 +20,7 @@ #include "smt/smt_engine_scope.h" #include "theory/quantifiers/extended_rewrite.h" #include "theory/rewriter.h" -#include "theory/strings/theory_strings_rewriter.h" +#include "theory/strings/sequences_rewriter.h" #include <cxxtest/TestSuite.h> #include <iostream> @@ -33,10 +33,10 @@ using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::strings; -class TheoryStringsRewriterWhite : public CxxTest::TestSuite +class SequencesRewriterWhite : public CxxTest::TestSuite { public: - TheoryStringsRewriterWhite() {} + SequencesRewriterWhite() {} void setUp() override { @@ -107,23 +107,23 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node three = d_nm->mkConst(Rational(3)); Node i = d_nm->mkVar("i", intType); - TS_ASSERT(TheoryStringsRewriter::checkEntailLengthOne(a)); - TS_ASSERT(TheoryStringsRewriter::checkEntailLengthOne(a, true)); + TS_ASSERT(SequencesRewriter::checkEntailLengthOne(a)); + TS_ASSERT(SequencesRewriter::checkEntailLengthOne(a, true)); Node substr = d_nm->mkNode(kind::STRING_SUBSTR, x, zero, one); - TS_ASSERT(TheoryStringsRewriter::checkEntailLengthOne(substr)); - TS_ASSERT(!TheoryStringsRewriter::checkEntailLengthOne(substr, true)); + TS_ASSERT(SequencesRewriter::checkEntailLengthOne(substr)); + TS_ASSERT(!SequencesRewriter::checkEntailLengthOne(substr, true)); substr = d_nm->mkNode(kind::STRING_SUBSTR, d_nm->mkNode(kind::STRING_CONCAT, a, x), zero, one); - TS_ASSERT(TheoryStringsRewriter::checkEntailLengthOne(substr)); - TS_ASSERT(TheoryStringsRewriter::checkEntailLengthOne(substr, true)); + TS_ASSERT(SequencesRewriter::checkEntailLengthOne(substr)); + TS_ASSERT(SequencesRewriter::checkEntailLengthOne(substr, true)); substr = d_nm->mkNode(kind::STRING_SUBSTR, x, zero, two); - TS_ASSERT(!TheoryStringsRewriter::checkEntailLengthOne(substr)); - TS_ASSERT(!TheoryStringsRewriter::checkEntailLengthOne(substr, true)); + TS_ASSERT(!SequencesRewriter::checkEntailLengthOne(substr)); + TS_ASSERT(!SequencesRewriter::checkEntailLengthOne(substr, true)); } void testCheckEntailArith() @@ -138,10 +138,10 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite // 1 >= (str.len (str.substr z n 1)) ---> true Node substr_z = d_nm->mkNode(kind::STRING_LENGTH, d_nm->mkNode(kind::STRING_SUBSTR, z, n, one)); - TS_ASSERT(TheoryStringsRewriter::checkEntailArith(one, substr_z)); + TS_ASSERT(SequencesRewriter::checkEntailArith(one, substr_z)); // (str.len (str.substr z n 1)) >= 1 ---> false - TS_ASSERT(!TheoryStringsRewriter::checkEntailArith(substr_z, one)); + TS_ASSERT(!SequencesRewriter::checkEntailArith(substr_z, one)); } void testCheckEntailArithWithAssumption() @@ -165,25 +165,25 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Rewriter::rewrite(d_nm->mkNode(kind::EQUAL, x_plus_slen_y, zero)); // x + (str.len y) = 0 |= 0 >= x --> true - TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption( + TS_ASSERT(SequencesRewriter::checkEntailArithWithAssumption( x_plus_slen_y_eq_zero, zero, x, false)); // x + (str.len y) = 0 |= 0 > x --> false - TS_ASSERT(!TheoryStringsRewriter::checkEntailArithWithAssumption( + TS_ASSERT(!SequencesRewriter::checkEntailArithWithAssumption( x_plus_slen_y_eq_zero, zero, x, true)); Node x_plus_slen_y_plus_z_eq_zero = Rewriter::rewrite(d_nm->mkNode( kind::EQUAL, d_nm->mkNode(kind::PLUS, x_plus_slen_y, z), zero)); // x + (str.len y) + z = 0 |= 0 > x --> false - TS_ASSERT(!TheoryStringsRewriter::checkEntailArithWithAssumption( + TS_ASSERT(!SequencesRewriter::checkEntailArithWithAssumption( x_plus_slen_y_plus_z_eq_zero, zero, x, true)); Node x_plus_slen_y_plus_slen_y_eq_zero = Rewriter::rewrite(d_nm->mkNode( kind::EQUAL, d_nm->mkNode(kind::PLUS, x_plus_slen_y, slen_y), zero)); // x + (str.len y) + (str.len y) = 0 |= 0 >= x --> true - TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption( + TS_ASSERT(SequencesRewriter::checkEntailArithWithAssumption( x_plus_slen_y_plus_slen_y_eq_zero, zero, x, false)); Node five = d_nm->mkConst(Rational(5)); @@ -193,11 +193,11 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Rewriter::rewrite(d_nm->mkNode(kind::LT, x_plus_five, six)); // x + 5 < 6 |= 0 >= x --> true - TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption( + TS_ASSERT(SequencesRewriter::checkEntailArithWithAssumption( x_plus_five_lt_six, zero, x, false)); // x + 5 < 6 |= 0 > x --> false - TS_ASSERT(!TheoryStringsRewriter::checkEntailArithWithAssumption( + TS_ASSERT(!SequencesRewriter::checkEntailArithWithAssumption( x_plus_five_lt_six, zero, x, true)); Node neg_x = d_nm->mkNode(kind::UMINUS, x); @@ -205,16 +205,16 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Rewriter::rewrite(d_nm->mkNode(kind::LT, x_plus_five, five)); // x + 5 < 5 |= -x >= 0 --> true - TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption( + TS_ASSERT(SequencesRewriter::checkEntailArithWithAssumption( x_plus_five_lt_five, neg_x, zero, false)); // x + 5 < 5 |= 0 > x --> true - TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption( + TS_ASSERT(SequencesRewriter::checkEntailArithWithAssumption( x_plus_five_lt_five, zero, x, false)); // 0 < x |= x >= (str.len (int.to.str x)) Node assm = Rewriter::rewrite(d_nm->mkNode(kind::LT, zero, x)); - TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption( + TS_ASSERT(SequencesRewriter::checkEntailArithWithAssumption( assm, x, d_nm->mkNode(kind::STRING_LENGTH, d_nm->mkNode(kind::STRING_ITOS, x)), @@ -243,7 +243,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite // (str.substr "A" x x) --> "" Node n = d_nm->mkNode(kind::STRING_SUBSTR, a, x, x); - Node res = TheoryStringsRewriter::rewriteSubstr(n); + Node res = SequencesRewriter::rewriteSubstr(n); TS_ASSERT_EQUALS(res, empty); // (str.substr "A" (+ x 1) x) -> "" @@ -251,7 +251,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite a, d_nm->mkNode(kind::PLUS, x, d_nm->mkConst(Rational(1))), x); - res = TheoryStringsRewriter::rewriteSubstr(n); + res = SequencesRewriter::rewriteSubstr(n); TS_ASSERT_EQUALS(res, empty); // (str.substr "A" (+ x (str.len s2)) x) -> "" @@ -260,24 +260,24 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite a, d_nm->mkNode(kind::PLUS, x, d_nm->mkNode(kind::STRING_LENGTH, s)), x); - res = TheoryStringsRewriter::rewriteSubstr(n); + res = SequencesRewriter::rewriteSubstr(n); TS_ASSERT_EQUALS(res, empty); // (str.substr "A" x y) -> (str.substr "A" x y) n = d_nm->mkNode(kind::STRING_SUBSTR, a, x, y); - res = TheoryStringsRewriter::rewriteSubstr(n); + res = SequencesRewriter::rewriteSubstr(n); TS_ASSERT_EQUALS(res, n); // (str.substr "ABCD" (+ x 3) x) -> "" n = d_nm->mkNode( kind::STRING_SUBSTR, abcd, d_nm->mkNode(kind::PLUS, x, three), x); - res = TheoryStringsRewriter::rewriteSubstr(n); + res = SequencesRewriter::rewriteSubstr(n); TS_ASSERT_EQUALS(res, empty); // (str.substr "ABCD" (+ x 2) x) -> (str.substr "ABCD" (+ x 2) x) n = d_nm->mkNode( kind::STRING_SUBSTR, abcd, d_nm->mkNode(kind::PLUS, x, two), x); - res = TheoryStringsRewriter::rewriteSubstr(n); + res = SequencesRewriter::rewriteSubstr(n); TS_ASSERT_EQUALS(res, n); // (str.substr (str.substr s x x) x x) -> "" @@ -440,8 +440,8 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite x, d_nm->mkNode(kind::STRING_STRREPL, x, gh, ij), ij); - Node res_concat1 = TheoryStringsRewriter::lengthPreserveRewrite(concat1); - Node res_concat2 = TheoryStringsRewriter::lengthPreserveRewrite(concat2); + Node res_concat1 = SequencesRewriter::lengthPreserveRewrite(concat1); + Node res_concat2 = SequencesRewriter::lengthPreserveRewrite(concat2); TS_ASSERT_EQUALS(res_concat1, res_concat2); } @@ -1049,32 +1049,32 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node empty_x_y = d_nm->mkNode(kind::AND, d_nm->mkNode(kind::EQUAL, empty, x), d_nm->mkNode(kind::EQUAL, empty, y)); - sameNormalForm(TheoryStringsRewriter::inferEqsFromContains(empty, xy), + sameNormalForm(SequencesRewriter::inferEqsFromContains(empty, xy), empty_x_y); // inferEqsFromContains(x, (str.++ x y)) returns false Node bxya = d_nm->mkNode(kind::STRING_CONCAT, b, y, x, a); - sameNormalForm(TheoryStringsRewriter::inferEqsFromContains(x, bxya), f); + sameNormalForm(SequencesRewriter::inferEqsFromContains(x, bxya), f); // inferEqsFromContains(x, y) returns null - Node n = TheoryStringsRewriter::inferEqsFromContains(x, y); + Node n = SequencesRewriter::inferEqsFromContains(x, y); TS_ASSERT(n.isNull()); // inferEqsFromContains(x, x) returns something equivalent to (= x x) Node eq_x_x = d_nm->mkNode(kind::EQUAL, x, x); - sameNormalForm(TheoryStringsRewriter::inferEqsFromContains(x, x), eq_x_x); + sameNormalForm(SequencesRewriter::inferEqsFromContains(x, x), eq_x_x); // inferEqsFromContains((str.replace x "B" "A"), x) returns something // equivalent to (= (str.replace x "B" "A") x) Node repl = d_nm->mkNode(kind::STRING_STRREPL, x, b, a); Node eq_repl_x = d_nm->mkNode(kind::EQUAL, repl, x); - sameNormalForm(TheoryStringsRewriter::inferEqsFromContains(repl, x), + sameNormalForm(SequencesRewriter::inferEqsFromContains(repl, x), eq_repl_x); // inferEqsFromContains(x, (str.replace x "B" "A")) returns something // equivalent to (= (str.replace x "B" "A") x) Node eq_x_repl = d_nm->mkNode(kind::EQUAL, x, repl); - sameNormalForm(TheoryStringsRewriter::inferEqsFromContains(x, repl), + sameNormalForm(SequencesRewriter::inferEqsFromContains(x, repl), eq_x_repl); } @@ -1402,7 +1402,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite std::vector<Node> nb; std::vector<Node> ne; bool res = - TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, 0); + SequencesRewriter::stripConstantEndpoints(n1, n2, nb, ne, 0); TS_ASSERT(!res); } @@ -1414,7 +1414,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite std::vector<Node> nb; std::vector<Node> ne; bool res = - TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, 0); + SequencesRewriter::stripConstantEndpoints(n1, n2, nb, ne, 0); TS_ASSERT(!res); } @@ -1430,7 +1430,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite std::vector<Node> n1r = {cd}; std::vector<Node> nbr = {ab}; bool res = - TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, 1); + SequencesRewriter::stripConstantEndpoints(n1, n2, nb, ne, 1); TS_ASSERT(res); TS_ASSERT_EQUALS(n1, n1r); TS_ASSERT_EQUALS(nb, nbr); @@ -1448,7 +1448,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite std::vector<Node> n1r = {c, x}; std::vector<Node> nbr = {ab}; bool res = - TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, 1); + SequencesRewriter::stripConstantEndpoints(n1, n2, nb, ne, 1); TS_ASSERT(res); TS_ASSERT_EQUALS(n1, n1r); TS_ASSERT_EQUALS(nb, nbr); @@ -1466,7 +1466,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite std::vector<Node> n1r = {a}; std::vector<Node> ner = {bc}; bool res = - TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, -1); + SequencesRewriter::stripConstantEndpoints(n1, n2, nb, ne, -1); TS_ASSERT(res); TS_ASSERT_EQUALS(n1, n1r); TS_ASSERT_EQUALS(ne, ner); @@ -1484,7 +1484,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite std::vector<Node> n1r = {x, a}; std::vector<Node> ner = {bc}; bool res = - TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, -1); + SequencesRewriter::stripConstantEndpoints(n1, n2, nb, ne, -1); TS_ASSERT(res); TS_ASSERT_EQUALS(n1, n1r); TS_ASSERT_EQUALS(ne, ner); |