gbury/dolmen issues and pull requests

#98 - [WIP] [Model] Handle definition of constants in smt2 file

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

#97 - Add FP to model

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

#96 - Model add Int, Real, Bitvector

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

#95 - [WIP] Model verification using Dolmen

Pull Request - State: closed - Opened by Gbury almost 3 years ago - 8 comments

#94 - bv2nat is not recognized

Issue - State: closed - Opened by yannickmoy almost 3 years ago - 7 comments
Labels: spec

#93 - Fix asserts in smtlib parsers

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

#92 - fix LSP config for neovim's builtin LSP

Pull Request - State: closed - Opened by c-cube almost 3 years ago - 1 comment

#91 - Use menhir's code backend

Pull Request - State: closed - Opened by Gbury almost 3 years ago - 1 comment

#90 - [Bitv] add the size of the bitvectors in the builtins

Pull Request - State: closed - Opened by bobot almost 3 years ago - 5 comments

#89 - Complete and fix alt-ergo's native language typing

Pull Request - State: closed - Opened by hra687261 almost 3 years ago - 1 comment

#88 - Add source code snippet printing for errors and warnings

Pull Request - State: closed - Opened by Gbury about 3 years ago

#87 - Add support for Alt-Ergo's built-ins

Pull Request - State: closed - Opened by hra687261 about 3 years ago - 15 comments

#86 - Support LSP's textDocument/definition

Issue - State: open - Opened by krobelus about 3 years ago - 1 comment
Labels: enhancement

#85 - [Pipeline] Don't print the backtrace directly

Pull Request - State: closed - Opened by bobot about 3 years ago - 4 comments

#84 - Allow users to control severity of warnings

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

#83 - Comments for suppression

Issue - State: closed - Opened by aytey over 3 years ago - 4 comments
Labels: enhancement

#82 - Add warning for multiple set-logics

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

#81 - Add hint about missing theory for unbound literals

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

#80 - Fixed handling of reset/reset-assertions

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

#79 - Remove float and extended bitv literals from FP theory

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

#78 - Dolmen "stops" at the first error

Issue - State: open - Opened by aytey over 3 years ago - 1 comment
Labels: enhancement

#77 - Parse error with `let`

Issue - State: closed - Opened by aytey over 3 years ago - 4 comments
Labels: enhancement

#76 - No warning when no quantifiers are used in quantified logic

Issue - State: open - Opened by mpreiner over 3 years ago - 4 comments
Labels: enhancement

#75 - Last `set-logic` "wins"

Issue - State: closed - Opened by aytey over 3 years ago - 6 comments
Labels: enhancement

#74 - False positive on `QF_BVFPLRA`

Issue - State: closed - Opened by aytey over 3 years ago - 4 comments
Labels: bug

#71 - Custom Trie implem for strings + Better abstraction for naming things

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

#70 - Fixes to_int

Pull Request - State: closed - Opened by bobot over 3 years ago - 4 comments

#67 - CI doesn't test 4.08

Issue - State: closed - Opened by c-cube over 3 years ago - 7 comments

#66 - Add higher-order type-checking to Dolmen

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

#65 - Let dolmen fix that for you

Issue - State: open - Opened by Gbury over 3 years ago - 5 comments
Labels: enhancement

#64 - SMT-LIB: print symbols with `|`

Issue - State: open - Opened by hansjoergschurr over 3 years ago - 3 comments
Labels: enhancement

#63 - Correctly handle parallel let-bindings

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

#62 - Better CI

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

#61 - Stricter typing of smtlib builtins

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

#60 - vendor linol

Pull Request - State: closed - Opened by c-cube over 3 years ago - 2 comments

#59 - Fix lexing of quoted symbols for smtlib 2.6 and poly

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

#58 - SMT-LIB: quoted symbols ar treated as distinct symbols

Issue - State: closed - Opened by hansjoergschurr over 3 years ago - 1 comment

#57 - SMT-LIB: dolmen fails to recognize `and` with only one argument

Issue - State: closed - Opened by hansjoergschurr over 3 years ago - 4 comments

#56 - Make files re-parsables

Pull Request - State: closed - Opened by Gbury about 4 years ago

#55 - Fix bad interaction between global state and def theory

Pull Request - State: closed - Opened by Gbury about 4 years ago

#54 - Reparsing a file and `Dolmen.Std.Loc.table`

Issue - State: closed - Opened by bobot about 4 years ago - 4 comments

#53 - [RFC] Add polymorphism of smt v3 in smt v2.6

Pull Request - State: closed - Opened by bobot about 4 years ago - 44 comments

#52 - error message for syntax

Pull Request - State: closed - Opened by c-cube about 4 years ago - 7 comments

#51 - Complete rework of restrictions and filters

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

#50 - Add some automaton flow constraints checks for SMTLIB

Issue - State: closed - Opened by Gbury over 4 years ago - 4 comments
Labels: enhancement

#49 - Superformats of dimacs: qdimacs and dqdimacs

Issue - State: open - Opened by hansjoergschurr over 4 years ago
Labels: enhancement

#48 - Smtlib v3

Issue - State: open - Opened by bobot over 4 years ago - 4 comments
Labels: enhancement

