gbury/dolmen issues and pull requests

#223 - Documentation page is missing the latest version

Issue - State: open - Opened by TDacik 18 days ago - 3 comments

#222 - Too restrictive well foundness criteria

Issue - State: open - Opened by bobot about 1 month ago - 13 comments

#221 - fix: Add missing model for `to_int` coercion

Pull Request - State: closed - Opened by bclement-ocp 2 months ago - 1 comment

#220 - feat: Support more Alt-Ergo primitives

Pull Request - State: open - Opened by bclement-ocp 2 months ago - 2 comments

#219 - [TEST] Trying out to build static binaries in CI

Pull Request - State: open - Opened by Gbury 4 months ago

#218 - Support custom printer for typing errors

Issue - State: open - Opened by Halbaroth 5 months ago

#217 - Support for custom attributes

Issue - State: closed - Opened by Halbaroth 5 months ago - 1 comment

#216 - Support for `get-assignment`

Issue - State: open - Opened by bclement-ocp 6 months ago - 2 comments

#215 - Confusing error message with pattern matching on polymorphic type in ae's native language

Issue - State: open - Opened by Gbury 6 months ago
Labels: enhancement

#214 - feat: Add support for user-defined builtins with Dune plugins

Pull Request - State: open - Opened by bclement-ocp 7 months ago - 5 comments

#213 - Can we get a formal 1.0 release please

Issue - State: open - Opened by rod-chapman 7 months ago - 7 comments

#212 - RDL check is a bit too lenient

Issue - State: open - Opened by Gbury 7 months ago - 1 comment
Labels: bug, spec

#211 - Smtlib Printer

Pull Request - State: open - Opened by Gbury 8 months ago - 1 comment

#210 - Fix attributes in nested binders

Pull Request - State: closed - Opened by Gbury 8 months ago

#209 - Attributes in nested quantifiers

Issue - State: closed - Opened by bclement-ocp 9 months ago - 2 comments

#208 - Add typing extensions, and the bvconv extension

Pull Request - State: closed - Opened by Gbury 9 months ago - 1 comment

#207 - Add warning for unknown attribute

Pull Request - State: closed - Opened by Gbury 9 months ago

#206 - Support `bv2nat` as a "relaxed mode"

Issue - State: closed - Opened by hansjoergschurr 9 months ago - 2 comments

#205 - Question regarding BV logic in SMT files

Issue - State: closed - Opened by rod-chapman 9 months ago - 14 comments

#204 - [WIP] Add Tptp v8.2

Pull Request - State: open - Opened by Gbury 10 months ago

#203 - Supporting evaluation for custom functions

Issue - State: open - Opened by Halbaroth 10 months ago - 5 comments
Labels: new feature

#202 - Handling abstract values in `(get-value)` statements

Issue - State: closed - Opened by Halbaroth 11 months ago - 8 comments
Labels: new feature

#201 - Add full mode stdin parsing

Pull Request - State: closed - Opened by Gbury about 1 year ago

#200 - Support non-incremental parsing from stdin

Issue - State: closed - Opened by bclement-ocp about 1 year ago - 1 comment

#199 - Add proper support for `:named` smtlib annotations

Pull Request - State: closed - Opened by Gbury about 1 year ago

#198 - Quoted symbols and printing for smtlib-related languages

Pull Request - State: closed - Opened by Gbury about 1 year ago

#197 - Warning regarding the `dolmen_type` file

Issue - State: closed - Opened by Halbaroth about 1 year ago - 2 comments

#196 - Quoted identifiers can be keywords

Issue - State: closed - Opened by bclement-ocp about 1 year ago - 12 comments
Labels: bug

#195 - 4.08 support broken (`List.concat_map`)

Issue - State: closed - Opened by bclement-ocp about 1 year ago - 10 comments

#194 - Also add statement extensions to psmt2 (following #190)

Pull Request - State: closed - Opened by Gbury about 1 year ago

#193 - More information for reserved id, and adjusted errors

Pull Request - State: closed - Opened by Gbury about 1 year ago

#192 - Ensure invalid chars always raise Error during lexing

Pull Request - State: closed - Opened by Gbury about 1 year ago

#191 - Uncaught exception on buggy file

Issue - State: closed - Opened by Stevendeo about 1 year ago
Labels: bug

#190 - Add language extensions in the parsing of smtlib2

Pull Request - State: closed - Opened by Gbury about 1 year ago - 1 comment

#189 - DIMACS variables do not appear as decls

