mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 01:54:08 +00:00
Code Activity
16038 commits 23 branches 48 tags 156 MiB
Commit graph

16038 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner da154b2f7e disable macos with ocaml as it fails too often 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-02 19:44:20 -08:00
Nikolaj Bjorner a71aa113e0 #5641 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-02 19:36:17 -08:00
Nikolaj Bjorner 9cbec3b0ca #5641 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-02 19:15:23 -08:00
Nikolaj Bjorner 43e449a805 #5641 2022-01-02 17:53:26 -08:00
Nikolaj Bjorner d0fb3cba15 #5641 - projection that skips interpreted functions can violate model evaluation. 2022-01-02 17:45:43 -08:00
Nikolaj Bjorner 0ca5e7207e #5746 2022-01-02 11:35:55 -08:00
Nikolaj Bjorner e84ddb0d9a more #5746 2022-01-02 11:33:21 -08:00
Nikolaj Bjorner 88707f37e7 Better error reporting #5746 2022-01-02 11:31:50 -08:00
Nikolaj Bjorner 543c16c73e Trace unexpected exceptions in or-else code #5746 2022-01-02 10:22:51 -08:00
Nikolaj Bjorner 5cd1fe31fd propagate parent default not add parent default) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-01 20:37:26 -08:00
Nikolaj Bjorner 8245935d41 #5641 add handlers for basic set operations to euf=true 2022-01-01 20:33:17 -08:00
Nikolaj Bjorner 9d3c8a6a2f na 2022-01-01 17:59:31 -08:00
Nikolaj Bjorner 42219204ed sketch replace_all 2022-01-01 17:39:37 -08:00
Nikolaj Bjorner 5672f5cc34 fix #5733 2022-01-01 16:40:48 -08:00
Nikolaj Bjorner 84f514a4f4 throttle ackerman on arrays 2022-01-01 15:33:33 -08:00
Nikolaj Bjorner a20b577b2f na 2022-01-01 11:26:38 -08:00
Nikolaj Bjorner ca18150c23 bypass append when src is empty 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-31 16:43:07 -08:00
Nikolaj Bjorner a44a46a514 fix #5745 2021-12-31 16:41:51 -08:00
Nikolaj Bjorner 9550321064 missed push lambdas 2021-12-31 16:33:06 -08:00
Nikolaj Bjorner 0ef0ed3b94 redoing arrays 2021-12-31 15:51:52 -08:00
Nikolaj Bjorner aa901c4e88 axiom solver improvements 2021-12-31 11:53:40 -08:00
Nikolaj Bjorner 79f0ceac4c na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-30 19:13:23 -08:00
Nikolaj Bjorner fc77345bec breaking change. Enforce append semantics everywhere for parameter updates #5744 
Replace semantics doesn't work with assumptions made elsewhere in code.
The remedy is to apply append (override) semantics for parameter changes.
 2021-12-30 19:11:14 -08:00
Nikolaj Bjorner e8833f4dac working on relevancy=3 2021-12-30 17:07:14 -08:00
Nikolaj Bjorner b87b464e69 set relevancy flag on enode 2021-12-29 17:57:28 -08:00
Nikolaj Bjorner a90b66134d make roots uniform for theory lemmas 2021-12-29 13:42:11 -08:00
Nikolaj Bjorner 69b4392210 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-29 13:04:31 -08:00
Nikolaj Bjorner f215b18e0e change registration mode for relevant_eh 2021-12-29 13:03:43 -08:00
Nikolaj Bjorner 1706f77b9e optimize propagation to only blocked literals 2021-12-28 18:53:37 -08:00
Nikolaj Bjorner 8ff8252e89 debug relevancy mode 2021-12-28 13:02:09 -08:00
Nikolaj Bjorner 743e56bda3 remove output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-28 12:08:10 -08:00
Nikolaj Bjorner 5ed27a6c38 fix initialization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-28 12:06:56 -08:00
Nikolaj Bjorner 95e26aaad9 #5742 
expose access to constructors/accessors/recognizers given datatype sort
 2021-12-28 11:00:34 -08:00
Nikolaj Bjorner 28bce8f09c working on relevant 2021-12-28 11:00:02 -08:00
Nikolaj Bjorner 9527471967 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-27 16:03:56 -08:00
Nikolaj Bjorner 6f1be09993 add direct and incremental relevancy propagator 2021-12-27 15:10:33 -08:00
Nikolaj Bjorner 42f206171d fix #5741 2021-12-27 15:10:09 -08:00
Nikolaj Bjorner d88f125818 build 2021-12-26 15:24:03 -08:00
Nikolaj Bjorner 0bd6725711 #5641 
mark all literals duplicated in dual solver as external
 2021-12-26 15:10:21 -08:00
Nikolaj Bjorner fcee2f5aa5 revert relevancy2 2021-12-26 15:10:21 -08:00
Nikolaj Bjorner 76e8e57204 Update azure-pipelines.yml for Azure Pipelines 
remove flaky MacOS build tests
 2021-12-26 13:12:50 -08:00
Nikolaj Bjorner 5a77c30ce0
Update README.md 2021-12-25 17:36:28 -08:00
Nikolaj Bjorner ec3e296050
Update docker-image.yml (#5739) 
* Update docker-image.yml

towards tweaking script to use ghcr

* Update docker-image.yml

* Update docker-image.yml

* Update docker-image.yml

change usr/pwd to names that are more descriptive

* Update docker-image.yml

rename back to use DOCKER prefix
it remains to bind to ghcr.io instead of docker.io

* Update ubuntu-20-04.Dockerfile

try to use ghcr instead of docker.io

* Update docker-image.yml

try with chcr token

* Update docker-image.yml

* Update docker-image.yml

* Update docker-image.yml

* Update ubuntu-20-04.Dockerfile

* Update docker-image.yml
 2021-12-25 17:33:35 -08:00
Nikolaj Bjorner 7d311ac2ef use netstandard 2.0 per recommendations 
seems that now the recommended starting point is 2.0 and not lower.
 2021-12-25 13:44:49 -08:00
Nikolaj Bjorner 6b0dc6d144
Create docker-image.yml 
thanks #5735
 2021-12-23 14:43:12 -08:00
Nikolaj Bjorner ecf41972b1 increase minor version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-23 14:41:52 -08:00
Nikolaj Bjorner dc09d3c5ea fix typo 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-23 14:41:52 -08:00
Nikolaj Bjorner df8f9d7dcb Update release.yml for Azure Pipelines 2021-12-23 12:43:00 -08:00
Nikolaj Bjorner bd2a53c475 Update release.yml for Azure Pipelines 2021-12-23 11:48:08 -08:00
Nikolaj Bjorner 5d4420a763 Update release.yml for Azure Pipelines 2021-12-23 11:46:47 -08:00