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
|
3f3ac924ab
|
add debugging output
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-06 09:48:09 -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
|
10d56d9af9
|
fixes, updates
|
2024-02-02 16:54:49 -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 |
|
Nikolaj Bjorner
|
8cc146e727
|
connect call to zero extend
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-01 23:38:07 -08:00 |
|
Nikolaj Bjorner
|
38771defa1
|
bugfixes to encoding overflow conditions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-01 22:49:21 -08:00 |
|
Nikolaj Bjorner
|
ac0a786484
|
bugfixes to encoding overflow conditions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-01 22:26:32 -08:00 |
|
Nikolaj Bjorner
|
88b315cdb0
|
update names and nature of multiplication blast rules
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-01 17:12:35 -08:00 |
|
Nikolaj Bjorner
|
60add85c47
|
add saturation rules for overflow
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-01 12:55:17 -08:00 |
|
Nikolaj Bjorner
|
32e23b3b6c
|
remove unsound simplification
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-01 12:39:37 -08:00 |
|
Nikolaj Bjorner
|
6e72182194
|
remove unused propagation in umul_overflow code. Rename propagate to saturate to reflect where it gets used
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-01 09:57:28 -08:00 |
|
Nikolaj Bjorner
|
111dee9143
|
simplify overflow check up front
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-02-01 09:37:46 -08:00 |
|
Jakob Rath
|
6a1f173e03
|
extend propagate_from_containing_slice to subslices with offset > 0
|
2024-02-01 17:23:26 +01:00 |
|
Jakob Rath
|
cb6fb7b26b
|
distinguish theory_vars in output
|
2024-02-01 12:14:14 +01:00 |
|
Jakob Rath
|
0b5f163ba7
|
fix warning
|
2024-02-01 12:13:49 +01:00 |
|
Nikolaj Bjorner
|
e6f7ba90f1
|
more saturation for overflow
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-31 20:12:01 -08:00 |
|
Nikolaj Bjorner
|
7dc61ca646
|
always fail if new axioms are true
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-31 15:50:35 -08:00 |
|
Nikolaj Bjorner
|
0dc204cd4a
|
add base support for signed multiplication over/under flow
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-30 12:47:28 -08:00 |
|
Jakob Rath
|
2da3261d8a
|
make lemma sound
|
2024-01-29 17:07:17 +01:00 |
|
Jakob Rath
|
8de2503f9f
|
bugfix?
|
2024-01-29 16:51:10 +01:00 |
|
Jakob Rath
|
75527e8e19
|
propagate intervals from containing slice
|
2024-01-29 16:45:14 +01:00 |
|
Nikolaj Bjorner
|
f0b056d859
|
add ad-hoc debug output, add rule for incremental linearization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-21 11:29:48 -08:00 |
|
Nikolaj Bjorner
|
677e261bb1
|
constant overflow forbidden interval
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-15 09:46:45 -08:00 |
|
Nikolaj Bjorner
|
a68bbb53e4
|
update assign to check fixed bits afterwards
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-15 09:18:51 -08:00 |
|
Nikolaj Bjorner
|
42aad423c9
|
parent list of root may miss nodes from children if they are not congruence roots. We walk parents of all siblings to not miss
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-14 18:20:44 -08:00 |
|
Nikolaj Bjorner
|
79a2c86c05
|
fixup fixedbits again
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-14 14:38:44 -08:00 |
|
Nikolaj Bjorner
|
ff637a3989
|
fix missing propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-14 13:10:35 -08:00 |
|
Nikolaj Bjorner
|
05d61ed090
|
fix incorrect fixed_bits forbidden interval calculation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-14 12:19:04 -08:00 |
|
Nikolaj Bjorner
|
8f3e8bd0bb
|
create proper extract terms
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-14 10:37:55 -08:00 |
|
Nikolaj Bjorner
|
60ac9388c8
|
fixup merges
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-14 09:57:29 -08:00 |
|
Nikolaj Bjorner
|
ec6e2139dd
|
fix unsound merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-13 17:49:29 -08:00 |
|
Nikolaj Bjorner
|
3f369ae962
|
fix unsound merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-13 17:47:20 -08:00 |
|
Nikolaj Bjorner
|
aed48e9f9b
|
fix type of get-id
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-13 17:17:02 -08:00 |
|
Nikolaj Bjorner
|
d422f7b067
|
reorder fields
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-13 17:14:41 -08:00 |
|
Nikolaj Bjorner
|
b7306f3c0c
|
fix srem encoding
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-13 17:04:18 -08:00 |
|
Nikolaj Bjorner
|
01c5a09575
|
put ensure concat on a list
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-13 13:44:59 -08:00 |
|
Nikolaj Bjorner
|
477db7d8bd
|
fix axiomatization for sdiv
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-13 13:10:00 -08:00 |
|
Nikolaj Bjorner
|
0ca94b9c2f
|
get-theory-id
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-13 12:22:11 -08:00 |
|
Nikolaj Bjorner
|
1f23ffb23c
|
add placeholder for tracking theory justifications in EUF
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-13 11:59:01 -08:00 |
|
Nikolaj Bjorner
|
73b032ae4e
|
propagate values in euf_bv_plugin over extract
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-13 11:46:53 -08:00 |
|
Nikolaj Bjorner
|
93be3d2b2c
|
arithmetic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-13 10:29:50 -08:00 |
|
Nikolaj Bjorner
|
33c43a474d
|
fix quot-rem axioms: cannot be rewritten because it looses information
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-12 19:28:53 -08:00 |
|
Nikolaj Bjorner
|
211aff4cba
|
fix missing handling of axiom
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-01-12 18:15:26 -08:00 |
|