Completed float solver

CatSAT.sln.DotSettings

@@ -6,6 +6,9 @@
 	<s:Boolean x:Key="/Default/UserDictionary/Words/=Biconditional/@EntryIndexedValue">True</s:Boolean>
 	<s:Boolean x:Key="/Default/UserDictionary/Words/=disjunct/@EntryIndexedValue">True</s:Boolean>
 	<s:Boolean x:Key="/Default/UserDictionary/Words/=disjuncts/@EntryIndexedValue">True</s:Boolean>
+	<s:Boolean x:Key="/Default/UserDictionary/Words/=fixedpoint/@EntryIndexedValue">True</s:Boolean>
+	<s:Boolean x:Key="/Default/UserDictionary/Words/=fixpoint/@EntryIndexedValue">True</s:Boolean>
+
 	<s:Boolean x:Key="/Default/UserDictionary/Words/=fluents/@EntryIndexedValue">True</s:Boolean>
 	<s:Boolean x:Key="/Default/UserDictionary/Words/=Horswill/@EntryIndexedValue">True</s:Boolean>
 	<s:Boolean x:Key="/Default/UserDictionary/Words/=lits/@EntryIndexedValue">True</s:Boolean>
@@ -16,4 +19,12 @@
 	<s:Boolean x:Key="/Default/UserDictionary/Words/=Preinitialization/@EntryIndexedValue">True</s:Boolean>
 	<s:Boolean x:Key="/Default/UserDictionary/Words/=preinitialize/@EntryIndexedValue">True</s:Boolean>
 	<s:Boolean x:Key="/Default/UserDictionary/Words/=Preinitialized/@EntryIndexedValue">True</s:Boolean>
-	<s:Boolean x:Key="/Default/UserDictionary/Words/=Uncompiled/@EntryIndexedValue">True</s:Boolean></wpf:ResourceDictionary>
+	<s:Boolean x:Key="/Default/UserDictionary/Words/=Preprecess/@EntryIndexedValue">True</s:Boolean>
+
+	<s:Boolean x:Key="/Default/UserDictionary/Words/=quantizations/@EntryIndexedValue">True</s:Boolean>
+	<s:Boolean x:Key="/Default/UserDictionary/Words/=requantize/@EntryIndexedValue">True</s:Boolean>
+	<s:Boolean x:Key="/Default/UserDictionary/Words/=throw_0020new_0020Arg/@EntryIndexedValue">True</s:Boolean>
+	<s:Boolean x:Key="/Default/UserDictionary/Words/=t_002E_000D_000A_0020_0020_0020_0020_0020_0020/@EntryIndexedValue">True</s:Boolean>
+	<s:Boolean x:Key="/Default/UserDictionary/Words/=Uncompiled/@EntryIndexedValue">True</s:Boolean>
+	<s:Boolean x:Key="/Default/UserDictionary/Words/=vari/@EntryIndexedValue">True</s:Boolean>
+	<s:Boolean x:Key="/Default/UserDictionary/Words/=_0020true_003B_000D_000A_0020_0020/@EntryIndexedValue">True</s:Boolean></wpf:ResourceDictionary>

CatSAT/CatSAT.csproj

@@ -43,6 +43,9 @@
     <Reference Include="System" />
     <Reference Include="System.Core" />
     <Reference Include="System.Data" />
+    <Reference Include="System.ValueTuple, Version=4.0.3.0, Culture=neutral, PublicKeyToken=cc7b13ffcd2ddd51, processorArchitecture=MSIL">
+      <HintPath>..\packages\System.ValueTuple.4.5.0\lib\netstandard1.0\System.ValueTuple.dll</HintPath>
+    </Reference>
   </ItemGroup>
   <ItemGroup>
     <Compile Include="Fluents\Actions.cs" />
@@ -55,6 +58,7 @@
     <Compile Include="NonBoolean\SMT\Float\Interval.cs" />
     <Compile Include="NonBoolean\SMT\Float\ConstantBound.cs" />
     <Compile Include="NonBoolean\SMT\Float\MonotoneFunction.cs" />
+    <Compile Include="NonBoolean\SMT\Float\PowerConstraint.cs" />
     <Compile Include="NonBoolean\SMT\Float\ProductConstraint.cs" />
     <Compile Include="NonBoolean\SMT\Float\BinarySumConstraint.cs" />
     <Compile Include="NonBoolean\SMT\Float\VariableBound.cs" />
@@ -114,6 +118,7 @@
     <Compile Include="NonBoolean\VariableType.cs" />
   </ItemGroup>
   <ItemGroup>
+    <None Include="packages.config" />
     <None Include="Properties\Settings.settings">
       <Generator>SettingsSingleFileGenerator</Generator>
       <LastGenOutput>Settings.Designer.cs</LastGenOutput>

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);
         }
 

CatSAT/NonBoolean/SMT/Float/FloatDomain.cs

@@ -22,6 +22,9 @@
 // </copyright>
 // --------------------------------------------------------------------------------------------------------------------
 #endregion
+
+using System;
+
 namespace CatSAT.NonBoolean.SMT.Float
 {
     /// <summary>
@@ -34,6 +37,44 @@ public class FloatDomain : Domain<float>
         /// The upper and lower bounds of the domain
         /// </summary>
         public readonly Interval Bounds;
+
+        /// <summary>
+        /// If non-zero, domain consists of only integer multiples of quantization.
+        /// </summary>
+        public float Quantization;
+
+        /// <summary>
+        /// True if num is a valid element of the domain.
+        /// </summary>
+        public bool Contains(float num)
+        {
+            return ((Bounds.Contains(num)) && (Quantization == 0 || IsQuantized(num, Quantization)));
+        }
+
+        /// <summary>
+        /// True if num is an integer multiple of quantization.
+        /// </summary>
+        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);
+        }
+
+        /// <summary>
+        /// A floating-point domain, specified by upper- and lower-bounds
+        /// </summary>
+        /// <param name="name">Name of the variable</param>
+        /// <param name="lowerBound">Lower bound of the variable</param>
+        /// <param name="upperBound">Upper bound of the variable</param>
+        /// <param name="quantization">If non-zero, include only integer multiples of quantization</param>
+        public FloatDomain(string name, float lowerBound, float upperBound, float quantization) : base(name)
+        {
+            Bounds = new Interval(lowerBound, upperBound);
+            Quantization = quantization;
+        }
+
         /// <summary>
         /// A floating-point domain, specified by upper- and lower-bounds
         /// </summary>
@@ -50,5 +91,87 @@ public override Variable Instantiate(object name, Problem p, Literal condition =
         {
             return new FloatVariable(name, this, condition, p);
         }
+
+        /// <summary>
+        /// A FloatDomain constrained to be the sum of two other FloatDomains
+        /// </summary>
+        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;
+            }
+        }
+
+        /// <summary>
+        /// A FloatDomain constrained to be the difference of two other FloatDomains
+        /// </summary>
+        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;
+            }
+        }
+
+        /// <summary>
+        /// A FloatDomain constrained to be the product of two other FloatDomains
+        /// </summary>
+        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;
+            }
+        }
+
+
+
     }
 }

CatSAT/NonBoolean/SMT/Float/FloatSolver.cs

@@ -26,6 +26,8 @@
 using System.Collections;
 using System.Collections.Generic;
 using System.Linq;
+using System.Diagnostics;
+using static System.Collections.StructuralComparisons;
 
 namespace CatSAT.NonBoolean.SMT.Float
 {
@@ -38,8 +40,20 @@ class FloatSolver : TheorySolver
         // Representatives of the equivalence classes of FloatVariables
         private readonly List<FloatVariable> representatives = new List<FloatVariable>();
 
+        /// <summary>
+        /// (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.
+        /// </summary>
         private readonly Queue<Tuple<FloatVariable,bool>> propagationQueue = new Queue<Tuple<FloatVariable, bool>>();
 
+        public Dictionary<(FloatVariable, FloatVariable), FloatVariable> ProductTable = new Dictionary<(FloatVariable, FloatVariable), FloatVariable>();
+        public Dictionary<(FloatVariable, FloatVariable), FloatVariable> SumTable = new Dictionary<(FloatVariable, FloatVariable), FloatVariable>();
+        public Dictionary<FloatVariable, FloatVariable> SquareTable = new Dictionary<FloatVariable, FloatVariable>();
+        public Dictionary<FloatVariable[], FloatVariable> ArraySumTable = new Dictionary<FloatVariable[], FloatVariable>(FloatVariableArrayComparer.EqualityComparer);
+        public Dictionary<FloatVariable[], FloatVariable> AverageTable = new Dictionary<FloatVariable[], FloatVariable>(FloatVariableArrayComparer.EqualityComparer);
+        public Dictionary<(Interval, FloatVariable[]), FloatVariable> ConstrainedAverageTable = new Dictionary<(Interval, FloatVariable[]), FloatVariable>();
+        public Dictionary<FloatVariable[], FloatVariable> VarianceTable = new Dictionary<FloatVariable[], FloatVariable>(FloatVariableArrayComparer.EqualityComparer);
+        public Dictionary<(Interval, FloatVariable[]), FloatVariable> ConstrainedVarianceTable = new Dictionary<(Interval, FloatVariable[]), FloatVariable>();
+
         /// <summary>
         /// Add clauses that follow from user-defined bounds, e.g. from transitivity.
         /// </summary>
@@ -50,7 +64,7 @@ void PreprecessBounds(List<ConstantBound> constraints, int sign)
             {
                 foreach (var p in Propositions)
                     p.Validate();
-                constraints.Sort((a, b) => sign*Comparer.Default.Compare(a.Bound, b.Bound));
+                constraints.Sort((a, b) => sign * Comparer.Default.Compare(a.Bound, b.Bound));
 
                 // Add forward inferences: if v < bounds[i], then v < bounds[i+1]
                 for (int i = 0; i < constraints.Count - 1; i++)
@@ -70,10 +84,10 @@ void PreprecessBounds(List<ConstantBound> constraints, int sign)
                 // way it's possible for them to be unsatisfied with non-zero probability is through
                 // floating-point quantization.  That suggests that someone trying to make a proposition
                 // dependent on a != b+C is probably making a mistake.
-                if (v.AllFunctionalConstraints != null)
-                    foreach (var f in v.AllFunctionalConstraints)
-                        if (f.IsDependency)
-                            throw new InvalidOperationException($"{f.Name}: Inferences dependent on the truth of functional constraint are not supported.");
+                //if (v.AllFunctionalConstraints != null)
+                //    foreach (var f in v.AllFunctionalConstraints)
+                //        if (f.IsDependency)
+                //            throw new InvalidOperationException($"{f.Name}: Inferences dependent on the truth of functional constraint are not supported.");
             }
 
             return null;
@@ -114,7 +128,7 @@ public override bool Solve(Solution s)
             FindEquivalenceClasses(s);
             FindActiveFunctionalConstraints(s);
 
-            if (!FindSolutionBounds(s)) 
+            if (!FindSolutionBounds(s))
                 // Constraint are contradictory
                 return false;
 
@@ -150,6 +164,7 @@ private void FindEquivalenceClasses(Solution s)
             // We can now focus on just the representatives of each equivalence class of variables
             // and ignore the rest.
             representatives.Clear();
+            // ReSharper disable once RedundantCast
             representatives.AddRange(Variables.Where(v => v.IsDefinedInInternal(s) && (object) v == (object) v.Representative));
         }
 
@@ -246,7 +261,9 @@ private bool FindSolutionBounds(Solution s)
 
             // Save bounds
             foreach (var v in representatives)
+            {
                 v.SolutionBounds = v.Bounds;
+            }
 
             return true;
         }
@@ -262,11 +279,39 @@ private void ResetAll()
         private bool TrySample()
         {
             Random.Shuffle(representatives);
+            var end = representatives.Count - 1;
+            for (var i = 0; i < end; i++)
+            {
+                if (representatives[i].PickLast)
+                {
+                    var temp = representatives[end];
+                    representatives[end] = representatives[i];
+                    representatives[i] = temp;
+                }
+            }
+
             foreach (var v in representatives)
             {
-                v.PickRandom(propagationQueue);
+                if (v.FloatDomain.Quantization == 0)
+                {
+
+                    v.PickValue(Random.Float(v.Bounds.Lower, v.Bounds.Upper), propagationQueue);
+                }
+
+                else
+                {
+                    int possibilities = (int)((v.Bounds.Upper - v.Bounds.Lower) / v.FloatDomain.Quantization);
+
+                    // ReSharper disable once RedundantNameQualifier
+                    int randStep = CatSAT.Random.InRange(0, possibilities);
+
+                    float rand = randStep * v.FloatDomain.Quantization + v.Bounds.Lower;
+
+                    v.PickValue(rand, propagationQueue);
+                }
+
                 if (!PropagateUpdates()) 
-                    return false;
+                        return false;
             }
 
             return true;