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 ServiceTests 22 { 23 [TestInitialize] SetUp()24 public void SetUp() 25 { 26 SolverContext context = SolverContext.GetContext(); 27 context.ClearModel(); 28 } 29 TestService1(Directive directive)30 private void TestService1(Directive directive) 31 { 32 SolverContext context = SolverContext.GetContext(); 33 Model model = context.CreateModel(); 34 35 Decision x1 = new Decision(Domain.RealRange(0, 2), "x1"); 36 Decision x2 = new Decision(Domain.RealRange(0, 2), "x2"); 37 38 Decision z = new Decision(Domain.IntegerRange(0, 1), "z"); 39 40 model.AddDecisions(x1, x2, z); 41 42 model.AddConstraint("Row0", x1 - z <= 1); 43 model.AddConstraint("Row1", x2 + z <= 2); 44 45 Goal goal = model.AddGoal("Goal0", GoalKind.Maximize, x1 + x2); 46 47 Solution solution = context.Solve(directive); 48 Assert.IsTrue(goal.ToInt32() == 3); 49 context.ClearModel(); 50 } 51 TestService2(Directive directive)52 private void TestService2(Directive directive) 53 { 54 SolverContext context = SolverContext.GetContext(); 55 Model model = context.CreateModel(); 56 57 Decision x1 = new Decision(Domain.RealNonnegative, "x1"); 58 Decision x2 = new Decision(Domain.RealNonnegative, "x2"); 59 60 Decision z = new Decision(Domain.IntegerRange(0, 1), "z"); 61 62 Rational M = 100; 63 64 model.AddDecisions(x1, x2, z); 65 66 model.AddConstraint("Row0", x1 + x2 >= 1); 67 model.AddConstraint("Row1", x1 - z * 100 <= 0); 68 model.AddConstraint("Row2", x2 + z * 100 <= 100); 69 70 Goal goal = model.AddGoal("Goal0", GoalKind.Maximize, x1 + x2); 71 72 Solution solution = context.Solve(directive); 73 Assert.IsTrue(goal.ToInt32() == 100); 74 context.ClearModel(); 75 } 76 77 [TestMethod] TestService1()78 public void TestService1() 79 { 80 TestService1(new Z3MILPDirective()); 81 TestService1(new Z3TermDirective()); 82 } 83 84 [TestMethod] TestService2()85 public void TestService2() 86 { 87 TestService2(new Z3MILPDirective()); 88 TestService2(new Z3TermDirective()); 89 } 90 91 } 92 } 93