[Draft] CI and Public library

.github/workflows/build.yml

@@ -0,0 +1,35 @@
+name: Build
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - main
+
+jobs:
+  build:
+    strategy:
+      fail-fast: false
+      matrix:
+        os:
+          - self-hosted
+        ocaml-compiler:
+          - "4.14"
+    runs-on: ${{ matrix.os }}
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          submodules: true
+      - name: Setup OCaml ${{ matrix.ocaml-compiler }}
+        uses: ocaml/setup-ocaml@v2
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-compiler }}
+      - name: Install dependencies
+        run: opam install -y . --deps-only --with-test
+      - name: Build
+        run: opam exec -- dune build @install
+      - name: Test
+        run: opam exec -- dune runtest

.ocamlformat

@@ -0,0 +1,43 @@
+version=0.26.1
+assignment-operator=end-line
+break-cases=fit
+break-fun-decl=wrap
+break-fun-sig=wrap
+break-infix=wrap
+break-infix-before-func=false
+break-separators=before
+break-sequences=true
+cases-exp-indent=2
+cases-matching-exp-indent=normal
+doc-comments=before
+doc-comments-padding=2
+doc-comments-tag-only=default
+dock-collection-brackets=false
+exp-grouping=preserve
+field-space=loose
+if-then-else=compact
+indicate-multiline-delimiters=space
+indicate-nested-or-patterns=unsafe-no
+infix-precedence=indent
+leading-nested-match-parens=false
+let-and=sparse
+let-binding-spacing=compact
+let-module=compact
+margin=80
+max-indent=2
+module-item-spacing=sparse
+ocaml-version=4.14.0
+ocp-indent-compat=false
+parens-ite=false
+parens-tuple=always
+parse-docstrings=true
+sequence-blank-line=preserve-one
+sequence-style=terminator
+single-case=compact
+space-around-arrays=true
+space-around-lists=true
+space-around-records=true
+space-around-variants=true
+type-decl=sparse
+wrap-comments=false
+wrap-fun-args=true

api/build_enums.ml

@@ -1 +1 @@
-external build_enums : unit -> unit = "build_enums"
+external build_enums : unit -> unit = "build_enums"

api/cvc5_enums.ml

@@ -1,4 +1,3 @@
 open Build_enums
 
-let () =
-  build_enums ()
+let () = build_enums ()

api/dune

@@ -6,15 +6,12 @@
 (library
  (name build_enums)
  (modules build_enums)
+ (no_dynlink)
  (foreign_stubs
   (language cxx)
   (names build_enums)
+  (extra_deps ../cvc5_export.h)
   (flags :standard -std=c++17 -I/opt/homebrew/include)
-  (include_dirs 
-   ../vendor/cvc5/include))
- (foreign_archives
-  ../vendor/cvc5
-  ../vendor/cadical
-  ../vendor/picpoly
-  ../vendor/picpolyxx)
- (c_library_flags :standard -std=c++17 -L/opt/homebrew/lib -lgmp))
+  (include_dirs ../vendor/cvc5/include))
+ (foreign_archives ../cvc5 ../cadical ../picpoly ../picpolyxx)
+ (c_library_flags :standard -std=c++17 -L/opt/homebrew/lib -lgmp))

cvc5.ml

@@ -5,67 +5,88 @@ let _ = Callback.register_exception "cvc5Exception" (Error "")
 module Kind = Cvc5_enums.Kind
 module RoundingMode = Cvc5_enums.RoundingMode
 
-module TermManager =
-struct
+module TermManager = struct
   type tm = Cvc5_external.term_manager
 
   let mk_tm = Cvc5_external.new_term_manager
+
   let delete_tm = Cvc5_external.delete_term_manager
 end
 
-module Sort =
-struct
+module Sort = struct
   type sort = Cvc5_external.sort
 
   let mk_bool_sort = Cvc5_external.get_boolean_sort
+
   let mk_int_sort = Cvc5_external.get_integer_sort
-  let mk_real_sort = Cvc5_external.get_real_sort 
-  let mk_string_sort = Cvc5_external.get_string_sort 
+
+  let mk_real_sort = Cvc5_external.get_real_sort
+
+  let mk_string_sort = Cvc5_external.get_string_sort
+
   let mk_bv_sort = Cvc5_external.mk_bitvector_sort
 end
 
-module Term =
-struct
+module Term = struct
   type term = Cvc5_external.term
 
   let id = Cvc5_external.term_id
+
   let equal = Cvc5_external.term_equal
+
   let kind t = Kind.of_cpp @@ Cvc5_external.term_kind t
+
   let sort = Cvc5_external.term_sort
+
   let to_string = Cvc5_external.term_to_string
+
   let mk_const = Cvc5_external.mk_const
