From 9039185001b789eadd8b20149455fe778a80fb69 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 21 Oct 2011 04:44:14 +0000 Subject: some printing and parser fixes for problems recently uncovered --- src/printer/smt2/smt2_printer.cpp | 150 ++++++++++++++++++++++++++++++++------ 1 file changed, 127 insertions(+), 23 deletions(-) (limited to 'src/printer') 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()) { -- cgit v1.2.3