README_old.md

INSTALLATION

Supposing you already have installed opam 2.0:

• opam pin add -n why3 "https://gitlab.inria.fr/why3/why3.git#e58d9baf8afbb"
• opam pin add -n why3-ide "https://gitlab.inria.fr/why3/why3.git#e58d9baf8afbb5"
• opam pin add -n cp cp_why3.tar.gz
• opam install why3 why3-ide cp

Play with it inside toplevel

For that we need a nice toplevel: utop

• opam install utop
• utop

Inside the toplevel you can run the commands (written after the utop #)

utop # #require "cp";;

utop # let c = Cp.Context.create ();;
val c : Cp.Context.t = <abstr>

utop # let v1 = Cp.Var.I.mk c ~min:(Z.of_int 10) ~max:(Z.of_int 20);;
val v1 : Cp.Var.I.t = <abstr>

utop # let v2 = Cp.Var.I.mk c ~min:(Z.of_int 10) ~max:(Z.of_int 20);;
val v2 : Cp.Var.I.t = <abstr>

utop # let v3 = Cp.Var.I.mk c ~min:(Z.of_int 10) ~max:(Z.of_int 20);;
val v3 : Cp.Var.I.t = <abstr>

utop # Cp.Constraint.add c v1 v2 v3;;
- : unit = ()

utop # let m = Cp.Context.solve c;;
val m : Cp.Model.t = <abstr>

utop # #install_printer Z.pp_print;;

utop # Cp.Var.I.get m v1;;
- : Z.t = 10

utop # Cp.Var.I.get m v2;;
- : Z.t = 10

utop # Cp.Var.I.get m v3;;
- : Z.t = 20

utop # Cp.Constraint.add c v3 v2 v1;;
- : unit = ()

utop # let m = Cp.Context.solve c;;
Exception: Cp__Cp__Type.Unsat.

As a program

Same example:

let c = Cp.Context.create ()
let v1 = Cp.Var.I.mk c ~min:(Z.of_int 10) ~max:(Z.of_int 20)
let v2 = Cp.Var.I.mk c ~min:(Z.of_int 10) ~max:(Z.of_int 20)
let v3 = Cp.Var.I.mk c ~min:(Z.of_int 10) ~max:(Z.of_int 20)

let () = Cp.Constraint.add c v1 v2 v3

let m = Cp.Context.solve c

let print = Format.printf "%a@." Z.pp_print

let () =
  print (Cp.Var.I.get m Cp.Var.I.zero);
  print (Cp.Var.I.get m v1);
  print (Cp.Var.I.get m v2);
  print (Cp.Var.I.get m v3)

let () =
  try
    Cp.Constraint.add c v3 v2 v1;
    ignore (Cp.Context.solve c)
  with Cp.Unsat -> Format.printf "Unsat@."

Development

• make for the compilation
• dune utop . for a toplevel with the library
• make ide for starting why3 ide with all the VCs
• make replay for checking all the proofs (long to load)