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

5639 commits

This branch
This branch
All branches
Author SHA1 Message Date
Murphy Berzish
ad7247df51 make calls to theory_str::dump_assignments depend on the correct trace flags 2016-09-14 19:32:14 -04:00
Murphy Berzish
15055c8041 use mk_int_var to make xor terms 2016-09-14 19:01:14 -04:00
Murphy Berzish
d334403720 remove relevancy testing experiment 2016-09-14 17:42:40 -04:00
Murphy Berzish
f22f4da023 remove unused variable 2016-09-14 17:33:47 -04:00
Murphy Berzish
9ee7326a19 tweaks to process_concat_eq_type_3 2016-09-14 17:26:52 -04:00
Murphy Berzish
a294c145dc add theory_str::try_eval_concat to work around rewriter behaviour 
this fixes a regression in concat-013.smt2
 2016-09-14 16:18:03 -04:00
Murphy Berzish
e46fc7b0b6 fix expr-app conversion 2016-09-14 15:51:33 -04:00
Murphy Berzish
804009a757 use z3str2 eqc semantics for get_eqc_value 2016-09-14 15:37:48 -04:00
Murphy Berzish
50353168ef fix semantics of get_concats_in_eqc and get_var_in_eqc 2016-09-14 15:36:36 -04:00
Murphy Berzish
87d61d6d6e fix semantics of in_same_eqc 2016-09-14 15:35:37 -04:00
Murphy Berzish
ec9e1686f7 fix semantics of collect_eq_nodes and simplify_parent 2016-09-14 15:32:49 -04:00
Murphy Berzish
9481601b4b restore z3str2 eqc semantics in theory_str::new_eq_check 2016-09-14 15:15:47 -04:00
Murphy Berzish
34dc655150 z3str2 eqc semantics for theory_str unroll checks 2016-09-13 18:24:59 -04:00
Murphy Berzish
8f636e1f57 fix typo'ed set reference in handle_equality 2016-09-13 18:16:21 -04:00
Murphy Berzish
aea0032aa7 manage our own union-find structure in theory_str 
concat-086.smt2 passes with this, for the first time ever
 2016-09-13 18:01:45 -04:00
Murphy Berzish
ca71a20ab7 add caching to theory_str::mk_concat, WIP 2016-09-12 17:17:17 -04:00
Murphy Berzish
015016c92b disable variable scope check if not tracing in theory_str 2016-09-12 16:57:05 -04:00
Murphy Berzish
b3fddf4707 performance optimization in theory_str::classify_ast_by_type 2016-09-12 16:41:35 -04:00
Murphy Berzish
2c5569aa1f change cut_var_map to obj_map 2016-09-12 15:43:58 -04:00
Murphy Berzish
82e07aae8c disable deferred eqc check in theory_str 2016-09-08 19:55:08 -04:00
Murphy Berzish
c83e39d3b8 fix incorrect axiom in theory_str for Contains check 
this partially fixes a regression in contains-034.smt2, which now
is at least not a SAT-as-UNSAT
 2016-09-05 17:45:10 -04:00
Murphy Berzish
7b34efada7 add aggressive unroll test option to theory_str 2016-09-04 18:48:15 -04:00
Murphy Berzish
347f441517 add a check for variable scope to theory_str 2016-09-02 20:44:14 -04:00
Murphy Berzish
2b8f165cc4 patch UNSAT to UNKNOWN in cmd_context for theory_str 2016-09-02 19:04:20 -04:00
Murphy Berzish
d3062a8eff omit out-of-scope length testers from axiom premise in theory_str::gen_len_test_options 
this fixes a regression in charAt-007.smt2
 2016-09-02 18:23:41 -04: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
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
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
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
Murphy Berzish
f7ba3ff084 crash avoidance in theory_str search start, fixes length-001.smt2 regression 2016-08-09 20:11:25 -04: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
Murphy Berzish
43b0cd5010 clean up unused variables in theory_str.cpp 2016-08-06 15:38:58 -04:00