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/expr | |
| 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/expr')
| -rw-r--r-- | src/expr/expr_manager_template.h | 4 | ||||
| -rw-r--r-- | src/expr/node.h | 2 | ||||
| -rw-r--r-- | src/expr/node_algorithm.h | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 0fd5bb4fa..16d66cf6a 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -523,7 +523,7 @@ private: /** * Create a new, fresh variable for use in a binder expression - * (the BOUND_VAR_LIST of a FORALL, EXISTS, LAMBDA, or CHOICE). It is + * (the BOUND_VAR_LIST of a FORALL, EXISTS, LAMBDA, or WITNESS). It is * an error for this bound variable to exist outside of a binder, * and it should also only be used in a single binder expression. * That is, two distinct FORALL expressions should use entirely @@ -542,7 +542,7 @@ private: /** * Create a (nameless) new, fresh variable for use in a binder - * expression (the BOUND_VAR_LIST of a FORALL, EXISTS, LAMBDA, or CHOICE). + * expression (the BOUND_VAR_LIST of a FORALL, EXISTS, LAMBDA, or WITNESS). * It is an error for this bound variable to exist outside of a * binder, and it should also only be used in a single binder * expression. That is, two distinct FORALL expressions should use diff --git a/src/expr/node.h b/src/expr/node.h index 8ded28f07..2f9d0b0ac 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -468,7 +468,7 @@ public: inline bool isClosure() const { assertTNodeNotExpired(); return getKind() == kind::LAMBDA || getKind() == kind::FORALL - || getKind() == kind::EXISTS || getKind() == kind::CHOICE + || getKind() == kind::EXISTS || getKind() == kind::WITNESS || getKind() == kind::COMPREHENSION || getKind() == kind::MATCH_BIND_CASE; } diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index e47029284..5e042d591 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -78,7 +78,7 @@ bool hasFreeVar(TNode n); /** * Returns true iff the node n contains a closure, that is, a node - * whose kind is FORALL, EXISTS, CHOICE, LAMBDA, or any other closure currently + * whose kind is FORALL, EXISTS, WITNESS, LAMBDA, or any other closure currently * supported. * @param n The node under investigation * @return true iff this node contains a closure. |