From 4a027b66821171a844e650491924305eba0dc243 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 2 Feb 2021 04:35:01 -0800 Subject: [PATCH] [sledge] Use Theory.solvables in Context.solve_poly_eq Summary: The current Context.max_solvables differs from Theory.solvables in that it incorrectly includes `Z _ | Q _ | Concat [||]` terms. Reviewed By: jvillard Differential Revision: D25883728 fbshipit-source-id: f39f67622 --- sledge/src/fol/context.ml | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml index d76454a83..6626cb7ac 100644 --- a/sledge/src/fol/context.ml +++ b/sledge/src/fol/context.ml @@ -854,12 +854,6 @@ let apply_and_elim ~wrt xs s r = (* Existential Witnessing and Elimination =================================*) -let rec max_solvables e = - if not (Theory.is_interpreted e) then Iter.return e - else Iter.flat_map ~f:max_solvables (Trm.trms e) - -let fold_max_solvables e s ~f = Iter.fold ~f (max_solvables e) s - let subst_invariant us s0 s = assert (s0 == s || not (Subst.equal s0 s)) ; assert ( @@ -885,7 +879,8 @@ let solve_poly_eq us p' q' subst = ; let diff = Trm.sub p' q' in let max_solvables_not_ito_us = - fold_max_solvables diff Zero ~f:(fun solvable_subterm -> function + Iter.fold (Theory.solvables diff) Zero ~f:(fun solvable_subterm -> + function | Many -> Many | zom when Var.Set.subset (Trm.fv solvable_subterm) ~of_:us -> zom | One _ -> Many