Nikolaj Bjorner
eb97fcc273
mild refactoring
2025-03-16 12:24:41 -07:00
Nikolaj Bjorner
0e881e7abb
fix #7584
2025-03-15 13:33:08 -07:00
Nikolaj Bjorner
7c226f40df
fix #4117
2025-03-12 20:14:36 -07:00
Nikolaj Bjorner
13c098f4b2
better equality solving pre-processing with bv
2025-03-12 17:18:26 -07:00
Nikolaj Bjorner
d980ac9a05
fix #7582
2025-03-12 17:17:47 -07:00
Nikolaj Bjorner
fa5a50c4f9
fix #7295
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-03-12 11:43:31 -07:00
Nikolaj Bjorner
07fa36e37a
fix #7466
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-03-09 18:50:07 -07:00
Nikolaj Bjorner
ea1360ee46
fix #7578
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-03-09 17:01:42 -07:00
Nikolaj Bjorner
c002c77e5a
fix #7569
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-03-07 11:53:01 -08:00
Nikolaj Bjorner
80f00f191a
fix #7572 and fix #7574
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-03-07 10:46:29 -08:00
Nikolaj Bjorner
d24c488482
fix error in mk_nuget_task.py
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-02-28 18:19:36 -08:00
Nikolaj Bjorner
a97e5fcf0e
fix error in mk_nuget_task.py
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-02-28 18:18:51 -08:00
Nikolaj Bjorner
ec93972356
fixup unit tests
2025-02-27 17:18:53 -08:00
Nikolaj Bjorner
b784b748d4
fix #7550
2025-02-27 14:43:11 -08:00
Nikolaj Bjorner
83ee21cd22
streamline tracing
2025-02-27 14:42:35 -08:00
Nikolaj Bjorner
db997cd64d
fix regression, missing idx increment in iterator loop #7566
2025-02-25 01:52:42 -08:00
Lev Nachmanson
a7310462df
throttle down cuts from proofs
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-23 19:38:35 -08:00
Nikolaj Bjorner
be8febedc3
add throttle, fixup bp.init() for proper initialization
2025-02-22 16:27:58 -08:00
Nikolaj Bjorner
c79967b2b6
using iterators
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-02-21 19:20:49 -08:00
Lev Nachmanson
67d77e26d2
remove a parameter when calling bound_analyzer_on_row
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-21 14:43:08 -08:00
Lev Nachmanson
b985838112
do not pass row index to bound_analyzer_on_row
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-21 14:38:40 -08:00
Nikolaj Bjorner
10c2af85c1
try for mixed-mode
2025-02-21 13:24:37 -08:00
Nikolaj Bjorner
ead8478046
fix build per new API for analyze_row
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-02-21 12:48:34 -08:00
Nikolaj Bjorner
1a3d1ad69d
add base line bounds tightening utility
2025-02-21 12:46:51 -08:00
Lev Nachmanson
7044bb8485
remove an unused parameter in bound_analyzer_on_row
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-21 10:17:43 -10:00
Nikolaj Bjorner
fbfbfa5d76
print column value
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-02-20 09:55:39 -08:00
Hari Govind V K
f50f21198e
Fix #7505 ( #7565 )
...
* fix #7505
* rename
2025-02-20 09:54:59 -08:00
Lev Nachmanson
bd3d288a08
tighten only core constrants
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-20 08:40:16 -08:00
Nikolaj Bjorner
45ad61438a
added logging
2025-02-19 17:40:59 -08:00
Nikolaj Bjorner
1fec0fa35b
remove verbose output
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-02-19 15:35:51 -08:00
Nikolaj Bjorner
01fbc0e8e7
fix #7563
2025-02-19 14:55:27 -08:00
Nikolaj Bjorner
712231dcda
fix #7560
2025-02-19 09:39:17 -08:00
Nikolaj Bjorner
075773e519
remove proviso for single index arrays
2025-02-19 00:02:38 -08:00
Nikolaj Bjorner
3e5abef145
fix #7549
2025-02-18 21:38:06 -08:00
Nikolaj Bjorner
e0945f57bb
fix #7554
...
mbp_qel uses two iterations of saturation.
The first iteration uses only congruences, not the model.
The second iteration uses the model.
Terms are marked as "seen" during either iteration and will not be reprocessed if they are "seen".
All select terms get marked as "seen" to avoid reproducing Ackerman axioms.
But this conflicts with expanding select-store axioms during
the phase of saturation where use_model is allowed.
2025-02-18 21:04:34 -08:00
Nikolaj Bjorner
28f3f8046e
#7559
2025-02-18 20:50:06 -08:00
Nikolaj Bjorner
11066486d7
#7559
2025-02-18 20:48:13 -08:00
Nikolaj Bjorner
991cffb519
handle multi-arity arrays
2025-02-18 20:38:45 -08:00
Nikolaj Bjorner
674e1b8f98
remove equality check on container
2025-02-18 20:15:42 -08:00
Nikolaj Bjorner
ce69b54b5f
adjust select/store rule for n-ary arrays
2025-02-18 20:08:56 -08:00
Nikolaj Bjorner
42f6e1300a
more review of mbp_arrays
2025-02-18 19:48:54 -08:00
Nikolaj Bjorner
a4a84ed083
arrays are not necessarily unary
2025-02-18 19:13:12 -08:00
Nikolaj Bjorner
a5e5a35755
code simplification
2025-02-18 19:07:58 -08:00
Nikolaj Bjorner
a143ed3bff
taking a look at mbp_qel for arrays
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-02-18 16:28:49 -08:00
Nikolaj Bjorner
813da35539
fix unit test
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-02-17 20:36:38 -08:00
Nikolaj Bjorner
f8f26788ad
convert def into expression tree
...
prior data-structure could not represent
((1 + x) div 2) * 2
It is possible to have nested expressions with div.
To deal with this, replace original def by an expression tree data-structure.
2025-02-17 18:47:00 -08:00
Nikolaj Bjorner
f977b48161
adjust solve_for to handle rationals
2025-02-17 13:59:23 -08:00
Nikolaj Bjorner
528efbb535
fixes to failure conditions for unification
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-02-16 13:41:17 -08:00
Nikolaj Bjorner
fe27ca1dd0
remove verbose output
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-02-16 13:23:56 -08:00
Nikolaj Bjorner
50f9fddfd2
Add unification based projection function
...
Heuristic for EMBPR is to unify terms that occur in uninterpreted contents. Walk partitions that are pure f(t) and an impure f(s)
and attempt to unify t with s ensuring that merges from s preserves satisfiability.
2025-02-16 13:18:21 -08:00
