summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/evaluator.cpp3
-rw-r--r--src/theory/quantifiers/sygus_sampler.cpp3
-rw-r--r--src/theory/strings/regexp_operation.cpp10
-rw-r--r--src/theory/strings/sequences_rewriter.cpp3
-rw-r--r--src/theory/strings/strings_rewriter.cpp5
-rw-r--r--src/theory/strings/theory_strings.cpp7
-rw-r--r--src/theory/strings/theory_strings_type_rules.h2
-rw-r--r--src/theory/strings/type_enumerator.cpp40
-rw-r--r--src/theory/strings/type_enumerator.h20
9 files changed, 70 insertions, 23 deletions
diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index b827912d5..646f903f5 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -626,8 +626,7 @@ EvalResult Evaluator::evalInternal(
const String& s = results[currNode[0]].d_str;
if (s.size() == 1)
{
- results[currNode] = EvalResult(
- Rational(String::convertUnsignedIntToCode(s.getVec()[0])));
+ results[currNode] = EvalResult(Rational(s.getVec()[0]));
}
else
{
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 28cfa69df..e9c858814 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -560,8 +560,7 @@ Node SygusSampler::getRandomValue(TypeNode tn)
for (unsigned ch : alphas)
{
d_rstring_alphabet.push_back(ch);
- Trace("sygus-sample-str-alpha")
- << " \"" << String::convertUnsignedIntToChar(ch) << "\"";
+ Trace("sygus-sample-str-alpha") << " \\u" << ch;
}
Trace("sygus-sample-str-alpha") << std::endl;
}
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback