import z3.scala._

class Solver {
  private[this] var freed = false

  private[this] var z3 = new Z3Context(
    "MODEL"             -> true,
    "TYPE_CHECK"        -> true,
    "WELL_SORTED_CHECK" -> true
  )

  def getContext: Z3Context = z3

  def free(): Unit = synchronized {
    freed = true
    if (z3 ne null) {
      z3.delete()
      z3 = null
    }
  }

  override def finalize() {
    if (!freed) {
      free()
    }
  }
}

object Solver {
  def getFactory(): Solver = new Solver
  def reclaim(solver: Solver): Unit = solver.free()
}
