Nikolaj Bjorner
ab43d2dcf1
fix semantics of check-int64 div operation to align with smtlib semantics
2025-01-29 04:29:38 -08:00
Nikolaj Bjorner
30d72f79ac
remove verbose output of overflow
2025-01-29 03:48:11 -08:00
Nikolaj Bjorner
3379155a63
add check for root literal assignment
2025-01-29 03:14:14 -08:00
Nikolaj Bjorner
fe5d17d515
handle exception internally, avoid passing rationals to integer operations
2025-01-28 20:09:59 -08:00
Nikolaj Bjorner
5b175c1bcd
fix crashes in sls_datatype
2025-01-28 19:24:32 -08:00
Nikolaj Bjorner
fe713eb8e9
disable quadratic moves for non-integers as sqrt isn't currently defined for rationals
2025-01-28 16:53:12 -08:00
Nikolaj Bjorner
d8430810fe
fix mixup between sync and sls managed variables
2025-01-28 16:35:50 -08:00
Nikolaj Bjorner
fa605454fb
fix crash reported by Nikhil on F* due to unhandled exception while using the rewriter during search
2025-01-28 16:27:28 -08:00
Nikolaj Bjorner
5c2a9d9936
fix pickup of new constraints
2025-01-28 15:04:13 -08:00
Nikolaj Bjorner
1676378be9
skip last power
2025-01-28 15:03:01 -08:00
Nikolaj Bjorner
8a7d971264
Update sls_bv_lookahead.h
2025-01-28 15:02:45 -08:00
Nikolaj Bjorner
2ebc647079
skip update stack items that are not Bool/bv
2025-01-28 15:02:33 -08:00
Nikolaj Bjorner
632e2b56e4
fix initialization of mod terms
2025-01-28 15:01:50 -08:00
Nikolaj Bjorner
fd5f5feb40
add cmake option to turn on asan
2025-01-28 15:01:31 -08:00
Nikolaj Bjorner
a8279dd9d5
reset kv map consistently with egraph
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-01-27 17:09:38 -08:00
Nikolaj Bjorner
57a5474ab4
revert flat default
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-01-27 16:56:12 -08:00
Nikolaj Bjorner
72ae161307
compress store array before model-eval rewriter sees it
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-01-27 16:55:07 -08:00
Nikolaj Bjorner
fe1622b592
sls fixes for ABV. Axiomatization required as saturation can produce conflicts by congruence closure
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-01-27 15:16:13 -08:00
Jonáš Fiala
2050fc3b35
Preserve fingerprint in trace ( #7534 )
2025-01-27 13:09:48 -08:00
Can Cebeci
2d8f024680
Mark fixed_eq literals as relevant ( #7533 )
2025-01-27 11:10:46 -08:00
Nikolaj Bjorner
63f9fdaf3e
fix build
2025-01-27 10:52:21 -08:00
Nikolaj Bjorner
15ee879602
fix #7532
2025-01-27 10:51:12 -08:00
Nikolaj Bjorner
b6e7b80704
updates to handle bugs exposed by qf-abv for local search
...
- ctx.is_true(e) - changed to work with expressions that are not literals, but come from top-level assertions
- set fixed in sls_bv_fixed to work with non-zero low order bits
- array plugin to deal with cases where e-graph is inconsistent after a merge.
2025-01-27 10:35:29 -08:00
Nikolaj Bjorner
7ffed8613a
fix bug with handling theory symbols of bit-vector type. Happens for data-type accessors. Reported by Clemens Eisenhofer
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-01-27 08:22:33 -08:00
Nikolaj Bjorner
09e84e0448
fix crash when accessing bool-info vars, reported by Clemens Eisenhofer
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-01-27 07:28:20 -08:00
Hari Govind V K
f574950237
fix #7521 ( #7531 )
2025-01-26 17:52:06 -08:00
Nikolaj Bjorner
5634dc5875
fix model construction bug: ignore non-relevant expressions when building model
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-01-26 17:50:15 -08:00
Nikolaj Bjorner
d3bf25ce85
throttle value smt -> sls
2025-01-26 14:16:43 -08:00
Nikolaj Bjorner
d4100fc472
fixes to update propagation.
...
rename update and update_args_value to
update_checked
update_unchecked
ensure upward propagation so that local values are consistent when entering lookahead solvers.
2025-01-26 12:55:03 -08:00
Nikolaj Bjorner
04d0e9492b
set log level of revert repair down to 3
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-01-26 11:56:59 -08:00
Nikolaj Bjorner
55fc57b5c7
relax out of range restrictions to handle large intervals
2025-01-26 11:24:26 -08:00
Nikolaj Bjorner
4f2272dbb2
increase log level for 'set value failed'
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-01-25 23:43:53 -08:00
Nikolaj Bjorner
7fb6497ce1
fix return value when in external mode bool-flip
...
return null_bool_var instead of false (= 0).
2025-01-25 22:57:58 -08:00
Nikolaj Bjorner
d4f2de734b
add smt_params dependency to sls in cmakelists
2025-01-25 22:38:32 -08:00
Nikolaj Bjorner
12e8082d86
consolidate functionality
2025-01-25 22:34:58 -08:00
Nikolaj Bjorner
a7010574c8
align use_list with number of variables during flatten, push clause and bool_vars_of addition into clause and atom creation time.
2025-01-25 20:47:57 -08:00
Nikolaj Bjorner
7fc59b65ad
add recursive updates to lookahead
2025-01-25 16:10:00 -08:00
Nikolaj Bjorner
57cb988461
fix gcc build
2025-01-25 15:51:58 -08:00
Nikolaj Bjorner
60fb53ad34
fix debug build
2025-01-25 15:50:07 -08:00
Nikolaj Bjorner
ecc302bdc8
fix trace build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-01-25 11:38:58 -08:00
Nikolaj Bjorner
d805322dfb
create separate file for expression based lookahead solver
2025-01-25 11:19:40 -08:00
Nikolaj Bjorner
f6e7dcff47
Fix crash exposed in QF_UFNIA
2025-01-24 15:31:10 -08:00
Nikolaj Bjorner
9e8dd68ee6
disable lookahead on compound values (fixes bug reported by Clemens), bail to rationals when there are reals.
2025-01-24 11:01:18 -08:00
Nikolaj Bjorner
053349cd36
remove incorrect calls to VERIFY in array solver
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-01-24 09:54:21 -08:00
Nikolaj Bjorner
0e8969ce60
deal with compiler warnings and include value exchange prior to final check.
2025-01-24 09:40:33 -08:00
Nikolaj Bjorner
ce615ee116
avoid repeated clauses during scoring function
2025-01-23 10:51:12 -08:00
Nikolaj Bjorner
b149d1f803
count every lookahead as activity
2025-01-22 22:57:43 -08:00
Nikolaj Bjorner
4d33f442b9
enable value import in parallel mode
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-01-22 22:45:01 -08:00
Nikolaj Bjorner
e32f685f14
disable backoff on smt->sls value export
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-01-22 22:15:10 -08:00
Nikolaj Bjorner
beb9d2e553
update restart next
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-01-22 21:40:35 -08:00
