5 Commits

Author	SHA1	Message	Date
Mathias Preiner	d01e59c13b	Update copyright headers for release 1.0 (#8539)	2022-04-05 20:38:57 +00:00
Mathias Preiner	bbcd471ed4	Introduce internal namespace and remove api namespace. (#8443) ... The public cvc5 API now lives in the cvc5 namespace. All internal parts were moved into the (new) internal namespace. The final hierarchy will be as follows: cvc5 ~~ public API ::context ::internal ::parser ::main After this PR it will be: cvc5 ~~ public API ::internal ::context ::main ::parser	2022-03-29 23:23:01 +00:00
Mathias Preiner	cc808da53d	api: Unify mkOp variants. (#8369) ... Co-authored-by: Gereon Kremer <nafur42@gmail.com>	2022-03-25 23:57:10 +00:00
Andrew Reynolds	2f1483e2e3	Remove unecessary methods from the API (#8260) ... Removes checkEntailed from Solver. Removes isEntailed, isNotEntailed, isEntailedUnknown from Result. Removes isSubsortOf, isFunctionLike, getUninterpretedSortName, getSortConstructorName from Sort. Updates examples and unit tests.	2022-03-14 18:29:30 +00:00
yoni206	ad885db118	Integrate new int-blaster (#7781) ... This PR removes the code that translates from bit-vectors to integers from the bv_to_int preprocessing pass, and replaces it with a call to the IntBlaster module. Tests are updated and added, as well as other minor changes. Solves the following issues (and contains corresponding tests): cvc5/cvc5-projects#345 cvc5/cvc5-projects#344 cvc5/cvc5-projects#343 @mpreiner FYI	2021-12-13 16:16:08 +00:00