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

5685 commits

This branch
This branch
All branches
Author SHA1 Message Date
Murphy Berzish
361f02ef1d remove assignment refcount hack from theory_str::pop_scope_eh 2016-11-28 21:34:55 -05:00
Murphy Berzish
f968f79d1c refactor solve_concat_eq_str to use expr_ref_vector 2016-11-28 18:47:42 -05:00
Murphy Berzish
b77f6666dc refactor process_concat_eq_type_6 to use expr_ref_vector 2016-11-28 18:40:28 -05:00
Murphy Berzish
1e65511a3f save a few functions to trail in theory_str 2016-11-28 16:21:26 -05:00
Murphy Berzish
8c33dfab39 fix escape character overflow print 2016-11-27 20:51:34 -05:00
Murphy Berzish
1fa8129c8f pretty-printing of general escape sequences for string literals 2016-11-25 18:02:24 -05:00
Murphy Berzish
889b6be2c3 fix smt-lib 2.5 double quotes in pp 2016-11-23 19:03:53 -05:00
Murphy Berzish
8e962aa427 escape chars in smt2 printing of string constants 2016-11-22 18:32:03 -05:00
Murphy Berzish
11d8ffc4d4 escape characters in theory_str 2016-11-22 18:21:40 -05:00
Murphy Berzish
5e37a21802 fix expr_ref in theory_str splits WIP 2016-11-18 16:07:20 -05:00
Murphy Berzish
855037eed7 refactor process_concat_eq_type2 in theory_str; fixes unsat/big/8558 2016-11-17 16:25:53 -05:00
Murphy Berzish
d260218e2b tabs to spaces test 2016-11-17 15:28:26 -05:00
Murphy Berzish
e2d05578d6 add extra trace message in smt_context for theory_str results change 2016-11-17 15:25:39 -05:00
Murphy Berzish
55ae83f47e Revert "experimental modification to simplify_parent call in theory_str, WIP" 
This reverts commit 9771428600.
 2016-11-16 13:00:05 -05:00
Murphy Berzish
9771428600 experimental modification to simplify_parent call in theory_str, WIP 2016-11-15 15:18:07 -05:00
Murphy Berzish
df6b461117 enhanced backpropagation in theory_str final_check for var=concat terms 
fixes kaluza sat/big/709.smt2
 2016-11-14 12:33:23 -05:00
Murphy Berzish
02aacab04e add z3str2-style free variable check to theory_str 2016-11-11 17:52:18 -05:00
Murphy Berzish
fbaee080b2 fix performance regression introduced with theory_str str.from-int 
more investigation is required to understand why this works.
 2016-11-11 00:32:50 -05:00
Murphy Berzish
5635016205 theory_str str.from-int very WIP 2016-11-09 18:06:02 -05:00
Murphy Berzish
fff1fadf3b add str.from-int in theory_str rewriter 2016-11-09 15:54:22 -05:00
Murphy Berzish
4aa2d965b3 Merge branch 'develop' of github.com:mtrberzi/z3 into develop 2016-11-09 14:05:38 -05:00
Murphy Berzish
61d1d5e8b0 add cache for length terms to theory_str, but it seems to slow things down so I disabled it 2016-11-08 15:20:47 -05:00
Murphy Berzish
521e0e175b refresh reused split vars in theory_str 
this fixes kaluza/unsat/big/7907, now SAT in ~30s
 2016-11-08 14:23:10 -05:00
Murphy Berzish
3ae336fa6f add experimental value tester caching to theory_str 2016-11-02 13:05:16 -04:00
Murphy Berzish
a61e1f17e8 fix crash in gen_len_test_options when fast length testers are disabled 2016-11-02 12:35:14 -04:00
Murphy Berzish
3da78f9d80 experimental cached length testers in theory_str 2016-11-01 20:35:01 -04:00
Murphy Berzish
a5b00641d8 Merge branch 'develop' of github.com:mtrberzi/z3 into develop 2016-11-01 13:02:59 -04:00
Murphy Berzish
452eed6626 move get_std_regex_str to str_util 2016-10-29 12:19:24 -04:00
Murphy Berzish
b06b9f9264 str.to-int WIP 2016-10-21 13:35:35 -04:00
Murphy Berzish
ef0f6f1de3 add str.to-int in theory_str WIP 2016-10-20 16:01:51 -04:00
Murphy Berzish
05dfa5509a theory_str high-level and regex API 2016-10-20 15:36:54 -04:00
Murphy Berzish
d57c92f69e theory_str api: concat, length 2016-10-20 12:25:52 -04:00
Murphy Berzish
ce53b36864 theory_str API started 2016-10-14 12:34:11 -04:00
Murphy Berzish
dc8062ba67 patch out contains check for substr reduction 
fixes all regressions in release build, we may want to revisit this later
 2016-09-22 20:14:42 -04:00
Murphy Berzish
1061cdf58a fix value tester theory var reuse in theory_str 
fixes release regression in charAt-007
 2016-09-22 15:40:43 -04:00
Murphy Berzish
4433417b6e faster push_scope in theory_str 2016-09-20 16:25:28 -04:00
Murphy Berzish
feef85c129 override scope check in theory_str::solve_concat_eq_str 
fixes indexof2-009.smt2
 2016-09-20 15:37:29 -04:00
Murphy Berzish
48eaa6159c disable aggressive unroll testing in theory_str, it may be doing more harm than good 2016-09-20 01:10:27 -04:00
Murphy Berzish
447c6e4ce3 refresh length tester in theory_str::gen_len_val_options_for_free_var 
fixes charAt-007.smt2
 2016-09-20 00:28:29 -04:00
Murphy Berzish
f1d7ffcdce fix regression regex-020 2016-09-20 00:14:38 -04:00
Murphy Berzish
9615b191de theory_str hacking for theory var stuff WIP 2016-09-19 23:40:17 -04:00
Murphy Berzish
c38f63dd2a fix eqc management and unroll test var gen in theory_str::final_check 2016-09-19 19:42:16 -04:00
Murphy Berzish
91b625768c fix tracing in theory_str 2016-09-15 17:01:59 -04:00
Murphy Berzish
e7c0c29ae5 potentially fix out-of-scope infinite loop bug in theory_str gen_unroll_conditional_options 2016-09-15 15:59:56 -04:00
Murphy Berzish
8776b97841 variable scope correctness hack in theory_str 2016-09-14 22:08:40 -04:00
Murphy Berzish
bed40c45b8 cleanup 2016-09-14 21:48:27 -04:00
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