Nikolaj Bjorner
|
293627c889
|
fix #6513
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-30 09:55:33 -08:00 |
|
Nikolaj Bjorner
|
07ab4d38b6
|
fix #6513
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-30 09:55:10 -08:00 |
|
Nikolaj Bjorner
|
1c7ac12af8
|
wip
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-29 20:07:14 -08:00 |
|
Nikolaj Bjorner
|
f8a3e428ff
|
wip
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-29 19:30:14 -08:00 |
|
Nikolaj Bjorner
|
96341d7f0a
|
wip try_add_mul_bound2
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-29 18:31:39 -08:00 |
|
Nikolaj Bjorner
|
ed76da1458
|
Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat
|
2022-12-29 16:55:56 -08:00 |
|
Nikolaj Bjorner
|
10589d59ba
|
wip based on notes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-29 16:55:46 -08:00 |
|
Clemens Eisenhofer
|
6f78c33558
|
Generalized variable elimination
|
2022-12-29 22:36:04 +01:00 |
|
Nuno Lopes
|
47324af210
|
be nicer when memout is reached in SMT internalize: return undef rather than crashing
|
2022-12-29 11:08:57 +00:00 |
|
Nikolaj Bjorner
|
ab9a9d2308
|
wip - more general ranges for add_mul_bound
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-28 14:09:51 -08:00 |
|
Clemens Eisenhofer
|
658877365c
|
Moved "easy part" of variable elimination to saturation.cpp
|
2022-12-28 15:07:03 +01:00 |
|
Nikolaj Bjorner
|
b4f5225ab3
|
outline
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-27 21:40:31 -08:00 |
|
Nikolaj Bjorner
|
6f8b3a997e
|
add max forbidden based on constant intervals
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-27 20:49:17 -08:00 |
|
Nikolaj Bjorner
|
45e772b223
|
Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat
|
2022-12-27 20:20:59 -08:00 |
|
Nikolaj Bjorner
|
b52379fe88
|
update
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-27 20:20:51 -08:00 |
|
Nikolaj Bjorner
|
7cc58c9cc3
|
Merge branch 'master' of https://github.com/z3prover/z3
|
2022-12-27 20:19:39 -08:00 |
|
Nikolaj Bjorner
|
ec74a87423
|
fix #6510
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-27 20:19:26 -08:00 |
|
Nikolaj Bjorner
|
3e8cbb6611
|
#5884
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-27 18:07:57 -08:00 |
|
Nikolaj Bjorner
|
abef260d67
|
Merge branch 'master' of https://github.com/z3prover/z3
|
2022-12-27 12:03:49 -08:00 |
|
Nikolaj Bjorner
|
bc19992543
|
add doc for ackermannize
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-27 12:02:08 -08:00 |
|
Clemens Eisenhofer
|
28e9014401
|
Merge branch 'polysat' of https://github.com/Z3Prover/z3 into polysat
|
2022-12-27 08:48:04 +01:00 |
|
Clemens Eisenhofer
|
4b8577eaa2
|
Reverted unintended changes
|
2022-12-27 08:47:27 +01:00 |
|
Clemens Eisenhofer
|
39a4bb025b
|
Propagate assignment if all bits are assigned and use better justification if any found
|
2022-12-27 08:44:55 +01:00 |
|
Nikolaj Bjorner
|
8d332cc3a1
|
#6508 (#6509)
|
2022-12-26 15:42:04 -08:00 |
|
Nikolaj Bjorner
|
6fab4fec23
|
#6508
|
2022-12-26 15:36:58 -08:00 |
|
Nikolaj Bjorner
|
b9c4f5d4fa
|
#6506
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-25 18:33:01 -08:00 |
|
Nikolaj Bjorner
|
8efaaaf249
|
Fix #6503
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-25 17:29:06 -08:00 |
|
Nikolaj Bjorner
|
67b9ecbd97
|
missing disequality parity constraint
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-25 16:13:26 -08:00 |
|
Nikolaj Bjorner
|
4c6499f28b
|
updated notes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-25 15:28:34 -08:00 |
|
Nikolaj Bjorner
|
be5b6f2839
|
add analysis
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-25 15:14:40 -08:00 |
|
Nikolaj Bjorner
|
403a126642
|
remove try_factor_equality1
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-25 11:37:55 -08:00 |
|
Clemens Eisenhofer
|
52eefb6e85
|
Some more commenting
|
2022-12-25 12:51:13 +01:00 |
|
Clemens Eisenhofer
|
74ec28201e
|
Merge remote-tracking branch 'Z3Prover/polysat' into polysat
|
2022-12-25 12:41:39 +01:00 |
|
Clemens Eisenhofer
|
674e309fa3
|
... and backtracking for bits
|
2022-12-25 12:23:49 +01:00 |
|
Nikolaj Bjorner
|
49a7f8446d
|
disable match_non_max and match_non_zero
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-24 15:19:37 -08:00 |
|
Nikolaj Bjorner
|
e978b81c7a
|
add review comment to bug location
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-24 12:40:47 -08:00 |
|
Nikolaj Bjorner
|
48cd05c725
|
introduce try_factor_equality2, disabled as it exposes new bugs. Old bug on bench15.smt2 exposed in debug mode
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-24 12:05:54 -08:00 |
|
Clemens Eisenhofer
|
173fb9c2bd
|
Bit-Propagation for most operations (Backtracking missing)
|
2022-12-24 16:37:53 +01:00 |
|
Nikolaj Bjorner
|
4e0604bc22
|
add hooks for multiplication overflow
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-23 15:48:03 -08:00 |
|
Nikolaj Bjorner
|
d18a2427a4
|
notes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-23 14:57:56 -08:00 |
|
Nikolaj Bjorner
|
50cbe2659a
|
extract multiple bounds for upper/lower bound
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-23 14:52:41 -08:00 |
|
Nikolaj Bjorner
|
9275930f50
|
fix bug in add-overflow propagation, move to use viable to mind for bounds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-23 13:38:51 -08:00 |
|
Nikolaj Bjorner
|
9fefa0040f
|
added updated bounds propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-23 12:47:17 -08:00 |
|
Nikolaj Bjorner
|
6f8fb39bc9
|
added updated bounds propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-23 12:29:47 -08:00 |
|
Jakob Rath
|
fda93c97f5
|
Try bounds propagation for the example case
|
2022-12-23 18:15:40 +01:00 |
|
Jakob Rath
|
993996c8a5
|
Negate premise in lemma; fixes (or at least hides) the segfault
|
2022-12-23 17:18:10 +01:00 |
|
Jakob Rath
|
19e44e4f57
|
update tests
|
2022-12-23 11:44:10 +01:00 |
|
Jakob Rath
|
68b74ca6a7
|
parity debugging
|
2022-12-23 11:42:45 +01:00 |
|
Nikolaj Bjorner
|
1434c1117c
|
wip - initial stab at bounds propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-22 21:49:33 -08:00 |
|
Nikolaj Bjorner
|
ce5cbefc56
|
fix missing parity propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-12-22 17:54:40 -08:00 |
|