mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
18628 commits 49 branches 53 tags 182 MiB
Commit graph

18628 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
c1c26f0726 restart after sat solution 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-06 09:21:35 -08:00
Nikolaj Bjorner
03a4920f3d fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-05 21:41:07 -08:00
Nikolaj Bjorner
75c573877d updates to ddfw, initial local search phase option 2023-02-05 21:35:22 -08:00
Nikolaj Bjorner
992793bd56 update nuget packaging targets #6570 2023-02-05 21:35:22 -08:00
Nikolaj Bjorner
3712cbdbfd fix #6559 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-04 13:33:40 -08:00
Jakob Rath
d69155b9e9
Shared features from polysat branch (#6567) 
* Allow setting default debug action

* Fix dlist and add iterator

* Add var_queue iterator

* Add some helpers

* rational: machine_div2k and pseudo_inverse

* Basic support for non-copyable types in map

* tbv helpers

* pdd updates

* Remove duplicate functions

gcc doesn't like having both versions
 2023-02-03 13:08:47 -08:00
Frederick Robinson
be44ace995
fix typo (#6569) 2023-02-03 13:08:35 -08:00
Nikolaj Bjorner
cb72b962d1 Merge branch 'master' of https://github.com/z3prover/z3 2023-02-02 20:50:58 -08:00
Nikolaj Bjorner
839f87a10c don't apply tactics in parse mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-02 20:50:53 -08:00
Nikolaj Bjorner
39d2818923 compiler warnings/bugs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-02 19:36:22 -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
741634b703 compiler warning fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-02 19:26:51 -08:00
Nikolaj Bjorner
efbecb19b1 compiler warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-02 19:23:30 -08:00
Nikolaj Bjorner
ed4a84e5d3 compiler warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-02 19:21:34 -08:00
Nikolaj Bjorner
4143c54257 add simplifier to java API 2023-02-02 19:06:26 -08:00
Nikolaj Bjorner
2e068e3f56 add simplifiers to .net API 2023-02-02 17:41:00 -08:00
Nikolaj Bjorner
72e7a8a481 fix incremental pre-processing to work with consequences/cubes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-01 20:00:38 -08:00
Nikolaj Bjorner
6c7dd4a863 fix incremental pre-processing to work with assumptions/cores and consequences 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-01 19:47:58 -08:00
Nikolaj Bjorner
7767144051 fix test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-01 11:07:47 -08:00
Nikolaj Bjorner
30fa37e393 fix warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-01 10:31:34 -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
682e868129 initialize field 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-01 10:18:14 -08:00
Nikolaj Bjorner
0f86a00229 use setter method to easier track updates to settings. 2023-02-01 10:18:14 -08:00
Nikolaj Bjorner
19fed09122 protecting add_simplifier API against mis-use 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-01 08:35:32 -08:00
dependabot[bot]
151a62338c
Bump docker/build-push-action from 3.3.0 to 4.0.0 (#6562) 2023-02-01 12:13:09 +00:00
Nikolaj Bjorner
63c0f35978 update ml api 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 19:27:17 -08:00
Nikolaj Bjorner
d51d518f96 update ml api 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 19:24:45 -08:00
Nikolaj Bjorner
1289937d1a update ml api 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 19:19:41 -08:00
Nikolaj Bjorner
9a94a9aa6f update ml api 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 19:14:24 -08:00
Nikolaj Bjorner
17bae9b4c1 update ml api 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 19:09:37 -08:00
Nikolaj Bjorner
162fa3dc96 disambiguate overloaded with for Julia bindings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 19:06:20 -08:00
Nikolaj Bjorner
4c6d44f974 add ocaml signature for simplifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 18:58:18 -08:00
Nikolaj Bjorner
550619bfcf add API for creating and attaching simplifiers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 17:06:03 -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
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