From 38c581f2403e4e6f28eeb60a2eaa81d05651bec5 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 30 Mar 2015 14:44:09 +0200
Subject: [PATCH] assert variables exist. quantified instead of free
---
.../smtlib/SMTLIBUnrollingCVC4Target.scala | 19 ++++++++++++++++++-
1 file changed, 18 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala
index 0600de6cb..9fcbc9de9 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala
@@ -3,9 +3,10 @@
package leon
package solvers.smtlib
+import leon.purescala.Expressions.Expr
import purescala.Definitions.TypedFunDef
import purescala.DefOps.typedTransitiveCallees
-import purescala.ExprOps.matchToIfThenElse
+import leon.purescala.ExprOps.{variablesOf, matchToIfThenElse}
import smtlib.parser.Commands._
import smtlib.parser.Terms._
@@ -54,4 +55,20 @@ trait SMTLIBUnrollingCVC4Target extends SMTLIBCVC4Target {
}
}
+ override def assertCnstr(expr: Expr): Unit = {
+ val existentials = variablesOf(expr).toSeq
+
+ val term = if (existentials.isEmpty) toSMT(expr)(Map()) else {
+ val es = existentials map { id =>
+ SortedVar(id2sym(id), declareSort(id.getType))
+ }
+ Exists(
+ es.head,
+ es.tail,
+ toSMT(expr)(existentials.map { id => id -> (id2sym(id): Term)}.toMap)
+ )
+ }
+ sendCommand(Assert(term))
+ }
+
}
--
GitLab