mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 22:59:02 +00:00
Code Activity
15225 commits 23 branches 48 tags 157 MiB
Commit graph

1594 commits

Author SHA1 Message Date
Nikolaj Bjorner e5892e5e97 #5215 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-27 15:26:56 -07:00
Nikolaj Bjorner c03fac8390 Investigating std::vector and #5178 2021-04-24 14:50:59 -07:00
Nikolaj Bjorner 770c79a939 prepare for std::vector 2021-04-20 09:24:24 -07:00
Nuno Lopes e67b9ebcf7 try to fix ARM32 build (#2776) 2021-04-17 16:14:05 +01: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 4a6083836a call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
Nikolaj Bjorner e89071d366 #5125 2021-03-26 14:58:24 -07:00
Luca Bruno b918f121ef
zstring: fix encode rountrip for '\' as printable ASCII (#5120) 
This fixes encode roundtripping for all printable ASCII characters.
In particular, this now leaves a plain '\' untouched by the
encoding logic, instead of converting it to escaped hex-digits.
It also adds unit testing covering this specific zstring encoding
property, in order to avoid future regressions.
 2021-03-23 11:25:59 -07:00
Nikolaj Bjorner 2fef6dc502 more scaffolding 2021-03-21 11:31:14 -07:00
Nikolaj Bjorner a1f484fa35 na 2021-03-19 16:42:45 -07:00
Nikolaj Bjorner 15a7621e27 remove template dependency for trail objects 2021-03-19 11:15:05 -07:00
Nikolaj Bjorner 857557ad93 deal with compiler warnings 2021-03-08 20:39:19 -08:00
Nikolaj Bjorner f29a596070 deal with compiler warnings, from MacOS CI build 2021-03-08 17:14:09 -08:00
Nikolaj Bjorner 38737db802 fixes and more porting seq_eq_solver to self-contained module 2021-03-04 16:23:22 -08:00
Nuno Lopes db04ccb137 scoped_timer: skip extra unneded heap allocation 2021-03-01 14:36:22 +00:00
Nikolaj Bjorner 830f314a3f fixes to dt_solver and related 2021-02-27 11:03:20 -08:00
Nikolaj Bjorner c3b7fa941a fix #5048 2021-02-22 10:56:19 -08:00
Nikolaj Bjorner 9ae3339c33 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-18 12:33:17 -08:00
Nuno Lopes d396d46bd1 let's test if all the buildbots are happy with C++17 
it's stil a bit too early for C++20
 2021-02-18 18:13:10 +00:00
Nikolaj Bjorner e63dc7efc2 more rewrite rules 2021-02-17 17:32:00 -08:00
Nikolaj Bjorner 96e7b811f9 fix #5029 2021-02-15 14:17:05 -08:00
Nikolaj Bjorner 6bd02e122b parse according to http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-15 09:32:31 -08:00
Nikolaj Bjorner c808f74591 fix multiplier base for #5022 
add also some C++ API shorthands for retrieving numerals
 2021-02-12 11:53:40 -08:00
Nikolaj Bjorner a152bb1e80 remove template Context dependency in every trail object 2021-02-08 15:41:57 -08:00
Nikolaj Bjorner 4dfdabc80f na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-31 16:36:55 -08:00
Nikolaj Bjorner 6d99a8f0cc fixes for unicode 2021-01-31 14:55:52 -08:00
Nikolaj Bjorner 8fde6c207d set unicode to default 2021-01-31 07:22:51 -08:00
Nikolaj Bjorner 657ed4db7a fix relevancy bug for recfun 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-30 07:19:57 -08:00
Nikolaj Bjorner 520b24aab4 string escaping 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-30 04:58:58 -08:00
Nikolaj Bjorner c99b805c14 mld 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-29 18:37:38 -08:00
Nikolaj Bjorner ec1e3cc14a encoding disaster 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-29 16:25:24 -08:00
Nikolaj Bjorner 4857446cf6 change handling of escapes for #4708 2021-01-29 13:36:47 -08:00
Nikolaj Bjorner 5414030875 #4939 escape character 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-28 11:57:00 -08:00
Nikolaj Bjorner 20332c6d3e adding char decl plugin for separate theory treatment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-26 16:28:44 -08:00
Nikolaj Bjorner 4b6d7ca097 working on mam 2021-01-25 17:54:53 -08:00
Nikolaj Bjorner 7d60d8462d patch for Sturm sequence bug #4961 2021-01-24 12:58:25 -08:00
Nikolaj Bjorner 680b185872 adding ematching engine, fixing seq_unicode 2021-01-22 17:10:45 -08:00
Nikolaj Bjorner 4d55f83654 misc 2020-12-04 16:59:13 -08:00
John Regehr b7e1b1e118
get rid of threads in the scoped_timer thread pool prior to forking, on non-Windows (#4833) 
* on POSIX systems, fork() is dangerous in the presence of a thread
pool, because the child process inherits only the thread from the
parent that actually called fork().

this patch winds down the scoped_timer thread pool in preparation for
forking; workers will get freshly created again following the fork
call.
 2020-11-29 21:26:53 +00:00
Nikolaj Bjorner 797f50e699 DRAT debugging updates 2020-11-22 15:38:57 -08:00
Nikolaj Bjorner 1b768c9b3a fix #4805 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-20 12:11:38 -08:00
Nikolaj Bjorner 6506d33b35 Add GCD test 2020-11-20 11:12:54 -08:00
Nuno Lopes 40159a3a96 fix single-thread build 2020-11-19 21:46:32 +00:00
John Regehr 0fa88efc2b
scoped_timer: wait for timer thread before main thread continues (#4803) 2020-11-19 21:42:55 +00:00
Christoph M. Wintersteiger eadf755628
Fix bonus subtraction in fp.rem. Fixes #4564. Fixes most of #2381. 2020-11-06 20:54:10 +00:00
Nikolaj Bjorner ab199dedf9 debug arith/mbi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-02 12:13:19 -08:00
Christoph M. Wintersteiger c03c395267
Add missing assertion. Fixes #4642. 2020-10-30 14:09:51 +00:00
Nuno Lopes 1730bc7c7f fix #4763: shell not finishing before hard timeout 
The timer thread for the hard timeout was leaking and thus the thread only exited on timeout
 2020-10-30 10:01:09 +00:00
Nikolaj Bjorner f354671465 add parameter for scenario from #4743 2020-10-30 01:14:34 -07:00
Nikolaj Bjorner 0de3149634 fix #4763 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-29 11:15:53 -07:00