mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
8223 commits 49 branches 53 tags 182 MiB
Commit graph

8223 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
dc48008d46 fixestoconsequences 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-02 11:00:40 +08:00
Nikolaj Bjorner
c746d46d80 add validation code, fix bugs in consequence finder 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-01 16:21:23 +08:00
Murphy Berzish
f9b4f21683 add rewrite for theory_str rewriter RegexPlus 
fixes regex-013.smt2
 2016-08-31 19:22:04 -04:00
Murphy Berzish
5e22bc57c8 theory_str cleanup 2016-08-31 19:19:23 -04:00
Nikolaj Bjorner
4d9aadde35 updated consequence finder to fix bug in processing enumeration types 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-31 16:15:36 +08:00
Nikolaj Bjorner
237fde1f76 fix crash during shutdown. Issue #719 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-31 09:57:46 +08:00
Nikolaj Bjorner
310c0f31a1 use type constrsaints for co-variant subtying to enable .net 3.5 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-30 12:07:06 +08:00
Nikolaj Bjorner
d4539b8887 fix dt2bv transformation to only work with constants, issue #725 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-30 11:42:14 +08:00
Nikolaj Bjorner
882c3bd0cd fix unused variable warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-23 18:18:11 -03:00
Nikolaj Bjorner
510231df42 fix to #717. The bottom-up COI filter can only use positive facts for filtering 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-23 12:26:38 -03:00
Nikolaj Bjorner
b5c521e4b2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-08-23 11:44:48 -03:00
Nikolaj Bjorner
0a09d5ff52 check for non-nullness when handling optional info fields for marking. Fixes issue #719 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-23 11:33:40 -03:00
Murphy Berzish
89d5f4ffb4 add compute_contains check to theory_str 
this may cause a crash in indexof-002.smt2 but
I cannot reproduce it
 2016-08-21 21:37:46 -04:00
Murphy Berzish
2a199294a1 remove incorrect null pointer check from theory_str::gen_len_val_options_for_free_var 
everything that calls this method knows that it can legally return null
 2016-08-21 00:43:00 -04:00
Murphy Berzish
7b3203b48e disable aggressive length/value testing in theory_str, it seems to be detrimental 2016-08-21 00:30:29 -04:00
Murphy Berzish
1a75781a3c add experimental option to defer new_eq_check to final_check in theory_str 2016-08-20 23:09:08 -04:00
Christoph M. Wintersteiger
b03dc0af3b fixed memory leaks 2016-08-20 17:57:00 -04:00
Christoph M. Wintersteiger
47e95f8676 Fixed binding substitution in macro_util 2016-08-20 17:56:52 -04:00
Nikolaj Bjorner
879f792125 fix axiomatization of str.replace. Fixes issue #703 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-20 06:13:52 -07:00
Nikolaj Bjorner
2d8325ed43 fix axiomatization of str.replace. Fixes issue #703 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-20 06:05:13 -07:00
Nikolaj Bjorner
439e8e6b04 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-08-20 03:53:55 -07:00
Nikolaj Bjorner
f2b5c11d1c add option for prettier proof printing, Issue #706 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-20 03:52:45 -07:00
Murphy Berzish
481e97a274 propagate early in theory_str to set up contains/regex maps 
this fixes an unsat-as-sat error in a regex test and flips around some timeouts
so more work will be required to track this down
 2016-08-19 22:53:36 -04:00
Nikolaj Bjorner
5069da62a3 safe sat clause_offset in debug mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-19 08:45:06 -07:00
Nikolaj Bjorner
e132c5eae8 safe sat clause_offset in debug mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-19 08:42:40 -07:00
Nikolaj Bjorner
b2383a481a Merge branch 'master' of https://github.com/Z3Prover/z3 2016-08-18 18:02:22 -07:00
Nikolaj Bjorner
665fccf07a addressing max-segment issue for AMD64 + Debug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-18 18:01:29 -07:00
Murphy Berzish
8598a48e3b fix weird Contains rewriter behaviour in theory_str 2016-08-18 19:14:50 -04:00
Murphy Berzish
3c8b833eeb fix expression dereference error in theory_str::gen_assign_unroll_Str2Reg 2016-08-18 17:03:32 -04:00
Murphy Berzish
54d7e4bbb5 remove the option to bypass check_regex_in in theory_str 2016-08-17 21:12:19 -04:00
Murphy Berzish
6263391c11 fix out-of-range integer comparison bug in string NFA 2016-08-17 20:58:57 -04:00
Murphy Berzish
71ad4d3a4a add regex_in_bool_map to theory_str 2016-08-17 16:21:19 -04:00
Murphy Berzish
0834229b39 theory_str model validation for substr 2016-08-17 15:33:02 -04:00
Murphy Berzish
48081864b0 add regex validation in str_rewriter 2016-08-16 18:07:31 -04:00
Murphy Berzish
685edbb268 pull out incorrectly-used data structures in theory_str for contains check, this will need to be revisited 2016-08-15 18:58:36 -04:00
Murphy Berzish
d28ef1d471 add theory_str::check_contain_by_eq_nodes 2016-08-15 17:38:24 -04:00
Murphy Berzish
f48377e780 temporarily disable a third Contains check for testing purposes 2016-08-14 16:14:48 -04:00
Murphy Berzish
ee6f1eef69 add theory_str::check_contain_by_substr 2016-08-14 15:14:48 -04:00
Murphy Berzish
1f594b190a add theory_str::check_contain_by_eqc_val 2016-08-14 14:55:29 -04:00
Murphy Berzish
6612971049 start adding Contains checks to theory_str 2016-08-14 14:15:29 -04:00
Christoph M. Wintersteiger
e8141aaa84 debug fixes 2016-08-12 19:52:59 +01:00
Christoph M. Wintersteiger
244c641234 debug check fix 2016-08-12 13:19:12 +01:00
Christoph M. Wintersteiger
b74bff7fb7 logic detection fix 2016-08-10 11:39:47 +01:00
Murphy Berzish
f7ba3ff084 crash avoidance in theory_str search start, fixes length-001.smt2 regression 2016-08-09 20:11:25 -04:00
Christoph M. Wintersteiger
f54a7db108 Added debug traces. 2016-08-09 16:36:49 +01:00
Christoph M. Wintersteiger
ff3c630207 .NET API: Added MkMul from IEnumerable. 2016-08-09 16:36:32 +01:00
Christoph M. Wintersteiger
03aa6914a3 Fixed sub-logic detection for the ALL logic. 2016-08-09 13:20:45 +01:00
Murphy Berzish
3dff240bb3 theory_str model validation for Length 2016-08-07 15:50:41 -04:00
Murphy Berzish
cb566ad5ce fix model validation for theory_str 2016-08-07 15:43:08 -04:00
Murphy Berzish
395ec4543c avoid crash in theory_str, this leaks memory 2016-08-06 22:19:10 -04:00