mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-10 16:12:03 +00:00
Code Activity
20119 commits 50 branches 53 tags 183 MiB
Commit graph

20119 commits

This branch
This branch
All branches
Author SHA1 Message Date
Ilana Shapiro
52fd59df1b
Add cube tree optimization about resolving cores recursively up the path, to prune. Also integrate asms into the tree so they're not tracked separately (#7960) 
* draft attempt at optimizing cube tree with resolvents. have not tested/ran yet

* adding comments

* fix bug about needing to bubble resolvent upwards to highest ancestor

* fix bug where we need to cover the whole resolvent in the path when bubbling up

* clean up comments

* close entire tree when sibling resolvent is empty

* integrate asms directly into cube tree, remove separate tracking

* try to fix bug about redundant resolutions, merging close and try_resolve_upwards into once function

* separate the logic again to avoid mutual recursion
 2025-10-11 06:58:14 -07:00
Lev Nachmanson
641741f3a8 parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-07 10:30:58 -07:00
Lev Nachmanson
8af9a20e01 parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-07 10:26:40 -07:00
Lev Nachmanson
6a9520bdc2 parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-07 10:21:09 -07:00
Lev Nachmanson
8ccf4cd8f7 parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-07 10:19:24 -07:00
Lev Nachmanson
40b980079b parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-07 10:14:02 -07:00
Lev Nachmanson
a41549eee6 parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-07 10:06:43 -07:00
Lev Nachmanson
2b3068d85f parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-07 09:17:12 -07:00
Lev Nachmanson
3a2bbf4802 param eval order 2025-10-07 09:13:21 -07:00
Lev Nachmanson
6e52b9584c param eval 2025-10-07 09:04:24 -07:00
Lev Nachmanson
93ff8c76db parameter evaluation order 2025-10-07 08:53:49 -07:00
Lev Nachmanson
00f1e6af7e parameter eval order 2025-10-07 08:40:24 -07:00
Lev Nachmanson
c154b9df90 param order evaluation 2025-10-07 08:34:56 -07:00
Lev Nachmanson
77c70bf812 param order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-06 15:52:09 -07:00
Lev Nachmanson
63bb367a10 param order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-06 15:52:09 -07:00
Nikolaj Bjorner
e9a2766e6c remove AI slop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-06 13:53:37 -07:00
Lev Nachmanson
5a9663247b fix the order of parameter evaluation 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-06 13:44:19 -07:00
Lev Nachmanson
5ae858f66b fixing the order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-06 13:44:19 -07:00
Lev Nachmanson
aa5645b54b fixing the order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-06 13:44:19 -07:00
Nikolaj Bjorner
542e015550
Remove unused variable 'first' in mpz.cpp 
Removed unused variable 'first' from the function.
 2025-10-06 13:39:27 -07:00
Copilot
cd1ceb6efe
[WIP] Add a mutex to warning.cpp to ensure that warning messages from different threads don't interfere (#7963) 
* Initial plan

* Add mutex to warning.cpp for thread safety

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2025-10-06 13:38:18 -07:00
Ilana Shapiro
b9fb032a67 separate the logic again to avoid mutual recursion 2025-10-05 15:43:27 -07:00
Ilana Shapiro
21422fab8b try to fix bug about redundant resolutions, merging close and try_resolve_upwards into once function 2025-10-05 13:52:27 -07:00
Ilana Shapiro
e2432b0d50 integrate asms directly into cube tree, remove separate tracking 2025-10-05 11:41:00 -07:00
Ilana Shapiro
f75d137911 close entire tree when sibling resolvent is empty 2025-10-04 09:18:22 -07:00
dependabot[bot]
3ce8aca411
Bump actions/checkout from 4 to 5 (#7954) 
Bumps [actions/checkout](https://github.com/actions/checkout) from 4 to 5.
- [Release notes](https://github.com/actions/checkout/releases)
- [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md)
- [Commits](https://github.com/actions/checkout/compare/v4...v5)

---
updated-dependencies:
- dependency-name: actions/checkout
  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-04 01:22:52 -07:00
Ilana Shapiro
5143ba0118 clean up comments 2025-10-03 16:39:32 -07:00
Ilana Shapiro
b42db215c4 fix bug where we need to cover the whole resolvent in the path when bubbling up 2025-10-03 13:38:02 -07:00
Nikolaj Bjorner
c8bdbd2dc4 remove directory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-03 11:58:57 -07:00
Ilana Shapiro
279c7d4d46 fix bug about needing to bubble resolvent upwards to highest ancestor 2025-10-03 10:48:47 -07:00
Ilana Shapiro
0898813f8c adding comments 2025-10-03 09:45:54 -07:00
Nikolaj Bjorner
e137aaa249 add user propagators to opt_solver 2025-10-02 19:44:22 -07:00
Nikolaj Bjorner
0e6b3a922a Add commands for forcing preferences during search 
Add commands:

(prefer <formula>)
- will instruct case split queue to assign formula to true.
- prefer commands added within a scope are forgotten after leaving the scope.

(reset-preferences)
- resets asserted preferences. Has to be invoked at base level.

This provides functionality related to MathSAT and based on an ask by Tomáš Kolárik who is integrating the functionality with OpenSMT2
 2025-10-02 10:47:10 -07:00
Nikolaj Bjorner
5d8fcaa3ee update clang format 2025-10-02 10:39:37 -07:00
Nikolaj Bjorner
72c89e1a4e fix #7952 - make auto-selector detect large bit-vectors so it does't use the datalog engine for hopelessly large tables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-30 15:58:48 -07:00
Nikolaj Bjorner
0881a71ed2 update format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-30 15:42:01 -07:00
Nikolaj Bjorner
65c9a18c3a fix #7956 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-30 15:41:49 -07:00
Ilana Shapiro
6da167ec09 draft attempt at optimizing cube tree with resolvents. have not tested/ran yet 2025-09-30 11:35:00 -07:00
Ruijie Fang
339f0cd5f9
Correctly distinguish between Lambda and Quantifier in Z3 Java API (#7955) 
* Distinguish between Quantifier and Lambda in AST.java

* Distinguish betwee Lambda and Quantifier in Expr.java

* Make things compile
 2025-09-30 09:55:14 -07:00
Nikolaj Bjorner
253a7245d0 add analysis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-28 13:05:04 +03:00
Nikolaj Bjorner
b5f79da76a add analysis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-28 13:03:31 +03:00
Nikolaj Bjorner
ae55b6fa1e add analysis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-28 13:02:05 +03:00
Nikolaj Bjorner
bda98d8da4 fix #7948 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-28 12:52:20 +03:00
Nikolaj Bjorner
b7eb21efed fix #7948 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-28 12:52:19 +03:00
Wael Boutglay
391880b6fc
Add missing ::z3::sdiv to z3++.h (#7947) 2025-09-25 22:04:15 +03:00
Nikolaj Bjorner
6173a0d025 propagate value initialization to atoms 2025-09-24 11:01:24 +03:00
Nikolaj Bjorner
eae4de075b fix latent bug in factorization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-23 10:47:24 +03:00
Nikolaj Bjorner
04ddade2dd remove stale comment 2025-09-22 04:43:41 +03:00
Nikolaj Bjorner
f5c28a0b76 household cleanup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-22 03:58:04 +03:00
Nikolaj Bjorner
e26f7b900c fix unsound axiom for lower-bounding 2025-09-21 19:24:13 +03:00