From e5f4e2c0c1dc79f9940ddb4fcdbf04d6cffe98f5 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 22 Jan 2019 15:48:48 -0600
Subject: [PATCH]  Fix tuple and record CVC printing (#2818)

---
 src/printer/cvc/cvc_printer.cpp               | 26 ++++++++++++++++---
 test/regress/CMakeLists.txt                   |  2 ++
 .../regress0/datatypes/tree-get-value.cvc     | 10 +++++++
 .../regress0/printer/tuples_and_records.cvc   | 18 +++++++++++++
 4 files changed, 52 insertions(+), 4 deletions(-)
 create mode 100644 test/regress/regress0/datatypes/tree-get-value.cvc
 create mode 100644 test/regress/regress0/printer/tuples_and_records.cvc

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index e6ff02f10..36d2ddfb7 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -407,12 +407,30 @@ void CvcPrinter::toStream(
     case kind::APPLY_SELECTOR_TOTAL: {
         TypeNode t = n[0].getType();
         Node opn = n.getOperator();
-        if( t.isTuple() ){
+        if (t.isTuple() || t.isRecord())
+        {
           toStream(out, n[0], depth, types, true);
+          out << '.';
           const Datatype& dt = ((DatatypeType)t.toType()).getDatatype();
-          int sindex = dt[0].getSelectorIndexInternal( opn.toExpr() );
-          Assert( sindex>=0 );
-          out << '.' << sindex;
+          if (t.isTuple())
+          {
+            int sindex;
+            if (n.getKind() == kind::APPLY_SELECTOR)
+            {
+              sindex = Datatype::indexOf(opn.toExpr());
+            }
+            else
+            {
+              sindex = dt[0].getSelectorIndexInternal(opn.toExpr());
+            }
+            Assert(sindex >= 0);
+            out << sindex;
+          }
+          else
+          {
+            toStream(out, opn, depth, types, false);
+          }
+          return;
         }else{
           toStream(op, opn, depth, types, false);
         }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 77f68aa45..6f147db3c 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -377,6 +377,7 @@ set(regress_0_tests
   regress0/datatypes/some-boolean-tests.cvc
   regress0/datatypes/stream-singleton.smt2
   regress0/datatypes/tenum-bug.smt2
+  regress0/datatypes/tree-get-value.cvc
   regress0/datatypes/tuple-model.cvc
   regress0/datatypes/tuple-no-clash.cvc
   regress0/datatypes/tuple-record-bug.cvc
@@ -573,6 +574,7 @@ set(regress_0_tests
   regress0/print_lambda.cvc
   regress0/printer/bv_consts_bin.smt2
   regress0/printer/bv_consts_dec.smt2
+  regress0/printer/tuples_and_records.cvc
   regress0/push-pop/boolean/fuzz_12.smt2
   regress0/push-pop/boolean/fuzz_13.smt2
   regress0/push-pop/boolean/fuzz_14.smt2
diff --git a/test/regress/regress0/datatypes/tree-get-value.cvc b/test/regress/regress0/datatypes/tree-get-value.cvc
new file mode 100644
index 000000000..0a7da7f69
--- /dev/null
+++ b/test/regress/regress0/datatypes/tree-get-value.cvc
@@ -0,0 +1,10 @@
+% EXPECT: sat
+% EXPECT: ((left(x), leaf))
+OPTION "produce-models";
+DATATYPE
+  tree = node(left : tree, right : tree) | leaf
+END;
+x : tree;
+ASSERT is_leaf(left(x));
+CHECKSAT;
+GET_VALUE left(x);
diff --git a/test/regress/regress0/printer/tuples_and_records.cvc b/test/regress/regress0/printer/tuples_and_records.cvc
new file mode 100644
index 000000000..267a316e8
--- /dev/null
+++ b/test/regress/regress0/printer/tuples_and_records.cvc
@@ -0,0 +1,18 @@
+% EXPECT: invalid
+% EXPECT: ((r.a, "active"))
+% EXPECT: ((y.1, 9))
+OPTION "produce-models";
+
+R : TYPE = [#
+   a : STRING,
+   b : STRING
+#];
+r : R;
+
+y: [REAL, INT, REAL];
+
+ASSERT r = (# a := "active", b := "who knows?" #);
+ASSERT y = ( 4/5, 9, 11/9 );
+QUERY r.a = "what?";
+GET_VALUE r.a;
+GET_VALUE y.1;
-- 
2.30.2