mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity
6457 commits 24 branches 48 tags 158 MiB
Commit graph

6457 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner
375682e98d Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-26 14:31:40 -07:00
Nikolaj Bjorner
9cab896632 adding sign option if keyfile is present 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-26 14:31:29 -07:00
Christoph M. Wintersteiger
8fa29f6970 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-26 19:21:57 +01:00