#47 - Parse smtlib2 destructors in the term namespace

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

#46 - Destructor for datatypes missing in environment

Issue - State: closed - Opened by bobot over 4 years ago - 2 comments

#45 - Why3 as input language

Issue - State: closed - Opened by bobot over 4 years ago - 4 comments

#44 - Fixes from COLIBRI

Pull Request - State: closed - Opened by bobot over 4 years ago - 8 comments

#43 - SMTLIB's FP theory might require Reals/Reals_Ints and BV

Issue - State: closed - Opened by Gbury over 4 years ago - 3 comments
Labels: spec

#42 - Datatype theory seems to be builtin and always present

Issue - State: closed - Opened by Gbury over 4 years ago - 4 comments

#41 - Dolmen's Typechecker is sometimes too smart for the SMTLIB

Issue - State: open - Opened by Gbury over 4 years ago
Labels: enhancement

#40 - Vendor dependencies (optionally) to allow opam-less installation

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

#39 - Fix bitv parsing

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

#38 - Bitvector `bv%i` is broken

Issue - State: closed - Opened by bobot over 4 years ago - 7 comments

#37 - SMTLIB refuses redefinition or redeclaration

Issue - State: closed - Opened by bobot over 4 years ago - 9 comments

#36 - Implement UF/DT theory restrictions

Pull Request - State: closed - Opened by Gbury over 4 years ago - 5 comments

#35 - Term_def gives the expr id given to the defined symbol

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

#34 - [smtlib_logic] Parse part by part instead of globally

Pull Request - State: closed - Opened by bobot over 4 years ago - 8 comments

#33 - [Pipes] return all the possible statements

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

#32 - Interface of Pipes

Issue - State: closed - Opened by bobot over 4 years ago - 3 comments

#31 - Fixes #28

Pull Request - State: closed - Opened by bobot over 4 years ago - 8 comments

#30 - Substitute type defs during type-checking

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

#29 - `Define-sort` not supported

Issue - State: closed - Opened by bobot over 4 years ago - 2 comments

#28 - Adding FP Library of the SMTLIB

Issue - State: closed - Opened by bobot over 4 years ago - 10 comments

#27 - Fix issue 26

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

#26 - smtlib parsing: assertion hit when parsing wrongly typed equation

Issue - State: closed - Opened by quicquid over 4 years ago - 1 comment

#25 - Try and handle all smtlib2 logics

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

#24 - smtlib parser: :named annotations lead to warnings

Issue - State: closed - Opened by quicquid over 4 years ago - 2 comments

#23 - Add up-to-date tptp parser

Issue - State: open - Opened by Gbury over 4 years ago
Labels: enhancement

#22 - Setup testing over all of tptp/smtlib libraries

Issue - State: open - Opened by Gbury over 4 years ago - 3 comments

#21 - Catch-all exceptions in lsp handler

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

#20 - Correctly handle tptp's THF

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

#19 - smtlib parser: Unknown logic UF

Issue - State: closed - Opened by quicquid over 4 years ago - 20 comments

#18 - Add versioned parser for languages

Pull Request - State: closed - Opened by Gbury almost 5 years ago - 3 comments

#17 - Compilation error

Issue - State: closed - Opened by Gbury about 5 years ago - 1 comment
Labels: bug

#16 - Files missing while installing on Mac OS

Issue - State: closed - Opened by elhaddadyacine over 5 years ago - 3 comments

#15 - Incomplete dependencies

Issue - State: closed - Opened by Gbury over 5 years ago - 1 comment
Labels: bug

#14 - Printer for terms

Pull Request - State: closed - Opened by Gbury about 6 years ago - 21 comments

#13 - Replace ocamlbuild with dune: First try

Pull Request - State: closed - Opened by Gbury about 6 years ago - 26 comments

#12 - Switch to dune ?

Issue - State: closed - Opened by Gbury about 6 years ago - 8 comments

#11 - Normalize

Pull Request - State: closed - Opened by Gbury about 6 years ago

#10 - Smtlib function def typo

Pull Request - State: closed - Opened by Gbury about 6 years ago

#9 - Typo in smtlib grammar

Issue - State: closed - Opened by anmaped about 6 years ago - 4 comments

#8 - Term printers

Issue - State: open - Opened by Gbury about 6 years ago - 7 comments
Labels: enhancement, help wanted

#7 - Term normalizer

Issue - State: closed - Opened by Gbury about 6 years ago
Labels: enhancement

#6 - Constructing smtlib set_info

Issue - State: closed - Opened by anmaped about 6 years ago - 5 comments

#5 - Ast_smtlib missing in mlpack

Issue - State: closed - Opened by anmaped about 6 years ago - 3 comments

#4 - Typechecking: first try

Pull Request - State: closed - Opened by Gbury over 6 years ago - 7 comments

#3 - update parsing of SMTlib to version 2.6 for constructs required by SL…

Pull Request - State: closed - Opened by mihasighi over 6 years ago - 12 comments

#2 - Let-bindings in smtlib and equality

Issue - State: closed - Opened by Gbury almost 7 years ago - 6 comments

#1 - document shape of terms

Issue - State: closed - Opened by c-cube almost 7 years ago - 3 comments

GitHub / gbury/dolmen issues and pull requests