initial support for polymorphic ADTs

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

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)

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

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) + ")"