issues
search
Gbury
/
dolmen
Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction
BSD 2-Clause "Simplified" License
80
stars
17
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Add VS Code config for the LSP
#173
hra687261
closed
1 year ago
7
Enforce invariants on bitvector size
#172
Gbury
closed
1 year ago
0
Bitvectors of size 0 should be forbidden
#171
bclement-ocp
closed
1 year ago
0
[RFC] Add support for the Model Checking Intermediate Language (MCIL)
#170
daniel-larraz
opened
1 year ago
5
Add an error for models of incremental problems
#169
Gbury
closed
1 year ago
0
Fix bvsdiv and fp.to_ubv fp.to_sbv
#168
bobot
closed
1 year ago
4
Fix windows CI
#167
Gbury
closed
1 year ago
0
Don't load all preludes if one of them is opened
#166
hra687261
closed
1 year ago
2
Propagate attributes from `Pack` Statements
#165
Gbury
closed
1 year ago
0
Fix issue #163
#164
Gbury
closed
1 year ago
0
Wrong check-model
#163
bobot
closed
1 year ago
0
Semantic triggers
#162
Halbaroth
closed
1 year ago
1
Added a test of AEs bv primitives
#161
hra687261
closed
1 year ago
0
Add support for prelude files
#160
bclement-ocp
closed
1 year ago
3
Additional builtins in the State?
#159
bclement-ocp
closed
1 year ago
1
Make the unknown logic fatal by default
#158
Gbury
closed
1 year ago
0
Add printing of type definitions in debug output
#157
Gbury
closed
1 year ago
0
Add convenience State.update and State.update_opt
#156
bclement-ocp
closed
1 year ago
2
Fix reason for reserved builtins
#155
Gbury
closed
1 year ago
0
Implement best mode for model verification
#154
Gbury
closed
1 year ago
0
[Draft] use algebraic number for reals
#153
bobot
opened
1 year ago
7
Build static binaries for releases
#152
Gbury
opened
1 year ago
2
Model fixes
#151
Gbury
closed
1 year ago
0
Unexpected Farith exception
#150
Gbury
closed
1 year ago
1
Unexpected exceptions with FP values
#149
Gbury
closed
1 year ago
5
Support hexadecimal reals in Alt-Ergo syntax
#148
bclement-ocp
closed
1 year ago
1
Re-enable support for "and" inside function/predicate
#147
bclement-ocp
closed
1 year ago
2
don't call dolmen_type 'dolmen_typecheck' in dolmen_type.opam
#146
bclement-ocp
closed
1 year ago
1
Incorrect parse of Alt-Ergo reals
#145
bclement-ocp
closed
1 year ago
0
Incorrect parse for Alt-Ergo language involving "and" token
#144
bclement-ocp
closed
1 year ago
1
Fix comparison of abstract array values
#143
Gbury
closed
1 year ago
0
Some more printing
#142
Gbury
closed
1 year ago
0
Ignore arith restriction in models
#141
Gbury
closed
1 year ago
0
Support check_sat statement for Alt-Ergo language
#140
Halbaroth
closed
1 year ago
2
Remove "error" as a reserved word in smtlib models
#139
Gbury
closed
1 year ago
0
Fix bug in model/bitv.ml
#138
Gbury
closed
1 year ago
1
Fix the support of the `in_interval` trigger in AE
#137
hra687261
closed
1 year ago
25
Support more Bit-Vector primitives in Alt-Ergo's native language
#136
hra687261
closed
1 year ago
2
Flow check + some windows fixes
#135
Gbury
closed
1 year ago
0
Ensure stable error codes
#134
Gbury
closed
1 year ago
0
Unchecked exit
#133
m-fleury
closed
1 year ago
4
Do not use octet and 'o' for memory size
#132
hansjoergschurr
closed
1 year ago
1
Add interleaved mode for model verification
#131
Gbury
closed
1 year ago
0
Add attributes on all decls/defs and properly attach them
#130
Gbury
closed
1 year ago
1
Add mutually recursive definition support for AE
#129
Halbaroth
closed
1 year ago
3
Workaround a bug in ocaml5.0 finalisers
#128
Gbury
closed
1 year ago
0
Some more CI tests
#127
Gbury
closed
1 year ago
0
CI updates
#126
Gbury
closed
1 year ago
0
A full mode for parsing from raw source
#125
Halbaroth
closed
1 year ago
1
CI tweaks
#124
Gbury
closed
1 year ago
0
Previous
Next