Proof blacklisting

README.md

@@ -15,7 +15,7 @@ Requires a configuration file `configuration.json` with information for each eng
         "enabled" : true,
         "verbose": true,
         "testTimeout": 30,
-        "testCount" : 4000,        
+        "testBound" : 4000,        
         "testSorting": "Random",
         "queryComplexity": [0, 1000],
         "testsSavePath": "/path/to/file"
@@ -42,14 +42,14 @@ Requires a configuration file `configuration.json` with information for each eng
 ```
 If an `executablePath` or `parameterExpression` is omitted, the engine is expected to be hosted externally. An example of this is the `External` engine in the above configuration. Engines can optionally be marked `verbose` to print failed queries while the tests are run from [Run Tests for Engine](#run-tests-for-engine)
 
-`testTimeout`, `testCount`, `testSorting`, `queryComplexity`, and `testsSavePath` are all optional attributes.
+`testTimeout`, `testBound`, `testSorting`, `queryComplexity`, and `testsSavePath` are all optional attributes.
 `testTimeout` sets the time limit in seconds for the duration of a test (default=30).
-`testCount` limits the number of tests to execute (default=all).
-`testSorting` determines how to sort the tests if `testCount` is set. There are four different sortings:
-* `Random` (default) - Takes `testCount` generated tests randomly
-* `FILO` - Takes the last `testCount` generated tests
-* `FIFO` - Takes the first `testCount` generated tests
-* `Split` - Takes an equal split of each test-sort by RoundRobin, summing up to no more than `testCount` tests
+`testBound` sets an upper bound of the number of tests to execute (default=all).
+`testSorting` determines how to sort the tests if `testBound` is set. There are four different sortings:
+* `Random` (default) - Takes `testBound` generated tests randomly
+* `FILO` - Takes the last `testBound` generated tests
+* `FIFO` - Takes the first `testBound` generated tests
+* `Split` - Takes an equal split of each test-sort by RoundRobin, summing up to no more than `testBound` tests
 
 `queryComplexity` determines the complexity of the queries in the tests (the number of operators).
 Both the upper and lower bound can be set.

src/main/kotlin/Main.kt

@@ -5,6 +5,7 @@ import facts.RelationLoader
 import parsing.EngineConfiguration
 import parsing.Sorting
 import parsing.parseEngineConfigurations
+import proofs.ProofKind
 import proofs.addAllProofs
 import tests.Test
 import tests.testgeneration.addAllTests
@@ -104,13 +105,32 @@ private fun executeTests(engine: EngineConfiguration, tests: Collection<Test>) {
 private fun generateTests(): Collection<Test> {
     val allRelations = ProofSearcher().addAllProofs().findNewRelations(RelationLoader.relations)
     //ProofLimiter(3).limit(allRelations)
+/*
+    allRelations.forEach {
+        println(it)
+    }
+
+    println(allRelations.size)
+    println(RelationLoader.relations.size)
+ */
     return TestGenerator().addAllTests().generateTests(allRelations)
 }
 
 private fun sortTests(engine: EngineConfiguration, tests: Collection<Test>) : Collection<Test> {
     val operators = listOf("||", "\\\\", "&&", "consistency:", "refinement:")
     var out = ArrayList(tests)
 
+    println("Test count: " + out.size)
+    engine.blackList?.let { it ->
+        val blacklisting = it.sumOf {it.value}
+        println(blacklisting)
+        // TODO: Check should be fixed
+        // This removes a test even if it has only one match. Not sure if this is a desired outcome
+        out = ArrayList(out.filter { test -> test.relatedProofs and blacklisting == 0})
+        //out = ArrayList(out.filter { test -> test.relatedProofs and blacklisting != test.relatedProofs})
+    }
+    println("Test count: " + out.size)
+
     if (engine.queryComplexity != null) { //Query Complexity
         val (lower, upper) = engine.bounds()
 
@@ -121,14 +141,15 @@ private fun sortTests(engine: EngineConfiguration, tests: Collection<Test>) : Co
         })
     }
 
-    if (engine.testCount != null) {  //Count
+    if (engine.testBound != null) {  //Bound
         out = when (engine.testSorting) {
-            Sorting.FILO -> ArrayList(out.takeLast(engine.testCount))
-            Sorting.FIFO -> ArrayList(out.take(engine.testCount))
-            Sorting.RoundRobin -> getEqualTests(out, engine.testCount)
-            Sorting.Random, null -> ArrayList(out.shuffled().take(engine.testCount))
+            Sorting.FILO -> ArrayList(out.takeLast(engine.testBound))
+            Sorting.FIFO -> ArrayList(out.take(engine.testBound))
+            Sorting.RoundRobin -> getEqualTests(out, engine.testBound)
+            Sorting.Random, null -> ArrayList(out.shuffled().take(engine.testBound))
         }
     }
+
     return out
 }
 

src/main/kotlin/parsing/EngineConfiguration.kt

@@ -2,6 +2,7 @@ package parsing
 
 import com.beust.klaxon.Json
 import com.beust.klaxon.Klaxon
+import proofs.ProofKind
 import java.io.File
 import java.io.IOException
 import java.net.ServerSocket
@@ -27,7 +28,7 @@ data class EngineConfiguration (
     val addresses: List<String> = (port until port + processes).map { "${ip}:$it" },
     val ports: List<Int> = (port until port + processes).toList(),
     @Json(serializeNull = false)
-    val testCount: Int?,
+    val testBound: Int?,
     @Json(serializeNull = false)
     val testSorting: Sorting?,
     @Json(serializeNull = false)
@@ -36,6 +37,8 @@ data class EngineConfiguration (
     val deadline: Long?,
     @Json(serializeNull = false)
     val testsSavePath: String?,
+    @Json(serializeNull = false)
+    val blackList: List<ProofKind>?,
 ) {
     private var procs : MutableList<Process>? = null
     var alive : AtomicBoolean = AtomicBoolean(true)
@@ -140,7 +143,7 @@ data class EngineConfiguration (
         return path == null || parameterExpression == null
     }
 
-    public fun bounds(): Pair<Int, Int> {
+    fun bounds(): Pair<Int, Int> {
         val upper: Int; val lower: Int
         if (this.queryComplexity!!.size >= 2) {
             upper = this.queryComplexity[1]

src/main/kotlin/parsing/System.kt

@@ -3,6 +3,7 @@ package parsing
 import facts.RelationLoader.getInputs
 import facts.RelationLoader.getOutputs
 import facts.RelationLoader.prefixMap
+import proofs.ProofKind
 import java.util.*
 
 interface System {
@@ -18,6 +19,7 @@ interface System {
     var isLocallyConsistent: Optional<Boolean>
     var inputs: HashSet<String>
     var outputs: HashSet<String>
+    var relatedProofs: Int
 
     fun isKnownLocallyConsistent(): Boolean {
         return isLocallyConsistent.orElse(false)
@@ -82,6 +84,7 @@ class Component(val prefix: String, val comp: String) : System {
         get() = 0
     override var components = 1
     override var isLocallyConsistent: Optional<Boolean> = Optional.empty()
+    override var relatedProofs: Int = 0
 
 
     override fun sameAs(other: System): Boolean {
@@ -125,6 +128,8 @@ class Quotient(var T: System, var S: System) : System {
     override var notRefinesThis = HashSet<System>()
     override var thisNotRefines = HashSet<System>()
     override var parents = HashSet<System>()
+    override var relatedProofs: Int = 0
+
     override val depth: Int
         get() = 1 + (this.children.map { it.depth }.maxOrNull() ?: 0)
     override val components: Int
@@ -230,7 +235,9 @@ class Quotient(var T: System, var S: System) : System {
     override var notRefinesThis = HashSet<System>()
     override var thisNotRefines = HashSet<System>()
     override var parents = HashSet<System>()
-    override val depth: Int
+    override var relatedProofs: Int = 0
+
+        override val depth: Int
         get() = 1 + (this.children.map { it.depth }.maxOrNull() ?: 0)
     override val components: Int
         get() = children.sumOf { it.components }
@@ -332,6 +339,8 @@ class Composition : System {
     override var notRefinesThis = HashSet<System>()
     override var thisNotRefines = HashSet<System>()
     override var parents = HashSet<System>()
+    override var relatedProofs: Int = 0
+
     override val components: Int
         get() = children.sumOf { it.components }
     override val depth: Int

src/main/kotlin/proofs/ConsistentCompositions.kt

@@ -6,11 +6,15 @@ import parsing.System
 import java.util.*
 
 class ConsistentCompositions : Proof() {
+    override val kind = ProofKind.ConsistentCompositions
+
     override fun search(component: System, ctx: ProofSearcher.IterationContext) {
         if (component.isLocallyConsistent.isEmpty && component is Composition) {
             calculateConsistency(component, ctx)
+            markComp(component)
         } else if (component.isKnownLocallyConsistent() && component is Composition) {
             makeChildrenConsistent(component, ctx)
+            markComp(component)
         }
     }
 

src/main/kotlin/proofs/ConsistentRefinements.kt

@@ -5,9 +5,12 @@ import parsing.System
 import java.util.*
 
 class ConsistentRefinements : Proof() {
+    override val kind = ProofKind.ConsistentRefinements
+
     override fun search(component: System, ctx: ProofSearcher.IterationContext) {
         if (hasAnyRefinementRelations(component)) {
             makeSystemConsistent(component, ctx)
+            markComp(component)
         }
     }
 

src/main/kotlin/proofs/ContextSwitch.kt

@@ -7,6 +7,7 @@ import parsing.Quotient
 import parsing.System
 
 class ContextSwitch : Proof() {
+    override val kind = ProofKind.ContextSwitch
     //override val maxContribution: Int = 4000
     // A <= B and B <= A imply C[A] == C[B] (A can be replaced by B in any context)
     override fun search(component: System, ctx: ProofSearcher.IterationContext) {
@@ -21,7 +22,10 @@ class ContextSwitch : Proof() {
                         other.refinesThis.addAll(component.refinesThis) or
                         other.notRefinesThis.addAll(component.notRefinesThis)
 
-                if (changed) ctx.setDirty(other, this)
+                if (changed) {
+                    ctx.setDirty(other, this)
+                    markComp(other)
+                }
 
                 for (parent in component.parents.toList()) {
                     replace(component, other, parent, ctx)

src/main/kotlin/proofs/Proof.kt

@@ -5,8 +5,8 @@ import parsing.System
 
 abstract class Proof {
     var contribution: Int = 0
-
     open val maxContribution: Int = 20000
+    abstract val kind: ProofKind
 
     fun reset() {
         contribution = 0
@@ -21,5 +21,19 @@ abstract class Proof {
         }
     }
 
+    fun markComp(component: System) {
+        component.relatedProofs = component.relatedProofs or kind.value
+    }
     abstract fun search(component: System, ctx: IterationContext)
+}
+
+enum class ProofKind(val value: Int) {
+    ConsistentCompositions(1 shl 0),
+    ConsistentRefinements(1 shl 1),
+    ContextSwitch(1 shl 2),
+    QuotientRule(1 shl 3),
+    RefinementTransitivity(1 shl 4),
+    SelfRefinement(1 shl 5),
+    Theorem6Conj1(1 shl 6),
+    Theorem6Conj2(1 shl 7)
 }

src/main/kotlin/proofs/QuotientRule.kt

@@ -5,6 +5,7 @@ import parsing.Quotient
 import parsing.System
 
 class QuotientRule : Proof() {
+    override val kind = ProofKind.QuotientRule
     //override val maxContribution: Int = 1000
     //Quotient rule: S || T ≤ X iff? S ≤ X \\ T
     override fun search(component: System, ctx: ProofSearcher.IterationContext) {
@@ -16,30 +17,34 @@ class QuotientRule : Proof() {
                 val children = composition.toHashSet()
                 children.remove(T)
 
-                val S = if (children.size==1) {
+                val s = if (children.size==1) {
                     ctx.addNewComponent(children.first())
                 } else {
                     ctx.addNewComponent(Composition(children))
                 }
 
-                S?.let{
+                s?.let{
 
                     for (X in S_comp_T.thisRefines) {
                         val X_quotient_T = ctx.addNewComponent(Quotient(X, T)) // X \\ T
                         X_quotient_T?.let{
 
-                        if (S.refines(X_quotient_T)) {
+                        if (s.refines(X_quotient_T)) {
                             ctx.setDirty(X_quotient_T, this)
-                            ctx.setDirty(S, this)
+                            ctx.setDirty(s, this)
+                            markComp(X_quotient_T)
+                            markComp(s)
                         }}
                     }
 
                     for (X in S_comp_T.thisNotRefines) {
                         val X_quotient_T = ctx.addNewComponent(Quotient(X, T)) // X \\ T
                         X_quotient_T?.let{
-                        if (S.notRefines(X_quotient_T)) {
+                        if (s.notRefines(X_quotient_T)) {
                             ctx.setDirty(X_quotient_T, this)
-                            ctx.setDirty(S, this)
+                            ctx.setDirty(s, this)
+                            markComp(X_quotient_T)
+                            markComp(s)
                         }}
                     }
                 }

src/main/kotlin/proofs/RefinementTransitivity.kt

@@ -4,6 +4,8 @@ import ProofSearcher
 import parsing.System
 
 class RefinementTransitivity : Proof() {
+    override val kind = ProofKind.RefinementTransitivity
+
     override fun search(component: System, ctx: ProofSearcher.IterationContext) {
         for (lhs in component.refinesThis) {
             if (component.inputs.containsAll(lhs.inputs) && component.outputs == lhs.outputs){ // S1 inputs ⊆ S2 inputs and S1 outputs = S2 outputs
@@ -20,6 +22,8 @@ class RefinementTransitivity : Proof() {
         if (lhs.refines(rhs)) {
             ctx.setDirty(lhs, this)
             ctx.setDirty(rhs, this)
+            markComp(lhs)
+            markComp(rhs)
         }
     }
 }

src/main/kotlin/proofs/SelfRefinement.kt

@@ -4,6 +4,7 @@ import ProofSearcher
 import parsing.System
 
 class SelfRefinement : Proof() {
+    override val kind = ProofKind.SelfRefinement
     override fun search(component: System, ctx: ProofSearcher.IterationContext) {
         if (hasAnyRefinementRelations(component)) { //E.g. the component is assumed to be consistent
             makeSelfRefining(component, ctx)
@@ -13,6 +14,7 @@ class SelfRefinement : Proof() {
     private fun makeSelfRefining(component: System, ctx: ProofSearcher.IterationContext) {
         if (component.refines(component)) {
             ctx.setDirty(component, this)
+            markComp(component)
         }
     }
 

src/main/kotlin/proofs/Theorem6Conj1.kt

@@ -6,6 +6,8 @@ import parsing.Conjunction
 import parsing.System
 
 class Theorem6Conj1 : Proof() {
+    override val kind = ProofKind.Theorem6Conj1
+
     //HSCC.Theorem6.part1, locally consistent S and T sharing the same alphabet : S ∧ T ≤ S and S ∧ T ≤ T (∧ is the same as &&)
     override fun search(component: System, ctx: ProofSearcher.IterationContext) {
         //TODO: we cant currently apply this to compositions because the ConsistentCompositions adds too many
@@ -37,6 +39,7 @@ class Theorem6Conj1 : Proof() {
         for (child in parent.children) {
             if (parent.refines(child)) {
                 ctx.setDirty(child, this)
+                markComp(child)
             }
         }
     }

src/main/kotlin/proofs/Theorem6Conj2.kt

@@ -5,6 +5,7 @@ import parsing.Conjunction
 import parsing.System
 
 class Theorem6Conj2 : Proof() {
+    override val kind = ProofKind.Theorem6Conj2
     //HSCC.Theorem6.part2, locally consistent S, U and T sharing the same alphabet: (U <= S) and (U <= T) implies U <= (S && T)
     override fun search(component: System, ctx: ProofSearcher.IterationContext) {
         if (component.thisRefines.size > 1) {
@@ -20,6 +21,8 @@ class Theorem6Conj2 : Proof() {
                         if (component.refines(newComp)) {
                             ctx.setDirty(newComp, this)
                             ctx.setDirty(component, this)
+                            markComp(newComp)
+                            markComp(component)
                         }}
                     }
                 }

src/main/kotlin/tests/ImplicationTest.kt

@@ -3,16 +3,16 @@ package tests
 import TestResult
 
 //This test acts like the implication logical operator i.e. precondition -> mainTest
-class ImplicationTest(precondition: SingleTest, mainTest: SingleTest) :
+class ImplicationTest(precondition: SingleTest, mainTest: SingleTest, relatedProofs: Int) :
     MultiTest(
         mainTest.testSuite,
         mainTest.projectPath,
         "(${precondition.query}) implies (${mainTest.query})",
-        precondition, mainTest
+        relatedProofs, precondition, mainTest
     ) {
 
     override fun toSingleTest(): SingleTest {
-        return SatisfiedTest(this.testSuite, this.projectPath, this.query)
+        return SatisfiedTest(this.testSuite, this.projectPath, this.query, this.relatedProofs)
     }
 
     override fun getResult(results: List<TestResult>): TestResult {