add examples

Makefile

@@ -36,7 +36,7 @@ doc:
 	cp -r _build/default/_doc/_html/* docs/
 
 build:
-	dune build absolute-solver/absolute.exe
+	dune build .
 
 test:
 	dune runtest -f

examples/dune

@@ -1,3 +1,3 @@
 (executables
- (names polynomial convex tree)
+ (names polynomial polygons sortedlist convex tree)
  (libraries libabsolute))

examples/polygons.ml

@@ -0,0 +1,75 @@
+(** this example defines the csp for convex polygons of size n and output a
+    graphviz file.
+
+    It is possible to view it by doing:
+
+    n=15; dune exec ./polygons.exe $n; neato -Goverlap=false -Tpng convex$n.viz
+    > convex$n.png; open convex$n.png
+
+    NB: neato produces a friendlier output than dot *)
+
+open Libabsolute
+
+(* vector from (x1,y1) yo (x2,y2) *)
+let vector (x1, y1) (x2, y2) =
+  let open Expr.Operators in
+  (x2 - x1, y2 - y1)
+
+(* cross product of two vectors *)
+let cross_product (x1, y1) (x2, y2) =
+  let open Expr.Operators in
+  (x1 * y2) - (y1 * x2)
+
+(* Function that builds the list of constraints corresponding to the check that
+   a list of points forms a convex polygon. This is done by verifying that the
+   vectors corresponding to two consecutive edges of the polygons have a
+   negative cross-product (We could have also picked positive, but we enforce
+   less representations for the same polyhedron that way). *)
+let is_convex points =
+  let rec check_convexity = function
+    | p1 :: p2 :: p3 :: rest ->
+        let v1 = vector p1 p2 in
+        let v2 = vector p2 p3 in
+        let open Constraint.Operators in
+        (cross_product v1 v2 < Expr.zero) :: check_convexity (p2 :: p3 :: rest)
+    | _ -> []
+  in
+  match points with
+  | [] | [_] | [_; _] ->
+      failwith "Invalid input: At least 3 points are required."
+  | h1 :: h2 :: _ -> check_convexity (points @ [h1; h2])
+
+(* build two variables xn, yn per points of the polygon *)
+let build_vars n =
+  let rec loop acc = function
+    | 0 -> List.rev acc
+    | n ->
+        let idx = string_of_int n in
+        loop (("x" ^ idx, "y" ^ idx) :: acc) (n - 1)
+  in
+  loop [] n
+
+let build_csp n =
+  let names = build_vars n in
+  let csp =
+    List.fold_left
+      (fun csp (v1, v2) ->
+        csp |> Csp.add_real_var_f v1 0. 100. |> Csp.add_real_var_f v2 0. 100. )
+      Csp.empty names
+  in
+  let var_exprs = List.map (fun (v1, v2) -> (Expr.var v1, Expr.var v2)) names in
+  let constrs = is_convex var_exprs in
+  List.fold_left Csp.add_constr csp constrs
+
+let () =
+  if Array.length Sys.argv < 2 then (
+    Format.printf "bad usage: expect a number of points\n" ;
+    exit 1 ) ;
+  match int_of_string_opt Sys.argv.(1) with
+  | Some nb_points ->
+      let csp = build_csp nb_points in
+      Format.printf "%a\n" Csp.print csp ;
+      Csp.to_graphviz csp (Format.sprintf "convex%i.viz" nb_points)
+  | None ->
+      Format.printf "expecting numeric argument %s\n" Sys.argv.(1) ;
+      exit 1

examples/sortedlist.ml

@@ -0,0 +1,61 @@
+(** this example defines the csp for sorted list of size n and output a graphviz
+    file.
+
+    It is possible to view it by doing:
+
+    n=15; dune exec ./sortedlist.exe $n; neato -Goverlap=false -Tpng
+    sortedlist$n.viz > sortedlist$n.png; open sortedlist$n.png
+
+    NB: neato produces a friendlier output than dot *)
+
+open Libabsolute
+
+(* Function that builds the list of constraints corresponding to the check that
+   a list of points forms a convex polygon. This is done by verifying that the
+   vectors corresponding to two consecutive edges of the polygons have a
+   negative cross-product (We could have also picked positive, but we enforce
+   less representations for the same polyhedron that way). *)
+let sorted l =
+  let rec loop = function
+    | x1 :: x2 :: rest ->
+        let open Constraint.Operators in
+        (x1 <= x2) :: loop (x2 :: rest)
+    | _ -> []
+  in
+  match l with
+  | [] | [_] -> failwith "Invalid input: At least 2 numbers are required."
+  | _ -> loop l
+
+(* build two variables xn, yn per points of the polygon *)
+let build_vars n =
+  let rec loop acc = function
+    | 0 -> List.rev acc
+    | n ->
+        let idx = string_of_int n in
+        loop (("x" ^ idx) :: acc) (n - 1)
+  in
+  loop [] n
+
+let build_csp n =
+  let names = build_vars n in
+  let csp =
+    List.fold_left
+      (fun csp v -> csp |> Csp.add_real_var_f v 0. 1000.)
+      Csp.empty names
+  in
+  let var_exprs = List.map Expr.var names in
+  let constrs = sorted var_exprs in
+  List.fold_left Csp.add_constr csp constrs
+
+let () =
+  if Array.length Sys.argv < 2 then (
+    Format.printf "bad usage: expect a number of points\n" ;
+    exit 1 ) ;
+  match int_of_string_opt Sys.argv.(1) with
+  | Some nb_points ->
+      let csp = build_csp nb_points in
+      Format.printf "%a\n" Csp.print csp ;
+      Csp.to_graphviz csp (Format.sprintf "sortedlist%i.viz" nb_points)
+  | None ->
+      Format.printf "expecting numeric argument %s\n" Sys.argv.(1) ;
+      exit 1

examples/tree.ml

@@ -15,12 +15,11 @@ let pp_constr fmt = List.iter (print_intern fmt)
 let () =
   let open Csp in
   let prob =
-    empty
-    |> add_real_var_f "x" (-1000.) 1000.
-    |> add_real_var_f "t" 0. 1000.
-    |> add_constr
-         (Parser.constr
-            {|(x in [0;10] && t in [0;1]) || (x in [5;15] && t in [1;2])|})
+    let csp = add_real_var_f "x" (-1000.) 1000. empty in
+    let csp = add_real_var_f "t" 0. 1000. csp in
+    add_constr csp
+      (Parser.constr
+         {|(x in [0;10] && t in [0;1]) || (x in [5;15] && t in [1;2])|} )
   in
   let s, c = init prob in
   Format.printf "%a, %a\n" D.print s pp_constr c ;
@@ -33,7 +32,8 @@ let () =
         | Unsat -> Format.printf "%a unsatisfiable\n" print_intern h
         | Filtered ((s', c'), _) ->
             Format.printf "new abstract value:\n %a\n" D.print s' ;
-            Format.printf "new constraint:\n%a\n" print_intern c' ) ;
+            Format.printf "new constraint:\n%a\n" print_intern c'
+        | Pruned _ -> Format.printf "pruned\n" ) ;
         aux t
   in
   aux c