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 |
|
Nikolaj Bjorner
|
89989627d0
|
add blast method for ite terms
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-11-04 13:33:02 -08:00 |
|
Leonardo de Moura
|
063f6fe15f
|
fix assertion violations (reported by Christoph Wintersteiger) at sage\app8\bench_2174.smt2, sage\app9\bench_1450.smt2, sage\app9\bench_1546.smt2
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-11-04 12:26:20 -08:00 |
|
Leonardo de Moura
|
88675ec728
|
fix assertion violations (reported by Christoph Wintersteiger) at sage/bench_1300.smt2 and sage/bench/2861.smt2
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-11-04 12:24:25 -08:00 |
|
Leonardo de Moura
|
825b72719c
|
fix https://z3.codeplex.com/workitem/62
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-11-04 11:57:29 -08:00 |
|
Leonardo de Moura
|
8b10e13251
|
fix bug in factor_tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-11-04 11:02:53 -08:00 |
|