-
Notifications
You must be signed in to change notification settings - Fork 16
Open
Description
From the recent 2.6 SMT-LIB Standard sections 1.1.1 - 1.1.4, the following commands are missing:
- define-fun-rec
- define-funs-rec
- get-unsat-assumptions
- declare-datatype
- declare-datatypes
The current implementation of generalized quantifiers in OpenJML utilize the define-fun-rec command. For older solvers, this command can be implemented as a series of declare-fun and assert forall commands. It is still useful to have the new commands as some solvers can perform additional optimizations.
Metadata
Metadata
Assignees
Labels
No labels