diff options
| author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-05-19 16:24:59 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-05-19 16:24:59 -0500 |
| commit | c8f149fa83fa16f821f37687fedfa778808809bd (patch) | |
| tree | 8808ec522b58c0d8273280923b984a72e0b7bb29 /src/theory/strings/theory_strings.cpp | |
| parent | 6bb98062a5578d126db6a3e8cdca083881893b32 (diff) | |
Renamed operator CHOICE to WITNESS (#4207)
Renamed operator CHOICE to WITNESS, and removed it from the front end
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 5b7c38361..b98bd1dea 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -580,7 +580,7 @@ Node TheoryStrings::expandDefinition(Node node) if (node.getKind() == STRING_FROM_CODE) { // str.from_code(t) ---> - // choice k. ite(0 <= t < |A|, t = str.to_code(k), k = "") + // 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())); @@ -590,7 +590,7 @@ Node TheoryStrings::expandDefinition(Node node) Node bvl = nm->mkNode(BOUND_VAR_LIST, k); Node emp = Word::mkEmptyWord(node.getType()); node = nm->mkNode( - CHOICE, + WITNESS, bvl, nm->mkNode( ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, k)), k.eqNode(emp))); |