simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat(lra): bugfixes

Browse source
This commit is contained in:
Simon Cruanes 2020-10-10 14:33:54 -04:00
parent 93b56618f1
commit 7c3c88d6f6
2 changed files with 7 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/th-lra/Sidekick_lra.ml
View file

@ -237,8 +237,12 @@ module Make(A : ARG) : S with module A = A = struct
| exception Not_found -> () | exception Not_found -> ()
| (pred, a, b) -> | (pred, a, b) ->
let pred = if sign then pred else FM.Pred.neg pred in let pred = if sign then pred else FM.Pred.neg pred in
if pred = Neq then (
Log.debugf 50 (fun k->k "skip neq in %a" T.pp t);
) else (
let c = FM_A.Constr.mk ~tag:lit pred a b in let c = FM_A.Constr.mk ~tag:lit pred a b in
FM_A.assert_c fm c; FM_A.assert_c fm c;
)
end) end)
end; end;
Log.debug 5 "lra: call arith solver"; Log.debug 5 "lra: call arith solver";

2
src/th-lra/fourier_motzkin.ml
View file

@ -248,7 +248,7 @@ module Make(A : ARG)
} }
let add_sys (sys:system) (c:Constr.t) : system = let add_sys (sys:system) (c:Constr.t) : system =
assert (match c.pred with Eq|Neq|Lt -> true | _ -> false); assert (match c.pred with Eq|Leq|Lt -> true | _ -> false);
if Constr.is_trivial c then ( if Constr.is_trivial c then (
Log.debugf 10 (fun k->k"(@[FM.drop-trivial@ %a@])" Constr.pp c); Log.debugf 10 (fun k->k"(@[FM.drop-trivial@ %a@])" Constr.pp c);
sys sys