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

4351 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
e5698119d7 debugging infinite upper bound checking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-01 17:27:24 -07:00
Nikolaj Bjorner
b35ed169b1 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2013-11-01 17:26:48 -07:00
Nikolaj Bjorner
3c6f0c737a debugging infinite upper bound checking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-01 17:26:27 -07:00
Ken McMillan
7ca6c744fd added binary interpolation 2013-11-01 15:58:59 -07:00
Anh-Dung Phan
926f2e0834 Add more object invariants 2013-11-01 14:50:17 -07:00
Nikolaj Bjorner
2a907ea52a fix objective value regression in simplex maximation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-01 12:45:26 -07:00
Ken McMillan
ac212ec54c fixing interpolation bugs 2013-11-01 11:03:55 -07:00
Anh-Dung Phan
736d43c084 Block lower bound of difference logic objectives 2013-11-01 08:05:29 +01:00
Nikolaj Bjorner
87141f4cb3 fix bugs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-31 22:09:52 -07:00
Nikolaj Bjorner
6ca0c7c6c7 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2013-10-31 21:32:18 -07:00
Nikolaj Bjorner
6baa469073 local updates to opt_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-31 21:32:11 -07:00
Nikolaj Bjorner
ae3a69b32e Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2013-10-31 18:51:28 -07:00
Anh-Dung Phan
195df69a1b Use optional<_> for infinite check 2013-10-31 18:34:40 -07:00
Nikolaj Bjorner
cfac32c57d add outline of object invariant 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-31 17:21:10 -07:00
Anh-Dung Phan
a66a14dbf0 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2013-10-31 16:41:42 -07:00
Anh-Dung Phan
29622229cb Add lower bound case for edge_state 2013-10-31 13:03:24 -07:00
Anh-Dung Phan
1a32a64b96 Use constraint graphs for minimum cost flow correctly 2013-10-31 12:11:56 -07:00
Nikolaj Bjorner
72e82532b2 enabling upper bound test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-31 09:43:15 -07:00
Nikolaj Bjorner
637b63cbe1 preparing for inf extension of arithmetic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-31 02:15:08 -07:00
Nikolaj Bjorner
5106c74b3e preparing for inf extension of arithmetic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-31 02:13:24 -07:00
Nikolaj Bjorner
0b65aa83e8 preparing for inf extension of arithmetic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-31 02:02:37 -07:00
Nikolaj Bjorner
acc7aa1636 use iterative weighted algorithm 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-31 00:57:36 -07:00
Anh-Dung Phan
a3a7af84c5 Minor updates 2013-10-30 18:25:39 -07:00
Anh-Dung Phan
3a3f93c4a5 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2013-10-30 16:52:52 -07:00
Anh-Dung Phan
01c3dd779b Add visualization of spanning trees 2013-10-30 16:52:37 -07:00
Nikolaj Bjorner
86151b4d52 dealing with cancel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-30 13:38:47 -07:00
Nikolaj Bjorner
946b888b32 adding timeout, parameters, statistics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-30 13:24:21 -07:00
Nikolaj Bjorner
9fc84f1389 adding timeout, parameters, statistics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-30 13:23:04 -07:00
Anh-Dung Phan
49aba844b8 Refactor network_flow 
Use a template method for pretty printing
 2013-10-30 10:04:56 -07:00
Nikolaj Bjorner
42cbbe830e working on wmaxsmt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-30 01:28:50 -07:00
Nikolaj Bjorner
6302d1b7db wmax nits 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-30 01:18:10 -07:00
Anh-Dung Phan
a6e103dd36 Make a few variables private 2013-10-30 06:30:51 +01:00
Nikolaj Bjorner
f5e6a18015 working on wmaxsmt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-29 21:16:02 -07:00
Nikolaj Bjorner
bc44bcad10 push blocking code to optimizer context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-29 20:26:54 -07:00
Anh-Dung Phan
b0fddd8e60 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2013-10-29 18:33:06 -07:00
Anh-Dung Phan
b67d333cf9 First complete version of Network Simplex 2013-10-29 18:32:10 -07:00
Nikolaj Bjorner
5170cbbd7e Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2013-10-29 17:40:50 -07:00
Nikolaj Bjorner
96562962fa working on wmaxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-29 17:40:37 -07:00
Anh-Dung Phan
e715ccbc98 Minor updates 2013-10-29 15:49:53 -07:00
Anh-Dung Phan
905f230b8f Add pretty printing for network_flow 
Reuse the original graph as much as possible
 2013-10-29 14:20:29 -07:00
Nikolaj Bjorner
1878d64b02 working on weighted maxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-28 21:32:41 -07:00
Nikolaj Bjorner
d30f183476 working on weighted maxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-28 21:30:57 -07:00
Anh-Dung Phan
906bbb4eeb Update Network Simplex implementation 2013-10-28 18:29:14 -07:00
Nikolaj Bjorner
d78d22deb6 working on weighted max smt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-28 17:13:23 -07:00
Nikolaj Bjorner
72c3473400 cleanup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-26 20:48:19 +08:00
Nikolaj Bjorner
9903c722af adding review notes to code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-26 16:24:21 +08:00
Nikolaj Bjorner
3852b3a753 working on internalizer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-26 15:03:39 +08:00
Anh-Dung Phan
3d943bf70d Fix a mistake in previous commit causing imcompilable code 
Also correct my alias
 2013-10-26 05:22:52 +02:00
Ken McMillan
81df4932fb added quantifiers in new interpolation 2013-10-25 18:40:26 -07:00
Anh-Dung Phan
532c345fd1 Reduce difference logic solver to min cost flow 2013-10-25 17:42:03 -07:00