update README and add examples

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

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

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

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]

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;

dune

@@ -40,8 +40,3 @@
   (with-stdout-to
    %{target}
    (run %{deps}))))
-
-(executable
- (name toy)
- (libraries cvc5)
- (modules toy))

examples/dune

@@ -0,0 +1,4 @@
+(executable
+ (name toy)
+ (libraries cvc5)
+ (modules toy))

toy.ml → 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"