Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
|
|
|
|
The build system (cmake) will automatically generate an export header
cvc4_export.h, which makes sure that the correct export features are
defined depending on the compiler and target platform. The macro CVC4_EXPORT
replaces CVC4_PUBLIC and its usage is reduced by 2/3.
Co-authored-by: Gereon Kremer <nafur42@gmail.com>
|
|
|
|
This PR removes subtyping for sets theory due to issues like #4502, #4507 and #4631.
Changes:
Add SingletonOp for singletons to specify the type of the single element in the set.
Add mkSingleton to the solver to enable the user to pass the sort of the single element.
Update smt and cvc parsers to use mkSingleton when the kind is SINGLETON
|
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback