formalsec / smtml / 577

40%

Build Type

push

github

Committed by filipeom

Commit Message

Quantifer support and unification of API for creation of const/var

Adds quantifier support in cvc5 and bitwuzla. As well as, unifies the API
for creating symbols. In particular, we adopt the `const` API more
commonly used in SMT solvers to replace the ambiguous `symbol` API
which, with the introduction of `Symbol.make_var` and `Typed.var`,
no longer made sense. In summary, API changes are summarised below:

symbol.ml:

- create: Ty.t -> name -> namespace -> t        (was make3)
- make_const: Ty.t -> string -> t               (was make)
- make_var: Ty.t -> string -> t                 (new)
- make: deprecated alias for make_const

typed.ml:

- const: 'a ty -> string -> 'a expr             (was symbol)
- var: 'a ty -> string -> 'a expr               (new)
- symbol: deprecated alias for const

BREAKING CHANGE: Creation of symbols now uses const/var convention

Coverage Stats

8 of 26 new or added lines in 7 files covered. (30.77%)

109 existing lines in 2 files now uncovered.

2450 of 6060 relevant lines covered (40.43%)

35.75 hits per line