1 
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4 
5 --*/
6 
7 using System;
8 using System.Collections.Generic;
9 using System.Linq;
10 using System.Text;
11 
12 using Microsoft.SolverFoundation.Common;
13 using Microsoft.SolverFoundation.Solvers;
14 using Microsoft.SolverFoundation.Services;
15 using Microsoft.SolverFoundation.Plugin.Z3;
16 using Microsoft.VisualStudio.TestTools.UnitTesting;
17 
18 namespace Microsoft.SolverFoundation.Plugin.Z3.Tests
19 {
20     [TestClass]
21     public class SolverTests
22     {
23         [TestMethod]
TestMILPSolver1()24         public void TestMILPSolver1()
25         {
26             var solver = new Z3MILPSolver();
27             int goal;
28 
29             solver.AddRow("goal", out goal);
30             int x1, x2, z;
31 
32             // 0 <= x1 <= 2
33             solver.AddVariable("x1", out x1);
34             solver.SetBounds(x1, 0, 2);
35 
36             // 0 <= x2 <= 2
37             solver.AddVariable("x2", out x2);
38             solver.SetBounds(x2, 0, 2);
39 
40             // z is an integer in [0,1]
41             solver.AddVariable("z", out z);
42             solver.SetIntegrality(z, true);
43             solver.SetBounds(z, 0, 1);
44 
45             //max x1 + x2
46             solver.SetCoefficient(goal, x1, 1);
47             solver.SetCoefficient(goal, x2, 1);
48             solver.AddGoal(goal, 1, false);
49 
50             // 0 <= x1 -z <= 1
51             int row1;
52             solver.AddRow("rowI1", out row1);
53             solver.SetBounds(row1, 0, 1);
54             solver.SetCoefficient(row1, x1, 1);
55             solver.SetCoefficient(row1, z, -1);
56 
57             // 0 <= x2 + z <= 2
58             int row2;
59             solver.AddRow("rowI2", out row2);
60             solver.SetBounds(row2, 0, 2);
61             solver.SetCoefficient(row2, x2, 1);
62             solver.SetCoefficient(row2, z, 1);
63 
64             var p = new Z3MILPParams();
65             solver.Solve(p);
66 
67             Assert.IsTrue(solver.Result == LinearResult.Optimal);
68             Assert.AreEqual(solver.GetValue(x1), 2 * Rational.One);
69             Assert.AreEqual(solver.GetValue(x2), Rational.One);
70             Assert.AreEqual(solver.GetValue(z), Rational.One);
71             Assert.AreEqual(solver.GetValue(goal), 3 * Rational.One);
72         }
73 
74         [TestMethod]
TestMILPSolver2()75         public void TestMILPSolver2()
76         {
77             var solver = new Z3MILPSolver();
78             int goal, extraGoal;
79 
80             Rational M = 100;
81             solver.AddRow("goal", out goal);
82             int x1, x2, z;
83 
84             // 0 <= x1 <= 100
85             solver.AddVariable("x1", out x1);
86             solver.SetBounds(x1, 0, M);
87 
88             // 0 <= x2 <= 100
89             solver.AddVariable("x2", out x2);
90             solver.SetBounds(x2, 0, M);
91 
92             // z is an integer in [0,1]
93             solver.AddVariable("z", out z);
94             solver.SetIntegrality(z, true);
95             solver.SetBounds(z, 0, 1);
96 
97             solver.SetCoefficient(goal, x1, 1);
98             solver.SetCoefficient(goal, x2, 2);
99             solver.AddGoal(goal, 1, false);
100 
101             solver.AddRow("extraGoal", out extraGoal);
102 
103             solver.SetCoefficient(extraGoal, x1, 2);
104             solver.SetCoefficient(extraGoal, x2, 1);
105             solver.AddGoal(extraGoal, 2, false);
106 
107             // x1 + x2 >= 1
108             int row;
109             solver.AddRow("row", out row);
110             solver.SetBounds(row, 1, Rational.PositiveInfinity);
111             solver.SetCoefficient(row, x1, 1);
112             solver.SetCoefficient(row, x2, 1);
113 
114 
115             // x1 - M*z <= 0
116             int row1;
117             solver.AddRow("rowI1", out row1);
118             solver.SetBounds(row1, Rational.NegativeInfinity, 0);
119             solver.SetCoefficient(row1, x1, 1);
120             solver.SetCoefficient(row1, z, -M);
121 
122             // x2 - M* (1-z) <= 0
123             int row2;
124             solver.AddRow("rowI2", out row2);
125             solver.SetBounds(row2, Rational.NegativeInfinity, M);
126             solver.SetCoefficient(row2, x2, 1);
127             solver.SetCoefficient(row2, z, M);
128 
129             var p = new Z3MILPParams();
130             p.OptKind = OptimizationKind.BoundingBox;
131 
132             solver.Solve(p);
133             Assert.IsTrue(solver.Result == LinearResult.Optimal);
134             Assert.AreEqual(solver.GetValue(goal), 200 * Rational.One);
135             Assert.AreEqual(solver.GetValue(extraGoal), 200 * Rational.One);
136         }
137     }
138 }
139