mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity
19289 commits 23 branches 48 tags 157 MiB
Commit graph

19289 commits

This branch
This branch
All branches
Author SHA1 Message Date
Jakob Rath
53bbb49031 Restore mod_interval for fixplex 2023-02-01 16:34:25 +01:00
Jakob Rath
20b5455d08 Merge branch 'master' into polysat 2023-02-01 16:28:57 +01:00
Clemens Eisenhofer
4648c35a35 Missing file 2023-02-01 15:10:47 +01:00
Jakob Rath
fe164c843d Fix/simplify constraint_manager::watch 2023-02-01 15:02:56 +01:00
Jakob Rath
0d56edb65c Fix missing boolean propagation after boolean conflict 
Usually in SAT solving, the conflict clause has at least two false literals at the max level (otherwise, the last literal would have been propagated at an earlier level).
But here we are adding clauses on demand; so after backtracking we may have the case that the conflict clause has exactly one undefined literal that must be propagated explicitly.
 2023-02-01 15:02:56 +01: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
Clemens Eisenhofer
783bd60598 Merge branch 'polysat' of https://github.com/Z3Prover/z3 into polysat 2023-02-01 11:28:15 +01:00
Clemens Eisenhofer
8db575ea3b Division monotonicity 2023-02-01 11:27:46 +01:00
Jakob Rath
975fb25221 Fix to bench15 bug was unsound 2023-02-01 11:17:29 +01:00
Jakob Rath
f0625b604a Promote assertions to release mode 2023-02-01 11:12:13 +01:00
Jakob Rath
576e0b70b2 stub for conflict::find_deps 2023-02-01 10:53:49 +01:00
Jakob Rath
1bb68a4fc1 track dependency of base-level conflict 2023-02-01 10:47:26 +01:00
Jakob Rath
3c822117d1 assert before deref 2023-02-01 10:41:02 +01:00
Jakob Rath
9314ad3808 minor changes to bounds propagation 2023-02-01 10:36:49 +01: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
Clemens Eisenhofer
63f7001117 Justify shift-premis in variable_elimination 2023-01-31 15:50:42 +01:00
Jakob Rath
9916a76543 try_eval constraints when adding clause 
(fix assertion in bench15)
 2023-01-31 15:15:51 +01: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
Clemens Eisenhofer
e8163b1769 Removed wrong assertion 2023-01-27 08:32:44 +01: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