Issue - State: closed - Opened by bclement-ocp about 1 year ago - 1 comment
Labels: new feature

#188 - Check sat assuming

Issue - State: closed - Opened by Stevendeo about 1 year ago - 2 comments

#187 - Handling of named terms

Issue - State: closed - Opened by Stevendeo about 1 year ago - 2 comments
Labels: bug

#186 - Handling of `set-option :global-declarations`

Issue - State: open - Opened by Stevendeo about 1 year ago
Labels: bug

#185 - Reject names starting with `@` and `.` outside of models

Issue - State: closed - Opened by bclement-ocp about 1 year ago
Labels: bug

#184 - Refine some arithmetic error/warning messages

Pull Request - State: closed - Opened by Gbury about 1 year ago

#183 - Spec errors on the difference logic benchmarks of the SMT-LIB

Issue - State: closed - Opened by hra687261 about 1 year ago - 2 comments

#182 - Add the String theory to the `ALL` logic of SMT-LIB

Pull Request - State: closed - Opened by hra687261 about 1 year ago - 2 comments

#181 - Run `realpath` on the paths of LSP prelude files

Pull Request - State: closed - Opened by hra687261 about 1 year ago - 5 comments

#180 - Unclear error message during model checking

Issue - State: open - Opened by Halbaroth over 1 year ago - 7 comments
Labels: enhancement, new feature

#179 - Add authors files

Issue - State: open - Opened by Gbury over 1 year ago
Labels: enhancement

#178 - Support Alt-Ergo's `cut` and `check`

Issue - State: closed - Opened by bclement-ocp over 1 year ago - 15 comments
Labels: new feature

#177 - Better interface for with_cache + expose it

Pull Request - State: closed - Opened by Gbury over 1 year ago

#176 - Expose `with_cache`?

Issue - State: closed - Opened by bclement-ocp over 1 year ago - 1 comment
Labels: enhancement

#175 - More checks on bitvector size for extract

Pull Request - State: closed - Opened by Gbury over 1 year ago

#174 - Ill-typed statement on Bitvector is accepted by Dolmen

Issue - State: closed - Opened by Halbaroth over 1 year ago - 1 comment
Labels: bug

#173 - Add VS Code config for the LSP

Pull Request - State: closed - Opened by hra687261 over 1 year ago - 7 comments

#172 - Enforce invariants on bitvector size

Pull Request - State: closed - Opened by Gbury over 1 year ago

#171 - Bitvectors of size 0 should be forbidden

Issue - State: closed - Opened by bclement-ocp over 1 year ago

#170 - [RFC] Add support for the Model Checking Intermediate Language (MCIL)

Pull Request - State: open - Opened by daniel-larraz over 1 year ago - 5 comments

#169 - Add an error for models of incremental problems

Pull Request - State: closed - Opened by Gbury over 1 year ago

#168 - Fix bvsdiv and fp.to_ubv fp.to_sbv

Pull Request - State: closed - Opened by bobot over 1 year ago - 4 comments

#167 - Fix windows CI

Pull Request - State: closed - Opened by Gbury over 1 year ago

#166 - Don't load all preludes if one of them is opened

Pull Request - State: closed - Opened by hra687261 over 1 year ago - 2 comments

#165 - Propagate attributes from `Pack` Statements

Pull Request - State: closed - Opened by Gbury over 1 year ago

#164 - Fix issue #163

Pull Request - State: closed - Opened by Gbury over 1 year ago

#163 - Wrong check-model

Issue - State: closed - Opened by bobot over 1 year ago

#162 - Semantic triggers

Pull Request - State: closed - Opened by Halbaroth over 1 year ago - 1 comment

#161 - Added a test of AEs bv primitives

Pull Request - State: closed - Opened by hra687261 over 1 year ago

#160 - Add support for prelude files

Pull Request - State: closed - Opened by bclement-ocp over 1 year ago - 3 comments

#159 - Additional builtins in the State?

Issue - State: closed - Opened by bclement-ocp over 1 year ago - 1 comment

#158 - Make the unknown logic fatal by default

Pull Request - State: closed - Opened by Gbury over 1 year ago

#157 - Add printing of type definitions in debug output

Pull Request - State: closed - Opened by Gbury over 1 year ago
Labels: enhancement

#156 - Add convenience State.update and State.update_opt

Pull Request - State: closed - Opened by bclement-ocp over 1 year ago - 2 comments
Labels: enhancement

#155 - Fix reason for reserved builtins

