translate Tuple to Z3

src/main/scala/leon/FairZ3Solver.scala

@@ -63,6 +63,10 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
     funDomainConstructors = Map.empty
     funDomainSelectors = Map.empty
 
+    tupleSorts = Map.empty
+    tupleConstructors = Map.empty
+    tupleSelectors = Map.empty
+
     mapRangeSorts.clear
     mapRangeSomeConstructors.clear
     mapRangeNoneConstructors.clear
@@ -98,6 +102,10 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
   protected[leon] var funDomainConstructors: Map[TypeTree, Z3FuncDecl] = Map.empty
   protected[leon] var funDomainSelectors: Map[TypeTree, Seq[Z3FuncDecl]] = Map.empty
 
+  protected[leon] var tupleSorts: Map[TypeTree, Z3Sort] = Map.empty
+  protected[leon] var tupleConstructors: Map[TypeTree, Z3FuncDecl] = Map.empty
+  protected[leon] var tupleSelectors: Map[TypeTree, Seq[Z3FuncDecl]] = Map.empty
+
   private var intSetMinFun: Z3FuncDecl = null
   private var intSetMaxFun: Z3FuncDecl = null
   private var setCardFuns: Map[TypeTree, Z3FuncDecl] = Map.empty
@@ -390,6 +398,17 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
         funSort
       }
     }
+    case tt @ TupleType(tpes) => tupleSorts.get(tt) match {
+      case Some(s) => s
+      case None => {
+        val tpesSorts = tpes.map(typeToSort)
+        val (tupleSort, consTuple, projsTuple) = z3.mkTupleSort(tpes.map(_.toString).mkString("Tuple2(",", ", ")"), tpesSorts: _*)
+        tupleSorts += (tt -> tupleSort)
+        tupleConstructors += (tt -> consTuple)
+        tupleSelectors += (tt -> projsTuple)
+        tupleSort
+      }
+    }
     case other => fallbackSorts.get(other) match {
       case Some(s) => s
       case None => {
@@ -839,6 +858,16 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
       //println("Stacking up call for:")
       //println(ex)
       val recResult = (ex match {
+        case tu@Tuple(args) => {
+          typeToSort(tu.getType)
+          val constructor = tupleConstructors(tu.getType)
+          constructor(args.map(rec(_)): _*)
+        }
+        case ts@TupleSelect(tu, i) => {
+          typeToSort(tu.getType)
+          val selector = tupleSelectors(tu.getType)(i-1)
+          selector(rec(tu))
+        }
         case Let(i, e, b) => {
           val re = rec(e)
           z3Vars = z3Vars + (i -> re)