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

15186 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nuno Lopes ce96182746 micro opt: dont reallocate an hashtable in a destructor 2021-04-14 17:32:34 +01:00
Nikolaj Bjorner 892e6d9ed5 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-14 05:06:46 -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
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 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
Lev Nachmanson 18610bf31f debug issue 5127 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2021-04-10 08:54:52 -07:00
Nikolaj Bjorner a5f957afb3 fixes for type #5164 2021-04-09 14:44:16 -07:00
Nikolaj Bjorner 673d2d700e more #5164 2021-04-09 13:11:53 -07:00
Nikolaj Bjorner 070eba0fe8 patch for #5164 2021-04-09 12:29:13 -07:00
Nikolaj Bjorner 7aa4fc2d8f fixing #5164 
overloading resolution has evolved a bit given how it inter-operates with automatic insertion of coercions, instantiation of polymorphic data-types, arrays as function spaces and other goodies. This is a rewrite of overloading resolution to disentangle the main components and allow them to cascade to give room for each-other.
 2021-04-09 11:29:00 -07:00
Nikolaj Bjorner a166aca48e na 2021-04-08 15:48:07 -07:00
Nikolaj Bjorner c849867eeb na 2021-04-08 12:41:21 -07:00
Nikolaj Bjorner 6b1642e272 fix #5068 2021-04-08 12:39:23 -07:00
Nikolaj Bjorner 9ef7cf1e81 test old connection 2021-04-08 12:14:29 -07:00
Nikolaj Bjorner 44156f9f55 patch to fix #5110 2021-04-08 11:25:20 -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 887b62efe6 another patch 2021-04-07 18:20:45 -07:00
Nikolaj Bjorner 6e1ac19c44 new name 2021-04-07 17:43:32 -07:00
Nikolaj Bjorner 90995b63c3 fix nightly 2021-04-07 15:43:39 -07:00
Nikolaj Bjorner d9af8ea9fb fix #5113 2021-04-07 12:20:12 -07:00
Nikolaj Bjorner a99e75f58f fix #5154 2021-04-07 11:28:51 -07:00
Nikolaj Bjorner 46831e7ebb provisionary fix for #5127 2021-04-06 22:32:22 -07:00
Nikolaj Bjorner dcfd9c859d fix build 2021-04-06 21:30:13 -07:00
Nikolaj Bjorner 1b503b8887 na 2021-04-06 20:09:51 -07:00
Nikolaj Bjorner 0b0efa83ca debugging #5127 2021-04-06 20:09:50 -07:00
Nikolaj Bjorner e5e663e874 fix for #5153 2021-04-06 20:09:50 -07:00
Nikolaj Bjorner a832ada3d1 fix #5152 2021-04-06 20:09:50 -07:00
Nikolaj Bjorner 6099b84ff6 fix #5149 2021-04-06 20:09:49 -07:00
Nuno Lopes a6ef99d56e constify ids of builtin AST families + remove some dead code 2021-04-04 18:13:52 +01:00
Nuno Lopes c47ab023e5 remove a few trivial destructors so they get inlined 2021-04-04 17:13:59 +01:00