cvc5: Extracted global cache for forking context and delegated to KCvc5ForkingSolverManager

dee-tree · dee-tree · commit e89ec8f665d0 · 2023-07-27T18:48:08.000+03:00
diff --git a/ksmt-cvc5/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Context.kt b/ksmt-cvc5/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Context.kt
@@ -32,20 +32,24 @@ import io.ksmt.sort.KSortVisitor
 import io.ksmt.sort.KUninterpretedSort
 import java.util.TreeMap
 
-class KCvc5Context private constructor(
+class KCvc5Context internal constructor(
     private val solver: Solver,
+    /**
+     * Used as context for expressions lifetime separation.
+     * Exprs which stored in [KCvc5Context], created with [mkExprSolver]
+     */
     val mkExprSolver: Solver,
     private val ctx: KContext,
-    parent: KCvc5Context?,
-    val isForking: Boolean
+    forkingSolverManager: KCvc5ForkingSolverManager? = null
 ) : AutoCloseable {
-    constructor(solver: Solver, mkExprSolver: Solver, ctx: KContext, isForking: Boolean = false)
-        : this(solver, mkExprSolver, ctx, null, isForking)
+    constructor(solver: Solver, mkExprSolver: Solver, ctx: KContext)
+        : this(solver, mkExprSolver, ctx, null)
 
-    constructor(solver: Solver, ctx: KContext, isForking: Boolean = false)
-        : this(solver, solver, ctx, null, isForking)
+    constructor(solver: Solver, ctx: KContext)
+        : this(solver, solver, ctx, null)
 
     private var isClosed = false
+    val isForking = forkingSolverManager != null
 
     private val uninterpretedSortCollector = KUninterpretedSortCollector(this)
     private var exprCurrentLevelCacheRestorer = KCurrentScopeExprCacheRestorer(uninterpretedSortCollector, ctx)
@@ -72,14 +76,11 @@ class KCvc5Context private constructor(
      *  that is in global cache, but whose sorts / decls have been erased after pop()
      *  (and put this expr to the cache of current accumulated scope)
      */
-    private val currentAccumulatedScopeExpressions: HashMap<KExpr<*>, Term>
+    private val currentAccumulatedScopeExpressions = HashMap<KExpr<*>, Term>()
     private val expressions: HashMap<KExpr<*>, Term>
 
     /**
      * We can't use HashMap with Term and Sort (hashcode is not implemented)
-     *
-     * Avoid to close cache explicitly due to its sharing between forking hierarchy.
-     * It will be garbage collected on last solver close in forking hierarchy
      */
     private val cvc5Expressions: TreeMap<Term, KExpr<*>>
     private val sorts: HashMap<KSort, Sort>
@@ -102,28 +103,26 @@ class KCvc5Context private constructor(
 
     init {
         if (isForking) {
-            uninterpretedSorts = (parent?.uninterpretedSorts as? ScopedLinkedFrame)?.fork()
-                ?: ScopedLinkedFrame(::HashSet, ::HashSet)
-            declarations = (parent?.declarations as? ScopedLinkedFrame)?.fork()
-                ?: ScopedLinkedFrame(::HashSet, ::HashSet)
+            uninterpretedSorts = ScopedLinkedFrame(::HashSet, ::HashSet)
+            declarations = ScopedLinkedFrame(::HashSet, ::HashSet)
         } else {
             uninterpretedSorts = ScopedArrayFrame(::HashSet)
             declarations = ScopedArrayFrame(::HashSet)
         }
 
-        if (parent != null) {
-            currentAccumulatedScopeExpressions = parent.currentAccumulatedScopeExpressions.toMap(HashMap())
-            expressions = parent.expressions
-            cvc5Expressions = parent.cvc5Expressions
-            sorts = parent.sorts
-            cvc5Sorts = parent.cvc5Sorts
-            decls = parent.decls
-            cvc5Decls = parent.cvc5Decls
-            uninterpretedSortValueDescriptors = parent.uninterpretedSortValueDescriptors
-            uninterpretedSortValueInterpreter = parent.uninterpretedSortValueInterpreter
-            uninterpretedSortValues = parent.uninterpretedSortValues
+        if (forkingSolverManager != null) {
+            with(forkingSolverManager) {
+                expressions = findExpressionsCache()
+                cvc5Expressions = findExpressionsReversedCache()
+                sorts = findSortsCache()
+                cvc5Sorts = findSortsReversedCache()
+                decls = findDeclsCache()
+                cvc5Decls = findDeclsReversedCache()
+                uninterpretedSortValueDescriptors = findUninterpretedSortsValueDescriptors()
+                uninterpretedSortValueInterpreter = findUninterpretedSortsValueInterpretersCache()
+                uninterpretedSortValues = findUninterpretedSortValues()
+            }
         } else {
-            currentAccumulatedScopeExpressions = HashMap()
             expressions = HashMap()
             cvc5Expressions = TreeMap()
             sorts = HashMap()
@@ -155,12 +154,18 @@ class KCvc5Context private constructor(
     val isActive: Boolean
         get() = !isClosed
 
-    fun fork(solver: Solver, mkExprSolver: Solver): KCvc5Context =
-        KCvc5Context(solver, mkExprSolver, ctx, this, true).also { forkCtx ->
+    fun fork(solver: Solver, forkingSolverManager: KCvc5ForkingSolverManager): KCvc5Context {
+        require(isForking) { "Can't fork non-forking context" }
+        return KCvc5Context(solver, mkExprSolver, ctx, forkingSolverManager).also { forkCtx ->
+            forkCtx.currentAccumulatedScopeExpressions += currentAccumulatedScopeExpressions
+            (forkCtx.uninterpretedSorts as ScopedLinkedFrame).fork(uninterpretedSorts as ScopedLinkedFrame)
+            (forkCtx.declarations as ScopedLinkedFrame).fork(declarations as ScopedLinkedFrame)
+
             repeat(assertedConstraintLevels.size) {
                 forkCtx.pushAssertionLevel()
             }
         }
+    }
 
     fun push() {
         declarations.push()
@@ -262,7 +267,7 @@ class KCvc5Context private constructor(
      *
      * todo: precise uninterpreted sort values tracking
      * */
-    private data class UninterpretedSortValueDescriptor(
+    internal data class UninterpretedSortValueDescriptor(
         val value: KUninterpretedSortValue,
         val nativeUniqueValueDescriptor: Term,
         val nativeValueTerm: Term
@@ -414,6 +419,18 @@ class KCvc5Context private constructor(
         isClosed = true
 
         currentAccumulatedScopeExpressions.clear()
+
+        if (!isForking) {
+            expressions.clear()
+            cvc5Expressions.clear()
+            sorts.clear()
+            cvc5Sorts.clear()
+            decls.clear()
+            cvc5Decls.clear()
+            uninterpretedSortValueDescriptors.clear()
+            uninterpretedSortValueInterpreter.clear()
+            uninterpretedSortValues.clear()
+        }
     }
 
     class KUninterpretedSortCollector(private val cvc5Ctx: KCvc5Context) : KSortVisitor<Unit> {
diff --git a/ksmt-cvc5/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ForkingSolver.kt b/ksmt-cvc5/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ForkingSolver.kt
@@ -16,29 +16,27 @@ open class KCvc5ForkingSolver internal constructor(
     ctx: KContext,
     private val manager: KCvc5ForkingSolverManager,
     /** store reference on Solver to separate lifetime of native expressions */
-    private val mkExprSolver: Solver,
+    mkExprSolver: Solver,
     parent: KCvc5ForkingSolver? = null
 ) : KCvc5SolverBase(ctx), KForkingSolver<KCvc5SolverConfiguration>, KSolver<KCvc5SolverConfiguration> {
 
     final override val cvc5Ctx: KCvc5Context
     private val isChild = parent != null
     private var assertionsInitiated = !isChild
 
-    private val trackedAssertions: ScopedLinkedFrame<TreeMap<Term, KExpr<KBoolSort>>>
-    private val cvc5Assertions: ScopedLinkedFrame<TreeSet<Term>>
+    private val trackedAssertions = ScopedLinkedFrame<TreeMap<Term, KExpr<KBoolSort>>>(::TreeMap, ::TreeMap)
+    private val cvc5Assertions = ScopedLinkedFrame<TreeSet<Term>>(::TreeSet, ::TreeSet)
 
     override val currentScope: UInt
         get() = trackedAssertions.currentScope
 
     init {
         if (parent != null) {
-            cvc5Ctx = parent.cvc5Ctx.fork(solver, this.mkExprSolver)
-            trackedAssertions = parent.trackedAssertions.fork()
-            cvc5Assertions = parent.cvc5Assertions.fork()
+            cvc5Ctx = parent.cvc5Ctx.fork(solver, manager)
+            trackedAssertions.fork(parent.trackedAssertions)
+            cvc5Assertions.fork(parent.cvc5Assertions)
         } else {
-            cvc5Ctx = KCvc5Context(solver, this.mkExprSolver, ctx, true)
-            trackedAssertions = ScopedLinkedFrame(::TreeMap, ::TreeMap)
-            cvc5Assertions = ScopedLinkedFrame(::TreeSet, ::TreeSet)
+            cvc5Ctx = KCvc5Context(solver, mkExprSolver, ctx, manager)
         }
     }
 
diff --git a/ksmt-cvc5/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ForkingSolverManager.kt b/ksmt-cvc5/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ForkingSolverManager.kt
@@ -1,23 +1,86 @@
 package io.ksmt.solver.cvc5
 
 import io.github.cvc5.Solver
+import io.github.cvc5.Sort
+import io.github.cvc5.Term
 import io.ksmt.KContext
+import io.ksmt.decl.KDecl
+import io.ksmt.expr.KExpr
+import io.ksmt.expr.KUninterpretedSortValue
 import io.ksmt.solver.KForkingSolver
 import io.ksmt.solver.KForkingSolverManager
+import io.ksmt.sort.KSort
+import io.ksmt.sort.KUninterpretedSort
 import java.util.IdentityHashMap
+import java.util.TreeMap
 import java.util.concurrent.ConcurrentHashMap
 
 open class KCvc5ForkingSolverManager(private val ctx: KContext) : KForkingSolverManager<KCvc5SolverConfiguration> {
 
     private val solvers: MutableSet<KCvc5ForkingSolver> = ConcurrentHashMap.newKeySet()
 
     /**
-     * for each parent to child hierarchy created only one mkExprSolver,
+     * for each parent-to-child hierarchy created only one mkExprSolver,
      * which is responsible for native expressions lifetime
      */
     private val forkingSolverToMkExprSolver = IdentityHashMap<KCvc5ForkingSolver, Solver>()
     private val mkExprSolverReferences = IdentityHashMap<Solver, Int>()
 
+    // shared cache
+    private val expressionsCache = IdentityHashMap<Solver, ExpressionsCache>()
+    private val expressionsReversedCache = IdentityHashMap<Solver, ExpressionsReversedCache>()
+    private val sortsCache = IdentityHashMap<Solver, SortsCache>()
+    private val sortsReversedCache = IdentityHashMap<Solver, SortsReversedCache>()
+    private val declsCache = IdentityHashMap<Solver, DeclsCache>()
+    private val declsReversedCache = IdentityHashMap<Solver, DeclsReversedCache>()
+
+    private val uninterpretedSortValueDescriptors = IdentityHashMap<Solver, UninterpretedSortValueDescriptors>()
+    private val uninterpretedSortValueInterpretersCache =
+        IdentityHashMap<Solver, UninterpretedSortValueInterpretersCache>()
+    private val uninterpretedSortValues = IdentityHashMap<Solver, UninterpretedSortValues>()
+
+    private fun Solver.ensureRegisteredAsMkExprSolver() = require(this in mkExprSolverReferences) {
+        "Solver is not registered by this manager"
+    }
+
+    internal fun KCvc5Context.findExpressionsCache() = mkExprSolver.ensureRegisteredAsMkExprSolver().let {
+        expressionsCache.getOrPut(mkExprSolver) { ExpressionsCache() }
+    }
+
+    internal fun KCvc5Context.findExpressionsReversedCache() = mkExprSolver.ensureRegisteredAsMkExprSolver().let {
+        expressionsReversedCache.getOrPut(mkExprSolver) { ExpressionsReversedCache() }
+    }
+
+    internal fun KCvc5Context.findSortsCache() = mkExprSolver.ensureRegisteredAsMkExprSolver().let {
+        sortsCache.getOrPut(mkExprSolver) { SortsCache() }
+    }
+
+    internal fun KCvc5Context.findSortsReversedCache() = mkExprSolver.ensureRegisteredAsMkExprSolver().let {
+        sortsReversedCache.getOrPut(mkExprSolver) { SortsReversedCache() }
+    }
+
+    internal fun KCvc5Context.findDeclsCache() = mkExprSolver.ensureRegisteredAsMkExprSolver().let {
+        declsCache.getOrPut(mkExprSolver) { DeclsCache() }
+    }
+
+    internal fun KCvc5Context.findDeclsReversedCache() = mkExprSolver.ensureRegisteredAsMkExprSolver().let {
+        declsReversedCache.getOrPut(mkExprSolver) { DeclsReversedCache() }
+    }
+
+    internal fun KCvc5Context.findUninterpretedSortsValueDescriptors() = mkExprSolver.ensureRegisteredAsMkExprSolver()
+        .let {
+            uninterpretedSortValueDescriptors.getOrPut(mkExprSolver) { UninterpretedSortValueDescriptors() }
+        }
+
+    internal fun KCvc5Context.findUninterpretedSortsValueInterpretersCache() = mkExprSolver
+        .ensureRegisteredAsMkExprSolver().let {
+            uninterpretedSortValueInterpretersCache.getOrPut(mkExprSolver) { UninterpretedSortValueInterpretersCache() }
+        }
+
+    internal fun KCvc5Context.findUninterpretedSortValues() = mkExprSolver.ensureRegisteredAsMkExprSolver().let {
+        uninterpretedSortValues.getOrPut(mkExprSolver) { UninterpretedSortValues() }
+    }
+
     override fun mkForkingSolver(): KForkingSolver<KCvc5SolverConfiguration> {
         val mkExprSolver = Solver()
         incRef(mkExprSolver)
@@ -58,6 +121,16 @@ open class KCvc5ForkingSolverManager(private val ctx: KContext) : KForkingSolver
         val referencesAfterDec = mkExprSolverReferences.getValue(mkExprSolver) - 1
         if (referencesAfterDec == 0) {
             mkExprSolverReferences -= mkExprSolver
+            expressionsCache -= mkExprSolver
+            expressionsReversedCache -= mkExprSolver
+            sortsCache -= mkExprSolver
+            sortsReversedCache -= mkExprSolver
+            declsCache -= mkExprSolver
+            declsReversedCache -= mkExprSolver
+            uninterpretedSortValueDescriptors -= mkExprSolver
+            uninterpretedSortValueInterpretersCache -= mkExprSolver
+            uninterpretedSortValues -= mkExprSolver
+
             mkExprSolver.close()
         } else {
             mkExprSolverReferences[mkExprSolver] = referencesAfterDec
@@ -70,3 +143,14 @@ open class KCvc5ForkingSolverManager(private val ctx: KContext) : KForkingSolver
         }
     }
 }
+
+private typealias ExpressionsCache = HashMap<KExpr<*>, Term>
+private typealias ExpressionsReversedCache = TreeMap<Term, KExpr<*>>
+private typealias SortsCache = HashMap<KSort, Sort>
+private typealias SortsReversedCache = TreeMap<Sort, KSort>
+private typealias DeclsCache = HashMap<KDecl<*>, Term>
+private typealias DeclsReversedCache = TreeMap<Term, KDecl<*>>
+private typealias UninterpretedSortValueDescriptors = ArrayList<KCvc5Context.UninterpretedSortValueDescriptor>
+private typealias UninterpretedSortValueInterpretersCache = HashMap<KUninterpretedSort, Term>
+@Suppress("MaxLineLength")
+private typealias UninterpretedSortValues = HashMap<KUninterpretedSort, MutableList<Pair<Term, KUninterpretedSortValue>>>
diff --git a/ksmt-cvc5/src/main/kotlin/io/ksmt/solver/cvc5/ScopedFrame.kt b/ksmt-cvc5/src/main/kotlin/io/ksmt/solver/cvc5/ScopedFrame.kt
@@ -106,11 +106,10 @@ internal class ScopedLinkedFrame<T> private constructor(
         current = LinkedFrame(newTopFrame, current.previous)
     }
 
-    fun fork(): ScopedLinkedFrame<T> = ScopedLinkedFrame(
-        current,
-        createNewFrame,
-        copyFrame
-    ).also { it.recreateTopFrame() }
+    fun fork(parent: ScopedLinkedFrame<T>) {
+        current = parent.current
+        recreateTopFrame()
+    }
 
     private inline fun forEachReversed(action: (T) -> Unit) {
         var cur: LinkedFrame<T>? = current
diff --git a/ksmt-test/src/test/kotlin/io/ksmt/test/KForkingSolverTest.kt b/ksmt-test/src/test/kotlin/io/ksmt/test/KForkingSolverTest.kt
@@ -284,7 +284,7 @@ class KForkingSolverTest {
             with(ctx) {
                 val parent = mkSolver(ctx)
                 val x by intSort
-                val f = x ge 100.expr
+                val f = x gt 100.expr
 
                 parent.assert(f)
                 parent.check().also { require(it == KSolverStatus.SAT) }
@@ -296,7 +296,7 @@ class KForkingSolverTest {
 
                 fork.assert(f and (x eq xVal))
                 fork.check().also { assertEquals(KSolverStatus.SAT, it) }
-                assertEquals(fork.model().eval(x), xVal)
+                assertEquals(xVal, fork.model().eval(x))
             }
 
         }

Original file line number	Diff line number	Diff line change
`@@ -284,7 +284,7 @@ class KForkingSolverTest {`
`284`	`284`	`with(ctx) {`
`285`	`285`	`val parent = mkSolver(ctx)`
`286`	`286`	`val x by intSort`
`287`		`- val f = x ge 100.expr`
	`287`	`+ val f = x gt 100.expr`
`288`	`288`
`289`	`289`	`parent.assert(f)`
`290`	`290`	`parent.check().also { require(it == KSolverStatus.SAT) }`
`@@ -296,7 +296,7 @@ class KForkingSolverTest {`
`296`	`296`
`297`	`297`	`fork.assert(f and (x eq xVal))`
`298`	`298`	`fork.check().also { assertEquals(KSolverStatus.SAT, it) }`
`299`		`- assertEquals(fork.model().eval(x), xVal)`
	`299`	`+ assertEquals(xVal, fork.model().eval(x))`
`300`	`300`	`}`
`301`	`301`
`302`	`302`	`}`