Skip to content
Snippets Groups Projects
Commit 0e4ea752 authored by Michele Alberti's avatar Michele Alberti
Browse files

[interpretation] Support has_length predicate.

parent 041bea32
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
src/interpretation.ml
+ 31
− 3
View file @ 0e4ea752
......@@ -36,6 +36,7 @@ type caisar_op =
| Dataset of dataset
| Data of data
| Index of index
| Vector of int
| Tensor of int
[@@deriving show]
......@@ -126,7 +127,7 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
Term.t_int_const (BigInt.of_int (Int.of_string label)) )
in
Term (Term.t_tuple [ t_features; t_label ])
| Data _ | Classifier _ | Tensor _ | Index _ -> assert false)
| Data _ | Classifier _ | Tensor _ | Vector _ | Index _ -> assert false)
| [ Term t1; Term t2 ] ->
(* Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2; *)
Term (Term.t_app_infer ls [ t1; t2 ])
......@@ -141,7 +142,7 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
| [ Term { t_node = Tapp (ls, []); _ } ] -> (
match caisar_op_of_ls engine ls with
| Dataset (DS_csv csv) -> Int (BigInt.of_int (Csv.lines csv))
| Data _ | Classifier _ | Tensor _ | Index _ -> assert false)
| Data _ | Classifier _ | Tensor _ | Vector _ | Index _ -> assert false)
| [ Term t ] ->
(* Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2; *)
Term (Term.t_app_infer ls [ t ])
......@@ -311,7 +312,7 @@ let bounded_quant engine vs ~cond : CRE.bounded_quant_result option =
in
let new_quant =
List.init n ~f:(fun _ ->
let preid = Ident.id_fresh "caisar_v" in
let preid = Ident.id_fresh "caisar_t" in
Term.create_vsymbol preid ty)
in
let args = List.map new_quant ~f:(fun vs -> (Term.t_var vs, ty)) in
......@@ -319,6 +320,33 @@ let bounded_quant engine vs ~cond : CRE.bounded_quant_result option =
[ term_of_caisar_op ~args engine (Tensor n) (Some vs.vs_ty) ]
in
Some { new_quant; substitutions }
| Tapp
( { ls_name = { id_string = "has_length"; _ }; _ },
[
({ t_node = Tvar vs1; _ } as _t1);
({ t_node = Tconst (ConstInt n); _ } as _t2);
] ) ->
(* Fmt.pr "--@.has_length: %a %a@." Pretty.print_term t1 Pretty.print_term
t2; *)
if not (Term.vs_equal vs vs1)
then None
else
let n = Number.to_small_integer n in
let ty =
match vs.vs_ty with
| { ty_node = Tyapp (_, ty :: _); _ } -> ty
| _ -> assert false
in
let new_quant =
List.init n ~f:(fun _ ->
let preid = Ident.id_fresh "caisar_v" in
Term.create_vsymbol preid ty)
in
let args = List.map new_quant ~f:(fun vs -> (Term.t_var vs, ty)) in
let substitutions =
[ term_of_caisar_op ~args engine (Vector n) (Some vs.vs_ty) ]
in
Some { new_quant; substitutions }
| Tapp
( { ls_name = { id_string = "valid_index"; _ }; _ },
[
......
stdlib/interpretation.mlw
+ 4
− 4
View file @ 0e4ea752
......@@ -30,11 +30,11 @@ theory Vector
predicate has_length (v: vector 'a) (i: int)
function map (v: vector 'a) (f: 'a -> 'b) : vector 'b
function mapi (v: vector 'a) (f: int -> 'a -> 'b) : vector 'b
function map2 (v1: vector 'a) (v2: vector 'b) (f: 'a -> 'b -> 'c) : vector 'c
scope L
function map (v: vector 'a) (f: 'a -> 'b) : vector 'b
function mapi (v: vector 'a) (f: int -> 'a -> 'b) : vector 'b
function map2 (v1: vector 'a) (v2: vector 'b) (f: 'a -> 'b -> 'c) : vector 'c
predicate forall_ (v: vector 'a) (f: 'a -> bool) =
forall i: int. 0 <= i < length v -> f v[i]
......
tests/interpretation_acasxu.t
+ 438
− 77
View file @ 0e4ea752
This diff is collapsed.
tests/interpretation_dataset.t
+ 40
− 40
View file @ 0e4ea752
......@@ -47,95 +47,95 @@ Test interpret on dataset
> robust classifier dataset eps
> end
> EOF
G : (forall caisar_v:t, caisar_v1:t, caisar_v2:t, caisar_v3:t, caisar_v4:t.
((((le (0.0:t) caisar_v4 /\ le caisar_v4 (1.0:t)) /\
le (0.0:t) caisar_v3 /\ le caisar_v3 (1.0:t)) /\
le (0.0:t) caisar_v2 /\ le caisar_v2 (1.0:t)) /\
le (0.0:t) caisar_v1 /\ le caisar_v1 (1.0:t)) /\
le (0.0:t) caisar_v /\ le caisar_v (1.0:t) ->
G : (forall caisar_t:t, caisar_t1:t, caisar_t2:t, caisar_t3:t, caisar_t4:t.
((((le (0.0:t) caisar_t4 /\ le caisar_t4 (1.0:t)) /\
le (0.0:t) caisar_t3 /\ le caisar_t3 (1.0:t)) /\
le (0.0:t) caisar_t2 /\ le caisar_t2 (1.0:t)) /\
le (0.0:t) caisar_t1 /\ le caisar_t1 (1.0:t)) /\
le (0.0:t) caisar_t /\ le caisar_t (1.0:t) ->
((((le (neg (0.375:t))
(sub RNE caisar_v4
(sub RNE caisar_t4
(0.776470588000000017103729987866245210170745849609375:t)) /\
le
(sub RNE caisar_v4
(sub RNE caisar_t4
(0.776470588000000017103729987866245210170745849609375:t))
(0.375:t)) /\
le (neg (0.375:t))
(sub RNE caisar_v3
(sub RNE caisar_t3
(0.01960784299999999980013143385804141871631145477294921875:t)) /\
le
(sub RNE caisar_v3
(sub RNE caisar_t3
(0.01960784299999999980013143385804141871631145477294921875:t))
(0.375:t)) /\
le (neg (0.375:t))
(sub RNE caisar_v2
(sub RNE caisar_t2
(0.78431372499999996161790249971090815961360931396484375:t)) /\
le
(sub RNE caisar_v2
(sub RNE caisar_t2
(0.78431372499999996161790249971090815961360931396484375:t))
(0.375:t)) /\
le (neg (0.375:t)) (sub RNE caisar_v1 (1.0:t)) /\
le (sub RNE caisar_v1 (1.0:t)) (0.375:t)) /\
le (neg (0.375:t)) (sub RNE caisar_v (0.0:t)) /\
le (sub RNE caisar_v (0.0:t)) (0.375:t) ->
le (neg (0.375:t)) (sub RNE caisar_t1 (1.0:t)) /\
le (sub RNE caisar_t1 (1.0:t)) (0.375:t)) /\
le (neg (0.375:t)) (sub RNE caisar_t (0.0:t)) /\
le (sub RNE caisar_t (0.0:t)) (0.375:t) ->
lt
(caisar_op
@@ caisar_op1 caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
@@ caisar_op1 caisar_t caisar_t1 caisar_t2 caisar_t3 caisar_t4)
[0]
(caisar_op
@@ caisar_op1 caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
@@ caisar_op1 caisar_t caisar_t1 caisar_t2 caisar_t3 caisar_t4)
[1] /\
lt
(caisar_op
@@ caisar_op1 caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
@@ caisar_op1 caisar_t caisar_t1 caisar_t2 caisar_t3 caisar_t4)
[2]
(caisar_op
@@ caisar_op1 caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
@@ caisar_op1 caisar_t caisar_t1 caisar_t2 caisar_t3 caisar_t4)
[1]) /\
(forall caisar_v:t, caisar_v1:t, caisar_v2:t, caisar_v3:t, caisar_v4:t.
((((le (0.0:t) caisar_v4 /\ le caisar_v4 (1.0:t)) /\
le (0.0:t) caisar_v3 /\ le caisar_v3 (1.0:t)) /\
le (0.0:t) caisar_v2 /\ le caisar_v2 (1.0:t)) /\
le (0.0:t) caisar_v1 /\ le caisar_v1 (1.0:t)) /\
le (0.0:t) caisar_v /\ le caisar_v (1.0:t) ->
(forall caisar_t:t, caisar_t1:t, caisar_t2:t, caisar_t3:t, caisar_t4:t.
((((le (0.0:t) caisar_t4 /\ le caisar_t4 (1.0:t)) /\
le (0.0:t) caisar_t3 /\ le caisar_t3 (1.0:t)) /\
le (0.0:t) caisar_t2 /\ le caisar_t2 (1.0:t)) /\
le (0.0:t) caisar_t1 /\ le caisar_t1 (1.0:t)) /\
le (0.0:t) caisar_t /\ le caisar_t (1.0:t) ->
((((le (neg (0.375:t))
(sub RNE caisar_v4
(sub RNE caisar_t4
(0.78431372499999996161790249971090815961360931396484375:t)) /\
le
(sub RNE caisar_v4
(sub RNE caisar_t4
(0.78431372499999996161790249971090815961360931396484375:t))
(0.375:t)) /\
le (neg (0.375:t))
(sub RNE caisar_v3
(sub RNE caisar_t3
(0.776470588000000017103729987866245210170745849609375:t)) /\
le
(sub RNE caisar_v3
(sub RNE caisar_t3
(0.776470588000000017103729987866245210170745849609375:t))
(0.375:t)) /\
le (neg (0.375:t))
(sub RNE caisar_v2
(sub RNE caisar_t2
(0.01960784299999999980013143385804141871631145477294921875:t)) /\
le
(sub RNE caisar_v2
(sub RNE caisar_t2
(0.01960784299999999980013143385804141871631145477294921875:t))
(0.375:t)) /\
le (neg (0.375:t)) (sub RNE caisar_v1 (0.0:t)) /\
le (sub RNE caisar_v1 (0.0:t)) (0.375:t)) /\
le (neg (0.375:t)) (sub RNE caisar_v (1.0:t)) /\
le (sub RNE caisar_v (1.0:t)) (0.375:t) ->
le (neg (0.375:t)) (sub RNE caisar_t1 (0.0:t)) /\
le (sub RNE caisar_t1 (0.0:t)) (0.375:t)) /\
le (neg (0.375:t)) (sub RNE caisar_t (1.0:t)) /\
le (sub RNE caisar_t (1.0:t)) (0.375:t) ->
lt
(caisar_op
@@ caisar_op1 caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
@@ caisar_op1 caisar_t caisar_t1 caisar_t2 caisar_t3 caisar_t4)
[1]
(caisar_op
@@ caisar_op1 caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
@@ caisar_op1 caisar_t caisar_t1 caisar_t2 caisar_t3 caisar_t4)
[0] /\
lt
(caisar_op
@@ caisar_op1 caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
@@ caisar_op1 caisar_t caisar_t1 caisar_t2 caisar_t3 caisar_t4)
[2]
(caisar_op
@@ caisar_op1 caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
@@ caisar_op1 caisar_t caisar_t1 caisar_t2 caisar_t3 caisar_t4)
[0])
caisar_op,
(Interpretation.Classifier
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment