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
Murphy Berzish
fb20951064
theory_str Substr support WIP
2016-06-15 20:26:07 -04:00
