From 75069e69d8802c65eaa5724e6e58b6737bf35550 Mon Sep 17 00:00:00 2001
From: joaomhmpereira <joaompereira07@gmail.com>
Date: Sat, 6 Apr 2024 00:22:43 +0100
Subject: [PATCH] update README and add examples

---
 README.md                 | 48 +++++++++++++++++++++++++++++++++++++--
 cvc5.ml                   |  2 ++
 cvc5.mli                  |  2 ++
 cvc5_external.ml          |  4 ++++
 cvc5_stubs.cpp            |  7 ++++++
 dune                      |  5 ----
 examples/dune             |  4 ++++
 toy.ml => examples/toy.ml | 14 +++++-------
 8 files changed, 71 insertions(+), 15 deletions(-)
 create mode 100644 examples/dune
 rename toy.ml => examples/toy.ml (55%)

diff --git a/README.md b/README.md
index 870052a..823fab2 100644
--- a/README.md
+++ b/README.md
@@ -1,3 +1,47 @@
-# ocaml_cvc5 #
+[![Build badge](https://github.com/formalsec/ocaml-cvc5/actions/workflows/build.yml/badge.svg)](https://github.com/formalsec/ocaml-cvc5/actions) ![Platform](https://img.shields.io/badge/platform-linux%20%7C%20macos-lightgrey)
 
-OCaml bindings for the cvc5 SMT solver
+ocaml-cvc5 
+===============================================================================
+
+OCaml bindings for the [cvc5] Satisfiability Modulo Theories (SMT) solver
+
+## Installation
+
+### Build from source
+
+---
+- Clone the complete source tree:
+
+```sh
+git clone --recurse-submodules https://github.com/formalsec/ocaml-cvc5
+```
+
+- Install the library dependencies:
+
+```sh
+cd ocaml-cvc5
+opam install . --deps-only
+```
+
+- Build and test:
+
+```sh
+dune build
+dune runtest
+```
+
+- Install cvc5's OCaml bindings on your path by running:
+
+```sh
+dune install
+```
+
+## Examples
+
+Run examples with:
+
+```sh
+dune exec -- examples/toy.exe  #replace toy with any other example
+```
+
+[cvc5]: https://github.com/cvc5/cvc5
\ No newline at end of file
diff --git a/cvc5.ml b/cvc5.ml
index 89f2289..b93ed46 100644
--- a/cvc5.ml
+++ b/cvc5.ml
@@ -82,6 +82,8 @@ module Solver = struct
 
   let set_logic = Cvc5_external.set_logic
 
+  let set_option = Cvc5_external.set_option
+
   let simplify = Cvc5_external.simplify
 
   let push = Cvc5_external.push
diff --git a/cvc5.mli b/cvc5.mli
index 590c5c6..bab3927 100644
--- a/cvc5.mli
+++ b/cvc5.mli
@@ -78,6 +78,8 @@ module Solver : sig
 
   val set_logic : solver -> string -> unit
 
+  val set_option : solver -> string -> string -> unit
+
   val simplify : solver -> Term.term -> Term.term
 
   val push : solver -> int -> unit
diff --git a/cvc5_external.ml b/cvc5_external.ml
index ed03944..961201a 100644
--- a/cvc5_external.ml
+++ b/cvc5_external.ml
@@ -138,6 +138,10 @@ external check_sat : solver -> result = "ocaml_cvc5_stub_check_sat"
 external set_logic : solver -> string -> unit = "ocaml_cvc5_stub_set_logic"
 [@@noalloc]
 
+external set_option : solver -> string -> string -> unit
+  = "ocaml_cvc5_stub_set_option"
+[@@noalloc]
+
 external simplify : solver -> term -> term = "ocaml_cvc5_stub_simplify"
 
 external push : solver -> int -> unit = "ocaml_cvc5_stub_push" [@@noalloc]
diff --git a/cvc5_stubs.cpp b/cvc5_stubs.cpp
index b0281c3..ddca4fd 100644
--- a/cvc5_stubs.cpp
+++ b/cvc5_stubs.cpp
@@ -451,6 +451,13 @@ CAMLprim value ocaml_cvc5_stub_set_logic(value v, value s){
   CVC5_TRY_CATCH_END;
 }
 
+CAMLprim value ocaml_cvc5_stub_set_option(value s, value opt, value v){
+  CVC5_TRY_CATCH_BEGIN;
+  Solver_val(s)->setOption(String_val(opt), String_val(v));
+  return Val_unit;
+  CVC5_TRY_CATCH_END;
+}
+
 CAMLprim value ocaml_cvc5_stub_simplify(value v, value t){
   value custom = Val_unit;
   CVC5_TRY_CATCH_BEGIN;
diff --git a/dune b/dune
index 8156784..b76a006 100644
--- a/dune
+++ b/dune
@@ -40,8 +40,3 @@
   (with-stdout-to
    %{target}
    (run %{deps}))))
-
-(executable
- (name toy)
- (libraries cvc5)
- (modules toy))
diff --git a/examples/dune b/examples/dune
new file mode 100644
index 0000000..684fd4d
--- /dev/null
+++ b/examples/dune
@@ -0,0 +1,4 @@
+(executable
+ (name toy)
+ (libraries cvc5)
+ (modules toy))
diff --git a/toy.ml b/examples/toy.ml
similarity index 55%
rename from toy.ml
rename to examples/toy.ml
index 1611194..3d2fd12 100644
--- a/toy.ml
+++ b/examples/toy.ml
@@ -11,18 +11,16 @@ let x = Term.mk_const_s tm int_sort "x"
 let zero = Term.mk_int tm 0
 
 let () =
-  let x_gt_zero = Term.mk_term tm Kind.Gt [| x; zero |] in
-  print_endline (Term.to_string x_gt_zero);
-  let x_lt_zero = Term.mk_term tm Kind.Lt [| zero; x |] in
-  print_endline (Term.to_string x_lt_zero);
   (* x > 0 *)
+  let x_gt_zero = Term.mk_term tm Kind.Geq [| x; zero |] in
+  Printf.printf "term 1: %s\n" (Term.to_string x_gt_zero);
+  (* x <= 0 *)
+  let x_lt_zero = Term.mk_term tm Kind.Leq [| x; zero |] in
+  Printf.printf "term 2: %s\n" (Term.to_string x_lt_zero);
   Solver.assert_formula solver x_gt_zero;
-  (* x < 0 *)
   Solver.assert_formula solver x_lt_zero;
   let r = Solver.check_sat solver in
   let b = Result.is_sat r in
   Solver.delete_solver solver;
   TermManager.delete_tm tm;
-  match b with
-  | true -> print_endline "sat OCaml"
-  | false -> print_endline "unsat OCaml"
+  match b with true -> print_endline "sat" | false -> print_endline "unsat"