mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-27 21:48:56 +00:00
Code Activity
1634 commits 64 branches 52 tags 178 MiB
Commit graph

280 commits

Author SHA1 Message Date
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
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
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
5566965a5a fix bug exposed from relevancy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-08 18:19:10 -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
5fc429c501 debugging network simplex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-05 16:31:29 -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
Nikolaj Bjorner
ead414c4ee add back skipped consequences, exposed by fu-malik assertion violation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-04 13:11:58 -08:00
Nikolaj Bjorner
d6f0c13f2a bug fixes exposed from regression tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-04 08:35:46 -08:00
Nikolaj Bjorner
8fa0d6e4f3 bug fixes exposed from regression tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-04 08:35:27 -08:00
Nikolaj Bjorner
b9d433e3e5 fix bug in conflict resoltion tracking decision variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-03 21:10:54 -08:00
Nikolaj Bjorner
af5d989d6c change verbosity level 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-02 21:51:20 -08:00
Nikolaj Bjorner
faa59ba7f9 debugging multi-objective interface and pb revisions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-02 14:14:44 -08:00
Nikolaj Bjorner
a016caa5d8 add expression conversion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-02 09:47:59 -08:00
Anh-Dung Phan
5ed8a48ac2 Add push/pop to box optimization 2013-11-26 14:16:59 -08:00
Anh-Dung Phan
87a2b99091 Clean up 2013-11-25 12:16:34 -08:00
Anh-Dung Phan
8fe50ff2d9 Display diff logic optimization and min cost flow in smt2 format 2013-11-25 02:15:21 +01:00
Anh-Dung Phan
fff3a1aae5 Normalize diff logic's optimal assignments 2013-11-25 00:30:15 +01:00
Anh-Dung Phan
cc3d65e544 Add facilities to get optimal assignments 2013-11-24 22:31:52 +01:00
Nikolaj Bjorner
2ff51e9a60 move model_evaluator from pdr to model, call it model_implicant 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-23 21:33:35 +01:00
Anh-Dung Phan
b35088f7e5 Update diff logic optimization 2013-11-22 18:15:34 -08:00
Anh-Dung Phan
37f5628824 Update basic spanning tree to be on par with threaded one 2013-11-22 13:44:12 -08:00
Anh-Dung Phan
7bc7a61a40 Debug undirected dfs and bfs 2013-11-22 08:58:17 +01:00
Anh-Dung Phan
3b2dd47cd4 Refactor pivot rules 2013-11-21 19:05:17 -08:00
Nikolaj Bjorner
97dfb6d521 moving to rational coefficients 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-21 15:55:08 -08:00
Nikolaj Bjorner
e44db06bb7 update conflict resolution 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-20 16:14:29 -08:00
Nikolaj Bjorner
33895d522b fix and enable learning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-19 20:47:16 -08:00
Nikolaj Bjorner
696db3a6a4 debug conflict 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-19 17:25:19 -08:00
Nikolaj Bjorner
96921355cc pb solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-19 00:54:30 -08:00
Nikolaj Bjorner
1a8ff9cea4 working on pb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-18 22:41:06 -08:00
Nikolaj Bjorner
efecb9b6c0 working on pb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-18 21:51:56 -08:00
Nikolaj Bjorner
475072f5da remove theory_card 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-18 21:27:36 -08:00
Nikolaj Bjorner
0ff1b63307 remove theory_card 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-18 21:26:23 -08:00
Nikolaj Bjorner
ee0abfbfe9 rename card->pb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-18 21:25:02 -08:00
Nikolaj Bjorner
2b2d0e155c debugged new pb solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-18 18:03:49 -08:00
Nikolaj Bjorner
86e22c1186 add validation option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-18 09:44:20 -08:00
Nikolaj Bjorner
c42f0d60e6 pb solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-18 05:10:30 -08:00