WIP: Printer for marabou.

config/caisar-detection-data.conf

@@ -16,7 +16,7 @@ exec = "Marabou"
 version_switch = "--version"
 version_regexp = "\\([0-9.+]+\\)"
 version_ok  = "1.0.+"
-command = "%e --timeout %t %f"
+command = "%e %{nnet-onnx} %f"
 driver = "caisar_drivers/marabou.drv"
 use_at_auto_level = 1
 

config/drivers/marabou.drv

 (* Why3 drivers for Marabou *)
+
+printer "marabou"
+filename "%f-%t-%g.why"
+
+valid "^[Ss]at"
+invalid "^[Uu]nsat"
+timeout "^[Tt]imeout"
+unknown "^[Uu]nknown" ""
+
+transformation "inline_trivial"
+transformation "introduce_premises"
+transformation "eliminate_builtin"
+transformation "simplify_formula"
+transformation "native_nn_prover"
+transformation "vars_on_lhs"
+
+theory BuiltIn
+  syntax type int   "int"
+  syntax type real  "real"
+
+  syntax predicate (=)  "(%1 = %2)"
+
+  meta "eliminate_algebraic" "keep_enums"
+  meta "eliminate_algebraic" "keep_recs"
+
+end
+
+theory int.Int
+
+  prelude "(* this is a prelude for Alt-Ergo integer arithmetic *)"
+
+  syntax function zero "0"
+  syntax function one  "1"
+
+  syntax function (+)  "(%1 + %2)"
+  syntax function (-)  "(%1 - %2)"
+  syntax function (*)  "(%1 * %2)"
+  syntax function (-_) "(-%1)"
+
+  meta "invalid trigger" predicate (<=)
+  meta "invalid trigger" predicate (<)
+  meta "invalid trigger" predicate (>=)
+  meta "invalid trigger" predicate (>)
+
+  syntax predicate (<=) "(%1 <= %2)"
+  syntax predicate (<)  "(%1 <  %2)"
+  syntax predicate (>=) "(%1 >= %2)"
+  syntax predicate (>)  "(%1 >  %2)"
+
+  remove prop MulComm.Comm
+  remove prop MulAssoc.Assoc
+  remove prop Unit_def_l
+  remove prop Unit_def_r
+  remove prop Inv_def_l
+  remove prop Inv_def_r
+  remove prop Assoc
+  remove prop Mul_distr_l
+  remove prop Mul_distr_r
+  remove prop Comm
+  remove prop Unitary
+  remove prop Refl
+  remove prop Trans
+  remove prop Total
+  remove prop Antisymm
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
+  remove prop ZeroLessOne
+
+end
+
+theory int.EuclideanDivision
+
+  syntax function div "(%1 / %2)"
+  syntax function mod "(%1 % %2)"
+
+end
+
+theory int.ComputerDivision
+
+  use for_drivers.ComputerOfEuclideanDivision
+
+end
+
+
+theory real.Real
+
+  prelude "(* this is a prelude for Alt-Ergo real arithmetic *)"
+
+  syntax function zero "0.0"
+  syntax function one  "1.0"
+
+  syntax function (+)  "(%1 + %2)"
+  syntax function (-)  "(%1 - %2)"
+  syntax function (*)  "(%1 * %2)"
+  syntax function (/)  "(%1 / %2)"
+  syntax function (-_) "(-%1)"
+  syntax function inv  "(1.0 / %1)"
+
+  meta "invalid trigger" predicate (<=)
+  meta "invalid trigger" predicate (<)
+  meta "invalid trigger" predicate (>=)
+  meta "invalid trigger" predicate (>)
+
+  syntax predicate (<=) "(%1 <= %2)"
+  syntax predicate (<)  "(%1 <  %2)"
+  syntax predicate (>=) "(%1 >= %2)"
+  syntax predicate (>)  "(%1 >  %2)"
+
+  remove prop MulComm.Comm
+  remove prop MulAssoc.Assoc
+  remove prop Unit_def_l
+  remove prop Unit_def_r
+  remove prop Inv_def_l
+  remove prop Inv_def_r
+  remove prop Assoc
+  remove prop Mul_distr_l
+  remove prop Mul_distr_r
+  remove prop Comm
+  remove prop Unitary
+  remove prop Refl
+  remove prop Trans
+  remove prop Total
+  remove prop Antisymm
+  remove prop Inverse
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
+  remove prop ZeroLessOne
+
+end
+
+theory ieee_float.Float64
+
+  syntax function (.+)  "(%1 + %2)"
+  syntax function (.-)  "(%1 - %2)"
+  syntax function (.*)  "(%1 * %2)"
+  syntax function (./)  "(%1 / %2)"
+  syntax function (.-_) "(-%1)"
+
+  syntax predicate le "%1 <= %2"
+  syntax predicate lt  "%1 <  %2"
+  syntax predicate ge "%1 >= %2"
+  syntax predicate gt  "%1 >  %2"
+
+
+end
+
+theory real.RealInfix
+
+  syntax function (+.)  "(%1 + %2)"
+  syntax function (-.)  "(%1 - %2)"
+  syntax function ( *.) "(%1 * %2)"
+  syntax function (/.)  "(%1 / %2)"
+  syntax function (-._) "(-%1)"
+
+  meta "invalid trigger" predicate (<=.)
+  meta "invalid trigger" predicate (<.)
+  meta "invalid trigger" predicate (>=.)
+  meta "invalid trigger" predicate (>.)
+
+  syntax predicate (<=.) "(%1 <= %2)"
+  syntax predicate (<.)  "(%1 <  %2)"
+  syntax predicate (>=.) "(%1 >= %2)"
+  syntax predicate (>.)  "(%1 >  %2)"
+
+end
+
+theory Bool
+  syntax type     bool  "bool"
+  syntax function True  "true"
+  syntax function False "false"
+end
+
+theory Tuple0
+  syntax type     tuple0 "unit"
+  syntax function Tuple0 "void"
+end
+
+theory algebra.AC
+  meta AC function op
+  remove prop Comm
+  remove prop Assoc
+end
+
+theory ieee_float.Float64
+  syntax predicate is_not_nan ""
+  remove allprops
+end

