diff --git a/examples/acasxu/property_5_aimos.why b/examples/acasxu/property_5_aimos.why
index e653e16cd1245844e081e185679e6371d8987beb..d0ca6f9a0f7594c5132630e96c65d5a3c5945439 100644
--- a/examples/acasxu/property_5_aimos.why
+++ b/examples/acasxu/property_5_aimos.why
@@ -3,6 +3,7 @@ theory ACASXU_P5
use ieee_float.Float64
use caisar.DatasetClassification
use caisar.DatasetClassificationProps
+ use option.Option
- goal G: meta_robust model dataset (1.0:t) ("reluplex_rotation":string) ("config/custom_transformations.py":string) ("classif_min":string) (0:int) (0:int) (0:int)
+ goal G: meta_robust model dataset (1.0:t) "reluplex_rotation" "config/custom_transformations.py" "classif_min" None
end
diff --git a/src/dataset.ml b/src/dataset.ml
index d08696f5d2ce4c2b4d1b1c13cd8e9e1ca3c86653..67f5446162fa9f593872075efd0627d938901c78 100644
--- a/src/dataset.ml
+++ b/src/dataset.ml
@@ -51,13 +51,15 @@ let term_of_eps env eps =
type threshold = float [@@deriving yojson, show]
-type amplitude = {
- start : int option;
+type amplitude_record = {
+ start : int;
stop : int;
- step : int option;
+ step : int;
}
[@@deriving yojson, show]
+type amplitude = amplitude_record option [@@deriving yojson, show]
+
type aimos_params = {
perturbation : string;
ctp : string;
@@ -69,20 +71,12 @@ type aimos_params = {
let string_of_threshold threshold = Float.to_string threshold
let string_of_amplitude amplitude =
- let start = match amplitude.start with Some a -> a | None -> 0 in
- if start = amplitude.stop
- then None
- else
- let start_str =
- Option.value_map amplitude.start ~default:"" ~f:Int.to_string
- in
- let step_str =
- Option.value_map amplitude.step ~default:"" ~f:Int.to_string
- in
+ match amplitude with
+ | Some a ->
Some
- (Fmt.str "range(%s, %s, %s)" start_str
- (Int.to_string amplitude.stop)
- step_str)
+ (Fmt.str "range(%s, %s, %s)" (Int.to_string a.start)
+ (Int.to_string a.stop) (Int.to_string a.step))
+ | None -> None
type property =
| Correct
@@ -107,6 +101,10 @@ let find_predicate_ls env p =
let th = Pmodule.read_module env [ "caisar" ] "DatasetClassificationProps" in
Theory.ns_find_ls th.mod_theory.th_export [ p ]
+let find_option_ls env p =
+ let th = Pmodule.read_module env [ "option" ] "Option" in
+ Theory.ns_find_ls th.mod_theory.th_export [ p ]
+
let failwith_unsupported_term t =
failwith (Fmt.str "Unsupported term %a" Pretty.print_term t)
@@ -143,27 +141,48 @@ let interpret_predicate env ~on_model ~on_dataset task =
{ t_node = Tconst (Constant.ConstStr p); _ };
{ t_node = Tconst (Constant.ConstStr ctp); _ };
{ t_node = Tconst (Constant.ConstStr om); _ };
- { t_node = Tconst (Constant.ConstInt start); _ };
- { t_node = Tconst (Constant.ConstInt stop); _ };
- { t_node = Tconst (Constant.ConstInt step); _ };
+ ampli_node;
] ->
let meta_robust_predicate = find_predicate_ls env "meta_robust" in
+ let some_ls = find_option_ls env "Some" in
+ let none_ls = find_option_ls env "None" in
let f = float_of_real_constant e in
if Term.ls_equal ls meta_robust_predicate
then
- MetaRobust
- ( f,
- {
- perturbation = p;
- ctp;
- om;
- amplitude =
- {
- start = Some (Number.to_small_integer start);
- stop = Number.to_small_integer stop;
- step = Some (Number.to_small_integer step);
- };
- } )
+ let ampli =
+ match ampli_node with
+ | {
+ t_node =
+ Term.Tapp
+ ( option_ls,
+ [
+ {
+ t_node =
+ Term.Tapp
+ ( _,
+ [
+ { t_node = Tconst (Constant.ConstInt start); _ };
+ { t_node = Tconst (Constant.ConstInt stop); _ };
+ { t_node = Tconst (Constant.ConstInt step); _ };
+ ] );
+ _;
+ };
+ ] );
+ _;
+ }
+ when Term.ls_equal option_ls some_ls ->
+ Some
+ {
+ start = Number.to_small_integer start;
+ stop = Number.to_small_integer stop;
+ step = Number.to_small_integer step;
+ }
+ | { t_node = Term.Tapp (option_ls, _); _ }
+ when Term.ls_equal option_ls none_ls ->
+ None
+ | _ -> failwith_unsupported_term ampli_node
+ in
+ MetaRobust (f, { perturbation = p; ctp; om; amplitude = ampli })
else failwith_unsupported_ls ls
| _ -> failwith_unsupported_term term
in
diff --git a/src/dataset.mli b/src/dataset.mli
index 1ad03f6dc56813f3c9b95d240e242f0e488d251d..4660c27d288a6bdef93988f4ace6958ccc5ed5ce 100644
--- a/src/dataset.mli
+++ b/src/dataset.mli
@@ -30,13 +30,15 @@ val term_of_eps : Env.env -> eps -> Term.term
type threshold [@@deriving yojson, show]
-type amplitude = {
- start : int option;
+type amplitude_record = {
+ start : int;
stop : int;
- step : int option;
+ step : int;
}
[@@deriving yojson, show]
+type amplitude = amplitude_record option [@@deriving yojson, show]
+
type aimos_params = {
perturbation : string;
ctp : string;
diff --git a/stdlib/caisar.mlw b/stdlib/caisar.mlw
index 8ff1b9d6e0343dcde158465466dc2994e79757de..31d5dbc82d8f0d2f74e1911c7d934bbcd44a0cc4 100644
--- a/stdlib/caisar.mlw
+++ b/stdlib/caisar.mlw
@@ -24,11 +24,14 @@ theory DatasetClassification
use ieee_float.Float64
use int.Int
use array.Array
+ use option.Option
type features = array t
type label_ = int
type record = (features, label_)
type dataset = array record
+ type amplitude_record = { start: int; stop: int; step: int }
+ type amplitude = option amplitude_record
constant dataset: dataset
@@ -69,7 +72,7 @@ theory DatasetClassificationProps
predicate cond_robust (m: model) (d: dataset) (eps: t) =
correct m d /\ robust m d eps
- predicate meta_robust (m: model) (d: dataset) (threshold: t) (perturbation: string) (pert_path: string) (out_mode: string) (start: int) (stop: int) (step: int)
+ predicate meta_robust (m: model) (d: dataset) (threshold: t) (perturbation: string) (pert_path: string) (out_mode: string) (ampli: amplitude)
end
theory NN
diff --git a/tests/aimos.t b/tests/aimos.t
index 0e37f12305d03d86d5afdcfd17c0101e28d95dfd..988acb268779d7295e147c2c47698ca578e6039d 100644
--- a/tests/aimos.t
+++ b/tests/aimos.t
@@ -16,8 +16,9 @@ Test verify
> use ieee_float.Float64
> use caisar.DatasetClassification
> use caisar.DatasetClassificationProps
+ > use option.Option
>
- > goal G: meta_robust model dataset (1.0:t) ("reluplex_rotation":string) ("config/custom_transformations.py":string) ("classif_min":string) (0:int) (0:int) (0:int)
+ > goal G: meta_robust model dataset (1.0:t) "reluplex_rotation" "config/custom_transformations.py" "classif_min" None
> end
> EOF
Goal G: Valid