Forking solver implementation

[dee-tree]

A forking solver presents an ability to create children with existed parental assertions memory efficiently as possible. Also, it has lazy assertions initialization.

It is draft implementation requiring following reviews.

Notes

1. Forking solver manager (KForkingSolverManager) provides shared resources for the solvers group. It allows to create KForkingSolver instance that lifetime upper bounded by the manager's life.
2. KForkingSolver is a solver, which can be branched in assertions and push-levels.

Usage

KZ3ForkingSolverManager(ctx).use { man ->
    val parent = man.createForkingSolver()
    parent.assert(formula)
    val child = parent.fork()
    println(child.checkSat())
}

Currently implemented:

• Core interfaces: KForkingSolver, KForkingSolverManager
• cvc5 forking impl
• Z3 forking impl
• Yices forking impl + uninterpreted sort values tracking
• Bitwuzla forking impl + uninterpreted sort values tracking

TODO:

• Portfolio forking solver impl
• Process runner forking solver impl