Nikolaj Bjorner
|
5438d5ad89
|
remove extraction of linear cores because it examines a stale core instead of the current core. A reintroduction of this feature would have to extract the lemma before the next solver call and save it aside in case the solver call returns l_undef
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-25 19:24:57 -08:00 |
|
Nikolaj Bjorner
|
151be6ac9a
|
statistics and configuable
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-22 16:48:15 -08:00 |
|
Nikolaj Bjorner
|
e44994b9a4
|
stellensatz fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-22 10:15:14 -08:00 |
|
Nikolaj Bjorner
|
ee63585581
|
update model-guide heuristic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-21 15:52:37 -08:00 |
|
Nikolaj Bjorner
|
ed84b14e6c
|
fixing coi bug
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-20 17:55:37 -08:00 |
|
Nikolaj Bjorner
|
7b265ba162
|
fix poly model bug
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-20 14:24:08 -08:00 |
|
Nikolaj Bjorner
|
b3f7d16606
|
fix memory leaks and handling of non-integer term coefficients
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-20 11:59:12 -08:00 |
|
Nikolaj Bjorner
|
2578218b6f
|
add new option for adding tangent lemmas for integer monomials
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-20 11:30:07 -08:00 |
|
Nikolaj Bjorner
|
fc96f827a1
|
updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-20 10:32:51 -08:00 |
|
Nikolaj Bjorner
|
823800541e
|
updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-19 14:02:27 -08:00 |
|
Nikolaj Bjorner
|
5d316a51d1
|
enable bound tracking
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-19 10:53:42 -08:00 |
|
Nikolaj Bjorner
|
5de01e5d1d
|
add stubs for bounds refinement
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-19 10:42:28 -08:00 |
|
Nikolaj Bjorner
|
179601ffac
|
testing model repair
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-18 14:14:54 -08:00 |
|
Nikolaj Bjorner
|
4df7ee67f5
|
updated sketch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-17 22:06:29 -08:00 |
|
Nikolaj Bjorner
|
92bc39dab5
|
add toggle to use polynomial translation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-17 20:52:34 -08:00 |
|
Nikolaj Bjorner
|
33709d3abb
|
add toggle to use polynomial translation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-17 17:28:28 -08:00 |
|
Nikolaj Bjorner
|
2eca05e59a
|
fix crash
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-17 09:57:17 -08:00 |
|
Nikolaj Bjorner
|
12df8f593e
|
reshuffle if conditions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-16 17:24:31 -08:00 |
|
Nikolaj Bjorner
|
e9905c05b1
|
fix crash
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-16 17:21:23 -08:00 |
|
Nikolaj Bjorner
|
711572e73c
|
fix crash on arie branch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-16 16:58:33 -08:00 |
|
Nikolaj Bjorner
|
b835bd4c92
|
self-contained tracking of values
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-16 12:55:58 -08:00 |
|
Nikolaj Bjorner
|
f347c24e04
|
fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-15 13:09:25 -08:00 |
|
Nikolaj Bjorner
|
072f1deccc
|
update
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-14 16:37:00 -08:00 |
|
Nikolaj Bjorner
|
d081321384
|
add substitution and division
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-14 16:26:10 -08:00 |
|
Nikolaj Bjorner
|
f55bdd923a
|
remove mul saturate
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-13 15:43:44 -08:00 |
|
Nikolaj Bjorner
|
5ea25dcf60
|
v2 running
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-13 13:59:12 -08:00 |
|
Nikolaj Bjorner
|
c7084e9998
|
revamp stellensatz to use polynomals
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-12 20:21:42 -08:00 |
|
Nikolaj Bjorner
|
21b36868b5
|
revamping stellensatz
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-12 10:13:09 -08:00 |
|
Nikolaj Bjorner
|
b8f5e1d646
|
small rewrite update
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-10 15:01:30 -08:00 |
|
Nikolaj Bjorner
|
9f848847c7
|
remove debug out from euf-completion
|
2025-11-07 08:06:13 -08:00 |
|
Nikolaj Bjorner
|
f4c5e14b6b
|
add fold-unfold simplification
this substitutes solve-eqs by including fold-unfold reductions.
|
2025-11-07 08:04:41 -08:00 |
|
Nikolaj Bjorner
|
5d36f53cd3
|
add rewrite to eliminate quot-rem tautologies
|
2025-11-07 08:04:03 -08:00 |
|
Nikolaj Bjorner
|
a3ec6a0f1b
|
add delayed diseq check
|
2025-11-07 08:03:37 -08:00 |
|
Nikolaj Bjorner
|
daf66e63c6
|
add more pre-processing for band
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-04 09:45:40 -08:00 |
|
Nikolaj Bjorner
|
4828ed97be
|
tweak bound propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-03 12:41:33 -08:00 |
|
Nikolaj Bjorner
|
88269edd4b
|
fixup bv operators
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-03 07:56:42 -08:00 |
|
Nikolaj Bjorner
|
919ac515bc
|
fix crash
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-02 16:05:09 -08:00 |
|
Nikolaj Bjorner
|
ceb424dc64
|
update clang format
|
2025-10-31 08:43:50 -07:00 |
|
Nikolaj Bjorner
|
1b48ec27e0
|
update format
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-10-31 08:43:50 -07:00 |
|
Nikolaj Bjorner
|
e3ef97e24d
|
propagate value initialization to atoms
|
2025-10-31 08:43:50 -07:00 |
|
Nikolaj Bjorner
|
e709885e72
|
gcd reduce and use c().val for sign constraints
|
2025-10-31 08:43:46 -07:00 |
|
Nikolaj Bjorner
|
018cb3c734
|
generate more proper proof format
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-10-31 08:41:14 -07:00 |
|
Nikolaj Bjorner
|
fdac93fff3
|
v0.1 of nla saturation
|
2025-10-31 08:36:15 -07:00 |
|
Nikolaj Bjorner
|
3e9afb30af
|
disable nuget
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-10-31 08:32:33 -07:00 |
|
Nikolaj Bjorner
|
7c28d936fb
|
bump version for release
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-10-31 08:32:33 -07:00 |
|
Nikolaj Bjorner
|
a75602b7e5
|
update release notes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-10-31 08:32:32 -07:00 |
|
Nikolaj Bjorner
|
bc28de931b
|
fix C++ example and add polymorphic interface for C++
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-10-31 08:32:32 -07:00 |
|
Nikolaj Bjorner
|
67dcb8bcc1
|
renemable Centos AMD nightly
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-10-31 08:32:32 -07:00 |
|
Nikolaj Bjorner
|
d8862f8f6a
|
fix build break introduced when adding support for polymorphic datatypes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-10-31 08:32:32 -07:00 |
|
dependabot[bot]
|
cf6a1ceb0e
|
Bump actions/upload-artifact from 4 to 5 (#7998)
Bumps [actions/upload-artifact](https://github.com/actions/upload-artifact) from 4 to 5.
- [Release notes](https://github.com/actions/upload-artifact/releases)
- [Commits](https://github.com/actions/upload-artifact/compare/v4...v5)
---
updated-dependencies:
- dependency-name: actions/upload-artifact
dependency-version: '5'
dependency-type: direct:production
update-type: version-update:semver-major
...
Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
|
2025-10-31 08:32:32 -07:00 |
|