From 89e3c1fd9811150ab4a8fb572f6416ba3ae5ae69 Mon Sep 17 00:00:00 2001 From: annalis97 Date: Tue, 27 Jul 2021 22:44:53 -0400 Subject: [PATCH 1/5] Quantization updates --- CatSAT.sln.DotSettings | 2 + CatSAT/CatSAT.csproj | 4 + CatSAT/NonBoolean/SMT/Float/FloatDomain.cs | 123 +++++++ CatSAT/NonBoolean/SMT/Float/FloatSolver.cs | 33 +- CatSAT/NonBoolean/SMT/Float/FloatVariable.cs | 114 ++++++- CatSAT/NonBoolean/SMT/Float/Interval.cs | 47 +++ CatSAT/packages.config | 4 + Tests/SMT.cs | 318 +++++++++++++++++++ 8 files changed, 625 insertions(+), 20 deletions(-) create mode 100644 CatSAT/packages.config diff --git a/CatSAT.sln.DotSettings b/CatSAT.sln.DotSettings index d5503c3..03d2b40 100644 --- a/CatSAT.sln.DotSettings +++ b/CatSAT.sln.DotSettings @@ -16,4 +16,6 @@ True True True + True + True True \ No newline at end of file diff --git a/CatSAT/CatSAT.csproj b/CatSAT/CatSAT.csproj index c2332e7..7ab53ca 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 + @@ -114,6 +117,7 @@ + SettingsSingleFileGenerator Settings.Designer.cs 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..cdcd32c 100644 --- a/CatSAT/NonBoolean/SMT/Float/FloatSolver.cs +++ b/CatSAT/NonBoolean/SMT/Float/FloatSolver.cs @@ -26,6 +26,7 @@ using System.Collections; using System.Collections.Generic; using System.Linq; +using System.Diagnostics; namespace CatSAT.NonBoolean.SMT.Float { @@ -38,8 +39,14 @@ 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>(); + /// /// Add clauses that follow from user-defined bounds, e.g. from transitivity. /// @@ -50,7 +57,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++) @@ -114,7 +121,7 @@ public override bool Solve(Solution s) FindEquivalenceClasses(s); FindActiveFunctionalConstraints(s); - if (!FindSolutionBounds(s)) + if (!FindSolutionBounds(s)) // Constraint are contradictory return false; @@ -246,7 +253,9 @@ private bool FindSolutionBounds(Solution s) // Save bounds foreach (var v in representatives) + { v.SolutionBounds = v.Bounds; + } return true; } @@ -264,9 +273,25 @@ private bool TrySample() Random.Shuffle(representatives); 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); + + int randStep = CatSAT.Random.InRange(0, possibilities-1); + + float rand = (float)(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..8a61a05 100644 --- a/CatSAT/NonBoolean/SMT/Float/FloatVariable.cs +++ b/CatSAT/NonBoolean/SMT/Float/FloatVariable.cs @@ -77,15 +77,30 @@ public FloatVariable(object name, float low, float high, Literal condition) /// public override Domain Domain => FloatDomain; + public float Quantization => FloatDomain.Quantization; + /// /// Saved bounds for current SMT Solution, after initial constraint processing, but before sampling /// internal Interval SolutionBounds; + private Interval _bounds; + /// /// Current bounds to which the variable has been narrowed /// - internal Interval Bounds; + internal Interval Bounds + { + get => _bounds; + set + { + _bounds = value; + //if (Quantization == 0) + // _bounds = value; + //else + // _bounds = value.Quantize(Quantization); + } + } /// /// The predetermined value for the variable, if any. @@ -140,10 +155,10 @@ internal static void Equate(FloatVariable v1, FloatVariable v2) 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 +189,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 +204,14 @@ internal void ResetSolverState() /// True is resulting bounds are consistent internal bool BoundAbove(float 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,17 @@ internal bool BoundAbove(float bound) /// True is resulting bounds are consistent internal bool BoundBelow(float 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; } @@ -214,10 +244,16 @@ internal bool BoundBelow(float bound) /// Upper bound on variable /// Propagation queue /// True is resulting bounds are consistent - internal bool BoundAbove(float bound, Queue> q) + internal bool BoundAbove(float bound, Queue> q, bool requantize=true) { + 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; } @@ -326,10 +362,18 @@ private void EnsurePresent(Queue> q, TupleLower bound on variable /// Propagation queue /// 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; + 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 +449,16 @@ 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, + v1.FloatDomain.Bounds.Lower + v2.FloatDomain.Bounds.Lower, + v1.FloatDomain.Bounds.Upper + v2.FloatDomain.Bounds.Upper, FunctionalConstraint.CombineConditions(v1.Condition, v2.Condition)); + sumTable[(v1, v2)] = sum; Problem.Current.Assert(Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, "IsSum", sum, v1, v2))); return sum; } @@ -418,12 +468,44 @@ 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 negv2 = new Interval(-1 * v2.FloatDomain.Bounds.Lower, -1 * v2.FloatDomain.Bounds.Upper); + 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)); + 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 product of another FloatVariable and a constant diff --git a/CatSAT/NonBoolean/SMT/Float/Interval.cs b/CatSAT/NonBoolean/SMT/Float/Interval.cs index e69acfd..dec7b1a 100644 --- a/CatSAT/NonBoolean/SMT/Float/Interval.cs +++ b/CatSAT/NonBoolean/SMT/Float/Interval.cs @@ -164,6 +164,52 @@ 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; + } + + public static Interval Quantize(Interval i, float Quantization) => i.Quantize(Quantization); + /// public override string ToString() { @@ -171,5 +217,6 @@ public override string ToString() } private string DebuggerDisplay => ToString(); + } } 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..941e070 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; @@ -321,6 +322,61 @@ public void SignedProductTest() } } + + [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); + Assert.IsTrue(Math.Abs(quotient.Value(s) - (x.Value(s) / y.Value(s))) < 0.00001f); + } + } + + [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); + Assert.IsTrue(Math.Abs(diff.Value(s) - (x.Value(s) - y.Value(s))) < 0.00001f); + } + } + + + [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); + Assert.IsTrue(Math.Abs(diff.Value(s) - (x.Value(s) / y.Value(s))) < 0.00001f); + } + } + [TestMethod] public void NaiveSquareTest() { @@ -460,6 +516,268 @@ public void SumConditionTest() } } + [TestMethod] + public void 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"); + + Assert.AreEqual(x + y, x + y); + Assert.AreNotEqual(x + y, x + z); + } + + [TestMethod] + public void 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"); + Assert.AreEqual(x * y, x * y); + Assert.AreNotEqual(x * y, x * z); + } + + [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); + Assert.IsTrue(Math.Abs(sum.Value(s) - (x.Value(s) + y.Value(s))) < 0.00001f); + } + } + + [TestMethod] + public void QuantizedBoundTest() + { + var p = new Problem(nameof(QuantizedBoundTest)); + var dom = new FloatDomain("unit", -1, 70, 7); + + var x = (FloatVariable)dom.Instantiate("x"); + + //Assert.AreEqual(x.Bounds.Upper, 70); + //Assert.AreEqual(x.Bounds.Lower, 0); + + 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); + Assert.IsTrue(Math.Abs(sum.Value(s) - (x.Value(s) + y.Value(s))) < 0.00001f); + } + } + + [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); + Assert.IsTrue(Math.Abs(prod.Value(s) - (x.Value(s) * y.Value(s))) < 0.00001f); + } + } + + + [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); + Assert.IsTrue(Math.Abs(div.Value(s) - (x.Value(s) / x.Value(s))) < 0.00001f); + } + } + + [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); + Assert.IsTrue(Math.Abs(diff.Value(s) - (x.Value(s) - x.Value(s))) < 0.00001f); + } + } + + [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); + Assert.IsTrue(Math.Abs(square.Value(s) - x.Value(s) * x.Value(s)) < 0.00001f); + } + } + [TestMethod] public void FloatPredeterminationTest() { From fd626ae779ee1841f2fbcaeea0cca79296bd113c Mon Sep 17 00:00:00 2001 From: annalis97 Date: Wed, 11 Aug 2021 11:13:00 -0400 Subject: [PATCH 2/5] Power functions revised --- CatSAT.sln.DotSettings | 10 +- CatSAT/CatSAT.csproj | 1 + CatSAT/NonBoolean/SMT/Float/FloatSolver.cs | 11 +- CatSAT/NonBoolean/SMT/Float/FloatVariable.cs | 472 +++++++++++++----- CatSAT/NonBoolean/SMT/Float/Interval.cs | 10 + .../NonBoolean/SMT/Float/MonotoneFunction.cs | 4 +- .../NonBoolean/SMT/Float/PowerConstraint.cs | 81 +++ CatSAT/NonBoolean/Variable.cs | 1 + CatSAT/Properties/Settings.Designer.cs | 2 +- CatSAT/SAT/Call.cs | 14 + Tests/SMT.cs | 471 ++++++++++++++++- 11 files changed, 957 insertions(+), 120 deletions(-) create mode 100644 CatSAT/NonBoolean/SMT/Float/PowerConstraint.cs diff --git a/CatSAT.sln.DotSettings b/CatSAT.sln.DotSettings index 03d2b40..f639bd7 100644 --- a/CatSAT.sln.DotSettings +++ b/CatSAT.sln.DotSettings @@ -6,6 +6,9 @@ True True True + True + True + True True True @@ -16,6 +19,11 @@ True True True + True + True + True True - True \ No newline at end of file + True + True + True \ No newline at end of file diff --git a/CatSAT/CatSAT.csproj b/CatSAT/CatSAT.csproj index 7ab53ca..775e192 100644 --- a/CatSAT/CatSAT.csproj +++ b/CatSAT/CatSAT.csproj @@ -58,6 +58,7 @@ + diff --git a/CatSAT/NonBoolean/SMT/Float/FloatSolver.cs b/CatSAT/NonBoolean/SMT/Float/FloatSolver.cs index cdcd32c..82656a0 100644 --- a/CatSAT/NonBoolean/SMT/Float/FloatSolver.cs +++ b/CatSAT/NonBoolean/SMT/Float/FloatSolver.cs @@ -27,6 +27,7 @@ using System.Collections.Generic; using System.Linq; using System.Diagnostics; +using static System.Collections.StructuralComparisons; namespace CatSAT.NonBoolean.SMT.Float { @@ -44,8 +45,13 @@ class FloatSolver : TheorySolver /// private readonly Queue> propagationQueue = new Queue>(); + private static FloatVariableArrayComparer IEqualityComparer = new FloatVariableArrayComparer(); + 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(IEqualityComparer); + public Dictionary AverageTable = new Dictionary(IEqualityComparer); /// /// Add clauses that follow from user-defined bounds, e.g. from transitivity. @@ -283,9 +289,10 @@ private bool TrySample() { int possibilities = (int)((v.Bounds.Upper - v.Bounds.Lower) / v.FloatDomain.Quantization); - int randStep = CatSAT.Random.InRange(0, possibilities-1); + // ReSharper disable once RedundantNameQualifier + int randStep = CatSAT.Random.InRange(0, possibilities); - float rand = (float)(randStep * v.FloatDomain.Quantization) + v.Bounds.Lower; + float rand = randStep * v.FloatDomain.Quantization + v.Bounds.Lower; v.PickValue(rand, propagationQueue); } diff --git a/CatSAT/NonBoolean/SMT/Float/FloatVariable.cs b/CatSAT/NonBoolean/SMT/Float/FloatVariable.cs index 8a61a05..f4d856d 100644 --- a/CatSAT/NonBoolean/SMT/Float/FloatVariable.cs +++ b/CatSAT/NonBoolean/SMT/Float/FloatVariable.cs @@ -22,11 +22,12 @@ // // -------------------------------------------------------------------------------------------------------------------- #endregion +using CatSAT.NonBoolean.SMT.Float; using System; using System.Collections.Generic; using System.Diagnostics; using System.Globalization; -using CatSAT.NonBoolean.SMT.Float; +using System.Linq; namespace CatSAT { @@ -77,6 +78,9 @@ 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; /// @@ -84,6 +88,7 @@ public FloatVariable(object name, float low, float high, Literal condition) /// internal Interval SolutionBounds; + // ReSharper disable once InconsistentNaming private Interval _bounds; /// @@ -92,14 +97,7 @@ public FloatVariable(object name, float low, float high, Literal condition) internal Interval Bounds { get => _bounds; - set - { - _bounds = value; - //if (Quantization == 0) - // _bounds = value; - //else - // _bounds = value.Quantize(Quantization); - } + set => _bounds = value; } /// @@ -204,6 +202,7 @@ 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); @@ -223,6 +222,7 @@ 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); @@ -243,9 +243,11 @@ 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, bool requantize=true) + internal bool BoundAbove(float bound, Queue> q, bool requantize = true) { + Debug.Assert(!float.IsNaN(bound)); if (Quantization != 0 && requantize) { bound = Interval.RoundDown(bound, Quantization); @@ -270,81 +272,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. @@ -361,15 +363,17 @@ 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, bool requantize=true) + internal bool BoundBelow(float bound, Queue> q, bool requantize = true) { + Debug.Assert(!float.IsNaN(bound)); if (Quantization != 0 && requantize) { bound = Interval.RoundUp(bound, Quantization); } if (!(bound > Bounds.Lower)) { - return true; + return true; } var b = Bounds; b.Lower = bound; @@ -479,13 +483,12 @@ internal bool BoundBelow(float bound, Queue> q, bool 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 negv2 = new Interval(-1 * v2.FloatDomain.Bounds.Lower, -1 * v2.FloatDomain.Bounds.Upper); 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)); Problem.Current.Assert(Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, "IsSum", v1, v2, difference))); @@ -505,7 +508,27 @@ internal bool BoundBelow(float bound, Queue> q, bool 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 @@ -514,7 +537,7 @@ internal bool BoundBelow(float bound, Queue> q, bool { 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 /// @@ -524,22 +547,160 @@ internal bool BoundBelow(float bound, Queue> q, bool } /// - /// 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, int c) { - var domainBounds = Interval.Zero; - foreach (var a in vars) - domainBounds += a.FloatDomain.Bounds; - foreach (var a in vars) - 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))); - return sum; + if (c < 0) + { + throw new InvalidOperationException($"Cannot raise bounds to a negative power"); + } + + //else if the exponent is even but the bounds don't match that criteria, + //Declare new FloatVariable while performing arithmetic with bounds, as with Craft's CSP. + //Assert a power constraint, passing in the new variable as a parameter as well. + if ((c % 2 != 0)) + { + return MonotoneFunctionConstraint.MonotoneFunction($"^{c}", x => (float)Math.Pow(x, c), + y => { + if (y < 0) + { + return (float)-Math.Pow(-y, 1.0 / c); + } + else + { + return (float)Math.Pow(y, 1.0 / c); + } + }, c > 0, v); + } + + else if (c % 2 == 0 && v.Bounds.Lower >= 0) + { + return MonotoneFunctionConstraint.MonotoneFunction($"^{c}", x => (float)Math.Pow(x, c), y => (float)Math.Pow(y, 1.0 / c), c > 0, v); + } + + else 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); + } + + else + { + var lower = Math.Min((float)Math.Pow(v.FloatDomain.Bounds.Lower, c), (float)Math.Pow(v.FloatDomain.Bounds.Upper, c)); + var upper = Math.Max((float)Math.Pow(v.FloatDomain.Bounds.Lower, c), (float)Math.Pow(v.FloatDomain.Bounds.Upper, c)); + var pow = new FloatVariable($"{v.Name}^{c}", v.FloatDomain.Bounds.Lower, v.FloatDomain.Bounds.Upper, FunctionalConstraint.CombineConditions(v.Condition, v.Condition)); + + 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; + } + + else 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; + } + + else + { + foreach (var a in vars) + { + newDomain += a.FloatDomain.Bounds.Quantize(vars[0].Quantization); + } + + foreach (var a in vars) + if (!ReferenceEquals(a.Condition, null)) + throw new ArgumentException("Sum does not support conditioned variables", a.Name.ToString()); + + 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; + } } /// @@ -550,18 +711,58 @@ 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; - foreach (var a in vars) - domainBounds += a.FloatDomain.Bounds; + 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) - 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 av = new FloatVariable("average", newDomain.Bounds.Lower * 1f / vars.Length, + newDomain.Bounds.Upper * 1f / vars.Length, null); + av.FloatDomain.Quantization = (vars[0].Quantization * 1f / vars.Length); + + averageTable[vars] = av; + + Problem.Current.Assert( + Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, + "IsAverage", av, 1f / vars.Length, vars))); + 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 mean = FloatVariable.Average(vars); + + return FloatVariable.Average(vars.Select(v => { var minusMean = v - mean; return Square(minusMean); }).ToArray()); } internal void AddUpperBound(FloatVariable bound) @@ -595,4 +796,47 @@ 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 + /// + /// + private static readonly IEqualityComparer equalityComparer; + + bool IEqualityComparer.Equals(FloatVariable[] a, FloatVariable[] b) + { + 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; + for (int i = 0; i < array.Length; i++) + { + int currentHashCode = array[i].GetHashCode(); + aggregate ^= currentHashCode; + } + + return aggregate; + } + } } diff --git a/CatSAT/NonBoolean/SMT/Float/Interval.cs b/CatSAT/NonBoolean/SMT/Float/Interval.cs index dec7b1a..8153222 100644 --- a/CatSAT/NonBoolean/SMT/Float/Interval.cs +++ b/CatSAT/NonBoolean/SMT/Float/Interval.cs @@ -98,6 +98,16 @@ public bool Contains(float value) return Lower <= value && value <= Upper; } + public static bool operator ==(Interval a, Interval b) + { + return (a.Lower - b.Lower < .00001f && a.Upper - b.Upper < .00001f); + } + + public static bool operator !=(Interval a, Interval b) + { + return (!(a == b)); + } + /// /// The interval sum of two intervals. /// This is the interval bounding all possible sums of values taken from the original intervals. diff --git a/CatSAT/NonBoolean/SMT/Float/MonotoneFunction.cs b/CatSAT/NonBoolean/SMT/Float/MonotoneFunction.cs index 6528ab2..415eb7d 100644 --- a/CatSAT/NonBoolean/SMT/Float/MonotoneFunction.cs +++ b/CatSAT/NonBoolean/SMT/Float/MonotoneFunction.cs @@ -32,7 +32,9 @@ 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); AddConstraint(name, function, inverseFunction, increasing, input, output); return output; } diff --git a/CatSAT/NonBoolean/SMT/Float/PowerConstraint.cs b/CatSAT/NonBoolean/SMT/Float/PowerConstraint.cs new file mode 100644 index 0000000..4acbde9 --- /dev/null +++ b/CatSAT/NonBoolean/SMT/Float/PowerConstraint.cs @@ -0,0 +1,81 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics; + +namespace CatSAT.NonBoolean.SMT.Float +{ + class PowerConstraint : FunctionalConstraint + { + private FloatVariable num; + + private float exponent; + + public override void Initialize(Problem p) + { + var c = (Call)Name; + Result = (FloatVariable)c.Args[0]; + num = (FloatVariable)c.Args[1]; + exponent = (int)c.Args[2]; + num.AddFunctionalConstraint(this); + base.Initialize(p); + } + + public override bool Propagate(FloatVariable changed, bool isUpper, Queue> q) + { + if (ReferenceEquals(changed, Result)) + { + float lower, upper; + if (Result.Bounds.Upper < 0) + { + upper = (float)-Math.Pow(-Result.Bounds.Upper, 1 / exponent); + } + + else + { + upper = (float)Math.Pow(Result.Bounds.Upper, 1 / exponent); + } + + if (Result.Bounds.Lower < 0) + { + lower = (float)-Math.Pow(-Result.Bounds.Lower, 1 / exponent); + } + else + { + lower = (float)Math.Pow(Result.Bounds.Lower, 1 / exponent); + } + var invBounds = new Interval(lower, upper); + return num.NarrowTo(invBounds, q); + } + + if (num.Bounds.Upper <= 0) + { + var lower = (float)-Math.Pow(Math.Max(0, -num.Bounds.Lower), 1 / exponent); + var upper = (float)-Math.Pow(Math.Max(0, -num.Bounds.Upper), 1 / exponent); + var invInterval = new Interval(-lower, -upper); + + return num.NarrowTo(invInterval, q); + } + else + { + var bound = (float)Math.Pow(num.Bounds.Upper, 1 / exponent); + var invInterval = new Interval(-bound, bound); + return num.NarrowTo(invInterval, q); + } + //check if ReferenceEquals(changed, Result) is true; + //return the result of num.NarrowTo using inverse function as a parameter + + //Narrow Result's bounds to bounds raised to the exponent. + + // To do this, since it's an even exponent: + // If num is non-positive, narrow to the negative interval returned by the inverse function. + + // Else, perform the inverse function and retrieve the Upper value. + // Narrow to a new interval between the negative and positive of that value. + } + + 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/Tests/SMT.cs b/Tests/SMT.cs index 941e070..6a75f90 100644 --- a/Tests/SMT.cs +++ b/Tests/SMT.cs @@ -519,11 +519,12 @@ public void SumConditionTest() [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); } @@ -531,14 +532,65 @@ public void SumTableTest() [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(); + Assert.IsTrue(Math.Abs(square.Value(s) - (x.Value(s) * x.Value(s))) < 0.00001f); + } + } + [TestMethod][ExpectedException(typeof(ArgumentException))] public void QuantizationSumErrorTest() { @@ -778,6 +830,417 @@ public void QuantizedNaiveSquareTest() } } + [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(); + Assert.IsTrue(Math.Abs(sum.Value(s) - realSum) < 0.00001f); + } + } + + [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(); + Assert.IsTrue(Math.Abs(sum.Value(s) - realSum) < 0.00001f); + } + } + + [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(); + Assert.IsTrue(Math.Abs(sum.Value(s) - realSum) < 0.00001f); + } + } + + [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(); + Assert.IsTrue(Math.Abs(average.Value(s) - avg) < 0.00001f); + } + } + + [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(); + + Assert.IsTrue(Math.Abs(average.Value(s) - avg) < .00001f); + } + + } + + [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, 9.7f); + var vars = new FloatVariable[1]; + 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(); + var avg = vars.Select(v => v.Value(s)).Average(); + float squareSum = 0; + for (int j = 0; j < vars.Length; j++) + { + squareSum += (vars[j].Value(s) - avg) * (vars[j].Value(s) - avg); + } + + Assert.IsTrue(Math.Abs(variance.Value(s) - squareSum/vars.Length)< .00001f); + } + + } + + [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(); + Assert.IsTrue(Math.Abs(square.Value(s) - (x.Value(s) * x.Value(s))) < 0.00001f); + } + } + + [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(); + Assert.IsTrue(Math.Abs(sum.Value(s) - (x.Value(s) + 3)) < 0.00001f); + } + + [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(); + Assert.IsTrue(Math.Abs(sum2.Value(s) - (3 + x.Value(s))) < 0.00001f); + } + + [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(); + Assert.IsTrue(Math.Abs(quotient.Value(s) - (x.Value(s)/2)) < 0.00001f); + } + + [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(); + Assert.IsTrue(Math.Abs(diff.Value(s) - (x.Value(s) - 2)) < 0.00001f); + } + + [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(); + Assert.IsTrue(Math.Abs((x.Value(s) * x.Value(s) * x.Value(s)) - y.Value(s)) < .0001f); + } + } + + [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(); + Assert.IsTrue(Math.Abs((x.Value(s) * x.Value(s) * x.Value(s)) - y.Value(s)) < .0001f); + } + } + + [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, 2); + 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 ^ 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 EvenPowerConstraintTest3() + { + var p = new Problem(nameof(EvenPowerConstraintTest3)); + var dom = new FloatDomain("unit", -50, -1); + 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 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", 1, 50); + 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 FloatPredeterminationTest() { @@ -822,5 +1285,11 @@ public void FloatPredeterminationTest() Assert.IsFalse(problem.IsPredetermined(yLTz)); } } + void AssertApproximatelyEqual(float a, float b, float tolerance = 0.0001f) + { + var difference = Math.Abs(a - b); + var magnitude = Math.Max(Math.Abs(a), Math.Abs(b)); + Assert.IsTrue(difference / magnitude < tolerance); + } } } From f778a1e05f990144fa1f9e3f923bbda94d3ffabc Mon Sep 17 00:00:00 2001 From: annalis97 Date: Fri, 13 Aug 2021 14:07:52 -0400 Subject: [PATCH 3/5] TODO: variance --- CatSAT/NonBoolean/SMT/Float/FloatSolver.cs | 4 ++ CatSAT/NonBoolean/SMT/Float/FloatVariable.cs | 24 ++++------- CatSAT/NonBoolean/SMT/Float/Interval.cs | 29 +++++++++++++ .../NonBoolean/SMT/Float/PowerConstraint.cs | 29 ++----------- Tests/SMT.cs | 42 +++++++++++++------ 5 files changed, 74 insertions(+), 54 deletions(-) diff --git a/CatSAT/NonBoolean/SMT/Float/FloatSolver.cs b/CatSAT/NonBoolean/SMT/Float/FloatSolver.cs index 82656a0..26b03a9 100644 --- a/CatSAT/NonBoolean/SMT/Float/FloatSolver.cs +++ b/CatSAT/NonBoolean/SMT/Float/FloatSolver.cs @@ -279,6 +279,10 @@ private bool TrySample() Random.Shuffle(representatives); foreach (var v in representatives) { + if (v.DontPick) + { + continue; + } if (v.FloatDomain.Quantization == 0) { diff --git a/CatSAT/NonBoolean/SMT/Float/FloatVariable.cs b/CatSAT/NonBoolean/SMT/Float/FloatVariable.cs index f4d856d..fa92d20 100644 --- a/CatSAT/NonBoolean/SMT/Float/FloatVariable.cs +++ b/CatSAT/NonBoolean/SMT/Float/FloatVariable.cs @@ -151,6 +151,8 @@ internal static void Equate(FloatVariable v1, FloatVariable v2) /// internal readonly int Index; + internal bool DontPick; + private string DebugValueString => Bounds.IsUnique ? Bounds.Lower.ToString(CultureInfo.InvariantCulture) : Bounds.ToString(); internal void PickValue(float r, Queue> q) @@ -549,17 +551,14 @@ internal bool BoundBelow(float bound, Queue> q, bool /// /// A FloatVariable constrained to be the power of another FloatVariable and a constant /// - public static FloatVariable operator ^(FloatVariable v, int c) + public static FloatVariable operator ^(FloatVariable v, uint c) { if (c < 0) { - throw new InvalidOperationException($"Cannot raise bounds to a negative power"); + throw new ArgumentException($"Cannot raise bounds to a negative power"); } - //else if the exponent is even but the bounds don't match that criteria, - //Declare new FloatVariable while performing arithmetic with bounds, as with Craft's CSP. - //Assert a power constraint, passing in the new variable as a parameter as well. - if ((c % 2 != 0)) + if ((c % 2 != 0) || (c%2==0 && v.Bounds.Lower >=0)) { return MonotoneFunctionConstraint.MonotoneFunction($"^{c}", x => (float)Math.Pow(x, c), y => { @@ -574,11 +573,6 @@ internal bool BoundBelow(float bound, Queue> q, bool }, c > 0, v); } - else if (c % 2 == 0 && v.Bounds.Lower >= 0) - { - return MonotoneFunctionConstraint.MonotoneFunction($"^{c}", x => (float)Math.Pow(x, c), y => (float)Math.Pow(y, 1.0 / c), c > 0, v); - } - else 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); @@ -586,9 +580,10 @@ internal bool BoundBelow(float bound, Queue> q, bool else { - var lower = Math.Min((float)Math.Pow(v.FloatDomain.Bounds.Lower, c), (float)Math.Pow(v.FloatDomain.Bounds.Upper, c)); var upper = Math.Max((float)Math.Pow(v.FloatDomain.Bounds.Lower, c), (float)Math.Pow(v.FloatDomain.Bounds.Upper, c)); - var pow = new FloatVariable($"{v.Name}^{c}", v.FloatDomain.Bounds.Lower, v.FloatDomain.Bounds.Upper, FunctionalConstraint.CombineConditions(v.Condition, v.Condition)); + var pow = new FloatVariable($"{v.Name}^{c}", 0, v.FloatDomain.Bounds.Upper, FunctionalConstraint.CombineConditions(v.Condition, v.Condition)); + + pow.DontPick = true; Problem.Current.Assert(Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, "IsPower", pow, v, c))); return pow; @@ -761,8 +756,7 @@ public static FloatVariable Average(params FloatVariable[] vars) public static FloatVariable Variance(params FloatVariable[] vars) { var mean = FloatVariable.Average(vars); - - return FloatVariable.Average(vars.Select(v => { var minusMean = v - mean; return Square(minusMean); }).ToArray()); + return FloatVariable.Average(vars.Select(v => (v - mean)^2 ).ToArray()); } internal void AddUpperBound(FloatVariable bound) diff --git a/CatSAT/NonBoolean/SMT/Float/Interval.cs b/CatSAT/NonBoolean/SMT/Float/Interval.cs index 8153222..3183dc6 100644 --- a/CatSAT/NonBoolean/SMT/Float/Interval.cs +++ b/CatSAT/NonBoolean/SMT/Float/Interval.cs @@ -154,6 +154,35 @@ public bool Contains(float value) Max(a.Lower / b.Lower, a.Upper / b.Upper, a.Lower / b.Upper, a.Upper / b.Lower)); } + 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); diff --git a/CatSAT/NonBoolean/SMT/Float/PowerConstraint.cs b/CatSAT/NonBoolean/SMT/Float/PowerConstraint.cs index 4acbde9..d77be85 100644 --- a/CatSAT/NonBoolean/SMT/Float/PowerConstraint.cs +++ b/CatSAT/NonBoolean/SMT/Float/PowerConstraint.cs @@ -8,14 +8,14 @@ class PowerConstraint : FunctionalConstraint { private FloatVariable num; - private float exponent; + private uint exponent; public override void Initialize(Problem p) { var c = (Call)Name; Result = (FloatVariable)c.Args[0]; num = (FloatVariable)c.Args[1]; - exponent = (int)c.Args[2]; + exponent = (uint)c.Args[2]; num.AddFunctionalConstraint(this); base.Initialize(p); } @@ -47,30 +47,7 @@ public override bool Propagate(FloatVariable changed, bool isUpper, Queue v.Value(s)).Average(); - float squareSum = 0; - for (int j = 0; j < vars.Length; j++) - { - squareSum += (vars[j].Value(s) - avg) * (vars[j].Value(s) - avg); - } + var actualvariance = vars.Select(v => Math.Pow(v.Value(s) - avg, 2)).Average(); - Assert.IsTrue(Math.Abs(variance.Value(s) - squareSum/vars.Length)< .00001f); + AssertApproximatelyEqual(variance.Value(s), (float)actualvariance); } } @@ -1177,11 +1173,11 @@ 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 ^ 4; + 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) * x.Value(s) * x.Value(s)); + AssertApproximatelyEqual(y.Value(s), x.Value(s) * x.Value(s)); } } @@ -1191,11 +1187,11 @@ 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 ^ 4; + var y = x ^ 6; 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)); + AssertApproximatelyEqual(y.Value(s), (float)Math.Pow(x.Value(s), 6)); } } @@ -1217,7 +1213,7 @@ public void EvenPowerConstraintTest4() public void EvenPowerConstraintTest5() { var p = new Problem(nameof(EvenPowerConstraintTest5)); - var dom = new FloatDomain("unit", 1, 50); + var dom = new FloatDomain("unit", -98, 102); var x = (FloatVariable)dom.Instantiate("x"); var y = x ^ 20; for (int i = 0; i < 100; i++) @@ -1241,6 +1237,23 @@ public void EvenPowerConstraintTest6() } } + [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)); + } + } + [TestMethod] public void FloatPredeterminationTest() { @@ -1289,7 +1302,10 @@ void AssertApproximatelyEqual(float a, float b, float tolerance = 0.0001f) { var difference = Math.Abs(a - b); var magnitude = Math.Max(Math.Abs(a), Math.Abs(b)); - Assert.IsTrue(difference / magnitude < tolerance); + if (magnitude != 0) + { + Assert.IsTrue(difference / magnitude < tolerance); + } } } } From 7f86c0b8286e6e6da7fd845c1bf9171055a59ffa Mon Sep 17 00:00:00 2001 From: annalis97 Date: Fri, 20 Aug 2021 11:45:41 -0400 Subject: [PATCH 4/5] Bounded and unbounded variance and average functions fixed --- .../SMT/Float/BinarySumConstraint.cs | 1 + CatSAT/NonBoolean/SMT/Float/FloatSolver.cs | 21 ++- CatSAT/NonBoolean/SMT/Float/FloatVariable.cs | 116 +++++++++++++++- .../SMT/Float/GeneralSumConstraint.cs | 13 +- .../NonBoolean/SMT/Float/MonotoneFunction.cs | 2 + .../NonBoolean/SMT/Float/PowerConstraint.cs | 37 +++-- Tests/SMT.cs | 126 +++++++++++++----- 7 files changed, 244 insertions(+), 72 deletions(-) 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/FloatSolver.cs b/CatSAT/NonBoolean/SMT/Float/FloatSolver.cs index 26b03a9..00436aa 100644 --- a/CatSAT/NonBoolean/SMT/Float/FloatSolver.cs +++ b/CatSAT/NonBoolean/SMT/Float/FloatSolver.cs @@ -83,10 +83,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; @@ -277,12 +277,19 @@ private void ResetAll() private bool TrySample() { Random.Shuffle(representatives); - foreach (var v in representatives) + var end = representatives.Count - 1; + for (var i = 0; i < end; i++) { - if (v.DontPick) + if (representatives[i].PickLast) { - continue; + var temp = representatives[end]; + representatives[end] = representatives[i]; + representatives[i] = temp; } + } + + foreach (var v in representatives) + { if (v.FloatDomain.Quantization == 0) { diff --git a/CatSAT/NonBoolean/SMT/Float/FloatVariable.cs b/CatSAT/NonBoolean/SMT/Float/FloatVariable.cs index fa92d20..533a557 100644 --- a/CatSAT/NonBoolean/SMT/Float/FloatVariable.cs +++ b/CatSAT/NonBoolean/SMT/Float/FloatVariable.cs @@ -151,7 +151,10 @@ internal static void Equate(FloatVariable v1, FloatVariable v2) /// internal readonly int Index; - internal bool DontPick; + /// + /// If true, result of an operation to be propogated last by solver. + /// + internal bool PickLast; private string DebugValueString => Bounds.IsUnique ? Bounds.Lower.ToString(CultureInfo.InvariantCulture) : Bounds.ToString(); @@ -464,6 +467,7 @@ internal bool BoundBelow(float bound, Queue> q, bool v1.FloatDomain.Bounds.Lower + v2.FloatDomain.Bounds.Lower, v1.FloatDomain.Bounds.Upper + v2.FloatDomain.Bounds.Upper, FunctionalConstraint.CombineConditions(v1.Condition, v2.Condition)); + sum.PickLast = true; sumTable[(v1, v2)] = sum; Problem.Current.Assert(Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, "IsSum", sum, v1, v2))); return sum; @@ -493,6 +497,7 @@ internal bool BoundBelow(float bound, Queue> q, bool { 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)); + difference.PickLast = true; Problem.Current.Assert(Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, "IsSum", v1, v2, difference))); return difference; } @@ -577,13 +582,13 @@ internal bool BoundBelow(float bound, Queue> q, bool { return MonotoneFunctionConstraint.MonotoneFunction($"^{c}", x => (float)Math.Pow(x, c), y => (float)-Math.Pow(y, 1.0 / c), false, v); } - + else { var upper = Math.Max((float)Math.Pow(v.FloatDomain.Bounds.Lower, c), (float)Math.Pow(v.FloatDomain.Bounds.Upper, c)); var pow = new FloatVariable($"{v.Name}^{c}", 0, v.FloatDomain.Bounds.Upper, FunctionalConstraint.CombineConditions(v.Condition, v.Condition)); - - pow.DontPick = true; + + pow.PickLast = true; Problem.Current.Assert(Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, "IsPower", pow, v, c))); return pow; @@ -737,16 +742,100 @@ public static FloatVariable Average(params FloatVariable[] vars) var av = new FloatVariable("average", newDomain.Bounds.Lower * 1f / vars.Length, newDomain.Bounds.Upper * 1f / vars.Length, null); - av.FloatDomain.Quantization = (vars[0].Quantization * 1f / vars.Length); + 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, 1f / vars.Length, vars))); + "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; + + 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)) + throw new ArgumentException("Average does not support conditioned variables", a.Name.ToString()); + + 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); + } + + Problem.Current.Assert( + Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, + "IsAverage", constrainedAvg, 1.0f / vars.Length, vars))); + + return constrainedAvg; + } + + else + { + Problem.Current.Assert( + Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, + "IsAverage", av, 1.0f / vars.Length, vars))); + + return av; + } + } + /// /// Computes the variance of the specified FloatVariables /// @@ -755,10 +844,23 @@ public static FloatVariable Average(params FloatVariable[] 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 mean = FloatVariable.Average(vars); + var mean = Average(vars); return FloatVariable.Average(vars.Select(v => (v - mean)^2 ).ToArray()); } + /// + /// Computes the variance of the specified FloatVariables + /// + /// Interval for variance to be constrained between + /// Variables to find 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 constraint, params FloatVariable[] vars) + { + var mean = Average(vars); + return FloatVariable.Average(constraint, vars.Select(v => (v - mean) ^ 2).ToArray()); + } + internal void AddUpperBound(FloatVariable bound) { if (UpperVariableBounds == null) 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/MonotoneFunction.cs b/CatSAT/NonBoolean/SMT/Float/MonotoneFunction.cs index 415eb7d..0c00afb 100644 --- a/CatSAT/NonBoolean/SMT/Float/MonotoneFunction.cs +++ b/CatSAT/NonBoolean/SMT/Float/MonotoneFunction.cs @@ -35,6 +35,7 @@ public static FloatVariable MonotoneFunction(string name, Func fun 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); + output.PickLast = true; AddConstraint(name, function, inverseFunction, increasing, input, output); return output; } @@ -63,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 index d77be85..ec7f9a2 100644 --- a/CatSAT/NonBoolean/SMT/Float/PowerConstraint.cs +++ b/CatSAT/NonBoolean/SMT/Float/PowerConstraint.cs @@ -4,10 +4,19 @@ 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) @@ -17,6 +26,7 @@ public override void Initialize(Problem p) num = (FloatVariable)c.Args[1]; exponent = (uint)c.Args[2]; num.AddFunctionalConstraint(this); + Result.PickLast = true; base.Initialize(p); } @@ -24,27 +34,12 @@ public override bool Propagate(FloatVariable changed, bool isUpper, Queue v.Value(s)).Sum(); - Assert.IsTrue(Math.Abs(sum.Value(s) - realSum) < 0.00001f); + AssertApproximatelyEqual(sum.Value(s), realSum); } } @@ -243,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); } } @@ -261,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)); } } @@ -300,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)); } } @@ -318,7 +318,7 @@ 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)); } } @@ -337,7 +337,7 @@ public void UnsignedDivisionConstraintTest() { var s = p.Solve(); Console.WriteLine(s.Model); - Assert.IsTrue(Math.Abs(quotient.Value(s) - (x.Value(s) / y.Value(s))) < 0.00001f); + AssertApproximatelyEqual(quotient.Value(s), x.Value(s) / y.Value(s)); } } @@ -354,7 +354,7 @@ public void SignedDifferenceTest() { var s = p.Solve(); Console.WriteLine(s.Model); - Assert.IsTrue(Math.Abs(diff.Value(s) - (x.Value(s) - y.Value(s))) < 0.00001f); + AssertApproximatelyEqual(diff.Value(s), (x.Value(s) - y.Value(s))); } } @@ -373,7 +373,7 @@ public void SignedQuotientTest() { var s = p.Solve(); Console.WriteLine(s.Model); - Assert.IsTrue(Math.Abs(diff.Value(s) - (x.Value(s) / y.Value(s))) < 0.00001f); + AssertApproximatelyEqual(diff.Value(s), (x.Value(s) / y.Value(s))); } } @@ -390,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)); } } @@ -512,7 +512,7 @@ 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)); } } @@ -587,7 +587,7 @@ public void SquareTableTest() for (int i = 0; i < 100; i++) { var s = problem.Solve(); - 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)); } } @@ -684,7 +684,7 @@ public void QuantizedSumTest() var s = p.Solve(); Console.WriteLine(s.Model); CheckVariables(s,x,y,sum); - 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))); } } @@ -754,7 +754,7 @@ public void QuantizedSumConstraintTest() var s = p.Solve(); Console.WriteLine(s.Model); CheckVariables(s, sum, x, y); - 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))); } } @@ -773,7 +773,7 @@ public void QuantizedProductTest() var s = p.Solve(); Console.WriteLine(s.Model); CheckVariables(s, prod, x, y); - Assert.IsTrue(Math.Abs(prod.Value(s) - (x.Value(s) * y.Value(s))) < 0.00001f); + AssertApproximatelyEqual(prod.Value(s), (x.Value(s) * y.Value(s))); } } @@ -791,7 +791,7 @@ public void QuantizedSelfDivTest() var s = p.Solve(); Console.WriteLine(s.Model); CheckVariables(s, div, x); - Assert.IsTrue(Math.Abs(div.Value(s) - (x.Value(s) / x.Value(s))) < 0.00001f); + AssertApproximatelyEqual(div.Value(s), (x.Value(s) / x.Value(s))); } } @@ -808,7 +808,7 @@ public void QuantizedSelfSubtractionTest() var s = p.Solve(); Console.WriteLine(s.Model); CheckVariables(s, diff, x); - Assert.IsTrue(Math.Abs(diff.Value(s) - (x.Value(s) - x.Value(s))) < 0.00001f); + AssertApproximatelyEqual(diff.Value(s), (x.Value(s) - x.Value(s))); } } @@ -826,7 +826,7 @@ public void QuantizedNaiveSquareTest() var s = p.Solve(); Console.WriteLine(s.Model); CheckVariables(s, square, x); - 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)); } } @@ -845,7 +845,7 @@ public void GeneralQuantizedSumConstraintTest() 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); } } @@ -864,7 +864,7 @@ public void GeneralQuantizedSumConstraintTest2() 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); } } @@ -883,7 +883,7 @@ public void GeneralQuantizedSumConstraintTest3() 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); } } @@ -902,7 +902,7 @@ public void QuantizedAverageConstraintTest() 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); } } @@ -980,7 +980,7 @@ public void NewAverageTest() var s = p.Solve(); var avg = vars.Select(v => v.Value(s)).Average(); - Assert.IsTrue(Math.Abs(average.Value(s) - avg) < .00001f); + AssertApproximatelyEqual(average.Value(s), avg); } } @@ -1041,6 +1041,70 @@ public void VarianceTest() } + [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(); + var avg = vars.Select(v => v.Value(s)).Average(); + var actualvariance = vars.Select(v => Math.Pow(v.Value(s) - avg, 2)).Average(); + + AssertApproximatelyEqual(variance.Value(s), (float)actualvariance); + } + + } + + [TestMethod] + public void BoundedAverageConstraintTest() + { + var p = new Problem(nameof(BoundedAverageConstraintTest)); + 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 constraint = new Interval(0.5f, 0.75f); + var average = FloatVariable.Average(constraint, 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); + Assert.IsTrue(average.Value(s) >= 0.5 && average.Value(s) <= 0.75); + } + } + + [TestMethod] + public void BoundedVarianceTest() + { + var p = new Problem(nameof(BoundedVarianceTest)); + 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 constraint = new Interval(-5f, 1f); + var variance = FloatVariable.Variance(constraint, vars); + + for (int i = 0; i < 5; i++) + { + var s = p.Solve(); + var avg = vars.Select(v => v.Value(s)).Average(); + var actualvariance = vars.Select(v => Math.Pow(v.Value(s) - avg, 2)).Average(); + + Assert.IsTrue(variance.Value(s) >= -5f && variance.Value(s) <= 1f); + + } + } + [TestMethod] public void SquareTest() { @@ -1052,7 +1116,7 @@ public void SquareTest() for (int i = 0; i < 100; i++) { var s = problem.Solve(); - 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)); } } @@ -1064,7 +1128,7 @@ public void MonotoneSumConstraintTest() var x = (FloatVariable)dom.Instantiate("x"); var sum = x + 3; var s = p.Solve(); - Assert.IsTrue(Math.Abs(sum.Value(s) - (x.Value(s) + 3)) < 0.00001f); + AssertApproximatelyEqual(sum.Value(s), (x.Value(s) + 3)); } [TestMethod] @@ -1075,7 +1139,7 @@ public void MonotoneSumConstraintTest2() var x = (FloatVariable)dom.Instantiate("x"); var sum2 = 3 + x; var s = p.Solve(); - Assert.IsTrue(Math.Abs(sum2.Value(s) - (3 + x.Value(s))) < 0.00001f); + AssertApproximatelyEqual(sum2.Value(s), 3 + x.Value(s)); } [TestMethod] @@ -1086,7 +1150,7 @@ public void MonotoneQuotientConstraintTest() var x = (FloatVariable)dom.Instantiate("x"); var quotient = x / 2; var s = p.Solve(); - Assert.IsTrue(Math.Abs(quotient.Value(s) - (x.Value(s)/2)) < 0.00001f); + AssertApproximatelyEqual(quotient.Value(s), (x.Value(s) / 2)); } [TestMethod] @@ -1097,7 +1161,7 @@ public void MonotoneDifferenceConstraintTest() var x = (FloatVariable)dom.Instantiate("x"); var diff = x - 2; var s = p.Solve(); - Assert.IsTrue(Math.Abs(diff.Value(s) - (x.Value(s) - 2)) < 0.00001f); + AssertApproximatelyEqual(diff.Value(s), (x.Value(s) - 2)); } [TestMethod] @@ -1110,7 +1174,7 @@ public void SignedMonotonePowerConstraintTest() for (int i = 0; i < 100; i++) { var s = p.Solve(); - Assert.IsTrue(Math.Abs((x.Value(s) * x.Value(s) * x.Value(s)) - y.Value(s)) < .0001f); + AssertApproximatelyEqual(x.Value(s) * x.Value(s) * x.Value(s), y.Value(s)); } } @@ -1124,7 +1188,7 @@ public void MonotonePowerConstraintTest() for (int i = 0; i < 100; i++) { var s = p.Solve(); - Assert.IsTrue(Math.Abs((x.Value(s) * x.Value(s) * x.Value(s)) - y.Value(s)) < .0001f); + AssertApproximatelyEqual(x.Value(s) * x.Value(s) * x.Value(s), y.Value(s)); } } @@ -1157,7 +1221,7 @@ public void MonotonePowerValueTest3() public void EvenPowerConstraintTest() { var p = new Problem(nameof(EvenPowerConstraintTest)); - var dom = new FloatDomain("unit", -1, 2); + var dom = new FloatDomain("unit", -1, 1); var x = (FloatVariable)dom.Instantiate("x"); var y = x ^ 2; for (int i = 0; i < 100; i++) @@ -1298,7 +1362,7 @@ public void FloatPredeterminationTest() Assert.IsFalse(problem.IsPredetermined(yLTz)); } } - void AssertApproximatelyEqual(float a, float b, float tolerance = 0.0001f) + 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)); From 0f29c15dd8baff03ad7a94904fc440ed57ac318b Mon Sep 17 00:00:00 2001 From: annalis97 Date: Tue, 24 Aug 2021 17:05:47 -0400 Subject: [PATCH 5/5] Float solver completed --- CatSAT.sln.DotSettings | 1 + CatSAT/NonBoolean/SMT/Float/FloatSolver.cs | 10 +- CatSAT/NonBoolean/SMT/Float/FloatVariable.cs | 164 ++++++++++-------- CatSAT/NonBoolean/SMT/Float/Interval.cs | 27 ++- .../NonBoolean/SMT/Float/MonotoneFunction.cs | 4 +- Tests/SMT.cs | 138 +++++++++++---- 6 files changed, 220 insertions(+), 124 deletions(-) diff --git a/CatSAT.sln.DotSettings b/CatSAT.sln.DotSettings index f639bd7..504e98c 100644 --- a/CatSAT.sln.DotSettings +++ b/CatSAT.sln.DotSettings @@ -26,4 +26,5 @@ True True True + True True \ No newline at end of file diff --git a/CatSAT/NonBoolean/SMT/Float/FloatSolver.cs b/CatSAT/NonBoolean/SMT/Float/FloatSolver.cs index 00436aa..10c1815 100644 --- a/CatSAT/NonBoolean/SMT/Float/FloatSolver.cs +++ b/CatSAT/NonBoolean/SMT/Float/FloatSolver.cs @@ -45,13 +45,14 @@ class FloatSolver : TheorySolver /// private readonly Queue> propagationQueue = new Queue>(); - private static FloatVariableArrayComparer IEqualityComparer = new FloatVariableArrayComparer(); - 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(IEqualityComparer); - public Dictionary AverageTable = new Dictionary(IEqualityComparer); + 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. @@ -163,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)); } diff --git a/CatSAT/NonBoolean/SMT/Float/FloatVariable.cs b/CatSAT/NonBoolean/SMT/Float/FloatVariable.cs index 533a557..389d77a 100644 --- a/CatSAT/NonBoolean/SMT/Float/FloatVariable.cs +++ b/CatSAT/NonBoolean/SMT/Float/FloatVariable.cs @@ -22,12 +22,13 @@ // // -------------------------------------------------------------------------------------------------------------------- #endregion -using CatSAT.NonBoolean.SMT.Float; + using System; using System.Collections.Generic; using System.Diagnostics; using System.Globalization; using System.Linq; +using CatSAT.NonBoolean.SMT.Float; namespace CatSAT { @@ -89,16 +90,11 @@ public FloatVariable(object name, float low, float high, Literal condition) internal Interval SolutionBounds; // ReSharper disable once InconsistentNaming - private Interval _bounds; /// /// Current bounds to which the variable has been narrowed /// - internal Interval Bounds - { - get => _bounds; - set => _bounds = value; - } + internal Interval Bounds { get; set; } /// /// The predetermined value for the variable, if any. @@ -152,7 +148,7 @@ internal static void Equate(FloatVariable v1, FloatVariable v2) internal readonly int Index; /// - /// If true, result of an operation to be propogated last by solver. + /// If true, result of an operation to be propagated last by solver. /// internal bool PickLast; @@ -463,11 +459,11 @@ internal bool BoundBelow(float bound, Queue> q, bool { 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)); - sum.PickLast = true; + 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; @@ -496,8 +492,8 @@ internal bool BoundBelow(float bound, Queue> q, bool 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)); - difference.PickLast = true; + 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; } @@ -530,7 +526,7 @@ internal bool BoundBelow(float bound, Queue> q, bool { if (c==0) { - throw new InvalidOperationException($"Cannot divide by 0"); + throw new InvalidOperationException("Cannot divide by 0"); } return MonotoneFunctionConstraint.MonotoneFunction($"/{c}", x => x * (1 / c), y => y / (1 / c), c>0, v); @@ -558,41 +554,31 @@ internal bool BoundBelow(float bound, Queue> q, bool /// public static FloatVariable operator ^(FloatVariable v, uint c) { - if (c < 0) - { - throw new ArgumentException($"Cannot raise bounds to a negative power"); - } - if ((c % 2 != 0) || (c%2==0 && v.Bounds.Lower >=0)) { return MonotoneFunctionConstraint.MonotoneFunction($"^{c}", x => (float)Math.Pow(x, c), - y => { + y => + { if (y < 0) { return (float)-Math.Pow(-y, 1.0 / c); } - else - { - return (float)Math.Pow(y, 1.0 / c); - } + + return (float)Math.Pow(y, 1.0 / c); }, c > 0, v); } - else if (c % 2 == 0 && v.Bounds.Upper < 0) + 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); } - - else - { - var upper = Math.Max((float)Math.Pow(v.FloatDomain.Bounds.Lower, c), (float)Math.Pow(v.FloatDomain.Bounds.Upper, c)); - var pow = new FloatVariable($"{v.Name}^{c}", 0, v.FloatDomain.Bounds.Upper, FunctionalConstraint.CombineConditions(v.Condition, v.Condition)); - - pow.PickLast = true; - Problem.Current.Assert(Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, "IsPower", pow, v, c))); - return pow; - } + 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; } /// @@ -649,7 +635,7 @@ public static FloatVariable Square(FloatVariable v1) return square; } - else if (v1.FloatDomain.Bounds.Upper <= 0) + if (v1.FloatDomain.Bounds.Upper <= 0) { var square = new FloatVariable($"{v1.Name}^2", upperSq, lowerSq, FunctionalConstraint.CombineConditions(v1.Condition, v1.Condition)); squareTable[v1] = square; @@ -682,25 +668,22 @@ public static FloatVariable Sum(params FloatVariable[] vars) return s; } - else + foreach (var a in vars) { - foreach (var a in vars) - { - newDomain += a.FloatDomain.Bounds.Quantize(vars[0].Quantization); - } + newDomain += a.FloatDomain.Bounds.Quantize(vars[0].Quantization); + } - foreach (var a in vars) - if (!ReferenceEquals(a.Condition, null)) - throw new ArgumentException("Sum does not support conditioned variables", a.Name.ToString()); + foreach (var a in vars) + if (!ReferenceEquals(a.Condition, null)) + throw new ArgumentException("Sum does not support conditioned variables", a.Name.ToString()); - 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; - } + 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; } /// @@ -767,6 +750,12 @@ public static FloatVariable Average(Interval constraint, params FloatVariable[] { 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)) { @@ -811,7 +800,6 @@ public static FloatVariable Average(Interval constraint, params FloatVariable[] 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) @@ -819,21 +807,26 @@ public static FloatVariable Average(Interval constraint, params FloatVariable[] 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; } - else - { - Problem.Current.Assert( - Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, - "IsAverage", av, 1.0f / vars.Length, vars))); + Problem.Current.Assert( + Problem.Current.GetSpecialProposition(Call.FromArgs(Problem.Current, + "IsAverage", av, 1.0f / vars.Length, vars))); - return av; - } + av.PickLast = true; + + constrainedAverageTable[(constraint, vars)] = av; + + return av; } /// @@ -844,21 +837,41 @@ public static FloatVariable Average(Interval constraint, params FloatVariable[] /// 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); - return FloatVariable.Average(vars.Select(v => (v - mean)^2 ).ToArray()); + 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 variance to be constrained between - /// Variables to find variance of + /// 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 constraint, params FloatVariable[] vars) + public static FloatVariable Variance(Interval meanRange, Interval varianceRange, params FloatVariable[] vars) { - var mean = Average(vars); - return FloatVariable.Average(constraint, vars.Select(v => (v - mean) ^ 2).ToArray()); + 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) @@ -902,22 +915,24 @@ public class FloatVariableArrayComparer : IEqualityComparer /// /// Singleton instance of the comparer /// - /// - private static readonly IEqualityComparer equalityComparer; + public static readonly IEqualityComparer EqualityComparer = new FloatVariableArrayComparer(); bool IEqualityComparer.Equals(FloatVariable[] a, FloatVariable[] b) { - if (a.Length != b.Length) - { - return false; - } - - for (int i = 0; i < a.Length; i++) + if (a != null && b != null) { - if (!ReferenceEquals(a[i], b[i])) + 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; @@ -926,6 +941,7 @@ bool IEqualityComparer.Equals(FloatVariable[] a, FloatVariable[ 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(); diff --git a/CatSAT/NonBoolean/SMT/Float/Interval.cs b/CatSAT/NonBoolean/SMT/Float/Interval.cs index 3183dc6..5bf3eef 100644 --- a/CatSAT/NonBoolean/SMT/Float/Interval.cs +++ b/CatSAT/NonBoolean/SMT/Float/Interval.cs @@ -98,16 +98,6 @@ public bool Contains(float value) return Lower <= value && value <= Upper; } - public static bool operator ==(Interval a, Interval b) - { - return (a.Lower - b.Lower < .00001f && a.Upper - b.Upper < .00001f); - } - - public static bool operator !=(Interval a, Interval b) - { - return (!(a == b)); - } - /// /// The interval sum of two intervals. /// This is the interval bounding all possible sums of values taken from the original intervals. @@ -154,6 +144,10 @@ 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) @@ -234,20 +228,23 @@ public static float RoundDown(float num, float quantization) /// /// Narrow the interval to the nearest quantized values /// - public Interval Quantize(float Quantization) + public Interval Quantize(float quantization) { - if (Quantization == 0) + if (quantization == 0) { return this; } - float lowerBound = RoundUp(Lower, Quantization); - float upperBound = RoundDown(Upper, Quantization); + float lowerBound = RoundUp(Lower, quantization); + float upperBound = RoundDown(Upper, quantization); Interval newBounds = new Interval(lowerBound, upperBound); return newBounds; } - public static Interval Quantize(Interval i, float Quantization) => i.Quantize(Quantization); + /// + /// Adjust the interval as needed according to quantization + /// + public static Interval Quantize(Interval i, float quantization) => i.Quantize(quantization); /// public override string ToString() diff --git a/CatSAT/NonBoolean/SMT/Float/MonotoneFunction.cs b/CatSAT/NonBoolean/SMT/Float/MonotoneFunction.cs index 0c00afb..239cd49 100644 --- a/CatSAT/NonBoolean/SMT/Float/MonotoneFunction.cs +++ b/CatSAT/NonBoolean/SMT/Float/MonotoneFunction.cs @@ -34,8 +34,8 @@ public static FloatVariable MonotoneFunction(string name, Func fun { 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); - output.PickLast = true; + 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; } diff --git a/Tests/SMT.cs b/Tests/SMT.cs index 98f2d15..ae7f70a 100644 --- a/Tests/SMT.cs +++ b/Tests/SMT.cs @@ -696,9 +696,6 @@ public void QuantizedBoundTest() var x = (FloatVariable)dom.Instantiate("x"); - //Assert.AreEqual(x.Bounds.Upper, 70); - //Assert.AreEqual(x.Bounds.Lower, 0); - for (int i = 0; i < 100; i++) { var s = p.Solve(); @@ -979,12 +976,17 @@ public void NewAverageTest() { 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() { @@ -1025,7 +1027,7 @@ public void VarianceTest() { var p = new Problem(nameof(VarianceTest)); var dom = new FloatDomain("unit", -6, 8); - var vars = new FloatVariable[1]; + 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); @@ -1033,10 +1035,7 @@ public void VarianceTest() for (int i = 0; i < 5; i++) { var s = p.Solve(); - var avg = vars.Select(v => v.Value(s)).Average(); - var actualvariance = vars.Select(v => Math.Pow(v.Value(s) - avg, 2)).Average(); - - AssertApproximatelyEqual(variance.Value(s), (float)actualvariance); + AssertApproximatelyEqual(variance.Value(s), getVariance(s, vars)); } } @@ -1054,54 +1053,135 @@ public void VarianceTest2() for (int i = 0; i < 1; i++) { var s = p.Solve(); - var avg = vars.Select(v => v.Value(s)).Average(); - var actualvariance = vars.Select(v => Math.Pow(v.Value(s) - avg, 2)).Average(); - - AssertApproximatelyEqual(variance.Value(s), (float)actualvariance); + 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 BoundedAverageConstraintTest() + public void ConstrainedAverageTest() { - var p = new Problem(nameof(BoundedAverageConstraintTest)); + 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 constraint = new Interval(0.5f, 0.75f); - var average = FloatVariable.Average(constraint, vars); + 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(); - Console.WriteLine(s.Model); - var avg = vars.Select(v => v.Value(s)).Average(); - AssertApproximatelyEqual(average.Value(s), avg); - Assert.IsTrue(average.Value(s) >= 0.5 && average.Value(s) <= 0.75); + checkAverage(s, avg, vars); } } [TestMethod] - public void BoundedVarianceTest() + public void ConstrainedAverageTest2() { - var p = new Problem(nameof(BoundedVarianceTest)); + 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[5]; + var vars = new FloatVariable[4]; for (int i = 0; i < vars.Length; i++) vars[i] = (FloatVariable)dom.Instantiate("x" + i); - var constraint = new Interval(-5f, 1f); - var variance = FloatVariable.Variance(constraint, vars); + 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(); - var avg = vars.Select(v => v.Value(s)).Average(); - var actualvariance = vars.Select(v => Math.Pow(v.Value(s) - avg, 2)).Average(); + 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); - Assert.IsTrue(variance.Value(s) >= -5f && variance.Value(s) <= 1f); + 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))); } }