mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 13:06:05 +00:00
Code Activity
18887 commits 63 branches 52 tags 178 MiB
Commit graph

167 commits

Author SHA1 Message Date
Nuno Lopes
737c2208fa delete more default constructors 
reduces code size by 0.1%
 2024-09-23 12:59:04 +01:00
Nuno Lopes
8061765574 remove default destructors & some default constructors 
Another ~700 KB reduction in binary size
 2024-09-04 22:30:23 +01:00
Nikolaj Bjorner
49ba3bc12f address compiler warnings gcc-13 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 11:33:54 -07:00
Nikolaj Bjorner
2ad9f220f2 add logging 2024-04-30 16:57:59 -07:00
Nikolaj Bjorner
974ea7b68d maintain ownership of dependency 2024-04-10 17:57:14 -07:00
Nikolaj Bjorner
51f1e2655c updates to sls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-30 12:59:05 -07:00
Nikolaj Bjorner
ea44c110bb gc expressions in the scope of updates, not old expressions 2023-12-18 20:08:29 -08:00
Nikolaj Bjorner
13be3c3fbb reset model converter between rounds to elim-unconstrained. 2023-12-18 16:57:52 -08:00
Nikolaj Bjorner
bb99f44214 fix bugs in elim-unconstr2 and fix bugs in intblast_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-17 17:42:55 -08:00
Bruce Mitchener
e90a844508
Use override more. (#7059) 2023-12-15 08:44:57 +00:00
Nikolaj Bjorner
8fac89cdcc enable more simplification in case inequality triggers a change. 2023-10-21 19:58:39 -07:00
Nikolaj Bjorner
b87a91379c fix #6894 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-14 17:14:14 -07:00
Nikolaj Bjorner
50d76a2fe3 fix #6894 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-14 17:14:14 -07:00
Nikolaj Bjorner
5e3df9ee77
Arith min max (#6864) 
* prepare for dependencies

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* snapshot

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* more refactoring

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* more refactoring

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* pass in u_dependency_manager

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* address NYIs

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* more refactoring names

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* eq_explanation update

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add outline of bounds improvement functionality

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix unit tests

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove unused structs

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* more bounds

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* more bounds

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* convert more internals to use u_dependency instead of constraint_index

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* convert more internals to use u_dependency instead of constraint_index

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remember to push/pop scopes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* use the main function for updating bounds

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove reset of shared dep manager

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* disable improve-bounds, add statistics

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-19 17:44:09 -07:00
Nikolaj Bjorner
5b2519d7a3 #6523 
attach original variable to pb expression.
 2023-08-01 08:41:26 -07:00
Nikolaj Bjorner
f4b87b3763 fix memory smash in euf completion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-05 13:04:49 -07:00
Nikolaj Bjorner
ac00306355 fix context simplification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-09 11:30:56 -07:00
Nikolaj Bjorner
d0085b41c1 disable breaking change 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-09 11:15:54 -07:00
Nikolaj Bjorner
555ccc8aab simplify bounds by subsumption checks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-09 10:21:45 -07:00
Nikolaj Bjorner
2e441e38c9 fix #6713 fix #6714 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-08 12:24:20 -07:00
Nikolaj Bjorner
a849a29b4f fix #6659 2023-03-31 10:31:18 -07:00
Nikolaj Bjorner
f075dc2882 remove experimental files 2023-03-20 17:07:48 +01:00
Nikolaj Bjorner
48de7c2da8 missing updates 2023-03-20 17:07:04 +01:00
Nikolaj Bjorner
c6e3fb446a print lemmas2console faster 
- add option pp.no_lets (default = false) to print formulas without let (used by the low-level SMT2 printer).
- print lemmas2console faster by using the low level printer
 2023-03-20 17:07:04 +01:00
Nikolaj Bjorner
d1c7ff1a36 add unconstrained elimination for sequences 2023-03-20 17:07:04 +01:00
Nikolaj Bjorner
42076a3c13 bug fixes to new core, elim_predicates and elim_unconstrained 2023-03-05 22:26:37 -08:00
Nikolaj Bjorner
b82d177276 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-03-03 11:26:13 -08:00
Nikolaj Bjorner
aa75ba8a6b remove parenthesis 2023-03-01 21:03:41 -08:00
Nikolaj Bjorner
94b79eefea add back max_occs parameter dependency to solve-eqs 2023-03-01 20:40:22 -08:00
Nikolaj Bjorner
027770930e fix bug in quasi macro identification: require quantifiers 2023-03-01 17:03:15 -08:00
Nikolaj Bjorner
cac5052685 fixes related to #6577 
- enforce elim-and in bool-rewriter when invoking hoisting.
- make cnf tactic more resilient to non-normalized input.
- enable eliminate predicates on ground formulas
 2023-02-12 13:43:44 -08:00
Nikolaj Bjorner
0d05104d8c remove unused field 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-02 19:33:23 -08:00
Nikolaj Bjorner
2e068e3f56 add simplifiers to .net API 2023-02-02 17:41:00 -08:00
Nikolaj Bjorner
38d526ee45 fix warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-01 10:18:14 -08:00
Nikolaj Bjorner
ebc2cd572b fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 14:53:04 -08:00
Nikolaj Bjorner
88bf3c6e51 check if trail is empty to avoid collecting variables 2023-01-31 13:35:43 -08:00
Nikolaj Bjorner
8495be11f9 add shortcut filter to avoid traversing model reconstruction trail if there are no intersections with model 2023-01-31 13:34:52 -08:00
Nikolaj Bjorner
d263b373ed update release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 12:19:33 -08:00
Nikolaj Bjorner
6022c17131 Add simplification customization for SMTLIB2 
Add the ability to customize incremental pre-processing simplification for the SMTLIB2 front-end. The main new capability is to use pre-processing tactics in incremental mode that were previously not available. The main new capabilities are
- solve-eqs
- reduce-args
- elim-unconstrained
There are several more. Documentation and exposed simplifiers are populated incrementally. The current set of supported simplifiers can be inspected by using z3 with the --simplifiers flag or referring to https://microsoft.github.io/z3guide/docs/strategies/simplifiers

Some pending features are:
- add the ability to update parameters to simplifiers similar to how tactics can be controlled using parameters.
- expose simplification solvers over the binary API.
 2023-01-30 22:38:51 -08:00
Nikolaj Bjorner
dd0decfe5d create simplifier_solver wrapper to supply simplifier layer 
move sat_smt_preprocess to solver
fix bugs in model_reconstruction_trail for dependency replay

This is a preparatory step for exposing pre-processing as tactics.
 2023-01-30 16:12:25 -08:00
Nikolaj Bjorner
4ffe3fab05 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-28 21:51:51 -08:00
Nikolaj Bjorner
8ea49eed8e convert reduce-args to a simplifier 
- convert reduce-args to a simplifier. Currently exposed as reduce-args2 tactic until the old tactic code gets removed.
- bug fixes in model_reconstruction trail
  - allow multiple defs to be added with same pool of removed formulas
  - fix tracking of function symbols instead of expressions to filter replay
- add nla_divisions to track (cheap) divisibility lemmas.
-
 2023-01-28 20:12:14 -08:00
Nikolaj Bjorner
0f3c56213e move dominator simplifier functionality to rewriter and simplifier, move bv_bounds simplifier functionality to simplifier 2023-01-27 17:11:48 -08:00
Nikolaj Bjorner
9e2ec9d018 add stubs for proof production in elim_unconstrained 2023-01-25 13:32:51 -08:00
Nikolaj Bjorner
b3de7ac595 remove passing proof parameter to expr-inverter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-25 11:15:09 -08:00
Nikolaj Bjorner
f100d2f4de add contextual simplification to bv-bounds-tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 17:49:55 -08:00
Nikolaj Bjorner
47c7ed3b17 update ml example to 64 bit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 04:33:52 -08:00
Nikolaj Bjorner
15d853dc04 add trail to avoid stale references in expr2var 2023-01-24 04:15:52 -08:00
Nikolaj Bjorner
3032c9315d handle to-real in variable mapping 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-23 14:31:24 -08:00
Nikolaj Bjorner
d9f9cceea4 use intervals for tracking bounds on arithmetic variables 
leverage interval propagation for bounds.
merge functionality with propagate-ineqs tactic
remove the new propagate-bounds tactic and instead use propagate-ineqs
 2023-01-23 14:13:03 -08:00