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

fix(tycheck): handle proper unary minus

Browse source
This commit is contained in:
Simon Cruanes 2020-11-14 13:17:23 -05:00
parent 103c320577
commit 77b33346f5
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smtlib/Typecheck.ml
View file

@ -280,6 +280,12 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
| PA.Add, [a;b] -> T.lra ctx.tst (LRA_op (Plus, a, b)) | PA.Add, [a;b] -> T.lra ctx.tst (LRA_op (Plus, a, b))
| PA.Add, (a::l) -> | PA.Add, (a::l) ->
List.fold_left (fun a b -> T.lra ctx.tst (LRA_op (Plus,a,b))) a l List.fold_left (fun a b -> T.lra ctx.tst (LRA_op (Plus,a,b))) a l
| PA.Minus, [a] ->
begin match t_as_q a with
| Some a -> T.lra ctx.tst (LRA_const (Q.neg a))
| None ->
T.lra ctx.tst (LRA_op (Minus, T.lra ctx.tst (LRA_const Q.zero), a))
end
| PA.Minus, [a;b] -> T.lra ctx.tst (LRA_op (Minus, a, b)) | PA.Minus, [a;b] -> T.lra ctx.tst (LRA_op (Minus, a, b))
| PA.Minus, (a::l) -> | PA.Minus, (a::l) ->
List.fold_left (fun a b -> T.lra ctx.tst (LRA_op (Minus,a,b))) a l List.fold_left (fun a b -> T.lra ctx.tst (LRA_op (Minus,a,b))) a l