[sledge] Improve Context.invariant with Theory.classify

Reviewed By: jvillard

Differential Revision: D25883721

fbshipit-source-id: 77de5fbbd

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))
+        Theory.is_noninterpreted trm || fail "non-interp %a" Trm.pp trm ()
-        || fail "non-interp %a" Trm.pp trm () ) ;
+      ) ;
-      (* carrier is closed under subterms *)
+      (* carrier is closed under solvable subterms *)
-      Iter.iter (Trm.trms trm) ~f:(fun subtrm ->
+      Iter.iter (Theory.solvable_trms trm) ~f:(fun subtrm ->
           assert (
-            Theory.is_interpreted subtrm
+            in_car r subtrm
-            || (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 () ) ) ;
       (* rep is idempotent *)