Nikolaj Bjorner
|
a199151f09
|
revamp propagation to bottom-up from bounds to occurrences in polynomials
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2026-01-18 11:51:59 -08:00 |
|
Nikolaj Bjorner
|
5d5a2bac32
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2026-01-15 21:47:57 -08:00 |
|
Nikolaj Bjorner
|
7b01f263f4
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2026-01-15 16:42:08 -08:00 |
|
Nikolaj Bjorner
|
2720d9ae59
|
incremental update
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2026-01-15 10:30:35 -08:00 |
|
Nikolaj Bjorner
|
7198aa22be
|
current dump
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2026-01-12 10:37:53 -08:00 |
|
Nikolaj Bjorner
|
e933e64858
|
porting to v4 or v5 of engine
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2026-01-07 20:22:19 -08:00 |
|
Nikolaj Bjorner
|
30f859a1f6
|
refine stellensatz solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2026-01-06 16:23:15 -08:00 |
|
Nikolaj Bjorner
|
f1b21ecbcc
|
fix unsound bounds propagaiton
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-12-31 16:30:21 -08:00 |
|
Nikolaj Bjorner
|
dd0ccce612
|
update case split strategy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-12-31 13:40:42 -08:00 |
|
Nikolaj Bjorner
|
9b8558ed92
|
throttle decision rounds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-12-30 17:32:21 -08:00 |
|
Nikolaj Bjorner
|
038ff121ed
|
updated heuristic to select bounds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-12-30 15:14:53 -08:00 |
|
Nikolaj Bjorner
|
8cf1e51b9f
|
update tabu policy, enable more propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-12-27 17:14:27 -08:00 |
|
Nikolaj Bjorner
|
01f79ebb76
|
tweaks and fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-12-26 15:00:36 -08:00 |
|
Nikolaj Bjorner
|
4c09ab27bc
|
tweaks and fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-12-26 14:59:56 -08:00 |
|
Nikolaj Bjorner
|
6ec3b59ad9
|
clean up, add comments
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-12-23 15:15:50 -08:00 |
|
Nikolaj Bjorner
|
9d714f0ab9
|
resurrect model-value based repair. Interleave with bounds splits
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-12-23 11:25:55 -08:00 |
|
Nikolaj Bjorner
|
65a57696af
|
price-fee working
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-12-22 09:11:31 -08:00 |
|
Nikolaj Bjorner
|
903f4d9261
|
wip
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-12-21 10:09:37 -08:00 |
|
Nikolaj Bjorner
|
8377428a17
|
ingest copilot bug fixs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-12-16 07:45:40 -08:00 |
|
Nikolaj Bjorner
|
c2bea4b493
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-12-16 07:38:16 -08:00 |
|
Nikolaj Bjorner
|
897f2b0f30
|
comments
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-12-13 15:24:41 +00:00 |
|
Nikolaj Bjorner
|
16bad349ce
|
code updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-12-13 14:53:27 +00:00 |
|
Nikolaj Bjorner
|
2aed71a91f
|
updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-12-12 23:14:06 +00:00 |
|
Nikolaj Bjorner
|
1887718da2
|
updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-12-12 00:26:23 +01:00 |
|
Nikolaj Bjorner
|
21dc38048f
|
fixing cause of divergence
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-12-03 16:37:45 -08:00 |
|
Nikolaj Bjorner
|
f352cc6393
|
various code bug fixes and algorithm fixes in factorization and tracking progress
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-12-02 20:30:54 -08:00 |
|
Nikolaj Bjorner
|
cbe1fc5474
|
fix bug checking for strictness before abandoning resolution
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-12-02 01:53:06 -08:00 |
|
Nikolaj Bjorner
|
d09dfaf57b
|
updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-30 17:35:46 -08:00 |
|
Nikolaj Bjorner
|
5381cb338f
|
turn on 3rd gen saturation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-30 08:59:18 -08:00 |
|
Nikolaj Bjorner
|
5438d5ad89
|
remove extraction of linear cores because it examines a stale core instead of the current core. A reintroduction of this feature would have to extract the lemma before the next solver call and save it aside in case the solver call returns l_undef
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-25 19:24:57 -08:00 |
|
Nikolaj Bjorner
|
151be6ac9a
|
statistics and configuable
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-22 16:48:15 -08:00 |
|
Nikolaj Bjorner
|
e44994b9a4
|
stellensatz fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-22 10:15:14 -08:00 |
|
Nikolaj Bjorner
|
ee63585581
|
update model-guide heuristic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-21 15:52:37 -08:00 |
|
Nikolaj Bjorner
|
ed84b14e6c
|
fixing coi bug
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-20 17:55:37 -08:00 |
|
Nikolaj Bjorner
|
7b265ba162
|
fix poly model bug
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-20 14:24:08 -08:00 |
|
Nikolaj Bjorner
|
b3f7d16606
|
fix memory leaks and handling of non-integer term coefficients
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-20 11:59:12 -08:00 |
|
Nikolaj Bjorner
|
2578218b6f
|
add new option for adding tangent lemmas for integer monomials
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-20 11:30:07 -08:00 |
|
Nikolaj Bjorner
|
fc96f827a1
|
updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-20 10:32:51 -08:00 |
|
Nikolaj Bjorner
|
823800541e
|
updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-19 14:02:27 -08:00 |
|
Nikolaj Bjorner
|
5d316a51d1
|
enable bound tracking
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-19 10:53:42 -08:00 |
|
Nikolaj Bjorner
|
5de01e5d1d
|
add stubs for bounds refinement
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-19 10:42:28 -08:00 |
|
Nikolaj Bjorner
|
179601ffac
|
testing model repair
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-18 14:14:54 -08:00 |
|
Nikolaj Bjorner
|
4df7ee67f5
|
updated sketch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-17 22:06:29 -08:00 |
|
Nikolaj Bjorner
|
92bc39dab5
|
add toggle to use polynomial translation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-17 20:52:34 -08:00 |
|
Nikolaj Bjorner
|
33709d3abb
|
add toggle to use polynomial translation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-17 17:28:28 -08:00 |
|
Nikolaj Bjorner
|
2eca05e59a
|
fix crash
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-17 09:57:17 -08:00 |
|
Nikolaj Bjorner
|
12df8f593e
|
reshuffle if conditions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-16 17:24:31 -08:00 |
|
Nikolaj Bjorner
|
e9905c05b1
|
fix crash
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-16 17:21:23 -08:00 |
|
Nikolaj Bjorner
|
711572e73c
|
fix crash on arie branch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-16 16:58:33 -08:00 |
|
Nikolaj Bjorner
|
b835bd4c92
|
self-contained tracking of values
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-16 12:55:58 -08:00 |
|