config/dune

@@ -2,5 +2,6 @@
  (section (site (caisar config)))
  (files caisar-detection-data.conf
         (drivers/pyrat.drv as drivers/pyrat.drv)
+        (drivers/marabou.drv as drivers/marabou.drv)
  )
 (package caisar))

src/main.ml

@@ -9,9 +9,13 @@ open Cmdliner
 
 let caisar = "caisar"
 
-let () = Native_nn_prover.init ()
+let () =
+  Native_nn_prover.init ();
+  Vars_on_lhs.init ()
 
-let () = Pyrat.init ()
+let () =
+  Pyrat.init ();
+  Marabou.init ()
 
 (* -- Logs. *)
 

src/printers/marabou.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+type info = {
+  info_syn : Why3.Printer.syntax_map;
+  variables : string Why3.Term.Hls.t;
+}
+
+let number_format =
+  {
+    Why3.Number.long_int_support = `Default;
+    Why3.Number.negative_int_support = `Default;
+    Why3.Number.dec_int_support = `Default;
+    Why3.Number.hex_int_support = `Unsupported;
+    Why3.Number.oct_int_support = `Unsupported;
+    Why3.Number.bin_int_support = `Unsupported;
+    Why3.Number.negative_real_support = `Default;
+    Why3.Number.dec_real_support = `Default;
+    Why3.Number.hex_real_support = `Unsupported;
+    Why3.Number.frac_real_support = `Unsupported (fun _ _ -> assert false);
+  }
+
+let rec print_term info fmt t =
+  let open Why3 in
+  match t.Term.t_node with
+  | Tbinop ((Timplies | Tiff | Tor), _, _)
+  | Tnot _ | Ttrue | Tfalse | Tvar _ | Tlet _ | Tif _ | Tcase _ | Tquant _
+  | Teps _ ->
+    Printer.unsupportedTerm t "Not supported by Marabou"
+  | Tbinop (Tand, _, _) -> assert false (* Should appear only at top-level. *)
+  | Tconst c -> Constant.(print number_format unsupported_escape) fmt c
+  | Tapp (ls, l) -> (
+    match Printer.query_syntax info.info_syn ls.ls_name with
+    | Some s -> Printer.syntax_arguments s (print_term info) fmt l
+    | None -> (
+      match (Term.Hls.find_opt info.variables ls, l) with
+      | Some s, [] -> Fmt.string fmt s
+      | _ -> Printer.unsupportedTerm t "Unknown variable(s)"))
+
+let rec print_top_level_term info fmt t =
+  let open Why3 in
+  (* Don't print things we don't know. *)
+  let t_is_known =
+    Term.t_s_all
+      (fun _ -> true)
+      (fun ls ->
+        Ident.Mid.mem ls.ls_name info.info_syn || Term.Hls.mem info.variables ls)
+  in
+  match t.Term.t_node with
+  | Tquant _ -> ()
+  | Tbinop (Tand, t1, t2) ->
+    if t_is_known t1 && t_is_known t2
+    then
+      Fmt.pf fmt "%a%a"
+        (print_top_level_term info)
+        t1
+        (print_top_level_term info)
+        t2
+  | _ -> if t_is_known t then Fmt.pf fmt "%a@." (print_term info) t
+
+let print_decl info fmt d =
+  let open Why3 in
+  match d.Decl.d_node with
+  | Dtype _ -> ()
+  | Ddata _ -> ()
+  | Dparam _ -> ()
+  | Dlogic _ -> ()
+  | Dind _ -> ()
+  | Dprop (Decl.Plemma, _, _) -> assert false
+  | Dprop (Decl.Paxiom, _, f) -> print_top_level_term info fmt f
+  | Dprop (Decl.Pgoal, _, f) -> print_top_level_term info fmt f
+
+let rec print_tdecl info fmt task =
+  let open Why3 in
+  match task with
+  | None -> ()
+  | Some { Task.task_prev; task_decl; _ } -> (
+    print_tdecl info fmt task_prev;
+    match task_decl.Theory.td_node with
+    | Use _ | Clone _ -> ()
+    | Meta (meta, l) when Theory.meta_equal meta Native_nn_prover.meta_input
+      -> (
+      match l with
+      | [ MAls ls; MAint i ] -> Term.Hls.add info.variables ls (Fmt.str "x%i" i)
+      | _ -> assert false)
+    | Meta (meta, l) when Theory.meta_equal meta Native_nn_prover.meta_output
+      -> (
+      match l with
+      | [ MAls ls; MAint i ] -> Term.Hls.add info.variables ls (Fmt.str "y%i" i)
+      | _ -> assert false)
+    | Meta (_, _) -> ()
+    | Decl d -> print_decl info fmt d)
+
+let print_task args ?old:_ fmt task =
+  let open Why3 in
+  let info =
+    {
+      info_syn = Discriminate.get_syntax_map task;
+      variables = Term.Hls.create 10;
+    }
+  in
+  Printer.print_prelude fmt args.Printer.prelude;
+  print_tdecl info fmt task
+
+let init () =
+  Why3.Printer.register_printer ~desc:"Printer for the Marabou prover."
+    "marabou" print_task

