/* Copyright 2009-2015 EPFL, Lausanne */

package leon
package solvers

import purescala.Common.Identifier
import purescala.Expressions.Expr

class SimpleAssumptionSolverAPI(sf: SolverFactory[AssumptionSolver]) extends SimpleSolverAPI(sf) {

  def solveSATWithCores(expression: Expr, assumptions: Set[Expr]): (Option[Boolean], Map[Identifier, Expr], Set[Expr]) = {
    val s = sf.getNewSolver()
    try {
      s.assertCnstr(expression)
      s.checkAssumptions(assumptions) match {
        case Some(true) =>
          (Some(true), s.getModel, Set())
        case Some(false) =>
          (Some(false), Map(), s.getUnsatCore)
        case None =>
          (None, Map(), Set())
      }
    } finally {
      s.free()
    }
  }
}