From b06a3d697c1dc57c58498c9e8612d4c21d6395d6 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 26 Sep 2012 22:00:19 +0000 Subject: [PATCH] Finish off SEXPR kind work. (this commit was certified error- and warning-free by the test-and-commit script.) --- src/compat/cvc3_compat.cpp | 25 ++++++++----------------- src/expr/command.cpp | 4 ++-- src/expr/type_node.cpp | 3 +++ src/printer/cvc/cvc_printer.cpp | 2 ++ src/printer/smt2/smt2_printer.cpp | 3 +++ src/smt/smt_engine.cpp | 5 ----- 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& 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(kids.begin(), kids.end()))); + return d_em->mkExpr(CVC4::kind::SEXPR, vector(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& kids) { - // list exprs aren't supported by CVC4; just return a tuple - return d_em->mkExpr(CVC4::kind::TUPLE, d_em->mkConst(op), vector(kids.begin(), kids.end())); + return d_em->mkExpr(CVC4::kind::SEXPR, d_em->mkConst(op), vector(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) -- 2.30.2