diff --git a/config/drivers/marabou.drv b/config/drivers/marabou.drv
index 8cafeddf2208c14909ef770ef4afbad975aa4bbe..3b14d16a0c57620bd06bbbd438bf7e99d6b37152 100644
--- a/config/drivers/marabou.drv
+++ b/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
diff --git a/config/drivers/pyrat.drv b/config/drivers/pyrat.drv
index 266e79a21bee6ac178816f4598d710a80422a109..ecac7d2a42575d57f16d406541c2c3eb458ea597 100644
--- a/config/drivers/pyrat.drv
+++ b/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"
diff --git a/config/drivers/vnnlib.gen b/config/drivers/vnnlib.gen
index a01ef74a36c47b924023c6e1cf1e8fa18dfd15c0..839e7c0b5f1c82667b567460056f96a07571a9b3 100644
--- a/config/drivers/vnnlib.gen
+++ b/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
diff --git a/src/main.ml b/src/main.ml
index 9a5e2ed237800d781a9580a82b69e6ef50cd47f0..7498e10547a2fbc93ed902020d09bbdadc09a669 100644
--- a/src/main.ml
+++ b/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 =
diff --git a/src/transformations/simplify_rel.ml b/src/transformations/simplify_rel.ml
new file mode 100644
index 0000000000000000000000000000000000000000..231676a619012c2e15d4a0a7b9b1cb3c64659757
--- /dev/null
+++ b/src/transformations/simplify_rel.ml
@@ -0,0 +1,145 @@
+(**************************************************************************)
+(* *)
+(* 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
diff --git a/src/transformations/simplify_rel.mli b/src/transformations/simplify_rel.mli
new file mode 100644
index 0000000000000000000000000000000000000000..694097b3b0dcc9bef16af63c6f16994dd897e63e
--- /dev/null
+++ b/src/transformations/simplify_rel.mli
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(* *)
+(* 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. *)
diff --git a/tests/interpretation_acasxu.t b/tests/interpretation_acasxu.t
index 40e170a294334502bbdd9a44d6d5f768be20cddb..64a36be28009baf0edb92483b1e3fd1f52b22e5f 100644
--- a/tests/interpretation_acasxu.t
+++ b/tests/interpretation_acasxu.t
@@ -1,5 +1,13 @@
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 ()
diff --git a/tests/interpretation_dataset.t b/tests/interpretation_dataset.t
index bd1b86e4f4389ad78bccf0d4b5c08d8784b3d303..0dd6f08893880fa641e540d05b6cfd0a2e61c0a3 100644
--- a/tests/interpretation_dataset.t
+++ b/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 ()