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

10995 commits

Author SHA1 Message Date
Nikolaj Bjorner
3fa3c8bf76 fix #2788 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-07 09:46:33 +03:00
Nikolaj Bjorner
8eb2356b68 fix #2787 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-07 09:03:36 +03:00
Murphy Berzish
e5ca451a02 z3str3: remove unused str_eq_todo worklist 2019-12-05 01:51:16 +03:00
Murphy Berzish
32e5c6ffd1 z3str3: missed instance of rewrite-then-assert 2019-12-05 01:51:16 +03:00
Nikolaj Bjorner
7e415c1b69 update to logging 2019-12-04 23:08:41 +03:00
Nikolaj Bjorner
20754bc72d fix #2768 2019-12-04 23:08:03 +03:00
Nikolaj Bjorner
f646c9ac11 fix #2780 2019-12-04 10:45:17 +03:00
Nikolaj Bjorner
3d874313d3 fix #2782 2019-12-04 10:31:02 +03:00
Nikolaj Bjorner
2f6a9ba39b na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-03 20:34:56 +01:00
Nikolaj Bjorner
eec153bb57 fix #2779 2019-12-03 14:49:58 +01:00
Nikolaj Bjorner
7f61d08496 fix #2777 2019-12-03 13:53:59 +01:00
Nikolaj Bjorner
b35ec49b40 fix #2778 2019-12-03 12:53:06 +01:00
Nikolaj Bjorner
9af4cc0fd6 links to API (related to issue in z3doc) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-03 12:20:11 +01:00
Nikolaj Bjorner
28cb13fb96 fix #2771 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-02 15:41:56 -08:00
Nikolaj Bjorner
37a4dd68d0 fix #2773 fix #2774 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-02 15:22:03 -08:00
Nikolaj Bjorner
1eab774b91 fix #2774 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-02 15:22:03 -08:00
Murphy Berzish
89c9bb2e0e z3str3: don't call propagate() in init_search_eh() 2019-12-02 15:20:04 -08:00
Nikolaj Bjorner
7b0327dbad fix #2767 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-02 09:19:23 -08:00
Nikolaj Bjorner
2bf9b5ca8b fix #2767 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-02 09:15:04 -08:00
Nikolaj Bjorner
17d67c1b50 fix #2726 2019-12-01 20:14:35 -08:00
Nikolaj Bjorner
86c35bc7c1 fix #2763 2019-12-01 17:10:21 -08:00
Nikolaj Bjorner
ad309e53a1 fix #2766 2019-12-01 16:06:14 -08:00
Nikolaj Bjorner
9ebaf19e47 fix #2765 2019-12-01 15:05:38 -08:00
Nikolaj Bjorner
23fcc21543 fix #2764 
fix #2764
 2019-12-01 12:05:58 -08:00
Nikolaj Bjorner
b371592c0d unused variable warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-30 19:21:35 -08:00
Nikolaj Bjorner
320d6640b1 ensure unfolding is increased with seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-30 18:32:19 -08:00
Nikolaj Bjorner
489448b869 fix #2762, fix #2750, add iterative unrolling to help on termination on sat instances (to address non-termination in #2759 and #2762) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-30 18:05:24 -08:00
Nikolaj Bjorner
0d004b5232 fix #2761 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-30 10:31:26 -08:00
Nikolaj Bjorner
cdf3c48349 clear memory on allocation to avoid msan warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-29 15:50:49 -08:00
Nikolaj Bjorner
7e452254c3 distribute string and regex concatenation on literals, scenario exposed by #2668 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-29 11:24:18 -08:00
Nikolaj Bjorner
b479c34c0b fix #2751 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-29 10:18:55 -08:00
Nikolaj Bjorner
001ddef058 fix #2749 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-29 10:18:55 -08:00
Murphy Berzish
bf28b815fa z3str3: add a method to rewrite-and-assert an axiom to reduce boilerplate 2019-11-29 09:37:22 -08:00
Murphy Berzish
b8f2cf5b0b z3str3: rewrite strong arrangement axiom to avoid assertion violation 2019-11-29 09:37:22 -08:00
Nikolaj Bjorner
a257ec0cc1 build warnings #2748 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-28 15:36:54 -08:00
Federico Mora
30d9ea5c2c Addressing comments from pull request: more descriptive variable names and m.mk_not 2019-11-27 22:06:59 -08:00
Federico Mora
574051df1b Step by step derivation of second int.to.str axiom 2019-11-27 22:06:59 -08:00
Federico Mora
900e707619 Added more comments 2019-11-27 22:06:59 -08:00
Federico Mora
6ffb475007 Add comments and make implication into xor. Logically equivalent. 2019-11-27 22:06:59 -08:00
Federico Mora
fc74689c1b int.to.str must not begin with 0 unless is 0 2019-11-27 22:06:59 -08:00
Nikolaj Bjorner
0b893afee4 pretty print algebraic numbers from fast pretty printer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-27 17:13:15 -08:00
Nikolaj Bjorner
c36d9f7b3e fix #2741 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-26 19:45:34 -08:00
Murphy Berzish
5f78ca9b58 z3str3: negative lengths in get_len_value don't count 2019-11-25 12:32:51 -08:00
Andreas Humenberger
58f3dce2be Make z3::exception a subclass of std::exception 2019-11-25 11:55:37 -08:00
Nikolaj Bjorner
055cf6c7b9 relevancy level is queried during smt_setup, so it has to update the local parameter that tracks the min 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-25 09:53:00 -08:00
Christoph M. Wintersteiger
ba03d99526
Fix forward declaration of fma in C++ API. Fixes #2735. 2019-11-25 11:32:50 +00:00
Nikolaj Bjorner
84025d5c11 add rewrites for moduli as exercised in example from #2319 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-24 19:02:28 -08:00
Nikolaj Bjorner
fad4356159 treat division by 0 as non-linearity, fix #2733 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-24 10:52:52 -08:00
Nikolaj Bjorner
ca2ad66d03 treat division by 0 as non-linearity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-24 10:49:35 -08:00
Nikolaj Bjorner
e2b6b12215 initialize relvancy level in constructor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-23 17:26:59 -08:00