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

4674 commits

Author SHA1 Message Date
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
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
Murphy Berzish 2c91f388df add defensive double-non-concat check in theory_str::simplify_concat_equality() 2016-08-06 15:35:47 -04:00
Murphy Berzish 91c336d7ee fix erroneous vector double-insert in theory_str::group_terms_by_eqc() 2016-08-06 15:32:37 -04:00
Murphy Berzish 0c4e725902 finish theory_str::mk_concat, no caching of generated terms yet 2016-08-04 16:40:05 -04:00
Murphy Berzish bc91d182bf mk_concat fixes WIP 2016-08-03 13:39:14 -04:00
Murphy Berzish 3c2fe497de modify theory_str::get_value() to check EQC for a numeral 
Instead of asking the arithmetic theory for the current assignment,
we return the (unique) numeral in the equivalence class of the term
whose length we want to know.

This is because the arithmetic theory may return a default / internal
value that doesn't correspond to anything actually asserted by the core solver.
 2016-08-02 16:44:54 -04:00
Murphy Berzish 45c4954959 add debugging to theory_str::get_len_value in preparation for fixes 2016-08-02 14:52:44 -04:00
Murphy Berzish a51ad07e3f crash avoidance in propagation of basic string axioms and gen_len_test_options 2016-08-01 20:52:49 -04:00
Murphy Berzish 97f07a8a7c fix debugging statements in theory_str::gen_len_test_options 
this fixes charAt-007.smt2 and prevents two unique crashes
 2016-08-01 18:14:56 -04:00
Murphy Berzish ee1af96f1b add opt_NoQuickReturn_IntegerTheory check in theory_str::new_eq_check() 
This allows us to assert an "inconsistent length" axiom from the integer theory
while continuing in new_eq_handler(). Currently active when
opt_NoQuickReturn_IntegerTheory is 'true' but this may be necessary
here and in other places, in general, to fix integer theory integration.
 2016-08-01 17:05:02 -04:00
Murphy Berzish 6e348720b1 add integer theory integration to theory_str::solve_concat_eq_str case 4 2016-07-31 18:12:57 -04:00
Murphy Berzish 778c0a5563 improve theory_str::group_terms_by_eqc now that we have simplify_concat 2016-07-31 16:55:17 -04:00
Murphy Berzish 9ceb2df28f add integer integration to theory_str::simplify_parent 2016-07-31 16:51:35 -04:00
Murphy Berzish 41497f44c1 prevent checking scope of XOR variables in theory_str::process_concat_eq 2016-07-31 16:30:52 -04:00
Murphy Berzish f5b82740c3 debugging length testers in theory_str::gen_len_val_options_for_free_var 2016-07-31 16:26:56 -04:00
Murphy Berzish 8958eea27c crash avoidance in theory_str cut_var_map writes 2016-07-31 11:22:04 -04:00
Murphy Berzish 7f3a260eda more aggressive simplifications in theory_str::handle equality, WIP, not tested yet 2016-07-30 16:58:59 -04:00
Murphy Berzish 6f67e9cdda fix theory_str::check_length_concat_concat to actually assert the conflict axiom 2016-07-28 17:18:56 -04:00
Murphy Berzish 244b611f1c fix infinite loop bug in theory_str::new_eq_check 2016-07-28 17:10:41 -04:00