+
   let mk_const_s = Cvc5_external.mk_const_s
+
   let mk_term (tm : TermManager.tm) (k : Kind.t) (terms : term array) =
     Cvc5_external.mk_term tm (Kind.to_cpp k) terms
+
   let mk_true = Cvc5_external.mk_true
+
   let mk_false = Cvc5_external.mk_false
+
   let mk_bool = Cvc5_external.mk_bool
+
   let mk_int = Cvc5_external.mk_int
-  let mk_rm (tm : TermManager.tm) (rm : RoundingMode.t) = 
+
+  let mk_rm (tm : TermManager.tm) (rm : RoundingMode.t) =
     Cvc5_external.mk_roundingmode tm (RoundingMode.to_cpp rm)
 end
 
-module Result =
-struct
+module Result = struct
   type result = Cvc5_external.result
 
   let is_sat = Cvc5_external.result_is_sat
+
   let is_unsat = Cvc5_external.result_is_unsat
+
   let is_unknown = Cvc5_external.result_is_unknown
 end
 
-module Solver =
-struct
+module Solver = struct
   type solver = Cvc5_external.solver
 
   let mk_solver = Cvc5_external.new_solver
+
   let delete_solver = Cvc5_external.delete
+
   let assert_formula = Cvc5_external.assert_formula
+
   let check_sat = Cvc5_external.check_sat
+
   let set_logic = Cvc5_external.set_logic
+
   let simplify = Cvc5_external.simplify
+
   let push = Cvc5_external.push
+
   let pop = Cvc5_external.pop
+
   let reset = Cvc5_external.reset_assertions
 end
-

cvc5.mli

@@ -3,64 +3,86 @@ exception Error of string
 module Kind = Cvc5_enums.Kind
 module RoundingMode = Cvc5_enums.RoundingMode
 
-module TermManager :
-sig 
+module TermManager : sig
   type tm
 
   val mk_tm : unit -> tm
+
   val delete_tm : tm -> unit
 end
 
-module Sort : 
-sig
+module Sort : sig
   type sort
-  
+
   val mk_bool_sort : TermManager.tm -> sort
+
   val mk_int_sort : TermManager.tm -> sort
+
   val mk_real_sort : TermManager.tm -> sort
+
   val mk_string_sort : TermManager.tm -> sort
+
   val mk_bv_sort : TermManager.tm -> int -> sort
 end
 
-module Term : 
-sig 
+module Term : sig
   type term
 
   val id : term -> int
+
   val equal : term -> term -> bool
+
   val kind : term -> Kind.t
+
   val sort : term -> Sort.sort
+
   val to_string : term -> string
+
   val mk_const : TermManager.tm -> Sort.sort -> term
+
   val mk_const_s : TermManager.tm -> Sort.sort -> string -> term
+
   val mk_term : TermManager.tm -> Kind.t -> term array -> term
+
   val mk_true : TermManager.tm -> term
+
   val mk_false : TermManager.tm -> term
+
   val mk_bool : TermManager.tm -> bool -> term
+
   val mk_int : TermManager.tm -> int -> term
+
   val mk_rm : TermManager.tm -> RoundingMode.t -> term
 end
 
-module Result : 
-sig 
-  type result 
+module Result : sig
+  type result
 
   val is_sat : result -> bool
+
   val is_unsat : result -> bool
+
   val is_unknown : result -> bool
 end
 
-module Solver :
-sig
+module Solver : sig
   type solver
 
   val mk_solver : TermManager.tm -> solver
+
   val delete_solver : solver -> unit
+
   val assert_formula : solver -> Term.term -> unit
+
   val check_sat : solver -> Result.result
+
   val set_logic : solver -> string -> unit
+
   val simplify : solver -> Term.term -> Term.term
+
   val push : solver -> int -> unit
+
   val pop : solver -> int -> unit
+
   val reset : solver -> unit
-end
+end

cvc5.opam

@@ -0,0 +1,33 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "OCaml bindings for the cvc5 SMT solver"
+description: "OCaml bindings for the cvc5 SMT solver"
+maintainer: ["João Pereira <joaomhmpereira@tecnico.ulisboa.pt>"]
+authors: ["João Pereira <joaomhmpereira@tecnico.ulisboa.pt>"]
+homepage: "https://github.com/formalsec/ocaml-cvc5"
+bug-reports: "https://github.com/formalsec/ocaml-cvc5/issues"
+depends: [
+  "dune" {>= "3.10"}
+  "ocaml" {>= "4.12"}
+  "conf-gcc" {build}
+  "conf-g++" {build}
+  "conf-gmp" {build}
+  "conf-cmake" {build}
+  "conf-python-3" {build}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/formalsec/ocaml-cvc5.git"