From 0b35328eb0a41856d8378c39a132fcc91485d5b0 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 13 Jan 2020 07:12:20 -0800 Subject: [PATCH] [sledge] Factor out solving polynomial = 0 equalities from solve Summary: Identifying and separating one of the monomials in a polynomial, and solving an equality for it, is much more dependent on the representation of polynomial terms than the rest of solve. Reviewed By: ngorogiannis Differential Revision: D19282645 fbshipit-source-id: 645191ae0 --- sledge/src/llair/term.ml | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml index e21dda086..bcebdbce0 100644 --- a/sledge/src/llair/term.ml +++ b/sledge/src/llair/term.ml @@ -1041,6 +1041,15 @@ let classify = function | Ap1 _ | Ap2 _ | Ap3 _ | ApN _ -> Uninterpreted | RecN _ | Var _ | Integer _ | Float _ | Nondet _ | Label _ -> Atomic +let solve_zero_eq = function + | Add args -> + let c, q = Qset.min_elt_exn args in + let n = Sum.to_term (Qset.remove args c) in + let d = rational (Q.neg q) in + let r = div n d in + Some (c, r) + | _ -> None + let solve e f = [%Trace.call fun {pf} -> pf "%a@ %a" pp e pp f] ; @@ -1067,14 +1076,10 @@ let solve e f = in match (e, f) with | (Add _ | Mul _ | Integer _), _ | _, (Add _ | Mul _ | Integer _) -> ( - match sub e f with - | Add args -> - let c, q = Qset.min_elt_exn args in - let n = Sum.to_term (Qset.remove args c) in - let d = rational (Q.neg q) in - let r = div n d in - Some (Map.add_exn s ~key:c ~data:r) - | e_f -> solve_uninterp e_f zero ) + let e_f = sub e f in + match solve_zero_eq e_f with + | Some (key, data) -> Some (Map.add_exn s ~key ~data) + | None -> solve_uninterp e_f zero ) | ApN (Concat, ms), ApN (Concat, ns) -> ( match (concat_size ms, concat_size ns) with | Some p, Some q -> solve_uninterp e f >>= solve_ p q