From f8ef4879b517a472ab224fef36cad077a638c2a2 Mon Sep 17 00:00:00 2001 From: Etienne Kneuss <colder@php.net> Date: Mon, 25 Mar 2013 21:55:03 +0100 Subject: [PATCH] Support for LetTuple in Fairz3 --- .../leon/solvers/z3/FunctionTemplate.scala | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala index 1c8ca1294..95a319a28 100644 --- a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala +++ b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala @@ -201,6 +201,23 @@ object FunctionTemplate { val rb = rec(pathVar, replace(Map(Variable(i) -> Variable(newExpr)), b)) rb + case l @ LetTuple(is, e, b) => + val tuple : Identifier = FreshIdentifier("t", true).setType(TupleType(is.map(_.getType))) + exprVars += tuple + val re = rec(pathVar, e) + storeGuarded(pathVar, Equals(Variable(tuple), re)) + + val mapping = for ((id, i) <- is.zipWithIndex) yield { + val newId = FreshIdentifier("ti", true).setType(id.getType) + exprVars += newId + storeGuarded(pathVar, Equals(Variable(newId), TupleSelect(Variable(tuple), i+1))) + + (Variable(id) -> Variable(newId)) + } + + val rb = rec(pathVar, replace(mapping.toMap, b)) + rb + case m : MatchExpr => sys.error("MatchExpr's should have been eliminated.") case i @ Implies(lhs, rhs) => -- GitLab