diff --git a/project/Build.scala b/project/Build.scala
index 9347b15361d3083052191957fefe7c343d2bdb6e..a5205b3f017b0c9a6e4eacce1f2e9df4bc422537 100644
--- a/project/Build.scala
+++ b/project/Build.scala
@@ -79,7 +79,7 @@ object Leon extends Build {
object Github {
lazy val bonsai = RootProject(uri("git://github.com/colder/bonsai.git#8f485605785bda98ac61885b0c8036133783290a"))
- private val scalaSmtLibVersion = "160a635e3677a185e2d5bd84669be98fcda8c574"
+ private val scalaSmtLibVersion = "d4622f38a04a191798eb29f39d3c8b2ec312e811"
lazy val scalaSmtLib = RootProject(uri("git://github.com/regb/scala-smtlib.git#%s".format(scalaSmtLibVersion)))
}
}
diff --git a/project/plugins.sbt b/project/plugins.sbt
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 3195b5cfb82061b748b481a382589e45a1d1ae14..b51a0746b3d2665b659885fbf3332e2f499fa9c2 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -3,6 +3,7 @@
package leon
import leon.utils._
+import solvers.SolverFactory
object Main {
@@ -34,6 +35,7 @@ object Main {
LeonFlagOptionDef ("synthesis", "--synthesis", "Partial synthesis of choose() constructs"),
LeonFlagOptionDef ("xlang", "--xlang", "Support for extra program constructs (imperative,...)"),
LeonFlagOptionDef ("library", "--library", "Inject Leon standard library"),
+ LeonValueOptionDef("solvers", "--solvers=s1,s2", "Use solvers s1 and s2 (fairz3,enum,smt)"),
LeonValueOptionDef("debug", "--debug=<sections..>", "Enables specific messages"),
LeonFlagOptionDef ("noop", "--noop", "No operation performed, just output program"),
LeonFlagOptionDef ("help", "--help", "Show help")
@@ -145,6 +147,14 @@ object Main {
settings = settings.copy(injectLibrary = value)
case LeonFlagOption("xlang", value) =>
settings = settings.copy(xlang = value)
+ case LeonValueOption("solvers", ListValue(ss)) =>
+ val available = SolverFactory.definedSolvers
+ val unknown = ss.toSet -- available
+ if (unknown.nonEmpty) {
+ initReporter.error("Unknown solver(s): "+unknown.mkString(", ")+" (Available: "+available.mkString(", ")+")")
+ }
+ settings = settings.copy(selectedSolvers = ss.toSet)
+
case LeonValueOption("debug", ListValue(sections)) =>
val debugSections = sections.flatMap { s =>
if (s == "all") {
@@ -168,7 +178,7 @@ object Main {
}
// Create a new reporter taking settings into account
- val reporter = new DefaultReporter(settings)
+ val reporter = new PlainTextReporter(settings)
reporter.whenDebug(DebugSectionOptions) { debug =>
@@ -275,9 +285,6 @@ object Main {
ctx.reporter.whenDebug(DebugSectionTimers) { debug =>
ctx.timers.outputTable(debug)
}
-
- println("time: " + smtlib.SMTLIBSolver.time)
-
} catch {
case LeonFatalError(None) =>
sys.exit(1)
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index ddd6eb9955b7cb637b196240c01cfb90fd9fb0a9..113c9ab878603dc389dcb1119625d37127fb9daa 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -180,3 +180,13 @@ class DefaultReporter(settings: Settings) extends Reporter(settings) {
}
}
+
+class PlainTextReporter(settings: Settings) extends DefaultReporter(settings) {
+ override protected def severityToPrefix(sev: Severity): String = sev match {
+ case ERROR => "[ Error ]"
+ case WARNING => "[Warning]"
+ case INFO => "[ Info ]"
+ case FATAL => "[ Fatal ]"
+ case DEBUG(_) => "[ Debug ]"
+ }
+}
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 702ef9c2e07d4b60d2670031262bd8d1f76ce568..0165a03b9f5e493fbd4ea306f446c973f3bf8f39 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -11,5 +11,7 @@ case class Settings(
val synthesis: Boolean = false,
val xlang: Boolean = false,
val verify: Boolean = true,
- val injectLibrary: Boolean = false
+ val injectLibrary: Boolean = false,
+ val classPath: List[String] = Settings.defaultClassPath(),
+ val selectedSolvers: Set[String] = Set("fairz3")
)
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index da44836d2ee6df09511c1e03718027ed66335ffe..2274336b9d7a332d760312d2c7a0c380c9d15119 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -12,6 +12,7 @@ import purescala.TypeTrees._
import solvers.TimeoutSolver
import xlang.Trees._
+import solvers.SolverFactory
abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int) extends Evaluator(ctx, prog) {
val name = "evaluator"
@@ -375,7 +376,6 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
gv
case choose: Choose =>
- import solvers.z3.FairZ3Solver
import purescala.TreeOps.simplestValue
implicit val debugSection = utils.DebugSectionSynthesis
@@ -386,14 +386,15 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
val tStart = System.currentTimeMillis;
- val solver = (new FairZ3Solver(ctx, program) with TimeoutSolver).setTimeout(10000L)
+ val solver = SolverFactory.getFromSettings(ctx, program).getNewSolver
- val inputsMap = p.as.map {
+ val eqs = p.as.map {
case id =>
Equals(Variable(id), rctx.mappings(id))
}
- solver.assertCnstr(And(Seq(p.pc, p.phi) ++ inputsMap))
+ val cnstr = And(eqs ::: p.pc :: p.phi :: Nil)
+ solver.assertCnstr(cnstr)
try {
solver.check match {
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index ba8b05cc2e4aa48c21dfc63a91ecc69f4d9169f8..28b197b474440807b78d55f997bf69ff93603608 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -29,7 +29,7 @@ object Common {
}
// the type is left blank (Untyped) for Identifiers that are not variables
- class Identifier private[Common](val name: String, private val globalId: Int, val id: Int, alwaysShowUniqueID: Boolean = false) extends Tree with Typed {
+ class Identifier private[Common](val name: String, val globalId: Int, val id: Int, alwaysShowUniqueID: Boolean = false) extends Tree with Typed {
self : Serializable =>
override def equals(other: Any): Boolean = {
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 387b085f18b4b8b0d66a58b450667214c6c51422..c70d835e5e59fa5ebcf9733b097da20457ade32d 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -475,7 +475,8 @@ object Trees {
}
class CaseClassSelector(val classType: CaseClassType, val caseClass: Expr, val selector: Identifier) extends Expr with FixedType {
- val fixedType = classType.fieldsTypes(classType.classDef.selectorID2Index(selector))
+ val selectorIndex = classType.classDef.selectorID2Index(selector)
+ val fixedType = classType.fieldsTypes(selectorIndex)
override def equals(that: Any): Boolean = (that != null) && (that match {
case t: CaseClassSelector => (t.classType, t.caseClass, t.selector) == (classType, caseClass, selector)
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
index 9b518db9d357c02f6ac68b74b44497705681ec8d..a4b86d0722c0ec44ea51a041fed524b2e19bd42e 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -51,49 +51,6 @@ object TypeTrees {
sealed abstract class TypeTree extends Tree
- // returns the number of distinct values that inhabit a type
- sealed abstract class TypeSize extends Serializable
- case class FiniteSize(size: Int) extends TypeSize
- case object InfiniteSize extends TypeSize
-
- def domainSize(typeTree: TypeTree) : TypeSize = typeTree match {
- case Untyped => FiniteSize(0)
- case BooleanType => FiniteSize(2)
- case UnitType => FiniteSize(1)
- case Int32Type => InfiniteSize
- case ListType(_) => InfiniteSize
- case ArrayType(_) => InfiniteSize
- case TypeParameter(_) => InfiniteSize
- case TupleType(bases) => {
- val baseSizes = bases.map(domainSize(_))
- baseSizes.find(_ == InfiniteSize) match {
- case Some(_) => InfiniteSize
- case None => FiniteSize(baseSizes.map(_.asInstanceOf[FiniteSize].size).reduceLeft(_ * _))
- }
- }
- case SetType(base) => domainSize(base) match {
- case InfiniteSize => InfiniteSize
- case FiniteSize(n) => FiniteSize(scala.math.pow(2, n).toInt)
- }
- case MultisetType(_) => InfiniteSize
- case MapType(from,to) => (domainSize(from),domainSize(to)) match {
- case (InfiniteSize,_) => InfiniteSize
- case (_,InfiniteSize) => InfiniteSize
- case (FiniteSize(n),FiniteSize(m)) => FiniteSize(scala.math.pow(m+1, n).toInt)
- }
- case FunctionType(fts, tt) => {
- val fromSizes = fts map domainSize
- val toSize = domainSize(tt)
- if (fromSizes.exists(_ == InfiniteSize) || toSize == InfiniteSize)
- InfiniteSize
- else {
- val n = toSize.asInstanceOf[FiniteSize].size
- FiniteSize(scala.math.pow(n, fromSizes.foldLeft(1)((acc, s) => acc * s.asInstanceOf[FiniteSize].size)).toInt)
- }
- }
- case c: ClassType => InfiniteSize
- }
-
case object Untyped extends TypeTree
case object BooleanType extends TypeTree
case object Int32Type extends TypeTree
diff --git a/src/main/scala/leon/smtlib/ExprToSExpr.scala b/src/main/scala/leon/smtlib/ExprToSExpr.scala
deleted file mode 100644
index b8e1be22ec7e21469560f1bf5253bf0b7861ba30..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/smtlib/ExprToSExpr.scala
+++ /dev/null
@@ -1,107 +0,0 @@
-package leon
-package smtlib
-
-import purescala._
-import Common._
-import Trees._
-import Extractors._
-import TreeOps._
-import TypeTrees._
-import Definitions._
-
-import _root_.smtlib.sexpr
-import sexpr.SExprs._
-import _root_.smtlib.Commands.{Identifier => SmtLibIdentifier, _}
-
-/** This pretty-printer prints an SMTLIB2 representation of the Purescala program */
-object ExprToSExpr {
-
- //returns the set of free identifier
- def apply(tree: Expr): (SExpr, Set[Identifier]) = {
-
- var freeVars: Set[Identifier] = Set()
-
- def rec(t: Expr): SExpr = t match {
- case Variable(id) => {
- val sym = id2sym(id)
- freeVars += id
- sym
- }
- //case LetTuple(ids,d,e) => SList(List(
- // SSymbol("let"),
- // SList(List(ids))
- case Let(b,d,e) => {
- val id = id2sym(b)
- val value = rec(d)
- val newBody = rec(e)
- freeVars -= b
-
- SList(
- SSymbol("let"),
- SList(
- SList(id, value)
- ),
- newBody
- )
- }
-
- case er@Error(_) => {
- val id = FreshIdentifier("error_value").setType(er.getType)
- val sym = id2sym(id)
- freeVars += id
- sym
- }
-
- case And(exprs) => SList(SSymbol("and") :: exprs.map(rec).toList)
- case Or(exprs) => SList(SSymbol("or") :: exprs.map(rec).toList)
- case Not(expr) => SList(SSymbol("not"), rec(expr))
- case Equals(l,r) => SList(SSymbol("="), rec(l), rec(r))
- case IntLiteral(v) => SInt(v)
- case BooleanLiteral(v) => SSymbol(v.toString) //TODO: maybe need some builtin type here
- case StringLiteral(s) => SString(s)
-
- case Implies(l,r) => SList(SSymbol("=>"), rec(l), rec(r))
- case Iff(l,r) => SList(SSymbol("="), rec(l), rec(r))
-
- case Plus(l,r) => SList(SSymbol("+"), rec(l), rec(r))
- case UMinus(expr) => SList(SSymbol("-"), rec(expr))
- case Minus(l,r) => SList(SSymbol("-"), rec(l), rec(r))
- case Times(l,r) => SList(SSymbol("*"), rec(l), rec(r))
- case Division(l,r) => SList(SSymbol("div"), rec(l), rec(r))
- case Modulo(l,r) => SList(SSymbol("mod"), rec(l), rec(r))
- case LessThan(l,r) => SList(SSymbol("<"), rec(l), rec(r))
- case LessEquals(l,r) => SList(SSymbol("<="), rec(l), rec(r))
- case GreaterThan(l,r) => SList(SSymbol(">"), rec(l), rec(r))
- case GreaterEquals(l,r) => SList(SSymbol(">="), rec(l), rec(r))
-
- case IfExpr(c, t, e) => SList(SSymbol("ite"), rec(c), rec(t), rec(e))
-
- case FunctionInvocation(fd, args) => SList(id2sym(fd.id) :: args.map(rec).toList)
-
- //case ArrayFill(length, defaultValue) => SList(
- // SList(SSymbol("as"), SSymbol("const"), tpe2sort(tree.getType)),
- // rec(defaultValue)
- //)
- //case ArrayMake(defaultValue) => SList(
- // SList(SSymbol("as"), SSymbol("const"), tpe2sort(tree.getType)),
- // rec(defaultValue)
- //)
- //case ArraySelect(array, index) => SList(SSymbol("select"), rec(array), rec(index))
- //case ArrayUpdated(array, index, newValue) => SList(SSymbol("store"), rec(array), rec(index), rec(newValue))
-
- case CaseClass(ccd, args) if args.isEmpty => id2sym(ccd.id)
- case CaseClass(ccd, args) => SList(id2sym(ccd.id) :: args.map(rec(_)).toList)
- case CaseClassSelector(_, arg, field) => SList(id2sym(field), rec(arg))
-
- case CaseClassInstanceOf(ccd, arg) => {
- val name = id2sym(ccd.id)
- val testerName = SSymbol("is-" + name.s)
- SList(testerName, rec(arg))
- }
- case o => sys.error("TODO converting to smtlib: " + o)
- }
-
- val res = rec(tree)
- (res, freeVars)
- }
-}
diff --git a/src/main/scala/leon/smtlib/PrettyPrinter.scala b/src/main/scala/leon/smtlib/PrettyPrinter.scala
deleted file mode 100644
index d13d4cc459dd47afeddccd5bc2ee852b9dff5cc0..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/smtlib/PrettyPrinter.scala
+++ /dev/null
@@ -1,46 +0,0 @@
-//package leon
-//package smtlib
-//
-//import purescala._
-//import Common._
-//import Trees._
-//import Extractors._
-//import TreeOps._
-//import TypeTrees._
-//import Definitions._
-//
-//import _root_.smtlib.sexpr
-//import sexpr.SExprs._
-//import _root_.smtlib.Commands.{Identifier => SmtLibIdentifier, _}
-//
-// // prec: there should be no lets and no pattern-matching in this expression
-// def collectWithPathCondition(matcher: Expr=>Boolean, expression: Expr) : Set[(Seq[Expr],Expr)] = {
-// var collected : Set[(Seq[Expr],Expr)] = Set.empty
-//
-// def rec(expr: Expr, path: List[Expr]) : Unit = {
-// if(matcher(expr)) {
-// collected = collected + ((path.reverse, expr))
-// }
-//
-// expr match {
-// case Let(i,e,b) => {
-// rec(e, path)
-// rec(b, Equals(Variable(i), e) :: path)
-// }
-// case IfExpr(cond, thn, els) => {
-// rec(cond, path)
-// rec(thn, cond :: path)
-// rec(els, Not(cond) :: path)
-// }
-// case NAryOperator(args, _) => args.foreach(rec(_, path))
-// case BinaryOperator(t1, t2, _) => rec(t1, path); rec(t2, path)
-// case UnaryOperator(t, _) => rec(t, path)
-// case t : Terminal => ;
-// case _ => scala.sys.error("Unhandled tree in collectWithPathCondition : " + expr)
-// }
-// }
-//
-// rec(expression, Nil)
-// collected
-// }
-//}
diff --git a/src/main/scala/leon/smtlib/SExprToExpr.scala b/src/main/scala/leon/smtlib/SExprToExpr.scala
deleted file mode 100644
index 9dc8690a0ae8b9066356f580019bd5e285781d61..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/smtlib/SExprToExpr.scala
+++ /dev/null
@@ -1,48 +0,0 @@
-package leon
-package smtlib
-
-import purescala._
-import Common._
-import Trees._
-import Extractors._
-import TreeOps._
-import TypeTrees._
-import Definitions._
-
-import _root_.smtlib.sexpr
-import sexpr.SExprs._
-import _root_.smtlib.Commands.{Identifier => SmtLibIdentifier, _}
-
-object SExprToExpr {
-
- def apply(sexpr: SExpr, context: Map[String, Expr], constructors: Map[String, CaseClassDef]): Expr = sexpr match {
- case SInt(n) => IntLiteral(n.toInt)
- case SSymbol("TRUE") => BooleanLiteral(true)
- case SSymbol("FALSE") => BooleanLiteral(false)
- case SSymbol(s) => constructors.get(s) match {
- case Some(app) => CaseClass(app, Seq())
- case None => context(s)
- }
- case SList(SSymbol(app) :: args) if(constructors.isDefinedAt(app)) =>
- CaseClass(constructors(app), args.map(apply(_, context, constructors)))
-
- case SList(List(SSymbol("LET"), SList(defs), body)) => {
- val leonDefs: Seq[(Identifier, Expr, String)] = defs.map {
- case SList(List(SSymbol(sym), value)) => (FreshIdentifier(sym), apply(value, context, constructors), sym)
- }
- val recBody = apply(body, context ++ leonDefs.map(p => (p._3, p._1.toVariable)), constructors)
- leonDefs.foldRight(recBody)((binding, b) => Let(binding._1, binding._2, b))
- }
- case SList(SSymbol(app) :: args) => {
- val recArgs = args.map(arg => apply(arg, context, constructors))
- app match {
- case "-" => recArgs match {
- case List(a) => UMinus(a)
- case List(a, b) => Minus(a, b)
- }
- }
- }
- case o => sys.error("TODO converting from s-expr: " + o)
- }
-
-}
diff --git a/src/main/scala/leon/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/smtlib/SMTLIBSolver.scala
deleted file mode 100644
index 510b00ff2c11c7e655acf53c69f67e53a57aed52..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/smtlib/SMTLIBSolver.scala
+++ /dev/null
@@ -1,147 +0,0 @@
-/* Copyright 2009-2013 EPFL, Lausanne */
-
-package leon
-package smtlib
-
-import solvers.IncrementalSolver
-import utils.Interruptible
-import purescala._
-import Common._
-import Trees._
-import Extractors._
-import TreeOps._
-import TypeTrees._
-import Definitions._
-
-import _root_.smtlib.{PrettyPrinter => CommandPrinter, Commands, CommandResponses, sexpr, Interpreter => SMTLIBInterpreter}
-import Commands.{Identifier => SMTLIBIdentifier, _}
-import CommandResponses.{Error => ErrorResponse, _}
-import sexpr.SExprs._
-import _root_.smtlib.Commands.{Identifier => SmtLibIdentifier, _}
-
-
-class SMTLIBSolver(override val context: LeonContext,
- val program: Program,
- smtlibInterpreterFactory: () => SMTLIBInterpreter)
- extends IncrementalSolver with Interruptible {
-
- override def interrupt: Unit = {}
- override def recoverInterrupt(): Unit = {}
-
-
- override def name: String = "smtlib-solver"
- val out = new java.io.FileWriter("vcs/vc_" + SMTLIBSolver.counter)
-
- //using a factory, so that creation and call to free are local to this class
- private val smtlibInterpreter = smtlibInterpreterFactory()
-
- private var errorConstants: Set[(SSymbol, SExpr)] = Set()
-
- val defs: Seq[ClassTypeDef] = program.definedClasses
-
- val partition: Seq[(AbstractClassDef, Seq[CaseClassDef])] = {
- val parents: Seq[AbstractClassDef] = defs.filter(!_.hasParent).asInstanceOf[Seq[AbstractClassDef]]
- parents.map(p => (p, defs.filter(c => c.parent match {
- case Some(p2) => p == p2
- case None => false
- }).asInstanceOf[Seq[CaseClassDef]]))
- }
-
- val sorts: Seq[SExpr] = partition.map{ case (parent, children) => {
- val name = id2sym(parent.id)
- val constructors: List[SExpr] = children.map(child => {
- val fields: List[SExpr] = child.fields.map{case VarDecl(id, tpe) => SList(id2sym(id), tpe2sort(tpe)) }.toList
- if(fields.isEmpty) id2sym(child.id) else SList(id2sym(child.id) :: fields)
- }).toList
-
- SList(name :: constructors)
- }}
- val constructors: Map[String, CaseClassDef] =
- partition.unzip._2.flatMap(ccds => ccds.map(ccd => (ccd.id.uniqueName.toUpperCase, ccd))).toMap
- val sortDecls = NonStandardCommand(SList(SSymbol("declare-datatypes"), SList(), SList(sorts.toList)))
- val funDefDecls: Seq[Command] = program.definedFunctions.flatMap(fd2sexp)
- val sortErrors: List[Command] = errorConstants.map(p => DeclareFun(p._1.s, Seq(), p._2)).toList
-
- def declareConst(id: Identifier): Command = DeclareFun(id2sym(id).s, Seq(), tpe2sort(id.getType))
-
- //SComment("! THEORY=1") +:
- //SComment("Generated by Leon") +:
- sendCommand(sortDecls)
- sortErrors.foreach(sendCommand(_))
- funDefDecls.foreach(sendCommand)
-
- //convertedFunDefs.flatMap(_._1) ++
- //convertedFunDefs.map(_._2) ++
- //convertedFunDefs.flatMap(_._3) ++
- //Seq(SList(SSymbol("check-sat")))
-
- private var freeVars: Set[Identifier] = program.definedFunctions.flatMap(fd => fd.args.map(_.id)).toSet
- override def assertCnstr(expression: Expr): Unit = {
-
- val (sexpr, exprFreevars) = ExprToSExpr(expression)
-
- val newFreeVars: Set[Identifier] = exprFreevars.diff(freeVars)
- freeVars ++= newFreeVars
- newFreeVars.foreach(id => sendCommand(declareConst(id)))
-
- sendCommand(Assert(sexpr))
- }
-
- override def check: Option[Boolean] = sendCommand(CheckSat) match {
- case CheckSatResponse(SatStatus) => Some(true)
- case CheckSatResponse(UnsatStatus) => Some(false)
- case CheckSatResponse(UnknownStatus) => None
- }
-
- override def getModel: Map[Identifier, Expr] = {
- val ids: List[Identifier] = freeVars.toList
- val sexprs: List[SSymbol] = ids.map(id => id2sym(id))
- val cmd: Command = GetValue(sexprs.head, sexprs.tail)
-
- val symToIds: Map[SExpr, Identifier] = sexprs.map(s => SSymbol(s.s.toUpperCase)).zip(ids).toMap
- val GetValueResponse(valuationPairs) = sendCommand(cmd)
- println("got valuation pairs: " + valuationPairs)
- valuationPairs.map{ case (sym, value) => (symToIds(sym), SExprToExpr(value, Map(), constructors)) }.toMap
- }
-
- override def free() = {
- sendCommand(Exit)
- smtlibInterpreter.free()
- out.close
- SMTLIBSolver.counter += 1
- }
-
- override def push(): Unit = {
- sendCommand(Push(1))
- }
- override def pop(lvl: Int = 1): Unit = {
- sendCommand(Pop(1))
- }
-
- def sendCommand(cmd: Command): CommandResponse = {
- val startTime = System.currentTimeMillis
- CommandPrinter(cmd, out)
- out.write("\n")
- val response = smtlibInterpreter.eval(cmd)
- assert(!response.isInstanceOf[Error])
- SMTLIBSolver.time = SMTLIBSolver.time + (System.currentTimeMillis - startTime)
- response
- }
-
- private def fd2sexp(funDef: FunDef): List[Command] = {
- val name = id2sym(funDef.id)
- val returnSort = tpe2sort(funDef.returnType)
-
- val varDecls: List[(SSymbol, SExpr)] = funDef.args.map(vd => (id2sym(vd.id), tpe2sort(vd.tpe))).toList
-
- val topLevelVarDecl: List[Command] = varDecls.map{ case (name, tpe) => DeclareFun(name.s, Seq(), tpe) }
- val funDecl: Command = DeclareFun(name.s, varDecls.map(_._2), returnSort)
-
- funDecl :: topLevelVarDecl
- }
-}
-
-object SMTLIBSolver {
- var counter = 0
- var time: Long = 0
-}
diff --git a/src/main/scala/leon/smtlib/package.scala b/src/main/scala/leon/smtlib/package.scala
deleted file mode 100644
index 63f6b6c0f561a56980cf5af22fc597af20f73438..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/smtlib/package.scala
+++ /dev/null
@@ -1,30 +0,0 @@
-package leon
-
-import purescala._
-import Common._
-import Trees._
-import Extractors._
-import TreeOps._
-import TypeTrees._
-import Definitions._
-
-import _root_.smtlib.sexpr
-import sexpr.SExprs._
-import _root_.smtlib.Commands.{Identifier => SmtLibIdentifier, _}
-
-package object smtlib {
-
- private[smtlib] def id2sym(id: Identifier): SSymbol = SSymbol(id.uniqueName)
- //return a series of declarations, an expression that defines the function,
- //and the seq of asserts for pre/post-conditions
-
-
- def tpe2sort[smtlib](tpe: TypeTree): SExpr = tpe match {
- case Int32Type => SSymbol("Int")
- case BooleanType => SSymbol("Bool")
- case ArrayType(baseTpe) => SList(SSymbol("Array"), SSymbol("Int"), tpe2sort(baseTpe))
- case AbstractClassType(abs) => id2sym(abs.id)
- case _ => sys.error("TODO tpe2sort: " + tpe)
- }
-
-}
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index 44c1f4140540e1afe65c5b8289cda5ad8eb12085..5343be2d2cbc8f47613182b932b9f6be52c4b7ec 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -3,12 +3,13 @@
package leon
package solvers
+import purescala.Definitions._
import scala.reflect.runtime.universe._
abstract class SolverFactory[+S <: Solver : TypeTag] {
def getNewSolver(): S
- val name = "SFact("+typeOf[S].toString+")"
+ val name = typeOf[S].toString.split("\\.").last.replaceAll("Solver", "")+"*"
}
object SolverFactory {
@@ -17,4 +18,43 @@ object SolverFactory {
def getNewSolver() = builder()
}
}
+
+ val definedSolvers = Set("fairz3", "enum", "smt", "smt-z3", "smt-cvc4");
+
+ def getFromSettings[S](ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
+ import combinators._
+ import z3._
+ import smtlib._
+
+ def getSolver(name: String): SolverFactory[TimeoutSolver] = name match {
+ case "fairz3" =>
+ SolverFactory(() => new FairZ3Solver(ctx, program) with TimeoutSolver)
+
+ case "enum" =>
+ SolverFactory(() => new EnumerationSolver(ctx, program) with TimeoutSolver)
+
+ case "smt" | "smt-z3" =>
+ val smtf = SolverFactory(() => new SMTLIBSolver(ctx, program) with SMTLIBZ3Target)
+ SolverFactory(() => new UnrollingSolver(ctx, smtf) with TimeoutSolver)
+
+ case "smt-cvc4" =>
+ val smtf = SolverFactory(() => new SMTLIBSolver(ctx, program) with SMTLIBCVC4Target)
+ SolverFactory(() => new UnrollingSolver(ctx, smtf) with TimeoutSolver)
+
+ case _ =>
+ ctx.reporter.fatalError("Unknown solver "+name)
+ }
+
+ val selectedSolvers = ctx.settings.selectedSolvers.map(getSolver)
+
+ if (selectedSolvers.isEmpty) {
+ ctx.reporter.fatalError("No solver selected. Aborting")
+ } else if (selectedSolvers.size == 1) {
+ selectedSolvers.head
+ } else {
+ SolverFactory( () => new PortfolioSolver(ctx, selectedSolvers.toSeq) with TimeoutSolver)
+ }
+
+ }
+
}
diff --git a/src/main/scala/leon/solvers/combinators/FunctionTemplate.scala b/src/main/scala/leon/solvers/combinators/FunctionTemplate.scala
index 85ad52f78d1870343c9d8678d2ec2176a4eddac6..abe4b684159eab6af7e3f4c6fe0b2fa871ca4b48 100644
--- a/src/main/scala/leon/solvers/combinators/FunctionTemplate.scala
+++ b/src/main/scala/leon/solvers/combinators/FunctionTemplate.scala
@@ -95,8 +95,6 @@ class FunctionTemplate private(
}
object FunctionTemplate {
- val splitAndOrImplies = false
-
def mkTemplate(tfd: TypedFunDef, isRealFunDef : Boolean = true) : FunctionTemplate = {
val condVars : MutableSet[Identifier] = MutableSet.empty
val exprVars : MutableSet[Identifier] = MutableSet.empty
@@ -138,6 +136,13 @@ object FunctionTemplate {
res
}
+ def requireDecomposition(e: Expr) = {
+ exists{
+ case (_: FunctionInvocation) | (_: Assert) | (_: Ensuring) | (_: Choose) => true
+ case _ => false
+ }(e)
+ }
+
def rec(pathVar : Identifier, expr : Expr) : Expr = {
expr match {
case a @ Assert(cond, _, body) =>
@@ -175,48 +180,16 @@ object FunctionTemplate {
case m : MatchExpr => sys.error("MatchExpr's should have been eliminated.")
case i @ Implies(lhs, rhs) =>
- if (splitAndOrImplies) {
- if (containsFunctionCalls(i)) {
- rec(pathVar, IfExpr(lhs, rhs, BooleanLiteral(true)))
- } else {
- i
- }
- } else {
- Implies(rec(pathVar, lhs), rec(pathVar, rhs))
- }
+ Implies(rec(pathVar, lhs), rec(pathVar, rhs))
case a @ And(parts) =>
- if (splitAndOrImplies) {
- if (containsFunctionCalls(a)) {
- val partitions = groupWhile((e: Expr) => !containsFunctionCalls(e), parts)
-
- val ifExpr = partitions.map(And(_)).reduceRight{ (a: Expr, b: Expr) => IfExpr(a, b, BooleanLiteral(false)) }
-
- rec(pathVar, ifExpr)
- } else {
- a
- }
- } else {
- And(parts.map(rec(pathVar, _)))
- }
+ And(parts.map(rec(pathVar, _)))
case o @ Or(parts) =>
- if (splitAndOrImplies) {
- if (containsFunctionCalls(o)) {
- val partitions = groupWhile((e: Expr) => !containsFunctionCalls(e), parts)
-
- val ifExpr = partitions.map(Or(_)).reduceRight{ (a: Expr, b: Expr) => IfExpr(a, BooleanLiteral(true), b) }
-
- rec(pathVar, ifExpr)
- } else {
- o
- }
- } else {
- Or(parts.map(rec(pathVar, _)))
- }
+ Or(parts.map(rec(pathVar, _)))
case i @ IfExpr(cond, thenn, elze) => {
- if(!containsFunctionCalls(cond) && !containsFunctionCalls(thenn) && !containsFunctionCalls(elze)) {
+ if(!requireDecomposition(i)) {
i
} else {
val newBool1 : Identifier = FreshIdentifier("b", true).setType(BooleanType)
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
index 7ddf0abcde8408ab09e61b326fe2e91acf3c4dba..f9fd8a7d4beaad38ebb352ba3406bba5484eb048 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -18,28 +18,20 @@ import scala.collection.mutable.{Map=>MutableMap}
import ExecutionContext.Implicits.global
-class PortfolioSolver(val context: LeonContext, solvers: Seq[SolverFactory[AssumptionSolver with IncrementalSolver with Interruptible]])
- extends Solver with IncrementalSolver with Interruptible with NaiveAssumptionSolver {
+class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext, solvers: Seq[SolverFactory[S]])
+ extends Solver with Interruptible {
val name = "Pfolio"
var constraints = List[Expr]()
- private var modelMap = Map[Identifier, Expr]()
- private var solversInsts = solvers.map(_.getNewSolver)
+ protected var modelMap = Map[Identifier, Expr]()
+ protected var solversInsts: Seq[S] = solvers.map(_.getNewSolver)
def assertCnstr(expression: Expr): Unit = {
solversInsts.foreach(_.assertCnstr(expression))
}
- def push(): Unit = {
- solversInsts.foreach(_.push())
- }
-
- def pop(lvl: Int): Unit = {
- solversInsts.foreach(_.pop(lvl))
- }
-
def check: Option[Boolean] = {
modelMap = Map()
@@ -88,3 +80,15 @@ class PortfolioSolver(val context: LeonContext, solvers: Seq[SolverFactory[Assum
solversInsts.foreach(_.recoverInterrupt())
}
}
+
+class PortfolioSolverSynth(context: LeonContext, solvers: Seq[SolverFactory[AssumptionSolver with IncrementalSolver with Interruptible]])
+ extends PortfolioSolver[AssumptionSolver with IncrementalSolver with Interruptible](context, solvers) with IncrementalSolver with Interruptible with NaiveAssumptionSolver {
+
+ def push(): Unit = {
+ solversInsts.foreach(_.push())
+ }
+
+ def pop(lvl: Int): Unit = {
+ solversInsts.foreach(_.pop(lvl))
+ }
+}
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 728ae07eb45a5cf4b29e823f85b2494069760591..ce527cfcc5691f67aeee4102ded69b4d80f38ae4 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -20,9 +20,11 @@ class UnrollingSolver(val context: LeonContext, underlyings: SolverFactory[Incre
private var theConstraint : Option[Expr] = None
private var theModel : Option[Map[Identifier,Expr]] = None
+ val reporter = context.reporter
+
private var stop: Boolean = false
- def name = "Unr("+underlyings.name+")"
+ def name = "U:"+underlyings.name
def free {}
@@ -36,14 +38,11 @@ class UnrollingSolver(val context: LeonContext, underlyings: SolverFactory[Incre
}
def check : Option[Boolean] = theConstraint.map { expr =>
- val solver = underlyings.getNewSolver//SimpleSolverAPI(underlyings)
-
- debugS("Check called on " + expr.asString + "...")
+ val solver = underlyings.getNewSolver
val template = getTemplate(expr)
val aVar : Identifier = template.activatingBool
- var allClauses : Seq[Expr] = Nil
var allBlockers : Map[Identifier,Set[FunctionInvocation]] = Map.empty
def unrollOneStep() : List[Expr] = {
@@ -52,20 +51,24 @@ class UnrollingSolver(val context: LeonContext, underlyings: SolverFactory[Incre
var newClauses : List[Seq[Expr]] = Nil
var newBlockers : Map[Identifier,Set[FunctionInvocation]] = Map.empty
- for(blocker <- allBlockers.keySet; FunctionInvocation(tfd, args) <- allBlockers(blocker)) {
- val (nc, nb) = getTemplate(tfd).instantiate(blocker, args)
+ for(blocker <- allBlockers.keySet; fi @ FunctionInvocation(tfd, args) <- allBlockers(blocker)) {
+ val tmpl = getTemplate(tfd)
+
+ val (nc, nb) = tmpl.instantiate(blocker, args)
newClauses = nc :: newClauses
newBlockers = newBlockers ++ nb
+ //reporter.debug("Unrolling behind "+fi+" ("+nc.size+")")
+ //for (c <- nc) {
+ // reporter.debug(" . "+c)
+ //}
}
- allClauses = newClauses.flatten ++ allClauses
allBlockers = newBlockers
newClauses.flatten
}
val (nc, nb) = template.instantiate(aVar, template.tfd.params.map(a => Variable(a.id)))
- allClauses = nc.reverse
allBlockers = nb
var unrollingCount : Int = 0
@@ -73,46 +76,42 @@ class UnrollingSolver(val context: LeonContext, underlyings: SolverFactory[Incre
var result : Option[Boolean] = None
solver.assertCnstr(Variable(aVar))
- solver.assertCnstr(And(allClauses))
+ solver.assertCnstr(And(nc))
// We're now past the initial step.
while(!done && !stop) {
- debugS("At lvl : " + unrollingCount)
-
solver.push()
- //val closed : Expr = fullClosedExpr
+ reporter.debug(" - Searching with blocked literals")
solver.assertCnstr(And(allBlockers.keySet.toSeq.map(id => Not(id.toVariable))))
-
- debugS("Going for SAT with this:\n")
-
solver.check match {
case Some(false) =>
solver.pop(1)
+ reporter.debug(" - Searching with unblocked literals")
//val open = fullOpenExpr
- debugS("Was UNSAT... Going for UNSAT with this:\n")
solver.check match {
case Some(false) =>
- debugS("Was UNSAT... Done !")
done = true
result = Some(false)
- case _ =>
- debugS("Was SAT or UNKNOWN. Let's unroll !")
+ case r =>
unrollingCount += 1
+ val model = solver.getModel
+ reporter.debug(" - Tentative model: "+model)
+ reporter.debug(" - more unrollings")
val newClauses = unrollOneStep()
+ reporter.debug(s" - ${newClauses.size} new clauses")
+ readLine()
solver.assertCnstr(And(newClauses))
}
case Some(true) =>
val model = solver.getModel
- debugS("WAS SAT ! We're DONE !")
done = true
result = Some(true)
theModel = Some(model)
case None =>
val model = solver.getModel
- debugS("WAS UNKNOWN ! We're DONE !")
done = true
result = Some(true)
theModel = Some(model)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f9f9a59e594d5b1663c0e1d4439d9a5624e63a68
--- /dev/null
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -0,0 +1,51 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
+package leon
+package solvers
+package smtlib
+
+import utils._
+import purescala._
+import Common._
+import Trees._
+import Extractors._
+import TypeTrees._
+
+import _root_.smtlib.sexpr.SExprs._
+import _root_.smtlib.interpreters.CVC4Interpreter
+
+trait SMTLIBCVC4Target extends SMTLIBTarget {
+ this: SMTLIBSolver =>
+
+ val targetName = "cvc4"
+
+ def getNewInterpreter() = new CVC4Interpreter
+
+ val extSym = SSymbol("_")
+
+ override def toSMT(e: Expr)(implicit bindings: Map[Identifier, SExpr]) = e match {
+ case fs @ FiniteSet(elems) =>
+ val ss = declareSort(fs.getType)
+ var res = SList(SSymbol("as"), SSymbol("const"), ss, toSMT(BooleanLiteral(false)))
+
+ for (e <- elems) {
+ res = SList(SSymbol("store"), res, toSMT(e), toSMT(BooleanLiteral(true)))
+ }
+
+ res
+
+ case sd @ SetDifference(a, b) =>
+ // a -- b
+ // becomes:
+ // a && not(b)
+ SList(SList(extSym, SSymbol("map"), SSymbol("and")), toSMT(a), SList(SList(extSym, SSymbol("map"), SSymbol("not")), toSMT(b)))
+ case SetUnion(l, r) =>
+ SList(SList(extSym, SSymbol("map"), SSymbol("or")), toSMT(l), toSMT(r))
+
+ case SetIntersection(l, r) =>
+ SList(SList(extSym, SSymbol("map"), SSymbol("and")), toSMT(l), toSMT(r))
+
+ case _ =>
+ super.toSMT(e)
+ }
+}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a1de9e9e220dc5a8769adcebcdf14eeef08ac170
--- /dev/null
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -0,0 +1,68 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
+package leon
+package solvers
+package smtlib
+
+import utils._
+import purescala._
+import Common._
+import Trees._
+import Extractors._
+import TreeOps._
+import TypeTrees._
+import Definitions._
+
+import _root_.smtlib.{PrettyPrinter => SMTPrinter, Interpreter => SMTInterpreter}
+import _root_.smtlib.Commands.{Identifier => _, Assert => SMTAssert, _}
+import _root_.smtlib.CommandResponses.{Error => ErrorResponse, _}
+import _root_.smtlib.sexpr.SExprs._
+import _root_.smtlib.interpreters._
+
+abstract class SMTLIBSolver(val context: LeonContext,
+ val program: Program)
+ extends IncrementalSolver with Interruptible with SMTLIBTarget {
+
+ override def interrupt: Unit = {}
+ override def recoverInterrupt(): Unit = {}
+
+ override def name: String = "smt-"+targetName
+
+ override def assertCnstr(expr: Expr): Unit = {
+ variablesOf(expr).foreach(declareVariable)
+ val sexpr = toSMT(expr)(Map())
+ sendCommand(SMTAssert(sexpr))
+ }
+
+ override def check: Option[Boolean] = sendCommand(CheckSat) match {
+ case CheckSatResponse(SatStatus) => Some(true)
+ case CheckSatResponse(UnsatStatus) => Some(false)
+ case CheckSatResponse(UnknownStatus) => None
+ }
+
+ override def getModel: Map[Identifier, Expr] = {
+ val syms = variables.bSet.toList
+ val cmd: Command = GetValue(syms.head, syms.tail)
+
+ val GetValueResponse(valuationPairs) = sendCommand(cmd)
+
+ valuationPairs.collect {
+ case (sym: SSymbol, value) if variables.containsB(sym) =>
+ //println("Getting model for "+sym)
+ //println("Value "+value)
+ (variables.toA(sym), fromSMT(value)(Map()))
+ }.toMap
+ }
+
+ override def free() = {
+ interpreter.free()
+ out.close
+ }
+
+ override def push(): Unit = {
+ sendCommand(Push(1))
+ }
+ override def pop(lvl: Int = 1): Unit = {
+ sendCommand(Pop(1))
+ }
+}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
new file mode 100644
index 0000000000000000000000000000000000000000..dc6e9adc36bffcfde7763b0674276140e48061e8
--- /dev/null
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -0,0 +1,346 @@
+package leon
+package solvers
+package smtlib
+
+import utils.Interruptible
+import purescala._
+import Common._
+import Trees.{Assert => _, _}
+import Extractors._
+import TreeOps._
+import TypeTrees._
+import Definitions._
+import utils.Bijection
+
+import _root_.smtlib.{PrettyPrinter => SMTPrinter, Interpreter => SMTInterpreter}
+import _root_.smtlib.Commands.{Identifier => _, _}
+import _root_.smtlib.CommandResponses.{Error => ErrorResponse, _}
+import _root_.smtlib.sexpr.SExprs._
+import _root_.smtlib.interpreters._
+
+trait SMTLIBTarget {
+ this: SMTLIBSolver =>
+
+ val reporter = context.reporter
+
+ def targetName: String
+ def getNewInterpreter(): SMTInterpreter
+
+ val interpreter = getNewInterpreter()
+
+ val out = new java.io.FileWriter(s"vcs-$targetName.log", true)
+ reporter.ifDebug { debug =>
+ out.write("; -----------------------------------------------------\n")
+ }
+
+ def id2sym(id: Identifier): SSymbol = SSymbol(id.name.toUpperCase+"!"+id.globalId)
+
+ // metadata for CC, and variables
+ val constructors = new Bijection[TypeTree, SSymbol]()
+ val selectors = new Bijection[(TypeTree, Int), SSymbol]()
+ val testers = new Bijection[TypeTree, SSymbol]()
+ val variables = new Bijection[Identifier, SSymbol]()
+ val sorts = new Bijection[TypeTree, SExpr]()
+ val functions = new Bijection[TypedFunDef, SSymbol]()
+
+ def normalizeType(t: TypeTree): TypeTree = t match {
+ case ct: ClassType if ct.parent.isDefined => ct.parent.get
+ case tt: TupleType => TupleType(tt.bases.map(normalizeType))
+ case _ => t
+ }
+
+ def unsupported(str: Any) = reporter.fatalError(s"Unsupported in $targetName: $str")
+
+ def declareSort(t: TypeTree): SExpr = {
+ val tpe = normalizeType(t)
+ sorts.cachedB(tpe) {
+ tpe match {
+ case BooleanType => SSymbol("Bool")
+ case Int32Type => SSymbol("Int")
+ case TypeParameter(id) =>
+ val s = id2sym(id)
+ val cmd = NonStandardCommand(SList(SSymbol("declare-sort"), s))
+ sendCommand(cmd)
+ s
+ case _: ClassType | _: TupleType =>
+ declareStructuralSort(tpe)
+ case _ =>
+ unsupported("Sort "+t)
+ }
+ }
+ }
+
+ def freshSym(id: Identifier): SSymbol = freshSym(id.name)
+ def freshSym(name: String): SSymbol = id2sym(FreshIdentifier(name))
+
+ def declareStructuralSort(t: TypeTree): SExpr = {
+
+ def getHierarchy(ct: ClassType): (ClassType, Seq[CaseClassType]) = ct match {
+ case act: AbstractClassType =>
+ (act, act.knownCCDescendents)
+ case cct: CaseClassType =>
+ cct.parent match {
+ case Some(p) =>
+ getHierarchy(p)
+ case None =>
+ (cct, List(cct))
+ }
+ }
+
+ case class DataType(sym: SSymbol, cases: Seq[Constructor])
+ case class Constructor(sym: SSymbol, tpe: TypeTree, fields: Seq[(SSymbol, TypeTree)])
+
+ var datatypes = Map[TypeTree, DataType]()
+
+
+ def findDependencies(t: TypeTree): Unit = t match {
+ case ct: ClassType =>
+ val (root, sub) = getHierarchy(ct)
+
+ if (!(datatypes contains root) && !(sorts containsA root)) {
+ val sym = freshSym(ct.id)
+
+ val conss = sub.map { case cct =>
+ Constructor(freshSym(cct.id), cct, cct.fields.map(vd => (freshSym(vd.id), vd.tpe)))
+ }
+
+ datatypes += root -> DataType(sym, conss)
+
+ // look for dependencies
+ for (ct <- root +: sub; f <- ct.fields) findDependencies(f.tpe)
+ }
+ case tt @ TupleType(bases) =>
+ if (!(datatypes contains tt) && !(sorts containsA tt)) {
+ val sym = freshSym("tuple"+bases.size)
+
+ val c = Constructor(freshSym(sym.s), tt, bases.zipWithIndex.map {
+ case (tpe, i) => (freshSym("_"+(i+1)), tpe)
+ })
+
+ datatypes += tt -> DataType(sym, Seq(c))
+
+ bases.foreach(findDependencies)
+ }
+
+ case st @ SetType(base) =>
+
+
+ case _ =>
+ }
+
+ // Populates the dependencies of the structural type to define.
+ findDependencies(t)
+
+ // We pre-declare ADTs
+ for ((tpe, DataType(sym, _)) <- datatypes) {
+ sorts += tpe -> sym
+ }
+
+ def toDecl(c: Constructor): SExpr = {
+ val s = c.sym
+
+ testers += c.tpe -> SSymbol("is-"+s.s)
+ constructors += c.tpe -> s
+
+ SList(s :: c.fields.zipWithIndex.map {
+ case ((cs, t), i) =>
+ selectors += (c.tpe, i) -> cs
+ SList(cs, declareSort(t))
+ }.toList)
+ }
+
+ val adts = for ((tpe, DataType(sym, cases)) <- datatypes.toList) yield {
+ SList(sym :: cases.map(toDecl).toList)
+ }
+
+
+ val cmd = NonStandardCommand(SList(SSymbol("declare-datatypes"), SList(), SList(adts)))
+ sendCommand(cmd)
+
+ sorts.toB(t)
+ }
+
+ def declareVariable(id: Identifier): SSymbol = {
+ variables.cachedB(id) {
+ val s = id2sym(id)
+ val cmd = NonStandardCommand(SList(SSymbol("declare-const"), s, declareSort(id.getType)))
+ sendCommand(cmd)
+ s
+ }
+ }
+
+ def declareFunction(tfd: TypedFunDef): SSymbol = {
+ functions.cachedB(tfd) {
+ val id = if (tfd.tps.isEmpty) {
+ tfd.id
+ } else {
+ FreshIdentifier(tfd.id.name)
+ }
+ val s = id2sym(id)
+ sendCommand(DeclareFun(s.s, tfd.params.map(p => declareSort(p.tpe)), declareSort(tfd.returnType)))
+ s
+ }
+ }
+
+ def toSMT(e: Expr)(implicit bindings: Map[Identifier, SExpr]): SExpr = {
+ e match {
+ case Variable(id) =>
+ declareSort(e.getType)
+ bindings.getOrElse(id, variables.toB(id))
+
+ case IntLiteral(v) => SInt(v)
+ case BooleanLiteral(v) => SSymbol(if (v) "true" else "false")
+ case StringLiteral(s) => SString(s)
+ case Let(b,d,e) =>
+ val id = id2sym(b)
+ val value = toSMT(d)
+ val newBody = toSMT(e)(bindings + (b -> id))
+
+ SList(
+ SSymbol("let"),
+ SList(
+ SList(id, value)
+ ),
+ newBody
+ )
+
+ case er @ Error(_) =>
+ declareVariable(FreshIdentifier("error_value").setType(er.getType))
+
+ case s @ CaseClassSelector(cct, e, id) =>
+ declareSort(cct)
+ SList(selectors.toB((cct, s.selectorIndex)), toSMT(e))
+
+ case CaseClassInstanceOf(cct, e) =>
+ declareSort(cct)
+ SList(testers.toB(cct), toSMT(e))
+
+ case CaseClass(cct, es) =>
+ declareSort(cct)
+ if (es.isEmpty) {
+ constructors.toB(cct)
+ } else {
+ SList(constructors.toB(cct) :: es.map(toSMT).toList)
+ }
+
+ case t @ Tuple(es) =>
+ val tpe = normalizeType(t.getType)
+ declareSort(tpe)
+ SList(constructors.toB(tpe) :: es.map(toSMT).toList)
+
+ case ts @ TupleSelect(t, i) =>
+ val tpe = normalizeType(t.getType)
+ SList(selectors.toB((tpe, i-1)), toSMT(t))
+
+ case e @ UnaryOperator(u, _) =>
+ val op = e match {
+ case _: Not => SSymbol("not")
+ case _: UMinus => SSymbol("-")
+ case _ => reporter.fatalError("Unhandled unary "+e)
+ }
+
+ SList(op :: List(u).map(toSMT))
+
+ case e @ BinaryOperator(a, b, _) =>
+ val op = e match {
+ case _: Equals => SSymbol("=")
+ case _: Implies => SSymbol("=>")
+ case _: Iff => SSymbol("=")
+ case _: Plus => SSymbol("+")
+ case _: Minus => SSymbol("-")
+ case _: Times => SSymbol("*")
+ case _: Division => SSymbol("div")
+ case _: Modulo => SSymbol("mod")
+ case _: LessThan => SSymbol("<")
+ case _: LessEquals => SSymbol("<=")
+ case _: GreaterThan => SSymbol(">")
+ case _: GreaterEquals => SSymbol(">=")
+ case _ => reporter.fatalError("Unhandled binary "+e)
+ }
+
+ SList(op :: List(a, b).map(toSMT))
+
+ case e @ NAryOperator(sub, _) =>
+ val op = e match {
+ case _: And => SSymbol("and")
+ case _: Or => SSymbol("or")
+ case _: IfExpr => SSymbol("ite")
+ case f: FunctionInvocation => declareFunction(f.tfd)
+ case _ => reporter.fatalError("Unhandled nary "+e)
+ }
+
+ SList(op :: sub.map(toSMT).toList)
+
+
+ case o => unsupported("Tree: " + o)
+ }
+ }
+
+ def fromSMT(s: SExpr)(implicit bindings: Map[SSymbol, Expr]): Expr = s match {
+ case SInt(n) => IntLiteral(n.toInt)
+ case SSymbol("TRUE") => BooleanLiteral(true)
+ case SSymbol("FALSE") => BooleanLiteral(false)
+ case s: SSymbol if constructors.containsB(s) =>
+ constructors.toA(s) match {
+ case cct: CaseClassType =>
+ CaseClass(cct, Nil)
+ case t =>
+ unsupported("woot? for a single constructor for non-case-object: "+t)
+ }
+
+ case s: SSymbol =>
+ println(s)
+ bindings.getOrElse(s, variables.fromB(s).toVariable)
+
+ case SList((s: SSymbol) :: args) if(constructors.containsB(s)) =>
+ val rargs = args.map(fromSMT)
+ constructors.toA(s) match {
+ case cct: CaseClassType =>
+ CaseClass(cct, rargs)
+ case tt: TupleType =>
+ Tuple(rargs)
+ case t =>
+ unsupported("Woot? structural type that is non-structural: "+t)
+ }
+
+ case SList(List(SSymbol("LET"), SList(defs), body)) =>
+ val leonDefs: Seq[(SSymbol, Identifier, Expr)] = defs.map {
+ case SList(List(s : SSymbol, value)) =>
+ (s, FreshIdentifier(s.s), fromSMT(value))
+ }
+
+ val newBindings = bindings ++ leonDefs.map(d => d._1 -> d._3)
+ val newBody = fromSMT(body)(newBindings)
+
+ LetTuple(leonDefs.map(_._2), Tuple(leonDefs.map(_._3)), newBody)
+
+ case SList(SSymbol(app) :: args) => {
+ val recArgs = args.map(fromSMT)
+
+ app match {
+ case "-" =>
+ recArgs match {
+ case List(a) => UMinus(a)
+ case List(a, b) => Minus(a, b)
+ }
+
+ case _ =>
+ unsupported(s)
+ }
+ }
+ case _ =>
+ unsupported(s)
+ }
+
+ def sendCommand(cmd: Command): CommandResponse = {
+ reporter.ifDebug { debug =>
+ SMTPrinter(cmd, out)
+ out.write("\n")
+ out.flush
+ }
+
+ val response = interpreter.eval(cmd)
+ assert(!response.isInstanceOf[Error])
+ response
+ }
+}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0a6198af400e6ab43f08066113ea351958149586
--- /dev/null
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -0,0 +1,82 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
+package leon
+package solvers
+package smtlib
+
+import utils._
+import purescala._
+import Common._
+import Trees._
+import Extractors._
+import TypeTrees._
+
+import _root_.smtlib.sexpr.SExprs._
+import _root_.smtlib.interpreters.Z3Interpreter
+
+import _root_.smtlib.Commands.NonStandardCommand
+
+trait SMTLIBZ3Target extends SMTLIBTarget {
+ this: SMTLIBSolver =>
+
+ def targetName = "z3"
+
+ def getNewInterpreter() = new Z3Interpreter
+
+ val extSym = SSymbol("_")
+
+ var setSort: Option[SSymbol] = None
+
+ override def declareSort(t: TypeTree): SExpr = {
+ val tpe = normalizeType(t)
+ sorts.cachedB(tpe) {
+ tpe match {
+ case SetType(base) =>
+ declareSetSort(base)
+ case _ => super.declareSort(t)
+ }
+ }
+ }
+
+ def declareSetSort(of: TypeTree) = {
+ setSort match {
+ case None =>
+ val s = SSymbol("Set")
+ val t = SSymbol("T")
+ setSort = Some(s)
+
+ val cmd = NonStandardCommand(SList(SSymbol("define-sort"), s, SList(t), SList(SSymbol("Array"), t, SSymbol("Bool"))))
+ sendCommand(cmd)
+ case _ =>
+ }
+
+ SList(setSort.get, declareSort(of))
+ }
+
+
+ override def toSMT(e: Expr)(implicit bindings: Map[Identifier, SExpr]) = e match {
+ case fs @ FiniteSet(elems) =>
+ val ss = declareSort(fs.getType)
+ var res = SList(SList(SSymbol("as"), SSymbol("const"), ss), toSMT(BooleanLiteral(false)))
+
+ for (e <- elems) {
+ res = SList(SSymbol("store"), res, toSMT(e), toSMT(BooleanLiteral(true)))
+ }
+
+ res
+
+ case sd @ SetDifference(a, b) =>
+ // a -- b
+ // becomes:
+ // a && not(b)
+ SList(SList(extSym, SSymbol("map"), SSymbol("and")), toSMT(a), SList(SList(extSym, SSymbol("map"), SSymbol("not")), toSMT(b)))
+ case SetUnion(l, r) =>
+ SList(SList(extSym, SSymbol("map"), SSymbol("or")), toSMT(l), toSMT(r))
+
+ case SetIntersection(l, r) =>
+ SList(SList(extSym, SSymbol("map"), SSymbol("and")), toSMT(l), toSMT(r))
+
+ case _ =>
+ super.toSMT(e)
+ }
+}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 208f8f18c30a5d1de382edb60dcf2243f83178fc..f61186f077adfe309754b52329a27432bda7935d 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -279,6 +279,8 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
var reintroducedSelf = false
for (fi <- fis) {
+ var newCls = Seq[Z3AST]()
+
val defBlocker = defBlockers.get(fi) match {
case Some(defBlocker) =>
// we already have defBlocker => f(args) = body
@@ -289,20 +291,28 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
defBlockers += fi -> defBlocker
val template = getTemplate(fi.tfd)
+ reporter.debug(template)
val (newExprs, newBlocks) = template.instantiate(defBlocker, fi.args)
for((i, fis2) <- newBlocks) {
registerBlocker(nextGeneration(gen), i, fis2)
}
- newClauses ++= newExprs
+ newCls ++= newExprs
defBlocker
}
// We connect it to the defBlocker: blocker => defBlocker
if (defBlocker != id) {
- newClauses ++= List(z3.mkImplies(id, defBlocker))
+ newCls ++= List(z3.mkImplies(id, defBlocker))
+ }
+
+ reporter.debug("Unrolling behind "+fi+" ("+newCls.size+")")
+ for (cl <- newCls) {
+ reporter.debug(" . "+cl)
}
+
+ newClauses ++= newCls
}
}
@@ -548,6 +558,8 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
solver.assertCnstr(ncl)
}
+ readLine()
+
reporter.debug(" - finished unrolling")
}
}
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index 47bac75591896c4410edcf5b46f608fa485b4ccb..6aa67da6b09184fa86df2e6f477d9ce7ffc8be00 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -4,7 +4,7 @@ package leon
package synthesis
import solvers._
-import solvers.combinators.PortfolioSolver
+import solvers.combinators.PortfolioSolverSynth
import solvers.z3._
import purescala.Trees._
@@ -35,7 +35,7 @@ case class SynthesisContext(
} else if (solversToUse.size == 1) {
solversToUse.values.head
} else {
- SolverFactory( () => new PortfolioSolver(context, solversToUse.values.toSeq) with TimeoutAssumptionSolver)
+ SolverFactory( () => new PortfolioSolverSynth(context, solversToUse.values.toSeq) with TimeoutAssumptionSolver)
}
def newSolver: SynthesisContext.SynthesisSolver = {
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index ad404e220b2575d64fe44f274eb6f4091413c3d5..cf1321c9523d1cb3fe9cb64678e2f9e5b3a17fd0 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -1,4 +1,3 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
package leon
package synthesis
@@ -25,7 +24,6 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
LeonValueOptionDef("timeout", "--timeout=T", "Timeout after T seconds when searching for synthesis solutions .."),
LeonValueOptionDef("costmodel", "--costmodel=cm", "Use a specific cost model for this search"),
LeonValueOptionDef("functions", "--functions=f1:f2", "Limit synthesis of choose found within f1,f2,.."),
- LeonValueOptionDef("solvers", "--solvers=s1,s2", "Use solvers s1 and s2 (fairz3,enum)", default = Some("fairz3")),
// CEGIS options
LeonFlagOptionDef( "cegis:gencalls", "--cegis:gencalls", "Include function calls in CEGIS generators", true),
LeonFlagOptionDef( "cegis:unintprobe", "--cegis:unintprobe", "Check for UNSAT without bloecks and with uninterpreted functions", false),
@@ -39,8 +37,6 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
def processOptions(ctx: LeonContext): SynthesisOptions = {
var options = SynthesisOptions()
- val allSolvers = Set("fairz3", "enum")
-
for(opt <- ctx.options) opt match {
case LeonFlagOption("manual", v) =>
options = options.copy(manualSearch = v)
@@ -70,13 +66,6 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
ctx.reporter.fatalError(errorMsg)
}
- case LeonValueOption("solvers", ListValue(ss)) =>
- val unknownSolvers = ss.toSet -- allSolvers
- if (unknownSolvers.nonEmpty) {
- ctx.reporter.error("Unknown solver(s): "+unknownSolvers.mkString(", ")+" (Available: "+allSolvers.mkString(", ")+")")
- }
- options = options.copy(selectedSolvers = Set() ++ ss)
-
case v @ LeonValueOption("timeout", _) =>
v.asInt(ctx).foreach { t =>
options = options.copy(timeoutMs = Some(t.toLong))
diff --git a/src/main/scala/leon/utils/Bijection.scala b/src/main/scala/leon/utils/Bijection.scala
new file mode 100644
index 0000000000000000000000000000000000000000..12233df8ac96aba1b9cb1151b3a5663615c83479
--- /dev/null
+++ b/src/main/scala/leon/utils/Bijection.scala
@@ -0,0 +1,51 @@
+package leon.utils
+
+class Bijection[A, B] {
+ var a2b = Map[A, B]()
+ var b2a = Map[B, A]()
+
+ def +=(a: A, b: B): Unit = {
+ a2b += a -> b
+ b2a += b -> a
+ }
+
+ def +=(t: (A,B)): Unit = {
+ this += (t._1, t._2)
+ }
+
+ def clear(): Unit = {
+ a2b = Map()
+ b2a = Map()
+ }
+
+ def getA(b: B) = b2a.get(b)
+ def getB(a: A) = a2b.get(a)
+
+ def toA(b: B) = getA(b).get
+ def toB(a: A) = getB(a).get
+
+ def fromA(a: A) = getB(a).get
+ def fromB(b: B) = getA(b).get
+
+ def cachedB(a: A)(c: => B) = {
+ getB(a).getOrElse {
+ val res = c
+ this += a -> res
+ res
+ }
+ }
+
+ def cachedA(b: B)(c: => A) = {
+ getA(b).getOrElse {
+ val res = c
+ this += res -> b
+ res
+ }
+ }
+
+ def containsA(a: A) = a2b contains a
+ def containsB(b: B) = b2a contains b
+
+ def aSet = a2b.keySet
+ def bSet = b2a.keySet
+}
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 2d8f544bcc99d21ced82ffcb47c8d53de3af22fd..6021b6b526db643cc58faa9d8e1557f70fb630f2 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -15,6 +15,8 @@ import solvers.combinators._
import scala.collection.mutable.{Set => MutableSet}
+import _root_.smtlib.interpreters.Z3Interpreter
+
object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val name = "Analysis"
val description = "Leon Verification"
@@ -23,7 +25,6 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
override val definedOptions : Set[LeonOptionDef] = Set(
LeonValueOptionDef("functions", "--functions=f1:f2", "Limit verification to f1,f2,..."),
- LeonValueOptionDef("solvers", "--solvers=s1,s2", "Use solvers s1 and s2 (fairz3,enum)", default = Some("fairz3")),
LeonValueOptionDef("timeout", "--timeout=T", "Timeout after T seconds when trying to prove a verification condition.")
)
@@ -147,13 +148,6 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
def run(ctx: LeonContext)(program: Program) : VerificationReport = {
var filterFuns: Option[Seq[String]] = None
var timeout: Option[Int] = None
- var selectedSolvers = Set[String]("fairz3")
-
- val allSolvers = Map(
- "fairz3" -> SolverFactory(() => new FairZ3Solver(ctx, program) with TimeoutSolver),
- "enum" -> SolverFactory(() => new EnumerationSolver(ctx, program) with TimeoutSolver),
- "smt" -> SolverFactory(() => new smtlib.SMTLIBSolver(ctx, program, new _root_.smtlib.interpreters.Z3Interpreter))
- )
val reporter = ctx.reporter
@@ -161,12 +155,6 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
case LeonValueOption("functions", ListValue(fs)) =>
filterFuns = Some(fs)
- case LeonValueOption("solvers", ListValue(ss)) =>
- val unknownSolvers = ss.toSet -- allSolvers.keySet
- if (unknownSolvers.nonEmpty) {
- reporter.error("Unknown solver(s): "+unknownSolvers.mkString(", ")+" (Available: "+allSolvers.keys.mkString(", ")+")")
- }
- selectedSolvers = Set() ++ ss
case v @ LeonValueOption("timeout", _) =>
timeout = v.asInt(ctx)
@@ -175,15 +163,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
}
// Solvers selection and validation
- val solversToUse = allSolvers.filterKeys(selectedSolvers)
-
- val entrySolver = if (solversToUse.isEmpty) {
- reporter.fatalError("No solver selected. Aborting")
- } else if (solversToUse.size == 1) {
- solversToUse.values.head
- } else {
- SolverFactory( () => new PortfolioSolver(ctx, solversToUse.values.toSeq) with TimeoutSolver)
- }
+ val entrySolver = SolverFactory.getFromSettings(ctx, program)
val mainSolver = timeout match {
case Some(sec) =>
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index 86b394053f4945ad86872fbbb70bbd231aa9885a..3a52f45070b48c057b90027daebbbfed8966c8a8 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -25,7 +25,7 @@ class PureScalaVerificationRegression extends LeonTestSuite {
PreprocessingPhase andThen
AnalysisPhase
- private def mkTest(file : File, leonOptions : Seq[LeonOption], forError: Boolean)(block: Output=>Unit) = {
+ private def mkTest(file : File, leonOptions : Seq[String], forError: Boolean)(block: Output=>Unit) = {
val fullName = file.getPath()
val start = fullName.indexOf("regression")
@@ -39,10 +39,7 @@ class PureScalaVerificationRegression extends LeonTestSuite {
assert(file.exists && file.isFile && file.canRead,
"Benchmark %s is not a readable file".format(displayName))
- val ctx = testContext.copy(
- options = leonOptions.toList,
- files = List(file)
- )
+ val ctx = createLeonContext((file.getPath +: leonOptions) :_*)
val pipeline = mkPipeline
@@ -65,9 +62,10 @@ class PureScalaVerificationRegression extends LeonTestSuite {
_.endsWith(".scala"))
for(f <- fs) {
- mkTest(f, List(LeonFlagOption("feelinglucky", true)), forError)(block)
- mkTest(f, List(LeonFlagOption("codegen", true), LeonFlagOption("evalground", true), LeonFlagOption("feelinglucky", true)), forError)(block)
- mkTest(f, List(LeonValueOption("solvers", "fairz3,enum"), LeonFlagOption("codegen", true), LeonFlagOption("evalground", true), LeonFlagOption("feelinglucky", true)), forError)(block)
+ mkTest(f, List("--feelinglucky", "--library=no"), forError)(block)
+ mkTest(f, List("--codegen", "--evalground", "--feelinglucky", "--library=no"), forError)(block)
+ mkTest(f, List("--solvers=fairz3,enum", "--codegen", "--evalground", "--feelinglucky", "--library=no"), forError)(block)
+ mkTest(f, List("--solvers=smt-z3", "--library=no"), forError)(block)
}
}