[trans] Add transformation for simplifying linear inequalities.

config/drivers/marabou.drv

@@ -34,6 +34,7 @@ transformation "inline_trivial"
 transformation "introduce_premises"
 transformation "eliminate_builtin"
 transformation "simplify_formula"
+transformation "simplify_rel"
 transformation "vars_on_lhs"
 
 theory BuiltIn

config/drivers/pyrat.drv

@@ -34,6 +34,7 @@ transformation "inline_trivial"
 transformation "introduce_premises"
 transformation "eliminate_builtin"
 transformation "simplify_formula"
+transformation "simplify_rel"
 
 theory BuiltIn
   syntax type int   "int"

config/drivers/vnnlib.gen

@@ -32,6 +32,7 @@ transformation "inline_trivial"
 transformation "introduce_premises"
 transformation "eliminate_builtin"
 transformation "simplify_formula"
+transformation "simplify_rel"
 transformation "vars_on_lhs"
 
 theory BuiltIn

src/main.ml

@@ -25,13 +25,15 @@ open Cmdliner
 
 let caisar = "caisar"
 
+let () =
+  Simplify_rel.init ();
+  Vars_on_lhs.init ()
+
 let () =
   Pyrat.init ();
   Marabou.init ();
   Vnnlib.init ()
 
-let () = Vars_on_lhs.init ()
-
 (* -- Logs. *)
 
 let pp_header =

