From 5346f79100fc8b63ec81e15c4757de4b88b4c1d9 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 2 Feb 2021 04:35:09 -0800 Subject: [PATCH] [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 | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml index 6626cb7ac..8c49d8c90 100644 --- a/sledge/src/fol/context.ml +++ b/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 - || is_var_in xs f - || Theory.is_uninterpreted e - && Iter.exists ~f:(is_var_in xs) (Trm.trms e) - || Theory.is_uninterpreted f - && Iter.exists ~f:(is_var_in xs) (Trm.trms f) ) + let noninterp_with_solvable_var_in xs e = + is_var_in xs e + || Theory.is_noninterpreted e + && Iter.exists ~f:(is_var_in xs) (Theory.solvable_trms e) + in + ( 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]