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