From bba8bc86b5386b81eb8db2e7325b1314ee48c263 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Fri, 21 Nov 2014 11:01:50 +0100
Subject: [PATCH] Some small changes to get CVC4 smt solver working with HO
functions
---
.../leon/solvers/smtlib/SMTLIBCVC4Target.scala | 9 +++++++++
.../leon/solvers/templates/UnrollingBank.scala | 16 +++++++++++++---
2 files changed, 22 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index 185d8646f..074fffce4 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -78,6 +78,15 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
case FiniteSet(elems) => elems
}).flatten.toSet).setType(tpe)
+ // FIXME (nicolas)
+ // 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, ft)
+
+ case (FunctionApplication(QualifiedIdentifier(SMTIdentifier(SSymbol("const"), _), _), Seq(elem)), RawArrayType(k, v)) =>
+ RawArrayValue(k, Map(), fromSMT(elem, v))
+
case _ =>
super[SMTLIBTarget].fromSMT(s, tpe)
}
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index fc6782dd1..4c7009e0f 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -157,6 +157,7 @@ class UnrollingBank[T](reporter: Reporter, templateGenerator: TemplateGenerator[
private def extendAppBlock(app: (T, App[T]), infos: Set[TemplateAppInfo[T]]) : T = {
assert(!appInfo.isDefinedAt(app), "appInfo -= app must have been called to ensure blocker freshness")
assert(appBlockers.isDefinedAt(app), "freshAppBlocks must have been called on app before it can be unlocked")
+ assert(infos.nonEmpty, "No point in extending blockers if no templates have been unrolled!")
val nextB = encoder.encodeId(FreshIdentifier("b_lambda", true).setType(BooleanType))
val extension = encoder.mkOr((infos.map(_.equals).toSeq :+ nextB) : _*)
@@ -194,7 +195,14 @@ class UnrollingBank[T](reporter: Reporter, templateGenerator: TemplateGenerator[
}
// ...so we must force it to true!
- template.start +: (newClauses ++ blockClauses)
+ val clauses = template.start +: (newClauses ++ blockClauses)
+
+ reporter.debug("Generating clauses for: " + expr)
+ for (cls <- clauses) {
+ reporter.debug(" . " + cls)
+ }
+
+ clauses
}
def nextGeneration(gen: Int) = gen + 3
@@ -238,8 +246,10 @@ class UnrollingBank[T](reporter: Reporter, templateGenerator: TemplateGenerator[
blockerToApp = blockerToApp -- ids
appInfo = appInfo -- apps
- for ((app, (_, _, _, _, infos)) <- appInfos) {
- newClauses :+= extendAppBlock(app, infos)
+ for ((app, (_, _, _, _, infos)) <- appInfos if infos.nonEmpty) {
+ val extension = extendAppBlock(app, infos)
+ reporter.debug(" -> extending lambda blocker: " + extension)
+ newClauses :+= extension
}
for ((id, (gen, _, _, infos)) <- callInfos; info @ TemplateCallInfo(tfd, args) <- infos) {
--
GitLab