summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/evaluator.cpp18
-rw-r--r--src/theory/strings/extf_solver.cpp4
-rw-r--r--src/theory/strings/kinds6
-rw-r--r--src/theory/strings/solver_state.cpp2
-rw-r--r--src/theory/strings/theory_strings.cpp34
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp18
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp45
-rw-r--r--src/theory/strings/theory_strings_rewriter.h14
8 files changed, 107 insertions, 34 deletions
diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index a3ea768d4..b827912d5 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -18,6 +18,7 @@
#include "theory/bv/theory_bv_utils.h"
#include "theory/rewriter.h"
+#include "theory/strings/theory_strings_utils.h"
#include "theory/theory.h"
#include "util/integer.h"
@@ -605,7 +606,22 @@ EvalResult Evaluator::evalInternal(
break;
}
- case kind::STRING_CODE:
+ case kind::STRING_FROM_CODE:
+ {
+ Integer i = results[currNode[0]].d_rat.getNumerator();
+ if (i >= 0 && i < strings::utils::getAlphabetCardinality())
+ {
+ std::vector<unsigned> svec = {i.toUnsignedInt()};
+ results[currNode] = EvalResult(String(svec));
+ }
+ else
+ {
+ results[currNode] = EvalResult(String(""));
+ }
+ break;
+ }
+
+ case kind::STRING_TO_CODE:
{
const String& s = results[currNode[0]].d_str;
if (s.size() == 1)
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 6ab74cf9a..b04b88b31 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -54,7 +54,7 @@ ExtfSolver::ExtfSolver(context::Context* c,
d_extt->addFunctionKind(kind::STRING_STRCTN);
d_extt->addFunctionKind(kind::STRING_IN_REGEXP);
d_extt->addFunctionKind(kind::STRING_LEQ);
- d_extt->addFunctionKind(kind::STRING_CODE);
+ d_extt->addFunctionKind(kind::STRING_TO_CODE);
d_extt->addFunctionKind(kind::STRING_TOLOWER);
d_extt->addFunctionKind(kind::STRING_TOUPPER);
d_extt->addFunctionKind(kind::STRING_REV);
@@ -166,7 +166,7 @@ bool ExtfSolver::doReduction(int effort, Node n, bool& isCd)
// context-dependent because it depends on the polarity of n itself
isCd = true;
}
- else if (k != kind::STRING_CODE)
+ else if (k != kind::STRING_TO_CODE)
{
NodeManager* nm = NodeManager::currentNM();
Assert(k == STRING_SUBSTR || k == STRING_STRCTN || k == STRING_STRIDOF
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 965c56ee4..9d12cd906 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -28,7 +28,8 @@ operator STRING_SUFFIX 2 "string suffixof"
operator STRING_IS_DIGIT 1 "string isdigit, returns true if argument is a string of length one that represents a digit"
operator STRING_ITOS 1 "integer to string"
operator STRING_STOI 1 "string to integer (total function)"
-operator STRING_CODE 1 "string to code, returns the code of the first character of the string if it has length one, -1 otherwise"
+operator STRING_TO_CODE 1 "string to code, returns the code of the first character of the string if it has length one, -1 otherwise"
+operator STRING_FROM_CODE 1 "string from code, returns a string containing a single character whose code point matches the argument to this function, empty string if the argument is out-of-bounds"
operator STRING_TOLOWER 1 "string to lowercase conversion"
operator STRING_TOUPPER 1 "string to uppercase conversion"
operator STRING_REV 1 "string reverse"
@@ -108,7 +109,8 @@ typerule STRING_SUFFIX "SimpleTypeRule<RBool, AString, AString>"
typerule STRING_IS_DIGIT "SimpleTypeRule<RBool, AString>"
typerule STRING_ITOS "SimpleTypeRule<RString, AInteger>"
typerule STRING_STOI "SimpleTypeRule<RInteger, AString>"
-typerule STRING_CODE "SimpleTypeRule<RInteger, AString>"
+typerule STRING_TO_CODE "SimpleTypeRule<RInteger, AString>"
+typerule STRING_FROM_CODE "SimpleTypeRule<RString, AInteger>"
typerule STRING_TOUPPER "SimpleTypeRule<RString, AString>"
typerule STRING_TOLOWER "SimpleTypeRule<RString, AString>"
typerule STRING_REV "SimpleTypeRule<RString, AString>"
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 422c9e58b..2b903a8da 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -95,7 +95,7 @@ const context::CDList<Node>& SolverState::getDisequalityList() const
void SolverState::eqNotifyNewClass(TNode t)
{
Kind k = t.getKind();
- if (k == STRING_LENGTH || k == STRING_CODE)
+ if (k == STRING_LENGTH || k == STRING_TO_CODE)
{
Node r = d_ee.getRepresentative(t[0]);
EqcInfo* ei = getOrMakeEqcInfo(r);
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index cd1d0cd67..2fbf16552 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -93,7 +93,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
- d_equalityEngine.addFunctionKind(kind::STRING_CODE);
+ d_equalityEngine.addFunctionKind(kind::STRING_TO_CODE);
// extended functions
d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
@@ -351,7 +351,7 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
if (eip && !eip->d_codeTerm.get().isNull())
{
// its value must be equal to its code
- Node ct = nm->mkNode(kind::STRING_CODE, eip->d_codeTerm.get());
+ Node ct = nm->mkNode(kind::STRING_TO_CODE, eip->d_codeTerm.get());
Node ctv = d_valuation.getModelValue(ct);
unsigned cvalue =
ctv.getConst<Rational>().getNumerator().toUnsignedInt();
@@ -600,6 +600,26 @@ void TheoryStrings::preRegisterTerm(TNode n) {
Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) {
Trace("strings-exp-def") << "TheoryStrings::expandDefinition : " << node << std::endl;
+
+ if (node.getKind() == STRING_FROM_CODE)
+ {
+ // str.from_code(t) --->
+ // choice k. ite(0 <= t < |A|, t = str.to_code(k), k = "")
+ NodeManager* nm = NodeManager::currentNM();
+ Node t = node[0];
+ Node card = nm->mkConst(Rational(utils::getAlphabetCardinality()));
+ Node cond =
+ nm->mkNode(AND, nm->mkNode(LEQ, d_zero, t), nm->mkNode(LT, t, card));
+ Node k = nm->mkBoundVar(nm->stringType());
+ Node bvl = nm->mkNode(BOUND_VAR_LIST, k);
+ node = nm->mkNode(CHOICE,
+ bvl,
+ nm->mkNode(ITE,
+ cond,
+ t.eqNode(nm->mkNode(STRING_TO_CODE, k)),
+ k.eqNode(d_emptyString)));
+ }
+
return node;
}
@@ -734,7 +754,7 @@ void TheoryStrings::conflict(TNode a, TNode b){
void TheoryStrings::eqNotifyNewClass(TNode t){
Kind k = t.getKind();
- if (k == STRING_LENGTH || k == STRING_CODE)
+ if (k == STRING_LENGTH || k == STRING_TO_CODE)
{
Trace("strings-debug") << "New length eqc : " << t << std::endl;
//we care about the length of this string
@@ -940,12 +960,12 @@ void TheoryStrings::checkCodes()
Node c = nfe.d_nf[0];
Trace("strings-code-debug") << "Get proxy variable for " << c
<< std::endl;
- Node cc = nm->mkNode(kind::STRING_CODE, c);
+ Node cc = nm->mkNode(kind::STRING_TO_CODE, c);
cc = Rewriter::rewrite(cc);
Assert(cc.isConst());
Node cp = d_im.getProxyVariableFor(c);
AlwaysAssert(!cp.isNull());
- Node vc = nm->mkNode(STRING_CODE, cp);
+ Node vc = nm->mkNode(STRING_TO_CODE, cp);
if (!d_state.areEqual(cc, vc))
{
d_im.sendInference(d_empty_vec, cc.eqNode(vc), "Code_Proxy");
@@ -957,7 +977,7 @@ void TheoryStrings::checkCodes()
EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false);
if (ei && !ei->d_codeTerm.get().isNull())
{
- Node vc = nm->mkNode(kind::STRING_CODE, ei->d_codeTerm.get());
+ Node vc = nm->mkNode(kind::STRING_TO_CODE, ei->d_codeTerm.get());
nconst_codes.push_back(vc);
}
}
@@ -1027,7 +1047,7 @@ void TheoryStrings::registerTerm(Node n, int effort)
// for concat/const/replace, introduce proxy var and state length relation
d_im.registerLength(n);
}
- else if (n.getKind() == STRING_CODE)
+ 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 )
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 6272ad129..a4b0a6705 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -217,8 +217,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
Node sx = nm->mkNode(STRING_SUBSTR, itost, x, d_one);
Node ux = nm->mkNode(APPLY_UF, u, x);
Node ux1 = nm->mkNode(APPLY_UF, u, xPlusOne);
- Node c0 = nm->mkNode(STRING_CODE, nm->mkConst(String("0")));
- Node c = nm->mkNode(MINUS, nm->mkNode(STRING_CODE, sx), c0);
+ Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0")));
+ Node c = nm->mkNode(MINUS, nm->mkNode(STRING_TO_CODE, sx), c0);
Node ten = nm->mkConst(Rational(10));
Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux)));
@@ -279,10 +279,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
Node k = nm->mkSkolem("k", nm->integerType());
Node kc1 = nm->mkNode(GEQ, k, d_zero);
Node kc2 = nm->mkNode(LT, k, lens);
- Node c0 = nm->mkNode(STRING_CODE, nm->mkConst(String("0")));
+ Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0")));
Node codeSk = nm->mkNode(
MINUS,
- nm->mkNode(STRING_CODE, nm->mkNode(STRING_SUBSTR, s, k, d_one)),
+ nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, s, k, d_one)),
c0);
Node ten = nm->mkConst(Rational(10));
Node kc3 = nm->mkNode(
@@ -310,7 +310,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
Node sx = nm->mkNode(STRING_SUBSTR, s, x, d_one);
Node ux = nm->mkNode(APPLY_UF, u, x);
Node ux1 = nm->mkNode(APPLY_UF, u, nm->mkNode(PLUS, x, d_one));
- Node c = nm->mkNode(MINUS, nm->mkNode(STRING_CODE, sx), c0);
+ Node c = nm->mkNode(MINUS, nm->mkNode(STRING_TO_CODE, sx), c0);
Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux)));
Node cb =
@@ -495,8 +495,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
Node i = nm->mkBoundVar(nm->integerType());
Node bvi = nm->mkNode(BOUND_VAR_LIST, i);
- Node ci = nm->mkNode(STRING_CODE, nm->mkNode(STRING_SUBSTR, x, i, d_one));
- Node ri = nm->mkNode(STRING_CODE, nm->mkNode(STRING_SUBSTR, r, i, d_one));
+ Node ci =
+ nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, x, i, d_one));
+ Node ri =
+ nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, r, i, d_one));
Node lb = nm->mkConst(Rational(t.getKind() == STRING_TOUPPER ? 97 : 65));
Node ub = nm->mkConst(Rational(t.getKind() == STRING_TOUPPER ? 122 : 90));
@@ -589,7 +591,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
Node tb = t[1 - r];
substr[r] = nm->mkNode(STRING_SUBSTR, ta, d_zero, k);
code[r] =
- nm->mkNode(STRING_CODE, nm->mkNode(STRING_SUBSTR, ta, k, d_one));
+ nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, ta, k, d_one));
conj.push_back(nm->mkNode(LEQ, k, nm->mkNode(STRING_LENGTH, ta)));
}
conj.push_back(substr[0].eqNode(substr[1]));
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index d8bc7f34f..2c14d5343 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1478,10 +1478,11 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) {
else if (r.getKind() == REGEXP_RANGE)
{
// x in re.range( char_i, char_j ) ---> i <= str.code(x) <= j
- Node xcode = nm->mkNode(STRING_CODE, x);
- retNode = nm->mkNode(AND,
- nm->mkNode(LEQ, nm->mkNode(STRING_CODE, r[0]), xcode),
- nm->mkNode(LEQ, xcode, nm->mkNode(STRING_CODE, r[1])));
+ Node xcode = nm->mkNode(STRING_TO_CODE, x);
+ retNode =
+ nm->mkNode(AND,
+ nm->mkNode(LEQ, nm->mkNode(STRING_TO_CODE, r[0]), xcode),
+ nm->mkNode(LEQ, xcode, nm->mkNode(STRING_TO_CODE, r[1])));
}
else if (r.getKind() == REGEXP_COMPLEMENT)
{
@@ -1667,7 +1668,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
else if (nk == STRING_IS_DIGIT)
{
// eliminate str.is_digit(s) ----> 48 <= str.to_code(s) <= 57
- Node t = nm->mkNode(STRING_CODE, node[0]);
+ Node t = nm->mkNode(STRING_TO_CODE, node[0]);
retNode = nm->mkNode(AND,
nm->mkNode(LEQ, nm->mkConst(Rational(48)), t),
nm->mkNode(LEQ, t, nm->mkConst(Rational(57))));
@@ -1709,9 +1710,9 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
{
retNode = rewriteMembership(node);
}
- else if (nk == STRING_CODE)
+ else if (nk == STRING_TO_CODE)
{
- retNode = rewriteStringCode(node);
+ retNode = rewriteStringToCode(node);
}
else if (nk == REGEXP_CONCAT)
{
@@ -3410,9 +3411,33 @@ Node TheoryStringsRewriter::rewritePrefixSuffix(Node n)
return retNode;
}
-Node TheoryStringsRewriter::rewriteStringCode(Node n)
+Node TheoryStringsRewriter::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 TheoryStringsRewriter::rewriteStringToCode(Node n)
{
- Assert(n.getKind() == kind::STRING_CODE);
+ Assert(n.getKind() == kind::STRING_TO_CODE);
if (n[0].isConst())
{
CVC4::String s = n[0].getConst<String>();
@@ -3428,7 +3453,7 @@ Node TheoryStringsRewriter::rewriteStringCode(Node n)
{
ret = NodeManager::currentNM()->mkConst(Rational(-1));
}
- return returnRewrite(n, ret, "code-eval");
+ return returnRewrite(n, ret, "to-code-eval");
}
return n;
diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index c9733433c..4accfca39 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -249,12 +249,20 @@ class TheoryStringsRewriter : public TheoryRewriter
* Returns the rewritten form of node.
*/
static Node rewritePrefixSuffix(Node node);
- /** rewrite str.code
+
+ /** 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 node.
+ */
+ static Node rewriteStringFromCode(Node node);
+
+ /** rewrite str.to_code
* This is the entry point for post-rewriting terms n of the form
- * str.code( t )
+ * str.to_code( t )
* Returns the rewritten form of node.
*/
- static Node rewriteStringCode(Node node);
+ static Node rewriteStringToCode(Node node);
static Node splitConstant( Node a, Node b, int& index, bool isRev );
/** can constant contain list
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback