[pulse] fix fuel debug message

Summary:
This would previously print that we ran out of fuel even if we didn't
and we simply reached a normal form.

Reviewed By: ezgicicek

Differential Revision: D23575571

fbshipit-source-id: 37d02ca8d
master
Jules Villard 4 years ago committed by Facebook GitHub Bot
parent a95ef1f842
commit b62c3f55b9

@ -1200,13 +1200,15 @@ end = struct
fuel). That's ok because there's not much fuel to begin with, and as long as we're making fuel). That's ok because there's not much fuel to begin with, and as long as we're making
progress it's probably worth it anyway. *) progress it's probably worth it anyway. *)
let rec normalize_with_fuel ~fuel phi = let rec normalize_with_fuel ~fuel phi =
let* new_linear_eqs, phi = normalize_linear_eqs ~fuel phi >>= normalize_atoms in if fuel <= 0 then (
if new_linear_eqs && fuel > 0 then (
L.d_printfln "new linear equalities, consuming fuel (from %d)" fuel ;
normalize_with_fuel ~fuel:(fuel - 1) phi )
else (
L.d_printfln "ran out of fuel when normalizing" ; L.d_printfln "ran out of fuel when normalizing" ;
Sat phi ) Sat phi )
else
let* new_linear_eqs, phi = normalize_linear_eqs ~fuel phi >>= normalize_atoms in
if new_linear_eqs then (
L.d_printfln "new linear equalities, consuming fuel (from %d)" fuel ;
normalize_with_fuel ~fuel:(fuel - 1) phi )
else Sat phi
in in
normalize_with_fuel ~fuel:base_fuel phi normalize_with_fuel ~fuel:base_fuel phi

Loading…
Cancel
Save