src/transformations/simplify_rel.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(*  Copyright (C) 2022                                                    *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  You can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the          *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Why3
+open Base
+
+let float_of_real_constant rc =
+  let is_neg, rc =
+    (BigInt.lt rc.Number.rl_real.rv_sig BigInt.zero, Number.abs_real rc)
+  in
+  let rc_str = Fmt.str "%a" Number.(print_real_constant full_support) rc in
+  let f = Float.of_string rc_str in
+  if is_neg then Float.neg f else f
+
+let real_constant_of_float value =
+  let neg = Float.is_negative value in
+  let value = Fmt.str "%.64f" (Float.abs value) in
+  (* Split into integer and fractional parts. *)
+  let int_frac = String.split value ~on:'.' in
+  let int = List.hd_exn int_frac in
+  let frac =
+    match List.tl_exn int_frac with
+    | [] -> ""
+    | [ s ] -> s
+    | _ -> assert false (* Since every float has one '.' at most. *)
+  in
+  Constant.ConstReal (Number.real_literal ~radix:10 ~neg ~int ~frac ~exp:None)
+
+let term_of_float env f =
+  let th = Env.read_theory env [ "ieee_float" ] "Float64" in
+  let ty = Ty.ty_app (Theory.ns_find_ts th.th_export [ "t" ]) [] in
+  Term.t_const (real_constant_of_float f) ty
+
+let make_rt env =
+  let th = Env.read_theory env [ "ieee_float" ] "Float64" in
+  let ty = Ty.ty_app (Theory.ns_find_ts th.th_export [ "t" ]) [] in
+  let le_fp = Theory.ns_find_ls th.th_export [ "le" ] in
+  let lt_fp = Theory.ns_find_ls th.th_export [ "lt" ] in
+  let ge_fp = Theory.ns_find_ls th.th_export [ "ge" ] in
+  let gt_fp = Theory.ns_find_ls th.th_export [ "gt" ] in
+  let rel_fp = [ le_fp; lt_fp; ge_fp; gt_fp ] in
+  let add_fp = Theory.ns_find_ls th.th_export [ "add" ] in
+  let sub_fp = Theory.ns_find_ls th.th_export [ "sub" ] in
+  let mul_fp = Theory.ns_find_ls th.th_export [ "mul" ] in
+  let div_fp = Theory.ns_find_ls th.th_export [ "div" ] in
+  let neg_fp = Theory.ns_find_ls th.th_export [ "neg" ] in
+  let op_fp = [ add_fp; sub_fp; mul_fp; div_fp; neg_fp ] in
+  let rec rt t =
+    let t = Term.t_map rt t in
+    match t.t_node with
+    | Tapp (ls, [ { t_node = Tconst (ConstReal rc); _ } ])
+      when Term.ls_equal ls neg_fp ->
+      let rc = Number.neg_real rc in
+      Term.t_const (ConstReal rc) ty
+    | Tapp
+        ( ls_rel,
+          [
+            { t_node = Tconst (ConstReal rc1); _ };
+            {
+              t_node =
+                Tapp
+                  (ls_op, [ _mode; t'; { t_node = Tconst (ConstReal rc2); _ } ]);
+              _;
+            };
+          ] )
+      when List.exists ~f:(Term.ls_equal ls_rel) rel_fp
+           && List.exists ~f:(Term.ls_equal ls_op) op_fp ->
+      let rc1_float = float_of_real_constant rc1 in
+      let rc2_float = float_of_real_constant rc2 in
+      let op_float =
+        if Term.ls_equal ls_op sub_fp
+        then Float.( + )
+        else if Term.ls_equal ls_op add_fp
+        then Float.( - )
+        else if Term.ls_equal ls_op mul_fp
+        then Float.( / )
+        else if Term.ls_equal ls_op div_fp
+        then Float.( * )
+        else assert false
+      in
+      let rc_float = op_float rc1_float rc2_float in
+      let rc_t = term_of_float env rc_float in
+      let t = Term.t_app_infer ls_rel [ rc_t; t' ] in
+      rt t
+    | Tapp
+        ( ls_rel,
+          [
+            {
+              t_node =
+                Tapp
+                  (ls_op, [ _mode; t'; { t_node = Tconst (ConstReal rc2); _ } ]);
+              _;
+            };
+            { t_node = Tconst (ConstReal rc1); _ };
+          ] )
+      when List.exists ~f:(Term.ls_equal ls_rel) rel_fp
+           && List.exists ~f:(Term.ls_equal ls_op) op_fp ->
+      let rc1_float = float_of_real_constant rc1 in
+      let rc2_float = float_of_real_constant rc2 in
+      let op_float =
+        if Term.ls_equal ls_op sub_fp
+        then Float.( + )
+        else if Term.ls_equal ls_op add_fp
+        then Float.( - )
+        else if Term.ls_equal ls_op mul_fp
+        then Float.( / )
+        else if Term.ls_equal ls_op div_fp
+        then Float.( * )
+        else assert false
+      in
+      let rc_float = op_float rc1_float rc2_float in
+      let rc_t = term_of_float env rc_float in
+      let t = Term.t_app_infer ls_rel [ t'; rc_t ] in
+      rt t
+    | _ -> t
+  in
+  rt
+
+let simplify_rel env =
+  let rt = make_rt env in
+  Trans.rewrite rt None
+
+let init () =
+  Trans.register_env_transform
+    ~desc:"Simplify linear inequalities with float values." "simplify_rel"
+    simplify_rel

src/transformations/simplify_rel.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(*  Copyright (C) 2022                                                    *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  You can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the          *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+val init : unit -> unit
+(** Register the transformation. *)

tests/interpretation_acasxu.t

 Test interpret on acasxu
-  $ caisar verify -L . --format whyml --prover PyRAT --prover-altern ACAS - 2>&1 <<EOF | ./filter_tmpdir.sh
+
+  $ chmod u+x bin/pyrat.py
+
+  $ bin/pyrat.py --version
+  PyRAT 1.1
+
+  $ PATH=$(pwd)/bin:$PATH
+
+  $ caisar verify -L . --format whyml --prover PyRAT - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory T
   >   use ieee_float.Float64
   >   use bool.Bool
@@ -34,7 +42,7 @@ Test interpret on acasxu
   >     /\ (100.0:t) .<= i[speed] .<= (1200.0:t)
   >     /\ (0.0:t) .<= i[intruder_speed] .<= (1200.0:t)
   > 
-  >   predicate valid_action (a: action) = 0 <= a <= 4
+  >   predicate valid_action (a: action) = clear_of_conflict <= a <= strong_right
   > 
   >   predicate advises (c: classifier) (i: input) (a: action) =
   >     valid_action a ->
@@ -76,10 +84,10 @@ Test interpret on acasxu
   > 
   >   predicate moving_towards (i: input) =
   >     i[intruder_heading] .>= (3.100000000000000088817841970012523233890533447265625:t)
-  >     /\ i[speed] .>= (900.0:t)
+  >     /\ i[speed] .>= (980.0:t)
   >     /\ i[intruder_speed] .>= (960.0:t)
   > 
-  >   goal P2:
+  >   goal P3:
   >     forall i: input.
   >       has_length i 5 ->
   >       let j = denormalize_input i in
@@ -87,5 +95,5 @@ Test interpret on acasxu
   >       not (advises classifier i clear_of_conflict)
   > end
   > EOF
-  [caisar] Goal P1: High failure
-  [caisar] Goal P2: High failure
+  [caisar] Goal P1: Unknown ()
+  [caisar] Goal P3: Unknown ()

tests/interpretation_dataset.t

@@ -4,6 +4,13 @@ Test interpret on dataset
   > 0,1.0,0.0,0.019607843,0.776470588,0.784313725
   > EOF
 
+  $ chmod u+x bin/Marabou
+
+  $ bin/Marabou --version
+  1.0.+
+
+  $ PATH=$(pwd)/bin:$PATH
+
   $ caisar verify -L . --format whyml --prover Marabou - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory T
   >   use ieee_float.Float64
@@ -46,4 +53,4 @@ Test interpret on dataset
   >     robust classifier dataset eps
   > end
   > EOF
-  [caisar] Goal G: High failure
+  [caisar] Goal G: Unknown ()