mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-17 06:15:37 +00:00
Code Activity
1644 commits 23 branches 48 tags 157 MiB
Commit graph

1644 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 22166d0760 remove print 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-18 05:59:16 +02:00
Nikolaj Bjorner 72130ac7b9 fix lower bound update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-18 05:49:43 +02:00
Nikolaj Bjorner 02f74f1028 trying Cezary's example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-17 05:03:20 +02:00
Nikolaj Bjorner 56b9c4c8a2 fix bugs reported by phan 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-17 04:20:24 +02:00
Nikolaj Bjorner 1bcf5b8b5f remove auxiliary variables from weighted maxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-16 11:42:28 +02:00
Nikolaj Bjorner 1ca44ed316 handle proof-wrapper justifications 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-16 11:25:50 +02:00
Nikolaj Bjorner e38729a1c6 redo marking mechanism as marked literals can disappear from lemma 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-16 07:50:24 +02:00
Nikolaj Bjorner b1caadee49 disabling skip steps to avoid bogus behavior 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-16 05:24:05 +02:00
Nikolaj Bjorner 15b64261dd fix wmaxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-16 04:55:56 +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 b764c7bbee fixes to bugs exposed by regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-15 05:25:47 +02:00
Nikolaj Bjorner fe5c42c90f fixes to bugs exposed by regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-15 05:23:47 +02:00
Nikolaj Bjorner 50f18a77af disable 'optimization' that led to wrong model' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-15 02:40:52 +02:00
Nikolaj Bjorner ac893e907f fixes to maxsmt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-14 16:06:03 +02:00
Nikolaj Bjorner 5f72325e99 working on maxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-14 10:00:21 +02:00
Nikolaj Bjorner 04824d86df fixes to model generation of weighted maxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-14 09:37:42 +02:00
Nikolaj Bjorner 5225ea18b7 fix lower/upper bound updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-14 09:04:48 +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 df5c2adc4e debug opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-12 15:39:38 -06:00
Nikolaj Bjorner f41d23bc0f debugging model generation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-12 12:18:34 -06: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 a737639790 Skip lower bound assertions for unbounded objectives 2013-12-11 12:56:48 -08:00
Anh-Dung Phan 1c0442ea31 Workaround for theory vars without unassigned atoms 2013-12-11 11:49:40 -08:00
Anh-Dung Phan caba15d6b3 Remove superfluouse indices to make .NET API thinner 2013-12-10 17:15:51 -08:00
Anh-Dung Phan 34c96a8fe0 Simple guard in order to not get model before setting solver 2013-12-10 17:10:23 -08:00
Nikolaj Bjorner 2c577a304d bug fixes to pb; working on model extraction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-10 15:16:58 -08:00
Nikolaj Bjorner 26bf64a0c3 debug pb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-09 19:58:34 -08:00
Nikolaj Bjorner fbf834f4c4 debugging pb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-09 15:48:58 -08:00
Nikolaj Bjorner d1e86f1d42 adding validation code for assignment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-09 15:48:15 -08:00
Nikolaj Bjorner ec84d69206 investigating conflict resolution bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-08 21:40:53 -08:00
Nikolaj Bjorner 0f0397b05f hunt bugs exposed by so.smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-08 18:58:48 -08:00
Nikolaj Bjorner 97b2fc9ee7 fix bugs exposed by testSolver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-08 18:34:28 -08:00
Nikolaj Bjorner 5566965a5a fix bug exposed from relevancy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-08 18:19:10 -08:00
Nikolaj Bjorner f0ef339623 fix bug exposed by lia2maxsmt4 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-08 12:30:52 -08:00
Nikolaj Bjorner ddb30c51b5 debugging lia2maxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-08 12:17:33 -08:00
Nikolaj Bjorner 370a4b66de update lower bounds from feasible solutiosn 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-07 22:09:57 -08:00
Nikolaj Bjorner e307c5fdda fix minimize->maxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-07 14:47:47 -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 6300d82224 fix release build break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-07 08:07:02 -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
Nikolaj Bjorner 437a545c3b fix pretty printer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-06 13:12:35 -08:00
Nikolaj Bjorner 4d6aa1a0f3 add to_string and get_help methods to optimize API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-06 11:34:41 -08:00
Nikolaj Bjorner 7884b2ab31 make lia2card general purpose functions visible 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-06 11:00:49 -08:00
Anh-Dung Phan d38e2b9b78 Expose objective indices to .NET API 2013-12-05 17:30:40 -08:00
Nikolaj Bjorner 5fc429c501 debugging network simplex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-05 16:31:29 -08:00
Nikolaj Bjorner 192ce11ca6 change model binding time 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-05 11:42:04 -08:00
Nikolaj Bjorner 56c4fa8f6d expose models, working on network flow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-04 17:39:54 -08:00
Nikolaj Bjorner 686d146cc6 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2013-12-04 14:38:24 -08:00
Nikolaj Bjorner a1a8aad09b start working on network flow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-04 14:38:03 -08:00