diff --git a/CatSAT.sln.DotSettings b/CatSAT.sln.DotSettings index d5503c3..504e98c 100644 --- a/CatSAT.sln.DotSettings +++ b/CatSAT.sln.DotSettings @@ -6,6 +6,9 @@ True True True + True + True + True True True @@ -16,4 +19,12 @@ True True True - True \ No newline at end of file + True + + True + True + True + True + True + True + True \ No newline at end of file diff --git a/CatSAT/CatSAT.csproj b/CatSAT/CatSAT.csproj index c2332e7..775e192 100644 --- a/CatSAT/CatSAT.csproj +++ b/CatSAT/CatSAT.csproj @@ -43,6 +43,9 @@ + + ..\packages\System.ValueTuple.4.5.0\lib\netstandard1.0\System.ValueTuple.dll + @@ -55,6 +58,7 @@ + @@ -114,6 +118,7 @@ + SettingsSingleFileGenerator Settings.Designer.cs diff --git a/CatSAT/NonBoolean/SMT/Float/BinarySumConstraint.cs b/CatSAT/NonBoolean/SMT/Float/BinarySumConstraint.cs index 3fce1bb..269d3f5 100644 --- a/CatSAT/NonBoolean/SMT/Float/BinarySumConstraint.cs +++ b/CatSAT/NonBoolean/SMT/Float/BinarySumConstraint.cs @@ -50,6 +50,7 @@ public override void Initialize(Problem p) rhs = (FloatVariable)c.Args[2]; lhs.AddFunctionalConstraint(this); rhs.AddFunctionalConstraint(this); + Result.PickLast = true; base.Initialize(p); } diff --git a/CatSAT/NonBoolean/SMT/Float/FloatDomain.cs b/CatSAT/NonBoolean/SMT/Float/FloatDomain.cs index b9ae536..be64424 100644 --- a/CatSAT/NonBoolean/SMT/Float/FloatDomain.cs +++ b/CatSAT/NonBoolean/SMT/Float/FloatDomain.cs @@ -22,6 +22,9 @@ // // -------------------------------------------------------------------------------------------------------------------- #endregion + +using System; + namespace CatSAT.NonBoolean.SMT.Float { /// @@ -34,6 +37,44 @@ public class FloatDomain : Domain /// The upper and lower bounds of the domain /// public readonly Interval Bounds; + + /// + /// If non-zero, domain consists of only integer multiples of quantization. + /// + public float Quantization; + + /// + /// True if num is a valid element of the domain. + /// + public bool Contains(float num) + { + return ((Bounds.Contains(num)) && (Quantization == 0 || IsQuantized(num, Quantization))); + } + + /// + /// True if num is an integer multiple of quantization. + /// + public bool IsQuantized(float num, float quantization) + { + var quotient = num / quantization; + var rounded = Math.Round(quotient); + var error = Math.Abs(quotient - rounded); + return (error < 0.0001f); + } + + /// + /// A floating-point domain, specified by upper- and lower-bounds + /// + /// Name of the variable + /// Lower bound of the variable + /// Upper bound of the variable + /// If non-zero, include only integer multiples of quantization + public FloatDomain(string name, float lowerBound, float upperBound, float quantization) : base(name) + { + Bounds = new Interval(lowerBound, upperBound); + Quantization = quantization; + } + /// /// A floating-point domain, specified by upper- and lower-bounds /// @@ -50,5 +91,87 @@ public override Variable Instantiate(object name, Problem p, Literal condition = { return new FloatVariable(name, this, condition, p); } + + /// + /// A FloatDomain constrained to be the sum of two other FloatDomains + /// + public static FloatDomain operator +(FloatDomain d1, FloatDomain d2) + { + // ReSharper disable once CompareOfFloatsByEqualityOperator + if (d1.Quantization != d2.Quantization) + { + throw new ArgumentException("Can't add float domains with different quantizations"); + } + + else if (d1.Quantization == 0 && d2.Quantization == 0) + { + var sum = new FloatDomain($"{d1.Name}+{d2.Name}", d1.Bounds.Lower + d2.Bounds.Lower, + d1.Bounds.Upper + d2.Bounds.Upper); + return sum; + } + + else + { + var sum = new FloatDomain($"{d1.Name}+{d2.Name}", d1.Bounds.Lower + d2.Bounds.Lower, + d1.Bounds.Upper + d2.Bounds.Upper) {Quantization = d1.Quantization}; + return sum; + } + } + + /// + /// A FloatDomain constrained to be the difference of two other FloatDomains + /// + public static FloatDomain operator -(FloatDomain d1, FloatDomain d2) + { + // ReSharper disable once CompareOfFloatsByEqualityOperator + if (d1.Quantization != d2.Quantization) + { + throw new ArgumentException("Can't subtract float domains with different quantizations"); + } + + else if (d1.Quantization == 0 && d2.Quantization == 0) + { + var difference = new FloatDomain($"{d1.Name}-{d2.Name}", d1.Bounds.Lower - d2.Bounds.Upper, + d1.Bounds.Upper - d2.Bounds.Lower); + return difference; + } + + else + { + var difference = new FloatDomain($"{d1.Name}-{d2.Name}", d1.Bounds.Lower - d2.Bounds.Upper, + d1.Bounds.Upper - d2.Bounds.Lower) {Quantization = d1.Quantization}; + return difference; + } + } + + /// + /// A FloatDomain constrained to be the product of two other FloatDomains + /// + public static FloatDomain operator *(FloatDomain d1, FloatDomain d2) + { + // ReSharper disable once CompareOfFloatsByEqualityOperator + if (d1.Quantization != d2.Quantization) + { + throw new ArgumentException("Can't multiply float domains with different quantizations"); + } + + else if (d1.Quantization == 0 && d2.Quantization == 0) + { + + var product = new FloatDomain($"{d1.Name}*{d2.Name}", d1.Bounds.Lower * d2.Bounds.Lower, + d1.Bounds.Upper * d2.Bounds.Upper); + return product; + } + + else + { + var product = new FloatDomain($"{d1.Name}*{d2.Name}", d1.Bounds.Lower * d2.Bounds.Lower, + d1.Bounds.Upper * d2.Bounds.Upper) {Quantization = d1.Quantization}; + return product; + } + } + + + } } diff --git a/CatSAT/NonBoolean/SMT/Float/FloatSolver.cs b/CatSAT/NonBoolean/SMT/Float/FloatSolver.cs index fa14b26..10c1815 100644 --- a/CatSAT/NonBoolean/SMT/Float/FloatSolver.cs +++ b/CatSAT/NonBoolean/SMT/Float/FloatSolver.cs @@ -26,6 +26,8 @@ using System.Collections; using System.Collections.Generic; using System.Linq; +using System.Diagnostics; +using static System.Collections.StructuralComparisons; namespace CatSAT.NonBoolean.SMT.Float { @@ -38,8 +40,20 @@ class FloatSolver : TheorySolver // Representatives of the equivalence classes of FloatVariables private readonly List representatives = new List(); + /// + /// (v, true) in this queue means v's upper bound has recently been tightened; (v, false) means v's lower bound has recently been tightened. + /// private readonly Queue> propagationQueue = new Queue>(); + public Dictionary<(FloatVariable, FloatVariable), FloatVariable> ProductTable = new Dictionary<(FloatVariable, FloatVariable), FloatVariable>(); + public Dictionary<(FloatVariable, FloatVariable), FloatVariable> SumTable = new Dictionary<(FloatVariable, FloatVariable), FloatVariable>(); + public Dictionary SquareTable = new Dictionary(); + public Dictionary ArraySumTable = new Dictionary(FloatVariableArrayComparer.EqualityComparer); + public Dictionary AverageTable = new Dictionary(FloatVariableArrayComparer.EqualityComparer); + public Dictionary<(Interval, FloatVariable[]), FloatVariable> ConstrainedAverageTable = new Dictionary<(Interval, FloatVariable[]), FloatVariable>(); + public Dictionary VarianceTable = new Dictionary(FloatVariableArrayComparer.EqualityComparer); + public Dictionary<(Interval, FloatVariable[]), FloatVariable> ConstrainedVarianceTable = new Dictionary<(Interval, FloatVariable[]), FloatVariable>(); + /// /// Add clauses that follow from user-defined bounds, e.g. from transitivity. /// @@ -50,7 +64,7 @@ void PreprecessBounds(List constraints, int sign) { foreach (var p in Propositions) p.Validate(); - constraints.Sort((a, b) => sign*Comparer.Default.Compare(a.Bound, b.Bound)); + constraints.Sort((a, b) => sign * Comparer.Default.Compare(a.Bound, b.Bound)); // Add forward inferences: if v < bounds[i], then v < bounds[i+1] for (int i = 0; i < constraints.Count - 1; i++) @@ -70,10 +84,10 @@ void PreprecessBounds(List constraints, int sign) // way it's possible for them to be unsatisfied with non-zero probability is through // floating-point quantization. That suggests that someone trying to make a proposition // dependent on a != b+C is probably making a mistake. - if (v.AllFunctionalConstraints != null) - foreach (var f in v.AllFunctionalConstraints) - if (f.IsDependency) - throw new InvalidOperationException($"{f.Name}: Inferences dependent on the truth of functional constraint are not supported."); + //if (v.AllFunctionalConstraints != null) + // foreach (var f in v.AllFunctionalConstraints) + // if (f.IsDependency) + // throw new InvalidOperationException($"{f.Name}: Inferences dependent on the truth of functional constraint are not supported."); } return null; @@ -114,7 +128,7 @@ public override bool Solve(Solution s) FindEquivalenceClasses(s); FindActiveFunctionalConstraints(s); - if (!FindSolutionBounds(s)) + if (!FindSolutionBounds(s)) // Constraint are contradictory return false; @@ -150,6 +164,7 @@ private void FindEquivalenceClasses(Solution s) // We can now focus on just the representatives of each equivalence class of variables // and ignore the rest. representatives.Clear(); + // ReSharper disable once RedundantCast representatives.AddRange(Variables.Where(v => v.IsDefinedInInternal(s) && (object) v == (object) v.Representative)); } @@ -246,7 +261,9 @@ private bool FindSolutionBounds(Solution s) // Save bounds foreach (var v in representatives) + { v.SolutionBounds = v.Bounds; + } return true; } @@ -262,11 +279,39 @@ private void ResetAll() private bool TrySample() { Random.Shuffle(representatives); + var end = representatives.Count - 1; + for (var i = 0; i < end; i++) + { + if (representatives[i].PickLast) + { + var temp = representatives[end]; + representatives[end] = representatives[i]; + representatives[i] = temp; + } + } + foreach (var v in representatives) { - v.PickRandom(propagationQueue); + if (v.FloatDomain.Quantization == 0) + { + + v.PickValue(Random.Float(v.Bounds.Lower, v.Bounds.Upper), propagationQueue); + } + + else + { + int possibilities = (int)((v.Bounds.Upper - v.Bounds.Lower) / v.FloatDomain.Quantization); + + // ReSharper disable once RedundantNameQualifier + int randStep = CatSAT.Random.InRange(0, possibilities); + + float rand = randStep * v.FloatDomain.Quantization + v.Bounds.Lower; + + v.PickValue(rand, propagationQueue); + } + if (!PropagateUpdates()) - return false; + return false; } return true; diff --git a/CatSAT/NonBoolean/SMT/Float/FloatVariable.cs b/CatSAT/NonBoolean/SMT/Float/FloatVariable.cs index e526bda..389d77a 100644 --- a/CatSAT/NonBoolean/SMT/Float/FloatVariable.cs +++ b/CatSAT/NonBoolean/SMT/Float/FloatVariable.cs @@ -22,10 +22,12 @@ // // -------------------------------------------------------------------------------------------------------------------- #endregion + using System; using System.Collections.Generic; using System.Diagnostics; using System.Globalization; +using System.Linq; using CatSAT.NonBoolean.SMT.Float; namespace CatSAT @@ -77,15 +79,22 @@ public FloatVariable(object name, float low, float high, Literal condition) /// public override Domain Domain => FloatDomain; + /// + /// If non-zero, interval consists of only integer multiples of quantization + /// + public float Quantization => FloatDomain.Quantization; + /// /// Saved bounds for current SMT Solution, after initial constraint processing, but before sampling /// internal Interval SolutionBounds; + // ReSharper disable once InconsistentNaming + /// /// Current bounds to which the variable has been narrowed /// - internal Interval Bounds; + internal Interval Bounds { get; set; } /// /// The predetermined value for the variable, if any. @@ -138,12 +147,17 @@ internal static void Equate(FloatVariable v1, FloatVariable v2) /// internal readonly int Index; + /// + /// If true, result of an operation to be propagated last by solver. + /// + internal bool PickLast; + private string DebugValueString => Bounds.IsUnique ? Bounds.Lower.ToString(CultureInfo.InvariantCulture) : Bounds.ToString(); - internal bool PickRandom(Queue> q) + internal void PickValue(float r, Queue> q) { - var f = Random.Float(Bounds.Lower, Bounds.Upper); - return BoundAbove(f, q) && BoundBelow(f, q); + var success = BoundAbove(r, q, false) && BoundBelow(r, q, false); + Debug.Assert(success); } /// @@ -174,7 +188,7 @@ public override void Reset() internal void ResetSolverState() { - Bounds = PredeterminedValueInternal == null ? FloatDomain.Bounds : new Interval(PredeterminedValueInternal.Value); + Bounds = Interval.Quantize(PredeterminedValueInternal == null ? FloatDomain.Bounds : new Interval(PredeterminedValueInternal.Value), Quantization); equivalence = null; UpperVariableBounds?.Clear(); LowerVariableBounds?.Clear(); @@ -189,8 +203,15 @@ internal void ResetSolverState() /// True is resulting bounds are consistent internal bool BoundAbove(float bound) { + Debug.Assert(!float.IsNaN(bound)); + if (Quantization != 0) + { + bound = Interval.RoundDown(bound, Quantization); + } if (!(bound < Bounds.Upper)) return true; - Bounds.Upper = bound; + var b = Bounds; + b.Upper = bound; + Bounds = b; return Bounds.IsNonEmpty; } @@ -202,8 +223,18 @@ internal bool BoundAbove(float bound) /// True is resulting bounds are consistent internal bool BoundBelow(float bound) { + Debug.Assert(!float.IsNaN(bound)); + if (Quantization != 0) + { + bound = Interval.RoundUp(bound, Quantization); + } if (!(bound > Bounds.Lower)) return true; - Bounds.Lower = bound; + if (!(bound > Bounds.Upper)) + { + var b = Bounds; + b.Lower = bound; + Bounds = b; + } return Bounds.IsNonEmpty; } @@ -213,11 +244,19 @@ internal bool BoundBelow(float bound) /// /// Upper bound on variable /// Propagation queue + /// Specifies if the bound should be rounded down to the nearest quantized value. /// True is resulting bounds are consistent - internal bool BoundAbove(float bound, Queue> q) + internal bool BoundAbove(float bound, Queue> q, bool requantize = true) { + Debug.Assert(!float.IsNaN(bound)); + if (Quantization != 0 && requantize) + { + bound = Interval.RoundDown(bound, Quantization); + } if (!(bound < Bounds.Upper)) return true; - Bounds.Upper = bound; + var b = Bounds; + b.Upper = bound; + Bounds = b; EnsurePresent(q, new Tuple(this, true)); return Bounds.IsNonEmpty; } @@ -234,81 +273,81 @@ public bool NarrowTo(Interval i, Queue> q) return BoundAbove(i.Upper, q) && BoundBelow(i.Lower, q); } -// public bool NarrowToQuotient(Interval numerator, Interval denominator, Queue> q) -// { -// if (denominator.IsZero) -// // Denominator is [0,0], so quotient is the empty set unless numerator contains zero -// return numerator.ContainsZero; - -// if (numerator.IsZero) -// { -// if (!denominator.ContainsZero) -// // Quotient is [0,0]. -// if (!NarrowTo(new Interval(0,0), q)) -// return false; -// // Denominator contains zero so quotient can be any value. -// return true; -// } - -// if (!denominator.ContainsZero) -// return NarrowTo(numerator * denominator.Reciprocal, q); - -// // Denominator contains zero, so there are three cases: crossing zero, [0, b], and [a, 0] - -//// ReSharper disable CompareOfFloatsByEqualityOperator -// if (denominator.Lower == 0) -//// ReSharper restore CompareOfFloatsByEqualityOperator -// { -// // Non-negative denominator -// if (numerator.Upper <= 0) -// return NarrowTo(new Interval(float.NegativeInfinity, numerator.Upper / denominator.Upper), q); - -// if (numerator.Lower >= 0) -// return NarrowTo(new Interval(numerator.Lower / denominator.Upper, float.PositiveInfinity), q); -// // Numerator crosses zero, so quotient is all the Reals, so can't narrow interval. -// return true; -// } - -//// ReSharper disable CompareOfFloatsByEqualityOperator -// if (denominator.Upper == 0) -//// ReSharper restore CompareOfFloatsByEqualityOperator -// { -// // Non-positive denominator -// if (numerator.Upper <= 0) -// return NarrowTo(new Interval(numerator.Upper / denominator.Lower, float.PositiveInfinity), q); - -// if (numerator.Lower >= 0) -// return NarrowTo(new Interval(float.NegativeInfinity, numerator.Lower / denominator.Lower), q); -// // Numerator crosses zero, so quotient is all the Reals, so can't narrow interval. -// return true; -// } - -// if (numerator.Upper < 0) -// { -// // Strictly negative -// var lowerHalf = new Interval(float.NegativeInfinity, numerator.Upper / denominator.Upper); -// var upperHalf = new Interval(numerator.Upper / denominator.Lower, float.PositiveInfinity); -// return NarrowToUnion(lowerHalf, upperHalf, q); -// } - -// // Denominator crosses zero -// if (numerator.Lower > 0) -// { -// // Strictly positive -// var lowerHalf = new Interval(float.NegativeInfinity, numerator.Lower / denominator.Lower); -// var upperHalf = new Interval(numerator.Lower / denominator.Upper, float.PositiveInfinity); - -// return NarrowToUnion(lowerHalf, upperHalf, q); -// } - -// // Numerator contains zero, so quotient is all the Reals, so can't narrow interval. -// return true; -// } - -// public bool NarrowToUnion(Interval a, Interval b, Queue> q) -// { -// return NarrowTo(Interval.UnionOfIntersections(Bounds, a, b), q); -// } + // public bool NarrowToQuotient(Interval numerator, Interval denominator, Queue> q) + // { + // if (denominator.IsZero) + // // Denominator is [0,0], so quotient is the empty set unless numerator contains zero + // return numerator.ContainsZero; + + // if (numerator.IsZero) + // { + // if (!denominator.ContainsZero) + // // Quotient is [0,0]. + // if (!NarrowTo(new Interval(0,0), q)) + // return false; + // // Denominator contains zero so quotient can be any value. + // return true; + // } + + // if (!denominator.ContainsZero) + // return NarrowTo(numerator * denominator.Reciprocal, q); + + // // Denominator contains zero, so there are three cases: crossing zero, [0, b], and [a, 0] + + //// ReSharper disable CompareOfFloatsByEqualityOperator + // if (denominator.Lower == 0) + //// ReSharper restore CompareOfFloatsByEqualityOperator + // { + // // Non-negative denominator + // if (numerator.Upper <= 0) + // return NarrowTo(new Interval(float.NegativeInfinity, numerator.Upper / denominator.Upper), q); + + // if (numerator.Lower >= 0) + // return NarrowTo(new Interval(numerator.Lower / denominator.Upper, float.PositiveInfinity), q); + // // Numerator crosses zero, so quotient is all the Reals, so can't narrow interval. + // return true; + // } + + //// ReSharper disable CompareOfFloatsByEqualityOperator + // if (denominator.Upper == 0) + //// ReSharper restore CompareOfFloatsByEqualityOperator + // { + // // Non-positive denominator + // if (numerator.Upper <= 0) + // return NarrowTo(new Interval(numerator.Upper / denominator.Lower, float.PositiveInfinity), q); + + // if (numerator.Lower >= 0) + // return NarrowTo(new Interval(float.NegativeInfinity, numerator.Lower / denominator.Lower), q); + // // Numerator crosses zero, so quotient is all the Reals, so can't narrow interval. + // return true; + // } + + // if (numerator.Upper < 0) + // { + // // Strictly negative + // var lowerHalf = new Interval(float.NegativeInfinity, numerator.Upper / denominator.Upper); + // var upperHalf = new Interval(numerator.Upper / denominator.Lower, float.PositiveInfinity); + // return NarrowToUnion(lowerHalf, upperHalf, q); + // } + + // // Denominator crosses zero + // if (numerator.Lower > 0) + // { + // // Strictly positive + // var lowerHalf = new Interval(float.NegativeInfinity, numerator.Lower / denominator.Lower); + // var upperHalf = new Interval(numerator.Lower / denominator.Upper, float.PositiveInfinity); + + // return NarrowToUnion(lowerHalf, upperHalf, q); + // } + + // // Numerator contains zero, so quotient is all the Reals, so can't narrow interval. + // return true; + // } + + // public bool NarrowToUnion(Interval a, Interval b, Queue> q) + // { + // return NarrowTo(Interval.UnionOfIntersections(Bounds, a, b), q); + // } /// /// Adds the specified (variable, IsUpper) task to queue if it is not already present. @@ -325,11 +364,21 @@ private void EnsurePresent(Queue> q, Tuple /// Lower bound on variable /// Propagation queue + /// Specifies if the bound should be rounded down to the nearest quantized value. /// True is resulting bounds are consistent - internal bool BoundBelow(float bound, Queue> q) + internal bool BoundBelow(float bound, Queue> q, bool requantize = true) { - if (!(bound > Bounds.Lower)) return true; - Bounds.Lower = bound; + Debug.Assert(!float.IsNaN(bound)); + if (Quantization != 0 && requantize) + { + bound = Interval.RoundUp(bound, Quantization); + } + if (!(bound > Bounds.Lower)) { + return true; + } + var b = Bounds; + b.Lower = bound; + Bounds = b; EnsurePresent(q, new Tuple(this, false)); return Bounds.IsNonEmpty; } @@ -405,10 +454,17 @@ internal bool BoundBelow(float bound, Queue> q) /// public static FloatVariable operator +(FloatVariable v1, FloatVariable v2) { + var sumTable = Problem.Current.GetSolver().SumTable; + if (sumTable.TryGetValue((v1, v2), out FloatVariable val)) + { + return val; + } + var sum = new FloatVariable($"{v1.Name}+{v2.Name}", - v1.FloatDomain.Bounds.Lower+v2.FloatDomain.Bounds.Lower, - v1.FloatDomain.Bounds.Upper+v2.FloatDomain.Bounds.Upper, - FunctionalConstraint.CombineConditions(v1.Condition, v2.Condition)); + v1.FloatDomain.Bounds.Lower + v2.FloatDomain.Bounds.Lower, + v1.FloatDomain.Bounds.Upper + v2.FloatDomain.Bounds.Upper, + FunctionalConstraint.CombineConditions(v1.Condition, v2.Condition)) {PickLast = true}; + sumTable[(v1, v2)] = sum; Problem.Current.Assert(Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, "IsSum", sum, v1, v2))); return sum; } @@ -418,13 +474,65 @@ internal bool BoundBelow(float bound, Queue> q) /// public static FloatVariable operator *(FloatVariable v1, FloatVariable v2) { + var productTable = Problem.Current.GetSolver().ProductTable; + if (productTable.TryGetValue((v1, v2), out FloatVariable val)) + { + return val; + } var range = v1.FloatDomain.Bounds * v2.FloatDomain.Bounds; - var product = new FloatVariable($"{v1.Name}*{v2.Name}", range.Lower, range.Upper, - FunctionalConstraint.CombineConditions(v1.Condition, v2.Condition)); + var product = new FloatVariable($"{v1.Name}*{v2.Name}", range.Lower, range.Upper, FunctionalConstraint.CombineConditions(v1.Condition, v2.Condition)); + productTable[(v1, v2)] = product; Problem.Current.Assert(Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, "IsProduct", product, v1, v2))); return product; } + /// + /// A FloatVariable constrained to be the difference between two other FloatVariables + /// + public static FloatVariable operator -(FloatVariable v1, FloatVariable v2) + { + var range = v1.FloatDomain - v2.FloatDomain; + var difference = new FloatVariable($"{v1.Name}-{v2.Name}", range.Bounds.Lower, range.Bounds.Upper, + FunctionalConstraint.CombineConditions(v1.Condition, v2.Condition)) {PickLast = true}; + Problem.Current.Assert(Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, "IsSum", v1, v2, difference))); + return difference; + } + + + + /// + /// A FloatVariable constrained to be the quotient of two other FloatVariables + /// + public static FloatVariable operator /(FloatVariable v1, FloatVariable v2) + { + var range = v1.FloatDomain.Bounds / v2.FloatDomain.Bounds; + var quotient = new FloatVariable($"{v1.Name}/{v2.Name}", range.Lower, range.Upper, FunctionalConstraint.CombineConditions(v1.Condition, v2.Condition)); + Problem.Current.Assert(Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, "IsProduct", v1, v2, quotient))); + return quotient; + } + + /// + /// A FloatVariable constrained to be the quotient of another FloatVariable and a constant + /// + public static FloatVariable operator /(float c, FloatVariable v) + { + return MonotoneFunctionConstraint.MonotoneFunction($"/{v}", x => c/x, y => c / (1 / y/c), false, v); + } + + /// + /// A FloatVariable constrained to be the quotient of another FloatVariable and a constant + /// + public static FloatVariable operator /(FloatVariable v, float c) + { + if (c==0) + { + throw new InvalidOperationException("Cannot divide by 0"); + } + + return MonotoneFunctionConstraint.MonotoneFunction($"/{c}", x => x * (1 / c), y => y / (1 / c), c>0, v); + + } + /// /// A FloatVariable constrained to be the product of another FloatVariable and a constant /// @@ -432,7 +540,7 @@ internal bool BoundBelow(float bound, Queue> q) { return MonotoneFunctionConstraint.MonotoneFunction($"*{c}", x => x * c, y => y / c, c > 0, v); } - + /// /// A FloatVariable constrained to be the product of another FloatVariable and a constant /// @@ -442,21 +550,139 @@ internal bool BoundBelow(float bound, Queue> q) } /// - /// The sum of a set of float variables + /// A FloatVariable constrained to be the power of another FloatVariable and a constant /// - /// set of variables to sum - /// Variable constrained to be the sum of vars - /// When one of the variables has a condition on its existence - public static FloatVariable Sum(params FloatVariable[] vars) + public static FloatVariable operator ^(FloatVariable v, uint c) { - var domainBounds = Interval.Zero; + if ((c % 2 != 0) || (c%2==0 && v.Bounds.Lower >=0)) + { + return MonotoneFunctionConstraint.MonotoneFunction($"^{c}", x => (float)Math.Pow(x, c), + y => + { + if (y < 0) + { + return (float)-Math.Pow(-y, 1.0 / c); + } + + return (float)Math.Pow(y, 1.0 / c); + }, c > 0, v); + } + + if (c % 2 == 0 && v.Bounds.Upper < 0) + { + return MonotoneFunctionConstraint.MonotoneFunction($"^{c}", x => (float)Math.Pow(x, c), y => (float)-Math.Pow(y, 1.0 / c), false, v); + } + + var pow = new FloatVariable($"{v.Name}^{c}", 0, v.FloatDomain.Bounds.Upper, + FunctionalConstraint.CombineConditions(v.Condition, v.Condition)) {PickLast = true}; + + + Problem.Current.Assert(Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, "IsPower", pow, v, c))); + return pow; + } + + /// + /// A FloatVariable constrained to be the difference of another FloatVariable and a constant + /// + public static FloatVariable operator -(float c, FloatVariable v) + { + return MonotoneFunctionConstraint.MonotoneFunction($"-{v}", x => c - x, y => c - y, false, v); + } + + /// + /// A FloatVariable constrained to be the difference of another FloatVariable and a constant + /// + public static FloatVariable operator -(FloatVariable v, float c) + { + return MonotoneFunctionConstraint.MonotoneFunction($"-{c}", x => x - c, y => y + c, true, v); + } + + /// + /// A FloatVariable constrained to be the sum of another FloatVariable and a constant + /// + public static FloatVariable operator +(FloatVariable v, float c) + { + return MonotoneFunctionConstraint.MonotoneFunction($"+{c}", x => x + c, y => y - c, true, v); + } + + /// + /// A FloatVariable constrained to be the sum of another FloatVariable and a constant + /// + public static FloatVariable operator +(float c, FloatVariable v) + { + return v+c; + } + + /// + /// A FloatVariable constrained to be the square of another FloatVariable + /// + public static FloatVariable Square(FloatVariable v1) + { + var squareTable = Problem.Current.GetSolver().SquareTable; + if (squareTable.TryGetValue(v1, out FloatVariable val)) + { + return val; + } + + var lowerSq = v1.FloatDomain.Bounds.Lower * v1.FloatDomain.Bounds.Lower; + var upperSq = v1.FloatDomain.Bounds.Upper * v1.FloatDomain.Bounds.Upper; + + if (v1.FloatDomain.Bounds.Lower < 0 && v1.FloatDomain.Bounds.Upper > 0) + { + var square = new FloatVariable($"{v1.Name}^2", 0, Math.Max(lowerSq, upperSq), FunctionalConstraint.CombineConditions(v1.Condition, v1.Condition)); + squareTable[v1] = square; + Problem.Current.Assert(Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, "IsProduct", square, v1, v1))); + return square; + } + + if (v1.FloatDomain.Bounds.Upper <= 0) + { + var square = new FloatVariable($"{v1.Name}^2", upperSq, lowerSq, FunctionalConstraint.CombineConditions(v1.Condition, v1.Condition)); + squareTable[v1] = square; + Problem.Current.Assert(Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, "IsProduct", square, v1, v1))); + return square; + } + + else + { + var square = new FloatVariable($"{v1.Name}^2", lowerSq, upperSq, FunctionalConstraint.CombineConditions(v1.Condition, v1.Condition)); + squareTable[v1] = square; + Problem.Current.Assert(Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, "IsProduct", square, v1, v1))); + return square; + } + } + + /// + /// The sum of a set of float variables + /// + /// set of variables to sum + /// Variable constrained to be the sum of vars + /// When one of the variables has a condition on its existence + public static FloatVariable Sum(params FloatVariable[] vars) + { + var newDomain = Interval.Zero; + var arraySumTable = Problem.Current.GetSolver().ArraySumTable; + + if (arraySumTable.TryGetValue(vars, out FloatVariable s)) + { + return s; + } + foreach (var a in vars) - domainBounds += a.FloatDomain.Bounds; + { + newDomain += a.FloatDomain.Bounds.Quantize(vars[0].Quantization); + } + foreach (var a in vars) - if (!ReferenceEquals(a.Condition,null)) + if (!ReferenceEquals(a.Condition, null)) throw new ArgumentException("Sum does not support conditioned variables", a.Name.ToString()); - var sum = new FloatVariable("sum", domainBounds.Lower, domainBounds.Upper, null); - Problem.Current.Assert(Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, "IsSum", sum, 1.0f, vars))); + + var sum = new FloatVariable("sum", newDomain.Lower, newDomain.Upper, null); + sum.FloatDomain.Quantization = vars[0].Quantization; + arraySumTable[vars] = sum; + Problem.Current.Assert( + Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, "IsSum", + sum, 1.0f, vars))); return sum; } @@ -468,18 +694,184 @@ public static FloatVariable Sum(params FloatVariable[] vars) /// When one of the vars has a condition on it (i.e. isn't defined in all models) public static FloatVariable Average(params FloatVariable[] vars) { - var domainBounds = Interval.Zero; + var newInter = Interval.Zero; + + var averageTable = Problem.Current.GetSolver().AverageTable; + var arraySumTable = Problem.Current.GetSolver().ArraySumTable; + + if (averageTable.TryGetValue(vars, out FloatVariable avg)) + { + return avg; + } + + if (arraySumTable.TryGetValue(vars, out FloatVariable s)) + { + newInter = s.FloatDomain.Bounds; + } + + else + { + foreach (var a in vars) + { + newInter += a.FloatDomain.Bounds.Quantize(vars[0].Quantization); + } + } + + var newDomain = new FloatDomain("sum", newInter.Lower, newInter.Upper); + foreach (var a in vars) - domainBounds += a.FloatDomain.Bounds; + if (!ReferenceEquals(a.Condition, null)) + throw new ArgumentException("Average does not support conditioned variables", a.Name.ToString()); + + var av = new FloatVariable("average", newDomain.Bounds.Lower * 1f / vars.Length, + newDomain.Bounds.Upper * 1f / vars.Length, null); + if (vars[0].Quantization != 0) + { + av.FloatDomain.Quantization = (vars[0].Quantization * 1f / vars.Length); + } + + averageTable[vars] = av; + + Problem.Current.Assert( + Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, + "IsAverage", av, 1.0f / vars.Length, vars))); + + return av; + } + + /// + /// Computes the average value of the specified FloatVariables + /// + /// Interval for average must be constrained between + /// Variables to average + /// A new FloatVariable constrained to be the average of vars, within the bounds of constraint + /// When one of the vars has a condition on it (i.e. isn't defined in all models) + public static FloatVariable Average(Interval constraint, params FloatVariable[] vars) + { + var newInter = Interval.Zero; + var arraySumTable = Problem.Current.GetSolver().ArraySumTable; + var constrainedAverageTable = Problem.Current.GetSolver().ConstrainedAverageTable; + + if (constrainedAverageTable.TryGetValue((constraint, vars), out FloatVariable avg)) + { + return avg; + } + + if (arraySumTable.TryGetValue(vars, out FloatVariable s)) + { + newInter = s.FloatDomain.Bounds; + } + + else + { + foreach (var a in vars) + { + newInter += a.FloatDomain.Bounds.Quantize(vars[0].Quantization); + } + } + foreach (var a in vars) - if (!ReferenceEquals(a.Condition,null)) + if (!ReferenceEquals(a.Condition, null)) throw new ArgumentException("Average does not support conditioned variables", a.Name.ToString()); - var avg = new FloatVariable("average", - domainBounds.Lower*1f/vars.Length, - domainBounds.Upper*1f/vars.Length, - null); - Problem.Current.Assert(Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, "IsAverage", avg, 1f/vars.Length, vars))); - return avg; + + var newDomain = new FloatDomain("sum", newInter.Lower, newInter.Upper); + + var av = new FloatVariable("average", newDomain.Bounds.Lower * 1f / vars.Length, + newDomain.Bounds.Upper * 1f / vars.Length, null); + + if (vars[0].Quantization != 0) + { + av.FloatDomain.Quantization = (vars[0].Quantization * 1f / vars.Length); + } + + if (av.FloatDomain.Bounds.Upper > constraint.Upper || av.FloatDomain.Bounds.Lower < constraint.Lower) + { + var constrainedInterval = new Interval(av.Bounds.Lower, av.Bounds.Upper); + + if (av.FloatDomain.Bounds.Upper > constraint.Upper) + { + constrainedInterval.Upper = constraint.Upper; + } + + if (av.FloatDomain.Bounds.Lower < constraint.Lower) + { + constrainedInterval.Lower = constraint.Lower; + } + + var constrainedDomain = new FloatDomain("constrained average", constrainedInterval.Lower, constrainedInterval.Upper); + + var constrainedAvg = new FloatVariable("average", constrainedDomain.Bounds.Lower, constrainedDomain.Bounds.Upper, null); + + if (vars[0].Quantization != 0) + { + constrainedAvg.FloatDomain.Quantization = (vars[0].Quantization * 1f / vars.Length); + } + + constrainedAvg.PickLast = true; + + Problem.Current.Assert( + Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, + "IsAverage", constrainedAvg, 1.0f / vars.Length, vars))); + + constrainedAverageTable[(constraint, vars)] = constrainedAvg; + + return constrainedAvg; + } + + Problem.Current.Assert( + Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, + "IsAverage", av, 1.0f / vars.Length, vars))); + + av.PickLast = true; + + constrainedAverageTable[(constraint, vars)] = av; + + return av; + } + + /// + /// Computes the variance of the specified FloatVariables + /// + /// Variables to find variance of + /// A new FloatVariable constrained to be the variance of vars + /// When one of the vars has a condition on it (i.e. isn't defined in all models) + public static FloatVariable Variance(params FloatVariable[] vars) + { + var varianceTable = Problem.Current.GetSolver().VarianceTable; + + if (varianceTable.TryGetValue(vars, out FloatVariable vari)) + { + return vari; + } + + var mean = Average(vars); + var variance = Average(vars.Select(v => (v - mean)^2 ).ToArray()); + varianceTable[vars] = variance; + variance.PickLast = true; + return variance; + } + + /// + /// Computes the variance of the specified FloatVariables + /// + /// Interval for average to be constrained between + /// Interval for variance to be constrained between + /// Variables to find average and variance of + /// A new FloatVariable constrained to be the variance of vars, within the bounds of constraint + /// When one of the vars has a condition on it (i.e. isn't defined in all models) + public static FloatVariable Variance(Interval meanRange, Interval varianceRange, params FloatVariable[] vars) + { + var constrainedVarianceTable = Problem.Current.GetSolver().ConstrainedVarianceTable; + + if (constrainedVarianceTable.TryGetValue((varianceRange, vars), out FloatVariable vari)) + { + return vari; + } + + var mean = Average(meanRange, vars); + var variance = Average(varianceRange, vars.Select(v => (v - mean) ^ 2).ToArray()); + constrainedVarianceTable[(varianceRange, vars)] = variance; + return variance; } internal void AddUpperBound(FloatVariable bound) @@ -513,4 +905,50 @@ internal void AddActiveFunctionalConstraint(FunctionalConstraint f) ActiveFunctionalConstraints.Add(f); } } + + /// + /// Compares arrays of FloatVariables in order to check if they are already in a hash table. + /// + public class FloatVariableArrayComparer : IEqualityComparer + { + + /// + /// Singleton instance of the comparer + /// + public static readonly IEqualityComparer EqualityComparer = new FloatVariableArrayComparer(); + + bool IEqualityComparer.Equals(FloatVariable[] a, FloatVariable[] b) + { + if (a != null && b != null) + { + if (a.Length != b.Length) + { + return false; + } + + for (int i = 0; i < a.Length; i++) + { + if (!ReferenceEquals(a[i], b[i])) + { + return false; + } + } + } + + return true; + } + + int IEqualityComparer.GetHashCode(FloatVariable[] array) + { + int aggregate = 0; + // ReSharper disable once ForCanBeConvertedToForeach + for (int i = 0; i < array.Length; i++) + { + int currentHashCode = array[i].GetHashCode(); + aggregate ^= currentHashCode; + } + + return aggregate; + } + } } diff --git a/CatSAT/NonBoolean/SMT/Float/GeneralSumConstraint.cs b/CatSAT/NonBoolean/SMT/Float/GeneralSumConstraint.cs index 0bcb496..81b3794 100644 --- a/CatSAT/NonBoolean/SMT/Float/GeneralSumConstraint.cs +++ b/CatSAT/NonBoolean/SMT/Float/GeneralSumConstraint.cs @@ -43,12 +43,13 @@ class GeneralSumConstraint : FunctionalConstraint public override void Initialize(Problem p) { var c = (Call)Name; - Result = (FloatVariable)c.Args[0]; - scaleFactor = (float) c.Args[1]; - addends = (FloatVariable[]) c.Args[2]; - foreach (var a in addends) - a.AddFunctionalConstraint(this); - base.Initialize(p); + Result = (FloatVariable)c.Args[0]; + scaleFactor = (float)c.Args[1]; + addends = (FloatVariable[])c.Args[2]; + foreach (var a in addends) + a.AddFunctionalConstraint(this); + Result.PickLast = true; + base.Initialize(p); } public override bool Propagate(FloatVariable changed, bool isUpper, Queue> q) diff --git a/CatSAT/NonBoolean/SMT/Float/Interval.cs b/CatSAT/NonBoolean/SMT/Float/Interval.cs index e69acfd..5bf3eef 100644 --- a/CatSAT/NonBoolean/SMT/Float/Interval.cs +++ b/CatSAT/NonBoolean/SMT/Float/Interval.cs @@ -144,6 +144,39 @@ public bool Contains(float value) Max(a.Lower / b.Lower, a.Upper / b.Upper, a.Lower / b.Upper, a.Upper / b.Lower)); } + /// + /// The result of the interval being raised to a power. + /// + /// + public static Interval operator ^(Interval a, uint exponent) + { + switch (exponent) + { + case 0: + return new Interval(1, 1); + + case 1: + return a; + + default: + if (exponent % 2 == 0) + { + // even exponent + if (a.Lower >= 0) + return new Interval((float)Math.Pow(a.Lower, exponent), (float)Math.Pow(a.Upper, exponent)); + if (a.Upper < 0) + return new Interval((float)Math.Pow(a.Upper, exponent), (float)Math.Pow(a.Lower, exponent)); + return new Interval( + 0, + Math.Max((float)Math.Pow(a.Upper, exponent), (float)Math.Pow(a.Lower, exponent)) + ); + } + // odd exponent + return new Interval((float)Math.Pow(a.Lower, exponent), (float)Math.Pow(a.Upper, exponent)); + } + + } + static float ProductMin(Interval a, Interval b) { return Min(a.Upper * b.Upper, a.Upper * b.Lower, a.Lower * b.Upper, a.Lower * b.Lower); @@ -164,6 +197,55 @@ static float Max(float a, float b, float c, float d) return Math.Max(Math.Max(a, b), Math.Max(c, d)); } + /// + /// Round num up to the nearest multiple of quantization + /// + public static float RoundUp(float num, float quantization) + { + var multiple = num / quantization; + var error = multiple - Math.Round(multiple); + if (error < .00001f && error >= 0) + { + return num; + } + return ((float)Math.Ceiling(num / quantization)) * quantization; + } + + /// + /// Round num down to the nearest multiple of quantization + /// + public static float RoundDown(float num, float quantization) + { + var multiple = num / quantization; + var error = Math.Round(multiple) - multiple; + if (error < .00001f && error >= 0) + { + return num; + } + return ((float)Math.Floor(num / quantization)) * quantization; + } + + /// + /// Narrow the interval to the nearest quantized values + /// + public Interval Quantize(float quantization) + { + if (quantization == 0) + { + return this; + } + float lowerBound = RoundUp(Lower, quantization); + float upperBound = RoundDown(Upper, quantization); + Interval newBounds = new Interval(lowerBound, upperBound); + + return newBounds; + } + + /// + /// Adjust the interval as needed according to quantization + /// + public static Interval Quantize(Interval i, float quantization) => i.Quantize(quantization); + /// public override string ToString() { @@ -171,5 +253,6 @@ public override string ToString() } private string DebuggerDisplay => ToString(); + } } diff --git a/CatSAT/NonBoolean/SMT/Float/MonotoneFunction.cs b/CatSAT/NonBoolean/SMT/Float/MonotoneFunction.cs index 6528ab2..239cd49 100644 --- a/CatSAT/NonBoolean/SMT/Float/MonotoneFunction.cs +++ b/CatSAT/NonBoolean/SMT/Float/MonotoneFunction.cs @@ -32,7 +32,10 @@ internal class MonotoneFunctionConstraint : FunctionalConstraint { public static FloatVariable MonotoneFunction(string name, Func function, Func inverseFunction, bool increasing, FloatVariable input) { - var output = new FloatVariable($"{name}({input.Name})", float.NegativeInfinity, float.PositiveInfinity, input.Condition); + var lower = function(input.Bounds.Lower); + var upper = function(input.Bounds.Upper); + var output = new FloatVariable($"{name}({input.Name})", increasing ? lower : upper, + increasing ? upper : lower, input.Condition) {PickLast = true}; AddConstraint(name, function, inverseFunction, increasing, input, output); return output; } @@ -61,6 +64,7 @@ public override void Initialize(Problem p) Result = (FloatVariable)c.Args[1]; input = (FloatVariable)c.Args[0]; input.AddFunctionalConstraint(this); + Result.PickLast = true; base.Initialize(p); } diff --git a/CatSAT/NonBoolean/SMT/Float/PowerConstraint.cs b/CatSAT/NonBoolean/SMT/Float/PowerConstraint.cs new file mode 100644 index 0000000..ec7f9a2 --- /dev/null +++ b/CatSAT/NonBoolean/SMT/Float/PowerConstraint.cs @@ -0,0 +1,53 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics; + +namespace CatSAT.NonBoolean.SMT.Float +{ + /// + /// Represents the constraint that Result = num ^ exponent + /// + class PowerConstraint : FunctionalConstraint + { + /// + /// The number to be raised to a power. + /// + private FloatVariable num; + + /// + /// The exponent a number is raised to. + /// + private uint exponent; + + public override void Initialize(Problem p) + { + var c = (Call)Name; + Result = (FloatVariable)c.Args[0]; + num = (FloatVariable)c.Args[1]; + exponent = (uint)c.Args[2]; + num.AddFunctionalConstraint(this); + Result.PickLast = true; + base.Initialize(p); + } + + public override bool Propagate(FloatVariable changed, bool isUpper, Queue> q) + { + if (ReferenceEquals(changed, Result)) + { + //Result has been altered + //Result = num ^ exponent, and because PowerConstraint only handles bounds that cross zero even-numbered exponents, + //the negative and positive values of the largest possible Result's inverse function are the bounds of num. + var bound = (float)Math.Pow(Result.Bounds.Upper, 1 / exponent); + + return num.NarrowTo(new Interval(-bound, bound), q); + } + + return Result.NarrowTo(num.Bounds^exponent, q); + } + + public override bool IsDefinedIn(Solution s) + { + return s[this] && Result.IsDefinedInInternal(s) && num.IsDefinedInInternal(s); + } + } +} \ No newline at end of file diff --git a/CatSAT/NonBoolean/Variable.cs b/CatSAT/NonBoolean/Variable.cs index cc66d66..58668b2 100644 --- a/CatSAT/NonBoolean/Variable.cs +++ b/CatSAT/NonBoolean/Variable.cs @@ -42,6 +42,7 @@ public abstract class Variable /// Problem to which this variable is attached /// public readonly Problem Problem; + /// /// Condition under which this variable is defined. /// If true or if Condition is null, the variable must have a value. diff --git a/CatSAT/Properties/Settings.Designer.cs b/CatSAT/Properties/Settings.Designer.cs index 1ba1b1f..8479bc0 100644 --- a/CatSAT/Properties/Settings.Designer.cs +++ b/CatSAT/Properties/Settings.Designer.cs @@ -12,7 +12,7 @@ namespace CatSAT.Properties { [global::System.Runtime.CompilerServices.CompilerGeneratedAttribute()] - [global::System.CodeDom.Compiler.GeneratedCodeAttribute("Microsoft.VisualStudio.Editors.SettingsDesigner.SettingsSingleFileGenerator", "16.6.0.0")] + [global::System.CodeDom.Compiler.GeneratedCodeAttribute("Microsoft.VisualStudio.Editors.SettingsDesigner.SettingsSingleFileGenerator", "16.10.0.0")] internal sealed partial class Settings : global::System.Configuration.ApplicationSettingsBase { private static Settings defaultInstance = ((Settings)(global::System.Configuration.ApplicationSettingsBase.Synchronized(new Settings()))); diff --git a/CatSAT/SAT/Call.cs b/CatSAT/SAT/Call.cs index 7b0ab3b..8fd4ae7 100644 --- a/CatSAT/SAT/Call.cs +++ b/CatSAT/SAT/Call.cs @@ -77,6 +77,20 @@ public static Call FromArgs(Problem p, string name, object arg1, object arg2) return FromArgArray(p, name, ArgBuffer2); } + /// + /// Find the (unique) Call object with the specified name and args in the specified problem. + /// + /// Problem to get the call for + /// Name of the predicate being called + /// Argument of the predicate + /// Argument of the predicate + public static Call FromArgs(Problem p, string name, object arg1, int arg2) + { + ArgBuffer2[0] = arg1; + ArgBuffer2[1] = arg2; + return FromArgArray(p, name, ArgBuffer2); + } + /// /// Find the (unique) Call object with the specified name and args in the specified problem. /// diff --git a/CatSAT/packages.config b/CatSAT/packages.config new file mode 100644 index 0000000..4d36b5d --- /dev/null +++ b/CatSAT/packages.config @@ -0,0 +1,4 @@ + + + + \ No newline at end of file diff --git a/Tests/SMT.cs b/Tests/SMT.cs index 773286c..ae7f70a 100644 --- a/Tests/SMT.cs +++ b/Tests/SMT.cs @@ -23,6 +23,7 @@ // -------------------------------------------------------------------------------------------------------------------- #endregion using System; +using System.Diagnostics; using System.Linq; using Microsoft.VisualStudio.TestTools.UnitTesting; using CatSAT; @@ -223,7 +224,7 @@ public void GeneralSumConstraintTest() var s = p.Solve(); Console.WriteLine(s.Model); var realSum = vars.Select(v => v.Value(s)).Sum(); - Assert.IsTrue(Math.Abs(sum.Value(s) - realSum) < 0.00001f); + AssertApproximatelyEqual(sum.Value(s), realSum); } } @@ -242,7 +243,7 @@ public void AverageConstraintTest() var s = p.Solve(); Console.WriteLine(s.Model); var avg = vars.Select(v => v.Value(s)).Average(); - Assert.IsTrue(Math.Abs(average.Value(s) - avg) < 0.00001f); + AssertApproximatelyEqual(average.Value(s), avg); } } @@ -260,7 +261,7 @@ public void SumConstraintTest() { var s = p.Solve(); Console.WriteLine(s.Model); - Assert.IsTrue(Math.Abs(sum.Value(s) - (x.Value(s)+y.Value(s))) < 0.00001f); + AssertApproximatelyEqual(sum.Value(s), x.Value(s) + y.Value(s)); } } @@ -299,7 +300,7 @@ public void UnsignedProductTest() { var s = p.Solve(); Console.WriteLine(s.Model); - Assert.IsTrue(Math.Abs(product.Value(s) - x.Value(s)*y.Value(s)) < 0.00001f); + AssertApproximatelyEqual(product.Value(s), x.Value(s) * y.Value(s)); } } @@ -317,7 +318,62 @@ public void SignedProductTest() { var s = p.Solve(); Console.WriteLine(s.Model); - Assert.IsTrue(Math.Abs(product.Value(s) - x.Value(s)*y.Value(s)) < 0.00001f); + AssertApproximatelyEqual(product.Value(s), x.Value(s) * y.Value(s)); + } + } + + + [TestMethod] + public void UnsignedDivisionConstraintTest() + { + var p = new Problem(nameof(UnsignedDivisionConstraintTest)); + var dom = new FloatDomain("unit", 1, 50); + var dom2 = new FloatDomain("unit2", 1, 10); + var x = (FloatVariable)dom.Instantiate("x"); + var y = (FloatVariable)dom2.Instantiate("y"); + var quotient = x / y; + + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + Console.WriteLine(s.Model); + AssertApproximatelyEqual(quotient.Value(s), x.Value(s) / y.Value(s)); + } + } + + [TestMethod] + public void SignedDifferenceTest() + { + var p = new Problem(nameof(SignedDifferenceTest)); + var dom = new FloatDomain("signed unit", -1, 1); + var x = (FloatVariable)dom.Instantiate("x"); + var y = (FloatVariable)dom.Instantiate("y"); + var diff = x - y; + + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + Console.WriteLine(s.Model); + AssertApproximatelyEqual(diff.Value(s), (x.Value(s) - y.Value(s))); + } + } + + + [TestMethod] + public void SignedQuotientTest() + { + var p = new Problem(nameof(SignedQuotientTest)); + var dom = new FloatDomain("signed unit", 1, 10); + var x = (FloatVariable)dom.Instantiate("x"); + var y = (FloatVariable)dom.Instantiate("y"); + //p.Assert("foo"); + var diff = x / y; + + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + Console.WriteLine(s.Model); + AssertApproximatelyEqual(diff.Value(s), (x.Value(s) / y.Value(s))); } } @@ -334,7 +390,7 @@ public void NaiveSquareTest() { var s = p.Solve(); Console.WriteLine(s.Model); - Assert.IsTrue(Math.Abs(square.Value(s) - x.Value(s)*x.Value(s)) < 0.00001f); + AssertApproximatelyEqual(square.Value(s), x.Value(s) * x.Value(s)); } } @@ -456,7 +512,889 @@ public void SumConditionTest() Console.WriteLine(s.Model); Assert.AreEqual(sum.IsDefinedInInternal(s), x.IsDefinedInInternal(s) & y.IsDefinedInInternal(s)); if (sum.IsDefinedInInternal(s)) - Assert.IsTrue(Math.Abs(sum.Value(s) - (x.Value(s) + y.Value(s))) < 0.00001f); + AssertApproximatelyEqual(sum.Value(s), x.Value(s) + y.Value(s)); + } + } + + [TestMethod] + public void SumTableTest() + { + var problem = new Problem("SumTableTest"); + var dom = new FloatDomain("unit", 0, 1); + var x = (FloatVariable)dom.Instantiate("x"); + var y = (FloatVariable)dom.Instantiate("y"); + var z = (FloatVariable)dom.Instantiate("z"); + var s = problem.Solve(); + Assert.AreEqual(x + y, x + y); + Assert.AreNotEqual(x + y, x + z); + } + + [TestMethod] + public void ProductTableTest() + { + var problem = new Problem("ProductTableTest"); + var dom = new FloatDomain("unit", 0, 1); + var x = (FloatVariable)dom.Instantiate("x"); + var y = (FloatVariable)dom.Instantiate("y"); + var z = (FloatVariable)dom.Instantiate("z"); + var s = problem.Solve(); + Assert.AreEqual(x * y, x * y); + Assert.AreNotEqual(x * y, x * z); + } + + [TestMethod] + public void ProductTableTest2() + { + var problem = new Problem("ProductTableTest"); + var s = problem.Solve(); + var dom = new FloatDomain("signed unit", -1, 1); + var x = (FloatVariable)dom.Instantiate("x"); + var y = (FloatVariable)dom.Instantiate("y"); + var z = (FloatVariable)dom.Instantiate("z"); + Assert.AreEqual(x * y, x * y); + Assert.AreNotEqual(x * y, x * z); + } + + [TestMethod] + public void ProductTableTest3() + { + var problem = new Problem("ProductTableTest3"); + var s = problem.Solve(); + var dom = new FloatDomain("signed unit", -9, 40, .3f); + var a = (FloatVariable)dom.Instantiate("a"); + var b = (FloatVariable)dom.Instantiate("b"); + var c = (FloatVariable)dom.Instantiate("c"); + var d = (FloatVariable)dom.Instantiate("d"); + var e = (FloatVariable)dom.Instantiate("e"); + var f = (FloatVariable)dom.Instantiate("f"); + + var vars = new FloatVariable[5]; + for (int i = 0; i < vars.Length; i++) + vars[i] = (a * b) + (c * c * d) * (f * e * a * d); + var toavg = FloatVariable.Average(vars); + var final = toavg * a * b * c * d * e * f; + } + + [TestMethod] + public void SquareTableTest() + { + var problem = new Problem("SquareTableTest"); + var dom = new FloatDomain("unit", 0, 1); + var x = (FloatVariable)dom.Instantiate("x"); + Assert.AreEqual(FloatVariable.Square(x), FloatVariable.Square(x)); + var square = FloatVariable.Square(x); + + for (int i = 0; i < 100; i++) + { + var s = problem.Solve(); + AssertApproximatelyEqual(square.Value(s), x.Value(s) * x.Value(s)); + } + } + + [TestMethod][ExpectedException(typeof(ArgumentException))] + public void QuantizationSumErrorTest() + { + var dom1 = new FloatDomain("unit1", 1, 2, 0.5f); + var dom2 = new FloatDomain("unit2", 0, 1, 1.0f); + + var badSum = dom1 + dom2; + } + + + [TestMethod][ExpectedException(typeof(ArgumentException))] + public void QuantizationProductErrorTest() + { + var dom1 = new FloatDomain("unit1", 1, 2, 0.5f); + var dom2 = new FloatDomain("unit2", 0, 1, 1.0f); + + var badProduct = dom1 * dom2; + } + + [TestMethod][ExpectedException(typeof(ArgumentException))] + public void QuantizationDifferenceErrorTest() + { + var dom1 = new FloatDomain("unit1", 1, 2, 0.5f); + var dom2 = new FloatDomain("unit2", 0, 1, 1.0f); + + var badDiff = dom1 - dom2; + } + + [TestMethod] + public void DomainSumTest() + { + var p = new Problem(nameof(DomainSumTest)); + var dom = new FloatDomain("unit", -2, 4, 0.5f); + var dom2 = new FloatDomain("unit2", 0, 1, 0.5f); + var newDom = dom + dom2; + + Assert.AreEqual(newDom.Bounds.Lower, -2); + Assert.AreEqual(newDom.Bounds.Upper, 5); + Assert.AreEqual(newDom.Quantization, 0.5f); + } + + [TestMethod] + public void DomainProductTest() + { + var p = new Problem(nameof(DomainProductTest)); + var dom = new FloatDomain("unit", -2, 4, 0.5f); + var dom2 = new FloatDomain("unit2", 0, 1, 0.5f); + var newDom = dom * dom2; + + Assert.AreEqual(newDom.Bounds.Lower, 0); + Assert.AreEqual(newDom.Bounds.Upper, 4); + Assert.AreEqual(newDom.Quantization, 0.5f); + } + + + [TestMethod] + public void DomainDifferenceTest() + { + var p = new Problem(nameof(DomainDifferenceTest)); + var dom = new FloatDomain("unit", -2, 4, 0.5f); + var dom2 = new FloatDomain("unit2", 0, 1, 0.5f); + var newDom = dom - dom2; + + Assert.AreEqual(newDom.Bounds.Lower, -3); + Assert.AreEqual(newDom.Bounds.Upper, 4); + Assert.AreEqual(newDom.Quantization, 0.5f); + } + + + void CheckVariables(Solution s, params FloatVariable[] variables) + { + foreach (var v in variables) + Assert.IsTrue(v.FloatDomain.Contains(v.Value(s))); + } + + [TestMethod] + public void QuantizedSumTest() + { + var p = new Problem(nameof(QuantizedSumTest)); + var dom = new FloatDomain("unit", -1, 2, 1); + var dom2 = new FloatDomain("unit2", 0, 1, 1); + var newDom = dom * dom2; + + var x = (FloatVariable)newDom.Instantiate("x"); + var y = (FloatVariable)newDom.Instantiate("y"); + + var sum = x + y; + + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + Console.WriteLine(s.Model); + CheckVariables(s,x,y,sum); + AssertApproximatelyEqual(sum.Value(s), (x.Value(s) + y.Value(s))); + } + } + + [TestMethod] + public void QuantizedBoundTest() + { + var p = new Problem(nameof(QuantizedBoundTest)); + var dom = new FloatDomain("unit", -1, 70, 7); + + var x = (FloatVariable)dom.Instantiate("x"); + + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + CheckVariables(s, x); + } + } + + + [TestMethod] + public void QuantizedBoundTest2() + { + var p = new Problem(nameof(QuantizedBoundTest2)); + var dom = new FloatDomain("unit", -14.3f, 97.1f, .7f); + + var x = (FloatVariable)dom.Instantiate("x"); + + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + CheckVariables(s, x); + } + } + + + [TestMethod] + public void QuantizedBoundTest3() + { + var p = new Problem(nameof(QuantizedBoundTest3)); + var dom = new FloatDomain("unit", 1, 11, .9f); + + var x = (FloatVariable)dom.Instantiate("x"); + + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + CheckVariables(s, x); + } + } + + [TestMethod] + public void QuantizedSumConstraintTest() + { + var p = new Problem(nameof(QuantizedSumConstraintTest)); + var dom = new FloatDomain("unit", 0, 1, 0.5f); + var dom2 = new FloatDomain("unit2", 0, 5, 0.5f); + var x = (FloatVariable)dom.Instantiate("x"); + var y = (FloatVariable)dom2.Instantiate("y"); + //p.Assert("foo"); + var sum = x + y; + + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + Console.WriteLine(s.Model); + CheckVariables(s, sum, x, y); + AssertApproximatelyEqual(sum.Value(s), (x.Value(s) + y.Value(s))); + } + } + + [TestMethod] + public void QuantizedProductTest() + { + var p = new Problem(nameof(QuantizedProductTest)); + var dom = new FloatDomain("unit", 0, 1, 0.5f); + var dom2 = new FloatDomain("unit2", 0, 5, 0.5f); + var x = (FloatVariable)dom.Instantiate("x"); + var y = (FloatVariable)dom2.Instantiate("y"); + var prod = x * y; + + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + Console.WriteLine(s.Model); + CheckVariables(s, prod, x, y); + AssertApproximatelyEqual(prod.Value(s), (x.Value(s) * y.Value(s))); + } + } + + + [TestMethod] + public void QuantizedSelfDivTest() + { + var p = new Problem(nameof(QuantizedSelfDivTest)); + var dom = new FloatDomain("unit", 1, 10, 0.9f); + var x = (FloatVariable)dom.Instantiate("x"); + var div = x / x; + + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + Console.WriteLine(s.Model); + CheckVariables(s, div, x); + AssertApproximatelyEqual(div.Value(s), (x.Value(s) / x.Value(s))); + } + } + + [TestMethod] + public void QuantizedSelfSubtractionTest() + { + var p = new Problem(nameof(QuantizedSelfSubtractionTest)); + var dom = new FloatDomain("unit", 1, 10, 0.9f); + var x = (FloatVariable)dom.Instantiate("x"); + var diff = x - x; + + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + Console.WriteLine(s.Model); + CheckVariables(s, diff, x); + AssertApproximatelyEqual(diff.Value(s), (x.Value(s) - x.Value(s))); + } + } + + [TestMethod] + public void QuantizedNaiveSquareTest() + { + var p = new Problem(nameof(QuantizedNaiveSquareTest)); + var dom = new FloatDomain("signed unit", -1, 1, 0.5f); + var x = (FloatVariable)dom.Instantiate("x"); + //p.Assert("foo"); + var square = x * x; + + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + Console.WriteLine(s.Model); + CheckVariables(s, square, x); + AssertApproximatelyEqual(square.Value(s), x.Value(s) * x.Value(s)); + } + } + + [TestMethod] + public void GeneralQuantizedSumConstraintTest() + { + var p = new Problem(nameof(GeneralQuantizedSumConstraintTest)); + var dom = new FloatDomain("unit", 10, 60, 6); + var vars = new FloatVariable[10]; + for (int i = 0; i < vars.Length; i++) + vars[i] = (FloatVariable)dom.Instantiate("x" + i); + var sum = FloatVariable.Sum(vars); + + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + Console.WriteLine(s.Model); + var realSum = vars.Select(v => v.Value(s)).Sum(); + AssertApproximatelyEqual(sum.Value(s), realSum); + } + } + + [TestMethod] + public void GeneralQuantizedSumConstraintTest2() + { + var p = new Problem(nameof(GeneralQuantizedSumConstraintTest2)); + var dom = new FloatDomain("unit", 10, 50, 0.5f); + var vars = new FloatVariable[10]; + for (int i = 0; i < vars.Length; i++) + vars[i] = (FloatVariable)dom.Instantiate("x" + i); + var sum = FloatVariable.Sum(vars); + + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + Console.WriteLine(s.Model); + var realSum = vars.Select(v => v.Value(s)).Sum(); + AssertApproximatelyEqual(sum.Value(s), realSum); + } + } + + [TestMethod] + public void GeneralQuantizedSumConstraintTest3() + { + var p = new Problem(nameof(GeneralQuantizedSumConstraintTest3)); + var dom = new FloatDomain("unit", -10, 49, 7); + var vars = new FloatVariable[10]; + for (int i = 0; i < vars.Length; i++) + vars[i] = (FloatVariable)dom.Instantiate("x" + i); + var sum = FloatVariable.Sum(vars); + + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + Console.WriteLine(s.Model); + var realSum = vars.Select(v => v.Value(s)).Sum(); + AssertApproximatelyEqual(sum.Value(s), realSum); + } + } + + [TestMethod] + public void QuantizedAverageConstraintTest() + { + var p = new Problem(nameof(QuantizedAverageConstraintTest)); + var dom = new FloatDomain("unit", -10, 49, 7); + var vars = new FloatVariable[10]; + for (int i = 0; i < vars.Length; i++) + vars[i] = (FloatVariable)dom.Instantiate("x" + i); + var average = FloatVariable.Average(vars); + + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + Console.WriteLine(s.Model); + var avg = vars.Select(v => v.Value(s)).Average(); + AssertApproximatelyEqual(average.Value(s), avg); + } + } + + [TestMethod] + public void ArraySumTableTest() + { + var p = new Problem(nameof(ArraySumTableTest)); + var dom = new FloatDomain("unit", 1, 3); + var vars = new FloatVariable[5]; + for (int i = 0; i < vars.Length; i++) + vars[i] = (FloatVariable)dom.Instantiate("x" + i); + var vars2 = new FloatVariable[5]; + for (int i = 0; i < vars2.Length; i++) + vars2[i] = vars[i]; + var sum = FloatVariable.Sum(vars); + var sum2 = FloatVariable.Sum(vars2); + + Assert.AreEqual(sum, sum2); + } + + [TestMethod] + public void AverageTableTest() + { + var p = new Problem(nameof(AverageTableTest)); + var dom = new FloatDomain("unit", 1, 3); + var vars = new FloatVariable[5]; + for (int i = 0; i < vars.Length; i++) + vars[i] = (FloatVariable)dom.Instantiate("x" + i); + var vars2 = new FloatVariable[5]; + for (int i = 0; i < vars2.Length; i++) + vars2[i] = vars[i]; + var avg = FloatVariable.Average(vars); + var avg2 = FloatVariable.Average(vars2); + + Assert.AreEqual(avg, avg2); + } + + [TestMethod] + public void AverageTableTest2() + { + var p = new Problem(nameof(AverageTableTest2)); + var dom = new FloatDomain("unit", -6, 9.7f, .1f); + var vars = new FloatVariable[5]; + for (int i = 0; i < vars.Length; i++) + vars[i] = (FloatVariable)dom.Instantiate("x" + i); + + var vars2 = new FloatVariable[5]; + for (int i = 0; i < vars2.Length; i++) + vars2[i] = vars[i]; + + var vars3 = new FloatVariable[5]; + for (int i = 0; i < vars3.Length; i++) + vars3[i] = (FloatVariable)dom.Instantiate("x" + i); + + var avg = FloatVariable.Average(vars); + var avg2 = FloatVariable.Average(vars2); + var avg3 = FloatVariable.Average(vars3); + + Assert.AreEqual(avg, avg2); + Assert.AreNotEqual(avg2, avg3); + } + + [TestMethod] + public void NewAverageTest() + { + var p = new Problem(nameof(NewAverageTest)); + var dom = new FloatDomain("unit", -6, 9.7f); + var vars = new FloatVariable[5]; + for (int i = 0; i < vars.Length; i++) + vars[i] = (FloatVariable)dom.Instantiate("x" + i); + var average = FloatVariable.Average(vars); + + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + var avg = vars.Select(v => v.Value(s)).Average(); + AssertApproximatelyEqual(average.Value(s), avg); + } + + } + + public float getVariance(Solution s, params FloatVariable[] vars) + { + var avg = vars.Select(v => v.Value(s)).Average(); + return (float)vars.Select(v => Math.Pow(v.Value(s) - avg, 2)).Average(); + } + + [TestMethod] + public void VarianceValueTest() + { + var p = new Problem(nameof(VarianceValueTest)); + var dom = new FloatDomain("unit", 1, 1); + var vars = new FloatVariable[5]; + for (int i = 0; i < vars.Length; i++) + vars[i] = (FloatVariable)dom.Instantiate("x" + i); + var variance = FloatVariable.Variance(vars); + + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + + Assert.AreEqual(variance.Value(s), 0); + } + } + + [TestMethod] + public void VarianceValueTest2() + { + var p = new Problem(nameof(VarianceValueTest2)); + var dom = new FloatDomain("unit", 1, 2); + var vars = new FloatVariable[5]; + for (int i = 0; i < vars.Length; i++) + vars[i] = (FloatVariable)dom.Instantiate("x" + i); + var variance = FloatVariable.Variance(vars); + + for (int i = 0; i < 5; i++) + { + var s = p.Solve(); + Assert.IsTrue(variance.Value(s) <= 1); + } + } + + [TestMethod] + public void VarianceTest() + { + var p = new Problem(nameof(VarianceTest)); + var dom = new FloatDomain("unit", -6, 8); + var vars = new FloatVariable[3]; + for (int i = 0; i < vars.Length; i++) + vars[i] = (FloatVariable)dom.Instantiate("x" + i); + var variance = FloatVariable.Variance(vars); + + for (int i = 0; i < 5; i++) + { + var s = p.Solve(); + AssertApproximatelyEqual(variance.Value(s), getVariance(s, vars)); + } + + } + + [TestMethod] + public void VarianceTest2() + { + var p = new Problem(nameof(VarianceTest2)); + var dom = new FloatDomain("unit", -6, 8); + var vars = new FloatVariable[5]; + for (int i = 0; i < vars.Length; i++) + vars[i] = (FloatVariable)dom.Instantiate("x" + i); + var variance = FloatVariable.Variance(vars); + + for (int i = 0; i < 1; i++) + { + var s = p.Solve(); + AssertApproximatelyEqual(variance.Value(s), getVariance(s, vars)); + } + + } + + public void checkAverage(Solution s, FloatVariable computedAvg, params FloatVariable[] vars) + { + var actualAvg = vars.Select(v => v.Value(s)).Average(); + AssertApproximatelyEqual(computedAvg.Value(s), actualAvg); + Assert.IsTrue(computedAvg.FloatDomain.Contains(actualAvg)); + } + + [TestMethod] + public void ConstrainedAverageTest() + { + var p = new Problem(nameof(ConstrainedAverageTest)); + var dom = new FloatDomain("unit", -1, 1); + var vars = new FloatVariable[10]; + for (int i = 0; i < vars.Length; i++) + vars[i] = (FloatVariable)dom.Instantiate("x" + i); + var meanRange = new Interval(0.4f, 0.75f); + var avg = FloatVariable.Average(meanRange, vars); + + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + checkAverage(s, avg, vars); + } + } + + [TestMethod] + public void ConstrainedAverageTest2() + { + var p = new Problem(nameof(ConstrainedAverageTest2)); + var dom = new FloatDomain("unit", -30, 20); + var vars = new FloatVariable[10]; + for (int i = 0; i < vars.Length; i++) + vars[i] = (FloatVariable)dom.Instantiate("x" + i); + var meanRange = new Interval(-7.5f, 17.7f); + var avg = FloatVariable.Average(meanRange, vars); + + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + checkAverage(s, avg, vars); + } + } + + [TestMethod] + public void ConstrainedVarianceTest() + { + var p = new Problem(nameof(ConstrainedVarianceTest)); + var dom = new FloatDomain("unit", -6, 8); + var vars = new FloatVariable[4]; + for (int i = 0; i < vars.Length; i++) + vars[i] = (FloatVariable)dom.Instantiate("x" + i); + var varianceRange = new Interval(0.2f, 0.3f); + var meanRange = new Interval(0, 1); + var variance = FloatVariable.Variance(meanRange, varianceRange, vars); + var avg = FloatVariable.Average(meanRange, vars); + + for (int i = 0; i < 5; i++) + { + var s = p.Solve(); + checkAverage(s, avg, vars); + Assert.IsTrue(varianceRange.Contains(getVariance(s, vars))); + } + } + + [TestMethod] + public void ConstrainedVarianceTest2() + { + var p = new Problem(nameof(ConstrainedVarianceTest2)); + var dom = new FloatDomain("unit", -10, 10); + var vars = new FloatVariable[4]; + for (int i = 0; i < vars.Length; i++) + vars[i] = (FloatVariable)dom.Instantiate("x" + i); + var meanRange = new Interval(-5, 5); + var varianceRange = new Interval(0, 5); + var variance = FloatVariable.Variance(meanRange, varianceRange, vars); + var avg = FloatVariable.Average(meanRange, vars); + + for (int i = 0; i < 5; i++) + { + var s = p.Solve(); + checkAverage(s, avg, vars); + Assert.IsTrue(varianceRange.Contains(getVariance(s, vars))); + } + } + + [TestMethod] + public void ConstrainedVarianceAndMeanTest() + { + var p = new Problem(nameof(ConstrainedVarianceAndMeanTest)); + var dom = new FloatDomain("unit", -10, 10); + var vars = new FloatVariable[4]; + for (int i = 0; i < vars.Length; i++) + vars[i] = (FloatVariable)dom.Instantiate("x" + i); + var meanRange = new Interval(-1, 1); + var varianceRange = new Interval(0, 9); + var variance = FloatVariable.Variance(meanRange, varianceRange, vars); + var avg = FloatVariable.Average(meanRange, vars); + + for (int i = 0; i < 5; i++) + { + var s = p.Solve(); + checkAverage(s, avg, vars); + Assert.IsTrue(varianceRange.Contains(getVariance(s, vars))); + } + } + + [TestMethod] + public void ConstrainedVarianceAndMeanTest2() + { + var p = new Problem(nameof(ConstrainedVarianceAndMeanTest2)); + var dom = new FloatDomain("unit", -100, 100); + var vars = new FloatVariable[4]; + for (int i = 0; i < vars.Length; i++) + vars[i] = (FloatVariable)dom.Instantiate("x" + i); + var meanRange = new Interval(-48.3f, 53); + var varianceRange = new Interval(0, 4); + var variance = FloatVariable.Variance(meanRange, varianceRange, vars); + var avg = FloatVariable.Average(meanRange, vars); + + for (int i = 0; i < 5; i++) + { + var s = p.Solve(); + checkAverage(s, avg, vars); + Assert.IsTrue(varianceRange.Contains(getVariance(s, vars))); + } + } + + [TestMethod] + public void SquareTest() + { + var problem = new Problem("SquareTest"); + var dom = new FloatDomain("signed unit", -1, 10, .2f); + var x = (FloatVariable)dom.Instantiate("x"); + var square = FloatVariable.Square(x); + + for (int i = 0; i < 100; i++) + { + var s = problem.Solve(); + AssertApproximatelyEqual(square.Value(s), x.Value(s) * x.Value(s)); + } + } + + [TestMethod] + public void MonotoneSumConstraintTest() + { + var p = new Problem(nameof(MonotoneSumConstraintTest)); + var dom = new FloatDomain("unit", 1, 2); + var x = (FloatVariable)dom.Instantiate("x"); + var sum = x + 3; + var s = p.Solve(); + AssertApproximatelyEqual(sum.Value(s), (x.Value(s) + 3)); + } + + [TestMethod] + public void MonotoneSumConstraintTest2() + { + var p = new Problem(nameof(MonotoneSumConstraintTest2)); + var dom = new FloatDomain("unit", 1, 2); + var x = (FloatVariable)dom.Instantiate("x"); + var sum2 = 3 + x; + var s = p.Solve(); + AssertApproximatelyEqual(sum2.Value(s), 3 + x.Value(s)); + } + + [TestMethod] + public void MonotoneQuotientConstraintTest() + { + var p = new Problem(nameof(MonotoneQuotientConstraintTest)); + var dom = new FloatDomain("unit", 1, 2); + var x = (FloatVariable)dom.Instantiate("x"); + var quotient = x / 2; + var s = p.Solve(); + AssertApproximatelyEqual(quotient.Value(s), (x.Value(s) / 2)); + } + + [TestMethod] + public void MonotoneDifferenceConstraintTest() + { + var p = new Problem(nameof(MonotoneDifferenceConstraintTest)); + var dom = new FloatDomain("unit", 2, 5); + var x = (FloatVariable)dom.Instantiate("x"); + var diff = x - 2; + var s = p.Solve(); + AssertApproximatelyEqual(diff.Value(s), (x.Value(s) - 2)); + } + + [TestMethod] + public void SignedMonotonePowerConstraintTest() + { + var p = new Problem(nameof(SignedMonotonePowerConstraintTest)); + var dom = new FloatDomain("unit", -5, 5); + var x = (FloatVariable)dom.Instantiate("x"); + var y = x ^ 3; + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + AssertApproximatelyEqual(x.Value(s) * x.Value(s) * x.Value(s), y.Value(s)); + } + } + + [TestMethod] + public void MonotonePowerConstraintTest() + { + var p = new Problem(nameof(MonotonePowerConstraintTest)); + var dom = new FloatDomain("unit", 0, 5); + var x = (FloatVariable)dom.Instantiate("x"); + var y = x ^ 3; + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + AssertApproximatelyEqual(x.Value(s) * x.Value(s) * x.Value(s), y.Value(s)); + } + } + + [TestMethod] + public void MonotonePowerValueTest() + { + var p = new Problem(nameof(MonotonePowerValueTest)); + var dom = new FloatDomain("unit", 5, 5); + var x = (FloatVariable)dom.Instantiate("x"); + var y = x ^ 3; + var s = p.Solve(); + Assert.AreEqual(y.Value(s), 125); + } + + [TestMethod] + public void MonotonePowerValueTest3() + { + var p = new Problem(nameof(MonotonePowerValueTest3)); + var dom = new FloatDomain("unit", 2, 50); + var x = (FloatVariable)dom.Instantiate("x"); + var y = x ^ 5; + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + AssertApproximatelyEqual(y.Value(s),(float)Math.Pow(x.Value(s), 5)); + } + } + + [TestMethod] + public void EvenPowerConstraintTest() + { + var p = new Problem(nameof(EvenPowerConstraintTest)); + var dom = new FloatDomain("unit", -1, 1); + var x = (FloatVariable)dom.Instantiate("x"); + var y = x ^ 2; + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + AssertApproximatelyEqual(y.Value(s), x.Value(s) * x.Value(s)); + } + } + + [TestMethod] + public void EvenPowerConstraintTest2() + { + var p = new Problem(nameof(EvenPowerConstraintTest2)); + var dom = new FloatDomain("unit", -50, 100); + var x = (FloatVariable)dom.Instantiate("x"); + var y = x ^ 2; + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + AssertApproximatelyEqual(y.Value(s), x.Value(s) * x.Value(s)); + } + } + + [TestMethod] + public void EvenPowerConstraintTest3() + { + var p = new Problem(nameof(EvenPowerConstraintTest3)); + var dom = new FloatDomain("unit", -50, -1); + var x = (FloatVariable)dom.Instantiate("x"); + var y = x ^ 6; + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + AssertApproximatelyEqual(y.Value(s), (float)Math.Pow(x.Value(s), 6)); + } + } + + [TestMethod] + public void EvenPowerConstraintTest4() + { + var p = new Problem(nameof(EvenPowerConstraintTest4)); + var dom = new FloatDomain("unit", 0, 5); + var x = (FloatVariable)dom.Instantiate("x"); + var y = x ^ 4; + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + AssertApproximatelyEqual(y.Value(s), x.Value(s) * x.Value(s) * x.Value(s) * x.Value(s)); + } + } + + [TestMethod] + public void EvenPowerConstraintTest5() + { + var p = new Problem(nameof(EvenPowerConstraintTest5)); + var dom = new FloatDomain("unit", -98, 102); + var x = (FloatVariable)dom.Instantiate("x"); + var y = x ^ 20; + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + AssertApproximatelyEqual(y.Value(s), (float)Math.Pow(x.Value(s), 20)); + } + } + + [TestMethod] + public void EvenPowerConstraintTest6() + { + var p = new Problem(nameof(EvenPowerConstraintTest6)); + var dom = new FloatDomain("unit", 1, 50); + var x = (FloatVariable)dom.Instantiate("x"); + var y = x ^ 0; + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + AssertApproximatelyEqual(y.Value(s), 1); + } + } + + [TestMethod] + public void SquareEquivalenceTest() + { + var p = new Problem(nameof(SquareEquivalenceTest)); + var dom = new FloatDomain("unit", -10, 50); + var y = (FloatVariable)dom.Instantiate("y"); + var x = (FloatVariable)dom.Instantiate("x"); + var diff = y - x; + var pow = diff ^ 2; + var sq = FloatVariable.Square(diff); + for (int i = 0; i < 100; i++) + { + var s = p.Solve(); + AssertApproximatelyEqual(pow.Value(s), sq.Value(s)); } } @@ -504,5 +1442,14 @@ public void FloatPredeterminationTest() Assert.IsFalse(problem.IsPredetermined(yLTz)); } } + void AssertApproximatelyEqual(float a, float b, float tolerance = 0.001f) + { + var difference = Math.Abs(a - b); + var magnitude = Math.Max(Math.Abs(a), Math.Abs(b)); + if (magnitude != 0) + { + Assert.IsTrue(difference / magnitude < tolerance); + } + } } }