Added real type

app/App.ml

@@ -72,4 +72,4 @@ let no_synth_PI () =
 
 
 let () = with_synth_PI ()
-       ; no_synth_PI ()
+       ; no_synth_PI ()

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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 |]
+let levels = [| all_qf ; all ; all_transformed_int_unary ; all_transformed_int_binary |]

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
+let of_string name = String.Table.find_exn all_supported name