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
Nikolaj Bjorner
8f577d3943
remove ast_manager get_sort method entirely
2021-02-02 13:57:01 -08:00
Nikolaj Bjorner
3ae4c6e9de
refactor get_sort
2021-02-02 04:45:54 -08:00
Nikolaj Bjorner
cfcd7f18a9
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-01-28 17:09:12 -08:00
Nikolaj Bjorner
5414030875
#4939 escape character
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-01-28 11:57:00 -08:00
Nikolaj Bjorner
49aebdbb02
adding unicode fixup base on #4939 discussion
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-01-27 20:21:46 -08:00
