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
Nikolaj Bjorner
e2a52ed6ee
#5259 again
2021-05-10 11:15:19 -07:00
Nikolaj Bjorner
987099c765
Hoist creation of m_rep for #5259
2021-05-10 10:54:21 -07:00
Nikolaj Bjorner
a61e9d6b49
#5260
2021-05-10 10:33:43 -07:00
Nikolaj Bjorner
28328e63fd
fix #5255
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-09 20:48:11 -07:00
Nikolaj Bjorner
31a5bd7fd7
regression from July 4 2020 tweeted by Dr. RJ and crowd profiled - let's submit this somwhere?
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-09 20:33:43 -07:00
Philipp Schröer
7373946d67
julia: fix duplicate method ( #5251 )
...
Resulted in "Double registration for method" errors when loading Z3.jl
with a current build of Z3.
2021-05-07 14:00:33 -07:00
Nikolaj Bjorner
7e7360dd0c
#5223
2021-05-05 17:40:42 -07:00
Nikolaj Bjorner
7e330c15e7
#5223
2021-05-05 16:57:06 -07:00
Nikolaj Bjorner
87c0a8136f
#5223
2021-05-05 16:11:21 -07:00
