From df563bc0cfb8ccf093aad5a34b31272331e34377 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 7 May 2015 18:18:36 +0200
Subject: [PATCH] Remove some code duplication
---
.../smtlib/SMTLIBCVC4QuantifiedTarget.scala | 27 ++++++-------------
.../smtlib/SMTLIBZ3QuantifiedTarget.scala | 22 ++++-----------
2 files changed, 13 insertions(+), 36 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
index e2bd8e2cf..c9189acd5 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
@@ -4,17 +4,16 @@ package leon
package solvers.smtlib
import purescala._
-import Common.FreshIdentifier
import Expressions._
import Definitions.{Program, TypedFunDef}
import Constructors.{application, implies}
import DefOps.typedTransitiveCallees
-import smtlib.parser.Commands.Assert
-import smtlib.parser.Commands._
+import smtlib.parser.Commands.{Assert => SMTAssert, _}
import smtlib.parser.Terms._
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) {
override val targetName = "cvc4-quantified"
@@ -34,27 +33,17 @@ abstract class SMTLIBCVC4QuantifiedTarget(context: LeonContext, program: Program
val (withParams, withoutParams) = funs.toSeq partition( _.params.nonEmpty)
val parameterlessAssertions = withoutParams filterNot functions.containsA flatMap { tfd =>
- // FIXME: Here we actually want to call super[SMTLIBCVC4Target].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))
+ val s = super.declareFunction(tfd)
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 term = implies(
tfd.precondition getOrElse BooleanLiteral(true),
application(post, Seq(FunctionInvocation(tfd, Seq())))
)
- Assert(toSMT(term)(Map()))
+ SMTAssert(toSMT(term)(Map()))
}
Seq(bodyAssert) ++ specAssert
@@ -106,7 +95,7 @@ abstract class SMTLIBCVC4QuantifiedTarget(context: LeonContext, program: Program
tfd.precondition getOrElse BooleanLiteral(true),
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
// For this solver, we prefer the variables of assert() commands to be exist. quantified instead of free
override def assertCnstr(expr: Expr) =
- sendCommand(Assert(quantifiedTerm(Exists, expr)))
+ sendCommand(SMTAssert(quantifiedTerm(Exists, expr)))
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
index bec1e7ac1..041f52260 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
@@ -6,12 +6,12 @@ import DefOps._
import Definitions._
import Expressions._
import Constructors._
-import smtlib.parser.Commands.{DeclareFun, Assert}
+import smtlib.parser.Commands.{Assert => SMTAssert}
import smtlib.parser.Terms.{ForAll => SMTForall, SSymbol}
/**
* 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) {
@@ -30,19 +30,7 @@ class SMTLIBZ3QuantifiedTarget(context: LeonContext, program: Program) extends S
val smtFunDecls = funs.toSeq.collect {
case tfd if !functions.containsA(tfd) =>
- val id = if (tfd.tps.isEmpty) {
- 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
+ super.declareFunction(tfd)
}
smtFunDecls foreach { sym =>
val tfd = functions.toA(sym)
@@ -54,7 +42,7 @@ class SMTLIBZ3QuantifiedTarget(context: LeonContext, program: Program) extends S
tfd.body.get
)
)
- sendCommand(Assert(term))
+ sendCommand(SMTAssert(term))
tfd.postcondition foreach { post =>
val axiom = implies(
@@ -64,7 +52,7 @@ class SMTLIBZ3QuantifiedTarget(context: LeonContext, program: Program) extends S
Seq(FunctionInvocation(tfd, tfd.params map { _.toVariable }))
)
)
- sendCommand(Assert(quantifiedTerm(SMTForall, axiom)))
+ sendCommand(SMTAssert(quantifiedTerm(SMTForall, axiom)))
}
}
--
GitLab