From dc320bf0c953d023f6e186ba4ee9ccbf5a41c240 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 10 Oct 2020 14:34:05 -0400 Subject: [PATCH] fix(tycheck): handle n-ary +/- --- src/smtlib/Typecheck.ml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index 6ac90497..221fad4e 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -278,9 +278,14 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t = | PA.Geq, [a;b] -> T.lra ctx.tst (LRA_pred (Geq, a, b)) | PA.Gt, [a;b] -> T.lra ctx.tst (LRA_pred (Gt, a, b)) | PA.Add, [a;b] -> T.lra ctx.tst (LRA_op (Plus, a, b)) + | PA.Add, (a::l) -> + List.fold_left (fun a b -> T.lra ctx.tst (LRA_op (Plus,a,b))) a l | PA.Minus, [a;b] -> T.lra ctx.tst (LRA_op (Minus, a, b)) + | PA.Minus, (a::l) -> + List.fold_left (fun a b -> T.lra ctx.tst (LRA_op (Minus,a,b))) a l | PA.Mult, [a;b] -> begin match t_as_q a, t_as_q b with + | Some a, Some b -> T.lra ctx.tst (LRA_const (Q.mul a b)) | Some a, _ -> T.lra ctx.tst (LRA_mult (a, b)) | _, Some b -> T.lra ctx.tst (LRA_mult (b, a)) | None, None -> @@ -288,6 +293,7 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t = end | PA.Div, [a;b] -> begin match t_as_q a, t_as_q b with + | Some a, Some b -> T.lra ctx.tst (LRA_const (Q.div a b)) | Some a, _ -> T.lra ctx.tst (LRA_mult (Q.inv a, b)) | _, Some b -> T.lra ctx.tst (LRA_mult (Q.inv b, a)) | None, None ->