From 440aed0f09fda9c89e514759b3f979d1a2d6c712 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 12 Jan 2021 04:29:01 -0800 Subject: [PATCH] [sledge] Strengthen Context.invariant Reviewed By: jvillard Differential Revision: D25756558 fbshipit-source-id: 4f371c8ea --- sledge/src/fol/context.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml index 5b304be1a..c3a707faf 100644 --- a/sledge/src/fol/context.ml +++ b/sledge/src/fol/context.ml @@ -560,7 +560,7 @@ let congruent r a b = semi_congruent r (Trm.map ~f:(Subst.norm r.rep) a) b let pre_invariant r = let@ () = Invariant.invariant [%here] r [%sexp_of: t] in - Subst.iteri r.rep ~f:(fun ~key:trm ~data:_ -> + Subst.iteri r.rep ~f:(fun ~key:trm ~data:rep -> (* no interpreted terms in carrier *) assert ( (not (is_interpreted trm)) || fail "non-interp %a" Trm.pp trm () ) ; @@ -571,7 +571,13 @@ let pre_invariant r = || (match subtrm with Z _ | Q _ -> true | _ -> false) || in_car r subtrm || fail "@[subterm %a@ of %a@ not in carrier of@ %a@]" Trm.pp - subtrm Trm.pp trm pp r () ) ) ) + subtrm Trm.pp trm pp r () ) ) ; + (* rep is idempotent *) + assert ( + let rep' = Subst.norm r.rep rep in + Trm.equal rep rep' + || fail "not idempotent: %a != %a in@ %a" Trm.pp rep Trm.pp rep' + Subst.pp r.rep () ) ) let invariant r = let@ () = Invariant.invariant [%here] r [%sexp_of: t] in