Gbury/dolmen
1
1
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction
701 commits 76 branches 12 tags 15 MiB
  • OCaml 85.4%
  • SMT 12.5%
  • Gnuplot 1.9%
  • Perl 0.1%
Find a file
Exact
Guillaume Bury 5c9161a691
 Add support for SMT-LIB's :global-declarations options (#269) 
* Add support for "global-declarations" options from SMT-LIB

* Only support global decls for SMT-LIB

* changes
2026-08-18 15:44:46 +02:00
.github/workflows Update ocaml compiler version in CI (#266) 2026-07-29 11:48:11 +02:00
doc Fix some small typos in the documentation 2026-02-12 13:32:38 +01:00
examples/extensions/abs_real feat: Add support for user-defined builtins with Dune plugins (#214) 2025-03-20 16:48:21 +01:00
src Add support for SMT-LIB's :global-declarations options (#269) 2026-08-18 15:44:46 +02:00
tests Add support for SMT-LIB's :global-declarations options (#269) 2026-08-18 15:44:46 +02:00
tools Fix evaluation of goals 2024-09-10 11:27:37 +02:00
.gitignore More uniformization 2021-03-26 10:10:10 +01:00
CHANGES.md Add support for SMT-LIB's :global-declarations options (#269) 2026-08-18 15:44:46 +02:00
dolmen.opam Try and fix Menhir tests (#255) 2026-02-17 16:37:36 +01:00
dolmen_bin.opam Upgrade deps (#231) 2025-03-18 16:35:10 +01:00
dolmen_loop.opam Smtlib Printer (#211) 2025-08-12 14:33:50 +01:00
dolmen_lsp.opam Bump linol to 0.10 (#241) 2025-08-05 13:54:37 +02:00
dolmen_model.opam Upgrade deps (#231) 2025-03-18 16:35:10 +01:00
dolmen_type.opam Upgrade deps (#231) 2025-03-18 16:35:10 +01:00
dune feat: Add support for user-defined builtins with Dune plugins (#214) 2025-03-20 16:48:21 +01:00
dune-project feat: Add support for user-defined builtins with Dune plugins (#214) 2025-03-20 16:48:21 +01:00
HACKING.md Try and fix Menhir tests (#255) 2026-02-17 16:37:36 +01:00
LICENSE Switched license to BSD 2016-04-29 16:01:49 +02:00
Makefile Try and fix Menhir tests (#255) 2026-02-17 16:37:36 +01:00
README.md Add ackowledgements to readme 2023-07-03 14:02:16 +02:00
TODO Smtlib Printer (#211) 2025-08-12 14:33:50 +01:00
VERSION prepare for v0.10 release 2024-06-14 18:32:58 +02:00

README.md

Dolmen build install

A library providing flexible parsers and typecheckers for languages used in automated deduction.

LICENSE

BSD2, see file LICENSE.

Documentation

Online documentation for the libraries can be found at http://gbury.github.io/dolmen. There is also a tutorial.

Installation

The main method of installation is to use opam. See this page for information about how to install opam on your system. Once you have installed and configured opam, you can use the following command to install the dolmen cli and lsp binaries:

opam install dolmen_bin dolmen_lsp

Additionally, pre-built binaries can be found on the release pages (starting from the v0.6 release for Linux and MacOS, and starting from the v0.8.1 release for Windows). You can get them on the latest release page.

The libraries can be installed using:

opam install dolmen dolmen_type dolmen_loop dolmen_model

Goals

The Dolmen project aims at providing an assortiment of tools to help handle languages that are used in automated deduction and formal logic.

More precisely, the Dolmen project provides:

  • A few OCaml libraries for:
  • A binary (which is using the above libraries), to parse and typecheck input files. This could be used to check a file against its language specification, and/or obtain detailed errors. See the bin doc
  • A LSP server so that the features of the above binary can also be used inside your favorite editor. See the dolmen lsp doc

Supported languages

Language Parsing Typing Model verification
ae (alt-ergo) ✔️ ✔️
dimacs ✔️ ✔️
iCNF ✔️ ✔️
smtlib ✔️ ✔️ ✔️
tptp ✔️ ✔️
zf (zipperposition) ✔️ ✔️

Acknowledgements

This work is currently in part funded by OCamlPro