mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity
16044 commits 23 branches 48 tags 157 MiB
Commit graph

13577 commits

Author SHA1 Message Date
Nikolaj Bjorner a086f6218b na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-03 14:15:41 -08:00
Nikolaj Bjorner a2a5924e5c purge more 2022-01-03 14:14:09 -08:00
Nikolaj Bjorner 8e3185ffe3 remove dual solver approach 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-03 14:08:01 -08:00
Nikolaj Bjorner 1f964eea90 na 2022-01-03 11:12:28 -08:00
Nikolaj Bjorner 2944449884 #5641 2022-01-03 11:12:09 -08:00
Nikolaj Bjorner cf08cdff9c #5747 2022-01-03 08:54:54 -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 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
Margus Veanes 5afb95b34a
improved subset checking for regexes with counters (#5731) 2021-12-22 17:53:34 -08:00
Nikolaj Bjorner 71b868d7f6 #5722 - internalize unary xnor 2021-12-22 13:32:53 -08:00
Nikolaj Bjorner 4d8bf2a874 wrong unit for xor in aig tactic #5722 2021-12-22 13:14:06 -08:00
Anton Kochkov f11fcec082
Migrate from deprecated distutils.sysconfig in scripts (#5729) 2021-12-22 07:59:13 -08:00