mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity
17542 commits 24 branches 48 tags 158 MiB
Commit graph

17542 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
6d8d8f1971 fix release message 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 12:43:05 -08:00
Nikolaj Bjorner
e6f8fe359e remove empty file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 12:32:28 -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
971b9d4081 fix #6564 
fixes to simplifier command front-end
 2023-01-31 09:32:34 -08:00
Nikolaj Bjorner
238d604a10 android 16 byte alignment for stack allocated memory? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-30 23:00:44 -08:00
Nikolaj Bjorner
5794d080b5 updated doc generation script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-30 22:52:32 -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
304b316314 move bounded division lemmas to nla solver/ nla_divisions. 2023-01-30 11:11:04 -08:00
Nikolaj Bjorner
03ca330926 fix division filter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-30 08:23:17 -08:00
Nikolaj Bjorner
2c4a9c2f5c fix division filter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-30 08:20:26 -08:00
Nikolaj Bjorner
8e37e2f913 handle non-linear division axioms, consolidate backtracking state in nla_core 
this update enables new incremental linear axioms based on division terms.
It also consolidates some of the backtracking state in nla_core / emons to use stack traces instead of custom backtracking state.
 2023-01-29 17:22:57 -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
246d6f7b77 fix #6561 2023-01-28 03:47:18 -08:00
Nikolaj Bjorner
83bd3d1e21 fix mk-project file for python build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-27 18:04:58 -08:00
Nikolaj Bjorner
fb1f4f3a2c add pragma 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-27 18:03:06 -08:00
Nikolaj Bjorner
91d6082f2f Move modular interval to interval directory 2023-01-27 17:55:36 -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
d4ca7e5374 #6555 2023-01-26 21:39:52 -08:00
Nikolaj Bjorner
ae24b73b19 bugfixes to incremental linearization for expanding power 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-26 21:19:45 -08:00
Nikolaj Bjorner
8be43ca68b reshuffle pre-conditions for powers 2023-01-25 13:51:19 -08:00
Nikolaj Bjorner
e41dd91893 add module for handling axioms for powers 2023-01-25 13:34:13 -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
dependabot[bot]
6c9358ce41
Bump docker/build-push-action from 3.2.0 to 3.3.0 (#6540) 
Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 3.2.0 to 3.3.0.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v3.2.0...v3.3.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>

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2023-01-24 13:22:41 -08:00
dependabot[bot]
8757778404
Bump mymindstorm/setup-emsdk from 11 to 12 (#6541) 
Bumps [mymindstorm/setup-emsdk](https://github.com/mymindstorm/setup-emsdk) from 11 to 12.
- [Release notes](https://github.com/mymindstorm/setup-emsdk/releases)
- [Commits](https://github.com/mymindstorm/setup-emsdk/compare/v11...v12)

---
updated-dependencies:
- dependency-name: mymindstorm/setup-emsdk
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2023-01-24 13:22:12 -08:00
Nikolaj Bjorner
6a7343aab4 update julia bindings to use 64-bit mk_real (real_val) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 13:06:41 -08:00
Nikolaj Bjorner
fa72ec5405 switch to expose fresh function instead of changing legacy function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 13:05:34 -08:00
Nikolaj Bjorner
eac7d7576f force to_fp to disambiguate +zero and -zero, #6548, filter unsupported on relevancy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 12:29:42 -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
3f1b7866ca convert caml mk_real to int64 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 03:53:42 -08:00
Nikolaj Bjorner
d5bd20978b fix #6550 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 03:38:19 -08:00
Nikolaj Bjorner
4601d1d664 fix #6550 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 03:37:09 -08:00
Nikolaj Bjorner
2ae476416c initial outline of exponentiation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-23 17:38:34 -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
Nikolaj Bjorner
eb751bec4c fix riscv/aarch/powerpc build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-22 23:57:59 -08:00
Nikolaj Bjorner
3b5ae285d9 add outline for interval reasoning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-22 23:28:36 -08:00
Nikolaj Bjorner
273aff5ed6 remove debug out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-22 22:21:23 -08:00
Nikolaj Bjorner
db79346ef7 Add new tactic bound-simplifier for integer-based bit-vector reasoning. 2023-01-22 22:07:28 -08:00
Nikolaj Bjorner
83662701b6
Update theory_lra.cpp 
remove spurious output
 2023-01-22 16:27:48 -08:00
Nikolaj Bjorner
dbc299efbb revise bv-bounds-tactic 
- share common functionality
- rename propagate-bv-bounds-new to propagate-bv-bound2 for now
- expose configuration options in bounds propagation
 2023-01-22 14:41:53 -08:00
Nikolaj Bjorner
e2a6376ddf detect bounds from mod 2023-01-22 14:40:36 -08:00
Nikolaj Bjorner
021ef699af detect bounds from mod 2023-01-22 14:40:19 -08:00
Nikolaj Bjorner
7d364bf786 Allow building AC functions without requiring arity check from API 2023-01-22 14:39:58 -08:00
Nikolaj Bjorner
806a4772bc revert effect of filtering unsupported 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-20 17:28:24 -08:00
Nikolaj Bjorner
4e6d498a60 adding placeholder for refining power of 2 2023-01-20 14:37:05 -08:00