diff --git a/examples/msf/README b/examples/msf/README
deleted file mode 100644
index d6e56f72f..000000000
--- a/examples/msf/README
+++ /dev/null
@@ -1,20 +0,0 @@
-In order to use Z3 MSF plugin, follow the following steps:
-1. Compile latest Z3 .NET API (from any branch consisting of opt features) and copy 'libz3.dll' and 'Microsoft.Z3.dll' to the folder of 'Z3MSFPlugin.sln'.
-2. Retrieve 'Microsoft.Solver.Foundation.dll' from http://archive.msdn.microsoft.com/solverfoundation/Release/ProjectReleases.aspx?ReleaseId=1799,
- preferably using DLL only version. Copy 'Microsoft.Solver.Foundation.dll' to the folder of 'Z3MSFPlugin.sln'
-3. Build 'Z3MSFPlugin.sln'. Note that you have to compile using x86 target for Microsoft.Z3.dll 32-bit and x64 target for Microsoft.Z3.dll 64-bit.
-
-The solution consists of a plugin project, a test project with a few simple test cases and a command line projects for external OML, MPS and SMPS models.
-To retrieve SMT2 models which are native to Z3, set the logging file in corresponding directives or solver params e.g.
-
- var p = new Z3MILPParams();
- p.SMT2LogFile = "model.smt2";
-
-For more details, check out the commands in 'Validator\Program.cs'.
-
-Enjoy!
-
-
-
-
-
\ No newline at end of file
diff --git a/examples/msf/SolverFoundation.Plugin.Z3.Tests/App.config b/examples/msf/SolverFoundation.Plugin.Z3.Tests/App.config
deleted file mode 100644
index 75e2872f1..000000000
--- a/examples/msf/SolverFoundation.Plugin.Z3.Tests/App.config
+++ /dev/null
@@ -1,60 +0,0 @@
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
diff --git a/examples/msf/SolverFoundation.Plugin.Z3.Tests/Properties/AssemblyInfo.cs b/examples/msf/SolverFoundation.Plugin.Z3.Tests/Properties/AssemblyInfo.cs
deleted file mode 100644
index b58f97eda..000000000
--- a/examples/msf/SolverFoundation.Plugin.Z3.Tests/Properties/AssemblyInfo.cs
+++ /dev/null
@@ -1,36 +0,0 @@
-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
deleted file mode 100644
index 196f89245..000000000
--- a/examples/msf/SolverFoundation.Plugin.Z3.Tests/ServiceTests.cs
+++ /dev/null
@@ -1,92 +0,0 @@
-
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
---*/
-
-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
deleted file mode 100644
index 24cecfa10..000000000
--- a/examples/msf/SolverFoundation.Plugin.Z3.Tests/SolverFoundation.Plugin.Z3.Tests.csproj
+++ /dev/null
@@ -1,70 +0,0 @@
-
-
-
-
- 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
deleted file mode 100644
index 4913c0f81..000000000
--- a/examples/msf/SolverFoundation.Plugin.Z3.Tests/SolverTests.cs
+++ /dev/null
@@ -1,138 +0,0 @@
-
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
---*/
-
-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
deleted file mode 100644
index 6ce66fa8f..000000000
--- a/examples/msf/SolverFoundation.Plugin.Z3/AbortWorker.cs
+++ /dev/null
@@ -1,98 +0,0 @@
-
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
---*/
-
-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/App.config b/examples/msf/SolverFoundation.Plugin.Z3/App.config
deleted file mode 100644
index 75e2872f1..000000000
--- a/examples/msf/SolverFoundation.Plugin.Z3/App.config
+++ /dev/null
@@ -1,60 +0,0 @@
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Properties/AssemblyInfo.cs b/examples/msf/SolverFoundation.Plugin.Z3/Properties/AssemblyInfo.cs
deleted file mode 100644
index 6d495a895..000000000
--- a/examples/msf/SolverFoundation.Plugin.Z3/Properties/AssemblyInfo.cs
+++ /dev/null
@@ -1,36 +0,0 @@
-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 2010")]
-[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
deleted file mode 100644
index 0b30e1677..000000000
--- a/examples/msf/SolverFoundation.Plugin.Z3/SolverFoundation.Plugin.Z3.csproj
+++ /dev/null
@@ -1,149 +0,0 @@
-
-
-
- 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
-
-
- 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
- prompt
-
-
- bin\commercial_64\
- TRACE
- true
- pdbonly
- AnyCPU
- prompt
-
-
- 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
-
-
-
- ..\Microsoft.Solver.Foundation.dll
-
-
- False
- ..\Microsoft.Z3.dll
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
\ No newline at end of file
diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Utils.cs b/examples/msf/SolverFoundation.Plugin.Z3/Utils.cs
deleted file mode 100644
index 5930caee1..000000000
--- a/examples/msf/SolverFoundation.Plugin.Z3/Utils.cs
+++ /dev/null
@@ -1,130 +0,0 @@
-
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
---*/
-
-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
deleted file mode 100644
index 199c3fe35..000000000
--- a/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseDirective.cs
+++ /dev/null
@@ -1,107 +0,0 @@
-
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
---*/
-
-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
deleted file mode 100644
index 6d6dd74a7..000000000
--- a/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseParams.cs
+++ /dev/null
@@ -1,109 +0,0 @@
-
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
---*/
-
-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
deleted file mode 100644
index 5297d3e67..000000000
--- a/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs
+++ /dev/null
@@ -1,387 +0,0 @@
-
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
---*/
-
-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 corresponding 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(pair.Value.Upper);
- _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(pair.Value.Upper);
- _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
deleted file mode 100644
index 4d6745634..000000000
--- a/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPDirective.cs
+++ /dev/null
@@ -1,15 +0,0 @@
-
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
---*/
-
-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
deleted file mode 100644
index d01b07725..000000000
--- a/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPParams.cs
+++ /dev/null
@@ -1,25 +0,0 @@
-
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
---*/
-
-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
deleted file mode 100644
index 4f8cdc759..000000000
--- a/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPSolver.cs
+++ /dev/null
@@ -1,236 +0,0 @@
-
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
---*/
-
-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 classes
- public Z3MILPSolver() : base(null)
- {
- _result = LinearResult.Feasible;
- _solver = new Z3BaseSolver(this);
- }
-
- /// Constructor that initializes the base classes
- 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
deleted file mode 100644
index ff9e4181a..000000000
--- a/examples/msf/SolverFoundation.Plugin.Z3/Z3TermDirective.cs
+++ /dev/null
@@ -1,15 +0,0 @@
-
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
---*/
-
-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
deleted file mode 100644
index 283bc9362..000000000
--- a/examples/msf/SolverFoundation.Plugin.Z3/Z3TermParams.cs
+++ /dev/null
@@ -1,23 +0,0 @@
-
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
---*/
-
-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
deleted file mode 100644
index de91c7b6e..000000000
--- a/examples/msf/SolverFoundation.Plugin.Z3/Z3TermSolver.cs
+++ /dev/null
@@ -1,388 +0,0 @@
-
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
---*/
-
-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 classes
- public Z3TermSolver() : base(null)
- {
- _solver = new Z3BaseSolver(this);
- }
-
- /// Constructor that initializes the base classes
- 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
deleted file mode 100644
index 75e2872f1..000000000
--- a/examples/msf/Validator/App.config
+++ /dev/null
@@ -1,60 +0,0 @@
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
diff --git a/examples/msf/Validator/MicrosoftSolverFoundationForExcel.dll.config b/examples/msf/Validator/MicrosoftSolverFoundationForExcel.dll.config
deleted file mode 100644
index cd9dcad25..000000000
--- a/examples/msf/Validator/MicrosoftSolverFoundationForExcel.dll.config
+++ /dev/null
@@ -1,58 +0,0 @@
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
diff --git a/examples/msf/Validator/Program.cs b/examples/msf/Validator/Program.cs
deleted file mode 100644
index 8afb28af5..000000000
--- a/examples/msf/Validator/Program.cs
+++ /dev/null
@@ -1,200 +0,0 @@
-
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
---*/
-
-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
deleted file mode 100644
index eb2f8ed71..000000000
--- a/examples/msf/Validator/Properties/AssemblyInfo.cs
+++ /dev/null
@@ -1,36 +0,0 @@
-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
deleted file mode 100644
index cfea3c80b..000000000
--- a/examples/msf/Validator/Validator.csproj
+++ /dev/null
@@ -1,123 +0,0 @@
-
-
-
- Debug
- AnyCPU
- 9.0.21022
- 2.0
- {54835857-129F-44C9-B529-A42158647B36}
- Exe
- Properties
- Validator
- Validator
- v4.0
- 512
- 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
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- {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
deleted file mode 100644
index c3af1dc22..000000000
--- a/examples/msf/Z3MSFPlugin.sln
+++ /dev/null
@@ -1,125 +0,0 @@
-
-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
-Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Solution Items", "Solution Items", "{F1E99540-BA5E-46DF-9E29-6146A309CD18}"
- ProjectSection(SolutionItems) = preProject
- README = README
- EndProjectSection
-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
diff --git a/src/ast/converters/generic_model_converter.cpp b/src/ast/converters/generic_model_converter.cpp
index 9adb9ee4b..1e81f9131 100644
--- a/src/ast/converters/generic_model_converter.cpp
+++ b/src/ast/converters/generic_model_converter.cpp
@@ -38,7 +38,7 @@ void generic_model_converter::operator()(model_ref & md) {
TRACE("model_converter", tout << "before generic_model_converter\n"; model_v2_pp(tout, *md); display(tout););
model_evaluator ev(*(md.get()));
- ev.set_model_completion(true);
+ ev.set_model_completion(m_completion);
ev.set_expand_array_equalities(false);
expr_ref val(m);
unsigned arity;
@@ -78,7 +78,7 @@ void generic_model_converter::operator()(model_ref & md) {
}
if (reset_ev) {
ev.reset();
- ev.set_model_completion(true);
+ ev.set_model_completion(m_completion);
ev.set_expand_array_equalities(false);
}
break;
diff --git a/src/ast/converters/model_converter.h b/src/ast/converters/model_converter.h
index 164becc09..720324919 100644
--- a/src/ast/converters/model_converter.h
+++ b/src/ast/converters/model_converter.h
@@ -64,14 +64,17 @@ class smt2_pp_environment;
class model_converter : public converter {
protected:
- smt2_pp_environment* m_env;
+ smt2_pp_environment* m_env = nullptr;
+ bool m_completion = true;
static void display_add(std::ostream& out, smt2_pp_environment& env, ast_manager& m, func_decl* f, expr* e);
void display_add(std::ostream& out, ast_manager& m, func_decl* f, expr* e) const;
void display_del(std::ostream& out, func_decl* f) const;
void display_add(std::ostream& out, ast_manager& m);
public:
- model_converter(): m_env(nullptr) {}
+ model_converter() {}
+
+ void set_completion(bool f) { m_completion = f; }
virtual void operator()(model_ref & m) = 0;
diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
index a05fbc68d..6c2f4038f 100644
--- a/src/smt/theory_array_base.cpp
+++ b/src/smt/theory_array_base.cpp
@@ -529,7 +529,7 @@ namespace smt {
// issue #3532, #3529
//
if (ctx.is_shared(r) || is_select_arg(r)) {
- TRACE("array", tout << "new shared var: #" << r->get_owner_id() << "\n";);
+ TRACE("array", tout << "new shared var: #" << r->get_owner_id() << " " << is_select_arg(r) << "\n";);
theory_var r_th_var = r->get_th_var(get_id());
SASSERT(r_th_var != null_theory_var);
result.push_back(r_th_var);