diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-01 13:35:07 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-11-01 13:35:07 -0500 |
| commit | 13e452be03bef09e2f54f42e2bc42383505ffcea (patch) | |
| tree | 39695fe22d387bc84bc49d20831a19648d55011f /src/smt/term_formula_removal.h | |
| parent | be11fae39055f213586058ec9129d1276f724b0e (diff) | |
CBQI BV choice expressions (#1296)
* Use Hilbert choice expressions for cbqi bv. Failing in debug due to TNode issues currently.
* Minor
* Make unique bound variables for choice functions in BvInstantor, clean up.
* Incorporate missing optimizations
* Clang format
* Unused field.
* Minor
* Fix, add regression.
* Fix regression.
* Fix bug that led to incorrect cleanup of instantiations.
* Add missing regression
* Improve handling of choice rewriting.
* Fix
* Clang format
* Use canonical variables for choice functions in cbqi bv.
* Add regression
* Clang format.
* Address review.
* Clang format
Diffstat (limited to 'src/smt/term_formula_removal.h')
| -rw-r--r-- | src/smt/term_formula_removal.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index f84f9dc37..371ca1f58 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -50,7 +50,7 @@ public: /** * By introducing skolem variables, this function removes all occurrences of: - * (1) term ITEs + * (1) term ITEs, * (2) terms of type Boolean that are not Boolean term variables, * (3) lambdas, and * (4) Hilbert choice expressions. |