diff --git a/examples/msf/SolverFoundation.Plugin.Z3.Tests/App.config b/examples/msf/SolverFoundation.Plugin.Z3.Tests/App.config new file mode 100644 index 000000000..75e2872f1 --- /dev/null +++ b/examples/msf/SolverFoundation.Plugin.Z3.Tests/App.config @@ -0,0 +1,60 @@ + + + +
+ + + + + + + + + + + + + + + + diff --git a/examples/msf/SolverFoundation.Plugin.Z3.Tests/Properties/AssemblyInfo.cs b/examples/msf/SolverFoundation.Plugin.Z3.Tests/Properties/AssemblyInfo.cs new file mode 100644 index 000000000..b58f97eda --- /dev/null +++ b/examples/msf/SolverFoundation.Plugin.Z3.Tests/Properties/AssemblyInfo.cs @@ -0,0 +1,36 @@ +using System.Reflection; +using System.Runtime.CompilerServices; +using System.Runtime.InteropServices; + +// General Information about an assembly is controlled through the following +// set of attributes. Change these attribute values to modify the information +// associated with an assembly. +[assembly: AssemblyTitle("SolverFoundation.Plugin.Z3.Tests")] +[assembly: AssemblyDescription("")] +[assembly: AssemblyConfiguration("")] +[assembly: AssemblyCompany("")] +[assembly: AssemblyProduct("SolverFoundation.Plugin.Z3.Tests")] +[assembly: AssemblyCopyright("Copyright © 2013")] +[assembly: AssemblyTrademark("")] +[assembly: AssemblyCulture("")] + +// Setting ComVisible to false makes the types in this assembly not visible +// to COM components. If you need to access a type in this assembly from +// COM, set the ComVisible attribute to true on that type. +[assembly: ComVisible(false)] + +// The following GUID is for the ID of the typelib if this project is exposed to COM +[assembly: Guid("27657eee-ca7b-4996-a905-86a3f4584988")] + +// Version information for an assembly consists of the following four values: +// +// Major Version +// Minor Version +// Build Number +// Revision +// +// You can specify all the values or you can default the Build and Revision Numbers +// by using the '*' as shown below: +// [assembly: AssemblyVersion("1.0.*")] +[assembly: AssemblyVersion("1.0.0.0")] +[assembly: AssemblyFileVersion("1.0.0.0")] diff --git a/examples/msf/SolverFoundation.Plugin.Z3.Tests/ServiceTests.cs b/examples/msf/SolverFoundation.Plugin.Z3.Tests/ServiceTests.cs new file mode 100644 index 000000000..25a8e2d26 --- /dev/null +++ b/examples/msf/SolverFoundation.Plugin.Z3.Tests/ServiceTests.cs @@ -0,0 +1,86 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; + +using Microsoft.SolverFoundation.Common; +using Microsoft.SolverFoundation.Solvers; +using Microsoft.SolverFoundation.Services; +using Microsoft.SolverFoundation.Plugin.Z3; +using Microsoft.VisualStudio.TestTools.UnitTesting; + +namespace Microsoft.SolverFoundation.Plugin.Z3.Tests +{ + [TestClass] + public class ServiceTests + { + [TestInitialize] + public void SetUp() + { + SolverContext context = SolverContext.GetContext(); + context.ClearModel(); + } + + private void TestService1(Directive directive) + { + SolverContext context = SolverContext.GetContext(); + Model model = context.CreateModel(); + + Decision x1 = new Decision(Domain.RealRange(0, 2), "x1"); + Decision x2 = new Decision(Domain.RealRange(0, 2), "x2"); + + Decision z = new Decision(Domain.IntegerRange(0, 1), "z"); + + model.AddDecisions(x1, x2, z); + + model.AddConstraint("Row0", x1 - z <= 1); + model.AddConstraint("Row1", x2 + z <= 2); + + Goal goal = model.AddGoal("Goal0", GoalKind.Maximize, x1 + x2); + + Solution solution = context.Solve(directive); + Assert.IsTrue(goal.ToInt32() == 3); + context.ClearModel(); + } + + private void TestService2(Directive directive) + { + SolverContext context = SolverContext.GetContext(); + Model model = context.CreateModel(); + + Decision x1 = new Decision(Domain.RealNonnegative, "x1"); + Decision x2 = new Decision(Domain.RealNonnegative, "x2"); + + Decision z = new Decision(Domain.IntegerRange(0, 1), "z"); + + Rational M = 100; + + model.AddDecisions(x1, x2, z); + + model.AddConstraint("Row0", x1 + x2 >= 1); + model.AddConstraint("Row1", x1 - z * 100 <= 0); + model.AddConstraint("Row2", x2 + z * 100 <= 100); + + Goal goal = model.AddGoal("Goal0", GoalKind.Maximize, x1 + x2); + + Solution solution = context.Solve(directive); + Assert.IsTrue(goal.ToInt32() == 100); + context.ClearModel(); + } + + [TestMethod] + public void TestService1() + { + TestService1(new Z3MILPDirective()); + TestService1(new Z3TermDirective()); + } + + [TestMethod] + public void TestService2() + { + TestService2(new Z3MILPDirective()); + TestService2(new Z3TermDirective()); + } + + } +} diff --git a/examples/msf/SolverFoundation.Plugin.Z3.Tests/SolverFoundation.Plugin.Z3.Tests.csproj b/examples/msf/SolverFoundation.Plugin.Z3.Tests/SolverFoundation.Plugin.Z3.Tests.csproj new file mode 100644 index 000000000..24cecfa10 --- /dev/null +++ b/examples/msf/SolverFoundation.Plugin.Z3.Tests/SolverFoundation.Plugin.Z3.Tests.csproj @@ -0,0 +1,70 @@ + + + + + Debug + AnyCPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B} + Library + Properties + Microsoft.SolverFoundation.Plugin.Z3.Tests + SolverFoundation.Plugin.Z3.Tests + v4.0 + 512 + + + + true + full + false + bin\Debug\ + DEBUG;TRACE + prompt + 4 + x86 + + + pdbonly + true + bin\Release\ + TRACE + prompt + 4 + x86 + + + + ..\Microsoft.Solver.Foundation.dll + + + + + + + + + + + + + + + + + + + + + {7340e664-f648-4ff7-89b2-f4da424996d3} + SolverFoundation.Plugin.Z3 + + + + + \ No newline at end of file diff --git a/examples/msf/SolverFoundation.Plugin.Z3.Tests/SolverTests.cs b/examples/msf/SolverFoundation.Plugin.Z3.Tests/SolverTests.cs new file mode 100644 index 000000000..c2cd0c270 --- /dev/null +++ b/examples/msf/SolverFoundation.Plugin.Z3.Tests/SolverTests.cs @@ -0,0 +1,132 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; + +using Microsoft.SolverFoundation.Common; +using Microsoft.SolverFoundation.Solvers; +using Microsoft.SolverFoundation.Services; +using Microsoft.SolverFoundation.Plugin.Z3; +using Microsoft.VisualStudio.TestTools.UnitTesting; + +namespace Microsoft.SolverFoundation.Plugin.Z3.Tests +{ + [TestClass] + public class SolverTests + { + [TestMethod] + public void TestMILPSolver1() + { + var solver = new Z3MILPSolver(); + int goal; + + solver.AddRow("goal", out goal); + int x1, x2, z; + + // 0 <= x1 <= 2 + solver.AddVariable("x1", out x1); + solver.SetBounds(x1, 0, 2); + + // 0 <= x2 <= 2 + solver.AddVariable("x2", out x2); + solver.SetBounds(x2, 0, 2); + + // z is an integer in [0,1] + solver.AddVariable("z", out z); + solver.SetIntegrality(z, true); + solver.SetBounds(z, 0, 1); + + //max x1 + x2 + solver.SetCoefficient(goal, x1, 1); + solver.SetCoefficient(goal, x2, 1); + solver.AddGoal(goal, 1, false); + + // 0 <= x1 -z <= 1 + int row1; + solver.AddRow("rowI1", out row1); + solver.SetBounds(row1, 0, 1); + solver.SetCoefficient(row1, x1, 1); + solver.SetCoefficient(row1, z, -1); + + // 0 <= x2 + z <= 2 + int row2; + solver.AddRow("rowI2", out row2); + solver.SetBounds(row2, 0, 2); + solver.SetCoefficient(row2, x2, 1); + solver.SetCoefficient(row2, z, 1); + + var p = new Z3MILPParams(); + solver.Solve(p); + + Assert.IsTrue(solver.Result == LinearResult.Optimal); + Assert.AreEqual(solver.GetValue(x1), 2 * Rational.One); + Assert.AreEqual(solver.GetValue(x2), Rational.One); + Assert.AreEqual(solver.GetValue(z), Rational.One); + Assert.AreEqual(solver.GetValue(goal), 3 * Rational.One); + } + + [TestMethod] + public void TestMILPSolver2() + { + var solver = new Z3MILPSolver(); + int goal, extraGoal; + + Rational M = 100; + solver.AddRow("goal", out goal); + int x1, x2, z; + + // 0 <= x1 <= 100 + solver.AddVariable("x1", out x1); + solver.SetBounds(x1, 0, M); + + // 0 <= x2 <= 100 + solver.AddVariable("x2", out x2); + solver.SetBounds(x2, 0, M); + + // z is an integer in [0,1] + solver.AddVariable("z", out z); + solver.SetIntegrality(z, true); + solver.SetBounds(z, 0, 1); + + solver.SetCoefficient(goal, x1, 1); + solver.SetCoefficient(goal, x2, 2); + solver.AddGoal(goal, 1, false); + + solver.AddRow("extraGoal", out extraGoal); + + solver.SetCoefficient(extraGoal, x1, 2); + solver.SetCoefficient(extraGoal, x2, 1); + solver.AddGoal(extraGoal, 2, false); + + // x1 + x2 >= 1 + int row; + solver.AddRow("row", out row); + solver.SetBounds(row, 1, Rational.PositiveInfinity); + solver.SetCoefficient(row, x1, 1); + solver.SetCoefficient(row, x2, 1); + + + // x1 - M*z <= 0 + int row1; + solver.AddRow("rowI1", out row1); + solver.SetBounds(row1, Rational.NegativeInfinity, 0); + solver.SetCoefficient(row1, x1, 1); + solver.SetCoefficient(row1, z, -M); + + // x2 - M* (1-z) <= 0 + int row2; + solver.AddRow("rowI2", out row2); + solver.SetBounds(row2, Rational.NegativeInfinity, M); + solver.SetCoefficient(row2, x2, 1); + solver.SetCoefficient(row2, z, M); + + var p = new Z3MILPParams(); + p.OptKind = OptimizationKind.BoundingBox; + + solver.Solve(p); + Assert.IsTrue(solver.Result == LinearResult.Optimal); + Assert.AreEqual(solver.GetValue(goal), 200 * Rational.One); + Assert.AreEqual(solver.GetValue(extraGoal), 200 * Rational.One); + } + } +} diff --git a/examples/msf/SolverFoundation.Plugin.Z3/AbortWorker.cs b/examples/msf/SolverFoundation.Plugin.Z3/AbortWorker.cs new file mode 100644 index 000000000..99d6fe17a --- /dev/null +++ b/examples/msf/SolverFoundation.Plugin.Z3/AbortWorker.cs @@ -0,0 +1,92 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using System.Threading; +using Microsoft.Z3; + +namespace Microsoft.SolverFoundation.Plugin.Z3 +{ + /// + /// Thread that will wait until the query abort function returns true or + /// the stop method is called. If the abort function returns true at some + /// point it will issue a softCancel() call to Z3. + /// + internal class AbortWorker + { + #region Private Members + + /// The Z3 solver + private Microsoft.Z3.Context _context; + /// The abort function to use to check if we are aborted + private Func _QueryAbortFunction; + /// Flag indicating that worker should stop + private bool _stop = false; + /// Flag indicating that we have been sent an abort signal + private bool _aborted = false; + + #endregion Private Members + + #region Construction + + /// + /// Worker constructor taking a Z3 instance and a function to periodically + /// check for aborts. + /// + /// Z3 instance + /// method to call to check for aborts + public AbortWorker(Context context, Func queryAbortFunction) + { + _context = context; + _QueryAbortFunction = queryAbortFunction; + } + + #endregion Construction + + #region Public Methods + + /// + /// Stop the abort worker. + /// + public void Stop() + { + _stop = true; + } + + /// + /// Is true if we have been aborted. + /// + public bool Aborted + { + get + { + return _aborted; + } + } + + /// + /// Starts the abort worker. The worker checks the abort method + /// periodically until either it is stopped by a call to the Stop() + /// method or it gets an abort signal. In the latter case it will + /// issue a soft abort signal to Z3. + /// + public void Start() + { + // We go until someone stops us + _stop = false; + while (!_stop && !_QueryAbortFunction()) + { + // Wait for a while + Thread.Sleep(10); + } + // If we were stopped on abort, cancel z3 + if (!_stop) + { + _context.Interrupt(); + _aborted = true; + } + } + + #endregion Public Methods + } +} diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Properties/AssemblyInfo.cs b/examples/msf/SolverFoundation.Plugin.Z3/Properties/AssemblyInfo.cs new file mode 100644 index 000000000..b30c01ab4 --- /dev/null +++ b/examples/msf/SolverFoundation.Plugin.Z3/Properties/AssemblyInfo.cs @@ -0,0 +1,36 @@ +using System.Reflection; +using System.Runtime.CompilerServices; +using System.Runtime.InteropServices; + +// General Information about an assembly is controlled through the following +// set of attributes. Change these attribute values to modify the information +// associated with an assembly. +[assembly: AssemblyTitle("SolverFoundation.Plugin.Z3")] +[assembly: AssemblyDescription("")] +[assembly: AssemblyConfiguration("")] +[assembly: AssemblyCompany("Microsoft")] +[assembly: AssemblyProduct("SolverFoundation.Plugin.Z3")] +[assembly: AssemblyCopyright("Copyright © Microsoft 2013")] +[assembly: AssemblyTrademark("")] +[assembly: AssemblyCulture("")] + +// Setting ComVisible to false makes the types in this assembly not visible +// to COM components. If you need to access a type in this assembly from +// COM, set the ComVisible attribute to true on that type. +[assembly: ComVisible(false)] + +// The following GUID is for the ID of the typelib if this project is exposed to COM +[assembly: Guid("ed1476c0-96de-4d2c-983d-3888b140c3ad")] + +// Version information for an assembly consists of the following four values: +// +// Major Version +// Minor Version +// Build Number +// Revision +// +// You can specify all the values or you can default the Build and Revision Numbers +// by using the '*' as shown below: +// [assembly: AssemblyVersion("1.0.*")] +[assembly: AssemblyVersion("1.0.0.0")] +[assembly: AssemblyFileVersion("1.0.0.0")] diff --git a/examples/msf/SolverFoundation.Plugin.Z3/SolverFoundation.Plugin.Z3.csproj b/examples/msf/SolverFoundation.Plugin.Z3/SolverFoundation.Plugin.Z3.csproj new file mode 100644 index 000000000..6a4a22aec --- /dev/null +++ b/examples/msf/SolverFoundation.Plugin.Z3/SolverFoundation.Plugin.Z3.csproj @@ -0,0 +1,185 @@ + + + + Debug + AnyCPU + 9.0.30729 + 2.0 + {7340E664-F648-4FF7-89B2-F4DA424996D3} + Library + Properties + Microsoft.SolverFoundation.Plugin.Z3 + SolverFoundation.Plugin.Z3 + v4.0 + 512 + false + + + + + 3.5 + + publish\ + true + Disk + false + Foreground + 7 + Days + false + false + true + 0 + 1.0.0.%2a + false + false + true + + + + true + full + false + bin\Debug\ + DEBUG;TRACE + prompt + 4 + AllRules.ruleset + + + pdbonly + true + bin\Release\ + TRACE + prompt + 4 + AllRules.ruleset + + + bin\commercial\ + TRACE + true + pdbonly + AnyCPU + bin\Release\Z3Solver.dll.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + AllRules.ruleset + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + + + bin\commercial_64\ + TRACE + true + pdbonly + AnyCPU + bin\Release\Z3Solver.dll.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + AllRules.ruleset + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + false + false + + + true + bin\x86\Debug\ + DEBUG;TRACE + full + x86 + prompt + AllRules.ruleset + + + bin\x86\Release\ + TRACE + true + pdbonly + x86 + prompt + AllRules.ruleset + + + bin\x86\commercial\ + TRACE + true + pdbonly + x86 + prompt + AllRules.ruleset + + + bin\x86\commercial_64\ + TRACE + true + pdbonly + x86 + prompt + AllRules.ruleset + false + + + + ..\Microsoft.Solver.Foundation.dll + + + ..\Microsoft.Z3.dll + + + + 3.5 + + + + 3.5 + + + 3.5 + + + + + + + + + + + + + + + + + + + + + False + .NET Framework 3.5 SP1 Client Profile + false + + + False + .NET Framework 3.5 SP1 + true + + + False + Windows Installer 3.1 + true + + + + + \ No newline at end of file diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Utils.cs b/examples/msf/SolverFoundation.Plugin.Z3/Utils.cs new file mode 100644 index 000000000..71c8647a1 --- /dev/null +++ b/examples/msf/SolverFoundation.Plugin.Z3/Utils.cs @@ -0,0 +1,124 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using System.Diagnostics; +using Microsoft.Z3; +using Microsoft.SolverFoundation.Common; + +namespace Microsoft.SolverFoundation.Plugin.Z3 +{ + public class Utils + { + /// + /// Returns the Z3 term corresponding to the MSF rational number. + /// + /// The MSF rational + /// The Z3 term + public static ArithExpr GetNumeral(Context context, Rational rational, Sort sort = null) + { + try + { + sort = rational.IsInteger() ? ((Sort)context.IntSort) : (sort == null ? (Sort)context.RealSort : sort); + return (ArithExpr)context.MkNumeral(rational.ToString(), sort); + } + catch (Z3Exception e) + { + Console.Error.WriteLine("Conversion of {0} failed:\n {1}", rational, e); + throw new NotSupportedException(); + } + } + + private static long BASE = 10 ^ 18; + + private static Rational ToRational(System.Numerics.BigInteger bi) + { + if (System.Numerics.BigInteger.Abs(bi) <= BASE) + { + return (Rational)((long)bi); + } + return BASE * ToRational(bi / BASE) + ToRational(bi % BASE); + } + + public static Rational ToRational(IntNum i) + { + return ToRational(i.BigInteger); + } + + public static Rational ToRational(RatNum r) + { + return ToRational(r.BigIntNumerator) / ToRational(r.BigIntDenominator); + } + + public static Rational ToRational(Expr expr) + { + Debug.Assert(expr is ArithExpr, "Only accept ArithExpr for now."); + var e = expr as ArithExpr; + + if (e is IntNum) + { + Debug.Assert(expr.IsIntNum, "Number should be an integer."); + return ToRational(expr as IntNum); + } + + if (e is RatNum) + { + Debug.Assert(expr.IsRatNum, "Number should be a rational."); + return ToRational(expr as RatNum); + } + + if (e.IsAdd) + { + Rational r = Rational.Zero; + foreach (var arg in e.Args) + { + r += ToRational(arg); + } + return r; + } + + if (e.IsMul) + { + Rational r = Rational.One; + foreach (var arg in e.Args) + { + r *= ToRational(arg); + } + return r; + } + + if (e.IsUMinus) + { + return -ToRational(e.Args[0]); + } + + if (e.IsDiv) + { + return ToRational(e.Args[0]) / ToRational(e.Args[1]); + } + + if (e.IsSub) + { + Rational r = ToRational(e.Args[0]); + for (int i = 1; i < e.Args.Length; ++i) + { + r -= ToRational(e.Args[i]); + } + return r; + } + + if (e.IsConst && e.FuncDecl.Name.ToString() == "oo") + { + return Rational.PositiveInfinity; + } + + if (e.IsConst && e.FuncDecl.Name.ToString() == "epsilon") + { + return Rational.One/Rational.PositiveInfinity; + } + + Debug.Assert(false, "Should not happen"); + return Rational.One; + } + } +} diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseDirective.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseDirective.cs new file mode 100644 index 000000000..e1403f698 --- /dev/null +++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseDirective.cs @@ -0,0 +1,101 @@ +using System; +using System.Text; +using Microsoft.SolverFoundation.Services; + +namespace Microsoft.SolverFoundation.Plugin.Z3 +{ + /// + /// Combining objective functions + /// + public enum OptimizationKind + { + Lexicographic, + BoundingBox, + ParetoOptimal + }; + + /// + /// Algorithm for solving cardinality constraints + /// + public enum CardinalityAlgorithm + { + FuMalik, + CoreMaxSAT + } + + /// + /// Algorithm for solving pseudo-boolean constraints + /// + public enum PseudoBooleanAlgorithm + { + WeightedMaxSAT, + IterativeWeightedMaxSAT, + BisectionWeightedMaxSAT, + WeightedPartialMaxSAT2 + } + + /// + /// Strategy for solving arithmetic optimization + /// + public enum ArithmeticStrategy + { + Basic, + Farkas + } + + public abstract class Z3BaseDirective : Directive + { + protected OptimizationKind _optKind; + protected CardinalityAlgorithm _cardAlgorithm; + protected PseudoBooleanAlgorithm _pboAlgorithm; + protected ArithmeticStrategy _arithStrategy; + + protected string _smt2LogFile; + + public Z3BaseDirective() + { + Arithmetic = Arithmetic.Exact; + } + + public OptimizationKind OptKind + { + get { return _optKind; } + set { _optKind = value; } + } + + public CardinalityAlgorithm CardinalityAlgorithm + { + get { return _cardAlgorithm; } + set { _cardAlgorithm = value; } + } + + public PseudoBooleanAlgorithm PseudoBooleanAlgorithm + { + get { return _pboAlgorithm; } + set { _pboAlgorithm = value; } + } + + public ArithmeticStrategy ArithmeticStrategy + { + get { return _arithStrategy; } + set { _arithStrategy = value; } + } + + public string SMT2LogFile + { + get { return _smt2LogFile; } + set { _smt2LogFile = value; } + } + + public override string ToString() + { + var sb = new StringBuilder(); + sb.Append(this.GetType().Name); + sb.Append("("); + sb.AppendFormat("OptKind: {0}, ", _optKind); + sb.AppendFormat("SMT2LogFile: {0}", _smt2LogFile); + sb.Append(")"); + return sb.ToString(); + } + } +} diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseParams.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseParams.cs new file mode 100644 index 000000000..6585181ec --- /dev/null +++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseParams.cs @@ -0,0 +1,103 @@ +using Microsoft.SolverFoundation.Services; +using System; + +namespace Microsoft.SolverFoundation.Plugin.Z3 +{ + /// + /// Implementation of the solver parameters for Z3 + /// + public class Z3BaseParams : ISolverParameters + { + #region Private Members + + /// The abort method we can call (defaults to always false) + protected Func _queryAbortFunction = delegate() { return false; }; + + /// The directive to use + protected Directive _directive = null; + + protected OptimizationKind _optKind; + protected CardinalityAlgorithm _cardAlgorithm; + protected PseudoBooleanAlgorithm _pboAlgorithm; + protected ArithmeticStrategy _arithStrategy; + + protected string _smt2LogFile; + + #endregion Private Members + + #region Construction + + public Z3BaseParams() { } + + public Z3BaseParams(Directive directive) + { + _directive = directive; + + var z3Directive = directive as Z3BaseDirective; + if (z3Directive != null) + { + _optKind = z3Directive.OptKind; + _cardAlgorithm = z3Directive.CardinalityAlgorithm; + _pboAlgorithm = z3Directive.PseudoBooleanAlgorithm; + _arithStrategy = z3Directive.ArithmeticStrategy; + _smt2LogFile = z3Directive.SMT2LogFile; + } + } + + public Z3BaseParams(Func queryAbortFunction) + { + _queryAbortFunction = queryAbortFunction; + } + + public Z3BaseParams(Z3BaseParams z3Parameters) + { + _queryAbortFunction = z3Parameters._queryAbortFunction; + } + + #endregion Construction + + #region ISolverParameters Members + + /// + /// Getter for the abort method + /// + public Func QueryAbort + { + get { return _queryAbortFunction; } + set { _queryAbortFunction = value; } + } + + public OptimizationKind OptKind + { + get { return _optKind; } + set { _optKind = value; } + } + + public CardinalityAlgorithm CardinalityAlgorithm + { + get { return _cardAlgorithm; } + set { _cardAlgorithm = value; } + } + + public PseudoBooleanAlgorithm PseudoBooleanAlgorithm + { + get { return _pboAlgorithm; } + set { _pboAlgorithm = value; } + } + + public ArithmeticStrategy ArithmeticStrategy + { + get { return _arithStrategy; } + set { _arithStrategy = value; } + } + + public string SMT2LogFile + { + get { return _smt2LogFile; } + set { _smt2LogFile = value; } + } + + #endregion + } + +} \ No newline at end of file diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs new file mode 100644 index 000000000..54e3893f0 --- /dev/null +++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs @@ -0,0 +1,381 @@ +using System; +using System.Collections.Generic; +using System.Threading; +using System.IO; +using System.Linq; +using System.Text; +using System.Diagnostics; +using Microsoft.Z3; +using Microsoft.SolverFoundation.Common; +using Microsoft.SolverFoundation.Services; + +namespace Microsoft.SolverFoundation.Plugin.Z3 +{ + internal enum Z3Result + { + Optimal, + LocalOptimal, + Feasible, + Interrupted, + Infeasible + } + + /// + /// The basic solver class to take care of transformation from an MSF instance to an Z3 instance + /// + internal class Z3BaseSolver + { + /// Representing MSF model + private IRowVariableModel _model; + + /// The Z3 solver we are currently using + private Context _context = null; + + /// Default optimization solver + private Optimize _optSolver = null; + + /// Marks when we are inside the Solve() method + private bool _isSolving = false; + + /// A map from MSF variable ids to Z3 variables + private Dictionary _variables = new Dictionary(); + + /// A map from MSF variable ids to Z3 goal ids + private Dictionary _goals = new Dictionary(); + + internal Z3BaseSolver(IRowVariableModel model) + { + _model = model; + } + + internal Context Context + { + get { return _context; } + } + + internal Dictionary Variables + { + get { return _variables; } + } + + internal Dictionary Goals + { + get { return _goals; } + } + + /// + /// Destructs a currently active Z3 solver and the associated data. + /// + internal void DestructSolver(bool checkInSolve) + { + if (_context != null) + { + if (checkInSolve && !_isSolving) + { + _variables.Clear(); + if (!_isSolving) + { + _optSolver.Dispose(); + _context.Dispose(); + } + } + else + { + Console.Error.WriteLine("Z3 destruction is invoked while in Solving phase."); + } + } + } + + /// + /// Constructs a Z3 solver to be used. + /// + internal void ConstructSolver(Z3BaseParams parameters) + { + // If Z3 is there already, kill it + if (_context != null) + { + DestructSolver(false); + } + + _context = new Context(); + _optSolver = _context.MkOptimize(); + var p = _context.MkParams(); + + switch (parameters.OptKind) + { + case OptimizationKind.BoundingBox: + p.Add("priority", _context.MkSymbol("box")); + break; + case OptimizationKind.Lexicographic: + p.Add("priority", _context.MkSymbol("lex")); + break; + case OptimizationKind.ParetoOptimal: + p.Add("priority", _context.MkSymbol("pareto")); + break; + default: + Debug.Assert(false, String.Format("Unknown optimization option {0}", parameters.OptKind)); + break; + } + + switch (parameters.CardinalityAlgorithm) + { + case CardinalityAlgorithm.FuMalik: + p.Add("maxsat_engine", _context.MkSymbol("fu_malik")); + break; + case CardinalityAlgorithm.CoreMaxSAT: + p.Add("maxsat_engine", _context.MkSymbol("core_maxsat")); + break; + default: + Debug.Assert(false, String.Format("Unknown cardinality algorithm option {0}", parameters.CardinalityAlgorithm)); + break; + } + + switch (parameters.PseudoBooleanAlgorithm) + { + case PseudoBooleanAlgorithm.WeightedMaxSAT: + p.Add("wmaxsat_engine", _context.MkSymbol("wmax")); + break; + case PseudoBooleanAlgorithm.IterativeWeightedMaxSAT: + p.Add("wmaxsat_engine", _context.MkSymbol("iwmax")); + break; + case PseudoBooleanAlgorithm.BisectionWeightedMaxSAT: + p.Add("wmaxsat_engine", _context.MkSymbol("bwmax")); + break; + case PseudoBooleanAlgorithm.WeightedPartialMaxSAT2: + p.Add("wmaxsat_engine", _context.MkSymbol("wpm2")); + break; + default: + Debug.Assert(false, String.Format("Unknown pseudo-boolean algorithm option {0}", parameters.PseudoBooleanAlgorithm)); + break; + } + + switch (parameters.ArithmeticStrategy) + { + case ArithmeticStrategy.Basic: + p.Add("engine", _context.MkSymbol("basic")); + break; + case ArithmeticStrategy.Farkas: + p.Add("engine", _context.MkSymbol("farkas")); + break; + default: + Debug.Assert(false, String.Format("Unknown arithmetic strategy option {0}", parameters.ArithmeticStrategy)); + break; + } + + _optSolver.Parameters = p; + } + + internal ArithExpr GetVariable(int vid) + { + Expr variable; + if (!_variables.TryGetValue(vid, out variable)) + { + AddVariable(vid); + variable = _variables[vid]; + } + return (ArithExpr)variable; + } + + internal void AssertBool(BoolExpr row) + { + _optSolver.Assert(row); + } + + internal void AssertArith(int vid, ArithExpr variable) + { + // Get the bounds on the row + Rational lower, upper; + _model.GetBounds(vid, out lower, out upper); + + // Case of equality + if (lower == upper) + { + // Create the equality term + Expr eqConst = GetNumeral(lower, variable.Sort); + BoolExpr constraint = _context.MkEq(eqConst, variable); + // Assert the constraint + _optSolver.Assert(constraint); + } + else + { + // If upper bound is finite assert the upper bound constraint + if (lower.IsFinite) + { + // Create the lower Bound constraint + ArithExpr lowerTerm = GetNumeral(lower, variable.Sort); + BoolExpr constraint = _context.MkLe(lowerTerm, variable); + // Assert the constraint + _optSolver.Assert(constraint); + } + // If lower bound is finite assert the lower bound constraint + if (upper.IsFinite) + { + // Create the upper bound constraint + ArithExpr upperTerm = GetNumeral(upper, variable.Sort); + BoolExpr constraint = _context.MkGe(upperTerm, variable); + // Assert the constraint + _optSolver.Assert(constraint); + } + } + } + + /// + /// Adds a MSF variable with the coresponding assertion to the Z3 variables. + /// + /// The MSF id of the variable + internal void AddVariable(int vid) + { + // Is the variable an integer + bool isInteger = _model.GetIntegrality(vid); + + // Construct the sort we will be using + Sort sort = isInteger ? (Sort)_context.IntSort : (Sort)_context.RealSort; + + // Get the variable key + object key = _model.GetKeyFromIndex(vid); + + // Try to construct the name + string name; + if (key != null) name = String.Format("x_{0}_{1}", key, vid); + else name = String.Format("x_{0}", vid); + ArithExpr variable = (ArithExpr)_context.MkConst(name, sort); + + // Create the variable and add it to the map + Debug.Assert(!_variables.ContainsKey(vid), "Variable names should be unique."); + _variables.Add(vid, variable); + + AssertArith(vid, variable); + } + + internal ArithExpr GetNumeral(Rational rational, Sort sort = null) + { + return Utils.GetNumeral(_context, rational, sort); + } + + internal void Solve(Z3BaseParams parameters, IEnumerable modelGoals, + Action addRow, Func mkGoalRow, Action setResult) + { + _variables.Clear(); + _goals.Clear(); + + try + { + // Mark that we are in solving phase + _isSolving = true; + + // Construct Z3 + ConstructSolver(parameters); + + // Add all the variables + foreach (int vid in _model.VariableIndices) + { + AddVariable(vid); + } + + // Add all the rows + foreach (int rid in _model.RowIndices) + { + addRow(rid); + } + + // Add enabled goals to optimization problem + foreach (IGoal g in modelGoals) + { + if (!g.Enabled) continue; + + ArithExpr gr = mkGoalRow(g.Index); + if (g.Minimize) + _goals.Add(g, _optSolver.MkMinimize(gr)); + else + _goals.Add(g, _optSolver.MkMaximize(gr)); + } + + if (_goals.Any() && parameters.SMT2LogFile != null) + { + Debug.WriteLine("Dumping SMT2 benchmark to log file..."); + File.WriteAllText(parameters.SMT2LogFile, _optSolver.ToString()); + } + + bool aborted = parameters.QueryAbort(); + + if (!aborted) + { + // Start the abort thread + AbortWorker abortWorker = new AbortWorker(_context, parameters.QueryAbort); + Thread abortThread = new Thread(abortWorker.Start); + abortThread.Start(); + + // Now solve the problem + Status status = _optSolver.Check(); + + // Stop the abort thread + abortWorker.Stop(); + abortThread.Join(); + + switch (status) + { + case Status.SATISFIABLE: + Microsoft.Z3.Model model = _optSolver.Model; + Debug.Assert(model != null, "Should be able to get Z3 model."); + // Remember the solution values + foreach (KeyValuePair pair in _variables) + { + var value = Utils.ToRational(model.Eval(pair.Value, true)); + _model.SetValue(pair.Key, value); + } + // Remember all objective values + foreach (var pair in _goals) + { + var optimalValue = Utils.ToRational(_optSolver.GetUpper(pair.Value)); + _model.SetValue(pair.Key.Index, optimalValue); + } + model.Dispose(); + setResult(_goals.Any() ? Z3Result.Optimal : Z3Result.Feasible); + break; + case Status.UNSATISFIABLE: + setResult(Z3Result.Infeasible); + break; + case Status.UNKNOWN: + if (abortWorker.Aborted) + { + Microsoft.Z3.Model subOptimalModel = _optSolver.Model; + if (subOptimalModel != null && subOptimalModel.NumConsts != 0) + { + // Remember the solution values + foreach (KeyValuePair pair in _variables) + { + var value = Utils.ToRational(subOptimalModel.Eval(pair.Value, true)); + _model.SetValue(pair.Key, value); + } + // Remember all objective values + foreach (var pair in _goals) + { + var optimalValue = Utils.ToRational(_optSolver.GetUpper(pair.Value)); + _model.SetValue(pair.Key.Index, optimalValue); + } + subOptimalModel.Dispose(); + + setResult(Z3Result.LocalOptimal); + } + else + setResult(Z3Result.Infeasible); + } + else + setResult(Z3Result.Interrupted); + break; + default: + Debug.Assert(false, "Unrecognized Z3 Status"); + break; + } + } + } + finally + { + _isSolving = false; + } + + // Now kill Z3 + DestructSolver(true); + } + } +} diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPDirective.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPDirective.cs new file mode 100644 index 000000000..69f9ff6c1 --- /dev/null +++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPDirective.cs @@ -0,0 +1,9 @@ +using Microsoft.SolverFoundation.Services; +using System; + +namespace Microsoft.SolverFoundation.Plugin.Z3 +{ + public class Z3MILPDirective : Z3BaseDirective + { + } +} diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPParams.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPParams.cs new file mode 100644 index 000000000..38bd9040a --- /dev/null +++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPParams.cs @@ -0,0 +1,19 @@ +using Microsoft.SolverFoundation.Services; +using System; + +namespace Microsoft.SolverFoundation.Plugin.Z3 +{ + public class Z3MILPParams : Z3BaseParams + { + // Need these constructors for reflection done by plugin model + + public Z3MILPParams() : base() { } + + public Z3MILPParams(Directive directive) : base(directive) { } + + public Z3MILPParams(Func queryAbortFunction) : base(queryAbortFunction) { } + + public Z3MILPParams(Z3BaseParams z3Parameters) : base (z3Parameters) { } + } + +} \ No newline at end of file diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPSolver.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPSolver.cs new file mode 100644 index 000000000..b31f6de97 --- /dev/null +++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPSolver.cs @@ -0,0 +1,230 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics; +using System.Linq; +using System.IO; + +using Microsoft.Z3; +using Microsoft.SolverFoundation.Common; +using Microsoft.SolverFoundation.Services; +using Microsoft.SolverFoundation.Plugin; + +namespace Microsoft.SolverFoundation.Plugin.Z3 +{ + /// + /// The class is implementation of the MSF mixed linear programming solver + /// using the Microsoft Z3 solver as the backend. + /// + public class Z3MILPSolver : LinearModel, ILinearSolver, ILinearSolution, IReportProvider + { + #region Private members + + private LinearResult _result; + private LinearSolutionQuality _solutionQuality; + private Z3BaseSolver _solver; + + #endregion Private members + + #region Solver construction and destruction + + /// Constructor that initializes the base clases + public Z3MILPSolver() : base(null) + { + _result = LinearResult.Feasible; + _solver = new Z3BaseSolver(this); + } + + /// Constructor that initializes the base clases + public Z3MILPSolver(ISolverEnvironment context) : this() { } + + /// + /// Shutdown can be called when when the solver is not active, i.e. + /// when it is done with Solve() or it has gracefully returns from Solve() + /// after an abort. + /// + public void Shutdown() { _solver.DestructSolver(true); } + + #endregion Solver construction and destruction + + #region Obtaining information about the solution + + public ILinearSolverReport GetReport(LinearSolverReportType reportType) + { + // We don't support sensitivity report + return null; + } + + #endregion Obtaining information about the solution + + #region Construction of the problem + + /// + /// Get corresponding Z3 formula of a MSF row. + /// + /// The MSF row id + private ArithExpr MkGoalRow(int rid) + { + // Start with the 0 term + List row = new List(); + + // Now, add all the entries of this row + foreach (LinearEntry entry in GetRowEntries(rid)) + { + // Get the variable and constant in the row + ArithExpr e = _solver.GetVariable(entry.Index); + if (!entry.Value.IsOne) + { + e = _solver.Context.MkMul(_solver.GetNumeral(entry.Value, e.Sort), e); + } + row.Add(e); + } + switch (row.Count) + { + case 0: return _solver.GetNumeral(new Rational()); + case 1: return row[0]; + default: return _solver.Context.MkAdd(row.ToArray()); + } + } + + /// + /// Adds a MSF row to the Z3 assertions. + /// + /// The MSF row id + private void AddRow(int rid) + { + // Start with the 0 term + ArithExpr row = MkGoalRow(rid); + _solver.AssertArith(rid, row); + } + + /// + /// Set results based on internal solver status + /// + private void SetResult(Z3Result status) + { + switch (status) + { + case Z3Result.Optimal: + _result = LinearResult.Optimal; + _solutionQuality = LinearSolutionQuality.Exact; + break; + case Z3Result.LocalOptimal: + _result = LinearResult.Feasible; + _solutionQuality = LinearSolutionQuality.Approximate; + break; + case Z3Result.Feasible: + _result = LinearResult.Feasible; + _solutionQuality = LinearSolutionQuality.Exact; + break; + case Z3Result.Infeasible: + _result = LinearResult.InfeasiblePrimal; + _solutionQuality = LinearSolutionQuality.None; + break; + case Z3Result.Interrupted: + _result = LinearResult.Interrupted; + _solutionQuality = LinearSolutionQuality.None; + break; + default: + Debug.Assert(false, "Unrecognized Z3 Result"); + break; + } + } + + #endregion Construction of the problem + + #region Solving the problem + + /// + /// Starts solving the problem using the Z3 solver. + /// + /// Parameters to the solver + /// The solution to the problem + public ILinearSolution Solve(ISolverParameters parameters) + { + // Get the Z3 parameters + var z3Params = parameters as Z3BaseParams; + Debug.Assert(z3Params != null, "Parameters should be an instance of Z3BaseParams."); + + _solver.Solve(z3Params, Goals, AddRow, MkGoalRow, SetResult); + + return this; + } + + #endregion Solving the problem + + #region ILinearSolution Members + + public Rational GetSolutionValue(int goalIndex) + { + var goal = Goals.ElementAt(goalIndex); + Debug.Assert(goal != null, "Goal should be an element of the goal list."); + return GetValue(goal.Index); + } + + public void GetSolvedGoal(int goalIndex, out object key, out int vid, out bool minimize, out bool optimal) + { + var goal = Goals.ElementAt(goalIndex); + Debug.Assert(goal != null, "Goal should be an element of the goal list."); + key = goal.Key; + vid = goal.Index; + minimize = goal.Minimize; + optimal = _result == LinearResult.Optimal; + } + + // LpResult is LP relaxation assignment. + + public LinearResult LpResult + { + get { return _result; } + } + + public Rational MipBestBound + { + get + { + Debug.Assert(GoalCount > 0, "MipBestBound is only applicable for optimization instances."); + return GetSolutionValue(0); + } + } + + public LinearResult MipResult + { + get { return _result; } + } + + public LinearResult Result + { + get { return _result; } + } + + public LinearSolutionQuality SolutionQuality + { + get { return _solutionQuality; } + } + + public int SolvedGoalCount + { + get { return GoalCount; } + } + + #endregion + + public Report GetReport(SolverContext context, Solution solution, SolutionMapping solutionMapping) + { + LinearSolutionMapping lpSolutionMapping = solutionMapping as LinearSolutionMapping; + if (lpSolutionMapping == null && solutionMapping != null) + throw new ArgumentException("solutionMapping is not a LinearSolutionMapping", "solutionMapping"); + return new Z3LinearSolverReport(context, this, solution, lpSolutionMapping); + } + } + + /// + /// Class implementing the LinearReport. + /// + public class Z3LinearSolverReport : LinearReport + { + public Z3LinearSolverReport(SolverContext context, ISolver solver, Solution solution, LinearSolutionMapping solutionMapping) + : base(context, solver, solution, solutionMapping) { + } + } +} diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3TermDirective.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3TermDirective.cs new file mode 100644 index 000000000..12dcb6e84 --- /dev/null +++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3TermDirective.cs @@ -0,0 +1,9 @@ +using Microsoft.SolverFoundation.Services; +using System; + +namespace Microsoft.SolverFoundation.Plugin.Z3 +{ + public class Z3TermDirective : Z3BaseDirective + { + } +} diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3TermParams.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3TermParams.cs new file mode 100644 index 000000000..48a90afe1 --- /dev/null +++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3TermParams.cs @@ -0,0 +1,17 @@ +using Microsoft.SolverFoundation.Services; +using System; + +namespace Microsoft.SolverFoundation.Plugin.Z3 +{ + public class Z3TermParams : Z3BaseParams + { + public Z3TermParams() : base() { } + + public Z3TermParams(Directive directive) : base(directive) { } + + public Z3TermParams(Func queryAbortFunction) : base(queryAbortFunction) { } + + public Z3TermParams(Z3BaseParams z3Parameters) : base(z3Parameters) { } + } + +} \ No newline at end of file diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3TermSolver.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3TermSolver.cs new file mode 100644 index 000000000..3317b9a4d --- /dev/null +++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3TermSolver.cs @@ -0,0 +1,382 @@ +using System; +using System.Threading; +using System.Globalization; +using System.Collections.Generic; +using Microsoft.SolverFoundation.Common; +using Microsoft.SolverFoundation.Properties; +using Microsoft.SolverFoundation.Solvers; +using Microsoft.SolverFoundation.Services; +using Microsoft.Z3; +using System.Linq; +using System.Diagnostics; +using System.IO; + +namespace Microsoft.SolverFoundation.Plugin.Z3 +{ + /// + /// The class is implementation of the MSF constraint solver + /// using the Microsoft Z3 solver as the backend. + /// This solver supports Int, Real constraints and their arbitrary boolean combinations. + /// + public class Z3TermSolver : TermModel, ITermSolver, INonlinearSolution, IReportProvider + { + private NonlinearResult _result; + private Z3BaseSolver _solver; + + /// Constructor that initializes the base clases + public Z3TermSolver() : base(null) + { + _solver = new Z3BaseSolver(this); + } + + /// Constructor that initializes the base clases + public Z3TermSolver(ISolverEnvironment context) : this() { } + + /// + /// Shutdown can be called when when the solver is not active, i.e. + /// when it is done with Solve() or it has gracefully returns from Solve() + /// after an abort. + /// + public void Shutdown() { _solver.DestructSolver(true); } + + private BoolExpr MkBool(int rid) + { + var context = _solver.Context; + + if (IsConstant(rid)) + { + Rational lower, upper; + GetBounds(rid, out lower, out upper); + Debug.Assert(lower == upper); + if (lower.IsZero) return context.MkFalse(); + return context.MkTrue(); + } + if (IsOperation(rid)) + { + BoolExpr[] children; + ArithExpr[] operands; + TermModelOperation op = GetOperation(rid); + switch(op) { + case TermModelOperation.And: + Debug.Assert(GetOperandCount(rid) >= 2, "Conjunction requires at least two operands."); + children = (GetOperands(rid)).Select(x => MkBool(x)).ToArray(); + return context.MkAnd(children); + case TermModelOperation.Or: + Debug.Assert(GetOperandCount(rid) >= 2, "Disjunction requires at least two operands."); + children = (GetOperands(rid)).Select(x => MkBool(x)).ToArray(); + return context.MkOr(children); + case TermModelOperation.Not: + Debug.Assert(GetOperandCount(rid) == 1, "Negation is unary."); + return context.MkNot(MkBool(GetOperand(rid, 0))); + case TermModelOperation.If: + Debug.Assert(GetOperandCount(rid) == 3, "If is ternary."); + BoolExpr b = MkBool(GetOperand(rid, 0)); + Expr x1 = MkBool(GetOperand(rid, 1)); + Expr x2 = MkBool(GetOperand(rid, 2)); + return (BoolExpr)context.MkITE(b, x1, x2); + case TermModelOperation.Unequal: + Debug.Assert(GetOperandCount(rid) >= 2, "Distinct should have at least two operands."); + return context.MkDistinct((GetOperands(rid)).Select(x => MkTerm(x)).ToArray()); + case TermModelOperation.Greater: + case TermModelOperation.Less: + case TermModelOperation.GreaterEqual: + case TermModelOperation.LessEqual: + case TermModelOperation.Equal: + Debug.Assert(GetOperandCount(rid) >= 2, "Comparison should have at least two operands."); + operands = (GetOperands(rid)).Select(x => MkTerm(x)).ToArray(); + return ReduceComparison(GetOperation(rid), operands); + case TermModelOperation.Identity: + Debug.Assert(GetOperandCount(rid) == 1, "Identity takes exactly one operand."); + return MkBool(GetOperand(rid, 0)); + default: + return context.MkEq(MkTerm(rid), _solver.GetNumeral(Rational.One)); + } + } + return context.MkEq(MkTerm(rid), _solver.GetNumeral(Rational.One)); + } + + private ArithExpr MkBoolToArith(BoolExpr e) + { + var context = _solver.Context; + return (ArithExpr)context.MkITE(e, _solver.GetNumeral(Rational.One), _solver.GetNumeral(Rational.Zero)); + } + + private ArithExpr MkTerm(int rid) + { + var context = _solver.Context; + + if (IsConstant(rid)) + { + Rational lower, upper; + GetBounds(rid, out lower, out upper); + Debug.Assert(lower == upper); + return _solver.GetNumeral(lower); + } + else if (IsOperation(rid)) + { + ArithExpr[] operands; + TermModelOperation op = GetOperation(rid); + switch(op) + { + case TermModelOperation.And: + case TermModelOperation.Or: + case TermModelOperation.Not: + case TermModelOperation.Unequal: + case TermModelOperation.Greater: + case TermModelOperation.Less: + case TermModelOperation.GreaterEqual: + case TermModelOperation.LessEqual: + case TermModelOperation.Equal: + return MkBoolToArith(MkBool(rid)); + case TermModelOperation.If: + Debug.Assert(GetOperandCount(rid) == 3, "If is ternary."); + BoolExpr b = MkBool(GetOperand(rid, 0)); + Expr x1 = MkTerm(GetOperand(rid, 1)); + Expr x2 = MkTerm(GetOperand(rid, 2)); + return (ArithExpr)context.MkITE(b, x1, x2); + case TermModelOperation.Plus: + Debug.Assert(GetOperandCount(rid) >= 2, "Plus takes at least two operands."); + operands = (GetOperands(rid)).Select(x => MkTerm(x)).ToArray(); + return context.MkAdd(operands); + case TermModelOperation.Minus: + Debug.Assert(GetOperandCount(rid) == 1, "Minus takes exactly one operand."); + return context.MkUnaryMinus(MkTerm(GetOperand(rid, 0))); + case TermModelOperation.Times: + Debug.Assert(GetOperandCount(rid) >= 2, "Times requires at least two operands."); + operands = (GetOperands(rid)).Select(x => MkTerm(x)).ToArray(); + return context.MkMul(operands); + case TermModelOperation.Identity: + Debug.Assert(GetOperandCount(rid) == 1, "Identity takes exactly one operand."); + return MkTerm(GetOperand(rid, 0)); + case TermModelOperation.Abs: + Debug.Assert(GetOperandCount(rid) == 1, "Abs takes exactly one operand."); + ArithExpr e = MkTerm(GetOperand(rid, 0)); + ArithExpr minusE = context.MkUnaryMinus(e); + ArithExpr zero = _solver.GetNumeral(Rational.Zero); + return (ArithExpr)context.MkITE(context.MkGe(e, zero), e, minusE); + default: + Console.Error.WriteLine("{0} operation isn't supported.", op); + throw new NotSupportedException(); + } + } + else + { + return _solver.GetVariable(rid); + } + } + + private BoolExpr ReduceComparison(TermModelOperation type, ArithExpr[] operands) + { + var context = _solver.Context; + Debug.Assert(operands.Length >= 2); + Func mkComparison; + switch (type) + { + case TermModelOperation.Greater: + mkComparison = (x, y) => context.MkGt(x, y); + break; + case TermModelOperation.Less: + mkComparison = (x, y) => context.MkLt(x, y); + break; + case TermModelOperation.GreaterEqual: + mkComparison = (x, y) => context.MkGe(x, y); + break; + case TermModelOperation.LessEqual: + mkComparison = (x, y) => context.MkLe(x, y); + break; + case TermModelOperation.Equal: + mkComparison = (x, y) => context.MkEq(x, y); + break; + default: + throw new NotSupportedException(); + } + + BoolExpr current = mkComparison(operands[0], operands[1]); + for (int i = 1; i < operands.Length - 1; ++i) + current = context.MkAnd(current, mkComparison(operands[i], operands[i + 1])); + return current; + } + + private bool IsBoolRow(int rid) + { + Rational lower, upper; + GetBounds(rid, out lower, out upper); + + return lower == upper && lower.IsOne && IsBoolTerm(rid); + } + + private bool IsBoolTerm(int rid) + { + if (IsConstant(rid)) + { + Rational lower, upper; + GetBounds(rid, out lower, out upper); + Debug.Assert(lower == upper); + return lower.IsOne || lower.IsZero; + } + if (IsOperation(rid)) + { + TermModelOperation op = GetOperation(rid); + switch (op) + { + case TermModelOperation.And: + case TermModelOperation.Or: + case TermModelOperation.Not: + case TermModelOperation.LessEqual: + case TermModelOperation.Less: + case TermModelOperation.Greater: + case TermModelOperation.GreaterEqual: + case TermModelOperation.Unequal: + case TermModelOperation.Equal: + return true; + case TermModelOperation.If: + return IsBoolTerm(GetOperand(rid, 1)) && + IsBoolTerm(GetOperand(rid, 2)); + case TermModelOperation.Identity: + return IsBoolTerm(GetOperand(rid, 0)); + default: + return false; + } + } + return false; + } + + /// + /// Adds a MSF row to the Z3 assertions. + /// + /// The MSF row id + private void AddRow(int rid) + { + if (IsConstant(rid)) + return; + + if (IsBoolRow(rid)) + { + _solver.AssertBool(MkBool(rid)); + return; + } + // Start with the 0 term + ArithExpr row = MkTerm(rid); + _solver.AssertArith(rid, row); + } + + private TermModelOperation[] _supportedOperations = + { TermModelOperation.And, + TermModelOperation.Or, + TermModelOperation.Not, + TermModelOperation.Unequal, + TermModelOperation.Greater, + TermModelOperation.Less, + TermModelOperation.GreaterEqual, + TermModelOperation.LessEqual, + TermModelOperation.Equal, + TermModelOperation.If, + TermModelOperation.Plus, + TermModelOperation.Minus, + TermModelOperation.Times, + TermModelOperation.Identity, + TermModelOperation.Abs }; + + /// + /// Gets the operations supported by the solver. + /// + /// All the TermModelOperations supported by the solver. + public IEnumerable SupportedOperations + { + get { return _supportedOperations; } + } + + /// + /// Set results based on internal solver status + /// + private void SetResult(Z3Result status) + { + switch (status) + { + case Z3Result.Optimal: + _result = NonlinearResult.Optimal; + break; + case Z3Result.LocalOptimal: + _result = NonlinearResult.LocalOptimal; + break; + case Z3Result.Feasible: + _result = NonlinearResult.Feasible; + break; + case Z3Result.Infeasible: + _result = NonlinearResult.Infeasible; + break; + case Z3Result.Interrupted: + _result = NonlinearResult.Interrupted; + break; + default: + Debug.Assert(false, "Unrecognized Z3 Result"); + break; + } + } + + /// + /// Starts solving the problem using the Z3 solver. + /// + /// Parameters to the solver + /// The solution to the problem + public INonlinearSolution Solve(ISolverParameters parameters) + { + // Get the Z3 parameters + var z3Params = parameters as Z3BaseParams; + Debug.Assert(z3Params != null, "Parameters should be an instance of Z3BaseParams."); + + _solver.Solve(z3Params, Goals, AddRow, MkTerm, SetResult); + + return this; + } + + double INonlinearSolution.GetValue(int vid) + { + Debug.Assert(_solver.Variables.ContainsKey(vid), "This index should correspond to a variable."); + return GetValue(vid).ToDouble(); + } + + public int SolvedGoalCount + { + get { return GoalCount; } + } + + public double GetSolutionValue(int goalIndex) + { + var goal = Goals.ElementAt(goalIndex); + Debug.Assert(goal != null, "Goal should be an element of the goal list."); + return GetValue(goal.Index).ToDouble(); + } + + public void GetSolvedGoal(int goalIndex, out object key, out int vid, out bool minimize, out bool optimal) + { + var goal = Goals.ElementAt(goalIndex); + Debug.Assert(goal != null, "Goal should be an element of the goal list."); + key = goal.Key; + vid = goal.Index; + minimize = goal.Minimize; + optimal = _result == NonlinearResult.Optimal; + } + + public NonlinearResult Result + { + get { return _result; } + } + + public Report GetReport(SolverContext context, Solution solution, SolutionMapping solutionMapping) + { + PluginSolutionMapping pluginSolutionMapping = solutionMapping as PluginSolutionMapping; + if (pluginSolutionMapping == null && solutionMapping != null) + throw new ArgumentException("solutionMapping is not a LinearSolutionMapping", "solutionMapping"); + return new Z3TermSolverReport(context, this, solution, pluginSolutionMapping); + } + } + + public class Z3TermSolverReport : Report + { + public Z3TermSolverReport(SolverContext context, ISolver solver, Solution solution, PluginSolutionMapping pluginSolutionMapping) + : base(context, solver, solution, pluginSolutionMapping) + { + } + } +} diff --git a/examples/msf/Validator/App.config b/examples/msf/Validator/App.config new file mode 100644 index 000000000..75e2872f1 --- /dev/null +++ b/examples/msf/Validator/App.config @@ -0,0 +1,60 @@ + + + +
+ + + + + + + + + + + + + + + + diff --git a/examples/msf/Validator/MicrosoftSolverFoundationForExcel.dll.config b/examples/msf/Validator/MicrosoftSolverFoundationForExcel.dll.config new file mode 100644 index 000000000..cd9dcad25 --- /dev/null +++ b/examples/msf/Validator/MicrosoftSolverFoundationForExcel.dll.config @@ -0,0 +1,58 @@ + + + +
+ + + + + + + + + + + + + diff --git a/examples/msf/Validator/Program.cs b/examples/msf/Validator/Program.cs new file mode 100644 index 000000000..758c65c78 --- /dev/null +++ b/examples/msf/Validator/Program.cs @@ -0,0 +1,194 @@ +using System; +using System.IO; +using System.Linq; +using System.Collections.Generic; +using Microsoft.SolverFoundation.Common; +using Microsoft.SolverFoundation.Solvers; +using Microsoft.SolverFoundation.Plugin.Z3; +using Microsoft.SolverFoundation.Services; +using System.Text; + +namespace Validator +{ + class Program + { + static void LoadModel(SolverContext context, string fileName) + { + string ext = Path.GetExtension(fileName).ToLower(); + + if (ext == ".mps") + { + context.LoadModel(FileFormat.MPS, Path.GetFullPath(fileName)); + } + else if (ext == ".smps") + { + context.LoadModel(FileFormat.SMPS, Path.GetFullPath(fileName)); + } + else if (ext == ".oml") + { + context.LoadModel(FileFormat.OML, Path.GetFullPath(fileName)); + } + else + { + throw new NotSupportedException("This file format hasn't been supported."); + } + } + + static void ExecuteZ3(string fileName, Z3BaseDirective directive) + { + SolverContext context = SolverContext.GetContext(); + try + { + LoadModel(context, fileName); + + Solution solution = context.Solve(directive); + Report report = solution.GetReport(); + Console.Write("{0}", report); + } + catch (Exception e) + { + Console.WriteLine("Skipping unsolvable instance in {0} with error message '{1}'.", fileName, e.Message); + } + finally + { + context.ClearModel(); + } + } + + static void ConvertToSMT2(string fileName, Z3BaseDirective directive) + { + SolverContext context = SolverContext.GetContext(); + try + { + LoadModel(context, fileName); + + if (context.CurrentModel.Goals.Any()) + { + directive.SMT2LogFile = Path.ChangeExtension(fileName, ".smt2"); + context.Solve(() => true, directive); + } + } + catch (Exception e) + { + Console.WriteLine("Skipping unconvertable instance in {0} with error message '{1}'.", fileName, e.Message); + } + finally + { + context.ClearModel(); + } + } + + static void ValidateZ3(string fileName, Z3BaseDirective directive) + { + SolverContext context = SolverContext.GetContext(); + try + { + LoadModel(context, fileName); + + if (context.CurrentModel.Goals.Any()) + { + var msfDirective = (directive is Z3MILPDirective) ? (Directive)new MixedIntegerProgrammingDirective() { TimeLimit = 10000 } + : (Directive)new Directive() { TimeLimit = 10000 }; + var sol1 = context.Solve(msfDirective); + + Console.WriteLine("Solved the model using MSF."); + Console.Write("{0}", sol1.GetReport()); + var expectedGoals = sol1.Goals.Select(x => x.ToDouble()); + context.ClearModel(); + + context.LoadModel(FileFormat.OML, Path.GetFullPath(fileName)); + directive.SMT2LogFile = Path.ChangeExtension(fileName, ".smt2"); + var sol2 = context.Solve(directive); + //Console.Write("{0}", sol2.GetReport()); + var actualGoals = sol2.Goals.Select(x => x.ToDouble()); + + Console.WriteLine("Solved the model using Z3."); + var goalPairs = expectedGoals.Zip(actualGoals, (expected, actual) => new { expected, actual }).ToArray(); + bool validated = goalPairs.All(p => Math.Abs(p.expected - p.actual) <= 0.0001); + if (validated) + { + Console.WriteLine("INFO: Two solvers give approximately the same results."); + } + else + { + Console.Error.WriteLine("ERROR: Discrepancy found between results."); + if (!validated && File.Exists(directive.SMT2LogFile)) + { + var sb = new StringBuilder(); + for(int i = 0; i < goalPairs.Length; i++) + { + sb.AppendFormat("\n(echo \"Goal {0}: actual |-> {1:0.0000}, expected |-> {2:0.0000}\")", + i + 1, goalPairs[i].actual, goalPairs[i].expected); + } + Console.Error.WriteLine(sb.ToString()); + File.AppendAllText(directive.SMT2LogFile, sb.ToString()); + } + } + } + else + { + Console.WriteLine("Ignoring this instance without having any goal."); + } + } + catch (Exception e) + { + Console.WriteLine("Skipping unsolvable instance in {0} with error message '{1}'.", + fileName, e.Message); + } + finally + { + context.ClearModel(); + } + } + + static void Main(string[] args) + { + Z3BaseDirective directive = new Z3MILPDirective(); + + for (int i = 0; i < args.Length; ++i) { + if (args[i] == "-s" || args[i] == "-solve") + { + ExecuteZ3(args[i + 1], directive); + return; + } + if (args[i] == "-c" || args[i] == "-convert") + { + ConvertToSMT2(args[i + 1], directive); + return; + } + if (args[i] == "-v" || args[i] == "-validate") + { + ValidateZ3(args[i + 1], directive); + return; + } + if (args[i] == "-t" || args[i] == "-term") + { + directive = new Z3TermDirective(); + } + } + + if (args.Length > 0) + { + ExecuteZ3(args[0], directive); + return; + } + + Console.WriteLine(@" +Validator is a simple command line to migrate benchmarks from OML, MPS and SMPS to SMT2 formats. + +Commands: + -solve : solving the model using Z3 + -convert : converting the model into SMT2 format + -validate : validating by comparing results between Z3 and MSF solvers + -term : change the default Z3 MILP solver to Z3 Term solver + + where is any file with OML, MPS or SMPS extension. + +Examples: + Validator.exe -convert model.mps + Validator.exe -term -solve model.oml + +"); + } + } +} diff --git a/examples/msf/Validator/Properties/AssemblyInfo.cs b/examples/msf/Validator/Properties/AssemblyInfo.cs new file mode 100644 index 000000000..eb2f8ed71 --- /dev/null +++ b/examples/msf/Validator/Properties/AssemblyInfo.cs @@ -0,0 +1,36 @@ +using System.Reflection; +using System.Runtime.CompilerServices; +using System.Runtime.InteropServices; + +// General Information about an assembly is controlled through the following +// set of attributes. Change these attribute values to modify the information +// associated with an assembly. +[assembly: AssemblyTitle("testSolver")] +[assembly: AssemblyDescription("")] +[assembly: AssemblyConfiguration("")] +[assembly: AssemblyCompany("Microsoft")] +[assembly: AssemblyProduct("testSolver")] +[assembly: AssemblyCopyright("Copyright © Microsoft 2009")] +[assembly: AssemblyTrademark("")] +[assembly: AssemblyCulture("")] + +// Setting ComVisible to false makes the types in this assembly not visible +// to COM components. If you need to access a type in this assembly from +// COM, set the ComVisible attribute to true on that type. +[assembly: ComVisible(false)] + +// The following GUID is for the ID of the typelib if this project is exposed to COM +[assembly: Guid("c03c1084-d119-483f-80fe-c639eae75959")] + +// Version information for an assembly consists of the following four values: +// +// Major Version +// Minor Version +// Build Number +// Revision +// +// You can specify all the values or you can default the Build and Revision Numbers +// by using the '*' as shown below: +// [assembly: AssemblyVersion("1.0.*")] +[assembly: AssemblyVersion("1.0.0.0")] +[assembly: AssemblyFileVersion("1.0.0.0")] diff --git a/examples/msf/Validator/Validator.csproj b/examples/msf/Validator/Validator.csproj new file mode 100644 index 000000000..97d00331d --- /dev/null +++ b/examples/msf/Validator/Validator.csproj @@ -0,0 +1,143 @@ + + + + Debug + AnyCPU + 9.0.21022 + 2.0 + {54835857-129F-44C9-B529-A42158647B36} + Exe + Properties + Validator + Validator + v4.0 + 512 + + + + + 3.5 + publish\ + true + Disk + false + Foreground + 7 + Days + false + false + true + 0 + 1.0.0.%2a + false + false + true + + + + true + full + false + bin\Debug\ + DEBUG;TRACE + prompt + 4 + + + pdbonly + true + bin\Release\ + TRACE + prompt + 4 + + + true + bin\x64\Debug\ + DEBUG;TRACE + full + x86 + true + GlobalSuppressions.cs + prompt + + + bin\x64\Release\ + TRACE + true + pdbonly + x64 + true + GlobalSuppressions.cs + prompt + + + true + bin\x86\Debug\ + DEBUG;TRACE + full + x86 + prompt + MinimumRecommendedRules.ruleset + + + bin\x86\Release\ + TRACE + true + pdbonly + x86 + prompt + MinimumRecommendedRules.ruleset + + + + ..\Microsoft.Solver.Foundation.dll + + + + 3.5 + + + 3.5 + + + 3.5 + + + + + + + + + + + + + + + False + .NET Framework 3.5 SP1 Client Profile + false + + + False + .NET Framework 3.5 SP1 + true + + + + + {7340e664-f648-4ff7-89b2-f4da424996d3} + SolverFoundation.Plugin.Z3 + + + + + \ No newline at end of file diff --git a/examples/msf/Z3MSFPlugin.sln b/examples/msf/Z3MSFPlugin.sln new file mode 100644 index 000000000..0554e16dd --- /dev/null +++ b/examples/msf/Z3MSFPlugin.sln @@ -0,0 +1,120 @@ + +Microsoft Visual Studio Solution File, Format Version 12.00 +# Visual Studio 2012 +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SolverFoundation.Plugin.Z3", "SolverFoundation.Plugin.Z3\SolverFoundation.Plugin.Z3.csproj", "{7340E664-F648-4FF7-89B2-F4DA424996D3}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SolverFoundation.Plugin.Z3.Tests", "SolverFoundation.Plugin.Z3.Tests\SolverFoundation.Plugin.Z3.Tests.csproj", "{280AEE2F-1FDB-4A27-BE37-14DC154C873B}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Validator", "Validator\Validator.csproj", "{54835857-129F-44C9-B529-A42158647B36}" +EndProject +Global + GlobalSection(SolutionConfigurationPlatforms) = preSolution + commercial_64|Any CPU = commercial_64|Any CPU + commercial_64|Mixed Platforms = commercial_64|Mixed Platforms + commercial_64|x64 = commercial_64|x64 + commercial_64|x86 = commercial_64|x86 + commercial|Any CPU = commercial|Any CPU + commercial|Mixed Platforms = commercial|Mixed Platforms + commercial|x64 = commercial|x64 + commercial|x86 = commercial|x86 + Debug|Any CPU = Debug|Any CPU + Debug|Mixed Platforms = Debug|Mixed Platforms + Debug|x64 = Debug|x64 + Debug|x86 = Debug|x86 + Release|Any CPU = Release|Any CPU + Release|Mixed Platforms = Release|Mixed Platforms + Release|x64 = Release|x64 + Release|x86 = Release|x86 + EndGlobalSection + GlobalSection(ProjectConfigurationPlatforms) = postSolution + {7340E664-F648-4FF7-89B2-F4DA424996D3}.commercial_64|Any CPU.ActiveCfg = commercial_64|Any CPU + {7340E664-F648-4FF7-89B2-F4DA424996D3}.commercial_64|Any CPU.Build.0 = commercial_64|Any CPU + {7340E664-F648-4FF7-89B2-F4DA424996D3}.commercial_64|Mixed Platforms.ActiveCfg = commercial_64|x86 + {7340E664-F648-4FF7-89B2-F4DA424996D3}.commercial_64|Mixed Platforms.Build.0 = commercial_64|x86 + {7340E664-F648-4FF7-89B2-F4DA424996D3}.commercial_64|x64.ActiveCfg = commercial_64|Any CPU + {7340E664-F648-4FF7-89B2-F4DA424996D3}.commercial_64|x86.ActiveCfg = commercial_64|x86 + {7340E664-F648-4FF7-89B2-F4DA424996D3}.commercial_64|x86.Build.0 = commercial_64|x86 + {7340E664-F648-4FF7-89B2-F4DA424996D3}.commercial|Any CPU.ActiveCfg = commercial|Any CPU + {7340E664-F648-4FF7-89B2-F4DA424996D3}.commercial|Any CPU.Build.0 = commercial|Any CPU + {7340E664-F648-4FF7-89B2-F4DA424996D3}.commercial|Mixed Platforms.ActiveCfg = commercial|x86 + {7340E664-F648-4FF7-89B2-F4DA424996D3}.commercial|Mixed Platforms.Build.0 = commercial|x86 + {7340E664-F648-4FF7-89B2-F4DA424996D3}.commercial|x64.ActiveCfg = commercial|Any CPU + {7340E664-F648-4FF7-89B2-F4DA424996D3}.commercial|x86.ActiveCfg = commercial|x86 + {7340E664-F648-4FF7-89B2-F4DA424996D3}.commercial|x86.Build.0 = commercial|x86 + {7340E664-F648-4FF7-89B2-F4DA424996D3}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {7340E664-F648-4FF7-89B2-F4DA424996D3}.Debug|Any CPU.Build.0 = Debug|Any CPU + {7340E664-F648-4FF7-89B2-F4DA424996D3}.Debug|Mixed Platforms.ActiveCfg = Debug|x86 + {7340E664-F648-4FF7-89B2-F4DA424996D3}.Debug|Mixed Platforms.Build.0 = Debug|x86 + {7340E664-F648-4FF7-89B2-F4DA424996D3}.Debug|x64.ActiveCfg = Debug|Any CPU + {7340E664-F648-4FF7-89B2-F4DA424996D3}.Debug|x86.ActiveCfg = Debug|x86 + {7340E664-F648-4FF7-89B2-F4DA424996D3}.Debug|x86.Build.0 = Debug|x86 + {7340E664-F648-4FF7-89B2-F4DA424996D3}.Release|Any CPU.ActiveCfg = Release|Any CPU + {7340E664-F648-4FF7-89B2-F4DA424996D3}.Release|Any CPU.Build.0 = Release|Any CPU + {7340E664-F648-4FF7-89B2-F4DA424996D3}.Release|Mixed Platforms.ActiveCfg = Release|x86 + {7340E664-F648-4FF7-89B2-F4DA424996D3}.Release|Mixed Platforms.Build.0 = Release|x86 + {7340E664-F648-4FF7-89B2-F4DA424996D3}.Release|x64.ActiveCfg = Release|Any CPU + {7340E664-F648-4FF7-89B2-F4DA424996D3}.Release|x86.ActiveCfg = Release|x86 + {7340E664-F648-4FF7-89B2-F4DA424996D3}.Release|x86.Build.0 = Release|x86 + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.commercial_64|Any CPU.ActiveCfg = Release|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.commercial_64|Any CPU.Build.0 = Release|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.commercial_64|Mixed Platforms.ActiveCfg = Release|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.commercial_64|Mixed Platforms.Build.0 = Release|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.commercial_64|x64.ActiveCfg = Release|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.commercial_64|x86.ActiveCfg = Release|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.commercial|Any CPU.ActiveCfg = Release|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.commercial|Any CPU.Build.0 = Release|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.commercial|Mixed Platforms.ActiveCfg = Release|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.commercial|Mixed Platforms.Build.0 = Release|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.commercial|x64.ActiveCfg = Release|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.commercial|x86.ActiveCfg = Release|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.Debug|Any CPU.Build.0 = Debug|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.Debug|x64.ActiveCfg = Debug|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.Debug|x86.ActiveCfg = Debug|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.Debug|x86.Build.0 = Debug|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.Release|Any CPU.ActiveCfg = Release|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.Release|Any CPU.Build.0 = Release|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.Release|Mixed Platforms.Build.0 = Release|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.Release|x64.ActiveCfg = Release|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.Release|x86.ActiveCfg = Release|Any CPU + {280AEE2F-1FDB-4A27-BE37-14DC154C873B}.Release|x86.Build.0 = Release|Any CPU + {54835857-129F-44C9-B529-A42158647B36}.commercial_64|Any CPU.ActiveCfg = Release|Any CPU + {54835857-129F-44C9-B529-A42158647B36}.commercial_64|Any CPU.Build.0 = Release|Any CPU + {54835857-129F-44C9-B529-A42158647B36}.commercial_64|Mixed Platforms.ActiveCfg = Release|x86 + {54835857-129F-44C9-B529-A42158647B36}.commercial_64|Mixed Platforms.Build.0 = Release|x86 + {54835857-129F-44C9-B529-A42158647B36}.commercial_64|x64.ActiveCfg = Release|x64 + {54835857-129F-44C9-B529-A42158647B36}.commercial_64|x64.Build.0 = Release|x64 + {54835857-129F-44C9-B529-A42158647B36}.commercial_64|x86.ActiveCfg = Release|x86 + {54835857-129F-44C9-B529-A42158647B36}.commercial_64|x86.Build.0 = Release|x86 + {54835857-129F-44C9-B529-A42158647B36}.commercial|Any CPU.ActiveCfg = Release|Any CPU + {54835857-129F-44C9-B529-A42158647B36}.commercial|Any CPU.Build.0 = Release|Any CPU + {54835857-129F-44C9-B529-A42158647B36}.commercial|Mixed Platforms.ActiveCfg = Release|x86 + {54835857-129F-44C9-B529-A42158647B36}.commercial|Mixed Platforms.Build.0 = Release|x86 + {54835857-129F-44C9-B529-A42158647B36}.commercial|x64.ActiveCfg = Release|x64 + {54835857-129F-44C9-B529-A42158647B36}.commercial|x64.Build.0 = Release|x64 + {54835857-129F-44C9-B529-A42158647B36}.commercial|x86.ActiveCfg = Release|x86 + {54835857-129F-44C9-B529-A42158647B36}.commercial|x86.Build.0 = Release|x86 + {54835857-129F-44C9-B529-A42158647B36}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {54835857-129F-44C9-B529-A42158647B36}.Debug|Any CPU.Build.0 = Debug|Any CPU + {54835857-129F-44C9-B529-A42158647B36}.Debug|Mixed Platforms.ActiveCfg = Debug|x86 + {54835857-129F-44C9-B529-A42158647B36}.Debug|Mixed Platforms.Build.0 = Debug|x86 + {54835857-129F-44C9-B529-A42158647B36}.Debug|x64.ActiveCfg = Debug|x64 + {54835857-129F-44C9-B529-A42158647B36}.Debug|x64.Build.0 = Debug|x64 + {54835857-129F-44C9-B529-A42158647B36}.Debug|x86.ActiveCfg = Debug|x86 + {54835857-129F-44C9-B529-A42158647B36}.Debug|x86.Build.0 = Debug|x86 + {54835857-129F-44C9-B529-A42158647B36}.Release|Any CPU.ActiveCfg = Release|Any CPU + {54835857-129F-44C9-B529-A42158647B36}.Release|Any CPU.Build.0 = Release|Any CPU + {54835857-129F-44C9-B529-A42158647B36}.Release|Mixed Platforms.ActiveCfg = Release|x86 + {54835857-129F-44C9-B529-A42158647B36}.Release|Mixed Platforms.Build.0 = Release|x86 + {54835857-129F-44C9-B529-A42158647B36}.Release|x64.ActiveCfg = Release|x64 + {54835857-129F-44C9-B529-A42158647B36}.Release|x64.Build.0 = Release|x64 + {54835857-129F-44C9-B529-A42158647B36}.Release|x86.ActiveCfg = Release|x86 + {54835857-129F-44C9-B529-A42158647B36}.Release|x86.Build.0 = Release|x86 + EndGlobalSection + GlobalSection(SolutionProperties) = preSolution + HideSolutionNode = FALSE + EndGlobalSection +EndGlobal