Skip to content

Commit

Permalink
Too long lines
Browse files Browse the repository at this point in the history
  • Loading branch information
Halbaroth committed Oct 9, 2023
1 parent 25defb2 commit 9c78100
Showing 1 changed file with 12 additions and 4 deletions.
16 changes: 12 additions & 4 deletions src/lib/reasoners/intervalCalculus.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2132,7 +2132,9 @@ let optimizing_split env uf opt_split =
let t2 = mk_const_term optim ty in
Debug.case_split r1 r2;
let o = Some {Th_util.opt_ord = order; opt_val = Th_util.Value t2} in
let s = LR.mkv_eq r1 r2, true, Th_util.CS (o, Th_util.Th_arith, Q.one) in
let s =
LR.mkv_eq r1 r2, true, Th_util.CS (o, Th_util.Th_arith, Q.one)
in
Some { opt_split with value = Value s }

| None ->
Expand All @@ -2150,7 +2152,9 @@ let optimizing_split env uf opt_split =
Printer.print_dbg
"%a is unbounded. Let other methods assign a value for it@."
E.print e;
let value = if to_max then Th_util.Pinfinity else Th_util.Minfinity in
let value =
if to_max then Th_util.Pinfinity else Th_util.Minfinity
in
Some { opt_split with value }

| Sim.Core.Max(mx,_sol) ->
Expand All @@ -2165,8 +2169,12 @@ let optimizing_split env uf opt_split =
let r2 = alien_of (P.create [] optim ty) in
Debug.case_split r1 r2;
let t2 = mk_const_term optim ty in
let o = Some {Th_util.opt_ord = order; opt_val = Th_util.Value t2} in
let s = LR.mkv_eq r1 r2, true, Th_util.CS (o, Th_util.Th_arith, Q.one) in
let o =
Some {Th_util.opt_ord = order; opt_val = Th_util.Value t2}
in
let s =
LR.mkv_eq r1 r2, true, Th_util.CS (o, Th_util.Th_arith, Q.one)
in
Some { opt_split with value = Value s; }
end
end
Expand Down

0 comments on commit 9c78100

Please sign in to comment.