Tias Guns
a52b485d9c
marco: immediately shrink to core if not subset ( #5203 )
...
Small improvement, found while translating it in another system
2021-04-20 12:29:52 -07:00
Nikolaj Bjorner
8263d20e0d
add code review comment
2021-04-20 11:30:25 -07:00
Nikolaj Bjorner
b658934bd8
fix #5197 fix #5193
2021-04-20 10:16:44 -07:00
Nikolaj Bjorner
44d77a978a
cw review comments #5200
2021-04-20 09:27:59 -07:00
Nikolaj Bjorner
770c79a939
prepare for std::vector
2021-04-20 09:24:24 -07:00
Zachary Wimer
831afa8124
Cpp api add missing fp methods (return type correction) ( #5200 )
...
* added is_nan and is_inf to API
* added support to to_ieee_bv
* bug fix
2021-04-19 17:55:23 -07:00
Zachary Wimer
10e9345cd7
C++ API add missing FP methods ( #5199 )
...
* added is_nan and is_inf to API
* added support to to_ieee_bv
2021-04-19 15:24:09 -07:00
Zachary Wimer
542878dea3
Add sge and sgt to API; now has sge,sgt,sle,slt, and unsigned counterparts ( #5194 )
2021-04-19 08:53:43 -07:00
Zachary Wimer
f8228ff50e
[c++ api] add const ( #5195 )
2021-04-19 10:24:12 +01:00
Nuno Lopes
e67b9ebcf7
try to fix ARM32 build ( #2776 )
2021-04-17 16:14:05 +01:00
Zachary Wimer
a1741e0e16
z3 c++ api: delete implicit constructor ( #5191 )
2021-04-16 10:46:03 +01:00
Zachary Wimer
239ace4353
expr move semantics supported via ast ( #5190 )
2021-04-15 13:37:31 -07:00
Nuno Lopes
21e59f7c6e
change model evaluator to respect resource limits ( #5184 )
2021-04-14 11:48:39 -07: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
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