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

4211 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
c6c7093a4c make max-smt solvers generic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-08 18:22:07 -08:00
Anh-Dung Phan
5a27c035e4 Add a vector of edges to handle spanning trees 2013-11-08 18:00:48 -08:00
Nikolaj Bjorner
9f53a4aa18 working on supporting multiple max-sat objectives 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-08 16:54:34 -08:00
Ken McMillan
0cc5c169a4 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-11-08 16:28:27 -08:00
Ken McMillan
749f95c9d7 handle eq-propagate arithetic rule 2013-11-08 16:18:48 -08:00
Nikolaj Bjorner
f350efffc7 working on pareto and upper/lower bound facilities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-08 13:52:27 -08:00
Nikolaj Bjorner
6caee5e3ca more refactoring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-08 13:16:10 -08:00
Nikolaj Bjorner
29cc9025cb renaming to optsmt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-08 12:41:05 -08:00
Christoph M. Wintersteiger
86f39cd4c1 Changed references to _DEBUG to Z3DEBUG. 
(gcc does not define _DEBUG for debug builds.)

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-11-08 19:21:55 +00:00
Nikolaj Bjorner
33be06c6dc continued re-factoring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-08 09:00:24 -08:00
Nikolaj Bjorner
acbeed2e97 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2013-11-07 18:09:58 -08:00
Nikolaj Bjorner
401fced400 separate out file for objectives 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-07 18:09:44 -08:00
Ken McMillan
763ae0d246 removed debugginf message in interpolation 2013-11-07 17:42:18 -08:00
Ken McMillan
a898bad961 fixed two interpolation bugs 2013-11-07 17:38:39 -08:00
Ken McMillan
b076c152b3 adding farkas axiom to interpolation 2013-11-07 16:17:56 -08:00
Anh-Dung Phan
ab4efe2da0 Update interface of network flows 2013-11-07 15:56:53 -08:00
Ken McMillan
cf176af48e looking for more farkas rules in interpolation 2013-11-07 15:40:44 -08:00
Ken McMillan
d9c69f5294 handling commutativity rule in interpolation 2013-11-07 15:13:39 -08:00
Nikolaj Bjorner
759d80dfe3 fix regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-07 12:15:51 -08:00
Nikolaj Bjorner
8fb92e6312 tested network sorting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-07 10:49:36 -08:00
Nikolaj Bjorner
c57594d463 tested network sorting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-07 10:47:12 -08:00
Christoph M. Wintersteiger
412f912c46 bugfix for pb2bv 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-11-07 15:06:36 +00:00
Nikolaj Bjorner
31e2d823c9 add cutting plane 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-07 01:35:25 -08:00
Nikolaj Bjorner
220b339e5e add cutting plane 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-07 01:30:19 -08:00
Nikolaj Bjorner
d434cbea41 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2013-11-07 00:53:23 -08:00
Nikolaj Bjorner
3ee8c3efb5 pb/car constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-07 00:53:08 -08:00
Anh-Dung Phan
bc9bfe7f97 Use templates on spanning trees 2013-11-07 07:33:25 +01:00
Anh-Dung Phan
55e91c099f Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2013-11-06 18:34:28 -08:00
Anh-Dung Phan
676e38ad0b Minor updates 2013-11-06 18:34:09 -08:00
Anh-Dung Phan
f7fdf134fd Create a separate class for spanning tree 
Remarks:

1. Templates should be in header files only

2. Should pass in svector<_> instead of returning a local one
 2013-11-06 17:42:09 -08:00
Anh-Dung Phan
034b33b6da Remove m_final from spanning tree representation 2013-11-06 13:30:29 -08:00
Nikolaj Bjorner
05b37b2f07 working on cardinality tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-06 12:40:56 -08:00
Nikolaj Bjorner
2f04918c39 working on cardinality tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-06 12:33:09 -08:00
Ken McMillan
33f941aaec interpolation fix 2013-11-06 12:20:55 -08:00
Ken McMillan
0696a7ef50 interpolation fix 2013-11-06 11:41:17 -08:00
Ken McMillan
b008d036dd trying to fix proof mode issue 2013-11-05 17:38:50 -08:00
Nikolaj Bjorner
e84c5e7e90 adding simple sorting network 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-05 16:53:35 -08:00
Nikolaj Bjorner
cf75a7743e network update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-05 16:18:21 -08:00
Nikolaj Bjorner
bd33e466c2 network update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-05 16:10:51 -08:00
Ken McMillan
fa05116e66 fixed vc++ compaibility issues 2013-11-05 14:45:44 -08:00
Ken McMillan
f83bca11a0 added interpolation options 2013-11-05 14:20:22 -08:00
Ken McMillan
9f78c454c9 removed foci instructions 2013-11-05 13:58:44 -08:00
Ken McMillan
d8972d4b17 removed commented-out code 2013-11-05 13:35:37 -08:00
Ken McMillan
a785a5a4b8 Merge branch 'unstable' into interp 2013-11-05 12:28:13 -08:00
Ken McMillan
49c72abb2d new interpolation fixes; re-added fixedpoint-push/pop 2013-11-05 12:17:09 -08:00
Nikolaj Bjorner
9467806a5c debugging cardinality theory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-05 09:39:28 -08:00
Nikolaj Bjorner
27f3f7b735 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2013-11-05 01:30:54 -08:00
Nikolaj Bjorner
2853b322ca sketch cardinality plugin module 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-05 01:30:34 -08:00
Anh-Dung Phan
8b776569e0 Add fix_depth 2013-11-05 07:30:42 +01:00
Nikolaj Bjorner
acb26d0cf9 review of network flow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-04 16:00:50 -08:00