added a couple of fuzz tests for FVI - mostly out of paranoia. All se…

…ems okay..
sdcondon · Oct 20, 2024 · 7f4f2b5 · 7f4f2b5
1 parent c9f33d6
commit 7f4f2b5
Showing 1 changed file with 109 additions and 13 deletions.
diff --git a/src/SCFirstOrderLogic.Tests/ClauseIndexing/FeatureVectorIndexTests.cs b/src/SCFirstOrderLogic.Tests/ClauseIndexing/FeatureVectorIndexTests.cs
@@ -31,38 +31,74 @@ public static class FeatureVectorIndexTests
     public static Test GetSubsumedBehaviour => TestThat
         .GivenEachOf(() =>
         {
+            var index = new FeatureVectorIndex<OccurenceCountFeature>(
+                OccurenceCountFeature.MakeFeatureVector,
+                new FeatureVectorIndexListNode<OccurenceCountFeature, CNFClause>(OccurenceCountFeature.MakeFeatureComparer(Comparer<object>.Default)),
+                AllNonEmptyClausesFromSubsumptionFacts);
+
             return AllNonEmptyClausesFromSubsumptionFacts
-                .Select(c => new GetTestCase(c, GetSubsumedClausesFromSubsumptionFacts(c), GetNonSubsumedClausesFromSubsumptionFacts(c)));
+                .Select(c => new GetTestCase(index, c, GetSubsumedClausesFromSubsumptionFacts(c), GetNonSubsumedClausesFromSubsumptionFacts(c)));
         })
