dolmen
forked from gbury/dolmen
Star 1
Fork 0
Watch

Version history of src/standard/expr.ml

October 2026

Hichem R. A.
Separate rounding modes into their own type (#271)
committed

August 2025

Guillaume Bury
Smtlib Printer (#211)
committed
Guillaume Bury
Hierarchical builtins (#240)
committed

May 2025

Guillaume Bury
Fixes for model validation in smt2.7
committed

April 2025

Guillaume Bury
Support for SMT-LIB 2.7 (#235)
committed

March 2024

Guillaume Bury
Fix attributes in nested binders (#210)
committed
Guillaume Bury
Add typing extensions, and the bvconv extension (#208)
committed

November 2023

Guillaume Bury
Keep only one implemenation of List.concat_map
committed

September 2023

Guillaume Bury
Better interface for with_cache + expose it (#177)
committed

July 2023

Guillaume Bury
More checks on bitvector size for extract
committed
Guillaume Bury
Enforce constraints on bitvectors indexes
committed

June 2023

François Bobot
Fix bvsdiv and fp.to_ubv fp.to_sbv (#168)
committed
Pierre Villemot
Proper handling of in_interval and bounds in triggers
committed
Guillaume Bury
Add printing of type definitions in debug output (#157)
committed

May 2023

Guillaume Bury
Model fixes (#151)
committed

January 2023

Guillaume Bury
Multliple fixes for recursive definitions (#123)
committed

October 2022

Hichem R. A
Expose Term Consts (#112)
committed

September 2022

Hichem R. A
Added tags to predicates to differentiate them from functions in Alt-Ergo's logic (#104)
committed

July 2022

Guillaume Bury
Remove unneeded builtin for div/mod by zero
committed

June 2022

Guillaume Bury
Better handling of corner cases in models + adjusted err/warn messages
committed
François Bobot
Model add Int, Real, Bitvector (#96)
committed
Guillaume Bury
Working first prototype
committed
Hichem R. A
Complete and fix alt-ergo's native language typing (#89)
committed

February 2022

François Bobot
[Bitv] add the size of the bitvectors in the builtins (#90)
committed

November 2021

HRA
Add support for Alt-Ergo's built-ins (#87)
committed

May 2021

Guillaume Bury
Add abstraction for Names and Paths
committed
François Bobot
Fixes to_int (#70)
committed
Guillaume Bury
Avoid infinite lookup loops in arith check
committed

April 2021

Guillaume Bury
Avoid exponential explosion whe handling let binders
committed
Guillaume Bury
Solve perf problems with inferred types
committed
Guillaume Bury
Some more fixes
committed
Guillaume Bury
Various fixes
committed
Guillaume Bury
Fix inference problems for tptp
committed
Guillaume Bury
Add higher-order type-checking to Dolmen (#66)
committed
Guillaume Bury
Correctly handle parallel let-bindings (#63)
committed

October 2020

Guillaume Bury
Fix use of substitution in pattern matching
committed

July 2020

Guillaume Bury
Optimize polymorphic inference
committed
Guillaume Bury
Optimize lookups, using maps instead of spelll indexes
committed
Guillaume Bury
Add String theory
committed
Guillaume Bury
Properly handle ADTs in SMTLIBv2.6
committed
Guillaume Bury
Complete rework of restrictions and filters (#51)
committed

June 2020

François Bobot
Fixes from COLIBRI (#44)
committed

May 2020

Guillaume Bury
Fix handling of let-bindings and a filter typo for RDL
committed
Guillaume Bury
Small printing fix
committed
Guillaume Bury
Better filters and some fixes for SMTLIB2 typing
committed
Guillaume Bury
Lots of fixes + reworked arith filters
committed
Guillaume Bury
Fix linear arith filter + add hint
committed
Guillaume Bury
Lots of bug fixes
committed
Guillaume Bury
More tests and small fixes
committed
Guillaume Bury
Fix typo + Bad_cstr_arity error
committed