From 383961f2d9782913147f8a0a22d8b16a20533780 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 8 May 2015 14:01:31 +0200
Subject: [PATCH] MapUnion in SMTSolver (bad)
---
.../leon/solvers/smtlib/SMTLIBSolver.scala | 45 +++++++++++++++++++
1 file changed, 45 insertions(+)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 9557b3030..60da64f87 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -18,6 +18,8 @@ import _root_.smtlib.common._
import _root_.smtlib.printer.{RecursivePrinter => SMTPrinter}
import _root_.smtlib.parser.Commands.{Constructor => SMTConstructor, FunDef => _, Assert => SMTAssert, _}
import _root_.smtlib.parser.Terms.{
+ ForAll => SMTForall,
+ Exists => SMTExists,
Identifier => SMTIdentifier,
Let => SMTLet,
_
@@ -446,6 +448,42 @@ abstract class SMTLIBSolver(val context: LeonContext,
}
}
+ protected def declareMapUnion(from: TypeTree, to: TypeTree): SSymbol = {
+ // FIXME cache results
+ val a = declareSort(from)
+ val b = declareSort(OptionManager.leonOptionType(to))
+ val arraySort = Sort(SMTIdentifier(SSymbol("Array")), Seq(a, b))
+
+ val f = freshSym("map_union")
+
+ sendCommand(DeclareFun(f, Seq(arraySort, arraySort), arraySort))
+
+ val v = SSymbol("v")
+ val a1 = SSymbol("a1")
+ val a2 = SSymbol("a2")
+
+ val axiom = SMTForall(
+ SortedVar(a1, arraySort), Seq(SortedVar(a2, arraySort), SortedVar(v,a)),
+ Core.Equals(
+ ArraysEx.Select(
+ FunctionApplication(f: QualifiedIdentifier, Seq(a1: Term, a2: Term)),
+ v: Term
+ ),
+ Core.ITE(
+ FunctionApplication(
+ OptionManager.someTester(to),
+ Seq(ArraysEx.Select(a2: Term, v: Term))
+ ),
+ ArraysEx.Select(a2,v),
+ ArraysEx.Select(a1,v)
+ )
+ )
+ )
+
+ sendCommand(SMTAssert(axiom))
+ f
+ }
+
protected def toSMT(e: Expr)(implicit bindings: Map[Identifier, Term]): Term = {
e match {
case Variable(id) =>
@@ -569,6 +607,13 @@ abstract class SMTLIBSolver(val context: LeonContext,
Seq(ArraysEx.Select(toSMT(m), toSMT(k)))
)
+ case MapUnion(m1, m2) =>
+ val MapType(vk, vt) = m1.getType
+ FunctionApplication(
+ declareMapUnion(vk, vt),
+ Seq(toSMT(m1), toSMT(m2))
+ )
+
case p : Passes =>
toSMT(matchToIfThenElse(p.asConstraint))
--
GitLab