-        .When(tc =>
+        .When(tc => tc.Index.GetSubsumed(tc.Query))
+        .ThenReturns()
+        .And((tc, rv) => tc.Expected.Should().BeSubsetOf(rv))
+        .And((tc, rv) => rv.Should().NotIntersectWith(tc.NotExpected));
+
+    public static Test GetSubsumingBehaviour => TestThat
+        .GivenEachOf(() =>
         {
             var index = new FeatureVectorIndex<OccurenceCountFeature>(
                 OccurenceCountFeature.MakeFeatureVector,
                 new FeatureVectorIndexListNode<OccurenceCountFeature, CNFClause>(OccurenceCountFeature.MakeFeatureComparer(Comparer<object>.Default)),
                 AllNonEmptyClausesFromSubsumptionFacts);
-            return index.GetSubsumed(tc.Query);
+
+            return AllNonEmptyClausesFromSubsumptionFacts
+                .Select(c => new GetTestCase(index, c, GetSubsumingClausesFromSubsumptionFacts(c), GetNonSubsumingClausesFromSubsumptionFacts(c)));
         })
+        .When(tc => tc.Index.GetSubsuming(tc.Query))
         .ThenReturns()
         .And((tc, rv) => tc.Expected.Should().BeSubsetOf(rv))
         .And((tc, rv) => rv.Should().NotIntersectWith(tc.NotExpected));
 
-    public static Test GetSubsumingBehaviour => TestThat
+    public static Test GetSubsumingBehaviourFuzz => TestThat
         .GivenEachOf(() =>
         {
-            return AllNonEmptyClausesFromSubsumptionFacts
-                .Select(c => new GetTestCase(c, GetSubsumingClausesFromSubsumptionFacts(c), GetNonSubsumingClausesFromSubsumptionFacts(c)));
+            var content = Enumerable.Range(0, 100)
+                .Select(i => MakeRandomClause())
+                .Distinct(new VariableIdIgnorantEqualityComparer())
+                .ToArray();
+
+            var index = new FeatureVectorIndex<OccurenceCountFeature>(
+                OccurenceCountFeature.MakeFeatureVector,
+                new FeatureVectorIndexListNode<OccurenceCountFeature, CNFClause>(OccurenceCountFeature.MakeFeatureComparer(Comparer<object>.Default)),
+                content);
+
+            return content
+                .Select(c => new GetTestCaseExact(index, c, content.Where(o => o.Subsumes(c))));
         })
-        .When(tc =>
+        .When(tc => tc.Index.GetSubsuming(tc.Query))
+        .ThenReturns()
+        .And((tc, rv) => rv.Should().BeEquivalentTo(tc.Expected));
+
+    public static Test GetSubsumedBehaviourFuzz => TestThat
+        .GivenEachOf(() =>
         {
+            var content = Enumerable.Range(0, 100)
+                .Select(i => MakeRandomClause())
+                .Distinct(new VariableIdIgnorantEqualityComparer())
+                .ToArray();
+
             var index = new FeatureVectorIndex<OccurenceCountFeature>(
                 OccurenceCountFeature.MakeFeatureVector,
                 new FeatureVectorIndexListNode<OccurenceCountFeature, CNFClause>(OccurenceCountFeature.MakeFeatureComparer(Comparer<object>.Default)),
-                AllNonEmptyClausesFromSubsumptionFacts);
-            return index.GetSubsuming(tc.Query);
+                content);
+
+            return content
+                .Select(c => new GetTestCaseExact(index, c, content.Where(o => o.IsSubsumedBy(c))));
         })
+        .When(tc => tc.Index.GetSubsumed(tc.Query))
         .ThenReturns()
-        .And((tc, rv) => tc.Expected.Should().BeSubsetOf(rv))
-        .And((tc, rv) => rv.Should().NotIntersectWith(tc.NotExpected));
+        .And((tc, rv) => rv.Should().BeEquivalentTo(tc.Expected));
 
     private static IEnumerable<CNFClause> AllNonEmptyClausesFromSubsumptionFacts => SubsumptionFacts
         .All
@@ -146,7 +182,67 @@ private static CNFClause[] GetNonSubsumingClausesFromSubsumptionFacts(CNFClause
             .ToArray();
     }
 
-    private record GetTestCase(CNFClause Query, CNFClause[] Expected, CNFClause[] NotExpected);
+    private static CNFClause MakeRandomClause()
+    {
+        return new CNFClause(Enumerable
+            .Range(0, Random.Shared.Next(1, 2))
+            .Select(i => new Literal(MakeRandomLiteral())));
+
+        Sentence MakeRandomLiteral()
+        {
+            return Random.Shared.Next(1, 12) switch
+            {
+                1 => P(),
+                2 => !P(),
+                3 => Q(),
+                4 => !Q(),
+                5 => P(MakeRandomTerm()),
+                6 => !P(MakeRandomTerm()),
+                7 => P(MakeRandomTerm(), MakeRandomTerm()),
+                8 => !P(MakeRandomTerm(), MakeRandomTerm()),
+                9 => Q(MakeRandomTerm()),
+                10 => !Q(MakeRandomTerm()),
+                11 => Q(MakeRandomTerm(), MakeRandomTerm()),
+                12 => !Q(MakeRandomTerm(), MakeRandomTerm()),
+                _ => throw new Exception()
+            };
+        }
+
+        Term MakeRandomTerm()
+        {
+            return Random.Shared.Next(1, 14) switch
+            {
+                1 => C,
+                2 => D,
+                3 => F(),
+                4 => G(),
+                5 => U,
+                6 => V,
+                7 => W,
+                8 => X,
+                9 => Y,
+                10 => Z,
+                11 => F(MakeRandomTerm()),
+                12 => F(MakeRandomTerm(), MakeRandomTerm()),
+                13 => G(MakeRandomTerm()),
+                14 => H(MakeRandomTerm(), MakeRandomTerm()),
+                _ => throw new Exception()
+            };
+        }
+    }
+
+    private record GetTestCase(
+        FeatureVectorIndex<OccurenceCountFeature> Index,
+        CNFClause Query,
+        IEnumerable<CNFClause> Expected,
+        IEnumerable<CNFClause> NotExpected);
+
+    private record GetTestCaseExact(
+        FeatureVectorIndex<OccurenceCountFeature> Index,
+        CNFClause Query,
+        IEnumerable<CNFClause> Expected);
 
-    private record AddTestCase(CNFClause[] PriorContent, CNFClause Add);
+    private record AddTestCase(
+        CNFClause[] PriorContent,
+        CNFClause Add);
 }