src/transformations/native_nn_prover.ml

@@ -78,27 +78,29 @@ let simplify_goal env input_variables =
       | Decl decl ->
         let meta = ref [] in
         let hls = ref [] in
-        let map term =
-          let term = aux meta hls term in
-          if List.is_empty !hls
-          then term
-          else
-            let known =
-              List.fold !hls ~init:task_hd.task_known ~f:(fun acc (d, _, _) ->
-                Decl.known_add_decl acc d)
-            in
-            let engine =
-              Reduction_engine.create
-                {
-                  compute_defs = false;
-                  compute_builtin = true;
-                  compute_def_set = Term.Sls.empty;
-                }
-                env known
-            in
-            Reduction_engine.normalize ~limit:100 engine Term.Mvs.empty term
+        let decl =
+          Decl.decl_map
+            (fun term ->
+              let term = aux meta hls term in
+              if List.is_empty !hls
+              then term
+              else
+                let known =
+                  List.fold !hls ~init:task_hd.task_known
+                    ~f:(fun acc (d, _, _) -> Decl.known_add_decl acc d)
+                in
+                let engine =
+                  Reduction_engine.create
+                    {
+                      compute_defs = false;
+                      compute_builtin = true;
+                      compute_def_set = Term.Sls.empty;
+                    }
+                    env known
+                in
+                Reduction_engine.normalize ~limit:100 engine Term.Mvs.empty term)
+            decl
         in
-        let decl = Decl.decl_map map decl in
         let acc =
           List.fold !hls ~init:acc ~f:(fun acc (d, ls, i) ->
             let task = Task.add_decl acc d in

src/transformations/vars_on_lhs.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+let make_rt env =
+  let open Why3 in
+  let th = Env.read_theory env [ "ieee_float" ] "Float64" in
+  let le = Theory.ns_find_ls th.th_export [ "le" ] in
+  let lt = Theory.ns_find_ls th.th_export [ "lt" ] in
+  let ge = Theory.ns_find_ls th.th_export [ "ge" ] in
+  let gt = Theory.ns_find_ls th.th_export [ "gt" ] in
+  let rec rt t =
+    let t = Term.t_map rt t in
+    match t.t_node with
+    | Tapp
+        ( ls,
+          [
+            ({ t_node = Tconst _; _ } as const);
+            ({ t_node = Tapp (_, []); _ } as var);
+          ] ) ->
+      Fmt.pr "HERE: %a!@." Pretty.print_term t;
+      if Term.ls_equal ls le
+      then Term.ps_app ge [ var; const ]
+      else if Term.ls_equal ls ge
+      then Term.ps_app le [ var; const ]
+      else if Term.ls_equal ls lt
+      then Term.ps_app gt [ var; const ]
+      else if Term.ls_equal ls gt
+      then Term.ps_app lt [ var; const ]
+      else t
+    | _ -> t
+  in
+  rt
+
+let vars_on_lhs env =
+  let rt = make_rt env in
+  Why3.Trans.rewrite rt None
+
+let init () =
+  Why3.Trans.register_env_transform
+    ~desc:
+      "Transformation for provers that need variables on the left-hand-side of \
+       logic symbols."
+    "vars_on_lhs" vars_on_lhs

src/verification.ml

@@ -49,6 +49,7 @@ let call_prover ~limit prover driver task =
 
 let verify format loadpath ?memlimit ~prover file =
   let open Why3 in
+  (* Debug.(set_flag (lookup_flag "call_prover")); *)
   let env, config = create_env loadpath in
   let steplimit = None in
   let timeout = None in