diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-11 03:21:06 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-11 09:21:06 +0000 |
| commit | 71e843a8e9e88fc739aaa5a4a5d608004648fafa (patch) | |
| tree | 6f18912dfcb230139bbb6bdb68b38400d23d7eff /src/theory/strings | |
| parent | 223155cfb300458f534f4be6b88e5fdc17b0ff14 (diff) | |
(proof-new) Clean up uses of witness with skolem lemmas (#6109)
This ensures we do not return WITNESS terms in response to ppRewrite. This makes standard utility methods in SkolemLemma to help make this easy.
It also removes TheorySetsPrivate::expandDefinitions, which was returning WITNESS in response to expandDefinitions, which is no longer permitted.
Diffstat (limited to 'src/theory/strings')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 7f838e411..fbede89f0 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -998,15 +998,13 @@ TrustNode TheoryStrings::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems) 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 v = nm->mkBoundVar(nm->stringType()); Node emp = Word::mkEmptyWord(atom.getType()); - // TODO: use skolem manager - Node ret = nm->mkNode( - WITNESS, - bvl, - nm->mkNode( - ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, k)), k.eqNode(emp))); + Node pred = nm->mkNode( + ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, v)), v.eqNode(emp)); + SkolemManager* sm = nm->getSkolemManager(); + Node ret = sm->mkSkolem(v, pred, "kFromCode"); + lems.push_back(SkolemLemma(ret, nullptr)); return TrustNode::mkTrustRewrite(atom, ret, nullptr); } TrustNode ret; |