mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-20 23:56:37 +00:00
Code Activity
5590 commits 23 branches 48 tags 157 MiB
Commit graph

5590 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Murphy Berzish 999420485b add theory_str::check_length_eq_var_concat and helper methods 2016-07-28 16:49:39 -04:00
Murphy Berzish 76ceac6664 add theory_str::check_length_const_string 2016-07-28 16:31:40 -04:00
Murphy Berzish 95f1cfa5a6 add theory_str::check_length_consistency, WIP 2016-07-27 16:18:05 -04:00
Murphy Berzish a31a948a5b add theory_str::can_concat_eq_concat 2016-07-27 15:21:33 -04:00
Murphy Berzish ceed3f3ff0 add theory_str::can_concat_eq_str 2016-07-27 15:15:01 -04:00
Murphy Berzish 1c518be61d new_eq_handler improvements in theory_str, WIP 2016-07-27 12:46:35 -04:00
Murphy Berzish f555074e27 add option to disable integer theory integration in theory_str; this is currently ENABLED 2016-07-23 23:29:56 -04:00
Murphy Berzish 02a66c425e add option to bypass quick returns in integer theory integration in theory_str 
this might not actually be that useful, if the problem is, as I suspect it to be,
that values we get from the integer theory need not correspond with
assertions in the core (that can get popped off the stack, etc.)
 2016-07-23 22:43:46 -04:00
Murphy Berzish ac16aa7c81 fix out-of-scope variable bug in theory_str::process_concat_eq_type6 
this fix will have to be made to all functions that use varForBreakConcat
 2016-07-23 16:02:11 -04:00
Murphy Berzish 0f38203779 add RegexCharRange to theory_str 2016-07-19 16:39:43 -04:00
Murphy Berzish 9ffcd135d5 add RegexPlus to theory_str 2016-07-19 15:47:41 -04:00
Murphy Berzish 8d47b08244 fix out-of-scope value tester bug in theory_str::gen_free_var_options() 
we now pass tests/z3str/charAt-003.smt2 with detailed debugging turned off!
 2016-07-10 13:05:41 -04:00
Murphy Berzish 8aa6fee0af fixups wip 2016-07-08 12:21:11 -04:00
Murphy Berzish 847a5fc1f8 replace old mk_value behaviour in theory_str that creates placeholders for unused terms instead of crashing 2016-07-07 16:13:48 -04:00
Murphy Berzish 9eead64d03 prevent assertion of basic string axioms on variables that go out of scope (theory_str) 
this is testing a crash avoidance feature, the regression is tests/z3str/regex-026.smt2

this also adds some debugging code for a substr() crash but that is WIP
 2016-07-06 17:31:37 -04:00
Murphy Berzish 7d903ff1fa implement process_concat_eq_unroll, WIP 2016-06-30 04:55:11 -04:00
Murphy Berzish b53da182b6 fix gen_assign_unroll_reg so that it does not assert a contradiction 2016-06-30 04:39:09 -04:00
Murphy Berzish a2d6149df5 add general-case regex unroll model generation 
WIP as there is currently a SAT-as-UNSAT bug I'm trying to fix

This also changes the semantics of lower_bound and upper_bound,
no longer wrapping the expr that is passed in with mk_strlen().
This actually makes these methods useful for checking bounds
of things other than strings.
 2016-06-30 04:00:42 -04:00
Murphy Berzish b4110c886f successful unroll of simple unbounded Str2Reg 2016-06-30 02:46:16 -04:00
Murphy Berzish 427632ede3 let free variable assignment work a bit more towards unrolls 2016-06-30 01:42:00 -04:00
Murphy Berzish 21f0a50aba add Unroll check to get_eqc_allUnroll 2016-06-30 01:24:43 -04:00
Murphy Berzish 03827cb487 add more Unroll support to final_check, ctx_dep_analysis 2016-06-30 01:21:21 -04:00
Murphy Berzish b31d1a92aa add more support for unroll (WIP) 2016-06-27 14:41:57 -04:00
Murphy Berzish 020e8aef6d regex union 2016-06-23 17:14:03 -04:00
Murphy Berzish 04803d7a3b starting regex support 2016-06-23 15:24:35 -04:00
Murphy Berzish 4c34629806 starting regex support, rewriter 2016-06-21 21:13:16 -04:00
Murphy Berzish a808a8c587 theory_str infer_len_concat_arg 2016-06-21 17:38:49 -04:00
Murphy Berzish 1e46782392 theory_str infer_len_concat 2016-06-21 17:25:28 -04:00
Murphy Berzish ba42478f9b string-integer wip 2016-06-20 20:02:22 -04:00
Murphy Berzish 89a337ba7e quick path with string-integer integration in theory_str::simplify_concat_equality 2016-06-19 18:25:31 -04:00
Murphy Berzish 5b3c868c90 theory_str Replace method 2016-06-15 21:14:54 -04:00