From 9039185001b789eadd8b20149455fe778a80fb69 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 21 Oct 2011 04:44:14 +0000 Subject: [PATCH] some printing and parser fixes for problems recently uncovered --- src/parser/smt2/Smt2.g | 8 +- src/printer/smt2/smt2_printer.cpp | 150 +++++++++++++++++++++++++----- test/unit/Makefile.am | 2 +- 3 files changed, 135 insertions(+), 25 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index f9a2cccf2..a1a98ac9b 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -380,6 +380,7 @@ extendedCommand[CVC4::Command*& cmd] symbolicExpr[CVC4::SExpr& sexpr] @declarations { std::vector children; + CVC4::Kind k; } : INTEGER_LITERAL { sexpr = SExpr(AntlrInput::tokenText($INTEGER_LITERAL)); } @@ -389,6 +390,11 @@ symbolicExpr[CVC4::SExpr& sexpr] { sexpr = SExpr(AntlrInput::tokenText($STRING_LITERAL)); } | SYMBOL { sexpr = SExpr(AntlrInput::tokenText($SYMBOL)); } + | builtinOp[k] + { std::stringstream ss; + ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2) << EXPR_MANAGER->mkConst(k); + sexpr = SExpr(ss.str()); + } | KEYWORD { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); } | LPAREN_TOK @@ -893,7 +899,7 @@ LESS_THAN_EQUAL_TOK : '<='; MINUS_TOK : '-'; NOT_TOK : 'not'; OR_TOK : 'or'; -PERCENT_TOK : '%'; +// PERCENT_TOK : '%'; PLUS_TOK : '+'; POUND_TOK : '#'; SELECT_TOK : 'select'; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index e926c350f..6741d5d2d 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -31,6 +31,8 @@ namespace CVC4 { namespace printer { namespace smt2 { +string smtKindString(Kind k); + void printBvParameterizedOp(std::ostream& out, TNode n); void Smt2Printer::toStream(std::ostream& out, TNode n, @@ -95,6 +97,27 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, // for our purposes out << (n.getConst() ? "true" : "false"); break; + case kind::BUILTIN: + out << smtKindString(n.getConst()); + break; + case kind::CONST_INTEGER: { + Integer i = n.getConst(); + if(i < 0) { + out << "(- " << i << ')'; + } else { + out << i; + } + break; + } + case kind::CONST_RATIONAL: { + Rational r = n.getConst(); + if(r < 0) { + out << "(- " << r << ')'; + } else { + out << r; + } + break; + } default: // fall back on whatever operator<< does on underlying type; we // might luck out and be SMT-LIB v2 compliant @@ -105,7 +128,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, } if(n.getKind() == kind::SORT_TYPE) { - std::string name; + string name; if(n.getAttribute(expr::VarNameAttr(), name)) { out << name; return; @@ -115,40 +138,40 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, bool stillNeedToPrintParams = true; // operator out << '('; - switch(n.getKind()) { + switch(Kind k = n.getKind()) { // builtin theory case kind::APPLY: break; - case kind::EQUAL: out << "= "; break; - case kind::DISTINCT: out << "distinct "; break; + case kind::EQUAL: + case kind::DISTINCT: out << smtKindString(k) << " "; break; case kind::TUPLE: break; // bool theory - case kind::NOT: out << "not "; break; - case kind::AND: out << "and "; break; - case kind::IFF: out << "iff "; break; - case kind::IMPLIES: out << "=> "; break; - case kind::OR: out << "or "; break; - case kind::XOR: out << "xor "; break; - case kind::ITE: out << "ite "; break; + case kind::NOT: + case kind::AND: + case kind::IFF: + case kind::IMPLIES: + case kind::OR: + case kind::XOR: + case kind::ITE: out << smtKindString(k) << " "; break; // uf theory case kind::APPLY_UF: break; // arith theory - case kind::PLUS: out << "+ "; break; - case kind::MULT: out << "* "; break; - case kind::MINUS: out << "- "; break; - case kind::UMINUS: out << "- "; break; - case kind::DIVISION: out << "/ "; break; - case kind::LT: out << "< "; break; - case kind::LEQ: out << "<= "; break; - case kind::GT: out << "> "; break; - case kind::GEQ: out << ">= "; break; + case kind::PLUS: + case kind::MULT: + case kind::MINUS: + case kind::UMINUS: + case kind::DIVISION: + case kind::LT: + case kind::LEQ: + case kind::GT: + case kind::GEQ: out << smtKindString(k) << " "; break; // arrays theory - case kind::SELECT: out << "select "; break; - case kind::STORE: out << "store "; break; - case kind::ARRAY_TYPE: out << "Array "; break; + case kind::SELECT: + case kind::STORE: + case kind::ARRAY_TYPE: out << smtKindString(k) << " "; break; // bv theory case kind::BITVECTOR_CONCAT: out << "concat "; break; @@ -226,6 +249,87 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, out << ')'; }/* Smt2Printer::toStream() */ +string smtKindString(Kind k) { + switch(k) { + // builtin theory + case kind::APPLY: break; + case kind::EQUAL: return "="; + case kind::DISTINCT: return "distinct"; + case kind::TUPLE: break; + + // bool theory + case kind::NOT: return "not"; + case kind::AND: return "and"; + case kind::IFF: return "="; + case kind::IMPLIES: return "=>"; + case kind::OR: return "or"; + case kind::XOR: return "xor"; + case kind::ITE: return "ite"; + + // uf theory + case kind::APPLY_UF: break; + + // arith theory + case kind::PLUS: return "+"; + case kind::MULT: return "*"; + case kind::MINUS: return "-"; + case kind::UMINUS: return "-"; + case kind::DIVISION: return "/"; + case kind::LT: return "<"; + case kind::LEQ: return "<="; + case kind::GT: return ">"; + case kind::GEQ: return ">="; + + // arrays theory + case kind::SELECT: return "select"; + case kind::STORE: return "store"; + case kind::ARRAY_TYPE: return "Array"; + + // bv theory + case kind::BITVECTOR_CONCAT: return "concat"; + case kind::BITVECTOR_AND: return "bvand"; + case kind::BITVECTOR_OR: return "bvor"; + case kind::BITVECTOR_XOR: return "bvxor"; + case kind::BITVECTOR_NOT: return "bvnot"; + case kind::BITVECTOR_NAND: return "bvnand"; + case kind::BITVECTOR_NOR: return "bvnor"; + case kind::BITVECTOR_XNOR: return "bvxnor"; + case kind::BITVECTOR_COMP: return "bvcomp"; + case kind::BITVECTOR_MULT: return "bvmul"; + case kind::BITVECTOR_PLUS: return "bvadd"; + case kind::BITVECTOR_SUB: return "bvsub"; + case kind::BITVECTOR_NEG: return "bvneg"; + case kind::BITVECTOR_UDIV: return "bvudiv"; + case kind::BITVECTOR_UREM: return "bvurem"; + case kind::BITVECTOR_SDIV: return "bvsdiv"; + case kind::BITVECTOR_SREM: return "bvsrem"; + case kind::BITVECTOR_SMOD: return "bvsmod"; + case kind::BITVECTOR_SHL: return "bvshl"; + case kind::BITVECTOR_LSHR: return "bvlshr"; + case kind::BITVECTOR_ASHR: return "bvashr"; + case kind::BITVECTOR_ULT: return "bvult"; + case kind::BITVECTOR_ULE: return "bvule"; + case kind::BITVECTOR_UGT: return "bvugt"; + case kind::BITVECTOR_UGE: return "bvuge"; + case kind::BITVECTOR_SLT: return "bvslt"; + case kind::BITVECTOR_SLE: return "bvsle"; + case kind::BITVECTOR_SGT: return "bvsgt"; + case kind::BITVECTOR_SGE: return "bvsge"; + + case kind::BITVECTOR_EXTRACT: return "extract"; + case kind::BITVECTOR_REPEAT: return "repeat"; + case kind::BITVECTOR_ZERO_EXTEND: return "zero_extend"; + case kind::BITVECTOR_SIGN_EXTEND: return "sign_extend"; + case kind::BITVECTOR_ROTATE_LEFT: return "rotate_left"; + case kind::BITVECTOR_ROTATE_RIGHT: return "rotate_right"; + default: + ; /* fall through */ + } + + // no SMT way to print these + return kind::kindToString(k); +} + void printBvParameterizedOp(std::ostream& out, TNode n) { out << "(_ "; switch(n.getKind()) { diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index b8e4c1679..4c97e5067 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -75,7 +75,7 @@ AM_CPPFLAGS = \ $(ANTLR_INCLUDES) \ $(TEST_CPPFLAGS) AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(TEST_CXXFLAGS) -AM_LDFLAGS = $(TEST_LDFLAGS) $(READLINE_LDFLAGS) +AM_LDFLAGS = $(TEST_LDFLAGS) $(READLINE_LIBS) AM_CXXFLAGS_WHITE = -fno-access-control -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST AM_CXXFLAGS_BLACK = -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST -- 2.30.2