Jakob Rath
|
0ada7f8e40
|
bug with sizes
|
2024-02-08 14:20:26 +01:00 |
|
Jakob Rath
|
0cef6bec4e
|
be explicit about intended division semantics
fixes bug in chop_off_lower
|
2024-02-08 13:02:26 +01:00 |
|
Bruce Mitchener
|
53f89a81c1
|
Fix some typos. (#7115)
|
2024-02-07 23:06:43 -08:00 |
|
Jakob Rath
|
85d3e266a4
|
Update viable::propagate_from_containing_slice to use new get_fixed_sub_slices (wip)
|
2024-02-07 17:16:26 +01:00 |
|
Jakob Rath
|
9283b4169c
|
Add get_fixed_sub_slices
|
2024-02-07 15:38:26 +01:00 |
|
Jakob Rath
|
b66849b7a0
|
remove duplicate header
|
2024-02-07 15:35:38 +01:00 |
|
Jakob Rath
|
5e545c8f86
|
Add merge_level
|
2024-02-07 15:26:15 +01:00 |
|
Jakob Rath
|
70785a095e
|
function as const-ref
|
2024-02-07 15:25:25 +01:00 |
|
Jakob Rath
|
098d35c519
|
Add types to track additional info with fixed sub slices
|
2024-02-07 15:23:10 +01:00 |
|
Jakob Rath
|
cbcb5ad92d
|
euf::theory_var is int
|
2024-02-07 15:21:47 +01:00 |
|
Jakob Rath
|
f0b0ce401e
|
take std::function as const reference
|
2024-02-07 15:16:44 +01:00 |
|
Nikolaj Bjorner
|
74a91f691f
|
fix bug in slice creation: exposed by 3047RIHj3agM.smt2
|
2024-02-06 16:00:33 -08:00 |
|
Nikolaj Bjorner
|
937d4aa8f4
|
move files from lib and java directory to bin
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-06 12:40:30 -08:00 |
|
Nikolaj Bjorner
|
3f3ac924ab
|
add debugging output
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-06 09:48:09 -08:00 |
|
Nikolaj Bjorner
|
c40e72aaa3
|
include debug output
|
2024-02-05 15:31:33 -08:00 |
|
Nikolaj Bjorner
|
f4eaa6fc98
|
improve logging
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-05 14:41:29 -08:00 |
|
Nikolaj Bjorner
|
683070a175
|
finish encoding of n'th root
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-05 10:44:41 -08:00 |
|
Nikolaj Bjorner
|
187a6b17dd
|
fix blast rule for overflow
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-05 08:16:34 -08:00 |
|
Nikolaj Bjorner
|
8555f25587
|
add todo note, and log more lemmas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-04 21:08:04 -08:00 |
|
Nikolaj Bjorner
|
f4474a3edb
|
typo
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-04 20:30:56 -08:00 |
|
Nikolaj Bjorner
|
446a9dec08
|
distinguish vs-arch from arch identifier
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-04 19:26:50 -08:00 |
|
Nikolaj Bjorner
|
d743e1b47c
|
add note that the encoding is a first approximation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-04 19:11:35 -08:00 |
|
Nikolaj Bjorner
|
b9528b1c56
|
update self-validator to handle root expressions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-04 19:06:30 -08:00 |
|
Nikolaj Bjorner
|
548b9d091f
|
move libz3.so from lib to bin, remove lib from distribution
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-04 18:23:46 -08:00 |
|
Nikolaj Bjorner
|
7970e4fe51
|
add clause persistence to sat/smt solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-04 16:42:10 -08:00 |
|
Nikolaj Bjorner
|
3cec3fc63d
|
bypass replaying new clause within propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-04 15:26:17 -08:00 |
|
Nikolaj Bjorner
|
3b90816025
|
add option to persist clauses #7109
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-04 11:15:59 -08:00 |
|
Nikolaj Bjorner
|
a2fa4ff1bc
|
update assembly names
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-03 16:52:20 -08:00 |
|
Nikolaj Bjorner
|
c9267055c2
|
update assembly names
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-03 16:14:03 -08:00 |
|
Nikolaj Bjorner
|
b9bec1861a
|
copy over dotnet files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-03 16:08:31 -08:00 |
|
Nikolaj Bjorner
|
bc70282a18
|
mute some compiler warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-03 15:42:06 -08:00 |
|
Nikolaj Bjorner
|
9425c419ad
|
port remaining egraph update
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-03 15:38:05 -08:00 |
|
Nikolaj Bjorner
|
a5a819c291
|
port updates to egraph from poly
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-03 12:48:58 -08:00 |
|
Nikolaj Bjorner
|
24ffef8ac5
|
fix typo
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-03 12:26:27 -08:00 |
|
Nikolaj Bjorner
|
e295ac93af
|
update build-win-signed-cmake
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-03 11:46:11 -08:00 |
|
Nikolaj Bjorner
|
e398f84e85
|
update build-win-signed-cmake
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-03 11:35:13 -08:00 |
|
Nikolaj Bjorner
|
10d56d9af9
|
fixes, updates
|
2024-02-02 16:54:49 -08:00 |
|
Nikolaj Bjorner
|
bd082ab653
|
update mk-win-dist-cmake
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-02 16:33:27 -08:00 |
|
Nikolaj Bjorner
|
14fb235dd8
|
update mk-win-dist-cmake
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-02 16:16:19 -08:00 |
|
Nikolaj Bjorner
|
736d6348e6
|
move windows builds to use mk_win_dist_cmake in nightly
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-02 13:05:01 -08:00 |
|
Nikolaj Bjorner
|
cfc8774dac
|
move windows builds to use mk_win_dist_cmake in nightly
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-02 13:04:09 -08:00 |
|
Nikolaj Bjorner
|
05d625bf0b
|
fixing paths and re-add arm64
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-02 11:07:17 -08:00 |
|
Nikolaj Bjorner
|
485a018c59
|
add back legacy build-win-signed
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-02 09:57:47 -08:00 |
|
Nikolaj Bjorner
|
9db834c223
|
add back legacy build-win-signed
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-02 09:57:47 -08:00 |
|
Yisu Remy Wang
|
2280e9562a
|
Improve instructions for working with the Julia API (#7108)
|
2024-02-02 09:46:31 -08:00 |
|
Nikolaj Bjorner
|
0d24ec3613
|
add 'dist' to folder path
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-02 09:45:38 -08:00 |
|
Jakob Rath
|
57324e953e
|
return propagated interval from viable::explain
|
2024-02-02 17:14:07 +01:00 |
|
Jakob Rath
|
85ef6b721e
|
can handle equal size now, weaken fixed_claim to avoid crash
|
2024-02-02 16:42:06 +01:00 |
|
Jakob Rath
|
52c6fd98fd
|
propagate from containing slice: consider e->bit_width
|
2024-02-02 15:00:24 +01:00 |
|
Jakob Rath
|
394f25a42f
|
viable display
|
2024-02-02 14:51:41 +01:00 |
|