From 548928a839e34de843ea9a4594a6e77c5d464629 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 16 Apr 2020 03:39:32 -0700 Subject: [PATCH] [sledge] Strengthen Equality invariant to ensure carrier closed under subterms Reviewed By: jvillard Differential Revision: D20831347 fbshipit-source-id: 374638285 --- sledge/lib/equality.ml | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/sledge/lib/equality.ml b/sledge/lib/equality.ml index 465c69b4a..113077702 100644 --- a/sledge/lib/equality.ml +++ b/sledge/lib/equality.ml @@ -32,9 +32,6 @@ let rec fold_max_solvables e ~init ~f = if non_interpreted e then f e init else Term.fold e ~init ~f:(fun d s -> fold_max_solvables ~f d ~init:s) -let rec iter_max_solvables e ~f = - if non_interpreted e then f e else Term.iter ~f:(iter_max_solvables ~f) e - (** Solution Substitutions *) module Subst : sig type t [@@deriving compare, equal, sexp] @@ -419,10 +416,11 @@ let pre_invariant r = (* no interpreted terms in carrier *) assert (non_interpreted trm || fail "non-interp %a" Term.pp trm ()) ; (* carrier is closed under subterms *) - iter_max_solvables trm ~f:(fun subtrm -> + Term.iter trm ~f:(fun subtrm -> assert ( - in_car r subtrm - || fail "@[subterm %a of %a not in carrier of@ %a@]" Term.pp + non_interpreted subtrm + ==> (Term.is_constant subtrm || in_car r subtrm) + || fail "@[subterm %a@ of %a@ not in carrier of@ %a@]" Term.pp subtrm Term.pp trm pp r () ) ) ) let invariant r =