Lev Nachmanson
e0185121c5
use u_dependency in eprime_pair
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:40 -10:00
Lev Nachmanson
b20566a488
work on tighten_with_S
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:40 -10:00
Lev Nachmanson
a1a9825e43
remove a throw
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:40 -10:00
Lev Nachmanson
a75eff6525
bug fix
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:40 -10:00
Lev Nachmanson
0c6dcfedb8
small optimization
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:40 -10:00
Lev Nachmanson
9ec55de5c6
optimize dio changes
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:40 -10:00
Lev Nachmanson
7c9cb44c94
less eager dio
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:40 -10:00
Lev Nachmanson
4fea4259ec
fix the build
2025-02-03 13:30:40 -10:00
Lev Nachmanson
1a99fa56cb
handle zero rows correctly
2025-02-03 13:30:40 -10:00
Lev Nachmanson
178411ad0c
dio passes regression\smt2 tests with limited functionality
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:39 -10:00
Lev Nachmanson
dcd80ac95b
fix term_o init
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:39 -10:00
Lev Nachmanson
c29d04dc3c
debug dio
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:39 -10:00
Lev Nachmanson
1cb71b4648
debug dio
2025-02-03 13:30:39 -10:00
Lev Nachmanson
db899fd670
fix in substitution of fresh variables, clean column.h
2025-02-03 13:30:39 -10:00
Lev Nachmanson
5f71604198
bug fix in init and getting explanations
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:39 -10:00
Lev Nachmanson
0814fa40b0
create a conflict explanation
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:39 -10:00
Lev Nachmanson
53605d4e0a
a version with less pointers: got a conflict
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:30:00 -10:00
Lev Nachmanson
876cbc527d
in the middle
2025-02-03 13:24:33 -10:00
Lev Nachmanson
778db5e763
use std::list
2025-02-03 13:24:33 -10:00
Lev Nachmanson
c1e577e932
fix the crash
2025-02-03 13:24:33 -10:00
Lev Nachmanson
484af98af6
crash
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:24:33 -10:00
Lev Nachmanson
0eeef3b806
fix the build
2025-02-03 13:24:33 -10:00
Lev Nachmanson
0b9b1c4472
move some functionality from int_solver to int_solver::imp
2025-02-03 13:24:33 -10:00
Lev Nachmanson
66b778cb25
fix the build
2025-02-03 13:24:33 -10:00
Lev Nachmanson
7050589adf
prepare for calling diophantine equations
2025-02-03 13:24:33 -10:00
Lev Nachmanson
049520483f
add parameter to control calling diophantine equations
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-02-03 13:24:33 -10:00
Nikolaj Bjorner
17d47ca8c7
fix #7493
2025-02-02 15:00:31 -08:00
Nikolaj Bjorner
99cbfa715c
Add a sharp throttle to lia2card tactic to control overhead in default tactic mode
...
lia2card was added to qfuflia tactic based on a user scenario, but it overshot: lia2card is by default harmful. It is here tamed to only convert binary variables and throttle on nested ite terms
2025-02-02 13:58:51 -08:00
Nikolaj Bjorner
fd2a8a554d
disable small clause generation for propagation
2025-02-01 20:04:29 -08:00
Nikolaj Bjorner
0ef26983fc
release
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-01-31 17:31:37 -08:00
Nikolaj Bjorner
aea4490fb2
throttle overhead with lia2card
2025-01-31 12:36:59 -08:00
Nikolaj Bjorner
d465bdbb87
include extensionality constraints for arrays
2025-01-31 11:06:40 -08:00
Nikolaj Bjorner
d6dcc515eb
rehearse release
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-01-31 09:49:42 -08:00
Nikolaj Bjorner
edc5679530
updated release notes
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-01-31 09:49:16 -08:00
Nikolaj Bjorner
8ae24e2b38
update release version
2025-01-31 09:29:28 -08:00
dependabot[bot]
1d622a678e
Bump docker/build-push-action from 6.12.0 to 6.13.0 ( #7535 )
...
Bumps [docker/build-push-action](https://github.com/docker/build-push-action ) from 6.12.0 to 6.13.0.
- [Release notes](https://github.com/docker/build-push-action/releases )
- [Commits](https://github.com/docker/build-push-action/compare/v6.12.0...v6.13.0 )
---
updated-dependencies:
- dependency-name: docker/build-push-action
dependency-type: direct:production
update-type: version-update:semver-minor
...
Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
2025-01-31 09:26:49 -08:00
Clemens Eisenhofer
9557e7cacf
Minor ( #7540 )
2025-01-31 08:22:30 -08:00
Nikolaj Bjorner
1ce6e66ac9
generalize logic detection to use sub-string matching
2025-01-30 16:34:54 -08:00
Nikolaj Bjorner
eb825855fa
increase the log level on callbacks with bit-indices that get set
2025-01-30 16:34:36 -08:00
Nikolaj Bjorner
c9ac4d6f75
pre-flatten use list before iterating over m_unsat
...
select_max_same_sign accesses the use-list which may cause it to be flattened.
2025-01-30 16:34:17 -08:00
Nikolaj Bjorner
e3566288a4
fixes based on benchmarking UFDTLIA/NIA/BV
2025-01-29 17:00:26 -08:00
Nikolaj Bjorner
f1e0950069
fix several crashes exposed by QF_UFDTNIA benchmark sets
2025-01-29 16:23:38 -08:00
Nikolaj Bjorner
bfe4673dac
this check is not an invariant in the first place
...
but nice to have.
2025-01-29 16:23:18 -08:00
Nikolaj Bjorner
51357f6d06
Add selective filter on Ackerman axioms
2025-01-29 11:42:50 -08:00
Clemens Eisenhofer
c2a0919f79
Removed no progress case in seq-sls ( #7537 )
2025-01-29 09:43:57 -08:00
Nikolaj Bjorner
6d3cfb63da
add eval1 functionality for replace_all
2025-01-29 04:36:55 -08:00
Nikolaj Bjorner
ab43d2dcf1
fix semantics of check-int64 div operation to align with smtlib semantics
2025-01-29 04:29:38 -08:00
Nikolaj Bjorner
30d72f79ac
remove verbose output of overflow
2025-01-29 03:48:11 -08:00
Nikolaj Bjorner
3379155a63
add check for root literal assignment
2025-01-29 03:14:14 -08:00
Nikolaj Bjorner
fe5d17d515
handle exception internally, avoid passing rationals to integer operations
2025-01-28 20:09:59 -08:00
