Commit 3ab4d176 authored by Eva Darulova's avatar Eva Darulova
Browse files

z3 and cvc4 solvers

parent 838529d5
......@@ -7,12 +7,8 @@ Acknowledgements
A big portion of the infrastructure has been inspired by and sometimes
directly taken from the Leon project (see the LEON_LICENSE).
Especially the following files bear more than a passing resemblance to Leon's code:
frontend.{ASTExtractors, CodeExtraction, DaisyExtraction, ExtractionPhase,
SaveImports, ScalaCompiler, SimpleReporter}
lang.{DefOps, Definitions, Extractors, Identifiers, PrettyPrinter, TreeOps, Trees, Types,CallGraph, Transformer, GraphOps}
utils.{Context,DaisyFatalError, DaisyOption, DaisyPhase, DebugSection, Position, Reporter,
Settings, Timer}
solvers.{SMTLibSolver, SMTLibTarget, Bijection}
Especially the files in frontend, lang, solvers and utils bear more than
a passing resemblance to Leon's code.
Leon version used: 978a08cab28d3aa6414a47997dde5d64b942cd3e
/* Copyright 2015 EPFL, Lausanne */
package daisy
package solvers
// import OptionParsers._
import lang._
import Definitions.Program
import Identifiers._
import Trees.{Assert => _, _}
import Extractors._
import Constructors._
import Types._
import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, ForAll => SMTForall, _}
import _root_.smtlib.parser.Commands._
import _root_.smtlib.interpreters.CVC4Interpreter
import _root_.smtlib.theories._
class CVC4Solver(context: Context, program: Program) extends SMTLibSolver(context, program) {
def targetName = "cvc4"
// TODO: CVC4 opetions
def userDefinedOps(ctx: Context) = {
//ctx.findOptionOrDefault(SMTLIBCVC4Component.optCVC4Options)
}
def interpreterOps(ctx: Context) = {
Seq(
"-q",
"--produce-models",
"--no-incremental",
"--tear-down-incremental",
"--rewrite-divk",
// "--dt-rewrite-error-sel", // Removing since it causes CVC4 to segfault on some inputs
"--print-success",
"--lang", "smt"
) //++ userDefinedOps(ctx).toSeq
}
def getNewInterpreter(ctx: Context) = {
val opts = interpreterOps(ctx)
reporter.debug("Invoking solver with "+opts.mkString(" "))
new CVC4Interpreter("cvc4", opts.toArray)
}
override def declareSort(t: TypeTree): Sort = {
val tpe = normalizeType(t)
sorts.cachedB(tpe) {
tpe match {
case TypeParameter(id) =>
val s = id2sym(id)
val cmd = DeclareSort(s, 0)
sendCommand(cmd)
Sort(SMTIdentifier(s))
case SetType(base) =>
Sort(SMTIdentifier(SSymbol("Set")), Seq(declareSort(base)))
case _ =>
super.declareSort(t)
}
}
}
override def fromSMT(s: Term, tpe: TypeTree)(implicit lets: Map[SSymbol, Term], letDefs: Map[SSymbol, DefineFun]): Expr = (s, tpe) match {
case (SimpleSymbol(s), tp: TypeParameter) =>
val n = s.name.split("_").toList.last
GenericValue(tp, n.toInt)
case (QualifiedIdentifier(SMTIdentifier(SSymbol("emptyset"), Seq()), _), SetType(base)) =>
EmptySet(base)
case (FunctionApplication(SimpleSymbol(SSymbol("__array_store_all__")), Seq(_, elem)), RawArrayType(k,v)) =>
RawArrayValue(k, Map(), fromSMT(elem, v))
case (FunctionApplication(SimpleSymbol(SSymbol("__array_store_all__")), Seq(_, elem)), ft @ FunctionType(from,to)) =>
finiteLambda(fromSMT(elem, to), Seq.empty, from)
case (FunctionApplication(SimpleSymbol(SSymbol("store")), Seq(arr, key, elem)), RawArrayType(k,v)) =>
val RawArrayValue(_, elems, base) = fromSMT(arr, tpe)
RawArrayValue(k, elems + (fromSMT(key, k) -> fromSMT(elem, v)), base)
case (FunctionApplication(SimpleSymbol(SSymbol("store")), Seq(arr, key, elem)), ft @ FunctionType(from,to)) =>
val FiniteLambda(dflt, mapping) = fromSMT(arr, tpe)
finiteLambda(dflt, mapping :+ (fromSMT(key, tupleTypeWrap(from)) -> fromSMT(elem, to)), from)
case (FunctionApplication(SimpleSymbol(SSymbol("singleton")), elems), SetType(base)) =>
finiteSet(elems.map(fromSMT(_, base)).toSet, base)
case (FunctionApplication(SimpleSymbol(SSymbol("insert")), elems), SetType(base)) =>
val selems = elems.init.map(fromSMT(_, base))
val FiniteSet(se) = fromSMT(elems.last, tpe)
finiteSet(se ++ selems, base)
case (FunctionApplication(SimpleSymbol(SSymbol("union")), elems), SetType(base)) =>
finiteSet(elems.map(fromSMT(_, tpe) match {
case FiniteSet(elems) => elems
}).flatten.toSet, base)
// some versions of CVC4 seem to generate array constants with "as const" notation instead of the __array_store_all__
// one I've witnessed up to now. Don't know why this is happening...
case (FunctionApplication(QualifiedIdentifier(SMTIdentifier(SSymbol("const"), _), _), Seq(elem)), ft @ FunctionType(from, to)) =>
finiteLambda(fromSMT(elem, to), Seq.empty, from)
case (FunctionApplication(QualifiedIdentifier(SMTIdentifier(SSymbol("const"), _), _), Seq(elem)), RawArrayType(k, v)) =>
RawArrayValue(k, Map(), fromSMT(elem, v))
case _ =>
super.fromSMT(s, tpe)
}
override def toSMT(e: Expr)(implicit bindings: Map[Identifier, Term]) = e match {
case a @ FiniteArray(elems, default, size) =>
val tpe @ ArrayType(base) = normalizeType(a.getType)
declareSort(tpe)
var ar: Term = declareVariable(FreshIdentifier("arrayconst", RawArrayType(Int32Type, base)))
for ((i, e) <- elems) {
ar = FunctionApplication(SSymbol("store"), Seq(ar, toSMT(IntLiteral(i)), toSMT(e)))
}
FunctionApplication(constructors.toB(tpe), Seq(toSMT(size), ar))
case fm @ FiniteMap(elems) =>
import OptionManager._
val mt @ MapType(from, to) = fm.getType
declareSort(mt)
var m: Term = declareVariable(FreshIdentifier("mapconst", RawArrayType(from, leonOptionType(to))))
sendCommand(Assert(SMTForall(
SortedVar(SSymbol("mapelem"), declareSort(from)), Seq(),
Core.Equals(
ArraysEx.Select(m, SSymbol("mapelem")),
toSMT(mkLeonNone(to))
)
)))
for ((k, v) <- elems) {
m = FunctionApplication(SSymbol("store"), Seq(m, toSMT(k), toSMT(mkLeonSome(v))))
}
m
/**
* ===== Set operations =====
*/
case fs @ FiniteSet(elems) =>
if (elems.isEmpty) {
QualifiedIdentifier(SMTIdentifier(SSymbol("emptyset")), Some(declareSort(fs.getType)))
} else {
val selems = elems.toSeq.map(toSMT)
val sgt = FunctionApplication(SSymbol("singleton"), Seq(selems.head))
if (selems.size > 1) {
FunctionApplication(SSymbol("insert"), selems.tail :+ sgt)
} else {
sgt
}
}
case SubsetOf(ss, s) =>
FunctionApplication(SSymbol("subset"), Seq(toSMT(ss), toSMT(s)))
case ElementOfSet(e, s) =>
FunctionApplication(SSymbol("member"), Seq(toSMT(e), toSMT(s)))
case SetDifference(a, b) =>
FunctionApplication(SSymbol("setminus"), Seq(toSMT(a), toSMT(b)))
case SetUnion(a, b) =>
FunctionApplication(SSymbol("union"), Seq(toSMT(a), toSMT(b)))
case SetIntersection(a, b) =>
FunctionApplication(SSymbol("intersection"), Seq(toSMT(a), toSMT(b)))
case _ =>
super.toSMT(e)
}
}
/*object SMTLIBCVC4Component extends LeonComponent {
val name = "cvc4 solver"
val description = "Solver invoked when --solvers=smt-cvc4"
val optCVC4Options = new LeonOptionDef[Set[String]] {
val name = "solver:cvc4"
val description = "Pass extra arguments to CVC4"
val default = Set[String]()
val parser = setParser(stringParser)
val usageRhs = "<cvc4-opt>"
}
override val definedOptions : Set[LeonOptionDef[Any]] = Set(optCVC4Options)
}*/
This diff is collapsed.
/* Copyright 2015 EPFL, Lausanne */
package daisy
package solvers
import lang._
import Identifiers._
import Definitions.Program
import Trees._
import Extractors._
import Types._
import Constructors._
import TreeOps.simplestValue
import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
import _root_.smtlib.parser.Commands.{FunDef => SMTFunDef, _}
import _root_.smtlib.interpreters.Z3Interpreter
import _root_.smtlib.parser.CommandsResponses.GetModelResponseSuccess
import _root_.smtlib.theories.Core.{Equals => SMTEquals, _}
import _root_.smtlib.theories.ArraysEx
class Z3Solver(context: Context, program: Program) extends SMTLibSolver(context, program) {
def targetName = "z3"
def interpreterOps(ctx: Context) = {
Seq(
"-in",
"-smt2"
)
}
def getNewInterpreter(ctx: Context) = new Z3Interpreter("z3", interpreterOps(ctx).toArray)
val extSym = SSymbol("_")
var setSort: Option[SSymbol] = None
override def declareSort(t: TypeTree): Sort = {
val tpe = normalizeType(t)
sorts.cachedB(tpe) {
tpe match {
case SetType(base) =>
super.declareSort(BooleanType)
declareSetSort(base)
case _ =>
super.declareSort(t)
}
}
}
def declareSetSort(of: TypeTree): Sort = {
setSort match {
case None =>
val s = SSymbol("Set")
val t = SSymbol("T")
setSort = Some(s)
val arraySort = Sort(SMTIdentifier(SSymbol("Array")),
Seq(Sort(SMTIdentifier(t)), BoolSort()))
val cmd = DefineSort(s, Seq(t), arraySort)
sendCommand(cmd)
case _ =>
}
Sort(SMTIdentifier(setSort.get), Seq(declareSort(of)))
}
override def fromSMT(s: Term, tpe: TypeTree)(implicit lets: Map[SSymbol, Term], letDefs: Map[SSymbol, DefineFun]): Expr = (s, tpe) match {
case (SimpleSymbol(s), tp: TypeParameter) =>
val n = s.name.split("!").toList.last
GenericValue(tp, n.toInt)
case (QualifiedIdentifier(ExtendedIdentifier(SSymbol("as-array"), k: SSymbol), _), tpe) =>
if (letDefs contains k) {
// Need to recover value form function model
fromRawArray(extractRawArray(letDefs(k), tpe), tpe)
} else {
unsupported(" as-array on non-function or unknown symbol "+k)
}
case (FunctionApplication(
QualifiedIdentifier(SMTIdentifier(SSymbol("const"), _), Some(ArraysEx.ArraySort(k, v))),
Seq(defV)
), tpe) =>
val ktpe = sorts.fromB(k)
val vtpe = sorts.fromB(v)
fromRawArray(RawArrayValue(ktpe, Map(), fromSMT(defV, vtpe)), tpe)
case _ =>
super.fromSMT(s, tpe)
}
override def toSMT(e: Expr)(implicit bindings: Map[Identifier, Term]): Term = e match {
case a @ FiniteArray(elems, oDef, size) =>
val tpe @ ArrayType(base) = normalizeType(a.getType)
declareSort(tpe)
val default: Expr = oDef.getOrElse(simplestValue(base))
var ar: Term = ArrayConst(declareSort(RawArrayType(Int32Type, base)), toSMT(default))
for ((i, e) <- elems) {
ar = ArraysEx.Store(ar, toSMT(IntLiteral(i)), toSMT(e))
}
FunctionApplication(constructors.toB(tpe), List(toSMT(size), ar))
/**
* ===== Set operations =====
*/
case fs @ FiniteSet(elems) =>
val ss = declareSort(fs.getType)
var res: Term = FunctionApplication(
QualifiedIdentifier(SMTIdentifier(SSymbol("const")), Some(ss)),
Seq(toSMT(BooleanLiteral(false)))
)
for (e <- elems) {
res = ArraysEx.Store(res, toSMT(e), toSMT(BooleanLiteral(true)))
}
res
case SubsetOf(ss, s) =>
// a isSubset b ==> (a zip b).map(implies) == (* => true)
val allTrue = ArrayConst(declareSort(s.getType), True())
SMTEquals(ArrayMap(SSymbol("implies"), toSMT(ss), toSMT(s)), allTrue)
case ElementOfSet(e, s) =>
ArraysEx.Select(toSMT(s), toSMT(e))
case SetDifference(a, b) =>
// a -- b
// becomes:
// a && not(b)
ArrayMap(SSymbol("and"), toSMT(a), ArrayMap(SSymbol("not"), toSMT(b)))
case SetUnion(l, r) =>
ArrayMap(SSymbol("or"), toSMT(l), toSMT(r))
case SetIntersection(l, r) =>
ArrayMap(SSymbol("and"), toSMT(l), toSMT(r))
case _ =>
super.toSMT(e)
}
def extractRawArray(s: DefineFun, tpe: TypeTree)(implicit lets: Map[SSymbol, Term], letDefs: Map[SSymbol, DefineFun]): RawArrayValue = s match {
case DefineFun(SMTFunDef(a, Seq(SortedVar(arg, akind)), rkind, body)) =>
val (argTpe, retTpe) = tpe match {
case SetType(base) => (base, BooleanType)
case ArrayType(base) => (Int32Type, base)
case FunctionType(args, ret) => (tupleTypeWrap(args), ret)
case RawArrayType(from, to) => (from, to)
case _ => unsupported("Unsupported type for (un)packing into raw arrays: "+tpe +" (got kinds "+akind+" -> "+rkind+")")
}
def extractCases(e: Term): (Map[Expr, Expr], Expr) = e match {
case ITE(SMTEquals(SimpleSymbol(`arg`), k), v, e) =>
val (cs, d) = extractCases(e)
(Map(fromSMT(k, argTpe) -> fromSMT(v, retTpe)) ++ cs, d)
case e =>
(Map(),fromSMT(e, retTpe))
}
val (cases, default) = extractCases(body)
RawArrayValue(argTpe, cases, default)
case _ =>
unsupported("Unable to extract "+s)
}
// EK: We use get-model instead in order to extract models for arrays
override def getModel: Map[Identifier, Expr] = {
val cmd = GetModel()
val res = sendCommand(cmd)
val smodel: Seq[SExpr] = res match {
case GetModelResponseSuccess(model) => model
case _ => Nil
}
var modelFunDefs = Map[SSymbol, DefineFun]()
// First pass to gather functions (arrays defs)
for (me <- smodel) me match {
case me @ DefineFun(SMTFunDef(a, args, _, _)) if args.nonEmpty =>
modelFunDefs += a -> me
case _ =>
}
var model = Map[Identifier, Expr]()
for (me <- smodel) me match {
case DefineFun(SMTFunDef(s, args, kind, e)) =>
if(args.isEmpty) {
variables.getA(s) match {
case Some(id) =>
// EK: this is a little hack, we pass models for array functions as let-defs
model += id -> fromSMT(e, id.getType)(Map(), modelFunDefs)
case _ => // function, should be handled elsewhere
}
}
case _ =>
}
model
}
object ArrayMap {
def apply(op: SSymbol, arrs: Term*) = {
FunctionApplication(
QualifiedIdentifier(SMTIdentifier(SSymbol("map"), List(op))),
arrs
)
}
}
object ArrayConst {
def apply(sort: Sort, default: Term) = {
FunctionApplication(
QualifiedIdentifier(SMTIdentifier(SSymbol("const")), Some(sort)),
List(default))
}
}
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment