[sledge] Simplify and (minor) strengthen Context.is_valid_eq

Summary:
Use Theory.solvable_trms for a minor strengthening and simplification
of Context.is_valid_eq.

Reviewed By: jvillard

Differential Revision: D25883735

fbshipit-source-id: 3d0f3fcfe

sledge/src/fol/context.ml

@@ -133,12 +133,13 @@ end = struct
     let is_var_in xs e =
       Option.exists ~f:(fun x -> Var.Set.mem x xs) (Var.of_trm e)
     in
-    ( is_var_in xs e
+    let noninterp_with_solvable_var_in xs e =
-    || is_var_in xs f
+      is_var_in xs e
-    || Theory.is_uninterpreted e
+      || Theory.is_noninterpreted e
-       && Iter.exists ~f:(is_var_in xs) (Trm.trms e)
+         && Iter.exists ~f:(is_var_in xs) (Theory.solvable_trms e)
-    || Theory.is_uninterpreted f
+    in
-       && Iter.exists ~f:(is_var_in xs) (Trm.trms f) )
+    ( noninterp_with_solvable_var_in xs e
+    || noninterp_with_solvable_var_in xs f )
     $> fun b ->
     [%Trace.info
       "is_valid_eq %a%a=%a = %b" Var.Set.pp_xs xs Trm.pp e Trm.pp f b]