diff --git a/app/App.ml b/app/App.ml index f1bf999..6b5fdac 100644 --- a/app/App.ml +++ b/app/App.ml @@ -72,4 +72,4 @@ let no_synth_PI () = let () = with_synth_PI () - ; no_synth_PI () \ No newline at end of file + ; no_synth_PI () 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/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) 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 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 |] diff --git a/src/Logic.ml b/src/Logic.ml index 5fb9d38..d296b20 100644 --- a/src/Logic.ml +++ b/src/Logic.ml @@ -41,9 +41,13 @@ 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 + }; { + name = "LRA" ; + components_per_level = RealComponents.levels ++ BooleanComponents.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 diff --git a/src/RealComponents.ml b/src/RealComponents.ml new file mode 100644 index 0000000..5c51c02 --- /dev/null +++ b/src/RealComponents.ml @@ -0,0 +1,154 @@ +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]; + 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); + 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 _ -> []) + } ; + { + name = "real-sub"; + codomain = Type.REAL; + domain = Type.[REAL; REAL]; + is_argument_valid = Value.(function + | [(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 ^ ")"); + global_constraints = (fun _ -> []) + } +] + +let scaling = [ + { + name = "real-mult"; + codomain = Type.REAL; + domain = Type.[REAL; REAL]; + is_argument_valid = Value.(function + | [x ; y] + -> (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 ^ ")"); + global_constraints = (fun _ -> []) + } ; + { + name = "real-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.))) + | _ -> 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 ^ "))"]); + } +] + +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"; + codomain = Type.BOOL; + domain = Type.[REAL; REAL]; + 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.(equal (value_of v1) (value_of v2))); + to_string = (fun [@warning "-8"] [a ; b] -> "(= " ^ a ^ " " ^ b ^ ")"); + global_constraints = (fun _ -> []) + } ; + { + name = "real-geq"; + codomain = Type.BOOL; + domain = Type.[REAL; REAL]; + 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.((value_of v1) >= (value_of v2))); + to_string = (fun [@warning "-8"] [a ; b] -> "(>= " ^ a ^ " " ^ b ^ ")"); + global_constraints = (fun _ -> []) + } ; + { + name = "real-leq"; + codomain = Type.BOOL; + domain = Type.[REAL; REAL]; + 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.((value_of v1) <= (value_of v2))); + to_string = (fun [@warning "-8"] [a ; b] -> "(<= " ^ a ^ " " ^ b ^ ")"); + global_constraints = (fun _ -> []) + } + +] + + + +let levels = [| translation ; conditionals ; linear |] + +let no_bool_levels = [| translation ; scaling |] diff --git a/src/Synthesizer.ml b/src/Synthesizer.ml index b9df624..a9a8637 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 @@ -207,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 = @@ -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 + } diff --git a/src/TestGen.ml b/src/TestGen.ml index 4da3bcd..4c30138 100644 --- a/src/TestGen.ml +++ b/src/TestGen.ml @@ -6,14 +6,19 @@ 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) >>= 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 _ | Type.TVAR _ - -> raise (Exceptions.Internal_Exn "Generator not implemented!") \ No newline at end of file + | Type.LIST (t) + -> (Int.gen_incl 0 14) + >>= 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!") diff --git a/src/Type.ml b/src/Type.ml index 766221a..8ddd320 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 diff --git a/src/Value.ml b/src/Value.ml index 8035d7b..6c24740 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.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) ^ ")" @@ -46,6 +49,8 @@ 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 ^ "`.")) @@ -82,6 +87,11 @@ and of_sexp (sexp : Sexp.t) : t = 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)) @@ -92,4 +102,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)) 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 + ]) diff --git a/test/Test_RealComponents.ml b/test/Test_RealComponents.ml new file mode 100644 index 0000000..16f19bd --- /dev/null +++ b/test/Test_RealComponents.ml @@ -0,0 +1,170 @@ +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 + ~f:(fun comp -> String.equal comp.name "real-sub")).evaluate + +let mult_eval = (List.find_exn RealComponents.scaling + ~f:(fun comp -> String.equal comp.name "real-mult")).evaluate +let div_eval = (List.find_exn RealComponents.scaling + ~f:(fun comp -> String.equal comp.name "real-div")).evaluate + +let eq_eval = (List.find_exn RealComponents.conditionals + ~f:(fun comp -> String.equal comp.name "real-eq")).evaluate +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 add () = + let rl = [Value.Real 3.54 ; Value.Real 7.52] in + let add_ret = add_eval rl in + 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 + 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_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 all = [ + "add", `Quick, add ; + "add_zero", `Quick, add_zero ; + "add_neg", `Quick, add_neg ; + "sub", `Quick, sub ; + "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 ; + +] 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 ; +]