fix small bugs + add biwidth in elo_to_ltl1

grayswandyr · Apr 30, 2024 · 7985916 · 7985916
1 parent fac59c1
commit 7985916
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 12 deletions.
diff --git a/src/Domain.ml b/src/Domain.ml
@@ -113,19 +113,19 @@ let log2 n =
 
 let compute_bitwidth =
   let exception Int_problem in
+  let tuple_of_int nb =
+    Tuple.tuple1 @@ Atom.of_raw_ident
+    @@ Raw_ident.ident (string_of_int nb) Lexing.dummy_pos Lexing.dummy_pos
+  in
   let check_int_set ints =
     let bitwidth = log2 (Tuple_set.size ints) in
     if
       bitwidth = 0
-      || Iter.(
-           for_all
-             (fun nb ->
-               Tuple_set.mem
-                 (Tuple.tuple1 @@ Atom.of_raw_ident
-                 @@ Raw_ident.ident (string_of_int nb) Lexing.dummy_pos
-                      Lexing.dummy_pos)
-                 ints)
-             (~-(Int.pow 2 (bitwidth - 1)) -- (Int.pow 2 (bitwidth - 1) - 1)))
+      || bitwidth > 0
+         && Iter.(
+              for_all
+                (fun nb -> Tuple_set.mem (tuple_of_int nb) ints)
+                (~-(Int.pow 2 (bitwidth - 1)) -- (Int.pow 2 (bitwidth - 1) - 1)))
     then bitwidth
     else raise Int_problem
   in

diff --git a/src/Elo_to_ltl1.ml b/src/Elo_to_ltl1.ml
@@ -198,12 +198,14 @@ module Make (Ltl : Solver.LTL) = struct
         | Some rel -> Relation.arity rel
 
       method make_atom (name : Name.t) (t : Tuple.t) =
-        assert (Domain.mem name elo.Elo.domain);
+        assert (Domain.mem name elo.domain);
         Ltl.atomic @@ make_atom_aux name t
 
       method is_const (name : Name.t) =
         assert (Domain.mem name elo.Elo.domain);
         Domain.get_exn name elo.Elo.domain |> Relation.is_const
+
+      method bitwidth = Domain.bitwidth elo.domain
     end
 
   class ['subst] converter (env : environment) =
@@ -346,7 +348,6 @@ module Make (Ltl : Solver.LTL) = struct
           summation ~on:may (fun t ->
               ifthenelse_arith (self#visit_exp subst r t) (ie' t) (num 0))
         in
-
         plus must_part may_part
 
       method build_Diff (_ : stack) (_ : G.exp) (_ : G.exp) e' f'

diff --git a/src/Smv.ml b/src/Smv.ml
@@ -195,7 +195,7 @@ module Make_SMV_LTL (At : Solver.ATOMIC_PROPOSITION) :
       and pp_term upper out (t : term) =
         match t with
         | Num n ->
-            if n < 0 then pf out "-0sd%d_%d" bitwidth n
+            if n < 0 then pf out "-0sd%d_%d" bitwidth (-n)
             else pf out "0sd%d_%d" bitwidth n
         | Bin (t1, Plus, t2) ->
             infixl ~paren:true upper 7 string pp_term pp_term out ("+", t1, t2)