diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 34 |
1 files changed, 27 insertions, 7 deletions
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 ) |