Finish off SEXPR kind work.

(this commit was certified error- and warning-free by the test-and-commit script.)

6 files changed, 18 insertions, 24 deletions

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 2c5bc0170..b7c7013d2 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -1304,47 +1304,38 @@ Expr ValidityChecker::idExpr(const std::string& name) {
 }
 
 Expr ValidityChecker::listExpr(const std::vector<Expr>& kids) {
-  // list exprs aren't supported by CVC4; make a tuple if two or more
-  CheckArgument(kids.size() > 0, kids);
-  return (kids.size() == 1) ? kids[0] : Expr(d_em->mkExpr(CVC4::kind::TUPLE, vector<CVC4::Expr>(kids.begin(), kids.end())));
+  return d_em->mkExpr(CVC4::kind::SEXPR, vector<CVC4::Expr>(kids.begin(), kids.end()));
 }
 
 Expr ValidityChecker::listExpr(const Expr& e1) {
-  // list exprs aren't supported by CVC4; just return e1
-  return e1;
+  return d_em->mkExpr(CVC4::kind::SEXPR, e1);
 }
 
 Expr ValidityChecker::listExpr(const Expr& e1, const Expr& e2) {
-  // list exprs aren't supported by CVC4; just return a tuple
-  return d_em->mkExpr(CVC4::kind::TUPLE, e1, e2);
+  return d_em->mkExpr(CVC4::kind::SEXPR, e1, e2);
 }
 
 Expr ValidityChecker::listExpr(const Expr& e1, const Expr& e2, const Expr& e3) {
-  // list exprs aren't supported by CVC4; just return a tuple
-  return d_em->mkExpr(CVC4::kind::TUPLE, e1, e2, e3);
+  return d_em->mkExpr(CVC4::kind::SEXPR, e1, e2, e3);
 }
 
 Expr ValidityChecker::listExpr(const std::string& op,
                                const std::vector<Expr>& kids) {
-  // list exprs aren't supported by CVC4; just return a tuple
-  return d_em->mkExpr(CVC4::kind::TUPLE, d_em->mkConst(op), vector<CVC4::Expr>(kids.begin(), kids.end()));
+  return d_em->mkExpr(CVC4::kind::SEXPR, d_em->mkConst(op), vector<CVC4::Expr>(kids.begin(), kids.end()));
 }
 
 Expr ValidityChecker::listExpr(const std::string& op, const Expr& e1) {
-  // list exprs aren't supported by CVC4; just return a tuple
-  return d_em->mkExpr(CVC4::kind::TUPLE, d_em->mkConst(op), e1);
+  return d_em->mkExpr(CVC4::kind::SEXPR, d_em->mkConst(op), e1);
 }
 
 Expr ValidityChecker::listExpr(const std::string& op, const Expr& e1,
                                const Expr& e2) {
-  // list exprs aren't supported by CVC4; just return a tuple
-  return d_em->mkExpr(CVC4::kind::TUPLE, d_em->mkConst(op), e1, e2);
+  return d_em->mkExpr(CVC4::kind::SEXPR, d_em->mkConst(op), e1, e2);
 }
 
 Expr ValidityChecker::listExpr(const std::string& op, const Expr& e1,
                                const Expr& e2, const Expr& e3) {
-  // list exprs aren't supported by CVC4; just return a tuple
-  return d_em->mkExpr(CVC4::kind::TUPLE, d_em->mkConst(op), e1, e2, e3);
+  return d_em->mkExpr(CVC4::kind::SEXPR, d_em->mkConst(op), e1, e2, e3);
 }
 
 void ValidityChecker::printExpr(const Expr& e) {
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 99662cb99..938f28635 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -790,9 +790,9 @@ void GetValueCommand::invoke(SmtEngine* smtEngine) throw() {
       smt::SmtScope scope(smtEngine);
       Node request = Node::fromExpr(options::expandDefinitions() ? smtEngine->expandDefinitions(*i) : *i);
       Node value = Node::fromExpr(smtEngine->getValue(*i));
-      result.push_back(nm->mkNode(kind::TUPLE, request, value));
+      result.push_back(nm->mkNode(kind::SEXPR, request, value));
     }
-    Node n = nm->mkNode(kind::TUPLE, result);
+    Node n = nm->mkNode(kind::SEXPR, result);
     d_result = nm->toExpr(n);
     d_commandStatus = CommandSuccess::instance();
   } catch(exception& e) {
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 2676fd6b2..b681f70d4 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -246,6 +246,9 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
         }
       case kind::FUNCTION_TYPE:
         return TypeNode(); // Not sure if this is right
+      case kind::SEXPR_TYPE:
+        Unimplemented("haven't implemented leastCommonType for symbolic expressions yet");
+        return TypeNode(); // Not sure if this is right
       case kind::TUPLE_TYPE:
         Unimplemented("haven't implemented leastCommonType for tuples yet");
         return TypeNode(); // Not sure if this is right
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index a6693dd22..56d9a20b0 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -198,6 +198,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       return;
       break;
     case kind::TUPLE_TYPE:
+    case kind::SEXPR_TYPE:
       out << '[';
       for (unsigned i = 0; i < n.getNumChildren(); ++ i) {
         if (i > 0) {
@@ -209,6 +210,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       return;
       break;
     case kind::TUPLE:
+    case kind::SEXPR:
       // no-op
       break;
     case kind::LAMBDA:
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 7f973aaee..5d9a13786 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -210,6 +210,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::DISTINCT: out << smtKindString(k) << " "; break;
   case kind::CHAIN: break;
   case kind::TUPLE: break;
+  case kind::SEXPR: break;
 
     // bool theory
   case kind::NOT:
@@ -355,7 +356,9 @@ static string smtKindString(Kind k) throw() {
   case kind::APPLY: break;
   case kind::EQUAL: return "=";
   case kind::DISTINCT: return "distinct";
+  case kind::CHAIN: break;
   case kind::TUPLE: break;
+  case kind::SEXPR: break;
 
     // bool theory
   case kind::NOT: return "not";
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ad72e0737..2db746c0a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1888,11 +1888,6 @@ Expr SmtEngine::getValue(const Expr& e)
       "Cannot get value unless immediately preceded by SAT/INVALID or UNKNOWN response.";
     throw ModalException(msg);
   }
-  if(type.isSort() || type.isSortConstructor()) {
-    const char* msg =
-      "Cannot get value of a sort.";
-    throw ModalException(msg);
-  }
 
   // do not need to apply preprocessing substitutions (should be recorded in model already)