Skip to content
Snippets Groups Projects
Commit df563bc0 authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

Remove some code duplication

parent 293b9f2c
Branches
Tags
No related merge requests found
...@@ -4,17 +4,16 @@ package leon ...@@ -4,17 +4,16 @@ package leon
package solvers.smtlib package solvers.smtlib
import purescala._ import purescala._
import Common.FreshIdentifier
import Expressions._ import Expressions._
import Definitions.{Program, TypedFunDef} import Definitions.{Program, TypedFunDef}
import Constructors.{application, implies} import Constructors.{application, implies}
import DefOps.typedTransitiveCallees import DefOps.typedTransitiveCallees
import smtlib.parser.Commands.Assert import smtlib.parser.Commands.{Assert => SMTAssert, _}
import smtlib.parser.Commands._
import smtlib.parser.Terms._ import smtlib.parser.Terms._
import smtlib.theories.Core.Equals import smtlib.theories.Core.Equals
// This solver utilizes the define-funs-rec command of SMTLIB-2.5 to define mutually recursive functions.
// It is not meant as an underlying solver to UnrollingSolver, and does not handle HOFs.
abstract class SMTLIBCVC4QuantifiedTarget(context: LeonContext, program: Program) extends SMTLIBCVC4Target(context, program) { abstract class SMTLIBCVC4QuantifiedTarget(context: LeonContext, program: Program) extends SMTLIBCVC4Target(context, program) {
override val targetName = "cvc4-quantified" override val targetName = "cvc4-quantified"
...@@ -34,27 +33,17 @@ abstract class SMTLIBCVC4QuantifiedTarget(context: LeonContext, program: Program ...@@ -34,27 +33,17 @@ abstract class SMTLIBCVC4QuantifiedTarget(context: LeonContext, program: Program
val (withParams, withoutParams) = funs.toSeq partition( _.params.nonEmpty) val (withParams, withoutParams) = funs.toSeq partition( _.params.nonEmpty)
val parameterlessAssertions = withoutParams filterNot functions.containsA flatMap { tfd => val parameterlessAssertions = withoutParams filterNot functions.containsA flatMap { tfd =>
// FIXME: Here we actually want to call super[SMTLIBCVC4Target].declareFunction(tfd), val s = super.declareFunction(tfd)
// but we inline it to work around a freakish compiler bug
val id = if (tfd.tps.isEmpty) {
tfd.id
} else {
FreshIdentifier(tfd.id.name)
}
sendCommand(DeclareFun(id2sym(id), Seq(), declareSort(tfd.returnType)))
// Until here, that is.
functions +=(tfd, id2sym(id))
try { try {
val bodyAssert = Assert(Equals(id2sym(id): Term, toSMT(tfd.body.get)(Map()))) val bodyAssert = SMTAssert(Equals(s: Term, toSMT(tfd.body.get)(Map())))
val specAssert = tfd.postcondition map { post => val specAssert = tfd.postcondition map { post =>
val term = implies( val term = implies(
tfd.precondition getOrElse BooleanLiteral(true), tfd.precondition getOrElse BooleanLiteral(true),
application(post, Seq(FunctionInvocation(tfd, Seq()))) application(post, Seq(FunctionInvocation(tfd, Seq())))
) )
Assert(toSMT(term)(Map())) SMTAssert(toSMT(term)(Map()))
} }
Seq(bodyAssert) ++ specAssert Seq(bodyAssert) ++ specAssert
...@@ -106,7 +95,7 @@ abstract class SMTLIBCVC4QuantifiedTarget(context: LeonContext, program: Program ...@@ -106,7 +95,7 @@ abstract class SMTLIBCVC4QuantifiedTarget(context: LeonContext, program: Program
tfd.precondition getOrElse BooleanLiteral(true), tfd.precondition getOrElse BooleanLiteral(true),
application(post, Seq(FunctionInvocation(tfd, tfd.params map { _.toVariable}))) application(post, Seq(FunctionInvocation(tfd, tfd.params map { _.toVariable})))
) )
sendCommand(Assert(quantifiedTerm(ForAll, term))) sendCommand(SMTAssert(quantifiedTerm(ForAll, term)))
} }
} }
...@@ -118,6 +107,6 @@ abstract class SMTLIBCVC4QuantifiedTarget(context: LeonContext, program: Program ...@@ -118,6 +107,6 @@ abstract class SMTLIBCVC4QuantifiedTarget(context: LeonContext, program: Program
// For this solver, we prefer the variables of assert() commands to be exist. quantified instead of free // For this solver, we prefer the variables of assert() commands to be exist. quantified instead of free
override def assertCnstr(expr: Expr) = override def assertCnstr(expr: Expr) =
sendCommand(Assert(quantifiedTerm(Exists, expr))) sendCommand(SMTAssert(quantifiedTerm(Exists, expr)))
} }
...@@ -6,12 +6,12 @@ import DefOps._ ...@@ -6,12 +6,12 @@ import DefOps._
import Definitions._ import Definitions._
import Expressions._ import Expressions._
import Constructors._ import Constructors._
import smtlib.parser.Commands.{DeclareFun, Assert} import smtlib.parser.Commands.{Assert => SMTAssert}
import smtlib.parser.Terms.{ForAll => SMTForall, SSymbol} import smtlib.parser.Terms.{ForAll => SMTForall, SSymbol}
/** /**
* This solver models function definitions as universally quantified formulas. * This solver models function definitions as universally quantified formulas.
* It is not meant as an underlying solver to UnrollingSolver. * It is not meant as an underlying solver to UnrollingSolver, and does not handle HOFs.
*/ */
class SMTLIBZ3QuantifiedTarget(context: LeonContext, program: Program) extends SMTLIBZ3Target(context, program) { class SMTLIBZ3QuantifiedTarget(context: LeonContext, program: Program) extends SMTLIBZ3Target(context, program) {
...@@ -30,19 +30,7 @@ class SMTLIBZ3QuantifiedTarget(context: LeonContext, program: Program) extends S ...@@ -30,19 +30,7 @@ class SMTLIBZ3QuantifiedTarget(context: LeonContext, program: Program) extends S
val smtFunDecls = funs.toSeq.collect { val smtFunDecls = funs.toSeq.collect {
case tfd if !functions.containsA(tfd) => case tfd if !functions.containsA(tfd) =>
val id = if (tfd.tps.isEmpty) { super.declareFunction(tfd)
tfd.id
} else {
tfd.id.freshen
}
val sym = id2sym(id)
functions +=(tfd, sym)
sendCommand(DeclareFun(
sym,
tfd.params map { p => declareSort(p.getType) },
declareSort(tfd.returnType)
))
sym
} }
smtFunDecls foreach { sym => smtFunDecls foreach { sym =>
val tfd = functions.toA(sym) val tfd = functions.toA(sym)
...@@ -54,7 +42,7 @@ class SMTLIBZ3QuantifiedTarget(context: LeonContext, program: Program) extends S ...@@ -54,7 +42,7 @@ class SMTLIBZ3QuantifiedTarget(context: LeonContext, program: Program) extends S
tfd.body.get tfd.body.get
) )
) )
sendCommand(Assert(term)) sendCommand(SMTAssert(term))
tfd.postcondition foreach { post => tfd.postcondition foreach { post =>
val axiom = implies( val axiom = implies(
...@@ -64,7 +52,7 @@ class SMTLIBZ3QuantifiedTarget(context: LeonContext, program: Program) extends S ...@@ -64,7 +52,7 @@ class SMTLIBZ3QuantifiedTarget(context: LeonContext, program: Program) extends S
Seq(FunctionInvocation(tfd, tfd.params map { _.toVariable })) Seq(FunctionInvocation(tfd, tfd.params map { _.toVariable }))
) )
) )
sendCommand(Assert(quantifiedTerm(SMTForall, axiom))) sendCommand(SMTAssert(quantifiedTerm(SMTForall, axiom)))
} }
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment