package leon package solvers import purescala.Common._ import purescala.Trees._ case class SimpleSolverAPI(sf: SolverFactory[Solver]) { def solveVALID(expression: Expr): Option[Boolean] = { val s = sf.getNewSolver() s.assertCnstr(Not(expression)) s.check.map(r => !r) } def solveSAT(expression: Expr): (Option[Boolean], Map[Identifier, Expr]) = { val s = sf.getNewSolver() s.assertCnstr(expression) s.check match { case Some(true) => (Some(true), s.getModel) case Some(false) => (Some(false), Map()) case None => (None, Map()) } } def solveSATWithCores(expression: Expr, assumptions: Set[Expr]): (Option[Boolean], Map[Identifier, Expr], Set[Expr]) = { val s = sf.getNewSolver() 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()) } } }