mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
16483 commits 49 branches 53 tags 182 MiB
Commit graph

16483 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
21baa2a70a Merge branch 'master' of https://github.com/z3prover/z3 into polysat 2021-04-14 03:51:12 -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
a0d112b7b0 general form migration 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-13 13:00:47 -07:00
Nikolaj Bjorner
7025d85da3 migrating to general form 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-13 11:21:41 -07:00
Nuno Lopes
524dcd35f9 reorder fields of context_params to save memory 
plus improve error checking in context_params::set_uint
 2021-04-13 18:35:58 +01:00
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
6402a80f10 Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat 2021-04-12 11:21:21 -07:00
Nikolaj Bjorner
f18789257e Print polynomials with power 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-12 11:20:40 -07:00
Jakob Rath
0e9fc4762a Fix PDD factor cache in case GC happens while factoring (#5170) 
* Add method to find largest power of two that is a divisor

* Binary resolve on PDDs

* Add unit tests for binary resolve

* Fix factor cache access in case GC happens while factoring

* Coding conventions

* Change to gc_generation
 2021-04-12 11:20:40 -07:00
Jakob Rath
75c87a2869 Test and memoize pdd factoring (#5163) 
* Test and fix pdd_manager::factor

* Memoize pdd_manager::factor

* Fix Windows build (maybe)
 2021-04-12 11:20:40 -07:00
Jakob Rath
f8562380d6 Fix pdd_manager::degree(PDD, unsigned) and add unit tests (#5155) 
* Fix pdd_manager::degree(PDD, unsigned) and add unit tests

* Another marking opportunity
 2021-04-12 11:20:40 -07:00
Nikolaj Bjorner
c575aa3973 remove sub 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-12 11:20:39 -07:00
Nikolaj Bjorner
16df37c484 clean 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-12 11:20:39 -07:00
Nikolaj Bjorner
11b547282a move to stash model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-12 11:20:39 -07:00
Nikolaj Bjorner
446654b680 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-12 11:20:39 -07:00
Nikolaj Bjorner
52d37f131d na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-12 11:20:38 -07:00
Nikolaj Bjorner
d247289606 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-12 11:20:38 -07:00
Nikolaj Bjorner
c2b213c049 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-12 11:20:38 -07:00
Nikolaj Bjorner
31baab49c8 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-12 11:20:37 -07:00
Nikolaj Bjorner
cec0cdce33 reorg resolution loop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-12 11:20:37 -07:00
Nikolaj Bjorner
d7456dc2a7 reorg resolution loop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-12 11:20:37 -07:00
Nikolaj Bjorner
ba5978723c introduce user-push/pop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-12 11:20:37 -07:00
Nikolaj Bjorner
112a70dd2c more stub 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-12 11:20:36 -07:00
Nikolaj Bjorner
00bf41daf4 add invariants and redundant constraint store 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-12 11:20:36 -07:00
Nikolaj Bjorner
bd04b5e8bd add testing stubs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-12 11:20:36 -07:00
Nikolaj Bjorner
b0e071aa2c na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-12 11:20:36 -07:00
Nikolaj Bjorner
7d4818d52c minor adjustments 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-12 11:20:35 -07:00
Nikolaj Bjorner
d2e25989b3 updated include 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-12 11:20:35 -07:00
Nikolaj Bjorner
23ae7e59d6 add unit test stub 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-12 11:20:35 -07:00
Nikolaj Bjorner
278babe625 Print polynomials with power 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-12 10:39:48 -07:00
Jakob Rath
6413c8717a
Fix PDD factor cache in case GC happens while factoring (#5170) 
* Add method to find largest power of two that is a divisor

* Binary resolve on PDDs

* Add unit tests for binary resolve

* Fix factor cache access in case GC happens while factoring

* Coding conventions

* Change to gc_generation
 2021-04-12 10:09:13 -07:00
Nikolaj Bjorner
ff1b35663b revert rewriting of OP_LE, OP_GE as it breaks axioms 2021-04-12 09:32:03 -07:00
Nikolaj Bjorner
804f065215 fixes for #4688 
https://github.com/Z3Prover/z3/issues/4866#issuecomment-778721073
 2021-04-11 17:42:12 -07:00
Nikolaj Bjorner
2dcfe799bc fix #4998 2021-04-11 04:42:16 -07:00
Nikolaj Bjorner
54f04a5751 being deliberate non-null #5156 2021-04-10 16:10:35 -07:00
Nikolaj Bjorner
878847179f fix #5144 2021-04-10 15:30:17 -07:00
Nikolaj Bjorner
8d9be5322f fix #4365 
m_library_aware_axiom_todo.reset(); should not be called because this vector is owned by the m_library_aware_trail_stack object.
 2021-04-10 13:03:05 -07:00
Nikolaj Bjorner
f607c15aa2 more rewrites for loop #4373 2021-04-10 11:15:59 -07:00
Lev Nachmanson
1a7c9fa54d rename a metod 2021-04-10 08:54:52 -07:00
Lev Nachmanson
6a1fd3b4d6 simplify the check for polarity, remove the struct with vertex and polarity 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2021-04-10 08:54:52 -07:00
Lev Nachmanson
8848e5b4c3 correctly explain the all fixed test in the octaganal tree 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2021-04-10 08:54:52 -07:00