mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-19 07:09:03 +00:00
Code Activity
15182 commits 23 branches 48 tags 157 MiB
Commit graph

2035 commits

Author SHA1 Message Date
Nuno Lopes 49906a5a58 api_context: remove basic&arith fids fields 
these are now constant,s o we can save some space
the remaining ones need to be made constant as well..
 2021-04-13 17:42:42 +01:00
Nuno Lopes afdf80509a remove api_context::m_search as it's always constant (false) 2021-04-13 17:32:17 +01:00
Nuno Lopes 853ce099ec api_context: consolidate ast trail vectors 
a context never changes between user rc/non-user rc, so we can reuse the trail for both options
and save memory & smallish speedup
 2021-04-13 17:21:42 +01:00
Zachary Wimer f4127bd6f3
Remove function arg names for deleted functions (#5176) 2021-04-12 14:37:44 -07:00
Zachary Wimer 8e6ab5b1bf
prefer parent operator= to manually copying parent data for extensibi… (#5177) 
* prefer parent operator= to manually copying parent data for extensibility reasons

* typos fixed
 2021-04-12 14:37:27 -07:00
Zachary Wimer dd3be32b98
Cpp api general minor improvements (#5175) 
* Added noexcepts, deleted trivial copy functions that can be implcit, small things

* Add back in virtual destructor. This has rule of 5 side effects, but move semantics are not supported yet so it is *mostly* ok. The move PR will address this.
 2021-04-12 14:03:20 -07:00
Zachary Wimer 70604a6856
Explicitly delete private constructors (#5174) 2021-04-12 13:46:55 -07:00
Zachary Wimer 973f79dc4d
rename final to register_final since final is a specifier in C++11+ (#5172) 2021-04-12 13:38:03 -07:00
Zachary Wimer 4625454a38
Fix fixedpoint rc bug and fix optimize non-const bug (#5173) 
* Fix fixedpoint rc bug and fix optimize non-const bug

* Fix indentation
 2021-04-12 13:37:05 -07:00
Zachary Wimer d73b883b38
array uses unique_ptr (#5171) 
* array uses unique_ptr

* Constructor initalize m_array over set it

* prefer arr.get() to &arr[0]
 2021-04-12 13:01:24 -07:00
Nikolaj Bjorner 54f04a5751 being deliberate non-null #5156 2021-04-10 16:10:35 -07:00
Nikolaj Bjorner d91eac24b7 more missing nullptr flexibility #5156 2021-04-08 10:34:09 -07:00
Nikolaj Bjorner b1f5933c7d fix missing nullptr check for #5156 2021-04-08 10:30:33 -07:00
Nikolaj Bjorner d9af8ea9fb fix #5113 2021-04-07 12:20:12 -07:00
Nikolaj Bjorner 94b4d1b442 fix travis build for python doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-29 15:30:31 -07:00
Zachary Wimer 531a828c57
Update setup.py to use cmake build system (#5128) 2021-03-28 14:17:33 -07:00
Alexander Kreuzer dc5fa89de3
Mixing Integers and Rational in the new Java API #5085 (#5098) 
* Added covariance to arithmetic operations

* Added distillSort

* Update JavaGenericExample.java

Co-authored-by: Alexander Kreuzer <alexander.kreuzer@sap.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-16 05:24:23 -07:00
Nikolaj Bjorner d03fdf5fed more descriptive naming convention 2021-03-15 15:48:33 -07:00
Nikolaj Bjorner 4b3fecc35e remove dependency on ast from params 2021-03-15 15:40:41 -07:00
Nikolaj Bjorner 8412ecbdbf fixes to new solver, add mode for using nlsat solver eagerly from nla_core 2021-03-14 13:57:04 -07:00
Graydon Hoare e8b3c90e14
Fix unintentional re-import of package z3 in z3printer, in python3. (#5082) 2021-03-06 10:44:07 -08:00
Nikolaj Bjorner e804f7743a
Revert "Adjust imports so z3.z3 is still available in python3 (#5079)" (#5081) 
This reverts commit 957d7bfe35.
 2021-03-05 15:26:00 -08:00
Graydon Hoare 957d7bfe35
Adjust imports so z3.z3 is still available in python3 (#5079) 2021-03-04 17:18:39 -08:00
Nikolaj Bjorner f7b1469462 Try freeing context in dispose method and not wait for finalizer #5043 2021-02-27 11:02:58 -08:00
Nikolaj Bjorner 08f55f9d1f start wcnf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-26 11:13:44 -08:00
Nikolaj Bjorner be68456c06 java compilation? 2021-02-26 05:04:46 -08:00
Nikolaj Bjorner 06caf57a86 fix #5033 2021-02-26 03:42:13 -08:00
Nuno Lopes 5e034e495f fix compiler warnings 2021-02-19 10:33:41 +00:00
Nuno Lopes bcad4d9435 revert my mess with the ast hashtable 
will share results form the experiments later
 2021-02-17 14:29:07 +00:00
Nikolaj Bjorner 1da7522893 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-14 17:47:19 -08:00
Nikolaj Bjorner 04a1d4245c fix #4801 2021-02-12 20:20:00 -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 2e648e2f02 glibc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-11 13:19:23 -08:00
Nikolaj Bjorner 98eae28fca try to update setup.py to libc naming 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-11 11:52:05 -08:00
Nikolaj Bjorner 692f159af8 try without format 2021-02-09 12:49:55 -08:00
Nikolaj Bjorner e722589810 address some of the ugliness pointed out by abandoned pull request #5008 2021-02-09 11:23:16 -08:00
Nikolaj Bjorner 0f29fff836 remove bit-vector dependencies in seq theory 2021-02-08 10:57:50 -08:00
Nikolaj Bjorner 43d1ef2fee iterable is a Python 3 thingy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-07 18:22:57 -08:00
Nuno Lopes 682b947ad3 the documentation of Z3_model_get_func_interp() says it returns NULL if there's no interpretation 
so let's honour that instead of throwing an exception
 2021-02-07 12:46:36 +00:00
Nuno Lopes e1572096ca delete some dead code 2021-02-07 12:14:52 +00:00
Julius Marozas 01d5f3259c
Fix show parameter in prove, solve, and solve_using (#5001) 
* Fix show parameter in prove function

* Fix show in solve & solve_using

* Use Python 2 compatible syntax

* Add default value for show
 2021-02-06 16:42:15 -08:00
Nikolaj Bjorner e856cfc458 coercions 2021-02-06 10:35:28 -08:00
Nikolaj Bjorner 16448104eb add new model event handler for incremental optimization 2021-02-05 17:11:04 -08:00
Nikolaj Bjorner 2c472aaa10 #4999 
use typing Iterable
 2021-02-05 12:09:24 -08:00
Nikolaj Bjorner a582014854 #4999 2021-02-05 12:01:30 -08:00
Malte Mues 5d8d42b1fa
Update the mkConstant parameter type (#4996) 2021-02-04 16:17:49 -08:00
Nikolaj Bjorner dfb7c87448 #4997 2021-02-04 15:46:34 -08:00
Nikolaj Bjorner cc39cf037e build again 2021-02-04 12:36:44 -08:00
Nikolaj Bjorner b3144a534d remove string conversion causing regression 2021-02-03 21:40:45 -08:00
Nikolaj Bjorner abcabba9fe fix python build 2021-02-03 09:57:16 -08:00