Merge pull request #227 from CatalaLang/afromher_z3

Proof platform: Better error message when Z3 encoding not supported, and extend GetYear support

compiler/lcalc/ast.ml

@@ -134,7 +134,9 @@ let make_matchopt_with_abs_arms
     (e_some : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box =
   let pos = Pos.get_position @@ Bindlib.unbox arg in
   let mark : 'a -> 'a Pos.marked = Pos.mark pos in
-  let+ arg = arg and+ e_none = e_none and+ e_some = e_some [@ocamlformat "disable"] in
+  let+ arg = arg
+  and+ e_none = e_none
+  and+ e_some = e_some [@ocamlformat "disable"] in
 
   mark @@ EMatch (arg, [ e_none; e_some ], option_enum)
 

compiler/verification/io.ml

@@ -179,5 +179,10 @@ module MakeBackendIO (B : Backend) = struct
             Cli.error_print "%s" (print_negative_result vc backend_ctx model)
         | Unknown ->
             failwith "The solver failed at proving or disproving the VC")
-    | Fail msg -> Cli.error_print "The translation to Z3 failed:@\n%s" msg
+    | Fail msg ->
+        Cli.error_print "%s The translation to Z3 failed:\n%s"
+          (Cli.with_style [ ANSITerminal.yellow ] "[%s.%s]"
+             (Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
+             (Bindlib.name_of (Pos.unmark vc.vc_variable)))
+          msg
 end

compiler/verification/z3backend.real.ml

@@ -475,6 +475,24 @@ let rec translate_op
              thus be directly translated as >= in the Z3 encoding using the
              number of days *)
           (ctx, Arithmetic.mk_ge ctx.ctx_z3 e1 e2)
+      | Eq, [ (EApp ((EOp (Unop GetYear), _), [ e1 ]), _); (ELit (LInt n), _) ]
+        ->
+          let n = Runtime.integer_to_int n in
+          let ctx, e1 = translate_expr ctx e1 in
+          let min_date =
+            Arithmetic.Integer.mk_numeral_i ctx.ctx_z3
+              (date_to_int (date_of_year n))
+          in
+          let max_date =
+            Arithmetic.Integer.mk_numeral_i ctx.ctx_z3
+              (date_to_int (date_of_year (n + 1)))
+          in
+          ( ctx,
+            Boolean.mk_and ctx.ctx_z3
+              [
+                Arithmetic.mk_ge ctx.ctx_z3 e1 min_date;
+                Arithmetic.mk_lt ctx.ctx_z3 e1 max_date;
+              ] )
       | _ -> (
           let ctx, e1, e2 =
             match args with