Jakob Rath
7311af699c
fix
2024-03-11 15:02:55 +01:00
Jakob Rath
d11c2b3265
Add ule_constraint simplification
2024-03-11 14:20:29 +01:00
Nikolaj Bjorner
2fdf2233f9
move side effect out of print statement
2024-03-11 04:08:07 -07:00
Nikolaj Bjorner
e8ac3aa88c
port fixes to intblast
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-03-09 09:43:14 -08:00
Jakob Rath
183e911a79
Merge remote-tracking branch 'origin/master' into poly
2024-02-26 11:46:22 +01:00
Jakob Rath
b2166da464
add code for offline validation
2024-02-26 10:57:39 +01:00
Jakob Rath
94e2e0c3e6
pass along lemma name
2024-02-26 10:51:01 +01:00
Jakob Rath
b561795214
fix
2024-02-26 10:40:37 +01:00
Jakob Rath
3eb42cdf4b
minor changes
2024-02-08 15:25:00 +01:00
Jakob Rath
705203ea4c
display
2024-02-08 15:13:22 +01:00
Jakob Rath
8d45c954c5
enable new propagate_from_containing_slice
2024-02-08 15:11:36 +01:00
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
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
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
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
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
Nikolaj Bjorner
5cac9b84e4
fix build warnings
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-01 09:36:52 -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
bdb9106f99
Api ( #7097 )
...
* rename ul_pair to column
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* simple test passed
* remove an assert
* relax an assertion
* remove an obsolete function
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* access a term by the term column
* remove the column index from colunm.h
* remove an unused method
* remove debug code
* fix the build of lp_tst
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---------
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Lev Nachmanson <levnach@hotmail.com>
2024-01-24 16:05:18 -08:00
Nikolaj Bjorner
8d4e7fac6b
add diagnostics option to new arithmetic solver
2024-01-22 16:23:55 -08: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
7486e8724f
track quantifier instantiation method in proof hint #7080
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-01-20 17:44:07 -08:00
