Merge branch 'feature/arithmetic' into develop

src/Elo_recursor.ml

@@ -91,7 +91,6 @@ class virtual ['self] recursor =
     method virtual build_X : _
     method virtual build_oexp : _
     method virtual build_Zershift : _
-    method virtual build_Sum : _
     method virtual build_Sershift : _
     method virtual build_Rem : _
     method virtual build_Mul : _

src/Invar_computation.ml

@@ -219,7 +219,7 @@ class ['self] computer (elo : Elo.t) =
     method build_Lshift () = max_color_wiwt
     method build_Div () = max_color_wiwt
     method build_Big_int () = Fun.id
-    method build_AIte () = failwith ("TODO" ^ __LOC__)
+    method build_AIte () cond_color _ _ = cond_color
   end
 
 (* Computes the color (Invar, Static_prop, Init or Temporal) of an

src/Parser.mly

@@ -496,8 +496,8 @@ iexpr:
   | HASH e = expr
   { G.iexp (Location.from_positions $startpos $endpos)
     @@ G.card e  }
-| formula IIMPLIES iexpr IELSE iexpr { G.iexp (Location.from_positions $startpos $endpos)
-    @@ G.num 0 }
+| c = formula IIMPLIES t = iexpr IELSE e = iexpr { G.iexp (Location.from_positions $startpos $endpos)
+    @@ G.ifthenelse_arith c t e }
   | SMALLINT e = brackets(expr)
 	{ G.iexp (Location.from_positions $startpos $endpos)
 	@@ G.small_int e }

src/Raw_to_ast.ml

@@ -519,14 +519,6 @@ let refine_identifiers unseen_shifts raw_pb =
  *  Check arities 
  *******************************************************************************)
 
-(* computes the arity of a join *)
-let join_arity ar1 ar2 =
-  match (ar1, ar2) with
-  | Some a1, Some a2 ->
-      let res = a1 + a2 - 2 in
-      if res > 0 then Some res else None
-  | Some _, None | None, Some _ | None, None -> None
-
 let str_exp = Fmtc.to_to_string (Fmtc.hbox2 Ast.pp_exp)
 
 let compute_arities elo =
@@ -675,13 +667,19 @@ let compute_arities elo =
                 let ar = Some (a1 + a2) in
                 return_exp exp ar @@ rbinary e1' op e2'
             | None, _ | _, None -> return_exp exp None @@ rbinary e1' op e2')
-        | Join ->
-            let ar_join = join_arity ar1 ar2 in
-            if Option.is_none ar_join then
-              Result.fail
-              @@ Fmtc.str "wrong arities for the dot join of %s and %s"
-                   (str_exp e1') (str_exp e2')
-            else return_exp exp ar_join @@ rbinary e1' op e2')
+        | Join -> (
+            match (ar1, ar2) with
+            | Some _, None | None, Some _ | None, None ->
+                return_exp exp None @@ rbinary e1' op e2'
+            | Some a1, Some a2 ->
+                let res = a1 + a2 - 2 in
+                if res < 0 then
+                  Result.fail
+                  @@ Fmtc.str "wrong arities for the dot join of %s and %s"
+                       (str_exp e1') (str_exp e2')
+                else
+                  return_exp exp (if res > 0 then Some res else None)
+                  @@ rbinary e1' op e2'))
     | RIte (c, t, e) -> (
         let c' = walk_fml ctx c in
         let t' = walk_exp ctx t in

src/Smv.ml

@@ -476,7 +476,7 @@ module Make_SMV_file_format (Ltl : Solver.LTL) :
         pf out "%s@\n" elo_str;
         stratified_fml
         |> List.iter
-             (pf out "TRANS@\n[<hv2>%a@];@\n@\n"
+             (pf out "TRANS@\n@[<hv2>%a@];@\n@\n"
                 (Ltl.pp_gather_variables ~next_is_X:false bitwidth auxiliaries
                    variables)))
       trans;

test/test_aite.elo

@@ -0,0 +1,17 @@
+univ : { A#0 A#1 A#2 -4 -3 -2 -1 0 1 2 3 };
+
+const Int##min :1 { ( -4 ) };
+const Int##zero :1 { ( 0 ) };
+const Int##max :1 { ( 3 ) };
+const Int##next :2 { ( -4 -3 ) ( -3 -2 ) ( -2 -1 ) ( -1 0 ) ( 0 1 ) ( 1 2 ) ( 2 3 ) };
+const seq##Int :1 { ( 0 ) ( 1 ) ( 2 ) };
+const String :1 { };
+const this##A :1 { } { ( A#0 ) ( A#1 ) ( A#2 ) };
+var this##B :1 { } { ( A#0 ) ( A#1 ) ( A#2 ) };
+var this##C :1 { } { ( A#0 ) ( A#1 ) ( A#2 ) };
+const ints :1 { ( -4 ) ( -3 ) ( -2 ) ( -1 ) ( 0 ) ( 1 ) ( 2 ) ( 3 ) };
+
+run
+((this##B = this##C) iimplies
+ (#(this##B)) ielse
+ (#((ints + String) + this##A))) < (2);