11 Commits

Author SHA1 Message Date
Aina Niemetz
0647c4c107 Update copyright headers. (#11561)
Co-authored-by: Daniel Larraz <daniel-larraz@users.noreply.github.com>
2025-01-23 17:54:20 +00:00
Andrew Reynolds
ad76979329 Disable support for experimental theories when safe-options is set (#11162)
This adds options that guard the usage of "experimental" theories or
extensions thereof when `--safe-options` is enabled.

This includes bags, finite fields, separation logic, higher-order logic,
and extensions of arithmetic (including transcendentals, iand and pow2).

The options `--sets-exp` (renamed from `--sets-ext` in this PR) and
`--fp-exp` continue to be disabled by default, thus do not need to
change.

Similar to other expert options, these theories can still be used with
`safe-options` if they are enabled prior to setting `safe-options`, e.g.
`--ho-exp --safe-options ...` allows HOL to be used. The options
configuration will only override the setting of `*-exp` options if not
set by user.

This does not impact the behavior of cvc5 when `--safe-options` is not
set.

FYI @alex-ozdemir @mudathirmahgoub @yoni206 .
2024-09-27 15:07:07 +00:00
Aina Niemetz
1a3a935fb5 Python API: Refactor to expose TermManager. (#10488)
This refactors the base Python API to expose TermManager (related to
previous refactor of the C++ API to expose TermManager in #10426).
2024-03-14 14:34:58 -07:00
Aina Niemetz
fdf9ce7138 Update copyright headers. (#10459) 2024-03-12 09:35:09 -07:00
Andrew Reynolds
2e41f64d47 Simplify API for constructing tuple values (#9766)
In preparation for 1.1.
2023-06-12 17:28:05 +00:00
mudathirmahgoub
12293a35d5 Add Relation and Table types to SMTLib parser (#8605) 2022-04-13 13:54:27 -05:00
Mathias Preiner
d01e59c13b Update copyright headers for release 1.0 (#8539) 2022-04-05 20:38:57 +00:00
Aina Niemetz
506a7b8c4a Python API: Do not rename enumerators. (#8507)
Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>
Co-authored-by: mudathirmahgoub <mudathirmahgoub@gmail.com>
Co-authored-by: Gereon Kremer <gkremer@stanford.edu>
2022-04-01 19:45:36 +00:00
Gereon Kremer
a7779de22d Remove decorator from python API (#8505)
This PR removes the expand_list_arg decorator from the python API. It was used to allow calling a function f(x, *args) with a list as second argument and automatically expand the list into *args. While it merely allows for calling f(x, l) instead of f(x, *l), it adds considerable complexity to the code and documentation. Thus, following the Zen of python (have only one way to do it) we remove this decorator. This is also consistent with the pythonic API, were we made the same decision.
2022-04-01 16:58:00 +00:00
Alex Ozdemir
6388657820 Change name of Python API's package from pycvc5 to cvc5. (#7953)
In the process, I changed a CMake target name from pycvc5 to
cvc5_base_py_api. I could not change the target to cvc5, because that
name is taken.
2022-02-02 23:45:42 +00:00
mudathirmahgoub
437c346559 Add relations.cpp, relations.py examples (#7801) 2021-12-17 19:23:16 +00:00