Jakob Rath
|
aeb6138c25
|
No result if there is no other interval
|
2023-01-05 17:21:25 +01:00 |
|
Jakob Rath
|
a406e01fb8
|
e0 instead of first?
|
2023-01-05 16:44:45 +01:00 |
|
Jakob Rath
|
6f18335604
|
need y0 value
|
2023-01-05 16:43:23 +01:00 |
|
Jakob Rath
|
ffa12eb37c
|
flip args to match description
|
2023-01-05 16:43:01 +01:00 |
|
Jakob Rath
|
55a50ea461
|
ule rewrites
|
2023-01-05 14:41:21 +01:00 |
|
Jakob Rath
|
0daf444cec
|
Actually revert boolean decisions
|
2023-01-04 17:20:34 +01:00 |
|
Nikolaj Bjorner
|
db1be0f247
|
unit test for bench 13 scenario
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-01-03 12:23:14 -08:00 |
|
Clemens Eisenhofer
|
075b548089
|
Merge branch 'polysat' of https://github.com/Z3Prover/z3 into polysat
|
2023-01-03 17:48:21 +01:00 |
|
Clemens Eisenhofer
|
79e7380ffc
|
Pseudo-inverse op_constraint
|
2023-01-03 17:47:54 +01:00 |
|
Jakob Rath
|
283e60a5cb
|
compile
|
2023-01-03 14:55:50 +01:00 |
|
Nikolaj Bjorner
|
84a5ec221f
|
diagnostics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-01-02 18:11:00 -08:00 |
|
Nikolaj Bjorner
|
824c10711c
|
testing inference based on complementary bounds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-01-02 17:30:08 -08:00 |
|
Nikolaj Bjorner
|
56bda59de9
|
bugfix in parity code, add try_infer_parity_equality per status notes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2023-01-02 15:01:05 -08:00 |
|
Clemens Eisenhofer
|
0301686856
|
Variant of variable elimination
|
2023-01-02 20:05:13 +01: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 |
|
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 |
|
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
|
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 |
|