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