Pull Request - State: closed - Opened by Gbury over 1 year ago
Labels: bugfix

#154 - Implement best mode for model verification

Pull Request - State: closed - Opened by Gbury over 1 year ago
Labels: enhancement

#153 - [Draft] use algebraic number for reals

Pull Request - State: open - Opened by bobot over 1 year ago - 7 comments
Labels: enhancement

#152 - Build static binaries for releases

Issue - State: open - Opened by Gbury over 1 year ago - 2 comments
Labels: enhancement

#151 - Model fixes

Pull Request - State: closed - Opened by Gbury over 1 year ago

#150 - Unexpected Farith exception

Issue - State: closed - Opened by Gbury over 1 year ago - 1 comment

#149 - Unexpected exceptions with FP values

Issue - State: closed - Opened by Gbury over 1 year ago - 5 comments
Labels: bug

#148 - Support hexadecimal reals in Alt-Ergo syntax

Pull Request - State: closed - Opened by bclement-ocp over 1 year ago - 1 comment

#147 - Re-enable support for "and" inside function/predicate

Pull Request - State: closed - Opened by bclement-ocp over 1 year ago - 2 comments

#146 - don't call dolmen_type 'dolmen_typecheck' in dolmen_type.opam

Pull Request - State: closed - Opened by bclement-ocp over 1 year ago - 1 comment

#145 - Incorrect parse of Alt-Ergo reals

Issue - State: closed - Opened by bclement-ocp over 1 year ago
Labels: bug

#144 - Incorrect parse for Alt-Ergo language involving "and" token

Issue - State: closed - Opened by bclement-ocp over 1 year ago - 1 comment
Labels: bug

#143 - Fix comparison of abstract array values

Pull Request - State: closed - Opened by Gbury over 1 year ago
Labels: bugfix

#142 - Some more printing

Pull Request - State: closed - Opened by Gbury over 1 year ago
Labels: enhancement

#141 - Ignore arith restriction in models

Pull Request - State: closed - Opened by Gbury over 1 year ago
Labels: bugfix

#140 - Support check_sat statement for Alt-Ergo language

Pull Request - State: closed - Opened by Halbaroth over 1 year ago - 2 comments
Labels: new feature

#139 - Remove "error" as a reserved word in smtlib models

Pull Request - State: closed - Opened by Gbury over 1 year ago
Labels: bugfix

#138 - Fix bug in model/bitv.ml

Pull Request - State: closed - Opened by Gbury over 1 year ago - 1 comment

#137 - Fix the support of the `in_interval` trigger in AE

Pull Request - State: closed - Opened by hra687261 over 1 year ago - 25 comments
Labels: bugfix

#136 - Support more Bit-Vector primitives in Alt-Ergo's native language

Pull Request - State: closed - Opened by hra687261 over 1 year ago - 2 comments
Labels: new feature

#135 - Flow check + some windows fixes

Pull Request - State: closed - Opened by Gbury over 1 year ago

#134 - Ensure stable error codes

Pull Request - State: closed - Opened by Gbury over 1 year ago

#133 - Unchecked exit

Issue - State: closed - Opened by m-fleury over 1 year ago - 4 comments

#132 - Do not use octet and 'o' for memory size

Pull Request - State: closed - Opened by hansjoergschurr over 1 year ago - 1 comment

#131 - Add interleaved mode for model verification

Pull Request - State: closed - Opened by Gbury almost 2 years ago

#115 - Add progress bars

Pull Request - State: open - Opened by Gbury almost 2 years ago
Labels: new feature

#104 - Added tags to predicates to differentiate them from functions in Alt-Ergo's logic

Pull Request - State: closed - Opened by hra687261 about 2 years ago

#103 - Memory leaks during Model Checking?

Issue - State: closed - Opened by bobot over 2 years ago - 14 comments
Labels: bug

#102 - Allow `(error ...)` in smtlib2 response files

Pull Request - State: closed - Opened by Gbury over 2 years ago

#101 - Add an option to force the smtlib2 logic

Pull Request - State: closed - Opened by Gbury over 2 years ago - 1 comment

#100 - Add fp.rem, fp.toIntegral fp.to_ubv, fp.to_sbv, fp.min, fp.max

Pull Request - State: closed - Opened by bobot over 2 years ago - 10 comments

#99 - Add support for evaluating `bvsub`

Pull Request - State: closed - Opened by 4tXJ7f over 2 years ago - 1 comment

GitHub / gbury/dolmen issues and pull requests