mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-06 16:01:55 +00:00
Code Activity
13711 commits 28 branches 52 tags 171 MiB
Commit graph

3197 commits

Author SHA1 Message Date
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
Christoph M. Wintersteiger
f54a7db108 Added debug traces. 2016-08-09 16:36:49 +01: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
Nikolaj Bjorner
6582330cc4 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-03 14:25:57 -07:00
Nikolaj Bjorner
bbfe02b25a modulating data-type solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-03 11:16:29 -07:00
Nikolaj Bjorner
491b3b34aa tune consequence finding. Factor solver pretty-printing as SMT-LIB into top-level 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-03 11:14:29 -07: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
Nikolaj Bjorner
cb2d8d2107 add detection of non-fixed variables to consequence finding 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-30 19:12:41 -07:00
Murphy Berzish
7f3a260eda more aggressive simplifications in theory_str::handle equality, WIP, not tested yet 2016-07-30 16:58:59 -04:00
Nikolaj Bjorner
7346098895 fix unsat core extraction code in smt_context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-30 11:22:34 -07:00
Nikolaj Bjorner
d32019f4c9 fix consequence tracking for negated assumptions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-30 10:49:06 -07:00
Nikolaj Bjorner
2263be1b4d adding consequence examples 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-29 17:24:14 -07:00
Nikolaj Bjorner
5c99405db3 finish consequence fast path code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 20:15:47 -07:00
Nikolaj Bjorner
4958edeb42 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 19:40:49 -07:00
Nikolaj Bjorner
8221a09659 fast path for antecedent extraction in smt_context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 16:49:19 -07: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
Nikolaj Bjorner
56c78753f0 updating default solver selection. Add dt2bv transformation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-24 18:16:32 -07: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
Nikolaj Bjorner
a59ed0fc2f Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-20 12:18:16 -07:00
Nikolaj Bjorner
60711bb0cd deal with model construction, issue #684. fix model construction for ite #678. WIth this version, issue #686 does not repro 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-20 12:18:07 -07:00
Nikolaj Bjorner
5f39c4371c fix proof generation for unit resolution. Issue #691 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-20 11:54:39 -07:00
Nikolaj Bjorner
6559fd817d Fix bit-blasting discrepancy. #690 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-20 10:53:53 -07:00
Nikolaj Bjorner
f30fb7639e Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-13 20:32:24 -07:00
Nikolaj Bjorner
3989d238c0 fix bugs exposed in #677. to_int(x) has the semantics that to_int(x) <= x, and to_int(x) is the largest integer satisfying this inequality. The encoding in purify_arith had it the other way x <= to_int(x) contrary to how to_int(x) is handled elsewhere. Another bug in theory_arith for mixed-integer linear case was also exposed. Fractional bounds on expressions of the form to_int(x), and more generally on integer rows were not rounded prior to internalization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-13 20:32:18 -07:00