From b9a516783c95c62c31c5a9e6b9b0d5ed53993b5b Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Mon, 16 Nov 2015 16:00:00 -0800 Subject: [PATCH] fix(library/blast/simplifier): remove unnecessary casts --- src/library/blast/simplifier.cpp | 45 ++++++++++-- tests/lean/simplifier10.lean | 13 ++-- tests/lean/simplifier11.lean | 28 ++++---- tests/lean/simplifier13.lean | 7 +- tests/lean/simplifier13.lean.expected.out | 2 +- tests/lean/simplifier3.lean | 11 ++- tests/lean/simplifier4.lean | 18 ++--- tests/lean/simplifier4.lean.expected.out | 4 +- tests/lean/simplifier5.lean | 26 +++---- tests/lean/simplifier6.lean | 15 ++-- tests/lean/simplifier7.lean | 8 +-- tests/lean/simplifier8.lean | 5 +- tests/lean/simplifier9.lean | 30 ++++---- tests/lean/simplifier_norm_num.lean | 84 +++++++++++------------ 14 files changed, 161 insertions(+), 135 deletions(-) diff --git a/src/library/blast/simplifier.cpp b/src/library/blast/simplifier.cpp index 7577f2bbe..c18c6af13 100644 --- a/src/library/blast/simplifier.cpp +++ b/src/library/blast/simplifier.cpp @@ -50,7 +50,7 @@ #define LEAN_DEFAULT_SIMPLIFY_FUSE false #endif #ifndef LEAN_DEFAULT_SIMPLIFY_NUMERALS -#define LEAN_DEFAULT_SIMPLIFY_NUMERALS true +#define LEAN_DEFAULT_SIMPLIFY_NUMERALS false #endif namespace lean { @@ -198,6 +198,7 @@ class simplifier { } expr unfold_reducible_instances(expr const & e); + expr remove_unnecessary_casts(expr const & e); bool instantiate_emetas(blast_tmp_type_context & tmp_tctx, unsigned num_emeta, list const & emetas, list const & instances); @@ -801,27 +802,59 @@ optional simplifier::synth_congr(expr const & e, F && simp) { expr proof = congr_lemma->get_proof(); expr type = congr_lemma->get_type(); unsigned i = 0; - bool simplified = false; + bool has_proof = false; + bool has_cast = false; buffer locals; for_each(congr_lemma->get_arg_kinds(), [&](congr_arg_kind const & ckind) { proof = mk_app(proof, args[i]); type = instantiate(binding_body(type), args[i]); if (ckind == congr_arg_kind::Eq) { result r_arg = simp(args[i]); - if (r_arg.has_proof()) simplified = true; + if (r_arg.has_proof()) has_proof = true; r_arg = finalize(r_arg); proof = mk_app(proof, r_arg.get_new(), r_arg.get_proof()); type = instantiate(binding_body(type), r_arg.get_new()); type = instantiate(binding_body(type), r_arg.get_proof()); + } else if (ckind == congr_arg_kind::Cast) { + has_cast = true; } i++; }); lean_assert(is_eq(type)); buffer type_args; get_app_args(type, type_args); - expr & new_e = type_args[2]; - if (simplified) return optional(result(new_e, proof)); - else return optional(result(new_e)); + expr e_new = remove_unnecessary_casts(type_args[2]); + if (has_proof) return optional(result(e_new, proof)); + else return optional(result(e_new)); +} + +expr simplifier::remove_unnecessary_casts(expr const & e) { + buffer args; + expr f = get_app_args(e, args); + fun_info f_info = get_fun_info(f, args.size()); + int i = -1; + for_each(f_info.get_params_info(), [&](param_info const & p_info) { + i++; + if (p_info.is_subsingleton()) { + while (is_constant(get_app_fn(args[i]))) { + buffer cast_args; + expr f_cast = get_app_args(args[i], cast_args); + name n_f = const_name(f_cast); + if (n_f == get_eq_rec_name() || n_f == get_eq_drec_name() || n_f == get_eq_nrec_name()) { + lean_assert(cast_args.size() == 6); + expr major_premise = cast_args[5]; + expr f_major_premise = get_app_fn(major_premise); + if (is_constant(f_major_premise) && const_name(f_major_premise) == get_eq_refl_name()) + args[i] = cast_args[3]; + else + return; + } else { + return; + } + } + } + }); + return mk_app(f, args); } /* Fusion */ diff --git a/tests/lean/simplifier10.lean b/tests/lean/simplifier10.lean index 2cf3c097b..fe47ccc65 100644 --- a/tests/lean/simplifier10.lean +++ b/tests/lean/simplifier10.lean @@ -4,15 +4,14 @@ universe l constants (T : Type.{l}) (x y z : T) (P : T → Prop) (Q : T → T → T → Prop) (R W V : T → T → Prop) constants (px : P x) (wxz : W x z) (vzy : V z y) constants (H : ∀ (x y z : T), P x → W x z → V z y → (Q z y x ↔ R x y)) -namespace tst + attribute px true_iff [simp] attribute wxz [simp] attribute vzy [simp] attribute H [simp] -end tst -#simplify iff tst 0 P x -#simplify iff tst 0 W x z -#simplify iff tst 0 V z y -#simplify iff tst 0 Q z y x -#simplify iff tst 0 V z y ↔ Q z y x +#simplify iff env 0 P x +#simplify iff env 0 W x z +#simplify iff env 0 V z y +#simplify iff env 0 Q z y x +#simplify iff env 0 V z y ↔ Q z y x diff --git a/tests/lean/simplifier11.lean b/tests/lean/simplifier11.lean index e4bb500a5..47e64154b 100644 --- a/tests/lean/simplifier11.lean +++ b/tests/lean/simplifier11.lean @@ -6,28 +6,28 @@ constants {A : Type} {b c : Prop} (dec_b : decidable b) (dec_c : decidable c) {x y u v : A} (h_c : b ↔ c) (h_t : x = u) (h_e : y = v) attribute dec_b [instance] - attribute dec_c [instance] - attribute h_c [simp] - attribute h_t [simp] - attribute h_e [simp] +attribute dec_c [instance] +attribute h_c [simp] +attribute h_t [simp] +attribute h_e [simp] attribute if_congr [congr] -#simplify eq if_congr 0 (ite b x y) +#simplify eq env 0 (ite b x y) end if_congr namespace if_ctx_simp_congr constants {A : Type} {b c : Prop} (dec_b : decidable b) {x y u v : A} (h_c : b ↔ c) (h_t : c → x = u) (h_e : ¬c → y = v) - attribute dec_b [instance] - attribute h_c [simp] - attribute h_t [simp] - attribute h_e [simp] +attribute dec_b [instance] +attribute h_c [simp] +attribute h_t [simp] +attribute h_e [simp] attribute if_ctx_simp_congr [congr] --- TODO(Daniel): lean_unreachable -#simplify eq if_ctx_simp_congr 0 (ite b x y) + +#simplify eq env 0 (ite b x y) end if_ctx_simp_congr @@ -43,7 +43,7 @@ constants {b c x y u v : Prop} (dec_b : decidable b) (dec_c : decidable c) attribute if_congr_prop [congr] -#simplify iff if_congr_prop 0 (ite b x y) +#simplify iff env 0 (ite b x y) end if_congr_prop namespace if_ctx_simp_congr_prop @@ -56,7 +56,7 @@ constants (b c x y u v : Prop) (dec_b : decidable b) attribute h_e [simp] attribute if_ctx_simp_congr_prop [congr] -#simplify iff if_ctx_simp_congr_prop 0 (ite b x y) +#simplify iff env 0 (ite b x y) end if_ctx_simp_congr_prop @@ -70,5 +70,5 @@ constants (b c x y u v : Prop) (dec_b : decidable b) attribute h_e [simp] attribute if_simp_congr_prop [congr] -#simplify iff if_simp_congr_prop 0 (ite b x y) +#simplify iff env 0 (ite b x y) end if_simp_congr_prop diff --git a/tests/lean/simplifier13.lean b/tests/lean/simplifier13.lean index 6ae62a1da..e12675a88 100644 --- a/tests/lean/simplifier13.lean +++ b/tests/lean/simplifier13.lean @@ -3,8 +3,7 @@ constants (T : Type.{l}) (f : T → T → T) (g : T → T) constants (P : T → Prop) (Q : Prop) (Hfg : ∀ (x : T), f x x = g x) constants (c : Π (x y z : T), P x → P y → P z → Q) constants (x y z : T) (px : P (f x x)) (py : P (f y y)) (pz : P (g z)) -namespace tst + attribute Hfg [simp] -end tst --- TODO(Daniel): extra step? Similar to simplifier1.hlean -#simplify eq tst 0 c (f x x) (f y y) (g z) px py pz + +#simplify eq env 0 c (f x x) (f y y) (g z) px py pz diff --git a/tests/lean/simplifier13.lean.expected.out b/tests/lean/simplifier13.lean.expected.out index 279c5cb07..cf1fded4b 100644 --- a/tests/lean/simplifier13.lean.expected.out +++ b/tests/lean/simplifier13.lean.expected.out @@ -1 +1 @@ -c (g x) (g y) (g z) (eq.rec px (Hfg x)) (eq.rec py (Hfg y)) (eq.rec pz (eq.refl (g z))) +c (g x) (g y) (g z) (eq.rec px (Hfg x)) (eq.rec py (Hfg y)) pz diff --git a/tests/lean/simplifier3.lean b/tests/lean/simplifier3.lean index a58624056..9f21dfa20 100644 --- a/tests/lean/simplifier3.lean +++ b/tests/lean/simplifier3.lean @@ -7,13 +7,12 @@ constant T : Type.{l} constants (x y z : T → T) (f g h : (T → T) → (T → T)) (a b c : T) constants (Hfxgy : f x = g y) (Hgyhz : g y = h z) (Hab : a = b) (Hbc : b = c) -namespace tst attribute Hfxgy [simp] attribute Hgyhz [simp] attribute Hab [simp] attribute Hbc [simp] -end tst -#simplify eq tst 2 (f x a) + +#simplify eq env 2 (f x a) end test_congr @@ -23,9 +22,9 @@ universes l1 l2 constants (T : Type.{l1}) (U : T → Type.{l2}) constants (f g : Π (x:T), U x) (x y : T) constants (Hfg : f = g) (Hxy : x = y) -namespace tst + attribute Hfg [simp] attribute Hxy [simp] -end tst -#simplify eq tst 2 (f x) + +#simplify eq env 2 (f x) end test_congr_fun diff --git a/tests/lean/simplifier4.lean b/tests/lean/simplifier4.lean index 4b17fbd58..9f125b89d 100644 --- a/tests/lean/simplifier4.lean +++ b/tests/lean/simplifier4.lean @@ -8,12 +8,12 @@ constants (R : T → T → Prop) constants (R_refl : ∀ x, R x x) (R_sym : ∀ x y, R x y → R y x) (R_trans : ∀ x y z, R x y → R y z → R x z) constants (Hfxgy : R (f x) (g y)) (Hgyhz : R (g y) (h z)) -namespace tst attribute R_refl [refl] end tst -namespace tst attribute R_sym [symm] end tst -#simplify R tst 2 (f x) -- f x -namespace tst attribute R_trans [trans] end tst -#simplify R tst 2 (f x) -- f x -namespace tst attribute Hfxgy [simp] end tst -#simplify R tst 2 (f x) -- f x -namespace tst attribute Hgyhz [simp] end tst -#simplify R tst 2 (f x) -- f x +attribute R_refl [refl] +attribute R_sym [symm] +#simplify R env 2 (f x) -- f x +attribute R_trans [trans] +#simplify R env 2 (f x) -- f x +attribute Hfxgy [simp] +#simplify R env 2 (f x) -- f x +attribute Hgyhz [simp] +#simplify R env 2 (f x) -- f x diff --git a/tests/lean/simplifier4.lean.expected.out b/tests/lean/simplifier4.lean.expected.out index fabfcc8ff..307d50d2b 100644 --- a/tests/lean/simplifier4.lean.expected.out +++ b/tests/lean/simplifier4.lean.expected.out @@ -1,4 +1,4 @@ - - +(refl): f x +(refl): f x R (f x) (g y) R (f x) (h z) diff --git a/tests/lean/simplifier5.lean b/tests/lean/simplifier5.lean index b506735aa..ff8ebc31f 100644 --- a/tests/lean/simplifier5.lean +++ b/tests/lean/simplifier5.lean @@ -1,16 +1,16 @@ /- Basic rewriting with iff with congr_iff -/ import logic.connectives open nat -namespace tst -attribute iff_self true_iff_false self_lt_succ_iff_true zero_lt_succ_iff_true zero_le_iff_true succ_le_self_iff_false succ_le_self_iff_false lt_self_iff_false [simp] -end tst -#simplify iff tst 2 (@le nat nat_has_le 0 0) -- true -#simplify iff tst 2 (@le nat nat_has_le 0 1) -- true -#simplify iff tst 2 (@le nat nat_has_le 0 2) -- true -#simplify iff tst 2 (@lt nat nat_has_lt 0 0) -- false -#simplify iff tst 2 (@lt nat nat_has_lt 0 (succ 0)) -- true -#simplify iff tst 2 (@lt nat nat_has_lt 1 (succ 1)) -- true -#simplify iff tst 2 (@lt nat nat_has_lt 0 (succ (succ 0))) -- true -#simplify iff tst 2 (@le nat nat_has_le 0 0 ↔ @le nat nat_has_le 0 0) -- true -#simplify iff tst 2 (@le nat nat_has_le 0 0 ↔ @le nat nat_has_le 0 1) -- true -#simplify iff tst 2 (@le nat nat_has_le 0 0 ↔ @lt nat nat_has_lt 0 0) -- false + +attribute not_true [simp] + +#simplify iff env 2 (@le nat nat_has_le 0 0) -- true +#simplify iff env 2 (@le nat nat_has_le 0 1) -- true +#simplify iff env 2 (@le nat nat_has_le 0 2) -- true +#simplify iff env 2 (@lt nat nat_has_lt 0 0) -- false +#simplify iff env 2 (@lt nat nat_has_lt 0 (succ 0)) -- true +#simplify iff env 2 (@lt nat nat_has_lt 1 (succ 1)) -- true +#simplify iff env 2 (@lt nat nat_has_lt 0 (succ (succ 0))) -- true +#simplify iff env 2 (@le nat nat_has_le 0 0 ↔ @le nat nat_has_le 0 0) -- true +#simplify iff env 2 (@le nat nat_has_le 0 0 ↔ @le nat nat_has_le 0 1) -- true +#simplify iff env 2 (@le nat nat_has_le 0 0 ↔ @lt nat nat_has_lt 0 0) -- false diff --git a/tests/lean/simplifier6.lean b/tests/lean/simplifier6.lean index a3d295b57..ea12f5433 100644 --- a/tests/lean/simplifier6.lean +++ b/tests/lean/simplifier6.lean @@ -3,29 +3,28 @@ import logic.connectives logic.quantifiers namespace pi_congr1 constants (p1 q1 p2 q2 p3 q3 : Prop) (H1 : p1 ↔ q1) (H2 : p2 ↔ q2) (H3 : p3 ↔ q3) -namespace tst + attribute congr_forall [congr] attribute congr_imp [congr] attribute H1 [simp] attribute H2 [simp] attribute H3 [simp] -end tst -#simplify iff tst 1 p1 -- Broken? -#simplify iff tst 1 p1 → p2 -#simplify iff tst 1 p1 → p2 → p3 +#simplify iff env 1 p1 -- Broken? +#simplify iff env 1 p1 → p2 +#simplify iff env 1 p1 → p2 → p3 end pi_congr1 namespace pi_congr2 universe l constants (T : Type.{l}) (P Q : T → Prop) (H : ∀ (x : T), P x ↔ Q x) -namespace tst +attribute congr_forall [congr] attribute H [simp] -end tst + constant (x : T) -#simplify iff tst 1 (∀ (x : T), P x) +#simplify iff env 1 (∀ (x : T), P x) end pi_congr2 diff --git a/tests/lean/simplifier7.lean b/tests/lean/simplifier7.lean index b9ea24897..c88df5cce 100644 --- a/tests/lean/simplifier7.lean +++ b/tests/lean/simplifier7.lean @@ -4,13 +4,13 @@ import logic.connectives constants (P1 Q1 P2 Q2 P3 Q3 : Prop) (H1 : P1 ↔ Q1) (H2 : P2 ↔ Q2) (H3 : P3 ↔ Q3) constants (f g : Prop → Prop → Prop) constants (Hf : and = f) (Hg : f = g) -namespace tst + attribute H1 [simp] attribute H2 [simp] attribute H3 [simp] attribute Hf [simp] attribute Hg [simp] -end tst -#simplify iff tst 2 (and P1 (and P2 P3)) -#simplify iff tst 2 (and P1 (iff P2 P3)) + +#simplify iff env 2 (and P1 (and P2 P3)) +#simplify iff env 2 (and P1 (iff P2 P3)) diff --git a/tests/lean/simplifier8.lean b/tests/lean/simplifier8.lean index a1754c593..7a167e6a6 100644 --- a/tests/lean/simplifier8.lean +++ b/tests/lean/simplifier8.lean @@ -6,10 +6,9 @@ constants (f_comm : ∀ x y, f x y = f y x) (f_l : ∀ x y z, f (f x y) z = f x (f y z)) (f_r : ∀ x y z, f x (f y z) = f y (f x z)) -namespace tst + attribute f_comm [simp] attribute f_l [simp] attribute f_r [simp] -end tst -#simplify eq tst 0 (f (f x2 x4) (f x5 (f x3 (f x1 x6)))) +#simplify eq env 0 (f (f x2 x4) (f x5 (f x3 (f x1 x6)))) diff --git a/tests/lean/simplifier9.lean b/tests/lean/simplifier9.lean index 6c7fa5f30..431ad89e5 100644 --- a/tests/lean/simplifier9.lean +++ b/tests/lean/simplifier9.lean @@ -1,30 +1,28 @@ -- Rewriting with (tmp)-local hypotheses import logic.quantifiers -namespace tst attribute congr_forall [congr] attribute congr_imp [congr] -end tst universe l constants (T : Type.{l}) (P Q : T → Prop) set_option simplify.max_steps 50000 constants (x y : T) --- TODO(Daniel): the following is looping... -#simplify iff tst 0 x = y → x = y -#simplify iff tst 0 T → x = y → x = y -#simplify iff tst 0 ∀ z : T, x = z → x = y -#simplify iff tst 0 ∀ z : T, z = x → x = z -#simplify iff tst 0 ∀ (z w : T), x = y → x = y -#simplify iff tst 0 ∀ (z w : T), x = y → P x -#simplify iff tst 0 ∀ (H : ∀ x, P x ↔ Q x), P x -#simplify iff tst 0 ∀ (p : Prop) (H : ∀ x, P x ↔ Q x) (q : Prop), P x +#simplify iff env 0 x = y → x = y +#simplify iff env 0 T → x = y → x = y +#simplify iff env 0 ∀ z : T, x = z → x = y +#simplify iff env 0 ∀ z : T, z = x → x = z +#simplify iff env 0 ∀ (z w : T), x = y → x = y +#simplify iff env 0 ∀ (z w : T), x = y → P x -#simplify iff tst 0 ∀ (p : Prop) (H : ∀ x, P x ↔ Q x), p ∨ P x -#simplify iff tst 0 (∀ (x : T), P x ↔ Q x) → P x -#simplify iff tst 0 (∀ (x : T), P x ↔ Q x) → P x -#simplify iff tst 0 ∀ (x y : T), (∀ (x : T), P x ↔ Q x) → P x +#simplify iff env 0 ∀ (H : ∀ x, P x ↔ Q x), P x +#simplify iff env 0 ∀ (p : Prop) (H : ∀ x, P x ↔ Q x) (q : Prop), P x -#simplify iff tst 0 ∀ (x z : T), x = z → (∀ (w : T), P w ↔ Q w) → P x +#simplify iff env 0 ∀ (p : Prop) (H : ∀ x, P x ↔ Q x), p ∨ P x +#simplify iff env 0 (∀ (x : T), P x ↔ Q x) → P x +#simplify iff env 0 (∀ (x : T), P x ↔ Q x) → P x +#simplify iff env 0 ∀ (x y : T), (∀ (x : T), P x ↔ Q x) → P x + +#simplify iff env 0 ∀ (x z : T), x = z → (∀ (w : T), P w ↔ Q w) → P x diff --git a/tests/lean/simplifier_norm_num.lean b/tests/lean/simplifier_norm_num.lean index ab46c46db..2d3eb385f 100644 --- a/tests/lean/simplifier_norm_num.lean +++ b/tests/lean/simplifier_norm_num.lean @@ -8,51 +8,51 @@ universe l constants (A : Type.{l}) (A_comm_ring : comm_ring A) attribute A_comm_ring [instance] -#simplify eq 0 (0:A) + 1 -#simplify eq 0 (1:A) + 0 -#simplify eq 0 (1:A) + 1 -#simplify eq 0 (0:A) + 2 -#simplify eq 0 (1:A) + 2 -#simplify eq 0 (2:A) + 1 -#simplify eq 0 (3:A) + 1 -#simplify eq 0 (2:A) + 2 -#simplify eq 0 (4:A) + 1 -#simplify eq 0 (3:A) + 2 -#simplify eq 0 (2:A) + 3 -#simplify eq 0 (0:A) + 6 -#simplify eq 0 (3:A) + 3 -#simplify eq 0 (4:A) + 2 -#simplify eq 0 (5:A) + 1 -#simplify eq 0 (4:A) + 3 -#simplify eq 0 (1:A) + 6 -#simplify eq 0 (6:A) + 1 -#simplify eq 0 (5:A) + 28 -#simplify eq 0 (0 : A) + (2 + 3) + 7 -#simplify eq 0 (70 : A) + (33 + 2) +#simplify eq env 0 (0:A) + 1 +#simplify eq env 0 (1:A) + 0 +#simplify eq env 0 (1:A) + 1 +#simplify eq env 0 (0:A) + 2 +#simplify eq env 0 (1:A) + 2 +#simplify eq env 0 (2:A) + 1 +#simplify eq env 0 (3:A) + 1 +#simplify eq env 0 (2:A) + 2 +#simplify eq env 0 (4:A) + 1 +#simplify eq env 0 (3:A) + 2 +#simplify eq env 0 (2:A) + 3 +#simplify eq env 0 (0:A) + 6 +#simplify eq env 0 (3:A) + 3 +#simplify eq env 0 (4:A) + 2 +#simplify eq env 0 (5:A) + 1 +#simplify eq env 0 (4:A) + 3 +#simplify eq env 0 (1:A) + 6 +#simplify eq env 0 (6:A) + 1 +#simplify eq env 0 (5:A) + 28 +#simplify eq env 0 (0 : A) + (2 + 3) + 7 +#simplify eq env 0 (70 : A) + (33 + 2) -#simplify eq 0 (23000000000 : A) + 22000000000 +#simplify eq env 0 (23000000000 : A) + 22000000000 -#simplify eq 0 (0 : A) * 0 -#simplify eq 0 (0 : A) * 1 -#simplify eq 0 (0 : A) * 2 -#simplify eq 0 (2 : A) * 0 -#simplify eq 0 (1 : A) * 0 -#simplify eq 0 (1 : A) * 1 -#simplify eq 0 (2 : A) * 1 -#simplify eq 0 (1 : A) * 2 -#simplify eq 0 (2 : A) * 2 -#simplify eq 0 (3 : A) * 2 -#simplify eq 0 (2 : A) * 3 -#simplify eq 0 (4 : A) * 1 -#simplify eq 0 (1 : A) * 4 -#simplify eq 0 (3 : A) * 3 -#simplify eq 0 (3 : A) * 4 -#simplify eq 0 (4 : A) * 4 -#simplify eq 0 (11 : A) * 2 -#simplify eq 0 (15 : A) * 6 -#simplify eq 0 (123456 : A) * 123456 +#simplify eq env 0 (0 : A) * 0 +#simplify eq env 0 (0 : A) * 1 +#simplify eq env 0 (0 : A) * 2 +#simplify eq env 0 (2 : A) * 0 +#simplify eq env 0 (1 : A) * 0 +#simplify eq env 0 (1 : A) * 1 +#simplify eq env 0 (2 : A) * 1 +#simplify eq env 0 (1 : A) * 2 +#simplify eq env 0 (2 : A) * 2 +#simplify eq env 0 (3 : A) * 2 +#simplify eq env 0 (2 : A) * 3 +#simplify eq env 0 (4 : A) * 1 +#simplify eq env 0 (1 : A) * 4 +#simplify eq env 0 (3 : A) * 3 +#simplify eq env 0 (3 : A) * 4 +#simplify eq env 0 (4 : A) * 4 +#simplify eq env 0 (11 : A) * 2 +#simplify eq env 0 (15 : A) * 6 +#simplify eq env 0 (123456 : A) * 123456 -#simplify eq 0 (0 + 45343453:A) * (53653343 + 1) * (53453 + 2) + (0 + 1 + 2 + 2200000000034733) +#simplify eq env 0 (0 + 45343453:A) * (53653343 + 1) * (53453 + 2) + (0 + 1 + 2 + 2200000000034733) -- The following test is too slow -- #simplify eq 0 (23000000000343434534345316:A) * (53653343563534534 + 5367536453653573573453) * 53453756475777536 + 2200000000034733531531531534536