fix pp typo; fix wrong arity handling for join

grayswandyr · May 23, 2024 · 578eda0 · 578eda0
1 parent 4e04783
commit 578eda0
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 16 deletions.
diff --git a/src/Raw_to_ast.ml b/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

diff --git a/src/Smv.ml b/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;