wrap around for integer terms added in Solver file and called in Ltl …

…smart constructor num

src/Elo_to_ltl1.ml

@@ -179,9 +179,9 @@ module Make (Ltl : Solver.LTL) = struct
         | None -> pairs)
       empty r_sup_seq
 
-  (* Produces the LTL formula corresponding to [SUM_(t \in on) f(t)]  *)
+  (* Produces the integer term corresponding to [SUM_(t \in on) f(t)]  *)
   let summation ~(on : TS.t) (f : Tuple.t -> term) : term =
-    on |> TS.to_iter |> Iter.fold (fun t1 t2 -> plus t1 (f t2)) (num 0)
+    on |> TS.to_iter |> Iter.fold (fun t1 t2 -> plus t1 (f t2)) (num 2 0)
 
   class environment (elo : Elo.t) =
     (* Atomic.make is a cached function for its last two arguments (out of 3), so we compute it for its first argument to avoid unnecessary recomputations *)
@@ -225,7 +225,7 @@ module Make (Ltl : Solver.LTL) = struct
 
       method build_Card subst r r' =
         let { must; may; _ } = env#must_may_sup subst r in
-        let must_card = num @@ TS.size must in
+        let must_card = num env#bitwidth (TS.size must) in
         let may_card = count @@ List.map r' @@ TS.to_list may in
         plus must_card may_card
 
@@ -330,11 +330,11 @@ module Make (Ltl : Solver.LTL) = struct
         else false_
 
       (* same reasoning as for visit_Compr *)
-      method! visit_Sum env _visitors_c0 _visitors_c1 =
-        let _visitors_r0 = self#visit_'exp env _visitors_c0 in
+      method! visit_Sum env2 _visitors_c0 _visitors_c1 =
+        let _visitors_r0 = self#visit_'exp env2 _visitors_c0 in
         (* min_int as a dummy default value to ignore later on *)
-        let _visitors_r1 = num @@ Int.min_int in
-        self#build_Sum env _visitors_c0 _visitors_c1 _visitors_r0 _visitors_r1
+        let _visitors_r1 = num env#bitwidth Int.min_int in
+        self#build_Sum env2 _visitors_c0 _visitors_c1 _visitors_r0 _visitors_r1
 
       (* [| sum x : r | ie |]_sigma =
          Sum_{t in must(r)} [|ie|]_sigma[x |-> t]
@@ -346,7 +346,7 @@ module Make (Ltl : Solver.LTL) = struct
         let must_part = summation ~on:must ie' in
         let may_part =
           summation ~on:may (fun t ->
-              ifthenelse_arith (self#visit_exp subst r t) (ie' t) (num 0))
+              ifthenelse_arith (self#visit_exp subst r t) (ie' t) (num env#bitwidth 0))
         in
         plus must_part may_part
 
@@ -425,7 +425,7 @@ module Make (Ltl : Solver.LTL) = struct
       method build_NotIn (subst : stack) r s r' s' =
         not_ @@ self#build_In subst r s r' s'
 
-      method build_Num (_ : stack) n _ = num n
+      method build_Num (_ : stack) n _ = num env#bitwidth n
       method build_O (_ : stack) (a : ltl) : ltl = once a
       method build_Or (_ : stack) (a : ltl) (b : ltl) : ltl = or_ a (lazy b)
 

src/Solver.ml

@@ -17,6 +17,18 @@ open Containers
 [@@@warning "-4"]
 [@@@warning "-32"]
 
+let wrap bw n =
+  let interval_length = Int.pow 2 bw in
+  let maxint = Int.pow (2-1) bw in
+  if (n > maxint -1) then
+    ((n + maxint) mod interval_length) - maxint
+  else
+    if (n < ~-maxint) then
+      ((n + maxint) mod interval_length) + interval_length
+    else
+      n
+
+
 (* fragile patterns, lots of them as we short-circuit *)
 
 module type ATOMIC_PROPOSITION = sig
@@ -98,7 +110,7 @@ module type LTL = sig
   val releases : t -> t -> t
   val since : t -> t -> t
   val triggered : t -> t -> t
-  val num : int -> term
+  val num : int -> int -> term
   val plus : term -> term -> term
   val minus : term -> term -> term
   val neg : term -> term
@@ -295,7 +307,7 @@ struct
   (* let neg t = Neg t *)
   (* let comp op t1 t2 = Comp (op, t1, t2) *)
 
-  let num n = Num n
+  let num bw n = Num (wrap bw n)
 
   let plus t1 t2 =
     match (t1, t2) with
@@ -308,7 +320,7 @@ struct
 
   let count ps =
     match List.filter (function False -> false | _ -> true) ps with
-    | [] -> num 0
+    | [] -> Num 0
     | props -> Count props
 
   let ifthenelse_arith c t e =

src/Solver.mli

@@ -108,7 +108,7 @@ module type LTL = sig
   val releases : t -> t -> t
   val since : t -> t -> t
   val triggered : t -> t -> t
-  val num : int -> term
+  val num : int -> int -> term
   val plus : term -> term -> term
   val minus : term -> term -> term
   val neg : term -> term