mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-04 16:44:07 +00:00
Code Activity
19575 commits 22 branches 48 tags 155 MiB
Commit graph

59 commits

Author SHA1 Message Date
Josh Berdine 934455a24b
Remove vestiges of old ml api (#7597) 2025-03-27 16:41:31 -07:00
Nikolaj Bjorner ec14ef765e Update Ubuntu job name in Azure pipeline and add string variable creation in C API example 2024-09-23 17:42:39 +01:00
Nuno Lopes 87e45221fd add missing break stmt to example 
Reported by Henrique Preto
 2022-10-14 09:43:18 +01:00
Nikolaj Bjorner 5322d4f241 fix #6326 2022-09-06 23:48:21 -07:00
Brenton Bostick 5351640e97
Fix stray semicolon in examples (#5669) 2021-11-18 10:35:22 -08:00
Alexander Traud f5f35f87d0
fix grouping for latest doxygen (#5626) 
Since doxygen 1.8.16, opening and closing a group must not be done as
C comment but as doxygen command. In other words, not one but two
asterisk characters are required so that doxygen finds a group.
 2021-10-27 23:46:31 +02:00
Rolf Eike Beer 7f8e2a9f75
clean up CMake code (#5182) 
* CMake: simplify FindGMP.cmake

Remove printing of all the different variables, and let FPHSA output the library
name. Add an imported target, which bundles the library and the include
directories for easier usage.

* fix build: vector::c_ptr() now is vector::data()

* CMake: use Threads::Threads imported module

Otherwise the setting of THREADS_PREFER_PTHREAD_FLAG has no effect.

* CMake: remove needless policy setting

The minimum required version is CMake 3.4, where these policies are already set
to new because they were introduced earlier.

* CMake: remove needless variable expansion
 2021-04-14 10:29:15 -07:00
Nikolaj Bjorner 85b4fc1865 void 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-23 10:47:39 -07:00
Nikolaj Bjorner 3eac4a4aa1 clean up examples for unused variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-22 10:24:05 -07:00
Bruce Mitchener 0eafeb9342 Fix confusing tabs mixed in with spaces in C examples. 2019-08-13 09:26:44 -07:00
Nikolaj Bjorner cb6d3d2458 increase minimal requirement to 3.4 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-07 17:05:12 -07:00
Bruce Mitchener 44bc00f13d Fix typos. 2018-12-23 21:58:57 -05:00
Bruce Mitchener edf8ba44d1 Switch from using Z3_bool to using bool. 
This is a continuation of the work started by using stdbool and
continued by switching from Z3_TRUE|FALSE to true|false.
 2018-11-20 11:27:09 +07:00
Bruce Mitchener 56bbed173e Remove usages of Z3_TRUE / Z3_FALSE. 
Now that this is all using stdbool.h, we can just use true/false.

For now, we leave the aliases in place in z3_api.h.
 2018-11-20 00:25:37 +07:00
Nikolaj Bjorner a85a612bae use old-fashined C for test_capi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-15 10:03:43 -08:00
Florian Pigorsch 326bf401b9 Fix some spelling errors (mostly in comments). 2018-10-20 17:07:41 +02:00
Bruce Mitchener a76397d3b8 Refer to macOS rather than Mac OS / OSX. 2018-10-02 17:38:09 +07:00
Nikolaj Bjorner adb9a1c797 fix c 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-04 17:31:26 -07:00
Nikolaj Bjorner 9f3da32a77 remove interpolation from test_capi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-24 16:28:23 -07:00
Nikolaj Bjorner fa93bc419d fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-01 10:53:36 -07:00
Nikolaj Bjorner f525f43e43 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-30 09:30:43 -07:00
Nikolaj Bjorner 32c9af5e5a fix use of Z3_bool -> Z3_lbool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-27 16:16:25 -07:00
Nikolaj Bjorner c513f3ca09 merge with master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-25 14:57:01 -07:00
Bruce Mitchener 73b3da37d8 Typo fixes. 2018-01-02 22:48:06 +07:00
Nikolaj Bjorner 2749e547cf fix c example, remove more smtlib1 printing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 18:14:24 -08:00
Nikolaj Bjorner fd49a0c89c added facility to persist model transformations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-02 00:05:52 -05:00
Nikolaj Bjorner fc73271b83 more C fixes to model example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 11:20:56 -07:00
Nikolaj Bjorner 7ed32f4315 re-add model example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 10:48:53 -07:00
Nikolaj Bjorner 2c27056283 disable model example pending C compliance or C99 or whatever adjustment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 10:24:49 -07:00
Dan Liew de3700e1fd [CMake] Try to unbreak the C example build with older GCC versions 
by forcing the language version to be C99.
 2017-10-25 11:13:25 +01:00
Dan Liew f27ac24fa0 Add example of using Z3's new model construction C API. This API 
was requested in #1223.

This example uses the new `Z3_mk_model()`, `Z3_add_const_interp()`
, `Z3_add_func_interp()`, and `Z3_mk_as_array()` API calls.
 2017-10-24 17:34:47 +01:00
Nikolaj Bjorner f63439603d streamlining proof generation (initial step of removing ast-manager dependency). Detect error in model creation when declaring constant with non-zero arity. See #1223 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-23 21:16:46 -07:00
Dan Liew a9fcfc531b [TravisCI][CMake] Add Z3_C_EXAMPLES_FORCE_CXX_LINKER CMake option 
and propagate its value into the C API examples.

This flag forces the C API examples to use the C++ compiler as the
linker rather than the C compiler. This a workaround to avoid linking
errors when building with UBSan.
 2017-10-16 08:56:17 +01:00
Nikolaj Bjorner 1a6f8c2fad working on parallel solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-10 16:35:05 -07:00
Nikolaj Bjorner 09ea370ea3 update C-example that fails to not use longjumps. Issue #1297 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-10 12:06:19 -07:00
Nikolaj Bjorner b482dbd589 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 17:02:27 -07:00
Dan Liew 4b517b96df [CMake] Move CMake files into their intended location so the 
`contrib/cmake/bootstrap.py` script no longer needs to be executed.

The previous location of the CMake files was a compromise proposed
by @agurfinkel in #461. While this has served us well (allowing progress
to be made) over time limitations of this approach have appeared.

The main problem is that doing many git operations (e.g. pull, rebase)
means the CMake files don't get updated unless the user remembers to
run the script. This can lead to broken and confusing build system
behaviour.

This commit only does the file moving and necessary changes to
`.gitignore`. Other changes will be done in subsequent commits.
 2017-06-12 11:59:00 +01:00
Nikolaj Bjorner 0ac80fc042 have parser produce ast-vector instead of single ast 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-01 21:21:05 -07:00
Takeshi Abe 5c2969c0f0 Fix typo 2016-03-23 12:51:41 +09:00
Christoph M. Wintersteiger 3b92128ed8 Fixed old-style C variable declaration problem in interpolation C example. 2016-02-16 12:12:59 +00:00
Ken McMillan 8b90bc9e91 fixed logginf on return of Z3_compute_interpolant and added interpolation example to test_capi.c 2016-02-11 16:09:54 -08:00
Nikolaj Bjorner 6c6da44f8f removing const qualifiers, perhaps this helps for #420 and adding assert to enable Clang analysis earlier for issue #440 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-09 22:24:37 +00:00
Nikolaj Bjorner 5ce85aba40 removing const qualifiers, perhaps this helps for #420 and adding assert to enable Clang analysis earlier for issue #440 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-09 22:23:37 +00:00
Christoph M. Wintersteiger de3cb7e5dc More FPA exponent/siginficand order consistency 2016-01-05 18:05:21 +00:00
Dan Liew 83e2b1c6e5 Typo in comment in C api example. 2015-12-15 11:52:35 +00:00
Nikolaj Bjorner 995e112a18 fix examples 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-20 08:01:59 -08:00
Nikolaj Bjorner 90400ec914 update C example to use new API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-16 15:03:58 -08:00
Christoph M. Wintersteiger 88b027ecce Eliminated unused variable from C example. 2015-10-29 13:32:58 +00:00
Nikolaj Bjorner d469a16bb8 add more Copyright notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-10 11:59:21 -07:00
Christoph M. Wintersteiger 48c72d2c38 FPA API: naming consistency 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-23 18:18:26 +00:00