From cd116fcf41fd454c9c59fd787e34afc4827205c1 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 2 Feb 2021 04:35:48 -0800 Subject: [PATCH] [sledge] Improve Context.invariant with Theory.classify Reviewed By: jvillard Differential Revision: D25883721 fbshipit-source-id: 77de5fbbd --- sledge/src/fol/context.ml | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml index e6a2074a1..635d3702e 100644 --- a/sledge/src/fol/context.ml +++ b/sledge/src/fol/context.ml @@ -352,14 +352,12 @@ let pre_invariant r = Subst.iteri r.rep ~f:(fun ~key:trm ~data:rep -> (* no interpreted terms in carrier *) assert ( - (not (Theory.is_interpreted trm)) - || fail "non-interp %a" Trm.pp trm () ) ; - (* carrier is closed under subterms *) - Iter.iter (Trm.trms trm) ~f:(fun subtrm -> + Theory.is_noninterpreted trm || fail "non-interp %a" Trm.pp trm () + ) ; + (* carrier is closed under solvable subterms *) + Iter.iter (Theory.solvable_trms trm) ~f:(fun subtrm -> assert ( - Theory.is_interpreted subtrm - || (match subtrm with Z _ | Q _ -> true | _ -> false) - || in_car r subtrm + in_car r subtrm || fail "@[subterm %a@ of %a@ not in carrier of@ %a@]" Trm.pp subtrm Trm.pp trm pp r () ) ) ; (* rep is idempotent *)