diff --git a/api/dune b/api/dune index 37bd731..3d18462 100644 --- a/api/dune +++ b/api/dune @@ -1,17 +1,21 @@ -(executable - (name cvc5_enums) - (modules cvc5_enums) - (libraries build_enums)) +; (executable +; (name cvc5_enums) +; (modules cvc5_enums) +; (libraries build_enums)) -(library - (name build_enums) - (modules build_enums) - (no_dynlink) - (foreign_stubs - (language cxx) - (names build_enums) - (extra_deps ../vendor/cvc5/include/cvc5/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)) +; (library +; (name build_enums) +; (modules build_enums) +; (no_dynlink) +; (foreign_stubs +; (language cxx) +; (names build_enums) +; (extra_deps ../vendor/cvc5/include/cvc5/cvc5_export.h) +; (flags :standard -std=c++17 -I/opt/homebrew/include) +; (include_dirs ../vendor/cvc5/include)) +; (foreign_archives +; ../cvc5 +; ../vendor/cadical/cadical +; ../picpoly +; ../vendor/libpoly/src/polyxx/picpolyxx) +; (c_library_flags :standard -std=c++17 -L/opt/homebrew/lib -lgmp)) diff --git a/dune b/dune index 35d50b8..ae550cb 100644 --- a/dune +++ b/dune @@ -4,67 +4,163 @@ (CMAKE_INCLUDE_PATH "../../cadical/src/:../../libpoly/:../../") (CMAKE_LIBRARY_PATH "../../cadical/build/:../../libpoly/build/src/")))) -(rule - (deps - (source_tree vendor)) - (targets libpicpolyxx.a libpicpoly.a libcadical.a libcvc5.a cvc5_export.h) - (action - (no-infer - (progn - (chdir - vendor/cadical - (progn - (bash "CXXFLAGS=-fPIC ./configure") - (bash "make -j $(opam var jobs)"))) - (copy vendor/cadical/build/libcadical.a libcadical.a) - (chdir - vendor/libpoly - (progn - (run - cmake - -B - build - -DCMAKE_BUILD_TYPE=$type - -DCMAKE_INSTALL_PREFIX=$prefix) - (chdir - build - (bash "make -j $(opam var jobs)")) - (run mv include poly))) - (copy vendor/libpoly/build/src/libpicpoly.a libpicpoly.a) - (copy vendor/libpoly/build/src/libpicpolyxx.a libpicpolyxx.a) - (chdir - vendor/cvc5 - (progn - (bash "./configure.sh --static") - (bash "make -C build -j $(opam var jobs)"))) - (copy vendor/cvc5/build/src/libcvc5.a libcvc5.a) - (copy vendor/cvc5/build/include/cvc5/cvc5_export.h cvc5_export.h))))) +(subdir + vendor/cadical + (include_subdirs unqualified) + (dirs src) + (foreign_library + (archive_name cadical) + (language cxx) + (names :standard \ mobical cadical) + (include_dirs src) + (flags :standard -std=c++11 -DNDEBUG -DNBUILD -DNCLOSEFORM))) (subdir - vendor/cvc5/include/cvc5 - (rule - (deps ../../../../cvc5_export.h) - (targets cvc5_export.h) - (action - (copy %{deps} %{targets})))) + vendor/libpoly + (dirs include src) + (subdir + src/utils + (foreign_library + (archive_name polyutils) + (language c) + (names :standard) + (flags :standard -std=gnu99 -Wall -Werror -Wextra -I..) + (include_dirs ../../include))) + (subdir + src/variable + (foreign_library + (archive_name polyvariable) + (language c) + (names :standard) + (flags :standard -std=gnu99 -Wall -Werror -Wextra -I..) + (include_dirs ../../include))) + (subdir + src/number + (foreign_library + (archive_name polynumber) + (language c) + (names :standard) + (flags :standard -std=gnu99 -Wall -Werror -Wextra -I..) + (include_dirs ../../include))) + (subdir + src/interval + (foreign_library + (archive_name polyinterval) + (language c) + (names :standard) + (flags :standard -std=gnu99 -Wall -Werror -Wextra -I..) + (include_dirs ../../include))) + (subdir + src/polynomial + (foreign_library + (archive_name polypolynomial) + (language c) + (names :standard) + (flags :standard -std=gnu99 -Wall -Werror -Wextra -I..) + (include_dirs ../../include))) + (subdir + src/upolynomial + (foreign_library + (archive_name polyupolynomial) + (language c) + (names :standard) + (flags :standard -std=gnu99 -Wall -Werror -Wextra -I..) + (include_dirs ../../include))) + (subdir + src/polyxx + (foreign_library + (archive_name polyxx) + (language cxx) + (names :standard) + (flags :standard -std=c++11 -Wall -Werror -Wextra) + (include_dirs ../../include))) + (subdir + src + (foreign_library + (archive_name poly) + (language c) + (names :standard) + (flags :standard -std=gnu99 -Wall -Werror -Wextra -I.) + (include_dirs ../include))) + ) (library - (public_name cvc5) - (name cvc5) - (modules cvc5 cvc5_enums cvc5_external) - (no_dynlink) - (foreign_stubs - (language cxx) - (names cvc5_stubs) - (flags :standard -std=c++17 -I/opt/homebrew/include) - (include_dirs vendor/cvc5/include vendor/cvc5/src vendor/cvc5/src/lib)) - (foreign_archives cvc5 cadical picpoly picpolyxx) - (c_library_flags :standard -std=c++17 -L/opt/homebrew/lib -lgmp)) + (name poly) + (modules ()) + (foreign_archives + vendor/libpoly/src/utils/polyutils + vendor/libpoly/src/variable/polyvariable + vendor/libpoly/src/number/polynumber + vendor/libpoly/src/interval/polyinterval + vendor/libpoly/src/polynomial/polypolynomial + vendor/libpoly/src/upolynomial/polyupolynomial + vendor/libpoly/src/poly) + (c_library_flags :standard -lgmp)) + + +; (rule +; (deps +; (source_tree vendor)) +; (targets libpicpoly.a libcvc5.a cvc5_export.h) +; (action +; (no-infer + ; (progn + ; (chdir + ; vendor/cadical + ; (progn + ; (bash "CXXFLAGS=-fPIC ./configure") + ; (bash "make -j $(opam var jobs)"))) + ; (copy vendor/cadical/build/libcadical.a libcadical.a) + ; (chdir + ; vendor/libpoly + ; (progn + ; (run + ; cmake + ; -B + ; build + ; -DCMAKE_BUILD_TYPE=$type + ; -DCMAKE_INSTALL_PREFIX=$prefix) + ; (chdir + ; build + ; (bash "make -j $(opam var jobs)")) + ; (run mv include poly))) + ; (copy vendor/libpoly/build/src/libpicpoly.a libpicpoly.a) + ; (copy vendor/libpoly/build/src/libpicpolyxx.a libpicpolyxx.a) + ; (chdir + ; vendor/cvc5 + ; (progn + ; (bash "./configure.sh --static") + ; (bash "make -C build -j $(opam var jobs)"))) + ; (copy vendor/cvc5/build/src/libcvc5.a libcvc5.a) + ; (copy vendor/cvc5/build/include/cvc5/cvc5_export.h cvc5_export.h))))) + +; (subdir +; vendor/cvc5/include/cvc5 +; (rule +; (deps ../../../../cvc5_export.h) +; (targets cvc5_export.h) +; (action +; (copy %{deps} %{targets})))) + +; (library +; (public_name cvc5) +; (name cvc5) +; (modules cvc5 cvc5_enums cvc5_external) +; (no_dynlink) +; (foreign_stubs +; (language cxx) +; (names cvc5_stubs) +; (flags :standard -std=c++17 -I/opt/homebrew/include) +; (include_dirs vendor/cvc5/include vendor/cvc5/src vendor/cvc5/src/lib)) +; (foreign_archives +; cadical +; vendor/libpoly/src/interval/picpolyinterval) +; (c_library_flags :standard -std=c++17 -L/opt/homebrew/lib -lgmp)) -(rule - (deps ./api/cvc5_enums.exe) - (target cvc5_enums.ml) - (action - (with-stdout-to - %{target} - (run %{deps})))) +; (rule +; (deps ./api/cvc5_enums.exe) +; (target cvc5_enums.ml) +; (action +; (with-stdout-to +; %{target} +; (run %{deps})))) diff --git a/dune-project b/dune-project index 5837a9b..2ed0966 100644 --- a/dune-project +++ b/dune-project @@ -16,6 +16,7 @@ (license "MIT") (package + (allow_empty) (name cvc5) (synopsis "OCaml bindings for the cvc5 SMT solver") (description "OCaml bindings for the cvc5 SMT solver") diff --git a/examples/dune b/examples/dune index 48fd2c9..d235b37 100644 --- a/examples/dune +++ b/examples/dune @@ -1,4 +1,4 @@ -(executables - (names toy incremental functions bitv fp) - (modules toy incremental functions bitv fp) - (libraries cvc5)) +; (executables +; (names toy incremental functions bitv fp) +; (modules toy incremental functions bitv fp) + ; (libraries cvc5)) diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..5e7cccf --- /dev/null +++ b/flake.lock @@ -0,0 +1,25 @@ +{ + "nodes": { + "nixpkgs": { + "locked": { + "lastModified": 1775888245, + "narHash": "sha256-nwASzrRDD1JBEu/o8ekKYEXm/oJW6EMCzCRdrwcLe90=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "13043924aaa7375ce482ebe2494338e058282925", + "type": "github" + }, + "original": { + "id": "nixpkgs", + "type": "indirect" + } + }, + "root": { + "inputs": { + "nixpkgs": "nixpkgs" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..bc9e1bd --- /dev/null +++ b/flake.nix @@ -0,0 +1,40 @@ +{ + description = "OCaml development environment"; + + inputs = { + nixpkgs.url = "nixpkgs"; + }; + + outputs = { self, nixpkgs }: + let + # Define supported systems + supportedSystems = [ "x86_64-linux" "aarch64-linux" "x86_64-darwin" "aarch64-darwin" ]; + + # Helper function to generate attributes for each system + forAllSystems = nixpkgs.lib.genAttrs supportedSystems; + in + { + devShells = forAllSystems (system: + let + pkgs = import nixpkgs { inherit system; }; + in + { + default = pkgs.mkShell { + nativeBuildInputs = with pkgs; [ + opam + pkg-config + ]; + + buildInputs = with pkgs; [ + zlib + gmp.dev + gmpxx + m4 + flint + cmake + ]; + }; + } + ); + }; +} diff --git a/test/dune b/test/dune index ebc652d..0ff36e4 100644 --- a/test/dune +++ b/test/dune @@ -1,3 +1,3 @@ -(tests - (names test_trivial test_terms test_val_interp test_model) - (libraries cvc5)) +; (tests +; (names test_trivial test_terms test_val_interp test_model) +; (libraries cvc5))