Expand definitions for sequences was wrong in two ways: (1) we replaced str.from_code with a witness term. This led to it being unevaluatable in models. (2) we did not handle seq.nth, meaning its model value was unevaluatable if it was out of bounds. Now it evaluates the value of the uninterpreted function we replace with.
This corrects both issues and adds a regression to demonstrate both kinds of terms evaluate correctly.
To do this, I added a helper function to skolem cache as well as a new (internal-only) kind SEQ_NTH_TOTAL. Notice applications of this kind should only be used for model evaluation.
Notice this fixes several check-model warnings in the regressions. It still does not fix others since other things must be corrected for model evaluation (e.g. expandDefinitions must be applied on theory assertions for --debug-check-models). This will be done in later PRs.
operator SEQ_UNIT 1 "a sequence of length one"
operator SEQ_NTH 2 "The nth element of a sequence"
+operator SEQ_NTH_TOTAL 2 "The nth element of a sequence (internal, for responses to expand definitions only)"
# equal equal / less than / output
operator STRING_TO_REGEXP 1 "convert string to regexp"
typerule CONST_SEQUENCE ::CVC4::theory::strings::ConstSequenceTypeRule
typerule SEQ_UNIT ::CVC4::theory::strings::SeqUnitTypeRule
typerule SEQ_NTH ::CVC4::theory::strings::SeqNthTypeRule
+typerule SEQ_NTH_TOTAL ::CVC4::theory::strings::SeqNthTypeRule
endtheory
case Rewrite::LEN_SEQ_UNIT: return "LEN_SEQ_UNIT";
case Rewrite::CHARAT_ELIM: return "CHARAT_ELIM";
case Rewrite::SEQ_UNIT_EVAL: return "SEQ_UNIT_EVAL";
- case Rewrite::SEQ_NTH_EVAL: return "SEQ_NTH_EVAL";
+ case Rewrite::SEQ_NTH_EVAL: return "SEQ_NTH_EVAL";
+ case Rewrite::SEQ_NTH_TOTAL_OOB: return "SEQ_NTH_TOTAL_OOB";
default: return "?";
}
}
LEN_SEQ_UNIT,
CHARAT_ELIM,
SEQ_UNIT_EVAL,
- SEQ_NTH_EVAL
+ SEQ_NTH_EVAL,
+ SEQ_NTH_TOTAL_OOB
};
/**
{
retNode = rewriteSeqUnit(node);
}
- else if (nk == SEQ_NTH)
+ else if (nk == SEQ_NTH || nk == SEQ_NTH_TOTAL)
{
retNode = rewriteSeqNth(node);
}
Node SequencesRewriter::rewriteSeqNth(Node node)
{
- Assert(node.getKind() == SEQ_NTH);
+ Assert(node.getKind() == SEQ_NTH || node.getKind() == SEQ_NTH_TOTAL);
Node ret;
Node s = node[0];
Node i = node[1];
ret = elements[pos];
return returnRewrite(node, ret, Rewrite::SEQ_NTH_EVAL);
}
+ else if (node.getKind() == SEQ_NTH_TOTAL)
+ {
+ // return arbitrary term
+ Node ret = s.getType().getSequenceElementType().mkGroundValue();
+ return returnRewrite(node, ret, Rewrite::SEQ_NTH_TOTAL_OOB);
+ }
else
{
return node;
return mkTypedSkolemCached(tn, a, Node::null(), id, c);
}
+Node SkolemCache::mkSkolemSeqNth(TypeNode seqType, const char* c)
+{
+ Assert(seqType.isSequence());
+ NodeManager* nm = NodeManager::currentNM();
+ std::vector<TypeNode> argTypes;
+ argTypes.push_back(seqType);
+ argTypes.push_back(nm->integerType());
+ TypeNode elemType = seqType.getSequenceElementType();
+ TypeNode ufType = nm->mkFunctionType(argTypes, elemType);
+ return mkTypedSkolemCached(
+ ufType, Node::null(), Node::null(), SkolemCache::SK_NTH, c);
+}
+
Node SkolemCache::mkSkolem(const char* c)
{
// TODO: eliminate this
TypeNode tn, Node a, Node b, SkolemId id, const char* c);
/** Same as mkTypedSkolemCached above for (a,[null],id) */
Node mkTypedSkolemCached(TypeNode tn, Node a, SkolemId id, const char* c);
+ /**
+ * Specific version for seq.nth, used for cases where the index is out of
+ * range for sequence type seqType.
+ */
+ Node mkSkolemSeqNth(TypeNode seqType, const char* c);
/** Returns a (uncached) skolem of type string with name c */
Node mkSkolem(const char* c);
/** Returns true if n is a skolem allocated by this class */
{
Trace("strings-exp-def") << "TheoryStrings::expandDefinition : " << node << std::endl;
- if (node.getKind() == STRING_FROM_CODE)
+ if (node.getKind() == kind::SEQ_NTH)
{
- // str.from_code(t) --->
- // witness 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 emp = Word::mkEmptyWord(node.getType());
- Node ret = nm->mkNode(
- WITNESS,
- bvl,
- nm->mkNode(
- ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, k)), k.eqNode(emp)));
+ SkolemCache* sc = d_termReg.getSkolemCache();
+ Node s = node[0];
+ Node n = node[1];
+ // seq.nth(s, n) --> ite(0 <= n < len(s), seq.nth_total(s,n), Uf(s, n))
+ Node cond = nm->mkNode(AND,
+ nm->mkNode(LEQ, d_zero, n),
+ nm->mkNode(LT, n, nm->mkNode(STRING_LENGTH, s)));
+ Node ss = nm->mkNode(SEQ_NTH_TOTAL, s, n);
+ Node uf = sc->mkSkolemSeqNth(s.getType(), "Uf");
+ Node u = nm->mkNode(APPLY_UF, uf, s, n);
+ Node ret = nm->mkNode(ITE, cond, ss, u);
+ Trace("strings-exp-def") << "...return " << ret << std::endl;
return TrustNode::mkTrustRewrite(node, ret, nullptr);
}
return TrustNode::null();
TrustNode TheoryStrings::ppRewrite(TNode atom)
{
Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl;
- // first, see if we need to expand definitions
- TrustNode texp = expandDefinition(atom);
- if (!texp.isNull())
+ if (atom.getKind() == STRING_FROM_CODE)
{
- return texp;
+ // str.from_code(t) --->
+ // witness k. ite(0 <= t < |A|, t = str.to_code(k), k = "")
+ NodeManager* nm = NodeManager::currentNM();
+ Node t = atom[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 emp = Word::mkEmptyWord(atom.getType());
+ Node ret = nm->mkNode(
+ WITNESS,
+ bvl,
+ nm->mkNode(
+ ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, k)), k.eqNode(emp)));
+ return TrustNode::mkTrustRewrite(atom, ret, nullptr);
}
TrustNode ret;
Node atomRet = atom;
Node b1 = nm->mkNode(AND, b11, b12, b13);
// nodes for the case where `seq.nth` is undefined.
- std::vector<TypeNode> argTypes;
- argTypes.push_back(s.getType());
- argTypes.push_back(nm->integerType());
- TypeNode elemType = s.getType().getSequenceElementType();
- TypeNode ufType = nm->mkFunctionType(argTypes, elemType);
- Node uf = sc->mkTypedSkolemCached(
- ufType, Node::null(), Node::null(), SkolemCache::SK_NTH, "Uf");
+ Node uf = sc->mkSkolemSeqNth(s.getType(), "Uf");
Node b2 = nm->mkNode(EQUAL, skt, nm->mkNode(APPLY_UF, uf, s, n));
// the full ite, split on definedness of `seq.nth`
regress0/seq/seq-ex4.smt2
regress0/seq/seq-ex5-dd.smt2
regress0/seq/seq-ex5.smt2
+ regress0/seq/seq-expand-defs.smt2
regress0/seq/seq-nemp.smt2
regress0/seq/seq-nth.smt2
regress0/seq/seq-nth-uf.smt2
--- /dev/null
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+; EXPECT: (((seq.nth y 7) 404))
+; EXPECT: (((str.from_code x) "?"))
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-fun x () Int)
+(declare-fun y () (Seq Int))
+
+(assert (< (seq.len y) 5))
+
+(assert (= x 63))
+
+(assert (= (seq.nth y 7) 404))
+
+(check-sat)
+
+(get-value ((seq.nth y 7)))
+(get-value ((str.from_code x)))
-; COMMAND-LINE: --strings-exp -q
+; COMMAND-LINE: --strings-exp
;EXPECT: unsat
(set-logic ALL)
(declare-fun s () (Seq Int))
-; COMMAND-LINE: --strings-exp -q
+; COMMAND-LINE: --strings-exp
;EXPECT: unsat
(set-logic ALL)
(declare-fun s () (Seq Int))
projects / cvc5.git / commitdiff