From e99beae12e0e6b25cf68c7f8882b7ab202d2e23a Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Thu, 4 Apr 2024 00:49:28 +0100 Subject: [PATCH 1/6] Opam configuration and public_name --- cvc5.opam | 32 ++++++++++++++++++++++++++++++++ dune | 19 ++++++++++--------- dune-project | 25 +++++++++++++++++++++++-- vendor/dune | 12 +++++++++--- 4 files changed, 74 insertions(+), 14 deletions(-) create mode 100644 cvc5.opam diff --git a/cvc5.opam b/cvc5.opam new file mode 100644 index 0000000..1fb6b2d --- /dev/null +++ b/cvc5.opam @@ -0,0 +1,32 @@ +# 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 "] +authors: ["João Pereira "] +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-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" diff --git a/dune b/dune index 74ab8c8..4feff3f 100644 --- a/dune +++ b/dune @@ -1,16 +1,12 @@ -(executable - (name toy) - (libraries cvc5) - (modules toy)) - (library + (public_name cvc5) (name cvc5) (modules cvc5 cvc5_enums cvc5_external) - (foreign_stubs + (foreign_stubs (language cxx) (names cvc5_stubs) (flags :standard -std=c++17 -I/opt/homebrew/include) - (include_dirs + (include_dirs vendor/cvc5/include vendor/cvc5/src vendor/cvc5/src/lib)) @@ -22,9 +18,14 @@ (c_library_flags :standard -std=c++17 -L/opt/homebrew/lib -lgmp)) (rule - (deps (:executable api/cvc5_enums.exe)) + (deps ./api/cvc5_enums.exe) (target cvc5_enums.ml) (action (with-stdout-to %{target} - (run %{deps})))) \ No newline at end of file + (run %{deps})))) + +(executable + (name toy) + (libraries cvc5) + (modules toy)) diff --git a/dune-project b/dune-project index 0293f42..353ce83 100644 --- a/dune-project +++ b/dune-project @@ -1,3 +1,24 @@ -(lang dune 3.7) +(lang dune 3.10) -(name cvc5_cxx) \ No newline at end of file +(name cvc5) + +(generate_opam_files true) + +(source + (github formalsec/ocaml-cvc5)) + +(authors "João Pereira ") + +(maintainers "João Pereira ") + +(package + (name cvc5) + (synopsis "OCaml bindings for the CVC5 SMT solver") + (description "OCaml bindings for the CVC5 SMT solver") + (depends + dune + (ocaml (>= 4.12)) + (conf-gcc :build) + (conf-g++ :build) + (conf-gmp :build) + (conf-python-3 :build))) diff --git a/vendor/dune b/vendor/dune index c961ee4..dcc8666 100644 --- a/vendor/dune +++ b/vendor/dune @@ -5,6 +5,12 @@ (source_tree cvc5)) (targets libcvc5.a libcadical.a libpicpoly.a libpicpolyxx.a) (action - (bash - "\ncd cvc5 && ./configure.sh --auto-download --static\ncd build && make\ncd ../../\ncp cvc5/build/src/libcvc5.a libcvc5.a\ncp cvc5/build/deps/lib/libcadical.a libcadical.a\n cp cvc5/build/deps/lib/libpicpoly.a libpicpoly.a\ncp cvc5/build/deps/lib/libpicpolyxx.a libpicpolyxx.a\n")) -) \ No newline at end of file + (chdir cvc5 + (progn + ; (run pipx install -r contrib/requirements_build.txt) + (run ./configure.sh --auto-download --static) + (run make -C build -j 4) + (bash "cp build/src/libcvc5.a ../libcvc5.a") + (bash "cp build/deps/lib/libcadical.a ../libcadical.a") + (bash "cp build/deps/lib/libpicpoly.a ../libpicpoly.a") + (bash "cp build/deps/lib/libpicpolyxx.a ../libpicpolyxx.a"))))) From aad7d729ac240166ab7fc26cc874e735ad31f16f Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Thu, 4 Apr 2024 00:56:10 +0100 Subject: [PATCH 2/6] simple CI --- .github/workflows/build.yml | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 .github/workflows/build.yml diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml new file mode 100644 index 0000000..38e133c --- /dev/null +++ b/.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 From 287d66d601d6499aa63d1873fe85137cabc05817 Mon Sep 17 00:00:00 2001 From: joaomhmpereira Date: Thu, 4 Apr 2024 16:10:17 +0100 Subject: [PATCH 3/6] link libraries statically --- api/dune | 15 +++++++++------ cvc5.opam | 4 ++-- dune | 35 ++++++++++++++++++++++++++++------- dune-project | 4 ++-- vendor/dune | 16 ---------------- 5 files changed, 41 insertions(+), 33 deletions(-) delete mode 100644 vendor/dune diff --git a/api/dune b/api/dune index ccf8d43..ac9ad0d 100644 --- a/api/dune +++ b/api/dune @@ -12,9 +12,12 @@ (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)) \ No newline at end of file + (c_library_flags + :standard -std=c++17 + -L/opt/homebrew/lib + -lgmp + -lcvc5 + -lcadical + -lpicpoly + -lpicpolyxx + -L%{project_root}/_build/default/)) \ No newline at end of file diff --git a/cvc5.opam b/cvc5.opam index 1fb6b2d..47b7689 100644 --- a/cvc5.opam +++ b/cvc5.opam @@ -2,8 +2,8 @@ opam-version: "2.0" synopsis: "OCaml bindings for the CVC5 SMT solver" description: "OCaml bindings for the CVC5 SMT solver" -maintainer: ["João Pereira "] -authors: ["João Pereira "] +maintainer: ["João Pereira "] +authors: ["João Pereira "] homepage: "https://github.com/formalsec/ocaml-cvc5" bug-reports: "https://github.com/formalsec/ocaml-cvc5/issues" depends: [ diff --git a/dune b/dune index 4feff3f..454ba1b 100644 --- a/dune +++ b/dune @@ -1,3 +1,21 @@ +(rule + (deps + (source_tree vendor)) + (targets libpicpolyxx.a libpicpoly.a libcadical.a libcvc5.a) + (action + (no-infer + (progn + (chdir vendor + (chdir cvc5 + (progn + ; (run pipx install -r contrib/requirements_build.txt) + (run ./configure.sh --auto-download --static) + (run make -C build -j 4)))) + (copy vendor/cvc5/build/src/libcvc5.a libcvc5.a) + (copy vendor/cvc5/build/deps/lib/libcadical.a libcadical.a) + (copy vendor/cvc5/build/deps/lib/libpicpoly.a libpicpoly.a) + (copy vendor/cvc5/build/deps/lib/libpicpolyxx.a libpicpolyxx.a))))) + (library (public_name cvc5) (name cvc5) @@ -10,12 +28,15 @@ vendor/cvc5/include vendor/cvc5/src vendor/cvc5/src/lib)) - (foreign_archives - vendor/cadical - vendor/cvc5 - vendor/picpoly - vendor/picpolyxx) - (c_library_flags :standard -std=c++17 -L/opt/homebrew/lib -lgmp)) + (c_library_flags + :standard -std=c++17 + -L/opt/homebrew/lib + -lgmp + -lcvc5 + -lcadical + -lpicpoly + -lpicpolyxx + -L%{project_root}/_build/default/)) (rule (deps ./api/cvc5_enums.exe) @@ -28,4 +49,4 @@ (executable (name toy) (libraries cvc5) - (modules toy)) + (modules toy)) \ No newline at end of file diff --git a/dune-project b/dune-project index 353ce83..07572bb 100644 --- a/dune-project +++ b/dune-project @@ -7,9 +7,9 @@ (source (github formalsec/ocaml-cvc5)) -(authors "João Pereira ") +(authors "João Pereira ") -(maintainers "João Pereira ") +(maintainers "João Pereira ") (package (name cvc5) diff --git a/vendor/dune b/vendor/dune deleted file mode 100644 index dcc8666..0000000 --- a/vendor/dune +++ /dev/null @@ -1,16 +0,0 @@ -(data_only_dirs cvc5) - -(rule - (deps - (source_tree cvc5)) - (targets libcvc5.a libcadical.a libpicpoly.a libpicpolyxx.a) - (action - (chdir cvc5 - (progn - ; (run pipx install -r contrib/requirements_build.txt) - (run ./configure.sh --auto-download --static) - (run make -C build -j 4) - (bash "cp build/src/libcvc5.a ../libcvc5.a") - (bash "cp build/deps/lib/libcadical.a ../libcadical.a") - (bash "cp build/deps/lib/libpicpoly.a ../libpicpoly.a") - (bash "cp build/deps/lib/libpicpolyxx.a ../libpicpolyxx.a"))))) From adfe0b65edb0abe6ceb69926e9cf6fe8d12314d0 Mon Sep 17 00:00:00 2001 From: joaomhmpereira Date: Thu, 4 Apr 2024 19:15:47 +0100 Subject: [PATCH 4/6] explicitly disable dynamic linking --- api/dune | 13 +++++++------ dune | 22 +++++++++++----------- 2 files changed, 18 insertions(+), 17 deletions(-) diff --git a/api/dune b/api/dune index ac9ad0d..111ac7e 100644 --- a/api/dune +++ b/api/dune @@ -6,18 +6,19 @@ (library (name build_enums) (modules build_enums) + (no_dynlink) (foreign_stubs (language cxx) (names build_enums) (flags :standard -std=c++17 -I/opt/homebrew/include) (include_dirs ../vendor/cvc5/include)) + (foreign_archives + ../cvc5 + ../cadical + ../picpoly + ../picpolyxx) (c_library_flags :standard -std=c++17 -L/opt/homebrew/lib - -lgmp - -lcvc5 - -lcadical - -lpicpoly - -lpicpolyxx - -L%{project_root}/_build/default/)) \ No newline at end of file + -lgmp)) \ No newline at end of file diff --git a/dune b/dune index 454ba1b..439dd80 100644 --- a/dune +++ b/dune @@ -1,7 +1,7 @@ (rule (deps (source_tree vendor)) - (targets libpicpolyxx.a libpicpoly.a libcadical.a libcvc5.a) + (targets libpicpolyxx.a libpicpoly.a libcadical.a libcvc5.a cvc5_export.h) (action (no-infer (progn @@ -14,29 +14,29 @@ (copy vendor/cvc5/build/src/libcvc5.a libcvc5.a) (copy vendor/cvc5/build/deps/lib/libcadical.a libcadical.a) (copy vendor/cvc5/build/deps/lib/libpicpoly.a libpicpoly.a) - (copy vendor/cvc5/build/deps/lib/libpicpolyxx.a libpicpolyxx.a))))) + (copy vendor/cvc5/build/deps/lib/libpicpolyxx.a libpicpolyxx.a) + (copy vendor/cvc5/build/include/cvc5/cvc5_export.h cvc5_export.h))))) (library (public_name cvc5) (name cvc5) (modules cvc5 cvc5_enums cvc5_external) + (no_dynlink) (foreign_stubs (language cxx) (names cvc5_stubs) + (extra_deps cvc5_export.h) (flags :standard -std=c++17 -I/opt/homebrew/include) (include_dirs vendor/cvc5/include vendor/cvc5/src vendor/cvc5/src/lib)) - (c_library_flags - :standard -std=c++17 - -L/opt/homebrew/lib - -lgmp - -lcvc5 - -lcadical - -lpicpoly - -lpicpolyxx - -L%{project_root}/_build/default/)) + (foreign_archives + cadical + cvc5 + picpoly + picpolyxx) + (c_library_flags :standard -std=c++17 -L/opt/homebrew/lib -lgmp)) (rule (deps ./api/cvc5_enums.exe) From f4b9d9eb443b87236cf3a0158084bb1effacee01 Mon Sep 17 00:00:00 2001 From: joaomhmpereira Date: Fri, 5 Apr 2024 18:01:37 +0100 Subject: [PATCH 5/6] export header file dependency --- api/dune | 1 + cvc5.opam | 5 +++-- dune | 2 +- dune-project | 5 +++-- 4 files changed, 8 insertions(+), 5 deletions(-) diff --git a/api/dune b/api/dune index 111ac7e..62dcba4 100644 --- a/api/dune +++ b/api/dune @@ -10,6 +10,7 @@ (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)) diff --git a/cvc5.opam b/cvc5.opam index 47b7689..7b6b91b 100644 --- a/cvc5.opam +++ b/cvc5.opam @@ -1,7 +1,7 @@ # 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" +synopsis: "OCaml bindings for the cvc5 SMT solver" +description: "OCaml bindings for the cvc5 SMT solver" maintainer: ["João Pereira "] authors: ["João Pereira "] homepage: "https://github.com/formalsec/ocaml-cvc5" @@ -12,6 +12,7 @@ depends: [ "conf-gcc" {build} "conf-g++" {build} "conf-gmp" {build} + "conf-cmake" {build} "conf-python-3" {build} "odoc" {with-doc} ] diff --git a/dune b/dune index 439dd80..152a8b2 100644 --- a/dune +++ b/dune @@ -8,13 +8,13 @@ (chdir vendor (chdir cvc5 (progn - ; (run pipx install -r contrib/requirements_build.txt) (run ./configure.sh --auto-download --static) (run make -C build -j 4)))) (copy vendor/cvc5/build/src/libcvc5.a libcvc5.a) (copy vendor/cvc5/build/deps/lib/libcadical.a libcadical.a) (copy vendor/cvc5/build/deps/lib/libpicpoly.a libpicpoly.a) (copy vendor/cvc5/build/deps/lib/libpicpolyxx.a libpicpolyxx.a) + (copy vendor/cvc5/build/include/cvc5/cvc5_export.h vendor/cvc5/include/cvc5/cvc5_export.h) (copy vendor/cvc5/build/include/cvc5/cvc5_export.h cvc5_export.h))))) (library diff --git a/dune-project b/dune-project index 07572bb..6a75bd5 100644 --- a/dune-project +++ b/dune-project @@ -13,12 +13,13 @@ (package (name cvc5) - (synopsis "OCaml bindings for the CVC5 SMT solver") - (description "OCaml bindings for the CVC5 SMT solver") + (synopsis "OCaml bindings for the cvc5 SMT solver") + (description "OCaml bindings for the cvc5 SMT solver") (depends dune (ocaml (>= 4.12)) (conf-gcc :build) (conf-g++ :build) (conf-gmp :build) + (conf-cmake :build) (conf-python-3 :build))) From 26ddd93c35ebf3ca9cbb0f94d6f091a5d0a656e2 Mon Sep 17 00:00:00 2001 From: joaomhmpereira Date: Fri, 5 Apr 2024 18:30:50 +0100 Subject: [PATCH 6/6] add .ocamlformat --- .ocamlformat | 43 ++++++++++++++++++++++ api/build_enums.ml | 2 +- api/cvc5_enums.ml | 3 +- api/dune | 14 ++----- cvc5.ml | 42 ++++++++++++++------- cvc5.mli | 43 +++++++++++++++------- cvc5_external.ml | 91 ++++++++++++++++++++++++++++++++++++++++------ dune | 27 ++++++-------- toy.ml | 10 +++-- 9 files changed, 204 insertions(+), 71 deletions(-) create mode 100644 .ocamlformat diff --git a/.ocamlformat b/.ocamlformat new file mode 100644 index 0000000..5c3c54e --- /dev/null +++ b/.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 \ No newline at end of file diff --git a/api/build_enums.ml b/api/build_enums.ml index f5ae294..8b00e65 100644 --- a/api/build_enums.ml +++ b/api/build_enums.ml @@ -1 +1 @@ -external build_enums : unit -> unit = "build_enums" \ No newline at end of file +external build_enums : unit -> unit = "build_enums" diff --git a/api/cvc5_enums.ml b/api/cvc5_enums.ml index 0db1139..604deb1 100644 --- a/api/cvc5_enums.ml +++ b/api/cvc5_enums.ml @@ -1,4 +1,3 @@ open Build_enums -let () = - build_enums () \ No newline at end of file +let () = build_enums () diff --git a/api/dune b/api/dune index 62dcba4..6cad891 100644 --- a/api/dune +++ b/api/dune @@ -12,14 +12,6 @@ (names build_enums) (extra_deps ../cvc5_export.h) (flags :standard -std=c++17 -I/opt/homebrew/include) - (include_dirs - ../vendor/cvc5/include)) - (foreign_archives - ../cvc5 - ../cadical - ../picpoly - ../picpolyxx) - (c_library_flags - :standard -std=c++17 - -L/opt/homebrew/lib - -lgmp)) \ No newline at end of file + (include_dirs ../vendor/cvc5/include)) + (foreign_archives ../cvc5 ../cadical ../picpoly ../picpolyxx) + (c_library_flags :standard -std=c++17 -L/opt/homebrew/lib -lgmp)) diff --git a/cvc5.ml b/cvc5.ml index 05a49bf..b891c36 100644 --- a/cvc5.ml +++ b/cvc5.ml @@ -6,61 +6,77 @@ let _ = Callback.register_exception "cvc5Exception" (Error "") module Kind = Kind -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 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 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 - diff --git a/cvc5.mli b/cvc5.mli index a3c8170..8e82e3c 100644 --- a/cvc5.mli +++ b/cvc5.mli @@ -2,59 +2,76 @@ exception Error of string module Kind = Cvc5_enums.Kind -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 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 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 \ No newline at end of file +end diff --git a/cvc5_external.ml b/cvc5_external.ml index 9eb21a6..94e5569 100644 --- a/cvc5_external.ml +++ b/cvc5_external.ml @@ -3,63 +3,130 @@ (** External declarations for cvc5's OCaml bindings. *) (**/**) + type ptr + and result = ptr + and synth_result = ptr + and sort = ptr + and term = ptr + and op = ptr + and datatype = ptr + and datatype_constructor_decl = ptr + and datatype_decl = ptr + and datatype_selector = ptr + and datatype_constructor = ptr + and grammar = ptr + and solver = ptr + and term_manager = ptr + and option_info = ptr + and proof = ptr + and proof_rule = ptr + and statistics = ptr + and unknown_explanation = ptr + and sort_kind = ptr + and kind = ptr + and rounding_mode = ptr + and proof_format = ptr + and proof_component = ptr + and learned_lit_type = ptr + and block_model_mode = ptr + and find_synth_target = ptr external result_is_sat : result -> bool = "ocaml_cvc5_stub_result_is_sat" + external result_is_unsat : result -> bool = "ocaml_cvc5_stub_result_is_unsat" -external result_is_unknown : result -> bool = "ocaml_cvc5_stub_result_is_unknown" + +external result_is_unknown : result -> bool + = "ocaml_cvc5_stub_result_is_unknown" + external mk_true : term_manager -> term = "ocaml_cvc5_stub_mk_true" + external mk_false : term_manager -> term = "ocaml_cvc5_stub_mk_false" + external mk_bool : term_manager -> bool -> term = "ocaml_cvc5_stub_mk_bool" + external mk_int : term_manager -> int -> term = "ocaml_cvc5_stub_mk_int" + external mk_bv : term_manager -> int -> int64 -> term = "ocaml_cvc5_stub_mk_bv" + external mk_real : term_manager -> string -> term = "ocaml_cvc5_stub_mk_real" -external mk_string : term_manager -> string -> term = "ocaml_cvc5_stub_mk_string" -external mk_term : term_manager -> int -> term array -> term = "ocaml_cvc5_stub_mk_term" -external get_boolean_sort : term_manager -> sort = "ocaml_cvc5_stub_get_boolean_sort" -external get_integer_sort : term_manager -> sort = "ocaml_cvc5_stub_get_integer_sort" + +external mk_string : term_manager -> string -> term + = "ocaml_cvc5_stub_mk_string" + +external mk_term : term_manager -> int -> term array -> term + = "ocaml_cvc5_stub_mk_term" + +external get_boolean_sort : term_manager -> sort + = "ocaml_cvc5_stub_get_boolean_sort" + +external get_integer_sort : term_manager -> sort + = "ocaml_cvc5_stub_get_integer_sort" + external get_real_sort : term_manager -> sort = "ocaml_cvc5_stub_get_real_sort" -external get_string_sort : term_manager -> sort = "ocaml_cvc5_stub_get_string_sort" -external mk_bitvector_sort : term_manager -> int -> sort = "ocaml_cvc5_stub_mk_bitvector_sort" -external mk_const_s : term_manager -> sort -> string -> term = "ocaml_cvc5_stub_mk_const_s" + +external get_string_sort : term_manager -> sort + = "ocaml_cvc5_stub_get_string_sort" + +external mk_bitvector_sort : term_manager -> int -> sort + = "ocaml_cvc5_stub_mk_bitvector_sort" + +external mk_const_s : term_manager -> sort -> string -> term + = "ocaml_cvc5_stub_mk_const_s" + external mk_const : term_manager -> sort -> term = "ocaml_cvc5_stub_mk_const" + external term_to_string : term -> string = "ocaml_cvc5_stub_term_to_string" + external new_solver : term_manager -> solver = "ocaml_cvc5_stub_new_solver" -external new_term_manager : unit -> term_manager = "ocaml_cvc5_stub_new_term_manager" -external delete_term_manager : term_manager -> unit = "ocaml_cvc5_stub_delete_term_manager" + +external new_term_manager : unit -> term_manager + = "ocaml_cvc5_stub_new_term_manager" + +external delete_term_manager : term_manager -> unit + = "ocaml_cvc5_stub_delete_term_manager" + external delete : solver -> unit = "ocaml_cvc5_stub_delete" -external assert_formula : solver -> term -> unit = "ocaml_cvc5_stub_assert_formula" + +external assert_formula : solver -> term -> unit + = "ocaml_cvc5_stub_assert_formula" + external check_sat : solver -> result = "ocaml_cvc5_stub_check_sat" + external set_logic : solver -> string -> unit = "ocaml_cvc5_stub_set_logic" + external simplify : solver -> term -> term = "ocaml_cvc5_stub_simplify" + external push : solver -> int -> unit = "ocaml_cvc5_stub_push" + external pop : solver -> int -> unit = "ocaml_cvc5_stub_pop" + external reset_assertions : solver -> unit = "ocaml_cvc5_stub_reset_assertions" -(**/**) \ No newline at end of file +(**/**) diff --git a/dune b/dune index 152a8b2..8156784 100644 --- a/dune +++ b/dune @@ -5,16 +5,18 @@ (action (no-infer (progn - (chdir vendor - (chdir cvc5 - (progn - (run ./configure.sh --auto-download --static) - (run make -C build -j 4)))) + (chdir + vendor/cvc5 + (progn + (run ./configure.sh --auto-download --static) + (run make -C build -j 4))) (copy vendor/cvc5/build/src/libcvc5.a libcvc5.a) (copy vendor/cvc5/build/deps/lib/libcadical.a libcadical.a) (copy vendor/cvc5/build/deps/lib/libpicpoly.a libpicpoly.a) (copy vendor/cvc5/build/deps/lib/libpicpolyxx.a libpicpolyxx.a) - (copy vendor/cvc5/build/include/cvc5/cvc5_export.h vendor/cvc5/include/cvc5/cvc5_export.h) + (copy + vendor/cvc5/build/include/cvc5/cvc5_export.h + vendor/cvc5/include/cvc5/cvc5_export.h) (copy vendor/cvc5/build/include/cvc5/cvc5_export.h cvc5_export.h))))) (library @@ -27,15 +29,8 @@ (names cvc5_stubs) (extra_deps cvc5_export.h) (flags :standard -std=c++17 -I/opt/homebrew/include) - (include_dirs - vendor/cvc5/include - vendor/cvc5/src - vendor/cvc5/src/lib)) - (foreign_archives - cadical - cvc5 - picpoly - picpolyxx) + (include_dirs vendor/cvc5/include vendor/cvc5/src vendor/cvc5/src/lib)) + (foreign_archives cadical cvc5 picpoly picpolyxx) (c_library_flags :standard -std=c++17 -L/opt/homebrew/lib -lgmp)) (rule @@ -49,4 +44,4 @@ (executable (name toy) (libraries cvc5) - (modules toy)) \ No newline at end of file + (modules toy)) diff --git a/toy.ml b/toy.ml index 09fd03b..1611194 100644 --- a/toy.ml +++ b/toy.ml @@ -1,15 +1,19 @@ open Cvc5 let tm = TermManager.mk_tm () + let solver = Solver.mk_solver tm + let int_sort = Sort.mk_int_sort tm + 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 + 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 + let x_lt_zero = Term.mk_term tm Kind.Lt [| zero; x |] in print_endline (Term.to_string x_lt_zero); (* x > 0 *) Solver.assert_formula solver x_gt_zero; @@ -21,4 +25,4 @@ let () = TermManager.delete_tm tm; match b with | true -> print_endline "sat OCaml" - | false -> print_endline "unsat OCaml" + | false -> print_endline "unsat OCaml"