Nuno Lopes
f1545b04d2
optimize symbol table for single-threaded mode
...
remotes a bunch of mem allocs + unnecessary computations on every string lookup
2021-05-23 16:35:44 +01:00
Nuno Lopes
aef38099bf
vector.h: add assert to fail compilation if alignment isn't ok
...
let's see if all buildbots are happy with this..
2021-05-23 15:57:56 +01:00
Nuno Lopes
8fd7226b6f
typo
2021-05-23 14:28:42 +01:00
Nuno Lopes
f1e0d5dc8a
remove a hundred implicit constructors/destructors
2021-05-23 14:25:01 +01:00
Nuno Lopes
f8406623b4
switch parameter to an std::variant
...
plus fix mem leak & move constructor for zstrings
2021-05-23 13:07:29 +01:00
Nuno Lopes
9eb566b401
simplify some constructors/destructors
2021-05-23 12:39:49 +01:00
Nuno Lopes
79201e5ce6
buffer.h c++17 improvements
...
1) ensure data is properly aligned
2) add move constructor (useful for zstrings)
2021-05-23 12:11:12 +01:00
Nuno Lopes
34e8a2f0f6
simplify
2021-05-23 12:01:04 +01:00
Nikolaj Bjorner
fd0778c3d0
fixing symbol -> zstring
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-22 14:22:55 -07:00
Nikolaj Bjorner
262daf5151
symbol/zstring transition
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-22 13:54:21 -07:00
Nikolaj Bjorner
20a67e47ca
remove symbol -> zstring -> symbol round-trips
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-22 13:12:49 -07:00
Nikolaj Bjorner
5cb0bac41d
patch
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-22 12:26:54 -07:00
Nikolaj Bjorner
e14e3ef291
#5140
2021-05-22 10:27:53 -07:00
Nikolaj Bjorner
a10de2e975
#5140
2021-05-22 10:15:06 -07:00
Nikolaj Bjorner
c230d89a3a
fix #5294
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-22 09:59:50 -07:00
Nikolaj Bjorner
8ba0fb5b58
rounding mode sort removed for incompatibility
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-21 16:18:43 -07:00
Nikolaj Bjorner
00deb12238
signed
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-21 15:51:27 -07:00
Nikolaj Bjorner
e63e4587a4
build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-21 15:41:12 -07:00
Mikhail R. Gadelha
ed59c838bf
Implemented missing methods to the C++ API ( #5242 )
...
* Add method to print Sort to an ostream
Signed-off-by: Mikhail R. Gadelha <mikhail.ramalho@gmail.com>
* Added new FP check methods and clarify documentation
Signed-off-by: Mikhail R. Gadelha <mikhail.ramalho@gmail.com>
* Added missing fp conversion calls to C++ API
Signed-off-by: Mikhail R. Gadelha <mikhail.ramalho@gmail.com>
* Added method to convert a bv (in ieee format) to fp
Signed-off-by: Mikhail R. Gadelha <mikhail.ramalho@gmail.com>
* Added bv reduction methods to C++ API
Signed-off-by: Mikhail R. Gadelha <mikhail.ramalho@gmail.com>
* Add fp equality method
Signed-off-by: Mikhail R. Gadelha <mikhail.ramalho@gmail.com>
* Added methods to creates fpa nan and fpa inf
Signed-off-by: Mikhail R. Gadelha <mikhail.ramalho@gmail.com>
* Changed default rounding mode of the C++ API to RNE (see issue #4673 )
Signed-off-by: Mikhail R. Gadelha <mikhail.ramalho@gmail.com>
* Added methods to generate rounding mode sorts and rounding mode numerals
Signed-off-by: Mikhail R. Gadelha <mikhail.ramalho@gmail.com>
2021-05-21 14:10:09 -07:00
Iain Scott
c18f012c83
Remove x64 suffix from NuGet package names. ( #5292 )
2021-05-21 13:51:02 -07:00
Jakob Rath
089015b250
Minor fix in sat::literal ( #5293 )
2021-05-21 13:50:01 -07:00
Matt Thornton
ce1a48486e
Fix NuGet package name and glibc rid. ( #5290 )
2021-05-21 08:41:29 -07:00
Nikolaj Bjorner
17be37a5f6
fix #5287
2021-05-20 15:40:18 -07:00
Nikolaj Bjorner
a59dcfdeab
update python tag
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-20 15:23:39 -07:00
Matt Thornton
9cc1549dbe
Use osx-x64 for mac rid rather than macos. ( #5288 )
2021-05-20 15:19:31 -07:00
Nikolaj Bjorner
03d2c5f3d0
consolidate literals
2021-05-20 12:58:27 -07:00
Nikolaj Bjorner
c959e28d4a
remove prints, remove ability to toggle eager_eq_axioms option
...
NB. Spacer sets eager_eq_axioms option to false, but relevancy of this option is not clear at all as all other default paths don't use this option and theory_lra is incorrect when it is set to false.
2021-05-20 04:26:45 -07:00
Nikolaj Bjorner
cc12e3ed38
fix #5280
2021-05-19 16:52:24 -07:00
Nikolaj Bjorner
e0860ea173
fix #5279
2021-05-19 13:31:31 -07:00
Nikolaj Bjorner
ec034679ce
#5215
...
memory leaks
2021-05-19 12:42:38 -07:00
Nikolaj Bjorner
abe3ef2382
#5215
2021-05-19 10:33:23 -07:00
Nikolaj Bjorner
d450fd4227
#5215
2021-05-19 10:03:49 -07:00
Nikolaj Bjorner
7b3a587505
fix #5225
2021-05-18 18:04:03 -07:00
Nikolaj Bjorner
9031b5b949
fix build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-18 11:46:46 -07:00
Nikolaj Bjorner
0490056e7a
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-17 19:19:28 -07:00
Nikolaj Bjorner
30974968af
fix #5256
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-17 17:41:34 -07:00
Nikolaj Bjorner
4f9ad28a05
fix #5252
2021-05-17 16:16:12 -07:00
Nikolaj Bjorner
55f8ad068f
fix #5262
2021-05-17 15:51:03 -07:00
Nikolaj Bjorner
8384f38eb5
fix #5254
2021-05-17 15:42:01 -07:00
Nikolaj Bjorner
1a432529dd
fix #5272
2021-05-17 11:10:05 -07:00
Nikolaj Bjorner
d2bd92eab9
fix #5271
2021-05-17 10:42:34 -07:00
Nikolaj Bjorner
93a9847815
BUILD_LIBZ3_SHARED
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-16 15:44:44 -07:00
Margus Veanes
8ca6f567d3
fixing issue #5140 ( #5268 )
2021-05-16 13:53:08 -07:00
Zachary Wimer
f942c3df91
operator= checks this equality before moving ( #5265 )
2021-05-12 13:10:14 -07:00
Nikolaj Bjorner
7869cdbbc8
#5259 - the Ranjit 2s shave
...
shave a couple of seconds from the Ranjit regression
2021-05-12 10:43:16 -07:00
Nikolaj Bjorner
cd82205b06
nit
2021-05-10 19:14:18 -07:00
Nikolaj Bjorner
d27d09f87a
#5261
2021-05-10 13:35:25 -07:00
Nikolaj Bjorner
897a2d6470
#5261
2021-05-10 13:33:37 -07:00
Nikolaj Bjorner
f02fbb49bb
fix #5253
2021-05-10 13:00:52 -07:00
Nikolaj Bjorner
2ea4b0f4e0
#5260
2021-05-10 11:42:11 -07:00
