Fmt and menhir constraints

dune-project

@@ -24,7 +24,10 @@
    dune
    (ocaml (>= "4.14.0"))
    (z3 (and (>= "4.12.2") (< "4.13")))
-   menhir
+   (menhir
+    (and
+    :build
+    (>= 20220210)))
    (cmdliner (>= "1.2.0"))
    (zarith (>= "1.5"))
    (ppx_inline_test :with-test)

encoding.opam

@@ -12,7 +12,7 @@ depends: [
   "dune" {>= "3.0"}
   "ocaml" {>= "4.14.0"}
   "z3" {>= "4.12.2" & < "4.13"}
-  "menhir"
+  "menhir" {build & >= "20220210"}
   "cmdliner" {>= "1.2.0"}
   "zarith" {>= "1.5"}
   "ppx_inline_test" {with-test}

lib/ast.ml

@@ -9,10 +9,8 @@ let pp fmt (instr : t) =
   | Declare s ->
     let ty = Symbol.type_of s in
     Format.fprintf fmt "(declare-fun %a %a)" Symbol.pp s Ty.pp ty
-  | Assert e ->
-      Format.fprintf fmt "(assert @[<h 2>%a@])" Expr.pp e
+  | Assert e -> Format.fprintf fmt "(assert @[<h 2>%a@])" Expr.pp e
   | CheckSat -> Format.pp_print_string fmt "(check-sat)"
   | GetModel -> Format.pp_print_string fmt "(get-model)"
 
-let to_string (instr : t) : string =
-  Format.asprintf "%a" pp instr
+let to_string (instr : t) : string = Format.asprintf "%a" pp instr

lib/expr.ml

@@ -88,7 +88,7 @@ let negate_relop ({ e; ty } : t) : (t, string) Result.t =
 module Pp = struct
   let fprintf = Format.fprintf
 
-  let rec pp fmt ({ e; ty} : t) =
+  let rec pp fmt ({ e; ty } : t) =
     match e with
     | Val v -> Value.pp fmt v
     | Ptr (base, offset) -> fprintf fmt "(Ptr (i32 %ld) %a)" base pp offset

lib/interpret.ml

@@ -20,8 +20,7 @@ module Make (Solver : Solver_intf.S) = struct
     let { solver; pc; _ } = state in
     let st pc = { state with pc } in
     match stmt with
-    | Declare _x ->
-      st pc
+    | Declare _x -> st pc
     | Assert e ->
       Solver.add solver [ e ];
       st (e :: pc)

lib/params.mli

@@ -7,11 +7,7 @@ type _ param =
 type t
 
 val default_value : 'a param -> 'a
-
 val default : unit -> t
-
 val ( & ) : t -> 'a param * 'a -> t
-
 val set : t -> 'a param -> 'a -> t
-
 val get : t -> 'a param -> 'a

test/test_axiom.ml

@@ -2,7 +2,6 @@ open Encoding
 module Batch = Solver.Batch (Z3_mappings)
 
 let solver = Batch.create ()
-
 let () = Batch.add solver Axioms.axioms
 
 let%test _ =