26 Commits

Author SHA1 Message Date
Daniel Larraz
e0ec61e050 Add support for compilation on Windows ARM64 (#12111)
This PR applies several changes required to compile cvc5 on Windows
ARM64 using MSYS2 CLANGARM64. In particular, `thread_local` class fields
and local function variables in classes and functions exported in the
API are not allowed, so they have been converted into global variables
within the compilation unit. Moreover, some functions in the cvc5 parser
library were using non-exported functions from the cvc5 base library.
This PR exports these functions and converts the ones that were inlined
into non-inlined functions to make them exportable.

Here is a summary of the results of running the cvc5 version in main and
in this branch:
```
config   status   total  solved     sat   unsat    best  timeout  memout  error  uniq  dis    time_cpu      memory 
main     ee      450474  385375  173928  211447  256627    57617     719      5    36    0  18909500.3  42742499.9 
pr       ee      450474  385370  173923  211447  192564    57621     720      5    31    0  18914388.1  42779989.7 
``` 
It seems that the Windows ARM64 changes do not significantly affect
solver performance compared to the main branch.
2025-09-10 15:44:59 +00:00
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
Daniel Larraz
545482a124 Use PRI macros to fix warnings in QuickStart C example (#11338)
Unlike the previous approach in PR #11251, this solution ensures
platform independence by using PRI macros for formatted printing.
Additionally, this PR enables the `-Werror` flag in the CI build for
examples, ensuring that future warnings are caught as errors.
2024-11-06 17:09:52 +00:00
Daniel Larraz
4f582c14a5 Fix format specifiers in QuickStart C example (#11251)
It addresses the following warnings triggered by clang on macOS:
```
warning: format specifies type 'long' but the argument has type 'int64_t' (aka 'long long') [-Wformat]
  printf("value for x: %ld/%lu\n", x_num, x_den);
                       ~~~         ^~~~~
                       %lld
warning: format specifies type 'unsigned long' but the argument has type 'uint64_t' (aka 'unsigned long long') [-Wformat]
  printf("value for x: %ld/%lu\n", x_num, x_den);
                           ~~~            ^~~~~
                           %llu
```
2024-10-03 15:48:03 +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
07bceca024 c api: Add parser_sym_manager example. (#10989) 2024-07-10 00:26:28 +00:00
Aina Niemetz
2e4db08c2f c api: Add parser example. (#10985) 2024-07-09 17:50:10 +00:00
Aina Niemetz
c997f10fa8 c api: Add uf example. (#10981) 2024-07-09 03:46:59 +00:00
Aina Niemetz
eeb9a97371 c api: Add transcendentals example. (#10980) 2024-07-09 02:52:28 +00:00
Aina Niemetz
82176dfcd3 c api: Add sygus-inv example. (#10979) 2024-07-09 01:00:10 +00:00
Aina Niemetz
9cf77ab9ac c api: Add sygus-fun example. (#10978) 2024-07-09 00:21:56 +00:00
Aina Niemetz
4e015283da c api: Add strings example. (#10972) 2024-07-08 23:45:35 +00:00
Aina Niemetz
8f17bd8890 c api: Add sets example. (#10971) 2024-07-08 23:10:27 +00:00
Aina Niemetz
7c6d78c653 c api: Add sequences example. (#10970) 2024-07-08 19:50:05 +00:00
Aina Niemetz
6e3a0aa013 c api: Add relations example. (#10969) 2024-07-08 18:57:16 +00:00
Aina Niemetz
92a4dceb5c c api: Add datatypes example. (#10952)
Note that this fixes a serious problem with DTypeSelector::getName()
where the delimiting 0-byte for self selectors was included, which
caused cutting off the name string for C strings.
2024-07-08 18:06:33 +00:00
Aina Niemetz
78c9ee57ec c api: Add quickstart example. (#10958) 2024-07-01 01:40:14 +00:00
Aina Niemetz
22ef689c5d c api: Add linear_arith example. (#10957) 2024-07-01 00:26:25 +00:00
Aina Niemetz
2eedebdb6a c api: Add floating_point_arithmetic example. (#10956) 2024-06-30 23:19:52 +00:00
Aina Niemetz
007487e33a c api: Add helloworld example. (#10955) 2024-06-30 21:26:28 +00:00
Aina Niemetz
1320c66626 c api: Add finite_field example. (#10954) 2024-06-30 19:41:56 +00:00
Aina Niemetz
b29a7ad434 c api: Add extract example. (#10953) 2024-06-30 17:37:41 +00:00
Aina Niemetz
c9d32d557a c api: Add combination example. (#10951) 2024-06-30 02:21:03 +00:00
Aina Niemetz
91ea1eca40 c api: Add bitvectors_and_arrays example. (#10950) 2024-06-30 01:14:50 +00:00
Aina Niemetz
20a7f71127 c api: Add bitvectors example. (#10949) 2024-06-29 23:09:30 +00:00