Nikolaj Bjorner
a6b12bb33c
call make-feasible after values are initialized
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-02-10 14:38:59 -08:00
Nikolaj Bjorner
f5ccdf6a47
disable value transfer to SMT
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-02-10 13:23:15 -08:00
Nikolaj Bjorner
edc3e0b05d
parameters, local search, arithmetic propagation
...
add get-info parameters to print current parameters in scope of solver
add interface to set values in int-blaster
settle on propagation for arithmetic assignments
2025-02-03 20:28:14 -08:00
Nikolaj Bjorner
3456af425e
with theory propagation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-02-03 14:08:02 -08:00
Nikolaj Bjorner
7808be0935
with theory lemma relevant
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-02-03 13:44:05 -08:00
Nikolaj Bjorner
ef7893cdca
use learned vs relevant distinction for theory lemmas
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-02-03 13:40:06 -08:00
Nikolaj Bjorner
a513488c54
add conflict throttle, experiment with pb2bv
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-02-03 03:14:20 -08: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
Nikolaj Bjorner
5b175c1bcd
fix crashes in sls_datatype
2025-01-28 19:24:32 -08:00
Nikolaj Bjorner
fe713eb8e9
disable quadratic moves for non-integers as sqrt isn't currently defined for rationals
2025-01-28 16:53:12 -08:00
Nikolaj Bjorner
d8430810fe
fix mixup between sync and sls managed variables
2025-01-28 16:35:50 -08:00
Nikolaj Bjorner
fa605454fb
fix crash reported by Nikhil on F* due to unhandled exception while using the rewriter during search
2025-01-28 16:27:28 -08:00
Nikolaj Bjorner
5c2a9d9936
fix pickup of new constraints
2025-01-28 15:04:13 -08:00
Nikolaj Bjorner
1676378be9
skip last power
2025-01-28 15:03:01 -08:00
Nikolaj Bjorner
8a7d971264
Update sls_bv_lookahead.h
2025-01-28 15:02:45 -08:00
Nikolaj Bjorner
2ebc647079
skip update stack items that are not Bool/bv
2025-01-28 15:02:33 -08:00
Nikolaj Bjorner
632e2b56e4
fix initialization of mod terms
2025-01-28 15:01:50 -08:00
Nikolaj Bjorner
fd5f5feb40
add cmake option to turn on asan
2025-01-28 15:01:31 -08:00
Nikolaj Bjorner
a8279dd9d5
reset kv map consistently with egraph
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-01-27 17:09:38 -08:00
Nikolaj Bjorner
57a5474ab4
revert flat default
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-01-27 16:56:12 -08:00
Nikolaj Bjorner
72ae161307
compress store array before model-eval rewriter sees it
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-01-27 16:55:07 -08:00
Nikolaj Bjorner
fe1622b592
sls fixes for ABV. Axiomatization required as saturation can produce conflicts by congruence closure
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-01-27 15:16:13 -08:00
Jonáš Fiala
2050fc3b35
Preserve fingerprint in trace ( #7534 )
2025-01-27 13:09:48 -08:00
Can Cebeci
2d8f024680
Mark fixed_eq literals as relevant ( #7533 )
2025-01-27 11:10:46 -08:00
Nikolaj Bjorner
63f9fdaf3e
fix build
2025-01-27 10:52:21 -08:00
Nikolaj Bjorner
15ee879602
fix #7532
2025-01-27 10:51:12 -08:00
Nikolaj Bjorner
b6e7b80704
updates to handle bugs exposed by qf-abv for local search
...
- ctx.is_true(e) - changed to work with expressions that are not literals, but come from top-level assertions
- set fixed in sls_bv_fixed to work with non-zero low order bits
- array plugin to deal with cases where e-graph is inconsistent after a merge.
2025-01-27 10:35:29 -08:00
