From 85c3a200c375a126ea9c6fe2e210a21e5812cd95 Mon Sep 17 00:00:00 2001
From: Philipp Ruemmer <ph_r@gmx.net>
Date: Mon, 8 Nov 2021 10:56:14 +0100
Subject: [PATCH] initial support for polymorphic ADTs

---
 regression-tests/horn-adt/Answers               |  4 ++++
 regression-tests/horn-adt/polymorphicTuple.smt2 | 15 +++++++++++++++
 regression-tests/horn-adt/runtests              |  3 ++-
 src/lazabs/viewer/HornSMTPrinter.scala          |  2 +-
 4 files changed, 22 insertions(+), 2 deletions(-)
 create mode 100644 regression-tests/horn-adt/polymorphicTuple.smt2

diff --git a/regression-tests/horn-adt/Answers b/regression-tests/horn-adt/Answers
index 2f17d5b5..336755d5 100644
--- a/regression-tests/horn-adt/Answers
+++ b/regression-tests/horn-adt/Answers
@@ -75,5 +75,9 @@ unsat
 5: p1(Pair(2, 1), 4) -> 6
 6: p1(Pair(1, 2), 5)
 
+polymorphicTuple.smt2
+sat
+(define-fun p1 ((A (Pair Int Int)) (B Int)) Bool (and (and (>= (first A) 1) (<= (second A) 2)) (>= B 42)))
+
 list-synasc-unsat.smt2
 unsat
diff --git a/regression-tests/horn-adt/polymorphicTuple.smt2 b/regression-tests/horn-adt/polymorphicTuple.smt2
new file mode 100644
index 00000000..99ab45f3
--- /dev/null
+++ b/regression-tests/horn-adt/polymorphicTuple.smt2
@@ -0,0 +1,15 @@
+
+(set-logic HORN)
+
+(declare-datatypes ( ( Pair 2 ) ) (
+  (par (S T) ( ( Pair ( first S ) ( second T ) )))))
+
+(declare-fun p1 ((Pair Int Int) Int) Bool)
+
+(assert (p1 (Pair 1 2) 42))
+(assert (forall ((p (Pair Int Int)) (x Int))
+     (=> (p1 p x) (p1 (Pair (+ (first p) 1) (- (second p) 1)) (+ x 1)))))
+(assert (forall ((p (Pair Int Int)) (x Int))
+     (=> (p1 p x) (> x 0))))
+
+(check-sat)
diff --git a/regression-tests/horn-adt/runtests b/regression-tests/horn-adt/runtests
index be8ddb5a..e7bc1633 100755
--- a/regression-tests/horn-adt/runtests
+++ b/regression-tests/horn-adt/runtests
@@ -11,7 +11,8 @@ TESTS="simple-adt-horn.smt2 \
        strings2-unsat.smt2 \
        testers.smt2 \
        tuple.smt2 \
-       tuple2.smt2"
+       tuple2.smt2 \
+       polymorphicTuple.smt2"
 
 for name in $TESTS; do
     echo
diff --git a/src/lazabs/viewer/HornSMTPrinter.scala b/src/lazabs/viewer/HornSMTPrinter.scala
index 605671d5..95832809 100644
--- a/src/lazabs/viewer/HornSMTPrinter.scala
+++ b/src/lazabs/viewer/HornSMTPrinter.scala
@@ -59,7 +59,7 @@ object HornSMTPrinter {
   }
   
   def type2String(t: Type) : String = t match {
-    case AdtType(s) => s.name
+    case AdtType(s) => SMTLineariser.sort2SMTString(s)
     case BooleanType() => "Bool"
     case BVType(n) => "(_ BitVec " + n + ")"
     case ArrayType(index, obj) => "(Array " + type2String(index) + " " + type2String(obj) + ")"