ada/cvc5

Fork 0

mirror of https://github.com/AdaCore/cvc5.git synced 2026-02-12 12:32:16 -08:00

Commit Graph

Author	SHA1	Message	Date
Aina Niemetz	7a4a17b193	c api: Introduce C/C++ specific handling of public enums. (#9915 ) This introduces a general way to use public enums both in the C++ and the (upcoming) C API. For the C++ case, we now use enum classes rather than enums for public enums. This also includes definitions for C API to_string conversions for public enums. C API definitions in cvc5_types.h are only included from the C API, guarded via a macro (thus, for now, not included yet when the header is included).	2023-08-22 18:17:16 +00:00
Aina Niemetz	0a8baa0f0a	Update copyright headers. (#9736 )	2023-05-09 18:06:18 +00:00
Andrew Reynolds	9aa2050e3e	Fix cases of abduction and interpolation where conjecture is not available (#9615 ) Fixes cvc5/cvc5-projects#567. Fixes cvc5/cvc5-projects#571. Both issues involved calling the subsolver in a way where the synthesis conjecture was not properly registered.	2023-03-28 19:28:29 +00:00

Author

SHA1

Message

Date

Aina Niemetz

7a4a17b193

c api: Introduce C/C++ specific handling of public enums. (#9915 )

This introduces a general way to use public enums both in the C++ and
the (upcoming) C API. For the C++ case, we now use enum classes rather
than enums for public enums. This also includes definitions for
C API to_string conversions for public enums. C API definitions in
cvc5_types.h are only included from the C API, guarded via a macro
(thus, for now, not included yet when the header is included).

2023-08-22 18:17:16 +00:00

Aina Niemetz

0a8baa0f0a

Update copyright headers. (#9736 )

2023-05-09 18:06:18 +00:00

Andrew Reynolds

9aa2050e3e

Fix cases of abduction and interpolation where conjecture is not available (#9615 )

Fixes cvc5/cvc5-projects#567.
Fixes cvc5/cvc5-projects#571.

Both issues involved calling the subsolver in a way where the synthesis conjecture was not properly registered.

2023-03-28 19:28:29 +00:00

3 Commits