From d514d0496c5dbf971d50d71295101081667e8d69 Mon Sep 17 00:00:00 2001 From: Basile Clement Date: Tue, 11 Jul 2023 13:17:08 +0200 Subject: [PATCH] Simplify trivial ites This patch adds some simple checks in [Expr.mk_ite] to simplify the trivial ites `(ite t u u)`, `(ite true t u)` and `(ite false t u)`. --- src/lib/structures/expr.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 39950c252..030175b03 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -1045,9 +1045,13 @@ let mk_if cond f2 f3 = (mk_and cond f2 true) (mk_and (neg cond) f3 true) false let mk_ite cond th el = - let ty = type_info th in - if ty == Ty.Tbool then mk_if cond th el - else mk_term (Sy.Op Sy.Tite) [cond; th; el] ty + if equal th el then th + else if equal cond vrai then th + else if equal cond faux then el + else + let ty = type_info th in + if ty == Ty.Tbool then mk_if cond th el + else mk_term (Sy.Op Sy.Tite) [cond; th; el] ty let [@inline always] const_term e = (* we use this function because depth is currently not correct to