mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 19:53:34 +00:00
Code Activity
14856 commits 23 branches 48 tags 156 MiB
Commit graph

14856 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner d08814a1fe have nightly generate doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 15:57:01 -08:00
Nikolaj Bjorner 909257f856 remove family id externals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 06:48:24 -08:00
Nikolaj Bjorner d3564f5b50 move unicode toggle to char-plugin 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 06:42:19 -08:00
Nikolaj Bjorner 0c770e25df na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 06:29:38 -08:00
Nikolaj Bjorner e969bd1c97 fully remove seq-based characters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 06:26:44 -08:00
Nikolaj Bjorner 8d8fe872ad remove plugin status to theory_seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 06:22:25 -08:00
Nikolaj Bjorner 696b3c79b9 fixes to self-contained character unicode 2021-01-27 06:13:37 -08:00
Nikolaj Bjorner d0f1d8f59e move to unicode as stand-alone theory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 05:46:45 -08:00
Nikolaj Bjorner ecba26beae missing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-26 17:07:46 -08:00
Nikolaj Bjorner 32058d9c68 add char_decl_plugin 2021-01-26 16:43:03 -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 33714ceb40 use _ 2021-01-26 14:56:48 -08:00
Nikolaj Bjorner e26e38b654 add error generation for #4977 2021-01-26 14:55:42 -08:00
Nikolaj Bjorner 8ed1992029 char value 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-26 11:29:40 -08:00
Nikolaj Bjorner a0b7879dd9 handle signed characters convertions into unsigned numbers 2021-01-26 11:20:28 -08:00
Nikolaj Bjorner 7dd7d83a36 make it easier to use string literals 2021-01-26 11:01:03 -08:00
Nikolaj Bjorner 31b7ad3012 prepare char utilities as a stand-alone theory 2021-01-26 10:34:10 -08:00
Matteo Nicoli 785fab74f4
Create bubble_sort.py (#4976) 2021-01-26 09:42:17 -08:00
Nikolaj Bjorner dccfecb488 generator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-25 19:18:55 -08:00
Nikolaj Bjorner 4b6d7ca097 working on mam 2021-01-25 17:54:53 -08:00
Nikolaj Bjorner f33d6f89b9 fix #4973 2021-01-25 12:20:27 -08:00
Nikolaj Bjorner 2646e0a1c0 have add_soft accept an interable of Booleans. 2021-01-25 12:17:35 -08:00
Nikolaj Bjorner 7d60d8462d patch for Sturm sequence bug #4961 2021-01-24 12:58:25 -08:00
Asger Gitz-Johansen 2d1684bc2d
Added the SUBMODULE_DIR_NAME variable for better submodule support (#4959) 
* Added the CMAKE_MODULE_DIR_NAME variable for better submodule support

* It should be called SUBMODULE_DIR_NAME instead
 2021-01-23 13:05:28 -08:00
Nikolaj Bjorner 47cb1d1207 remove bit-vector dependencies in theory_str_mc. See discussion #4939 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-23 13:03:06 -08:00
Nikolaj Bjorner e4cec19f03 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-23 12:16:00 -08:00
Nikolaj Bjorner 96f1f4a567 rename to seq_char instead of seq_unicode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-23 12:12:06 -08:00
Artem Alekseev 7e668e9a1f
Fix build (#4960) 2021-01-23 11:13:10 -08:00
Nikolaj Bjorner 03fd251ccb streamline unicode/ascii toggling. Fix bit-width for unicode to 18 2021-01-23 11:11:44 -08:00
Nikolaj Bjorner 90eb4de526 track reference counts of allocated characters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-23 10:42:43 -08:00
Nikolaj Bjorner 6edabd6c03 egraph 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-22 18:11:27 -08:00
Nikolaj Bjorner 680b185872 adding ematching engine, fixing seq_unicode 2021-01-22 17:10:45 -08:00
Nikolaj Bjorner db17ae03c6 early return, statistics, remove unused field 2021-01-21 23:53:34 -08:00
Nikolaj Bjorner 4c82350ca4 na 2021-01-21 23:35:04 -08:00
Nikolaj Bjorner 2051cac3a3 tidy 2021-01-21 23:34:47 -08:00
Nikolaj Bjorner d2abc9ed0f remove comment #4956 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-21 22:18:24 -08:00
pcarbonn 0eb04df834
fix #4956 (#4958) 2021-01-21 22:16:49 -08:00
Nikolaj Bjorner 4e8ba8b160 regression fix, fix unicode mode 2021-01-21 22:06:15 -08:00
Nikolaj Bjorner 64ba44d2ac fix underflow bug when subtracting unsigned numbers 2021-01-21 21:01:02 -08:00
Nikolaj Bjorner 987efced76 upgrade compilers 2021-01-21 14:25:08 -08:00
Nikolaj Bjorner 6f09ecb229 set version 2021-01-21 14:24:58 -08:00
Nikolaj Bjorner dafee71500 reshuffle unicode support to use global parameter, and use bit-vectors on demand 2021-01-21 14:24:26 -08:00
Nikolaj Bjorner fb48481860 update version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-20 12:51:48 -08:00
Nikolaj Bjorner 517d907567 Update release.yml for Azure Pipelines 2021-01-20 12:06:47 -08:00
Nikolaj Bjorner af914f101e change to macos latest 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-20 10:19:00 -08:00
Nikolaj Bjorner c5432dbd88 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-20 09:12:09 -08:00
Nuno Lopes 3a572edb9c fix build 2021-01-20 10:42:29 +00:00
Nikolaj Bjorner 48058e706f fix #4951 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-20 02:21:42 -08:00
Nikolaj Bjorner 3f2349f0f7 update release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-20 01:36:09 -08:00
Saurav Yadav 9dcf44b767
fix git_utils.cmake (#4954) 
The code should refrain from using global parameters such as CMAKE_SOURCE_DIR/CMAKE_BINARY_DIR, especially here which is handling the case of Z3 being a submodule. Instead, use project specific variables like Z3_SOURCE_DIR so that people can incorporate z3 build as part of their build-system.
 2021-01-20 01:33:33 -08:00