Fix tuple and record CVC printing (#2818)

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index e6ff02f104dc823422bed0da3028af6678a29d2a..36d2ddfb74e50103ae747aa71622ab215fd39cfb 100644 (file)
--- 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 77f68aa456f0574b4ef5f4951294e405c2dffedd..6f147db3c7ca16aeff33c0d69b3381f92234157c 100644 (file)
--- 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 (file)
index 0000000..0a7da7f
--- /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 (file)
index 0000000..267a316
--- /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;