mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-17 09:56:39 +00:00
Code Activity
4050 commits 43 branches 51 tags 169 MiB
Commit graph

72 commits

Author SHA1 Message Date
Nikolaj Bjorner
05c6ed1698 fixing issue #254 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-22 09:54:05 -07:00
Nikolaj Bjorner
ac902dad1a fix another regression and missing detection of bounds, Issue #254 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-22 08:53:12 -07:00
Nikolaj Bjorner
ffa78b95ab fix unbounded, issue #252 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-21 14:38:47 -07:00
Nikolaj Bjorner
6e852762ba patch for issue #232 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-06 19:07:47 -07:00
Nikolaj Bjorner
d7da64f946 fix crash with incorrect bound computation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-08 16:27:57 -07:00
Nikolaj Bjorner
73a8f9960f fix regressions exposed in Internal 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-07 20:17:46 -07:00
Nikolaj Bjorner
963981b3a6 fix memory alias bug and non-termination bug exposed by issue #184 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-31 14:45:10 -07:00
Nikolaj Bjorner
0ed38ed59b add option for using corr set and use partial cores 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-30 14:48:24 -07:00
Nikolaj Bjorner
7f219e84de check cancellation flag in min/max. Fixes issue #206 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-29 15:51:58 -07:00
Nikolaj Bjorner
655b44c07b make :weight understand both decimal and integral values, remove dweight, remove deprecated commands for optimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-15 00:48:22 +02:00
Nikolaj Bjorner
96c8b1e7ff fixup model construction on undef results for arithmetic. Fixes issue #161 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-13 12:44:07 -07:00
Nikolaj Bjorner
4bc044c982 update header guards to be C++ style. Fixes issue #9 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-08 23:18:40 -07:00
Nikolaj Bjorner
d815cf9b7b fix bug in optimization where a variable is updated twice 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-07 16:01:48 -07:00
Nikolaj Bjorner
d9522cfd07 fix mixed integer/real bugs for maximization exposed by non-termination in slow.smt. partially fixes issue #56 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-23 12:05:19 +02:00
Nikolaj Bjorner
9734407cde disable throttle on unbounded objectives in shared theories. It may violate an interface equality, to fix issue #120 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-06-02 11:14:59 -07:00
Nikolaj Bjorner
e8811748d3 fix regressions in nl/smt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-16 19:08:37 +01:00
Nikolaj Bjorner
64bd62b17e fix gcc compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-16 11:56:04 +01:00
Nikolaj Bjorner
ffc3a36dcb checked ite-expressions as shared for bounds detection 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-23 19:59:33 +02:00
Nikolaj Bjorner
51267f3aba take into account that bound from optimization may create atom that clashes with inequality bound from term 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-03-11 00:26:49 -07:00
Nikolaj Bjorner
e50e02e656 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2015-01-20 16:38:55 -08:00
Nikolaj Bjorner
e24db56650 integrating new integer primal loop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-01-20 16:38:45 -08:00
Nikolaj Bjorner
82f1e81ac2 fix build errors on gcc 
Signed-off-by: Nikolaj Bjorner <nbjorner@z3-mac.local>
 2015-01-19 00:50:08 +00:00
Nikolaj Bjorner
4bb5302def template args 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-01-18 15:54:18 -08:00
Nikolaj Bjorner
d45c7ce082 prepare revised primal phase 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-01-18 04:11:40 +05:30
Nikolaj Bjorner
e28701a64c add assertions to simplifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-01-14 22:09:48 +05:30
Nikolaj Bjorner
52c6f7c3b1 refine the safety check for leaving basis. As long as all base variables are unbounded in compatible directions as the non-basic variable we can detect unbounded variables. This partial check fixes integer divergence in a case exposed by Karpenov. Establishing or converting this to a check that always identifies unbounded integer variables is left for further analysis. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-01-06 15:22:40 -08:00
Nikolaj Bjorner
ae3d16bc50 fix overflow and integrality bugs reported by Phan 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-12-15 16:18:09 -08:00
Nikolaj Bjorner
08cb8b8de8 address divergence in the case of shared theory symbols. Codeplex issue 147, thanks to George Karpenkov 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-12-09 16:04:25 +01:00
Nikolaj Bjorner
ce18421a7a fix box 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-15 14:29:39 -07:00
Nikolaj Bjorner
465eafbf45 fix assertion for integrality, lax noprogress bail out code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-09 05:04:00 +02:00
Nikolaj Bjorner
57fc0f3f55 bug fixes to min-max, and experiments with hsmax 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-28 15:44:39 -07:00
Nikolaj Bjorner
ff1543d700 fix APIs, add python API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-23 21:28:11 -07:00
Nikolaj Bjorner
99b4ce037d integrating diff opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-05 16:29:26 -08:00
Nikolaj Bjorner
363af825c0 working on stand-alone simplex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-26 20:25:36 -08:00
Nikolaj Bjorner
c14c65465a working on stand-alone simplex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-26 19:46:42 -08:00
Nikolaj Bjorner
32762b54a7 debug looping behavior 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-27 07:50:25 -08:00
Nikolaj Bjorner
58f8181a74 fixes to dotnet interface 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-26 17:14:29 -08:00
Nikolaj Bjorner
0d6220f383 revert is_all_int bugfix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-18 21:53:04 +02:00
Nikolaj Bjorner
cff0e0fc6c debug min_max 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-18 09:18:06 +02:00
Nikolaj Bjorner
392b419367 debug min_max 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-18 09:14:10 +02:00
Nikolaj Bjorner
eb1b578bfb fixing optimizaiton bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-18 08:43:07 +02:00
Nikolaj Bjorner
909408d6ef fix is_all_int bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-15 10:58:23 +02:00
Nikolaj Bjorner
ddd0bf875d fix bugs in optimization for integers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-15 08:46:24 +02:00
Nikolaj Bjorner
8c85ee6b7c fixing lex optimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-13 23:36:42 +01:00
Nikolaj Bjorner
56562a725d fixing bugs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-11 19:24:20 -06:00
Nikolaj Bjorner
eacb48268c fixing bugs exposed by msf unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-11 19:02:36 -06:00
Anh-Dung Phan
1c0442ea31 Workaround for theory vars without unassigned atoms 2013-12-11 11:49:40 -08:00
Nikolaj Bjorner
da348fe1c0 first pass on normalization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-07 14:38:09 -08:00
Nikolaj Bjorner
a617eac010 enable bounding for various domains 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-06 19:36:12 -08:00
Anh-Dung Phan
87a2b99091 Clean up 2013-11-25 12:16:34 -08:00