Remove alt-ergo-lib pin and make it compile with 2.6.0

By doing this we had to disable model generation for the alt-ergo solver
formalsec · Mar 7, 2025 · 9331fc9 · 9331fc9
1 parent ab18f81
commit 9331fc9
Show file tree

Hide file tree

Showing 7 changed files with 85 additions and 87 deletions.
diff --git a/doc/dune b/doc/dune
@@ -8,6 +8,7 @@
  (enabled_if
   (and
    %{lib-available:z3}
+   (not %{lib-available:alt-ergo-lib})
    (not %{lib-available:bitwuzla-cxx})
    (not %{lib-available:colibri2.core})
    (not %{lib-available:cvc5})))

diff --git a/dune b/dune
@@ -2,6 +2,7 @@
  (enabled_if
   (and
    %{lib-available:z3}
+   (not %{lib-available:alt-ergo-lib})
    (not %{lib-available:bitwuzla-cxx})
    (not %{lib-available:colibri2.core})
    (not %{lib-available:cvc5}))))
diff --git a/smtml.opam b/smtml.opam
@@ -73,7 +73,6 @@ available: arch != "arm32" & arch != "x86_32"
 pin-depends: [
   ["colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#e15e6fc52b1f4e9a015b630a1f377d203ed9ec5b"]
   ["colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#e15e6fc52b1f4e9a015b630a1f377d203ed9ec5b"]
-  ["alt-ergo-lib.2.6.0" "git+https://github.com/OCamlPro/alt-ergo.git#7ee96296a5de9588a4d585b3b8abec35f4755425"]
   ["cvc5.dev" "git+https://github.com/formalsec/ocaml-cvc5.git#b7aade52d49a19d646036d7e6aac09039c3e95cf"]
   ["benchpress.dev" "git+https://github.com/sneeuwballen/benchpress.git#7f44cdd9f0511afcce2c9ad3c04cc9b72919bcff"]
   ["extunix.0.4.3" "git+https://github.com/filipeom/extunix.git#ff54e8cc7ec9cdc7171861d74d85f326dbcec62e"]

diff --git a/smtml.opam.template b/smtml.opam.template
@@ -2,7 +2,6 @@ available: arch != "arm32" & arch != "x86_32"
 pin-depends: [
   ["colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#e15e6fc52b1f4e9a015b630a1f377d203ed9ec5b"]
   ["colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#e15e6fc52b1f4e9a015b630a1f377d203ed9ec5b"]
-  ["alt-ergo-lib.2.6.0" "git+https://github.com/OCamlPro/alt-ergo.git#7ee96296a5de9588a4d585b3b8abec35f4755425"]
   ["cvc5.dev" "git+https://github.com/formalsec/ocaml-cvc5.git#b7aade52d49a19d646036d7e6aac09039c3e95cf"]
   ["benchpress.dev" "git+https://github.com/sneeuwballen/benchpress.git#7f44cdd9f0511afcce2c9ad3c04cc9b72919bcff"]
   ["extunix.0.4.3" "git+https://github.com/filipeom/extunix.git#ff54e8cc7ec9cdc7171861d74d85f326dbcec62e"]

diff --git a/src/smtml/altergo_mappings.default.ml b/src/smtml/altergo_mappings.default.ml
@@ -101,7 +101,7 @@ module Fresh = struct
             if ConstMap.mem c sym_acc then sym_acc
             else
               let mk_res =
-                AEL.Translate.make dummy_file []
+                AEL.D_cnf.make dummy_file []
                   (mk_dstmt (`Decls [ `Term_decl c ]))
               in
               match mk_res with
@@ -112,7 +112,7 @@ module Fresh = struct
       let mk_cmds sym_acc e_acc el =
         let new_syms, stl = exprl_stmtl el in
         let sym_acc = mk_decls new_syms sym_acc in
-        let mk_res = AEL.Translate.make dummy_file e_acc stl in
+        let mk_res = AEL.D_cnf.make dummy_file e_acc stl in
         (sym_acc, mk_res)
 
       let add s el =
@@ -245,78 +245,83 @@ module Fresh = struct
               Fmt.failwith "Altergo_mappings: dvalue_to_value(%a)"
                 DM.Value.print v ) ) )
 
