Nikolaj Bjorner
|
07bda4d629
|
bugfix
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-10-10 19:29:23 -07:00 |
|
Nikolaj Bjorner
|
ff975e49f2
|
use model-based FM strategy for saturation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-10-10 16:34:58 -07:00 |
|
Nikolaj Bjorner
|
ce614ac26d
|
gcd reduce and use c().val for sign constraints
|
2025-10-10 16:34:05 -07:00 |
|
Nikolaj Bjorner
|
6aeca8253b
|
generate more proper proof format
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-10-10 16:31:08 -07:00 |
|
Nikolaj Bjorner
|
df3847a379
|
v0.1 of nla saturation
|
2025-10-10 16:28:22 -07:00 |
|
Nikolaj Bjorner
|
27bcca72f1
|
fix #7948
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-10-10 15:35:37 -07:00 |
|
Nikolaj Bjorner
|
201731baf1
|
fix #7948
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-10-10 15:35:36 -07:00 |
|
Nikolaj Bjorner
|
95ab02aa4f
|
propagate value initialization to atoms
|
2025-10-10 15:35:35 -07:00 |
|
Arie Gurfinkel
|
599e9da8a9
|
optionally limit linearization
|
2025-10-06 16:40:06 -04:00 |
|
Nikolaj Bjorner
|
5846570012
|
gcd reduce and use c().val for sign constraints
|
2025-10-01 18:42:34 -07:00 |
|
Nikolaj Bjorner
|
538480b4f8
|
limit sos loop
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-30 13:51:05 -07:00 |
|
Nikolaj Bjorner
|
3b1ac52ff9
|
generate more proper proof format
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-30 07:42:27 -07:00 |
|
Nikolaj Bjorner
|
4162d89170
|
move to lex-leading resolvents
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-29 19:21:30 -07:00 |
|
Nikolaj Bjorner
|
fa2d7a1c57
|
fix introduced memory leak
|
2025-09-29 18:33:47 -07:00 |
|
Nikolaj Bjorner
|
c3281f08ef
|
wip
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-29 16:14:59 -07:00 |
|
Nikolaj Bjorner
|
69a9d9f0b0
|
move to global occurs list, throttle saturation lemmas based on monomial size
|
2025-09-29 08:57:49 -07:00 |
|
Nikolaj Bjorner
|
eff17a6252
|
notes
|
2025-09-29 04:52:51 -07:00 |
|
Nikolaj Bjorner
|
81cffee736
|
add factorization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-29 04:29:54 -07:00 |
|
Nikolaj Bjorner
|
184fae6fcc
|
wip stellensatz
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-28 23:06:35 +03:00 |
|
Nikolaj Bjorner
|
72f5fe1f7f
|
logging and bug fixes
|
2025-09-28 18:16:23 +03:00 |
|
Nikolaj Bjorner
|
c621f59740
|
fix bug with saturation of monotonicity, and add more general case for downward saturation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-28 14:36:53 +03:00 |
|
Nikolaj Bjorner
|
e684537b01
|
retrieve both bounds and explanations recursively
|
2025-09-28 13:46:22 +03:00 |
|
Nikolaj Bjorner
|
360de4af03
|
add basic linearization as pre-processing and refinement
|
2025-09-28 12:27:13 +03:00 |
|
Nikolaj Bjorner
|
a12f4b9686
|
prepare for enforcing cheap incremental linearization axioms
|
2025-09-27 20:33:53 +03:00 |
|
Nikolaj Bjorner
|
ad11e4626e
|
household
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-27 16:59:22 +03:00 |
|
Nikolaj Bjorner
|
88844a84aa
|
mul-saturation wip
fixup conflict explanations in mul_saturation, add parameter to enable it, add statistics
|
2025-09-27 12:17:40 +03:00 |
|
Nikolaj Bjorner
|
ef27e38d5f
|
v0.1 of nla saturation
|
2025-09-26 23:05:02 +03:00 |
|
Nikolaj Bjorner
|
6adb234673
|
outline for adding monomials
|
2025-09-26 12:03:26 +03:00 |
|
Nikolaj Bjorner
|
a6ea667776
|
fix access to k'th emon
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-23 11:31:23 +03:00 |
|
Nikolaj Bjorner
|
08ef4de4a6
|
introduce shuffle
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-23 11:24:50 +03:00 |
|
Nikolaj Bjorner
|
3c9ab28731
|
remove secondary random traversal
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-23 11:16:16 +03:00 |
|
Nikolaj Bjorner
|
18d7231c4c
|
latent bug found with relevancy filtering
|
2025-09-23 10:46:33 +03:00 |
|
Nikolaj Bjorner
|
0ed37be40f
|
missing update
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-22 15:30:32 +03:00 |
|
Nikolaj Bjorner
|
9579064671
|
setup
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-22 15:19:40 +03:00 |
|
Nikolaj Bjorner
|
b02b0cf31f
|
fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-22 14:44:50 +03:00 |
|
Nikolaj Bjorner
|
db5a991257
|
more imp notes and relevancy experiment
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-22 12:44:50 +03:00 |
|
Nikolaj Bjorner
|
0a0e925f27
|
updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-22 11:26:48 +03:00 |
|
Nikolaj Bjorner
|
fae67b79b7
|
outline
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-22 10:55:08 +03:00 |
|
Nikolaj Bjorner
|
dcdae5a61c
|
add smt debug output for nla_core
|
2025-09-21 19:24:13 +03:00 |
|
Nikolaj Bjorner
|
a8ae52bfbf
|
fix missing call change to cross-nested. Prepare for lower-bound and upper-bound cardinality constraints
|
2025-09-19 18:57:50 -07:00 |
|
Nikolaj Bjorner
|
2517b5a40a
|
port improvements from ilana branch to master regarding nla
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-19 12:28:31 -07:00 |
|
Nikolaj Bjorner
|
6752be7263
|
Remove unused variable in polynomial.cpp
Removed unused variable 'sz2' in polynomial multiplication.
|
2025-09-15 10:43:09 -07:00 |
|
Nikolaj Bjorner
|
b0bc41457f
|
Update polynomial.cpp
|
2025-09-15 10:41:56 -07:00 |
|
Nikolaj Bjorner
|
7efcda2674
|
Update polynomial.cpp
|
2025-09-15 09:46:29 -07:00 |
|
Nikolaj Bjorner
|
f4a87d4f61
|
shelve experiment with a variant of geobuckets
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-15 09:46:29 -07:00 |
|
Nikolaj Bjorner
|
0d0dd0315a
|
evaluate unhandled arithmetic operators based on an initialized model #7876
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-14 06:45:36 -07:00 |
|
Nikolaj Bjorner
|
573c2cb8f7
|
micro tuning perfect square test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-13 20:10:43 -07:00 |
|
Nikolaj Bjorner
|
866393a842
|
update defaults for new grobner featuers
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-05 14:34:03 -07:00 |
|
Nikolaj Bjorner
|
d7718623a4
|
handle case where all variables are bounded
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-04 12:58:03 -07:00 |
|
Nikolaj Bjorner
|
98a9a34f2b
|
add option to reduce pseudo-linear monomials
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-09-04 11:04:12 -07:00 |
|