From 91b5a4a801d569381973b965d4b1f0e5ab73fa5f Mon Sep 17 00:00:00 2001 From: juliaofferman <59590610+juliaofferman@users.noreply.github.com> Date: Mon, 29 Jun 2020 10:52:29 -0700 Subject: [PATCH 01/38] Add list generator to TestGen.ml --- src/TestGen.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/TestGen.ml b/src/TestGen.ml index 4da3bcd..e384829 100644 --- a/src/TestGen.ml +++ b/src/TestGen.ml @@ -15,5 +15,9 @@ let rec for_type (t : Type.t) : Value.t Generator.t = | Type.ARRAY (key,value) -> (Int.gen_incl 0 64) >>= fun len -> ((tuple2 (List.gen_with_length len (tuple2 (for_type key) (for_type value))) (for_type value)) >>= fun (arr, def) -> singleton (Value.Array (key, value, arr, def))) - | Type.LIST _ | Type.TVAR _ - -> raise (Exceptions.Internal_Exn "Generator not implemented!") \ No newline at end of file + | Type.LIST (t) + -> (Int.gen_incl 0 64) + >>= fun len -> (List.gen_with_length len (for_type t)) + >>= fun (l) -> singleton (Value.List (t, l)) + | Type.TVAR _ + -> raise (Exceptions.Internal_Exn "Generator not implemented!") From 2bbf0a0ec290b6d0bd841bae2f5127f298ee2bcc Mon Sep 17 00:00:00 2001 From: juliaofferman <59590610+juliaofferman@users.noreply.github.com> Date: Mon, 29 Jun 2020 11:01:22 -0700 Subject: [PATCH 02/38] Add rev and list equality components --- src/ListComponents.ml | 23 +++++++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) diff --git a/src/ListComponents.ml b/src/ListComponents.ml index d88dd74..dfa6051 100644 --- a/src/ListComponents.ml +++ b/src/ListComponents.ml @@ -29,7 +29,26 @@ let all_qf = [ evaluate = Value.(fun [@warning "-8"] [List (t,l)] -> List (t, (List.tl_exn l))); to_string = (fun [@warning "-8"] [a] -> "(tl " ^ a ^ ")"); global_constraints = (fun _ -> []) - } + }; + { + name = "rev"; + codomain = Type.(LIST (TVAR "T1")); + domain = Type.[LIST (TVAR "T1")]; + is_argument_valid = (function _ -> true); + evaluate = Value.(fun [@warning "-8"] [List (t,l)] -> List (t, (List.rev l))); + to_string = (fun [@warning "-8"] [a] -> "(rev " ^ a ^ ")"); + global_constraints = (fun _ -> []) + }; + + { + name = "equal"; + codomain = Type.BOOL; + domain = Type.[LIST (TVAR "T1"); LIST (TVAR "T1") ]; + is_argument_valid = (function _ -> true); + evaluate = Value.(fun [@warning "-8"] [List (t, l1) ; List (_, l2)] -> Bool (List.equal Value.equal l1 l2)); + to_string = (fun [@warning "-8"] [a ; b] -> "(= " ^ a ^ " " ^ b ^ ")"); + global_constraints = (fun _ -> []) + } ; ] let all = all_qf @ [ @@ -117,4 +136,4 @@ let all_transformed_int_binary = ~f:(fun c -> try Some (map_transform_binary c) with _ -> None))) -let levels = [| all_qf ; all ; all_transformed_int_unary ; all_transformed_int_binary |] \ No newline at end of file +let levels = [| all_qf ; all ; all_transformed_int_unary ; all_transformed_int_binary |] From ece299041d0991418c6120c36d2c0af8de27ad5b Mon Sep 17 00:00:00 2001 From: juliaofferman <59590610+juliaofferman@users.noreply.github.com> Date: Mon, 29 Jun 2020 11:57:22 -0700 Subject: [PATCH 03/38] Add real number type --- src/Type.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Type.ml b/src/Type.ml index 766221a..388c5c6 100644 --- a/src/Type.ml +++ b/src/Type.ml @@ -7,6 +7,7 @@ module T = struct | BOOL | CHAR | STRING + | REAL | TVAR of string | LIST of t | ARRAY of (t * t) @@ -23,6 +24,7 @@ let rec of_sexp (sexp: Sexp.t) : t = | Atom "Bool" -> BOOL | Atom "Char" -> CHAR | Atom "String" -> STRING + | Atom "Real" -> REAL | List [Atom "List" ; typ] -> LIST (of_sexp typ) | List [Atom "Array" ; index ; value] @@ -34,6 +36,7 @@ let rec to_string : t -> string = function | BOOL -> "Bool" | CHAR -> "Char" | STRING -> "String" + | REAL -> "Real" | LIST t -> "(List " ^ (to_string t) ^ ")" | ARRAY (k,v) -> "(Array " ^ (to_string k) ^ " " ^ (to_string v) ^ ")" | TVAR n -> n @@ -105,4 +108,4 @@ module Unification = struct let of_types ?(env = []) (t1 : t list) (t2 : t list) : (string * t) list option = try Some (of_types_exn t1 t2) with _ -> None -end \ No newline at end of file +end From a0ab6f5e5740e2647a911b1b0f23aebffb27147c Mon Sep 17 00:00:00 2001 From: juliaofferman <59590610+juliaofferman@users.noreply.github.com> Date: Mon, 29 Jun 2020 12:03:44 -0700 Subject: [PATCH 04/38] Add real number value --- src/Value.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Value.ml b/src/Value.ml index 8035d7b..418cc82 100644 --- a/src/Value.ml +++ b/src/Value.ml @@ -7,6 +7,7 @@ module T = struct | Bool of bool | Char of char | String of string + | Real of float | List of Type.t * t list | Array of Type.t * Type.t * (t * t) list * t (* FIXME: Use HashTable instead of List *) @@ -21,6 +22,7 @@ let rec typeof : t -> Type.t = function | Bool _ -> Type.BOOL | Char _ -> Type.CHAR | String _ -> Type.STRING + | Real _ -> Type.REAL | List (typ, _) -> Type.LIST typ | Array (key_type, value_type, _, _) -> Type.ARRAY (key_type,value_type) @@ -30,6 +32,7 @@ let rec to_string : t -> string = function | Bool b -> Bool.to_string b | Char c -> "\'" ^ (Char.to_string c) ^ "\'" | String s -> "\"" ^ s ^ "\"" + | Real r -> Float.(if r < 0. then "(" ^ (to_string r) ^ ")" else to_string r) | List _ -> raise (Internal_Exn "List type (de/)serialization not implemented!") | Array (key_type, val_type, value, default_v) -> let default_string = "((as const (Array " ^ (Type.to_string key_type) ^ " " ^ (Type.to_string val_type) ^ ")) " ^ (to_string default_v) ^ ")" @@ -92,4 +95,4 @@ and of_sexp (sexp : Sexp.t) : t = ^ (to_string_hum sexp))) let of_string (s : string) : t = - (of_sexp (Core.Sexp.of_string s)) \ No newline at end of file + (of_sexp (Core.Sexp.of_string s)) From 242a7a33553c49cc8525ccd0b9b669f34705acb1 Mon Sep 17 00:00:00 2001 From: juliaofferman <59590610+juliaofferman@users.noreply.github.com> Date: Mon, 29 Jun 2020 12:13:14 -0700 Subject: [PATCH 05/38] Create RealComponents.ml --- src/RealComponents.ml | 129 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 129 insertions(+) create mode 100644 src/RealComponents.ml diff --git a/src/RealComponents.ml b/src/RealComponents.ml new file mode 100644 index 0000000..e80a63f --- /dev/null +++ b/src/RealComponents.ml @@ -0,0 +1,129 @@ +open Base + +open Expr +open Utils + +let value_of : Value.t -> float = + function [@warning "-8"] + | Real x -> x + | String "" -> 0. + +let translation = [ + { + name = "real-add"; + codomain = Type.REAL; + domain = Type.[REAL; REAL]; + can_apply = Value.(function + | [x ; y] -> (x =/= Constant (Real 0.)) && (y =/= Constant (Real 0.)) + && (match [x ; y] with + | [x ; Application (comp, [_ ; y])] + when String.equal comp.name "real-sub" + -> x =/= y + | [Application (comp, [_ ; x]) ; y] + when String.equal comp.name "real-sub" + -> x =/= y + | _ -> true) + | _ -> false); + evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Real ((value_of v1) +. (value_of v2))); + to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "+" ^ b ^ ")") + } ; + { + name = "real-sub"; + codomain = Type.REAL; + domain = Type.[REAL; REAL]; + can_apply = Value.(function + | [x ; y] -> (x =/= y) + && (x =/= Constant (Real 0.)) && (y =/= Constant (Real 0.)) + && (match [x ; y] with + | [(Application (comp, [x ; y])) ; z] + when String.equal comp.name "real-add" + -> x =/= z && y =/= z + | [(Application (comp, [x ; _])) ; y] + when String.equal comp.name "real-sub" + -> x =/= y + | [x ; (Application (comp, [y ; _]))] + when String.(equal comp.name "real-sub" || equal comp.name "real-add") + -> x =/= y + | _ -> true) + | _ -> false); + evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Real ((value_of v1) -. (value_of v2))); + to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "-" ^ b ^ ")") + } +] + +let scaling = [ + { + name = "real-mult"; + codomain = Type.REAL; + domain = Type.[REAL; REAL]; + can_apply = Value.(function + | [x ; y] + -> (x =/= Constant (Real 0.)) && (x =/= Constant (Real 1.)) && (x =/= Constant (Real (-1.))) + && (y =/= Constant (Real 0.)) && (y =/= Constant (Real 1.)) && (x =/= Constant (Real (-1.))) + | _ -> false); + evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Real ((value_of v1) *. (value_of v2))); + to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "*" ^ b ^ ")") + } ; + { + name = "real-div"; + codomain = Type.REAL; + domain = Type.[REAL; REAL]; + can_apply = Value.(function + | [x ; y] -> x =/= y + && (x =/= Constant (Real 0.)) && (x =/= Constant (Real 1.)) && (x =/= Constant (Real (-1.))) + && (y =/= Constant (Real 0.)) && (y =/= Constant (Real 1.)) && (y =/= Constant (Real (-1.))) + | _ -> false); + evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Real ((value_of v1) /. (value_of v2))); + to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "/" ^ b ^ ")") + } +] + +let conditionals = [ + { + name = "real-eq"; + codomain = Type.BOOL; + domain = Type.[REAL; REAL]; + can_apply = (function + | [x ; y] -> (x =/= y) && (not (is_constant x && is_constant y)) + | _ -> false); + evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Bool Float.Approx.(equal (value_of v1) (value_of v2))); + to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "=" ^ b ^ ")") + } ; + { + name = "real-geq"; + codomain = Type.BOOL; + domain = Type.[REAL; REAL]; + can_apply = (function + | [x ; y] -> (x =/= y) && (not (is_constant x && is_constant y)) + | _ -> false); + evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Bool Float.Approx.(compare (value_of v1) (value_of v2) >= 0)); + to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ ">=" ^ b ^ ")") + } ; + { + name = "real-leq"; + codomain = Type.BOOL; + domain = Type.[REAL; REAL]; + can_apply = (function + | [x ; y] -> (x =/= y) && (not (is_constant x && is_constant y)) + | _ -> false); + evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Bool Float.Approx.(compare (value_of v1) (value_of v2) <= 0)); + to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "<=" ^ b ^ ")") + } ; + { + name = "real-ite"; + codomain = Type.REAL; + domain = Type.[BOOL; REAL; REAL]; + can_apply = (function + | [x ; y ; z] -> (not (is_constant x)) && (y =/= z) + | _ -> false); + evaluate = Value.(fun [@warning "-8"] [Bool x ; v1 ; v2] + -> Real (if x then (value_of v1) else (value_of v2))); + to_string = (fun [@warning "-8"] [a ; b ; c] -> "IF(" ^ a ^ "," ^ b ^ "," ^ c ^ ")") + } +] + + + +let levels = Array.accumulate_lists [| translation ; scaling ; conditionals |] + +let no_bool_levels = Array.accumulate_lists [| translation ; scaling |] From f28ac8b5fbde54481c593aa2ff6797eafbb7c9e7 Mon Sep 17 00:00:00 2001 From: juliaofferman <59590610+juliaofferman@users.noreply.github.com> Date: Mon, 29 Jun 2020 17:53:07 -0700 Subject: [PATCH 06/38] change can_apply to is_argument_valid --- src/RealComponents.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/RealComponents.ml b/src/RealComponents.ml index e80a63f..1d35066 100644 --- a/src/RealComponents.ml +++ b/src/RealComponents.ml @@ -13,7 +13,7 @@ let translation = [ name = "real-add"; codomain = Type.REAL; domain = Type.[REAL; REAL]; - can_apply = Value.(function + is_argument_valid = Value.(function | [x ; y] -> (x =/= Constant (Real 0.)) && (y =/= Constant (Real 0.)) && (match [x ; y] with | [x ; Application (comp, [_ ; y])] @@ -31,7 +31,7 @@ let translation = [ name = "real-sub"; codomain = Type.REAL; domain = Type.[REAL; REAL]; - can_apply = Value.(function + is_argument_valid = Value.(function | [x ; y] -> (x =/= y) && (x =/= Constant (Real 0.)) && (y =/= Constant (Real 0.)) && (match [x ; y] with @@ -56,7 +56,7 @@ let scaling = [ name = "real-mult"; codomain = Type.REAL; domain = Type.[REAL; REAL]; - can_apply = Value.(function + is_argument_valid = Value.(function | [x ; y] -> (x =/= Constant (Real 0.)) && (x =/= Constant (Real 1.)) && (x =/= Constant (Real (-1.))) && (y =/= Constant (Real 0.)) && (y =/= Constant (Real 1.)) && (x =/= Constant (Real (-1.))) @@ -68,7 +68,7 @@ let scaling = [ name = "real-div"; codomain = Type.REAL; domain = Type.[REAL; REAL]; - can_apply = Value.(function + is_argument_valid = Value.(function | [x ; y] -> x =/= y && (x =/= Constant (Real 0.)) && (x =/= Constant (Real 1.)) && (x =/= Constant (Real (-1.))) && (y =/= Constant (Real 0.)) && (y =/= Constant (Real 1.)) && (y =/= Constant (Real (-1.))) @@ -83,7 +83,7 @@ let conditionals = [ name = "real-eq"; codomain = Type.BOOL; domain = Type.[REAL; REAL]; - can_apply = (function + is_argument_valid = (function | [x ; y] -> (x =/= y) && (not (is_constant x && is_constant y)) | _ -> false); evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Bool Float.Approx.(equal (value_of v1) (value_of v2))); @@ -93,7 +93,7 @@ let conditionals = [ name = "real-geq"; codomain = Type.BOOL; domain = Type.[REAL; REAL]; - can_apply = (function + is_argument_valid = (function | [x ; y] -> (x =/= y) && (not (is_constant x && is_constant y)) | _ -> false); evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Bool Float.Approx.(compare (value_of v1) (value_of v2) >= 0)); @@ -103,7 +103,7 @@ let conditionals = [ name = "real-leq"; codomain = Type.BOOL; domain = Type.[REAL; REAL]; - can_apply = (function + is_argument_valid = (function | [x ; y] -> (x =/= y) && (not (is_constant x && is_constant y)) | _ -> false); evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Bool Float.Approx.(compare (value_of v1) (value_of v2) <= 0)); @@ -113,7 +113,7 @@ let conditionals = [ name = "real-ite"; codomain = Type.REAL; domain = Type.[BOOL; REAL; REAL]; - can_apply = (function + is_argument_valid = (function | [x ; y ; z] -> (not (is_constant x)) && (y =/= z) | _ -> false); evaluate = Value.(fun [@warning "-8"] [Bool x ; v1 ; v2] From c81c3081003b63c87c36475ef47dc01330e6c826 Mon Sep 17 00:00:00 2001 From: juliaofferman <59590610+juliaofferman@users.noreply.github.com> Date: Mon, 29 Jun 2020 18:10:47 -0700 Subject: [PATCH 07/38] Update RealComponents.ml --- src/RealComponents.ml | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/src/RealComponents.ml b/src/RealComponents.ml index 1d35066..db354a4 100644 --- a/src/RealComponents.ml +++ b/src/RealComponents.ml @@ -14,12 +14,12 @@ let translation = [ codomain = Type.REAL; domain = Type.[REAL; REAL]; is_argument_valid = Value.(function - | [x ; y] -> (x =/= Constant (Real 0.)) && (y =/= Constant (Real 0.)) + | [x ; y] -> (x =/= Const (Real 0.)) && (y =/= Const (Real 0.)) && (match [x ; y] with - | [x ; Application (comp, [_ ; y])] + | [x ; FCall (comp, [_ ; y])] when String.equal comp.name "real-sub" -> x =/= y - | [Application (comp, [_ ; x]) ; y] + | [FCall (comp, [_ ; x]) ; y] when String.equal comp.name "real-sub" -> x =/= y | _ -> true) @@ -33,15 +33,15 @@ let translation = [ domain = Type.[REAL; REAL]; is_argument_valid = Value.(function | [x ; y] -> (x =/= y) - && (x =/= Constant (Real 0.)) && (y =/= Constant (Real 0.)) + && (x =/= Const (Real 0.)) && (y =/= Const (Real 0.)) && (match [x ; y] with - | [(Application (comp, [x ; y])) ; z] + | [(FCall (comp, [x ; y])) ; z] when String.equal comp.name "real-add" -> x =/= z && y =/= z - | [(Application (comp, [x ; _])) ; y] + | [(FCall (comp, [x ; _])) ; y] when String.equal comp.name "real-sub" -> x =/= y - | [x ; (Application (comp, [y ; _]))] + | [x ; (FCall (comp, [y ; _]))] when String.(equal comp.name "real-sub" || equal comp.name "real-add") -> x =/= y | _ -> true) @@ -58,8 +58,8 @@ let scaling = [ domain = Type.[REAL; REAL]; is_argument_valid = Value.(function | [x ; y] - -> (x =/= Constant (Real 0.)) && (x =/= Constant (Real 1.)) && (x =/= Constant (Real (-1.))) - && (y =/= Constant (Real 0.)) && (y =/= Constant (Real 1.)) && (x =/= Constant (Real (-1.))) + -> (x =/= Const (Real 0.)) && (x =/= Const (Real 1.)) && (x =/= Const (Real (-1.))) + && (y =/= Const (Real 0.)) && (y =/= Const (Real 1.)) && (x =/= Const (Real (-1.))) | _ -> false); evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Real ((value_of v1) *. (value_of v2))); to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "*" ^ b ^ ")") @@ -70,8 +70,8 @@ let scaling = [ domain = Type.[REAL; REAL]; is_argument_valid = Value.(function | [x ; y] -> x =/= y - && (x =/= Constant (Real 0.)) && (x =/= Constant (Real 1.)) && (x =/= Constant (Real (-1.))) - && (y =/= Constant (Real 0.)) && (y =/= Constant (Real 1.)) && (y =/= Constant (Real (-1.))) + && (x =/= Const (Real 0.)) && (x =/= Const (Real 1.)) && (x =/= Const (Real (-1.))) + && (y =/= Const (Real 0.)) && (y =/= Const (Real 1.)) && (y =/= Const (Real (-1.))) | _ -> false); evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Real ((value_of v1) /. (value_of v2))); to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "/" ^ b ^ ")") From 7aee380bc4fc0b65ced9dd3941ee9fd901efc941 Mon Sep 17 00:00:00 2001 From: juliaofferman <59590610+juliaofferman@users.noreply.github.com> Date: Mon, 29 Jun 2020 18:24:48 -0700 Subject: [PATCH 08/38] Update RealComponents.ml --- src/RealComponents.ml | 36 ++++++++++++++++-------------------- 1 file changed, 16 insertions(+), 20 deletions(-) diff --git a/src/RealComponents.ml b/src/RealComponents.ml index db354a4..c6c658c 100644 --- a/src/RealComponents.ml +++ b/src/RealComponents.ml @@ -14,16 +14,14 @@ let translation = [ codomain = Type.REAL; domain = Type.[REAL; REAL]; is_argument_valid = Value.(function - | [x ; y] -> (x =/= Const (Real 0.)) && (y =/= Const (Real 0.)) - && (match [x ; y] with | [x ; FCall (comp, [_ ; y])] when String.equal comp.name "real-sub" - -> x =/= y + -> x =/= y && (x =/= Const (Real 0.)) | [FCall (comp, [_ ; x]) ; y] when String.equal comp.name "real-sub" - -> x =/= y - | _ -> true) - | _ -> false); + -> x =/= y && (y =/= Const (Real 0.)) + | [x ; y] -> (x =/= Const (Real 0.)) && (y =/= Const (Real 0.)) + | _ -> false); evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Real ((value_of v1) +. (value_of v2))); to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "+" ^ b ^ ")") } ; @@ -32,20 +30,18 @@ let translation = [ codomain = Type.REAL; domain = Type.[REAL; REAL]; is_argument_valid = Value.(function - | [x ; y] -> (x =/= y) - && (x =/= Const (Real 0.)) && (y =/= Const (Real 0.)) - && (match [x ; y] with - | [(FCall (comp, [x ; y])) ; z] - when String.equal comp.name "real-add" - -> x =/= z && y =/= z - | [(FCall (comp, [x ; _])) ; y] - when String.equal comp.name "real-sub" - -> x =/= y - | [x ; (FCall (comp, [y ; _]))] - when String.(equal comp.name "real-sub" || equal comp.name "real-add") - -> x =/= y - | _ -> true) - | _ -> false); + | [(FCall (comp, [x ; y])) ; z] + when String.equal comp.name "real-add" + -> x =/= z && y =/= z && (z =/= Const (Real 0.)) + | [(FCall (comp, [x ; _])) ; y] + when String.equal comp.name "real-sub" + -> x =/= y && (y =/= Const (Real 0.)) + | [x ; (FCall (comp, [y ; _]))] + when (String.equal comp.name "real-sub" || String.equal comp.name "real-add") + -> x =/= y + | [x ; y] -> (x =/= y) + && (x =/= Const (Real 0.)) && (y =/= Const (Real 0.)) + | _ -> false); evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Real ((value_of v1) -. (value_of v2))); to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "-" ^ b ^ ")") } From f2add887adca845bcc01e420996a9dd7f9b082aa Mon Sep 17 00:00:00 2001 From: juliaofferman <59590610+juliaofferman@users.noreply.github.com> Date: Mon, 29 Jun 2020 18:29:56 -0700 Subject: [PATCH 09/38] Update RealComponents.ml --- src/RealComponents.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/RealComponents.ml b/src/RealComponents.ml index c6c658c..9532962 100644 --- a/src/RealComponents.ml +++ b/src/RealComponents.ml @@ -14,14 +14,14 @@ let translation = [ codomain = Type.REAL; domain = Type.[REAL; REAL]; is_argument_valid = Value.(function - | [x ; FCall (comp, [_ ; y])] - when String.equal comp.name "real-sub" - -> x =/= y && (x =/= Const (Real 0.)) - | [FCall (comp, [_ ; x]) ; y] - when String.equal comp.name "real-sub" - -> x =/= y && (y =/= Const (Real 0.)) - | [x ; y] -> (x =/= Const (Real 0.)) && (y =/= Const (Real 0.)) - | _ -> false); + | [x ; FCall (comp, [_ ; y])] + when String.equal comp.name "real-sub" + -> x =/= y && (x =/= Const (Real 0.)) + | [FCall (comp, [_ ; x]) ; y] + when String.equal comp.name "real-sub" + -> x =/= y && (y =/= Const (Real 0.)) + | [x ; y] -> (x =/= Const (Real 0.)) && (y =/= Const (Real 0.)) + | _ -> false); evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Real ((value_of v1) +. (value_of v2))); to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "+" ^ b ^ ")") } ; From 6488ca2566bf1534539b3e525fb826997b40cc35 Mon Sep 17 00:00:00 2001 From: juliaofferman <59590610+juliaofferman@users.noreply.github.com> Date: Mon, 29 Jun 2020 18:46:24 -0700 Subject: [PATCH 10/38] Update RealComponents.ml --- src/RealComponents.ml | 24 ++++++++++++++++-------- 1 file changed, 16 insertions(+), 8 deletions(-) diff --git a/src/RealComponents.ml b/src/RealComponents.ml index 9532962..2feaaa6 100644 --- a/src/RealComponents.ml +++ b/src/RealComponents.ml @@ -23,7 +23,8 @@ let translation = [ | [x ; y] -> (x =/= Const (Real 0.)) && (y =/= Const (Real 0.)) | _ -> false); evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Real ((value_of v1) +. (value_of v2))); - to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "+" ^ b ^ ")") + to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "+" ^ b ^ ")"); + global_constraints = (fun _ -> []) } ; { name = "real-sub"; @@ -43,7 +44,8 @@ let translation = [ && (x =/= Const (Real 0.)) && (y =/= Const (Real 0.)) | _ -> false); evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Real ((value_of v1) -. (value_of v2))); - to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "-" ^ b ^ ")") + to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "-" ^ b ^ ")"); + global_constraints = (fun _ -> []) } ] @@ -58,7 +60,8 @@ let scaling = [ && (y =/= Const (Real 0.)) && (y =/= Const (Real 1.)) && (x =/= Const (Real (-1.))) | _ -> false); evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Real ((value_of v1) *. (value_of v2))); - to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "*" ^ b ^ ")") + to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "*" ^ b ^ ")"); + global_constraints = (fun _ -> []) } ; { name = "real-div"; @@ -70,7 +73,8 @@ let scaling = [ && (y =/= Const (Real 0.)) && (y =/= Const (Real 1.)) && (y =/= Const (Real (-1.))) | _ -> false); evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Real ((value_of v1) /. (value_of v2))); - to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "/" ^ b ^ ")") + to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "/" ^ b ^ ")"); + global_constraints = (fun [@warning "-8"] [_ ; b] -> ["(not (= 0 " ^ b ^ "))"]); } ] @@ -83,7 +87,8 @@ let conditionals = [ | [x ; y] -> (x =/= y) && (not (is_constant x && is_constant y)) | _ -> false); evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Bool Float.Approx.(equal (value_of v1) (value_of v2))); - to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "=" ^ b ^ ")") + to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "=" ^ b ^ ")"); + global_constraints = (fun _ -> []) } ; { name = "real-geq"; @@ -93,7 +98,8 @@ let conditionals = [ | [x ; y] -> (x =/= y) && (not (is_constant x && is_constant y)) | _ -> false); evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Bool Float.Approx.(compare (value_of v1) (value_of v2) >= 0)); - to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ ">=" ^ b ^ ")") + to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ ">=" ^ b ^ ")"); + global_constraints = (fun _ -> []) } ; { name = "real-leq"; @@ -103,7 +109,8 @@ let conditionals = [ | [x ; y] -> (x =/= y) && (not (is_constant x && is_constant y)) | _ -> false); evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Bool Float.Approx.(compare (value_of v1) (value_of v2) <= 0)); - to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "<=" ^ b ^ ")") + to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "<=" ^ b ^ ")"); + global_constraints = (fun _ -> []) } ; { name = "real-ite"; @@ -114,7 +121,8 @@ let conditionals = [ | _ -> false); evaluate = Value.(fun [@warning "-8"] [Bool x ; v1 ; v2] -> Real (if x then (value_of v1) else (value_of v2))); - to_string = (fun [@warning "-8"] [a ; b ; c] -> "IF(" ^ a ^ "," ^ b ^ "," ^ c ^ ")") + to_string = (fun [@warning "-8"] [a ; b ; c] -> "IF(" ^ a ^ "," ^ b ^ "," ^ c ^ ")"); + global_constraints = (fun _ -> []) } ] From fdfdd4bd918ec5074175fd254cf73cf1149b9029 Mon Sep 17 00:00:00 2001 From: juliaofferman <59590610+juliaofferman@users.noreply.github.com> Date: Wed, 1 Jul 2020 13:36:05 -0700 Subject: [PATCH 11/38] Update RealComponents.ml --- src/RealComponents.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/RealComponents.ml b/src/RealComponents.ml index 2feaaa6..65bf636 100644 --- a/src/RealComponents.ml +++ b/src/RealComponents.ml @@ -86,7 +86,7 @@ let conditionals = [ is_argument_valid = (function | [x ; y] -> (x =/= y) && (not (is_constant x && is_constant y)) | _ -> false); - evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Bool Float.Approx.(equal (value_of v1) (value_of v2))); + evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Bool Float.(equal (value_of v1) (value_of v2))); to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "=" ^ b ^ ")"); global_constraints = (fun _ -> []) } ; @@ -97,7 +97,7 @@ let conditionals = [ is_argument_valid = (function | [x ; y] -> (x =/= y) && (not (is_constant x && is_constant y)) | _ -> false); - evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Bool Float.Approx.(compare (value_of v1) (value_of v2) >= 0)); + evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Bool Float.((value_of v1) >= (value_of v2))); to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ ">=" ^ b ^ ")"); global_constraints = (fun _ -> []) } ; @@ -108,7 +108,7 @@ let conditionals = [ is_argument_valid = (function | [x ; y] -> (x =/= y) && (not (is_constant x && is_constant y)) | _ -> false); - evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Bool Float.Approx.(compare (value_of v1) (value_of v2) <= 0)); + evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Bool Float.((value_of v1) <= (value_of v2))); to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "<=" ^ b ^ ")"); global_constraints = (fun _ -> []) } ; @@ -128,6 +128,6 @@ let conditionals = [ -let levels = Array.accumulate_lists [| translation ; scaling ; conditionals |] +let levels = [| translation ; scaling ; conditionals |] -let no_bool_levels = Array.accumulate_lists [| translation ; scaling |] +let no_bool_levels = [| translation ; scaling |] From 3d974bd751e95df008e9b7b92653cc061445be7e Mon Sep 17 00:00:00 2001 From: juliaofferman <59590610+juliaofferman@users.noreply.github.com> Date: Wed, 1 Jul 2020 13:58:22 -0700 Subject: [PATCH 12/38] Add Real components --- src/Logic.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Logic.ml b/src/Logic.ml index 5fb9d38..0cc1999 100644 --- a/src/Logic.ml +++ b/src/Logic.ml @@ -41,9 +41,9 @@ let all_supported = (* FIXME: The verification side for lists, especially with transformed components, doesn't work as of now -- we need to emit valid SMTLIB expressions for them *) components_per_level = ArrayComponents.levels ++ BooleanComponents.levels - ++ IntegerComponents.non_linear_levels ++ ListComponents.levels ; + ++ IntegerComponents.non_linear_levels ++ ListComponents.levels ++ RealComponents.levels ; sample_set_size_multiplier = 8 }] ; table -let of_string name = String.Table.find_exn all_supported name \ No newline at end of file +let of_string name = String.Table.find_exn all_supported name From 67914a5d95974e10716d4331ccd15efe07f19005 Mon Sep 17 00:00:00 2001 From: juliaofferman <59590610+juliaofferman@users.noreply.github.com> Date: Wed, 1 Jul 2020 13:59:27 -0700 Subject: [PATCH 13/38] Add real type --- src/Synthesizer.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/Synthesizer.ml b/src/Synthesizer.ml index b9df624..f6aca64 100644 --- a/src/Synthesizer.ml +++ b/src/Synthesizer.ml @@ -168,6 +168,7 @@ let solve_impl (config : Config.t) (task : task) (stats : stats) = let bool_components = typed_components Type.BOOL in let char_components = typed_components Type.CHAR in let string_components = typed_components Type.STRING in + let real_components = typed_components Type.REAL in let poly_list_components = typed_components Type.(LIST (TVAR "_")) in let poly_array_components = typed_components Type.(ARRAY (TVAR "_", TVAR "_")) in @@ -180,6 +181,7 @@ let solve_impl (config : Config.t) (task : task) (stats : stats) = let bool_candidates = empty_candidates () in let char_candidates = empty_candidates () in let string_candidates = empty_candidates () in + let real_candidates = empty_candidates () in let list_candidates = empty_candidates () in let array_candidates = empty_candidates () in @@ -188,6 +190,7 @@ let solve_impl (config : Config.t) (task : task) (stats : stats) = | Type.BOOL -> bool_candidates | Type.CHAR -> char_candidates | Type.STRING -> string_candidates + | Type.REAL -> real_candidates | Type.LIST _ -> list_candidates | Type.ARRAY _ -> array_candidates | Type.TVAR _ when not no_tvar @@ -310,12 +313,14 @@ let solve_impl (config : Config.t) (task : task) (stats : stats) = ; (INT, int_candidates) ; (CHAR, char_candidates) ; (STRING, string_candidates) + ; (REAL, real_candidates) ; (LIST (TVAR "_"), list_candidates) ; (ARRAY (TVAR "_", TVAR "_"), array_candidates) ] [ bool_components.(l) ; int_components.(l) ; char_components.(l) ; string_components.(l) + ; real_components.(l) ; poly_list_components.(l) ; poly_array_components.(l) ] ~f:(fun (cand_type, cands) comps @@ -344,4 +349,4 @@ let solve ?(config = Config.default) (task : task) : result = ; func = Expr.to_function solution ; constraints = solution_constraints ; stats = stats - } \ No newline at end of file + } From ace86c6f76bba2255f2b60d061aa7ad518bb782c Mon Sep 17 00:00:00 2001 From: juliaofferman <59590610+juliaofferman@users.noreply.github.com> Date: Wed, 1 Jul 2020 14:23:10 -0700 Subject: [PATCH 14/38] Additional job examples --- app/App.ml | 425 +++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 410 insertions(+), 15 deletions(-) diff --git a/app/App.ml b/app/App.ml index f1bf999..7d6ca2b 100644 --- a/app/App.ml +++ b/app/App.ml @@ -14,14 +14,14 @@ let print_PI_results (result, stats) = "" ]) -(* a job for inferring a precondition to ensure that the absolute value +(* a job for inferring a precondition to ensure that the absolute value` function has a result equal to its argument *) let abs_job = Job.create_unlabeled ~f:(fun [@warning "-8"] [ Value.Int x ] -> Value.Int (if x > 0 then x else -x)) ~args:([ ("x", Type.INT) ]) ~post:(fun inp res -> match [@warning "-8"] inp , res with - | [ Value.Int x ], Ok (Value.Int y) -> x = y) + | [ Value.Int x ], Ok (Value.Int y) -> -x = y) (* We start with no initial features *) ~features:[] (* We have a random generator for Type.INT. @@ -36,19 +36,61 @@ let with_synth_PI () = Stdio.print_endline "PI for { x = abs(x) } with feature learning:" ; print_PI_results (PIE.learnPreCond abs_job) +let real_abs_job = Job.create_unlabeled + ~f:(fun [@warning "-8"] [ Value.Real x ] -> Value.Real (if Float.(x > 0.) then x else (-1. *. x))) + ~args:([ ("x", Type.REAL) ]) + ~post:(fun inp res -> + match [@warning "-8"] inp , res with + | [ Value.Real x ], Ok (Value.Real y) -> Float.(equal (-1. *. x) y)) + (* We start with no initial features *) + ~features:[] + (* We have a random generator for Type.INT. + * We generate 64 random Value.Int elements + * and then wrap them in singleton lists (single arguments to abs). *) + (List.map ~f:(fun i -> [ i ]) + Quickcheck.(random_value + (Generator.list_with_length 64 + (TestGen.for_type Type.REAL)))) + +let real_abs_PI () = + Stdio.print_endline "PI for { x = abs(x) } with feature learning:" ; + print_PI_results ( + PIE.learnPreCond real_abs_job + ~config:PIE.Config.{ default with _Synthesizer = { default._Synthesizer with logic = Logic.of_string "ALL" } } + ) + + +let real_prod_job = Job.create_unlabeled + ~f:(fun [@warning "-8"] [ Value.Real x ] -> Value.Real ( x *. x)) + ~args:([ ("x", Type.REAL) ]) + ~post:(fun inp res -> + match [@warning "-8"] inp , res with + | [ Value.Real x ], Ok (Value.Real y) -> Float.( Float.(y > x))) + (* We start with no initial features *) + ~features:[] + (* We have a random generator for Type.INT. + * We generate 64 random Value.Int elements + * and then wrap them in singleton lists (single arguments to abs). *) + (List.map ~f:(fun i -> [ i ]) + Quickcheck.(random_value + (Generator.list_with_length 64 + (TestGen.for_type Type.REAL)))) + +let real_prod_PI () = + Stdio.print_endline "PI for { x = x*x } with feature learning:" ; + print_PI_results (PIE.learnPreCond real_prod_job + ~config:PIE.Config.{ default with _Synthesizer = { default._Synthesizer with logic = Logic.of_string "ALL" } } + ) -(* a job for inferring a precondition to check when the result of appending - two (integer) lists is an empty list *) let append_job = - let open Value in - let open Type in + Job.create_unlabeled ~f:(fun [@warning "-8"] [ List (INT, x) ; List (INT, y) ] -> List (INT, (x @ y))) ~args:([ ("x", Type.(LIST INT)) ; ("y", Type.(LIST INT)) ]) ~post:(fun inp res -> match [@warning "-8"] inp , res with - | [ List _ ; List _ ] , Ok (List (INT, res)) -> List.is_empty res) + | [ List (_, l1) ; List (_, l2) ] , Ok (List (INT, res)) -> List.is_empty res) (* We start with these two features and disable feature synthesis *) ~features:[ ((fun [@warning "-8"] [ List (INT, list1) ; _ ] -> List.is_empty list1), @@ -56,20 +98,373 @@ let append_job = ((fun [@warning "-8"] [ _ ; List (INT, list2) ] -> List.is_empty list2), "(= y [])") ; ] - (* Generators for Type.LIST are not yet implemented. *) - (List.map [ ([], []) - ; ([Int 1 ; Int 2], [Int 3]) - ; ([Int 4], []) - ; ([], [Int 5]) ] - ~f:(fun (l1,l2) -> [ List (INT, l1) ; List (INT, l2) ])) + +(List.map ~f:( + fun (x,y) -> [x ;y]) + Quickcheck.(random_value + (Generator.list_with_length 64 + (Generator.tuple2 + (TestGen.for_type (Type.LIST Type.INT)) + (TestGen.for_type (Type.LIST Type.INT)))))) + + + + let no_synth_PI () = Stdio.print_endline "PI for { append(l1,l2) = [] } without feature learning:" ; print_PI_results ( PIE.learnPreCond append_job - ~config:{ PIE.Config.default with disable_synth = true } + ~config:{ PIE.Config.default with disable_synth = true } + ) + +let append_job_2 = + + Job.create_unlabeled + ~f:(fun [@warning "-8"] [ List (INT, x) ; List (INT, y) ] + -> List (INT, (x @ y))) + ~args:([ ("x", Type.(LIST INT)) ; ("y", Type.(LIST INT)) ]) + ~post:(fun inp res -> + match [@warning "-8"] inp , res with + | [ List (INT, l1) ; List (INT, l2) ] , Ok (List (INT, res)) -> List.equal Value.equal res l1) + (* We start with these two features and disable feature synthesis *) + ~features:[ + ((fun [@warning "-8"] [ List (INT, list1) ; _ ] -> List.is_empty list1), + "(= x [])") ; + ((fun [@warning "-8"] [ _ ; List (INT, list2) ] -> List.is_empty list2), + "(= y [])") ; + ] + + (List.map ~f:( + fun (x,y) -> [x ;y]) + Quickcheck.(random_value + (Generator.list_with_length 512 + (Generator.tuple2 + (TestGen.for_type (Type.LIST Type.INT)) + (TestGen.for_type (Type.LIST Type.INT)))))) + +let no_synth_PI_2 () = + Stdio.print_endline "PI for { append(l1,l2) = [] } without feature learning:" ; + print_PI_results ( + PIE.learnPreCond append_job_2 + ~config:{ PIE.Config.default with disable_synth = true } + ) + + let append_job_3 = + + Job.create_unlabeled + ~f:(fun [@warning "-8"] [ List (INT, x) ; List (INT, y) ] + -> List (INT, (x @ y))) + ~args:([ ("x", Type.(LIST INT)) ; ("y", Type.(LIST INT)) ]) + ~post:(fun inp res -> + match [@warning "-8"] inp , res with + | [ List (INT, l1) ; List (INT, l2) ] , Ok (List (INT, res)) -> (List.length res) = 2) + (* We start with these two features and disable feature synthesis *) + ~features:[ + ((fun [@warning "-8"] [ List (INT, list1) ; _ ] -> List.is_empty list1), + "(= x [])") ; + ((fun [@warning "-8"] [ _ ; List (INT, list2) ] -> List.is_empty list2), + "(= y [])") ; + ] + + + (List.map ~f:( + fun (x,y) -> [x ;y]) + Quickcheck.(random_value + (Generator.list_with_length 4096 + (Generator.tuple2 + (TestGen.for_type (Type.LIST Type.INT)) + (TestGen.for_type (Type.LIST Type.INT)))))) + +let no_synth_PI_3 () = + Stdio.print_endline "PI for { append(l1,l2) = [] } without feature learning:" ; + print_PI_results ( + PIE.learnPreCond append_job_3 + ~config:PIE.Config.{ default with _Synthesizer = { default._Synthesizer with logic = Logic.of_string "ALL" } } ) +let rev_append_job = + + Job.create_unlabeled + ~f:(fun [@warning "-8"] [ List (INT, x) ; List (INT, y) ] + -> List (INT, (List.rev x @ y))) + ~args:([ ("x", Type.(LIST INT)) ; ("y", Type.(LIST INT)) ]) + ~post:(fun inp res -> + match [@warning "-8"] inp , res with + | [ List (INT, l1) ; List (INT, l2) ] , Ok (List (INT, res)) -> (List.equal Value.equal res (l1 @ l2))) + (* We start with these two features and disable feature synthesis *) + ~features:[ + ((fun [@warning "-8"] [ List (INT, list1) ; _ ] -> List.is_empty list1), + "(= x [])") ; + ((fun [@warning "-8"] [ _ ; List (INT, list2) ] -> List.is_empty list2), + "(= y [])") ; + ] + + (List.map ~f:( + fun (x,y) -> [x ;y]) + Quickcheck.(random_value + (Generator.list_with_length 4096 + (Generator.tuple2 + (TestGen.for_type (Type.LIST Type.INT)) + (TestGen.for_type (Type.LIST Type.INT)))))) + +let rev_append_synth_pi () = + Stdio.print_endline "PI for { rev append(l1,l2) = [] } without feature learning:" ; + print_PI_results ( + PIE.learnPreCond rev_append_job + ~config:PIE.Config.{ default with _Synthesizer = { default._Synthesizer with logic = Logic.of_string "ALL" } } + ) + + + + let comp_len_job = + + Job.create_unlabeled + ~f:(fun [@warning "-8"] [ List (INT, x) ; List (INT, y) ] + -> Int (compare( List.length x) (List.length y) )) + ~args:([ ("x", Type.(LIST INT)) ; ("y", Type.(LIST INT)) ]) + ~post:(fun inp res -> + match [@warning "-8"] inp , res with + | [ List (INT, l1) ; List (INT, l2) ] , Ok (Int res) -> (res = 0)) + (* We start with these two features and disable feature synthesis *) + ~features:[ + ((fun [@warning "-8"] [ List (INT, list1) ; _ ] -> List.is_empty list1), + "(= x [])") ; + ((fun [@warning "-8"] [ _ ; List (INT, list2) ] -> List.is_empty list2), + "(= y [])") ; + ] + + (List.map ~f:( + fun (x,y) -> [x ;y]) + Quickcheck.(random_value + (Generator.list_with_length 4096 + (Generator.tuple2 + (TestGen.for_type (Type.LIST Type.INT)) + (TestGen.for_type (Type.LIST Type.INT)))))) + +let comp_len_PI () = + Stdio.print_endline "PI for { compare_lengths l1 l2 = 0 } without feature learning:" ; + print_PI_results ( + PIE.learnPreCond comp_len_job + ~config:PIE.Config.{ default with _Synthesizer = { default._Synthesizer with logic = Logic.of_string "ALL" } } + ) + + + + + +let square_job = Job.create_unlabeled + ~f:(fun [@warning "-8"] [ Value.Int x ] -> Value.Int (x*x)) + ~args:([ ("x", Type.INT) ]) + ~post:(fun inp res -> + match [@warning "-8"] inp , res with + | [ Value.Int x ], Ok (Value.Int y) -> y/x = abs(x)) + (* We start with no initial features *) + ~features:[] + (* We have a random generator for Type.INT. + * We generate 64 random Value.Int elements + * and then wrap them in singleton lists (single arguments to abs). *) + (List.map ~f:(fun i -> [ i ]) + Quickcheck.(random_value + (Generator.list_with_length 64 + (TestGen.for_type Type.INT)))) + + let square_synth_pi () = + Stdio.print_endline "PI for { x = x*x } with feature learning:" ; + print_PI_results (PIE.learnPreCond square_job) + + + + + let cube_job = Job.create_unlabeled + ~f:(fun [@warning "-8"] [ Value.Int x ] -> Value.Int (x*x*x)) + ~args:([ ("x", Type.INT) ]) + ~post:(fun inp res -> + match [@warning "-8"] inp , res with + | [ Value.Int x ], Ok (Value.Int y) -> 1 < y) + (* We start with no initial features *) + ~features:[] + (* We have a random generator for Type.INT. + * We generate 64 random Value.Int elements + * and then wrap them in singleton lists (single arguments to abs). *) + (List.map ~f:(fun i -> [ i ]) + Quickcheck.(random_value + (Generator.list_with_length 64 + (TestGen.for_type Type.INT)))) + + let cube_synth_pi () = + Stdio.print_endline "PI for { x = x*x*x } with feature learning:" ; + print_PI_results (PIE.learnPreCond cube_job) + +let inverse_job = Job.create_unlabeled + ~f:(fun [@warning "-8"] [ Value.Int x ] -> Value.Int (1/x)) + ~args:([ ("x", Type.INT) ]) + ~post:(fun inp res -> + match [@warning "-8"] inp , res with + | [ Value.Int x ], Ok (Value.Int y) -> -x > y) + (* We start with no initial features *) + ~features:[] + (* We have a random generator for Type.INT. + * We generate 64 random Value.Int elements + * and then wrap them in singleton lists (single arguments to abs). *) + (List.map ~f:(fun i -> [ i ]) + Quickcheck.(random_value + (Generator.list_with_length 64 + (TestGen.for_type Type.INT)))) + + let inverse_synth_pi () = + Stdio.print_endline "PI for { x = 1 / x } with feature learning:" ; + print_PI_results (PIE.learnPreCond inverse_job) + + let even_job = Job.create_unlabeled + ~f:(fun [@warning "-8"] [ Value.Int x ] -> Value.Int ((x / 2) * 2)) + ~args:([ ("x", Type.INT) ]) + ~post:(fun inp res -> + match [@warning "-8"] inp , res with + | [ Value.Int x ], Ok (Value.Int y) -> x = y) + (* We start with no initial features *) + ~features:[] + (* We have a random generator for Type.INT. + * We generate 64 random Value.Int elements + * and then wrap them in singleton lists (single arguments to abs). *) + (List.map ~f:(fun i -> [ i ]) + Quickcheck.(random_value + (Generator.list_with_length 100 + (TestGen.for_type Type.INT)))) + + let even_synth_pi () = + Stdio.print_endline "PI for { x = (x / 2) * 2 } with feature learning:" ; + print_PI_results (PIE.learnPreCond even_job + ~config:{ PIE.Config.default with + _Synthesizer = { PIE.Config.default._Synthesizer with + logic = Logic.of_string "NIA" } } +) + + let product_job = Job.create_unlabeled + ~f:(fun [@warning "-8"] [ Value.Int x ; Value.Int y] -> Value.Int (x*y)) + ~args:([ ("x", Type.INT) ; ("y", Type.INT) ]) + ~post:(fun inp res -> + match [@warning "-8"] inp , res with + | [ Value.Int x ; Value.Int y], Ok (Value.Int r) -> r > x) + (* We start with no initial features *) + ~features:[] + (* We have a random generator for Type.INT. + * We generate 64 random Value.Int elements + * and then wrap them in singleton lists (single arguments to abs). *) + (List.map ~f:(fun i -> [ i ]) + Quickcheck.(random_value + (Generator.list_with_length 64 + (TestGen.for_type Type.INT)))) + + let product_synth_pi () = + Stdio.print_endline "PI for { x = x*y} with feature learning:" ; + print_PI_results (PIE.learnPreCond product_job) + + + + let avg_job = Job.create_unlabeled + ~f:(fun [@warning "-8"] [ Value.Int x ; Value.Int y; Value.Int z] -> Value.Int ((x + y + z) / 3)) + ~args:([ ("x", Type.INT) ; ("y", Type.INT) ; ("z", Type.INT) ]) + ~post:(fun inp res -> + match [@warning "-8"] inp , res with + | [ Value.Int x ; Value.Int y ; Value.Int z], Ok (Value.Int r) -> r = x) + (* We start with no initial features *) + ~features:[] + + + (List.map ~f:(fun (x,y,z) -> [ x ; y ; z]) + Quickcheck.(random_value + (Generator.list_with_length 64 + (Generator.tuple3 (TestGen.for_type Type.INT) (TestGen.for_type Type.INT) (TestGen.for_type Type.INT))))) + + let avg_synth_pi () = + Stdio.print_endline "PI for { x = avg(x, y, z)} with feature learning:" ; + print_PI_results (PIE.learnPreCond avg_job) + + + + let max_job = Job.create_unlabeled + ~f:(fun [@warning "-8"] [ Value.Int x ; Value.Int y] -> Value.Int (if x > y then x else y)) + ~args:([ ("x", Type.INT) ; ("y", Type.INT) ]) + ~post:(fun inp res -> + match [@warning "-8"] inp , res with + | [ Value.Int x ; Value.Int y], Ok (Value.Int r) -> r = x && r = y) + (* We start with no initial features *) + ~features:[] + (List.map ~f:(fun (x,y) -> [ x ; y ]) + Quickcheck.(random_value + (Generator.list_with_length 64 + (Generator.tuple2 (TestGen.for_type Type.INT) (TestGen.for_type Type.INT))))) + + let max_synth_pi () = + Stdio.print_endline "PI for { x = max(x, y)} with feature learning:" ; + print_PI_results (PIE.learnPreCond max_job) + + + +let int_average_job = Job.create_unlabeled + ~f:(fun [@warning "-8"] [ Value.Int x ; Value.Int y] -> Value.Int ((x+y)/2)) + ~args:([ ("x", Type.INT) ; ("y", Type.INT) ]) + ~post:(fun inp res -> + match [@warning "-8"] inp , res with + | [ Value.Int x ; Value.Int y], Ok (Value.Int r) -> r > x) + (* We start with no initial features *) + ~features:[] + [[Value.Int 1; Value.Int 3]; [Value.Int 4; Value.Int 4]; [Value.Int 5; Value.Int 3] ; [Value.Int 3; Value.Int 5]] + + let average_synth_pi () = + Stdio.print_endline "PI for { x = (x + y) / 2} with feature learning:" ; + print_PI_results (PIE.learnPreCond int_average_job) + + let int_average_job_2 = Job.create_unlabeled + ~f:(fun [@warning "-8"] [ Value.Int x ; Value.Int y] -> Value.Int ((x+y)/2)) + ~args:([ ("x", Type.INT) ; ("y", Type.INT) ]) + ~post:(fun inp res -> + match [@warning "-8"] inp , res with + | [ Value.Int x ; Value.Int y], Ok (Value.Int r) -> r < x) + (* We start with no initial features *) + ~features:[] + [[Value.Int 1; Value.Int 3]; [Value.Int 4; Value.Int 4]; [Value.Int 5; Value.Int 3] ; [Value.Int 3; Value.Int 5] ; [Value.Int 4; Value.Int 2]] + + let average_synth_pi_2 () = + Stdio.print_endline "PI for { x = (x + y) / 2} with feature learning:" ; + print_PI_results (PIE.learnPreCond int_average_job_2) + + let int_average_job_3 = Job.create_unlabeled + ~f:(fun [@warning "-8"] [ Value.Int x ; Value.Int y] -> Value.Int ((x+y)/2)) + ~args:([ ("x", Type.INT) ; ("y", Type.INT) ]) + ~post:(fun inp res -> + match [@warning "-8"] inp , res with + | [ Value.Int x ; Value.Int y], Ok (Value.Int r) -> r = x) + (* We start with no initial features *) + ~features:[] + [[Value.Int 1; Value.Int 3]; [Value.Int 4; Value.Int 4]; [Value.Int 5; Value.Int 3] ; [Value.Int 3; Value.Int 5] ; [Value.Int 4; Value.Int 2]] + + let average_synth_pi_3 () = + Stdio.print_endline "PI for { x = (x + y) / 2} with feature learning:" ; + print_PI_results (PIE.learnPreCond int_average_job_3) + + + + let () = with_synth_PI () - ; no_synth_PI () \ No newline at end of file + ; real_abs_PI () + ; real_prod_PI () + ; no_synth_PI () + ; no_synth_PI_2 () + ; no_synth_PI_3 () + ; rev_append_synth_pi () + ; comp_len_PI () + ; square_synth_pi () + ; cube_synth_pi () + ; inverse_synth_pi () + ; product_synth_pi () + ; max_synth_pi () + ; average_synth_pi () + ; average_synth_pi_2 () + ; average_synth_pi_3 () + ; even_synth_pi () + ; avg_synth_pi () + + From 11c33b0b14a59c564f792835a664c76de6446a0b Mon Sep 17 00:00:00 2001 From: juliaofferman <59590610+juliaofferman@users.noreply.github.com> Date: Wed, 1 Jul 2020 14:31:45 -0700 Subject: [PATCH 15/38] Update TestGen.ml --- src/TestGen.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/TestGen.ml b/src/TestGen.ml index e384829..4dcc17f 100644 --- a/src/TestGen.ml +++ b/src/TestGen.ml @@ -12,11 +12,12 @@ let rec for_type (t : Type.t) : Value.t Generator.t = | Type.STRING -> (Int.gen_incl 0 64) >>= fun len -> (String.gen_with_length len (Char.gen_print) >>= fun s -> singleton (Value.String s)) + | Type.REAL -> (Float.gen_incl (-4096.) 4096. ) >>= fun i -> singleton (Value.Real i) | Type.ARRAY (key,value) -> (Int.gen_incl 0 64) >>= fun len -> ((tuple2 (List.gen_with_length len (tuple2 (for_type key) (for_type value))) (for_type value)) >>= fun (arr, def) -> singleton (Value.Array (key, value, arr, def))) | Type.LIST (t) - -> (Int.gen_incl 0 64) + -> (Int.gen_incl 0 14) >>= fun len -> (List.gen_with_length len (for_type t)) >>= fun (l) -> singleton (Value.List (t, l)) | Type.TVAR _ From 85c3494ef116ab4d18b8c26833e97e06e5ed09c9 Mon Sep 17 00:00:00 2001 From: juliaofferman <59590610+juliaofferman@users.noreply.github.com> Date: Wed, 1 Jul 2020 14:41:45 -0700 Subject: [PATCH 16/38] Update TestGen.ml --- src/TestGen.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/TestGen.ml b/src/TestGen.ml index 4dcc17f..eabbbf1 100644 --- a/src/TestGen.ml +++ b/src/TestGen.ml @@ -12,7 +12,7 @@ let rec for_type (t : Type.t) : Value.t Generator.t = | Type.STRING -> (Int.gen_incl 0 64) >>= fun len -> (String.gen_with_length len (Char.gen_print) >>= fun s -> singleton (Value.String s)) - | Type.REAL -> (Float.gen_incl (-4096.) 4096. ) >>= fun i -> singleton (Value.Real i) + | Type.REAL -> (Float.gen_incl (-4096.) 4096.) >>= fun i -> singleton (Value.Real i) | Type.ARRAY (key,value) -> (Int.gen_incl 0 64) >>= fun len -> ((tuple2 (List.gen_with_length len (tuple2 (for_type key) (for_type value))) (for_type value)) >>= fun (arr, def) -> singleton (Value.Array (key, value, arr, def))) From cf97993f985034aabd8bc71adb7ddb2a9916a787 Mon Sep 17 00:00:00 2001 From: juliaofferman <59590610+juliaofferman@users.noreply.github.com> Date: Thu, 2 Jul 2020 19:27:36 -0700 Subject: [PATCH 17/38] Update real constants --- src/Synthesizer.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Synthesizer.ml b/src/Synthesizer.ml index f6aca64..a9a8637 100644 --- a/src/Synthesizer.ml +++ b/src/Synthesizer.ml @@ -210,7 +210,7 @@ let solve_impl (config : Config.t) (task : task) (stats : stats) = let constants = Value.( List.dedup_and_sort ~compare - ( Value.[ Int 0 ; Int 1 ; Bool true ; Bool false ] + ( Value.[ Int 0 ; Int 1 ; Bool true ; Bool false ; Real 0.0 ; Real 1.0 ; Real 2.0 ] @ (List.map task.constants ~f:(function Int x -> Int (abs x) | x -> x)))) in let add_constant_candidate value = From 47131ad0f5b28be5e0502e3af05e5918712d3def Mon Sep 17 00:00:00 2001 From: juliaofferman <59590610+juliaofferman@users.noreply.github.com> Date: Thu, 2 Jul 2020 19:29:29 -0700 Subject: [PATCH 18/38] Update Real component to_string's --- src/RealComponents.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/RealComponents.ml b/src/RealComponents.ml index 65bf636..924f6e9 100644 --- a/src/RealComponents.ml +++ b/src/RealComponents.ml @@ -23,7 +23,7 @@ let translation = [ | [x ; y] -> (x =/= Const (Real 0.)) && (y =/= Const (Real 0.)) | _ -> false); evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Real ((value_of v1) +. (value_of v2))); - to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "+" ^ b ^ ")"); + to_string = (fun [@warning "-8"] [a ; b] -> "(+ " ^ a ^ " " ^ b ^ ")"); global_constraints = (fun _ -> []) } ; { @@ -44,7 +44,7 @@ let translation = [ && (x =/= Const (Real 0.)) && (y =/= Const (Real 0.)) | _ -> false); evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Real ((value_of v1) -. (value_of v2))); - to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "-" ^ b ^ ")"); + to_string = (fun [@warning "-8"] [a ; b] -> "(- " ^ a ^ " " ^ b ^ ")"); global_constraints = (fun _ -> []) } ] @@ -60,7 +60,7 @@ let scaling = [ && (y =/= Const (Real 0.)) && (y =/= Const (Real 1.)) && (x =/= Const (Real (-1.))) | _ -> false); evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Real ((value_of v1) *. (value_of v2))); - to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "*" ^ b ^ ")"); + to_string = (fun [@warning "-8"] [a ; b] -> "(* " ^ a ^ " " ^ b ^ ")"); global_constraints = (fun _ -> []) } ; { @@ -73,7 +73,7 @@ let scaling = [ && (y =/= Const (Real 0.)) && (y =/= Const (Real 1.)) && (y =/= Const (Real (-1.))) | _ -> false); evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Real ((value_of v1) /. (value_of v2))); - to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "/" ^ b ^ ")"); + to_string = (fun [@warning "-8"] [a ; b] -> "(/ " ^ a ^ " " ^ b ^ ")"); global_constraints = (fun [@warning "-8"] [_ ; b] -> ["(not (= 0 " ^ b ^ "))"]); } ] @@ -87,7 +87,7 @@ let conditionals = [ | [x ; y] -> (x =/= y) && (not (is_constant x && is_constant y)) | _ -> false); evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Bool Float.(equal (value_of v1) (value_of v2))); - to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "=" ^ b ^ ")"); + to_string = (fun [@warning "-8"] [a ; b] -> "(= " ^ a ^ " " ^ b ^ ")"); global_constraints = (fun _ -> []) } ; { @@ -98,7 +98,7 @@ let conditionals = [ | [x ; y] -> (x =/= y) && (not (is_constant x && is_constant y)) | _ -> false); evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Bool Float.((value_of v1) >= (value_of v2))); - to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ ">=" ^ b ^ ")"); + to_string = (fun [@warning "-8"] [a ; b] -> "(>= " ^ a ^ " " ^ b ^ ")"); global_constraints = (fun _ -> []) } ; { @@ -109,7 +109,7 @@ let conditionals = [ | [x ; y] -> (x =/= y) && (not (is_constant x && is_constant y)) | _ -> false); evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Bool Float.((value_of v1) <= (value_of v2))); - to_string = (fun [@warning "-8"] [a ; b] -> "(" ^ a ^ "<=" ^ b ^ ")"); + to_string = (fun [@warning "-8"] [a ; b] -> "(<= " ^ a ^ " " ^ b ^ ")"); global_constraints = (fun _ -> []) } ; { From 3a2d80d97eae0cdf04e1056a951341f36ffc3a6e Mon Sep 17 00:00:00 2001 From: juliaofferman <59590610+juliaofferman@users.noreply.github.com> Date: Thu, 2 Jul 2020 19:30:09 -0700 Subject: [PATCH 19/38] Update TestGen.ml --- src/TestGen.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/TestGen.ml b/src/TestGen.ml index eabbbf1..4c30138 100644 --- a/src/TestGen.ml +++ b/src/TestGen.ml @@ -6,7 +6,7 @@ let rec for_type (t : Type.t) : Value.t Generator.t = match t with (* Full range of Int: | Type.INT -> Int.gen >>= fun i -> singleton (Value.Int i) *) - | Type.INT -> (Int.gen_incl (-4096) 4095) >>= fun i -> singleton (Value.Int i) + | Type.INT -> (Int.gen_incl (-4096) 4096) >>= fun i -> singleton (Value.Int i) | Type.BOOL -> bool >>= fun b -> singleton (Value.Bool b) | Type.CHAR -> char >>= fun c -> singleton (Value.Char c) | Type.STRING -> (Int.gen_incl 0 64) From c633438ffff1a201967b844bd5cc00efbb1ba77d Mon Sep 17 00:00:00 2001 From: juliaofferman <59590610+juliaofferman@users.noreply.github.com> Date: Thu, 2 Jul 2020 19:43:06 -0700 Subject: [PATCH 20/38] Update App.ml --- app/App.ml | 6 ------ 1 file changed, 6 deletions(-) diff --git a/app/App.ml b/app/App.ml index 7d6ca2b..8134473 100644 --- a/app/App.ml +++ b/app/App.ml @@ -44,9 +44,6 @@ let real_abs_job = Job.create_unlabeled | [ Value.Real x ], Ok (Value.Real y) -> Float.(equal (-1. *. x) y)) (* We start with no initial features *) ~features:[] - (* We have a random generator for Type.INT. - * We generate 64 random Value.Int elements - * and then wrap them in singleton lists (single arguments to abs). *) (List.map ~f:(fun i -> [ i ]) Quickcheck.(random_value (Generator.list_with_length 64 @@ -68,9 +65,6 @@ let real_prod_job = Job.create_unlabeled | [ Value.Real x ], Ok (Value.Real y) -> Float.( Float.(y > x))) (* We start with no initial features *) ~features:[] - (* We have a random generator for Type.INT. - * We generate 64 random Value.Int elements - * and then wrap them in singleton lists (single arguments to abs). *) (List.map ~f:(fun i -> [ i ]) Quickcheck.(random_value (Generator.list_with_length 64 From 427c2ff94d44d8f671ff6e7d3cd6cc0d2ced810a Mon Sep 17 00:00:00 2001 From: juliaofferman <59590610+juliaofferman@users.noreply.github.com> Date: Mon, 6 Jul 2020 20:43:17 -0700 Subject: [PATCH 21/38] Update App.ml --- app/App.ml | 417 ++--------------------------------------------------- 1 file changed, 14 insertions(+), 403 deletions(-) diff --git a/app/App.ml b/app/App.ml index 8134473..6b5fdac 100644 --- a/app/App.ml +++ b/app/App.ml @@ -14,14 +14,14 @@ let print_PI_results (result, stats) = "" ]) -(* a job for inferring a precondition to ensure that the absolute value` +(* a job for inferring a precondition to ensure that the absolute value function has a result equal to its argument *) let abs_job = Job.create_unlabeled ~f:(fun [@warning "-8"] [ Value.Int x ] -> Value.Int (if x > 0 then x else -x)) ~args:([ ("x", Type.INT) ]) ~post:(fun inp res -> match [@warning "-8"] inp , res with - | [ Value.Int x ], Ok (Value.Int y) -> -x = y) + | [ Value.Int x ], Ok (Value.Int y) -> x = y) (* We start with no initial features *) ~features:[] (* We have a random generator for Type.INT. @@ -36,55 +36,19 @@ let with_synth_PI () = Stdio.print_endline "PI for { x = abs(x) } with feature learning:" ; print_PI_results (PIE.learnPreCond abs_job) -let real_abs_job = Job.create_unlabeled - ~f:(fun [@warning "-8"] [ Value.Real x ] -> Value.Real (if Float.(x > 0.) then x else (-1. *. x))) - ~args:([ ("x", Type.REAL) ]) - ~post:(fun inp res -> - match [@warning "-8"] inp , res with - | [ Value.Real x ], Ok (Value.Real y) -> Float.(equal (-1. *. x) y)) - (* We start with no initial features *) - ~features:[] - (List.map ~f:(fun i -> [ i ]) - Quickcheck.(random_value - (Generator.list_with_length 64 - (TestGen.for_type Type.REAL)))) - -let real_abs_PI () = - Stdio.print_endline "PI for { x = abs(x) } with feature learning:" ; - print_PI_results ( - PIE.learnPreCond real_abs_job - ~config:PIE.Config.{ default with _Synthesizer = { default._Synthesizer with logic = Logic.of_string "ALL" } } - ) - - -let real_prod_job = Job.create_unlabeled - ~f:(fun [@warning "-8"] [ Value.Real x ] -> Value.Real ( x *. x)) - ~args:([ ("x", Type.REAL) ]) - ~post:(fun inp res -> - match [@warning "-8"] inp , res with - | [ Value.Real x ], Ok (Value.Real y) -> Float.( Float.(y > x))) - (* We start with no initial features *) - ~features:[] - (List.map ~f:(fun i -> [ i ]) - Quickcheck.(random_value - (Generator.list_with_length 64 - (TestGen.for_type Type.REAL)))) - -let real_prod_PI () = - Stdio.print_endline "PI for { x = x*x } with feature learning:" ; - print_PI_results (PIE.learnPreCond real_prod_job - ~config:PIE.Config.{ default with _Synthesizer = { default._Synthesizer with logic = Logic.of_string "ALL" } } - ) +(* a job for inferring a precondition to check when the result of appending + two (integer) lists is an empty list *) let append_job = - + let open Value in + let open Type in Job.create_unlabeled ~f:(fun [@warning "-8"] [ List (INT, x) ; List (INT, y) ] -> List (INT, (x @ y))) ~args:([ ("x", Type.(LIST INT)) ; ("y", Type.(LIST INT)) ]) ~post:(fun inp res -> match [@warning "-8"] inp , res with - | [ List (_, l1) ; List (_, l2) ] , Ok (List (INT, res)) -> List.is_empty res) + | [ List _ ; List _ ] , Ok (List (INT, res)) -> List.is_empty res) (* We start with these two features and disable feature synthesis *) ~features:[ ((fun [@warning "-8"] [ List (INT, list1) ; _ ] -> List.is_empty list1), @@ -92,373 +56,20 @@ let append_job = ((fun [@warning "-8"] [ _ ; List (INT, list2) ] -> List.is_empty list2), "(= y [])") ; ] - -(List.map ~f:( - fun (x,y) -> [x ;y]) - Quickcheck.(random_value - (Generator.list_with_length 64 - (Generator.tuple2 - (TestGen.for_type (Type.LIST Type.INT)) - (TestGen.for_type (Type.LIST Type.INT)))))) - - - - + (* Generators for Type.LIST are not yet implemented. *) + (List.map [ ([], []) + ; ([Int 1 ; Int 2], [Int 3]) + ; ([Int 4], []) + ; ([], [Int 5]) ] + ~f:(fun (l1,l2) -> [ List (INT, l1) ; List (INT, l2) ])) let no_synth_PI () = Stdio.print_endline "PI for { append(l1,l2) = [] } without feature learning:" ; print_PI_results ( PIE.learnPreCond append_job - ~config:{ PIE.Config.default with disable_synth = true } - ) - -let append_job_2 = - - Job.create_unlabeled - ~f:(fun [@warning "-8"] [ List (INT, x) ; List (INT, y) ] - -> List (INT, (x @ y))) - ~args:([ ("x", Type.(LIST INT)) ; ("y", Type.(LIST INT)) ]) - ~post:(fun inp res -> - match [@warning "-8"] inp , res with - | [ List (INT, l1) ; List (INT, l2) ] , Ok (List (INT, res)) -> List.equal Value.equal res l1) - (* We start with these two features and disable feature synthesis *) - ~features:[ - ((fun [@warning "-8"] [ List (INT, list1) ; _ ] -> List.is_empty list1), - "(= x [])") ; - ((fun [@warning "-8"] [ _ ; List (INT, list2) ] -> List.is_empty list2), - "(= y [])") ; - ] - - (List.map ~f:( - fun (x,y) -> [x ;y]) - Quickcheck.(random_value - (Generator.list_with_length 512 - (Generator.tuple2 - (TestGen.for_type (Type.LIST Type.INT)) - (TestGen.for_type (Type.LIST Type.INT)))))) - -let no_synth_PI_2 () = - Stdio.print_endline "PI for { append(l1,l2) = [] } without feature learning:" ; - print_PI_results ( - PIE.learnPreCond append_job_2 - ~config:{ PIE.Config.default with disable_synth = true } + ~config:{ PIE.Config.default with disable_synth = true } ) - let append_job_3 = - - Job.create_unlabeled - ~f:(fun [@warning "-8"] [ List (INT, x) ; List (INT, y) ] - -> List (INT, (x @ y))) - ~args:([ ("x", Type.(LIST INT)) ; ("y", Type.(LIST INT)) ]) - ~post:(fun inp res -> - match [@warning "-8"] inp , res with - | [ List (INT, l1) ; List (INT, l2) ] , Ok (List (INT, res)) -> (List.length res) = 2) - (* We start with these two features and disable feature synthesis *) - ~features:[ - ((fun [@warning "-8"] [ List (INT, list1) ; _ ] -> List.is_empty list1), - "(= x [])") ; - ((fun [@warning "-8"] [ _ ; List (INT, list2) ] -> List.is_empty list2), - "(= y [])") ; - ] - - - (List.map ~f:( - fun (x,y) -> [x ;y]) - Quickcheck.(random_value - (Generator.list_with_length 4096 - (Generator.tuple2 - (TestGen.for_type (Type.LIST Type.INT)) - (TestGen.for_type (Type.LIST Type.INT)))))) - -let no_synth_PI_3 () = - Stdio.print_endline "PI for { append(l1,l2) = [] } without feature learning:" ; - print_PI_results ( - PIE.learnPreCond append_job_3 - ~config:PIE.Config.{ default with _Synthesizer = { default._Synthesizer with logic = Logic.of_string "ALL" } } - ) - -let rev_append_job = - - Job.create_unlabeled - ~f:(fun [@warning "-8"] [ List (INT, x) ; List (INT, y) ] - -> List (INT, (List.rev x @ y))) - ~args:([ ("x", Type.(LIST INT)) ; ("y", Type.(LIST INT)) ]) - ~post:(fun inp res -> - match [@warning "-8"] inp , res with - | [ List (INT, l1) ; List (INT, l2) ] , Ok (List (INT, res)) -> (List.equal Value.equal res (l1 @ l2))) - (* We start with these two features and disable feature synthesis *) - ~features:[ - ((fun [@warning "-8"] [ List (INT, list1) ; _ ] -> List.is_empty list1), - "(= x [])") ; - ((fun [@warning "-8"] [ _ ; List (INT, list2) ] -> List.is_empty list2), - "(= y [])") ; - ] - - (List.map ~f:( - fun (x,y) -> [x ;y]) - Quickcheck.(random_value - (Generator.list_with_length 4096 - (Generator.tuple2 - (TestGen.for_type (Type.LIST Type.INT)) - (TestGen.for_type (Type.LIST Type.INT)))))) - -let rev_append_synth_pi () = - Stdio.print_endline "PI for { rev append(l1,l2) = [] } without feature learning:" ; - print_PI_results ( - PIE.learnPreCond rev_append_job - ~config:PIE.Config.{ default with _Synthesizer = { default._Synthesizer with logic = Logic.of_string "ALL" } } - ) - - - - let comp_len_job = - - Job.create_unlabeled - ~f:(fun [@warning "-8"] [ List (INT, x) ; List (INT, y) ] - -> Int (compare( List.length x) (List.length y) )) - ~args:([ ("x", Type.(LIST INT)) ; ("y", Type.(LIST INT)) ]) - ~post:(fun inp res -> - match [@warning "-8"] inp , res with - | [ List (INT, l1) ; List (INT, l2) ] , Ok (Int res) -> (res = 0)) - (* We start with these two features and disable feature synthesis *) - ~features:[ - ((fun [@warning "-8"] [ List (INT, list1) ; _ ] -> List.is_empty list1), - "(= x [])") ; - ((fun [@warning "-8"] [ _ ; List (INT, list2) ] -> List.is_empty list2), - "(= y [])") ; - ] - - (List.map ~f:( - fun (x,y) -> [x ;y]) - Quickcheck.(random_value - (Generator.list_with_length 4096 - (Generator.tuple2 - (TestGen.for_type (Type.LIST Type.INT)) - (TestGen.for_type (Type.LIST Type.INT)))))) - -let comp_len_PI () = - Stdio.print_endline "PI for { compare_lengths l1 l2 = 0 } without feature learning:" ; - print_PI_results ( - PIE.learnPreCond comp_len_job - ~config:PIE.Config.{ default with _Synthesizer = { default._Synthesizer with logic = Logic.of_string "ALL" } } - ) - - - - - -let square_job = Job.create_unlabeled - ~f:(fun [@warning "-8"] [ Value.Int x ] -> Value.Int (x*x)) - ~args:([ ("x", Type.INT) ]) - ~post:(fun inp res -> - match [@warning "-8"] inp , res with - | [ Value.Int x ], Ok (Value.Int y) -> y/x = abs(x)) - (* We start with no initial features *) - ~features:[] - (* We have a random generator for Type.INT. - * We generate 64 random Value.Int elements - * and then wrap them in singleton lists (single arguments to abs). *) - (List.map ~f:(fun i -> [ i ]) - Quickcheck.(random_value - (Generator.list_with_length 64 - (TestGen.for_type Type.INT)))) - - let square_synth_pi () = - Stdio.print_endline "PI for { x = x*x } with feature learning:" ; - print_PI_results (PIE.learnPreCond square_job) - - - - - let cube_job = Job.create_unlabeled - ~f:(fun [@warning "-8"] [ Value.Int x ] -> Value.Int (x*x*x)) - ~args:([ ("x", Type.INT) ]) - ~post:(fun inp res -> - match [@warning "-8"] inp , res with - | [ Value.Int x ], Ok (Value.Int y) -> 1 < y) - (* We start with no initial features *) - ~features:[] - (* We have a random generator for Type.INT. - * We generate 64 random Value.Int elements - * and then wrap them in singleton lists (single arguments to abs). *) - (List.map ~f:(fun i -> [ i ]) - Quickcheck.(random_value - (Generator.list_with_length 64 - (TestGen.for_type Type.INT)))) - - let cube_synth_pi () = - Stdio.print_endline "PI for { x = x*x*x } with feature learning:" ; - print_PI_results (PIE.learnPreCond cube_job) - -let inverse_job = Job.create_unlabeled - ~f:(fun [@warning "-8"] [ Value.Int x ] -> Value.Int (1/x)) - ~args:([ ("x", Type.INT) ]) - ~post:(fun inp res -> - match [@warning "-8"] inp , res with - | [ Value.Int x ], Ok (Value.Int y) -> -x > y) - (* We start with no initial features *) - ~features:[] - (* We have a random generator for Type.INT. - * We generate 64 random Value.Int elements - * and then wrap them in singleton lists (single arguments to abs). *) - (List.map ~f:(fun i -> [ i ]) - Quickcheck.(random_value - (Generator.list_with_length 64 - (TestGen.for_type Type.INT)))) - - let inverse_synth_pi () = - Stdio.print_endline "PI for { x = 1 / x } with feature learning:" ; - print_PI_results (PIE.learnPreCond inverse_job) - - let even_job = Job.create_unlabeled - ~f:(fun [@warning "-8"] [ Value.Int x ] -> Value.Int ((x / 2) * 2)) - ~args:([ ("x", Type.INT) ]) - ~post:(fun inp res -> - match [@warning "-8"] inp , res with - | [ Value.Int x ], Ok (Value.Int y) -> x = y) - (* We start with no initial features *) - ~features:[] - (* We have a random generator for Type.INT. - * We generate 64 random Value.Int elements - * and then wrap them in singleton lists (single arguments to abs). *) - (List.map ~f:(fun i -> [ i ]) - Quickcheck.(random_value - (Generator.list_with_length 100 - (TestGen.for_type Type.INT)))) - - let even_synth_pi () = - Stdio.print_endline "PI for { x = (x / 2) * 2 } with feature learning:" ; - print_PI_results (PIE.learnPreCond even_job - ~config:{ PIE.Config.default with - _Synthesizer = { PIE.Config.default._Synthesizer with - logic = Logic.of_string "NIA" } } -) - - let product_job = Job.create_unlabeled - ~f:(fun [@warning "-8"] [ Value.Int x ; Value.Int y] -> Value.Int (x*y)) - ~args:([ ("x", Type.INT) ; ("y", Type.INT) ]) - ~post:(fun inp res -> - match [@warning "-8"] inp , res with - | [ Value.Int x ; Value.Int y], Ok (Value.Int r) -> r > x) - (* We start with no initial features *) - ~features:[] - (* We have a random generator for Type.INT. - * We generate 64 random Value.Int elements - * and then wrap them in singleton lists (single arguments to abs). *) - (List.map ~f:(fun i -> [ i ]) - Quickcheck.(random_value - (Generator.list_with_length 64 - (TestGen.for_type Type.INT)))) - - let product_synth_pi () = - Stdio.print_endline "PI for { x = x*y} with feature learning:" ; - print_PI_results (PIE.learnPreCond product_job) - - - - let avg_job = Job.create_unlabeled - ~f:(fun [@warning "-8"] [ Value.Int x ; Value.Int y; Value.Int z] -> Value.Int ((x + y + z) / 3)) - ~args:([ ("x", Type.INT) ; ("y", Type.INT) ; ("z", Type.INT) ]) - ~post:(fun inp res -> - match [@warning "-8"] inp , res with - | [ Value.Int x ; Value.Int y ; Value.Int z], Ok (Value.Int r) -> r = x) - (* We start with no initial features *) - ~features:[] - - - (List.map ~f:(fun (x,y,z) -> [ x ; y ; z]) - Quickcheck.(random_value - (Generator.list_with_length 64 - (Generator.tuple3 (TestGen.for_type Type.INT) (TestGen.for_type Type.INT) (TestGen.for_type Type.INT))))) - - let avg_synth_pi () = - Stdio.print_endline "PI for { x = avg(x, y, z)} with feature learning:" ; - print_PI_results (PIE.learnPreCond avg_job) - - - - let max_job = Job.create_unlabeled - ~f:(fun [@warning "-8"] [ Value.Int x ; Value.Int y] -> Value.Int (if x > y then x else y)) - ~args:([ ("x", Type.INT) ; ("y", Type.INT) ]) - ~post:(fun inp res -> - match [@warning "-8"] inp , res with - | [ Value.Int x ; Value.Int y], Ok (Value.Int r) -> r = x && r = y) - (* We start with no initial features *) - ~features:[] - (List.map ~f:(fun (x,y) -> [ x ; y ]) - Quickcheck.(random_value - (Generator.list_with_length 64 - (Generator.tuple2 (TestGen.for_type Type.INT) (TestGen.for_type Type.INT))))) - - let max_synth_pi () = - Stdio.print_endline "PI for { x = max(x, y)} with feature learning:" ; - print_PI_results (PIE.learnPreCond max_job) - - - -let int_average_job = Job.create_unlabeled - ~f:(fun [@warning "-8"] [ Value.Int x ; Value.Int y] -> Value.Int ((x+y)/2)) - ~args:([ ("x", Type.INT) ; ("y", Type.INT) ]) - ~post:(fun inp res -> - match [@warning "-8"] inp , res with - | [ Value.Int x ; Value.Int y], Ok (Value.Int r) -> r > x) - (* We start with no initial features *) - ~features:[] - [[Value.Int 1; Value.Int 3]; [Value.Int 4; Value.Int 4]; [Value.Int 5; Value.Int 3] ; [Value.Int 3; Value.Int 5]] - - let average_synth_pi () = - Stdio.print_endline "PI for { x = (x + y) / 2} with feature learning:" ; - print_PI_results (PIE.learnPreCond int_average_job) - - let int_average_job_2 = Job.create_unlabeled - ~f:(fun [@warning "-8"] [ Value.Int x ; Value.Int y] -> Value.Int ((x+y)/2)) - ~args:([ ("x", Type.INT) ; ("y", Type.INT) ]) - ~post:(fun inp res -> - match [@warning "-8"] inp , res with - | [ Value.Int x ; Value.Int y], Ok (Value.Int r) -> r < x) - (* We start with no initial features *) - ~features:[] - [[Value.Int 1; Value.Int 3]; [Value.Int 4; Value.Int 4]; [Value.Int 5; Value.Int 3] ; [Value.Int 3; Value.Int 5] ; [Value.Int 4; Value.Int 2]] - - let average_synth_pi_2 () = - Stdio.print_endline "PI for { x = (x + y) / 2} with feature learning:" ; - print_PI_results (PIE.learnPreCond int_average_job_2) - - let int_average_job_3 = Job.create_unlabeled - ~f:(fun [@warning "-8"] [ Value.Int x ; Value.Int y] -> Value.Int ((x+y)/2)) - ~args:([ ("x", Type.INT) ; ("y", Type.INT) ]) - ~post:(fun inp res -> - match [@warning "-8"] inp , res with - | [ Value.Int x ; Value.Int y], Ok (Value.Int r) -> r = x) - (* We start with no initial features *) - ~features:[] - [[Value.Int 1; Value.Int 3]; [Value.Int 4; Value.Int 4]; [Value.Int 5; Value.Int 3] ; [Value.Int 3; Value.Int 5] ; [Value.Int 4; Value.Int 2]] - - let average_synth_pi_3 () = - Stdio.print_endline "PI for { x = (x + y) / 2} with feature learning:" ; - print_PI_results (PIE.learnPreCond int_average_job_3) - - - - let () = with_synth_PI () - ; real_abs_PI () - ; real_prod_PI () ; no_synth_PI () - ; no_synth_PI_2 () - ; no_synth_PI_3 () - ; rev_append_synth_pi () - ; comp_len_PI () - ; square_synth_pi () - ; cube_synth_pi () - ; inverse_synth_pi () - ; product_synth_pi () - ; max_synth_pi () - ; average_synth_pi () - ; average_synth_pi_2 () - ; average_synth_pi_3 () - ; even_synth_pi () - ; avg_synth_pi () - - From a92dd867e297541eeb5dc5409d082c092341cae1 Mon Sep 17 00:00:00 2001 From: Julia Offerman <59590610+juliaofferman@users.noreply.github.com> Date: Fri, 31 Jul 2020 13:25:11 -0700 Subject: [PATCH 22/38] Tests for real components --- test/Test_RealComponents.ml | 83 +++++++++++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) create mode 100644 test/Test_RealComponents.ml diff --git a/test/Test_RealComponents.ml b/test/Test_RealComponents.ml new file mode 100644 index 0000000..98793d6 --- /dev/null +++ b/test/Test_RealComponents.ml @@ -0,0 +1,83 @@ +open Base + +open LoopInvGen + +let add_eval = (List.find_exn RealComponents.translation + ~f:(fun comp -> String.equal comp.name "real-add")).evaluate +let sub_eval = (List.find_exn RealComponents.translation + ~f:(fun comp -> String.equal comp.name "real-sub")).evaluate + +let mult_eval = (List.find_exn ArrayComponents.scaling + ~f:(fun comp -> String.equal comp.name "real-mult")).evaluate +let div_eval = (List.find_exn ArrayComponents.scaling + ~f:(fun comp -> String.equal comp.name "real-div")).evaluate + +let eq_eval = (List.find_exn ArrayComponents.conditionals + ~f:(fun comp -> String.equal comp.name "real-eq")).evaluate +let geq_eval = (List.find_exn ArrayComponents.conditionals + ~f:(fun comp -> String.equal comp.name "real-geq")).evaluate +let leq_eval = (List.find_exn ArrayComponents.conditionals + ~f:(fun comp -> String.equal comp.name "real-leq")).evaluate +let ite_eval = (List.find_exn ArrayComponents.conditionals + ~f:(fun comp -> String.equal comp.name "real-ite")).evaluate + +let add () = + let rl = [Value.Real 3.54 ; Value.Real 7.52] in + let add_ret = add_eval rl in + let res = Value.equal add_ret (Value.Real 11.06) + in Alcotest.(check bool) "identical" true res + +let sub () = + let rl = [Value.Real 7.52 ; Value.Real 3.54] in + let sub_ret = sub_eval rl in + let res = Value.equal add_ret (Value.Real 3.98) + in Alcotest.(check bool) "identical" true res + +let mult () = + let rl = [Value.Real 3.54 ; Value.Real 7.52] in + let mult_ret = mult_eval rl in + let res = Value.equal add_ret (Value.Real 26.8208) + in Alcotest.(check bool) "identical" true res + +let div () = + let rl = [Value.Real 3. ; Value.Real 2.] in + let div_ret = div_eval rl in + let res = Value.equal div_ret (Value.Real 1.5) + in Alcotest.(check bool) "identical" true res + +let eq () = + let rl = [Value.Real 3.54 ; Value.Real 3.54] in + let eq_ret = eq_eval rl in + let res = Value.equal eq_ret (Value.Bool true) + in Alcotest.(check bool) "identical" true res + + +let geq () = + let rl = [Value.Real 7.52 ; Value.Real 3.54] in + let geq_ret = geq_eval rl in + let res = Value.equal geq_ret (Value.Bool true) + in Alcotest.(check bool) "identical" true res + +let leq () = + let rl = [Value.Real 3.54 ; Value.Real 7.52] in + let leq_ret = leq_eval rl in + let res = Value.equal leq_ret (Value.Bool true) + in Alcotest.(check bool) "identical" true res + +let ite () = + let rl = [Value.Bool false ; Value.Real 3.54 ; Value.Real 7.52] in + let ite_ret = ite_eval rl in + let res = Value.equal ite_ret (Value.Real 7.52) + in Alcotest.(check bool) "identical" true res + + +let all = [ + "add", `Quick, add ; + "sub", `Quick, sub ; + "mult", `Quick, mult ; + "div", `Quick, div ; + "eq", `Quick, eq ; + "geq", `Quick, geq ; + "leq", `Quick, leq ; + "ite", `Quick, ite ; +] From 0992af0b228fbb4b3744ecbad81413c664dab031 Mon Sep 17 00:00:00 2001 From: Julia Offerman <59590610+juliaofferman@users.noreply.github.com> Date: Fri, 31 Jul 2020 14:00:55 -0700 Subject: [PATCH 23/38] Update to include real component tests --- test/Runner.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/test/Runner.ml b/test/Runner.ml index c5554a1..96eac49 100644 --- a/test/Runner.ml +++ b/test/Runner.ml @@ -3,6 +3,7 @@ let () = (* FIXME: Find a way to pass command-line arguments within dune's runtest alias *) (let zpath = if (Array.length Sys.argv) > 1 then Sys.argv.(1) else "" in [ "Test_ArrayComponents", Test_ArrayComponents.all + ; "Test_RealComponents", Test_RealComponents.all ; "Test_BFL", Test_BFL.all ; "Test_Expr", Test_Expr.all ; "Test_NormalForm", Test_NormalForm.all @@ -11,4 +12,4 @@ let () = ; "Test_Unification", Test_Unification.all ; "Test_VPIE", (Test_VPIE.all ~zpath) ; "Test_ZProc", (Test_ZProc.all ~zpath) - ]) \ No newline at end of file + ]) From 3e54caa3b17e89e22502c9ea6b96cd116c9534b5 Mon Sep 17 00:00:00 2001 From: Julia Offerman <59590610+juliaofferman@users.noreply.github.com> Date: Fri, 31 Jul 2020 14:13:18 -0700 Subject: [PATCH 24/38] Update Test_RealComponents.ml --- test/Test_RealComponents.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/test/Test_RealComponents.ml b/test/Test_RealComponents.ml index 98793d6..d181e5c 100644 --- a/test/Test_RealComponents.ml +++ b/test/Test_RealComponents.ml @@ -7,18 +7,18 @@ let add_eval = (List.find_exn RealComponents.translation let sub_eval = (List.find_exn RealComponents.translation ~f:(fun comp -> String.equal comp.name "real-sub")).evaluate -let mult_eval = (List.find_exn ArrayComponents.scaling +let mult_eval = (List.find_exn RealComponents.scaling ~f:(fun comp -> String.equal comp.name "real-mult")).evaluate -let div_eval = (List.find_exn ArrayComponents.scaling +let div_eval = (List.find_exn RealComponents.scaling ~f:(fun comp -> String.equal comp.name "real-div")).evaluate -let eq_eval = (List.find_exn ArrayComponents.conditionals +let eq_eval = (List.find_exn RealComponents.conditionals ~f:(fun comp -> String.equal comp.name "real-eq")).evaluate -let geq_eval = (List.find_exn ArrayComponents.conditionals +let geq_eval = (List.find_exn RealComponents.conditionals ~f:(fun comp -> String.equal comp.name "real-geq")).evaluate -let leq_eval = (List.find_exn ArrayComponents.conditionals +let leq_eval = (List.find_exn RealComponents.conditionals ~f:(fun comp -> String.equal comp.name "real-leq")).evaluate -let ite_eval = (List.find_exn ArrayComponents.conditionals +let ite_eval = (List.find_exn RealComponents.conditionals ~f:(fun comp -> String.equal comp.name "real-ite")).evaluate let add () = @@ -30,13 +30,13 @@ let add () = let sub () = let rl = [Value.Real 7.52 ; Value.Real 3.54] in let sub_ret = sub_eval rl in - let res = Value.equal add_ret (Value.Real 3.98) + let res = Value.equal sub_ret (Value.Real 3.98) in Alcotest.(check bool) "identical" true res let mult () = let rl = [Value.Real 3.54 ; Value.Real 7.52] in let mult_ret = mult_eval rl in - let res = Value.equal add_ret (Value.Real 26.8208) + let res = Value.equal mult_ret (Value.Real 26.8208) in Alcotest.(check bool) "identical" true res let div () = From e9746d5dfc46832d96bf0ecd7b0150a0b99229ad Mon Sep 17 00:00:00 2001 From: Julia Offerman <59590610+juliaofferman@users.noreply.github.com> Date: Thu, 6 Aug 2020 10:39:52 -0700 Subject: [PATCH 25/38] Update Test_RealComponents.ml --- test/Test_RealComponents.ml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/test/Test_RealComponents.ml b/test/Test_RealComponents.ml index d181e5c..1880bff 100644 --- a/test/Test_RealComponents.ml +++ b/test/Test_RealComponents.ml @@ -2,6 +2,10 @@ open Base open LoopInvGen +let value_of : Value.t -> float = + function [@warning "-8"] + | Real x -> x + let add_eval = (List.find_exn RealComponents.translation ~f:(fun comp -> String.equal comp.name "real-add")).evaluate let sub_eval = (List.find_exn RealComponents.translation @@ -24,19 +28,19 @@ let ite_eval = (List.find_exn RealComponents.conditionals let add () = let rl = [Value.Real 3.54 ; Value.Real 7.52] in let add_ret = add_eval rl in - let res = Value.equal add_ret (Value.Real 11.06) + let res = Value.equal (Value.Int 0) (Value.Int (Core_kernel.Float.robustly_compare (value_of add_ret) 11.06)) in Alcotest.(check bool) "identical" true res let sub () = let rl = [Value.Real 7.52 ; Value.Real 3.54] in let sub_ret = sub_eval rl in - let res = Value.equal sub_ret (Value.Real 3.98) + let res = Value.equal (Value.Int 0) (Value.Int (Core_kernel.Float.robustly_compare (value_of sub_ret) 3.98)) in Alcotest.(check bool) "identical" true res let mult () = let rl = [Value.Real 3.54 ; Value.Real 7.52] in let mult_ret = mult_eval rl in - let res = Value.equal mult_ret (Value.Real 26.8208) + let res = Value.equal (Value.Int 0) (Value.Int (Core_kernel.Float.robustly_compare (value_of mult_ret) 26.6208)) in Alcotest.(check bool) "identical" true res let div () = @@ -80,4 +84,5 @@ let all = [ "geq", `Quick, geq ; "leq", `Quick, leq ; "ite", `Quick, ite ; + ] From 105745e67a91d6234da7e6f5dceb187ce2dc7709 Mon Sep 17 00:00:00 2001 From: Julia Offerman <59590610+juliaofferman@users.noreply.github.com> Date: Thu, 6 Aug 2020 10:47:47 -0700 Subject: [PATCH 26/38] Update Test_RealComponents.ml --- test/Test_RealComponents.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/test/Test_RealComponents.ml b/test/Test_RealComponents.ml index 1880bff..651c789 100644 --- a/test/Test_RealComponents.ml +++ b/test/Test_RealComponents.ml @@ -28,19 +28,19 @@ let ite_eval = (List.find_exn RealComponents.conditionals let add () = let rl = [Value.Real 3.54 ; Value.Real 7.52] in let add_ret = add_eval rl in - let res = Value.equal (Value.Int 0) (Value.Int (Core_kernel.Float.robustly_compare (value_of add_ret) 11.06)) + let res = equal 0 (Core_kernel.Float.robustly_compare (value_of add_ret) 11.06) in Alcotest.(check bool) "identical" true res let sub () = let rl = [Value.Real 7.52 ; Value.Real 3.54] in let sub_ret = sub_eval rl in - let res = Value.equal (Value.Int 0) (Value.Int (Core_kernel.Float.robustly_compare (value_of sub_ret) 3.98)) + let res = equal 0 (Core_kernel.Float.robustly_compare (value_of sub_ret) 3.98) in Alcotest.(check bool) "identical" true res let mult () = let rl = [Value.Real 3.54 ; Value.Real 7.52] in let mult_ret = mult_eval rl in - let res = Value.equal (Value.Int 0) (Value.Int (Core_kernel.Float.robustly_compare (value_of mult_ret) 26.6208)) + let res = equal 0 (Core_kernel.Float.robustly_compare (value_of mult_ret) 26.6208) in Alcotest.(check bool) "identical" true res let div () = From 189fb5c4ba729464378a9741bc4473ee928def9c Mon Sep 17 00:00:00 2001 From: Julia Offerman <59590610+juliaofferman@users.noreply.github.com> Date: Sat, 8 Aug 2020 12:47:26 -0700 Subject: [PATCH 27/38] Add additional tests --- test/Test_RealComponents.ml | 104 +++++++++++++++++++++++++++++++++++- 1 file changed, 102 insertions(+), 2 deletions(-) diff --git a/test/Test_RealComponents.ml b/test/Test_RealComponents.ml index 651c789..6d5d9a9 100644 --- a/test/Test_RealComponents.ml +++ b/test/Test_RealComponents.ml @@ -31,30 +31,84 @@ let add () = let res = equal 0 (Core_kernel.Float.robustly_compare (value_of add_ret) 11.06) in Alcotest.(check bool) "identical" true res +let add_zero () = + let rl = [Value.Real 993.54 ; Value.Real 0.] in + let add_ret = add_eval rl in + let res = equal 0 (Core_kernel.Float.robustly_compare (value_of add_ret) 993.54) + in Alcotest.(check bool) "identical" true res + +let add_neg () = + let rl = [Value.Real 3.54 ; Value.Real ~-.10.1] in + let add_ret = add_eval rl in + let res = equal 0 (Core_kernel.Float.robustly_compare (value_of add_ret) ~-.6.56) + in Alcotest.(check bool) "identical" true res + + let sub () = let rl = [Value.Real 7.52 ; Value.Real 3.54] in let sub_ret = sub_eval rl in let res = equal 0 (Core_kernel.Float.robustly_compare (value_of sub_ret) 3.98) in Alcotest.(check bool) "identical" true res +let sub_zero () = + let rl = [Value.Real 7.543 ; Value.Real 0. ] in + let sub_ret = sub_eval rl in + let res = equal 0 (Core_kernel.Float.robustly_compare (value_of sub_ret) 7.543) + in Alcotest.(check bool) "identical" true res + +let sub_neg () = + let rl = [Value.Real 0. ; Value.Real 3.54] in + let sub_ret = sub_eval rl in + let res = equal 0 (Core_kernel.Float.robustly_compare (value_of sub_ret) ~-.3.54) + in Alcotest.(check bool) "identical" true res + let mult () = let rl = [Value.Real 3.54 ; Value.Real 7.52] in let mult_ret = mult_eval rl in let res = equal 0 (Core_kernel.Float.robustly_compare (value_of mult_ret) 26.6208) in Alcotest.(check bool) "identical" true res +let mult_zero () = + let rl = [Value.Real 3.54 ; Value.Real 0.] in + let mult_ret = mult_eval rl in + let res = equal 0 (Core_kernel.Float.robustly_compare (value_of mult_ret) 0.) + in Alcotest.(check bool) "identical" true res + +let mult_neg () = + let rl = [Value.Real 3.54 ; Value.Real ~-.5.42] in + let mult_ret = mult_eval rl in + let res = equal 0 (Core_kernel.Float.robustly_compare (value_of mult_ret) ~-.19.1868) + in Alcotest.(check bool) "identical" true res + let div () = let rl = [Value.Real 3. ; Value.Real 2.] in let div_ret = div_eval rl in let res = Value.equal div_ret (Value.Real 1.5) in Alcotest.(check bool) "identical" true res +let div_neg () = + let rl = [Value.Real 3. ; Value.Real ~-.2.] in + let div_ret = div_eval rl in + let res = Value.equal div_ret (Value.Real ~-.1.5) + in Alcotest.(check bool) "identical" true res + let eq () = let rl = [Value.Real 3.54 ; Value.Real 3.54] in let eq_ret = eq_eval rl in let res = Value.equal eq_ret (Value.Bool true) in Alcotest.(check bool) "identical" true res - + +let eq_not () = + let rl = [Value.Real 3.54 ; Value.Real 3.59] in + let eq_ret = eq_eval rl in + let res = Value.equal eq_ret (Value.Bool false) + in Alcotest.(check bool) "identical" true res + +let eq_neg () = + let rl = [Value.Real 3.54 ; Value.Real ~-.3.54] in + let eq_ret = eq_eval rl in + let res = Value.equal eq_ret (Value.Bool false) + in Alcotest.(check bool) "identical" true res let geq () = let rl = [Value.Real 7.52 ; Value.Real 3.54] in @@ -62,27 +116,73 @@ let geq () = let res = Value.equal geq_ret (Value.Bool true) in Alcotest.(check bool) "identical" true res +let geq_eq () = + let rl = [Value.Real 7.52 ; Value.Real 7.52] in + let geq_ret = geq_eval rl in + let res = Value.equal geq_ret (Value.Bool true) + in Alcotest.(check bool) "identical" true res + +let geq_not () = + let rl = [Value.Real 7.52 ; Value.Real 7.54] in + let geq_ret = geq_eval rl in + let res = Value.equal geq_ret (Value.Bool false) + in Alcotest.(check bool) "identical" true res + let leq () = let rl = [Value.Real 3.54 ; Value.Real 7.52] in let leq_ret = leq_eval rl in let res = Value.equal leq_ret (Value.Bool true) in Alcotest.(check bool) "identical" true res +let leq_eq () = + let rl = [Value.Real 7.42 ; Value.Real 7.42] in + let leq_ret = leq_eval rl in + let res = Value.equal leq_ret (Value.Bool true) + in Alcotest.(check bool) "identical" true res + +let leq_not () = + let rl = [Value.Real ~-.3.54 ; Value.Real ~-.7.52] in + let leq_ret = leq_eval rl in + let res = Value.equal leq_ret (Value.Bool false) + in Alcotest.(check bool) "identical" true res + let ite () = let rl = [Value.Bool false ; Value.Real 3.54 ; Value.Real 7.52] in let ite_ret = ite_eval rl in let res = Value.equal ite_ret (Value.Real 7.52) in Alcotest.(check bool) "identical" true res +let ite_true () = + let rl = [Value.Bool true ; Value.Real 3.54 ; Value.Real 7.52] in + let ite_ret = ite_eval rl in + let res = Value.equal ite_ret (Value.Real 3.54) + in Alcotest.(check bool) "identical" true res + + + let all = [ "add", `Quick, add ; + "add_zero", `Quick, add_zero ; + "add_neg", `Quick, add_neg ; "sub", `Quick, sub ; - "mult", `Quick, mult ; + "sub_zero", `Quick, sub_zero ; + "sub_neg", `Quick, sub_neg ; + "mult", `Quick, mult ; + "mult_zero", `Quick, mult_zero ; + "mult_neg", `Quick, mult_neg ; "div", `Quick, div ; + "div_neg", `Quick, div_neg ; "eq", `Quick, eq ; + "eq_not", `Quick, eq_not ; + "eq_neg", `Quick, eq_neg ; "geq", `Quick, geq ; + "geq_eq", `Quick, geq_eq ; + "geq_not", `Quick, geq_not ; "leq", `Quick, leq ; + "leq_eq", `Quick, leq_eq ; + "leq_not", `Quick, leq_not ; "ite", `Quick, ite ; + "ite_true", `Quick, ite_true ; ] From 00cb3d706b78da80c176dd27c5c3c24edd0f8171 Mon Sep 17 00:00:00 2001 From: Julia Offerman <59590610+juliaofferman@users.noreply.github.com> Date: Thu, 13 Aug 2020 12:24:25 -0700 Subject: [PATCH 28/38] Fix negation --- test/Test_RealComponents.ml | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/test/Test_RealComponents.ml b/test/Test_RealComponents.ml index 6d5d9a9..c3f4dd3 100644 --- a/test/Test_RealComponents.ml +++ b/test/Test_RealComponents.ml @@ -38,9 +38,9 @@ let add_zero () = in Alcotest.(check bool) "identical" true res let add_neg () = - let rl = [Value.Real 3.54 ; Value.Real ~-.10.1] in + let rl = [Value.Real 3.54 ; Value.Real (-10.1)] in let add_ret = add_eval rl in - let res = equal 0 (Core_kernel.Float.robustly_compare (value_of add_ret) ~-.6.56) + let res = equal 0 (Core_kernel.Float.robustly_compare (value_of add_ret) (-6.56)) in Alcotest.(check bool) "identical" true res @@ -59,7 +59,7 @@ let sub_zero () = let sub_neg () = let rl = [Value.Real 0. ; Value.Real 3.54] in let sub_ret = sub_eval rl in - let res = equal 0 (Core_kernel.Float.robustly_compare (value_of sub_ret) ~-.3.54) + let res = equal 0 (Core_kernel.Float.robustly_compare (value_of sub_ret) (-3.54)) in Alcotest.(check bool) "identical" true res let mult () = @@ -75,9 +75,9 @@ let mult_zero () = in Alcotest.(check bool) "identical" true res let mult_neg () = - let rl = [Value.Real 3.54 ; Value.Real ~-.5.42] in + let rl = [Value.Real 3.54 ; Value.Real (-5.42)] in let mult_ret = mult_eval rl in - let res = equal 0 (Core_kernel.Float.robustly_compare (value_of mult_ret) ~-.19.1868) + let res = equal 0 (Core_kernel.Float.robustly_compare (value_of mult_ret) (-19.1868)) in Alcotest.(check bool) "identical" true res let div () = @@ -87,9 +87,9 @@ let div () = in Alcotest.(check bool) "identical" true res let div_neg () = - let rl = [Value.Real 3. ; Value.Real ~-.2.] in + let rl = [Value.Real 3. ; Value.Real (-2.)] in let div_ret = div_eval rl in - let res = Value.equal div_ret (Value.Real ~-.1.5) + let res = Value.equal div_ret (Value.Real (-1.5)) in Alcotest.(check bool) "identical" true res let eq () = @@ -105,7 +105,7 @@ let eq_not () = in Alcotest.(check bool) "identical" true res let eq_neg () = - let rl = [Value.Real 3.54 ; Value.Real ~-.3.54] in + let rl = [Value.Real 3.54 ; Value.Real (-3.54)] in let eq_ret = eq_eval rl in let res = Value.equal eq_ret (Value.Bool false) in Alcotest.(check bool) "identical" true res @@ -141,7 +141,7 @@ let leq_eq () = in Alcotest.(check bool) "identical" true res let leq_not () = - let rl = [Value.Real ~-.3.54 ; Value.Real ~-.7.52] in + let rl = [Value.Real (-3.54) ; Value.Real (-7.52)] in let leq_ret = leq_eval rl in let res = Value.equal leq_ret (Value.Bool false) in Alcotest.(check bool) "identical" true res From 80027a7a18b7011ed9b8d7d61941765354dea9bc Mon Sep 17 00:00:00 2001 From: Julia Offerman <59590610+juliaofferman@users.noreply.github.com> Date: Thu, 19 Nov 2020 13:34:04 -0800 Subject: [PATCH 29/38] Adding "LRA" logic --- src/Logic.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Logic.ml b/src/Logic.ml index 0cc1999..d296b20 100644 --- a/src/Logic.ml +++ b/src/Logic.ml @@ -43,6 +43,10 @@ let all_supported = components_per_level = ArrayComponents.levels ++ BooleanComponents.levels ++ IntegerComponents.non_linear_levels ++ ListComponents.levels ++ RealComponents.levels ; sample_set_size_multiplier = 8 + }; { + name = "LRA" ; + components_per_level = RealComponents.levels ++ BooleanComponents.levels ; + sample_set_size_multiplier = 8 }] ; table From c6ebeeb8b17911cde32452301b8f46322b16ad2e Mon Sep 17 00:00:00 2001 From: Julia Offerman <59590610+juliaofferman@users.noreply.github.com> Date: Thu, 19 Nov 2020 13:35:07 -0800 Subject: [PATCH 30/38] Remove scaling from levels --- src/RealComponents.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/RealComponents.ml b/src/RealComponents.ml index 924f6e9..fa53bf2 100644 --- a/src/RealComponents.ml +++ b/src/RealComponents.ml @@ -128,6 +128,6 @@ let conditionals = [ -let levels = [| translation ; scaling ; conditionals |] +let levels = [| translation ; conditionals |] let no_bool_levels = [| translation ; scaling |] From c5b1c6646f59f918e59fb98b6df19da8d2cf8fec Mon Sep 17 00:00:00 2001 From: Julia Offerman <59590610+juliaofferman@users.noreply.github.com> Date: Thu, 19 Nov 2020 13:38:27 -0800 Subject: [PATCH 31/38] Various changes to support Real type Added case for evaluating sexp's using division, updated of_atomic_string to support reals --- src/Value.ml | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/src/Value.ml b/src/Value.ml index 418cc82..52db4bb 100644 --- a/src/Value.ml +++ b/src/Value.ml @@ -1,7 +1,10 @@ open Base + open Exceptions + + module T = struct type t = Int of int | Bool of bool @@ -17,6 +20,7 @@ end include T include Comparable.Make (T) + let rec typeof : t -> Type.t = function | Int _ -> Type.INT | Bool _ -> Type.BOOL @@ -32,7 +36,7 @@ let rec to_string : t -> string = function | Bool b -> Bool.to_string b | Char c -> "\'" ^ (Char.to_string c) ^ "\'" | String s -> "\"" ^ s ^ "\"" - | Real r -> Float.(if r < 0. then "(" ^ (to_string r) ^ ")" else to_string r) + | Real r -> Float.to_string r | List _ -> raise (Internal_Exn "List type (de/)serialization not implemented!") | Array (key_type, val_type, value, default_v) -> let default_string = "((as const (Array " ^ (Type.to_string key_type) ^ " " ^ (Type.to_string val_type) ^ ")) " ^ (to_string default_v) ^ ")" @@ -49,9 +53,19 @@ let of_atomic_string (s : string) : t = (chop_prefix_exn ~prefix:"\'" s)))) with Invalid_argument _ -> try String String.(chop_suffix_exn ~suffix:"\"" (chop_prefix_exn ~prefix:"\"" s)) + with Invalid_argument _ -> try + Real (Float.of_string s) with Invalid_argument _ -> raise (Parse_Exn ("Failed to parse value `" ^ s ^ "`.")) + + let value_of_real_atomic_string (s : string) : float = + try + (Float.of_string s) + with Invalid_argument _ -> + raise (Parse_Exn ("Failed to parse value `" ^ s ^ "`.")) + + (* We assume that an array serialization provides explicit (k,v) pairs -- * either using nested `store` calls, or if-then-else constructs. * The different array formats are described in more details here: @@ -82,9 +96,15 @@ and [@warning "-8"] parse_named_array (sexp : Sexp.t) and of_sexp (sexp : Sexp.t) : t = let open Sexp in + Log.debug (lazy ("sexp: " ^ (Sexp.to_string sexp))); match sexp with | Atom v -> (of_atomic_string v) | List([(Atom "-") ; (Atom v)]) -> (of_atomic_string ("-" ^ v)) + | List([(Atom "-") ; s]) -> begin match (of_sexp s) with + | Real r -> Real (-1.0 *. r) + | _ -> raise (Internal_Exn ("Real type not passed: " + ^ (to_string_hum sexp))) end + | List([(Atom "/") ; (Atom num) ; (Atom denom)]) -> Real ((Float.of_string num) /. (Float.of_string denom)) | List([List([ Atom "as"; Atom "const"; _ ]); _]) | List([Atom "store";_;_;_]) -> (let key_type, val_type, arr,def_val = (parse_array [] sexp) in Array ((key_type) , (val_type) ,arr, def_val)) @@ -94,5 +114,7 @@ and of_sexp (sexp : Sexp.t) : t = | _ -> raise (Internal_Exn ("Unable to deserialize value: " ^ (to_string_hum sexp))) + + let of_string (s : string) : t = (of_sexp (Core.Sexp.of_string s)) From 9524dd75cb2f0bfa27850490aa74f84615d4b699 Mon Sep 17 00:00:00 2001 From: Julia Offerman <59590610+juliaofferman@users.noreply.github.com> Date: Thu, 21 Jan 2021 18:10:00 -0800 Subject: [PATCH 32/38] Add linear multiplication and division --- src/RealComponents.ml | 35 ++++++++++++++++++++++++++++++++++- 1 file changed, 34 insertions(+), 1 deletion(-) diff --git a/src/RealComponents.ml b/src/RealComponents.ml index fa53bf2..4617f6e 100644 --- a/src/RealComponents.ml +++ b/src/RealComponents.ml @@ -78,6 +78,38 @@ let scaling = [ } ] +let linear = [ + { + name = "real-lin-div"; + codomain = Type.REAL; + domain = Type.[REAL; REAL]; + is_argument_valid = Value.(function + | [x ; y] -> x =/= y + && (x =/= Const (Real 0.)) && (x =/= Const (Real 1.)) && (x =/= Const (Real (-1.))) + && (y =/= Const (Real 0.)) && (y =/= Const (Real 1.)) && (y =/= Const (Real (-1.))) + && ((is_constant y)) + | _ -> false); + evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Real ((value_of v1) /. (value_of v2))); + to_string = (fun [@warning "-8"] [a ; b] -> "(/ " ^ a ^ " " ^ b ^ ")"); + global_constraints = (fun [@warning "-8"] [_ ; b] -> ["(not (= 0 " ^ b ^ "))"]); + } ; + { + name = "real-lin-mult"; + codomain = Type.REAL; + domain = Type.[REAL; REAL]; + is_argument_valid = Value.(function + | [x ; y] + -> (x =/= Const (Real 0.)) && (x =/= Const (Real 1.)) + && (y =/= Const (Real 0.)) && (y =/= Const (Real 1.)) + && (is_constant x || is_constant y) + | _ -> false); + evaluate = Value.(fun [@warning "-8"] [x ; y] -> Real ((value_of x) *. (value_of y))); + to_string = (fun [@warning "-8"] [a ; b] -> "(* " ^ a ^ " " ^ b ^ ")"); + global_constraints = (fun _ -> []) + } + +] + let conditionals = [ { name = "real-eq"; @@ -124,10 +156,11 @@ let conditionals = [ to_string = (fun [@warning "-8"] [a ; b ; c] -> "IF(" ^ a ^ "," ^ b ^ "," ^ c ^ ")"); global_constraints = (fun _ -> []) } + ] -let levels = [| translation ; conditionals |] +let levels = [| translation ; conditionals ; linear |] let no_bool_levels = [| translation ; scaling |] From c9981aaaced4c42e11c7a7e7fe5e68ea6f527185 Mon Sep 17 00:00:00 2001 From: Julia Offerman <59590610+juliaofferman@users.noreply.github.com> Date: Thu, 21 Jan 2021 19:12:34 -0800 Subject: [PATCH 33/38] Remove unnecessary log --- src/Value.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Value.ml b/src/Value.ml index 52db4bb..c133d9d 100644 --- a/src/Value.ml +++ b/src/Value.ml @@ -96,7 +96,6 @@ and [@warning "-8"] parse_named_array (sexp : Sexp.t) and of_sexp (sexp : Sexp.t) : t = let open Sexp in - Log.debug (lazy ("sexp: " ^ (Sexp.to_string sexp))); match sexp with | Atom v -> (of_atomic_string v) | List([(Atom "-") ; (Atom v)]) -> (of_atomic_string ("-" ^ v)) From a06b01b0c41c5a4781dbad37acc05a89ca5343b5 Mon Sep 17 00:00:00 2001 From: Julia Offerman <59590610+juliaofferman@users.noreply.github.com> Date: Thu, 21 Jan 2021 19:15:25 -0800 Subject: [PATCH 34/38] Fix spacing --- src/Type.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Type.ml b/src/Type.ml index 388c5c6..8ddd320 100644 --- a/src/Type.ml +++ b/src/Type.ml @@ -24,7 +24,7 @@ let rec of_sexp (sexp: Sexp.t) : t = | Atom "Bool" -> BOOL | Atom "Char" -> CHAR | Atom "String" -> STRING - | Atom "Real" -> REAL + | Atom "Real" -> REAL | List [Atom "List" ; typ] -> LIST (of_sexp typ) | List [Atom "Array" ; index ; value] From 1eb5d9351fdbed5118ab8050c3280500a9bca950 Mon Sep 17 00:00:00 2001 From: Julia Offerman <59590610+juliaofferman@users.noreply.github.com> Date: Thu, 21 Jan 2021 19:38:36 -0800 Subject: [PATCH 35/38] Add real tests --- test/Test_Synthesizer.ml | 31 +++++++++++++++++++++++++++++-- 1 file changed, 29 insertions(+), 2 deletions(-) diff --git a/test/Test_Synthesizer.ml b/test/Test_Synthesizer.ml index 43c77a4..6ee0a94 100644 --- a/test/Test_Synthesizer.ml +++ b/test/Test_Synthesizer.ml @@ -180,9 +180,34 @@ let all_mapR_ge_l_0 () = constants = [] } in Alcotest.(check string) "identical" "(all (map-fixR-int-geq l 0))" result.string +let real_add () = + let open Synthesizer in + let result = solve ~config:{ Config.default with logic = Logic.of_string "LRA" } { + arg_names = [ "x" ; "y" ; "z" ]; + inputs = List.map ~f:(Array.map ~f:(fun r -> Value.Real r)) + [ [| 1.7 ; 2. ; 3. ; 4.1 ; 5.; 6.|]; + [| 1. ; 0.5; 1.; 0.25 ; (-0.2); 1. |]; + [| 2.7 ; 2.5; 3.; 4.35 ; 4.8; 8.1 |] ]; + outputs = Array.map ~f:(fun b -> Value.Bool b) + [| true; true; false; true; true; false |]; + constants = [] + } in Alcotest.(check string) "identical" "(= (+ x y) z)" result.string + +let real_div () = + let open Synthesizer in + let result = solve ~config:{ Config.default with logic = Logic.of_string "LRA" } { + arg_names = [ "x" ; "y" ]; + inputs = List.map ~f:(Array.map ~f:(fun r -> Value.Real r)) + [ [| 3. ; 7. ; -1.5 ; -4.5 ; -3.2 ; 8.1 |]; + [| 6.0 ; 15.6 ; -3.0 ; -9.0 ; -6.0 ; 16.2 |] ]; + outputs = Array.map ~f:(fun b -> Value.Bool b) + [| true ; false ; true ; true ; false ; true |]; + constants = [] + } in Alcotest.(check string) "identical" "(= (/ y 2.) x)" result.string + let all = [ "(+ x y)", `Quick, plus_x_y ; - "(>= (+ x z) y)", `Quick, ge_plus_x_z_y ; + "(>= (+ x z) y)", `Quick, ge_plus_x_z_y ; "(not (= (= w x) (= y z)))", `Quick, not_or_eq_w_x_eq_y_z ; "(select a k)", `Quick, select_a_k ; "(store a k v) ; empty", `Quick, store_a_k_v__empty ; @@ -191,4 +216,6 @@ let all = [ "(store a k v) ; with duplicates", `Quick, store_a_k_v__with_duplicates ; "(>= y (len x))", `Quick, ge_y_len_x ; "(all (map-fixR-int-geq l 0))", `Quick, all_mapR_ge_l_0 ; -] \ No newline at end of file + "(= (+ x y) z)", `Quick, real_add ; + "(= (/ y 2.) x)", `Quick, real_div ; +] From f32bbcf6737d4c5efd5e9069e8dae0f4c5522517 Mon Sep 17 00:00:00 2001 From: Julia Offerman <59590610+juliaofferman@users.noreply.github.com> Date: Thu, 21 Jan 2021 21:15:35 -0800 Subject: [PATCH 36/38] LRA benchmark --- benchmarks/LRA/dec-simpl.sl | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 benchmarks/LRA/dec-simpl.sl diff --git a/benchmarks/LRA/dec-simpl.sl b/benchmarks/LRA/dec-simpl.sl new file mode 100644 index 0000000..9ceafd9 --- /dev/null +++ b/benchmarks/LRA/dec-simpl.sl @@ -0,0 +1,15 @@ +(set-logic LRA) + +(synth-inv inv_fun ((x Real) (n Real))) + +(define-fun pre_fun ((x Real) (n Real)) Bool + (= x n)) +(define-fun trans_fun ((x Real) (n Real) (x! Real) (n! Real)) Bool + (and (and (>= x 1.0) (= x! (- x 1.0))) (= n! (* n 2.)))) +(define-fun post_fun ((x Real) (n Real)) Bool + (not (and (<= x 0.0) (and (not (= x 0.0)) (>= n 0.0))))) + + +(inv-constraint inv_fun pre_fun trans_fun post_fun) + +(check-synth) From 80687de36d9bc6074dc0ef7534b6e4fc103a7555 Mon Sep 17 00:00:00 2001 From: Julia Offerman <59590610+juliaofferman@users.noreply.github.com> Date: Thu, 21 Jan 2021 21:16:42 -0800 Subject: [PATCH 37/38] Add real benchmarks --- benchmarks/LRA/anfp_r.sl | 14 ++++++++++++++ benchmarks/LRA/array-new_r.sl | 14 ++++++++++++++ benchmarks/LRA/cegar1_r.sl | 14 ++++++++++++++ benchmarks/LRA/div_r.sl | 15 +++++++++++++++ benchmarks/LRA/ex11_r.sl | 14 ++++++++++++++ benchmarks/LRA/ex14_r.sl | 14 ++++++++++++++ benchmarks/LRA/ex1_r.sl | 14 ++++++++++++++ benchmarks/LRA/ex7_r.sl | 14 ++++++++++++++ benchmarks/LRA/fig1_r.sl | 15 +++++++++++++++ benchmarks/LRA/fig9_r.sl | 14 ++++++++++++++ benchmarks/LRA/mult2_r.sl | 14 ++++++++++++++ benchmarks/LRA/mult_r.sl | 15 +++++++++++++++ 12 files changed, 171 insertions(+) create mode 100644 benchmarks/LRA/anfp_r.sl create mode 100644 benchmarks/LRA/array-new_r.sl create mode 100644 benchmarks/LRA/cegar1_r.sl create mode 100644 benchmarks/LRA/div_r.sl create mode 100644 benchmarks/LRA/ex11_r.sl create mode 100644 benchmarks/LRA/ex14_r.sl create mode 100644 benchmarks/LRA/ex1_r.sl create mode 100644 benchmarks/LRA/ex7_r.sl create mode 100644 benchmarks/LRA/fig1_r.sl create mode 100644 benchmarks/LRA/fig9_r.sl create mode 100644 benchmarks/LRA/mult2_r.sl create mode 100644 benchmarks/LRA/mult_r.sl diff --git a/benchmarks/LRA/anfp_r.sl b/benchmarks/LRA/anfp_r.sl new file mode 100644 index 0000000..9ee3d2f --- /dev/null +++ b/benchmarks/LRA/anfp_r.sl @@ -0,0 +1,14 @@ +(set-logic LRA) + +(synth-inv inv_fun ((x Real) (y Real))) + +(define-fun pre_fun ((x Real) (y Real)) Bool + (and (= x 1.0) (= y 0.0))) +(define-fun trans_fun ((x Real) (y Real) (x! Real) (y! Real)) Bool + (and (and (< y 1000.0) (= x! (+ x y))) (= y! (+ y 1.0)))) +(define-fun post_fun ((x Int) (y Int)) Bool + (not (and (>= y 1000) (< x y)))) + +(inv-constraint inv_fun pre_fun trans_fun post_fun) + +(check-synth) \ No newline at end of file diff --git a/benchmarks/LRA/array-new_r.sl b/benchmarks/LRA/array-new_r.sl new file mode 100644 index 0000000..dfd3808 --- /dev/null +++ b/benchmarks/LRA/array-new_r.sl @@ -0,0 +1,14 @@ +(set-logic LRA) + +(synth-inv inv_fun ((x Real) (y Real) (z Real))) + +(define-fun pre_fun ((x Real) (y Real) (z Real)) Bool + (= x 0.)) +(define-fun trans_fun ((x Real) (y Real) (z Real) (x! Real) (y! Real) (z! Real)) Bool + (or (and (= x! (+ x 1.)) (and (= y! z!) (and (<= z! y) (< x 500.)))) (and (= x! (+ x 1.)) (and (= y! y) (and (> z! y) (< x 500.)))))) +(define-fun post_fun ((x Int) (y Int) (z Int)) Bool + (not (and (>= x 500.) (< z y)))) + +(inv-constraint inv_fun pre_fun trans_fun post_fun) + +(check-synth) \ No newline at end of file diff --git a/benchmarks/LRA/cegar1_r.sl b/benchmarks/LRA/cegar1_r.sl new file mode 100644 index 0000000..1fa14e3 --- /dev/null +++ b/benchmarks/LRA/cegar1_r.sl @@ -0,0 +1,14 @@ +(set-logic LRA) + +(synth-inv inv_fun ((x Real) (y Real))) + +(define-fun pre_fun ((x Real) (y Real)) Bool + (and (and (>= x 0.) (and (<= x 2.) (<= y 2.))) (>= y 0.))) +(define-fun trans_fun ((x Real) (y Real) (x! Real) (y! Real)) Bool + (and (= x! (+ x 2.)) (= y! (+ y 2.)))) +(define-fun post_fun ((x Real) (y Real)) Bool + (not (and (= x 4.) (= y 0.)))) + +(inv-constraint inv_fun pre_fun trans_fun post_fun) + +(check-synth) \ No newline at end of file diff --git a/benchmarks/LRA/div_r.sl b/benchmarks/LRA/div_r.sl new file mode 100644 index 0000000..22ba79d --- /dev/null +++ b/benchmarks/LRA/div_r.sl @@ -0,0 +1,15 @@ +(set-logic LRA) + +(synth-inv inv_fun ((x Real) (n Real))) + +(define-fun pre_fun ((x Real) (n Real)) Bool + (= x n)) +(define-fun trans_fun ((x Real) (n Real) (x! Real) (n! Real)) Bool + (and (and (>= x 1.) (= x! (/ x 2.))) (= n! n))) +(define-fun post_fun ((x Real) (n Real)) Bool + (not (and (<= x 0.) (and (not (= x 0.)) (>= n 0.))))) + + +(inv-constraint inv_fun pre_fun trans_fun post_fun) + +(check-synth) diff --git a/benchmarks/LRA/ex11_r.sl b/benchmarks/LRA/ex11_r.sl new file mode 100644 index 0000000..6abb5d1 --- /dev/null +++ b/benchmarks/LRA/ex11_r.sl @@ -0,0 +1,14 @@ +(set-logic LRA) + +(synth-inv inv_fun ((x Real) (y Real) (lock Real))) + +(define-fun pre_fun ((x Real) (y Real) (lock Real)) Bool + (or (and (= x y) (= lock 1.)) (and (= (+ x 1.) y) (= lock 0.)))) +(define-fun trans_fun ((x Real) (y Real) (lock Real) (x! Real) (y! Real) (lock! Real)) Bool + (or (and (and (not (= x y)) (= lock! 1.)) (= x! y)) (and (and (and (not (= x y)) (= lock! 0)) (= x! y)) (= y! (+ y 1.))))) +(define-fun post_fun ((x Real) (y Real) (lock Real)) Bool + (not (and (= x y) (not (= lock 1.))))) + +(inv-constraint inv_fun pre_fun trans_fun post_fun) + +(check-synth) \ No newline at end of file diff --git a/benchmarks/LRA/ex14_r.sl b/benchmarks/LRA/ex14_r.sl new file mode 100644 index 0000000..d8a9bb9 --- /dev/null +++ b/benchmarks/LRA/ex14_r.sl @@ -0,0 +1,14 @@ +(set-logic LRA) + +(synth-inv inv_fun ((x Real) (y Real))) + +(define-fun pre_fun ((x Real) (y Real)) Bool + (= x 1)) +(define-fun trans_fun ((x Real) (y Real) (x! Real) (y! Real)) Bool + (and (and (<= x 10.) (= y! (- 10. x))) (= x! (+ x 1.)))) +(define-fun post_fun ((x Real) (y Real)) Bool + (not (and (and (<= x 10.) (= y (- 10. x))) (or (>= y 10.) (> 0. y))))) + +(inv-constraint inv_fun pre_fun trans_fun post_fun) + +(check-synth) \ No newline at end of file diff --git a/benchmarks/LRA/ex1_r.sl b/benchmarks/LRA/ex1_r.sl new file mode 100644 index 0000000..02de84b --- /dev/null +++ b/benchmarks/LRA/ex1_r.sl @@ -0,0 +1,14 @@ +(set-logic LRA) + +(synth-inv inv_fun ((x Real) (y Real) (xa Real) (ya Real))) + +(define-fun pre_fun ((x Real) (y Real) (xa Real) (ya Real)) Bool + (and (= xa 0.) (= ya 0.))) +(define-fun trans_fun ((x Real) (y Real) (xa Real) (ya Real) (x! Real) (y! Real) (xa! Real) (ya! Real)) Bool + (and (= x! (+ 1. (+ xa (* 2. ya)))) (or (= y! (+ (- ya (* 2. xa)) x!)) (= y! (- (- ya (* 2. xa)) x!))) (= xa! (- x! (* 2. y!))) (= ya! (+ (* 2. x!) y!)))) +(define-fun post_fun ((x Real) (y Real) (xa Real) (ya Real)) Bool + (>= (+ xa (* 2. ya)) 0.)) + +(inv-constraint inv_fun pre_fun trans_fun post_fun) + +(check-synth) \ No newline at end of file diff --git a/benchmarks/LRA/ex7_r.sl b/benchmarks/LRA/ex7_r.sl new file mode 100644 index 0000000..285efae --- /dev/null +++ b/benchmarks/LRA/ex7_r.sl @@ -0,0 +1,14 @@ +(set-logic LRA) + +(synth-inv inv_fun ((x Real) (y Real) (i Real))) + +(define-fun pre_fun ((x Real) (y Real) (i Real)) Bool + (and (and (and (= i 0.) (>= x 0.)) (>= y 0.)) (>= x y))) +(define-fun trans_fun ((x Real) (y Real) (i Real) (x! Real) (y! Real) (i! Real)) Bool + (and (and (< i y) (= i! (+ i 1.))) (and (= y! y) (= x! x)))) +(define-fun post_fun ((x Real) (y Real) (i Real)) Bool + (not (and (< i y) (or (>= i x) (> 0. i))))) + +(inv-constraint inv_fun pre_fun trans_fun post_fun) + +(check-synth) \ No newline at end of file diff --git a/benchmarks/LRA/fig1_r.sl b/benchmarks/LRA/fig1_r.sl new file mode 100644 index 0000000..468a6ed --- /dev/null +++ b/benchmarks/LRA/fig1_r.sl @@ -0,0 +1,15 @@ + +(set-logic LRA) + +(synth-inv inv_fun ((x Real) (y Real))) + +(define-fun pre_fun ((x Real) (y Real)) Bool + (= x (- 50.))) +(define-fun trans_fun ((x Real) (y Real) (x! Real) (y! Real)) Bool + (and (and (< x 0.) (= x! (+ x y))) (= y! (+ y 1.)))) +(define-fun post_fun ((x Int) (y Int)) Bool + (not (and (>= x 0.) (<= y 0.)))) + +(inv-constraint inv_fun pre_fun trans_fun post_fun) + +(check-synth) \ No newline at end of file diff --git a/benchmarks/LRA/fig9_r.sl b/benchmarks/LRA/fig9_r.sl new file mode 100644 index 0000000..ac134e0 --- /dev/null +++ b/benchmarks/LRA/fig9_r.sl @@ -0,0 +1,14 @@ +(set-logic LRA) + +(synth-inv inv_fun ((x Real) (y Real))) + +(define-fun pre_fun ((x Real) (y Real)) Bool + (and (= x 0.) (= y 0.))) +(define-fun trans_fun ((x Real) (y Real) (x! Real) (y! Real)) Bool + (and (= x! x) (and (<= 0. y) (= y! (+ x y))))) +(define-fun post_fun ((x Real) (y Real)) Bool + (>= y 0.)) + +(inv-constraint inv_fun pre_fun trans_fun post_fun) + +(check-synth) \ No newline at end of file diff --git a/benchmarks/LRA/mult2_r.sl b/benchmarks/LRA/mult2_r.sl new file mode 100644 index 0000000..8957e6f --- /dev/null +++ b/benchmarks/LRA/mult2_r.sl @@ -0,0 +1,14 @@ +(set-logic LRA) + +(synth-inv inv_fun ((x Real) (y Real))) + +(define-fun pre_fun ((x Real) (y Real)) Bool + (and (= x 0.) (= y 0.))) +(define-fun trans_fun ((x Real) (y Real) (x! Real) (y! Real)) Bool + (and (= x! x) (and (<= 0. y) (= y! (* 4. y))))) +(define-fun post_fun ((x Real) (y Real)) Bool + (= y 0.)) + +(inv-constraint inv_fun pre_fun trans_fun post_fun) + +(check-synth) \ No newline at end of file diff --git a/benchmarks/LRA/mult_r.sl b/benchmarks/LRA/mult_r.sl new file mode 100644 index 0000000..0dbcde6 --- /dev/null +++ b/benchmarks/LRA/mult_r.sl @@ -0,0 +1,15 @@ +(set-logic LRA) + +(synth-inv inv_fun ((x Real) (n Real))) + +(define-fun pre_fun ((x Real) (n Real)) Bool + (= x (* 2. n))) +(define-fun trans_fun ((x Real) (n Real) (x! Real) (n! Real)) Bool + (and (and (>= x 1.0) (= x! (/ x 2.))) (= n! (/ n 2.)))) +(define-fun post_fun ((x Real) (n Real)) Bool + (and (not (and (<= x 1.) (and (not (= x 1.)) (>= n 0.5)))) (= x (* 2. n)))) + + +(inv-constraint inv_fun pre_fun trans_fun post_fun) + +(check-synth) \ No newline at end of file From b0f5170b23e04070d6a3ab547a9b28f991a8b80b Mon Sep 17 00:00:00 2001 From: Julia Offerman Date: Fri, 22 Jan 2021 15:29:40 -0800 Subject: [PATCH 38/38] Removie real ite component Removie Real ite component and unnecessary of_string function --- src/RealComponents.ml | 14 +------------- src/Value.ml | 14 -------------- test/Test_RealComponents.ml | 18 ------------------ 3 files changed, 1 insertion(+), 45 deletions(-) diff --git a/src/RealComponents.ml b/src/RealComponents.ml index 4617f6e..5c51c02 100644 --- a/src/RealComponents.ml +++ b/src/RealComponents.ml @@ -143,19 +143,7 @@ let conditionals = [ evaluate = Value.(fun [@warning "-8"] [v1 ; v2] -> Bool Float.((value_of v1) <= (value_of v2))); to_string = (fun [@warning "-8"] [a ; b] -> "(<= " ^ a ^ " " ^ b ^ ")"); global_constraints = (fun _ -> []) - } ; - { - name = "real-ite"; - codomain = Type.REAL; - domain = Type.[BOOL; REAL; REAL]; - is_argument_valid = (function - | [x ; y ; z] -> (not (is_constant x)) && (y =/= z) - | _ -> false); - evaluate = Value.(fun [@warning "-8"] [Bool x ; v1 ; v2] - -> Real (if x then (value_of v1) else (value_of v2))); - to_string = (fun [@warning "-8"] [a ; b ; c] -> "IF(" ^ a ^ "," ^ b ^ "," ^ c ^ ")"); - global_constraints = (fun _ -> []) - } + } ] diff --git a/src/Value.ml b/src/Value.ml index c133d9d..6c24740 100644 --- a/src/Value.ml +++ b/src/Value.ml @@ -1,10 +1,7 @@ open Base - open Exceptions - - module T = struct type t = Int of int | Bool of bool @@ -20,7 +17,6 @@ end include T include Comparable.Make (T) - let rec typeof : t -> Type.t = function | Int _ -> Type.INT | Bool _ -> Type.BOOL @@ -58,14 +54,6 @@ let of_atomic_string (s : string) : t = with Invalid_argument _ -> raise (Parse_Exn ("Failed to parse value `" ^ s ^ "`.")) - - let value_of_real_atomic_string (s : string) : float = - try - (Float.of_string s) - with Invalid_argument _ -> - raise (Parse_Exn ("Failed to parse value `" ^ s ^ "`.")) - - (* We assume that an array serialization provides explicit (k,v) pairs -- * either using nested `store` calls, or if-then-else constructs. * The different array formats are described in more details here: @@ -113,7 +101,5 @@ and of_sexp (sexp : Sexp.t) : t = | _ -> raise (Internal_Exn ("Unable to deserialize value: " ^ (to_string_hum sexp))) - - let of_string (s : string) : t = (of_sexp (Core.Sexp.of_string s)) diff --git a/test/Test_RealComponents.ml b/test/Test_RealComponents.ml index c3f4dd3..16f19bd 100644 --- a/test/Test_RealComponents.ml +++ b/test/Test_RealComponents.ml @@ -22,8 +22,6 @@ let geq_eval = (List.find_exn RealComponents.conditionals ~f:(fun comp -> String.equal comp.name "real-geq")).evaluate let leq_eval = (List.find_exn RealComponents.conditionals ~f:(fun comp -> String.equal comp.name "real-leq")).evaluate -let ite_eval = (List.find_exn RealComponents.conditionals - ~f:(fun comp -> String.equal comp.name "real-ite")).evaluate let add () = let rl = [Value.Real 3.54 ; Value.Real 7.52] in @@ -146,20 +144,6 @@ let leq_not () = let res = Value.equal leq_ret (Value.Bool false) in Alcotest.(check bool) "identical" true res -let ite () = - let rl = [Value.Bool false ; Value.Real 3.54 ; Value.Real 7.52] in - let ite_ret = ite_eval rl in - let res = Value.equal ite_ret (Value.Real 7.52) - in Alcotest.(check bool) "identical" true res - -let ite_true () = - let rl = [Value.Bool true ; Value.Real 3.54 ; Value.Real 7.52] in - let ite_ret = ite_eval rl in - let res = Value.equal ite_ret (Value.Real 3.54) - in Alcotest.(check bool) "identical" true res - - - let all = [ "add", `Quick, add ; @@ -182,7 +166,5 @@ let all = [ "leq", `Quick, leq ; "leq_eq", `Quick, leq_eq ; "leq_not", `Quick, leq_not ; - "ite", `Quick, ite ; - "ite_true", `Quick, ite_true ; ]