-    let cgraph_to_value hs g =
-      match (g : AEL.ModelMap.graph) with
-      | Free e -> e
-      | C c when AEL.ModelMap.M.cardinal c = 1 -> (
-        match AEL.ModelMap.M.min_binding c with [], e -> e | _ -> assert false )
-      | C c ->
-        (* Currently, there are no uninterpred functions in the tests/benchs,
-           therefore this is ok, but it should be fixed in the future *)
-        Fmt.failwith "Altergo_mappings: no value for %a (%a)" AEL.Id.pp hs
-          (fun fmt m ->
-            AEL.ModelMap.M.iter
-              (fun k v ->
-                Fmt.pf fmt "[%a] -> %a; "
-                  (Fmt.list ~sep:Fmt.comma AEL.Expr.print)
-                  k AEL.Expr.print v )
-              m )
-          c
-
-    let value (Model ((module Sat), m) : model) (e : Expr.t) : Value.t =
-      match Sat.get_model m with
-      | None -> Fmt.failwith "Altergo_mappings: no value for (%a)" Expr.pp e
-      | Some AEL.Models.{ model; _ } ->
-        let m =
-          AEL.ModelMap.fold
-            (fun ((hs, _, _) as id) g acc ->
-              let e = cgraph_to_value hs g in
-              let tcst = Dolmenexpr_to_expr.tcst_of_symbol (aeid_to_sym id) in
-              DM.Model.Cst.add tcst (ae_expr_to_dvalue e) acc )
-            model DM.Model.empty
-        in
-        let env =
-          DM.Env.mk m
-            ~builtins:
-              (DM.Eval.builtins
-                 [ DM.Core.builtins
-                 ; DM.Bool.builtins
-                 ; DM.Int.builtins
-                 ; DM.Rat.builtins
-                 ; DM.Real.builtins
-                 ; DM.Bitv.builtins
-                   (* ; Array.builtins
-                      ; Fp.builtins *)
-                 ] )
-        in
-        let v = DM.Eval.eval env (encode_expr e) in
-        dvalue_to_value (Expr.ty e) v
-
-    let values_of_model ?symbols (Model ((module Sat), m)) : Model.t =
-      match Sat.get_model m with
-      | None -> assert false
-      | Some AEL.Models.{ model; _ } -> (
-        let r = Hashtbl.create 17 in
-        match symbols with
-        | None ->
-          AEL.ModelMap.fold
-            (fun ((hs, _, _) as aeid) g () ->
-              let sym = aeid_to_sym aeid in
-              Hashtbl.add r sym (ae_expr_to_value (cgraph_to_value hs g)) )
-            model ();
-          r
-        | Some syml ->
-          List.iter
-            (fun sym ->
-              let ((hs, _, _) as aeid) = sym_to_aeid sym in
-              let e =
-                try cgraph_to_value hs (AEL.ModelMap.find aeid model)
-                with Not_found ->
-                  Fmt.failwith "Altergo_mappings: no value for %a" AEL.Id.pp hs
-              in
-              Hashtbl.add r sym (ae_expr_to_value e) )
-            syml;
-          r )
+    let cgraph_to_value _hs _g =
+      (* match (g : AEL.ModelMap.graph) with *)
+      (* | Free e -> e *)
+      (* | C c when AEL.ModelMap.M.cardinal c = 1 -> ( *)
+      (*   match AEL.ModelMap.M.min_binding c with [], e -> e | _ -> assert false ) *)
+      (* | C c -> *)
+      (*   (1* Currently, there are no uninterpred functions in the tests/benchs, *)
+      (*      therefore this is ok, but it should be fixed in the future *1) *)
+      (*   Fmt.failwith "Altergo_mappings: no value for %a (%a)" AEL.Id.pp hs *)
+      (*     (fun fmt m -> *)
+      (*       AEL.ModelMap.M.iter *)
+      (*         (fun k v -> *)
+      (*           Fmt.pf fmt "[%a] -> %a; " *)
+      (*             (Fmt.list ~sep:Fmt.comma AEL.Expr.print) *)
+      (*             k AEL.Expr.print v ) *)
+      (*         m ) *)
+      (*     c *)
+      assert false (* This function should never be reached *)
+
+    let value (Model ((module Sat), _m) : model) (_e : Expr.t) : Value.t =
+      (* match Sat.get_model m with *)
+      (* | None -> Fmt.failwith "Altergo_mappings: no value for (%a)" Expr.pp e *)
+      (* | Some AEL.Models.{ model; _ } -> *)
+      (*   let m = *)
+      (*     AEL.ModelMap.fold *)
+      (*       (fun ((hs, _, _) as id) g acc -> *)
+      (*         let e = cgraph_to_value hs g in *)
+      (*         let tcst = Dolmenexpr_to_expr.tcst_of_symbol (aeid_to_sym id) in *)
+      (*         DM.Model.Cst.add tcst (ae_expr_to_dvalue e) acc ) *)
+      (*       model DM.Model.empty *)
+      (*   in *)
+      (*   let env = *)
+      (*     DM.Env.mk m *)
+      (*       ~builtins: *)
+      (*         (DM.Eval.builtins *)
+      (*            [ DM.Core.builtins *)
+      (*            ; DM.Bool.builtins *)
+      (*            ; DM.Int.builtins *)
+      (*            ; DM.Rat.builtins *)
+      (*            ; DM.Real.builtins *)
+      (*            ; DM.Bitv.builtins *)
+      (*              (1* ; Array.builtins *)
+      (*                 ; Fp.builtins *1) *)
+      (*            ] ) *)
+      (*   in *)
+      (*   let v = DM.Eval.eval env (encode_expr e) in *)
+      (*   dvalue_to_value (Expr.ty e) v *)
+      Fmt.failwith
+        "Altergo_mappings: model generation is currently unsupported!"
+
+    let values_of_model ?symbols:_ (Model ((module Sat), _m)) : Model.t =
+      (* match Sat.get_model m with *)
+      (* | None -> assert false *)
+      (* | Some AEL.Models.{ model; _ } -> ( *)
+      (*   let r = Hashtbl.create 17 in *)
+      (*   match symbols with *)
+      (*   | None -> *)
+      (*     AEL.ModelMap.fold *)
+      (*       (fun ((hs, _, _) as aeid) g () -> *)
+      (*         let sym = aeid_to_sym aeid in *)
+      (*         Hashtbl.add r sym (ae_expr_to_value (cgraph_to_value hs g)) ) *)
+      (*       model (); *)
+      (*     r *)
+      (*   | Some syml -> *)
+      (*     List.iter *)
+      (*       (fun sym -> *)
+      (*         let ((hs, _, _) as aeid) = sym_to_aeid sym in *)
+      (*         let e = *)
+      (*           try cgraph_to_value hs (AEL.ModelMap.find aeid model) *)
+      (*           with Not_found -> *)
+      (*             Fmt.failwith "Altergo_mappings: no value for %a" AEL.Id.pp hs *)
+      (*         in *)
+      (*         Hashtbl.add r sym (ae_expr_to_value e) ) *)
+      (*       syml; *)
+      (*     r ) *)
+      Fmt.failwith
+        "Altergo_mappings: model generation is currently unsupported!"
 
     let set_debug _ = ()
   end

diff --git a/test/solver/test_solver_altergo.expected b/test/solver/test_solver_altergo.expected
@@ -1,7 +0,0 @@
-(model
-  (x int 0))
-(model
-  (w i32 4)
-  (x i32 1)
-  (y i32 2)
-  (z i32 3))

diff --git a/test/solver/test_solver_altergo.ml b/test/solver/test_solver_altergo.ml
@@ -6,7 +6,7 @@ let () =
   assert Altergo_mappings.is_available;
   let module Alt_ergo = Test_solver.Make (Altergo_mappings.Fresh.Make ()) in
   Alt_ergo.test_params ();
-  Alt_ergo.test_cached ();
-  Alt_ergo.test ();
-  Alt_ergo.test_bv ();
-  Alt_ergo.test_lia ()
+  (* Alt_ergo.test_cached (); *)
+  (* Alt_ergo.test (); *)
+  (* Alt_ergo.test_bv (); *)
+  (* Alt_ergo.test_lia () *)