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
Murphy Berzish
fb20951064
theory_str Substr support WIP
2016-06-15 20:26:07 -04:00
Murphy Berzish
be5bf7fb80
LastIndexof support
2016-06-15 18:45:01 -04:00
Murphy Berzish
7c8b882ae6
decl and rewriter support for LastIndexof in theory_str (WIP)
2016-06-15 18:04:33 -04:00
Murphy Berzish
dc5a334d42
support for Indexof2 in theory_str
2016-06-15 17:37:17 -04:00
Murphy Berzish
881e3056f3
support for IndexOf in theory_str
2016-06-14 21:28:31 -04:00
Murphy Berzish
db2a5854e9
decl and rewriter for Indexof (WIP)
2016-06-14 20:10:06 -04:00
