diff options
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 10 | ||||
-rw-r--r-- | src/theory/strings/sequences_rewriter.cpp | 3 | ||||
-rw-r--r-- | src/theory/strings/strings_rewriter.cpp | 5 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 7 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_type_rules.h | 2 | ||||
-rw-r--r-- | src/theory/strings/type_enumerator.cpp | 40 | ||||
-rw-r--r-- | src/theory/strings/type_enumerator.h | 20 |
7 files changed, 68 insertions, 19 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index d5105a489..9a2091eac 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -739,9 +739,7 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset) } case kind::REGEXP_RANGE: { unsigned a = r[0].getConst<String>().front(); - a = String::convertUnsignedIntToCode(a); unsigned b = r[1].getConst<String>().front(); - b = String::convertUnsignedIntToCode(b); Assert(a < b); Assert(b < std::numeric_limits<unsigned>::max()); for (unsigned c = a; c <= b; c++) @@ -756,7 +754,6 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset) String s = st.getConst<String>(); if(s.size() != 0) { unsigned sc = s.front(); - sc = String::convertUnsignedIntToCode(sc); cset.insert(sc); } } @@ -765,7 +762,6 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset) if(st[0].isConst()) { String s = st[0].getConst<String>(); unsigned sc = s.front(); - sc = String::convertUnsignedIntToCode(sc); cset.insert(sc); } else { vset.insert( st[0] ); @@ -887,13 +883,11 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes case kind::REGEXP_RANGE: { std::vector< Node > vec; unsigned a = r[0].getConst<String>().front(); - a = String::convertUnsignedIntToCode(a); unsigned b = r[1].getConst<String>().front(); - b = String::convertUnsignedIntToCode(b); for (unsigned c = a; c <= b; c++) { std::vector<unsigned> tmpVec; - tmpVec.push_back(String::convertCodeToUnsignedInt(c)); + tmpVec.push_back(c); Node tmp = s.eqNode(nm->mkConst(String(tmpVec))).negate(); vec.push_back( tmp ); } @@ -1522,7 +1516,7 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > ++it) { std::vector<unsigned> cvec; - cvec.push_back(String::convertCodeToUnsignedInt(*it)); + cvec.push_back(*it); String c(cvec); Trace("regexp-int-debug") << "Try character " << c << " ... " << std::endl; Node r1l = derivativeSingle(r1, c); diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 716634d5f..b0940b7e1 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -1421,11 +1421,8 @@ bool SequencesRewriter::testConstStringInRegExp(CVC4::String& s, if (s.size() == index_start + 1) { unsigned a = r[0].getConst<String>().front(); - a = String::convertUnsignedIntToCode(a); unsigned b = r[1].getConst<String>().front(); - b = String::convertUnsignedIntToCode(b); unsigned c = s.back(); - c = String::convertUnsignedIntToCode(c); return (a <= c && c <= b); } else diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp index 75dfe7432..c7676d049 100644 --- a/src/theory/strings/strings_rewriter.cpp +++ b/src/theory/strings/strings_rewriter.cpp @@ -93,7 +93,7 @@ Node StringsRewriter::rewriteStrConvert(Node node) 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]); + unsigned newChar = nvec[i]; // transform it // upper 65 ... 90 // lower 97 ... 122 @@ -111,7 +111,6 @@ Node StringsRewriter::rewriteStrConvert(Node node) newChar = newChar + 32; } } - newChar = String::convertCodeToUnsignedInt(newChar); nvec[i] = newChar; } Node retNode = nm->mkConst(String(nvec)); @@ -231,7 +230,7 @@ Node StringsRewriter::rewriteStringToCode(Node n) { std::vector<unsigned> vec = s.getVec(); Assert(vec.size() == 1); - ret = nm->mkConst(Rational(String::convertUnsignedIntToCode(vec[0]))); + ret = nm->mkConst(Rational(vec[0])); } else { diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 16183abdd..a81c96318 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -382,7 +382,7 @@ bool TheoryStrings::collectModelInfoType( ctv.getConst<Rational>().getNumerator().toUnsignedInt(); Trace("strings-model") << "(code: " << cvalue << ") "; std::vector<unsigned> vec; - vec.push_back(String::convertCodeToUnsignedInt(cvalue)); + vec.push_back(cvalue); Node mv = nm->mkConst(String(vec)); pure_eq_assign[eqc] = mv; m->getEqualityEngine()->addTerm(mv); @@ -1099,13 +1099,14 @@ void TheoryStrings::registerTerm(Node n, int effort) else if (n.getKind() == STRING_TO_CODE) { d_has_str_code = true; - // ite( str.len(s)==1, 0 <= str.code(s) < num_codes, str.code(s)=-1 ) + // ite( str.len(s)==1, 0 <= str.code(s) < |A|, str.code(s)=-1 ) Node code_len = utils::mkNLength(n[0]).eqNode(d_one); Node code_eq_neg1 = n.eqNode(d_neg_one); Node code_range = nm->mkNode( AND, nm->mkNode(GEQ, n, d_zero), - nm->mkNode(LT, n, nm->mkConst(Rational(CVC4::String::num_codes())))); + nm->mkNode( + LT, n, nm->mkConst(Rational(utils::getAlphabetCardinality())))); regTermLem = nm->mkNode(ITE, code_len, code_range, code_eq_neg1); } else if (n.getKind() == STRING_STRIDOF) diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 7ef31a92a..93a32f26e 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -299,7 +299,7 @@ public: throw TypeCheckingExceptionPrivate(n, "expecting a single constant string term in regexp range"); } unsigned ci = (*it).getConst<String>().front(); - ch[i] = String::convertUnsignedIntToCode(ci); + ch[i] = ci; ++it; } if(ch[0] > ch[1]) { diff --git a/src/theory/strings/type_enumerator.cpp b/src/theory/strings/type_enumerator.cpp index 12cf899b4..7352ae5de 100644 --- a/src/theory/strings/type_enumerator.cpp +++ b/src/theory/strings/type_enumerator.cpp @@ -21,6 +21,44 @@ namespace CVC4 { namespace theory { namespace strings { +Node makeStandardModelConstant(const std::vector<unsigned>& vec, + uint32_t cardinality) +{ + std::vector<unsigned> mvec; + // if we contain all of the printable characters + if (cardinality >= 255) + { + for (unsigned i = 0, vsize = vec.size(); i < vsize; i++) + { + unsigned curr = vec[i]; + // convert + Assert(vec[i] < cardinality); + if (vec[i] <= 61) + { + // first 62 printable characters [\u{65}-\u{126}]: 'A', 'B', 'C', ... + curr = vec[i] + 65; + } + else if (vec[i] <= 94) + { + // remaining 33 printable characters [\u{32}-\u{64}]: ' ', '!', '"', ... + curr = vec[i] - 30; + } + else + { + // the remaining characters, starting with \u{127} and wrapping around + // the first 32 non-printable characters. + curr = (vec[i] + 32) % cardinality; + } + mvec.push_back(curr); + } + } + else + { + mvec = vec; + } + return NodeManager::currentNM()->mkConst(String(mvec)); +} + WordIter::WordIter(uint32_t startLength) : d_hasEndLength(false), d_endLength(0) { for (uint32_t i = 0; i < startLength; i++) @@ -117,7 +155,7 @@ bool StringEnumLen::increment() void StringEnumLen::mkCurr() { - d_curr = NodeManager::currentNM()->mkConst(String(d_witer->getData())); + d_curr = makeStandardModelConstant(d_witer->getData(), d_cardinality); } StringEnumerator::StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep) diff --git a/src/theory/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h index 2061628a5..b379ce5c3 100644 --- a/src/theory/strings/type_enumerator.h +++ b/src/theory/strings/type_enumerator.h @@ -28,6 +28,26 @@ namespace theory { namespace strings { /** + * Make standard model constant + * + * In our string representation, we represent characters using vectors + * of unsigned integers indicating code points for the characters of that + * string. + * + * To make models user-friendly, we make unsigned integer 0 correspond to the + * 65th character ("A") in the ASCII alphabet to make models intuitive. In + * particular, say if we have a set of string variables that are distinct but + * otherwise unconstrained, then the model may assign them "A", "B", "C", ... + * + * @param vec The code points of the string in a given model, + * @param cardinality The cardinality of the alphabet, + * @return A string whose characters have the code points corresponding + * to vec in the standard model construction described above. + */ +Node makeStandardModelConstant(const std::vector<unsigned>& vec, + uint32_t cardinality); + +/** * Generic iteration over vectors of indices of a given start/end length. */ class WordIter |