mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
7010 commits 49 branches 53 tags 182 MiB
Commit graph

7010 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
7562efbe84 add consequence command 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-30 12:59:29 -07: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
7d545d902d switch to specialized consequence generator in combined_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-29 17:36:11 -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
82d0310d94 remove repeated default argument, remove tabs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 21:13:12 -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
fa48703445 fix build for non C++11 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 17:04:47 -07:00
Nikolaj Bjorner
0055254f4c fix build for non C++11 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 17:04:06 -07:00
Christoph M. Wintersteiger
2e362aa6c0 build fix 2016-07-29 01:02:48 +01:00
Nikolaj Bjorner
46c911a92f Merge pull request #700 from lorisdanto/master 
added symbolic automata complement for sequences
 2016-07-28 17:00:23 -07:00
Christoph M. Wintersteiger
6e85c5e987 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-29 00:55:22 +01:00
Christoph M. Wintersteiger
7fd931d480 build fix 2016-07-29 00:55:05 +01:00
Nikolaj Bjorner
55cffc5247 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-28 16:49: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
Loris D'Antoni
73bd4acfc5 added symbolic automata complement for sequences 2016-07-28 13:50:05 -07: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
Christoph M. Wintersteiger
5f449b5c0d Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-28 19:52:56 +01:00
Nikolaj Bjorner
ceb3f0c869 patch full version for cmake to re-enable build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 11:30:39 -07:00
Nikolaj Bjorner
074f1ad778 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-28 11:20:23 -07:00
Nikolaj Bjorner
14f29e7265 add basic built-in consequence finding 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 11:20:17 -07:00
Christoph M. Wintersteiger
d5954e829b Enabled donet key file in dist scripts 2016-07-28 18:49:57 +01:00
Christoph M. Wintersteiger
6f874c5c1d Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-28 18:07:48 +01:00
Christoph M. Wintersteiger
7fefe40f21 Added/improved facilities for strong name signing of the .NET assembly. 2016-07-28 18:07:34 +01:00
Christoph M. Wintersteiger
0d83f99d8d Fixed comment 2016-07-28 18:06:26 +01:00
Christoph M. Wintersteiger
3587baaf24 Added full version strings and associated API functions. 2016-07-28 18:06:02 +01:00
Nikolaj Bjorner
b7de813c63 set solver on simplify command 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-27 15:35:44 -07:00
Nikolaj Bjorner
0997eba700 adding hash/eq to uint_set 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-27 13:41:41 -07: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
Nikolaj Bjorner
1239c8f8e8 update MSF example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-27 11:20:31 -07:00
Murphy Berzish
1c518be61d new_eq_handler improvements in theory_str, WIP 2016-07-27 12:46:35 -04:00
Nikolaj Bjorner
5f5ef8b38d adding support for distinct for dt2bv, re-entry harness for ~Context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-27 09:02:56 -07:00