dolmen
forked from gbury/dolmen
Star 1
Fork 0
Watch

Commits on master

Hichem R. A.
Separate rounding modes into their own type (#271)
committed
Hichem R. A.
Rename macOS release asset from amd64 to arm64
committed
Guillaume Bury
Add support for SMT-LIB's :global-declarations options (#269)
committed
Guillaume Bury
promote tests
committed
Guillaume Bury
Fix printing of type annotation for poly ho maps
committed
Guillaume Bury
Implement 'dumb' polymophism for SMT-LIB + various HO fixes (#268)
committed
Guillaume Bury
Emit less `exit` statements, notably for preludes (#263)
committed
Guillaume Bury
More precise error for lexing errors (#265)
committed
Guillaume Bury
Split HO into a separate builtin theory for typechecking (#267)
committed
Guillaume Bury
Update ocaml compiler version in CI (#266)
committed
Guillaume Bury
better error message
committed
Guillaume Bury
small cleanup
committed
Guillaume Bury
Fix one assertion
committed
Guillaume Bury
Properly recurse in logic detection
committed
Guillaume Bury
Add Integer exponentiation (#259)
committed
Guillaume Bury
Correctly handle smt2.7 map application syntactic sugar in annotations (#258)
committed
Guillaume Bury
Try and fix Menhir tests (#255)
committed
Guillaume Bury
Fixes for implicit type vars and datatype decls in smt-lib
committed
filipeom.tngl.sh
Fix some small typos in the documentation
committed
Guillaume Bury
Add upper bound on menhir
committed
Basile Clément
Add uutf as a dependency to dolmen
committed
Guillaume Bury
changes
committed
Basile Clément
Support SMT-LIB v2.7 bit-vector operators in psmt2
committed
Guillaume Bury
Prevent overlapping of parameters in def-fun in SMT-LIB (#247)
committed
Guillaume Bury
changes for PR#246
committed
Guillaume Bury
Reject overlapping parallel bindings (#246)
committed
Guillaume Bury
Smtlib Printer (#211)
committed
Guillaume Bury
changes
committed
Guillaume Bury
Reject SMT-LIB2 distinct applications to less than 2 arguments (#243)
committed
Guillaume Bury
changes
committed
Guillaume Bury
Hierarchical builtins (#240)
committed
stepbrobd.com
Bump linol to 0.10 (#241)
committed
Guillaume Bury
Consider Fake_apply indirection in the arith check for smt2.7 (#238)
committed
Guillaume Bury
Fixes for model validation in smt2.7
committed
Guillaume Bury
Add some tests for the ADT well-foundedness check
committed
Guillaume Bury
Support for SMT-LIB 2.7 (#235)
committed
Guillaume Bury
Fix bad error message (#234)
committed
Basile Clément
feat: Add support for user-defined builtins with Dune plugins (#214)
committed
Basile Clément
Fix doc of `-w` / `--warn` to match what the code actually does
committed
Basile Clément
feat: Support more Alt-Ergo primitives (#220)
committed
Guillaume Bury
Upgrade deps (#231)
committed
Guillaume Bury
changes
committed
Guillaume Bury
Fix broken `Loc.compact` function
committed
Guillaume Bury
Update setup-ocaml version for CI (#230)
committed
Basile Clément
fix: Add missing model for `to_int` coercion (#221)
committed
Guillaume Bury
Fix evaluation of goals
committed
Guillaume Bury
Update ocaml versions in CI scripts
committed
Guillaume Bury
Add lower bounds on qcheck and mdx
committed
Guillaume Bury
prepare for v0.10 release
committed
Guillaume Bury
Fix attributes in nested binders (#210)
committed
Guillaume Bury
Add warning for unknown attribute (#207)
committed
Guillaume Bury
Add typing extensions, and the bvconv extension (#208)
committed
Guillaume Bury
Add full mode stdin parsing (#201)
committed
Guillaume Bury
Add proper support for `:named` smtlib annotations (#199)
committed
Guillaume Bury
Some more doc in HACKING.md
committed
Guillaume Bury
Quoted symbols and printing for smtlib-related languages (#198)
committed
Guillaume Bury
Fix opam warning about synopsis
committed
Guillaume Bury
Keep only one implemenation of List.concat_map
committed
Guillaume Bury
Fix synopsis
committed
Guillaume Bury
Minor patch for 4.08 compat
committed