diff options
26 files changed, 829 insertions, 157 deletions
diff --git a/config/mkbuilddir b/config/mkbuilddir index 252f17ea5..1ed5eda92 100755 --- a/config/mkbuilddir +++ b/config/mkbuilddir @@ -21,6 +21,11 @@ fi target=$1 build_type=$2 +: {$as_echo:=echo} +: {$RM:=rm -f} +: {$MKDIR_P:=mkdir -p} +: {LN_S:=ln -s} + $as_echo "Setting up builds/$target/$build_type..." $RM config.log config.status confdefs.h builds/Makefile $MKDIR_P "builds/$target/$build_type" diff --git a/src/Makefile.am b/src/Makefile.am index 8224deb8f..48e052eef 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -17,7 +17,7 @@ AM_CPPFLAGS = \ -I@srcdir@/include -I@srcdir@ -I@builddir@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -SUBDIRS = lib expr util context theory prop smt . parser main +SUBDIRS = lib expr util context theory prop smt printer . parser main lib_LTLIBRARIES = libcvc4.la noinst_LTLIBRARIES = libcvc4_noinst.la @@ -35,6 +35,7 @@ libcvc4_la_LIBADD = \ @builddir@/context/libcontext.la \ @builddir@/prop/libprop.la \ @builddir@/prop/minisat/libminisat.la \ + @builddir@/printer/libprinter.la \ @builddir@/smt/libsmt.la \ @builddir@/theory/libtheory.la \ @builddir@/lib/libreplacements.la @@ -44,6 +45,7 @@ libcvc4_noinst_la_LIBADD = \ @builddir@/context/libcontext.la \ @builddir@/prop/libprop.la \ @builddir@/prop/minisat/libminisat.la \ + @builddir@/printer/libprinter.la \ @builddir@/smt/libsmt.la \ @builddir@/theory/libtheory.la \ @builddir@/lib/libreplacements.la diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index be089bca8..2e27b4f66 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -648,15 +648,23 @@ public: ExprSetLanguage(OutputLanguage l) : d_language(l) {} inline void applyLanguage(std::ostream& out) { - out.iword(s_iosIndex) = int(d_language); + // (offset by one to detect whether default has been set yet) + out.iword(s_iosIndex) = int(d_language) + 1; } static inline OutputLanguage getLanguage(std::ostream& out) { - return OutputLanguage(out.iword(s_iosIndex)); + long& l = out.iword(s_iosIndex); + if(l == 0) { + // set the default language on this ostream + // (offset by one to detect whether default has been set yet) + l = s_defaultLanguage + 1; + } + return OutputLanguage(l - 1); } static inline void setLanguage(std::ostream& out, OutputLanguage l) { - out.iword(s_iosIndex) = int(l); + // (offset by one to detect whether default has been set yet) + out.iword(s_iosIndex) = int(l) + 1; } };/* class ExprSetLanguage */ @@ -664,7 +672,7 @@ public: ${getConst_instantiations} -#line 659 "${template}" +#line 676 "${template}" namespace expr { diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index cb9730d34..c4604d40e 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -88,11 +88,6 @@ struct NodeValueCompare { inline static size_t constHash(const ::CVC4::expr::NodeValue* nv); };/* struct NodeValueCompare */ -struct NodeValueConstPrinter { - inline static void toStream(std::ostream& out, - const ::CVC4::expr::NodeValue* nv); -}; - /** * "metakinds" represent the "kinds" of kinds at the meta-level. * "metakind" is an ugly name but it's not used by client code, just @@ -264,6 +259,12 @@ ${metakind_constHashes} } } +struct NodeValueConstPrinter { + inline static void toStream(std::ostream& out, + const ::CVC4::expr::NodeValue* nv); + inline static void toStream(std::ostream& out, TNode n); +}; + inline void NodeValueConstPrinter::toStream(std::ostream& out, const ::CVC4::expr::NodeValue* nv) { Assert(nv->getMetaKind() == kind::metakind::CONSTANT); @@ -275,6 +276,10 @@ ${metakind_constPrinters} } } +inline void NodeValueConstPrinter::toStream(std::ostream& out, TNode n) { + toStream(out, n.d_nv); +} + /** * Cleanup to be performed when a NodeValue zombie is collected, and * it has CONSTANT metakind. This calls the destructor for the underlying diff --git a/src/expr/node.h b/src/expr/node.h index c30e2e856..bd4864fed 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -105,6 +105,12 @@ class NodeValue; class ExprSetDepth; }/* CVC4::expr namespace */ +namespace kind { + namespace metakind { + struct NodeValueConstPrinter; + }/* CVC4::kind::metakind namespace */ +}/* CVC4::kind namespace */ + /** * Encapsulation of an NodeValue pointer. The reference count is * maintained in the NodeValue if ref_count is true. @@ -149,6 +155,8 @@ class NodeTemplate { friend class ::CVC4::expr::attr::AttributeManager; + friend struct ::CVC4::kind::metakind::NodeValueConstPrinter; + /** * Assigns the expression value and does reference counting. No assumptions * are made on the expression, and should only be used if we know what we diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index ce0928209..cc8c780a8 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -178,9 +178,6 @@ namespace CVC4 { namespace CVC4 { -template <unsigned nchild_thresh> -inline std::ostream& operator<<(std::ostream&, const NodeBuilder<nchild_thresh>&); - /* see expr/convenience_node_builders.h */ class AndNodeBuilder; class OrNodeBuilder; @@ -692,13 +689,6 @@ public: operator Node(); operator Node() const; - inline void toStream(std::ostream& out, int depth = -1, bool types = false, - OutputLanguage language = language::output::LANG_AST) const { - Assert(!isUsed(), "NodeBuilder is one-shot only; " - "attempt to access it after conversion"); - d_nv->toStream(out, depth, types, language); - } - NodeBuilder<nchild_thresh>& operator&=(TNode); NodeBuilder<nchild_thresh>& operator|=(TNode); NodeBuilder<nchild_thresh>& operator+=(TNode); @@ -1250,15 +1240,6 @@ void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) { } } -template <unsigned nchild_thresh> -inline std::ostream& operator<<(std::ostream& out, - const NodeBuilder<nchild_thresh>& b) { - b.toStream(out, - Node::setdepth::getDepth(out), - Node::printtypes::getPrintTypes(out)); - return out; -} - }/* CVC4 namespace */ #endif /* __CVC4__NODE_BUILDER_H */ diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index a5fff2095..666462875 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -25,6 +25,7 @@ #include "expr/kind.h" #include "expr/metakind.h" #include "util/language.h" +#include "printer/printer.h" #include <sstream> using namespace std; @@ -44,67 +45,7 @@ string NodeValue::toString() const { void NodeValue::toStream(std::ostream& out, int toDepth, bool types, OutputLanguage language) const { - using namespace CVC4; - using namespace CVC4::kind; - using namespace CVC4::language::output; - - switch(language) { - case LANG_CVC4: - // FIXME support cvc output language - case LANG_SMTLIB: - // FIXME support smt-lib output language - case LANG_SMTLIB_V2: - // FIXME support smt-lib v2 output language - case LANG_AST: - if(getKind() == kind::NULL_EXPR) { - out << "null"; - } else if(getMetaKind() == kind::metakind::VARIABLE) { - if(getKind() != kind::VARIABLE && - getKind() != kind::SORT_TYPE) { - out << getKind() << ':'; - } - - string s; - NodeManager* nm = NodeManager::currentNM(); - - // conceptually "this" is const, and hasAttribute() doesn't change - // its argument, but it requires a non-const key arg (for now) - if(nm->getAttribute(const_cast<NodeValue*>(this), - VarNameAttr(), s)) { - out << s; - } else { - out << "var_" << d_id; - } - if(types) { - // print the whole type, but not *its* type - out << ":"; - nm->getType(TNode(this)).toStream(out, -1, false, language); - } - } else { - out << '(' << Kind(d_kind); - if(getMetaKind() == kind::metakind::CONSTANT) { - out << ' '; - kind::metakind::NodeValueConstPrinter::toStream(out, this); - } else { - for(const_nv_iterator i = nv_begin(); i != nv_end(); ++i) { - if(i != nv_end()) { - out << ' '; - } - if(toDepth != 0) { - (*i)->toStream(out, toDepth < 0 ? toDepth : toDepth - 1, - types, language); - } else { - out << "(...)"; - } - } - } - out << ')'; - } - break; - - default: - out << "[output language " << language << " unsupported]"; - }// end switch(language) + Printer::getPrinter(language)->toStream(out, TNode(this), toDepth, types); } void NodeValue::printAst(std::ostream& out, int ind) const { diff --git a/src/printer/Makefile b/src/printer/Makefile new file mode 100644 index 000000000..72baefbd9 --- /dev/null +++ b/src/printer/Makefile @@ -0,0 +1,4 @@ +topdir = ../.. +srcdir = src/printer + +include $(topdir)/Makefile.subdir diff --git a/src/printer/Makefile.am b/src/printer/Makefile.am new file mode 100644 index 000000000..8fd50d823 --- /dev/null +++ b/src/printer/Makefile.am @@ -0,0 +1,21 @@ +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) + +noinst_LTLIBRARIES = libprinter.la + +libprinter_la_SOURCES = \ + printer.h \ + printer.cpp \ + ast/ast_printer.h \ + ast/ast_printer.cpp \ + smt/smt_printer.h \ + smt/smt_printer.cpp \ + smt2/smt2_printer.h \ + smt2/smt2_printer.cpp \ + cvc/cvc_printer.h \ + cvc/cvc_printer.cpp + +libprinter_la_LIBADD = \ + @builddir@/../lib/libreplacements.la diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp new file mode 100644 index 000000000..cd9b0cad5 --- /dev/null +++ b/src/printer/ast/ast_printer.cpp @@ -0,0 +1,100 @@ +/********************* */ +/*! \file ast_printer.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief The pretty-printer interface for the AST output language + ** + ** The pretty-printer interface for the AST output language. + **/ + +#include "printer/ast/ast_printer.h" +#include "util/language.h" // for LANG_AST +#include "expr/node_manager.h" // for VarNameAttr + +#include <iostream> + +using namespace std; + +namespace CVC4 { +namespace printer { +namespace ast { + +std::ostream& AstPrinter::toStream(std::ostream& out, TNode n, + int toDepth, bool types) const { + // null + if(n.getKind() == kind::NULL_EXPR) { + out << "null"; + return out; + } + + // variable + if(n.getMetaKind() == kind::metakind::VARIABLE) { + if(n.getKind() != kind::VARIABLE && + n.getKind() != kind::SORT_TYPE) { + out << n.getKind() << ':'; + } + + string s; + if(n.getAttribute(expr::VarNameAttr(), s)) { + out << s; + } else { + out << "var_" << n.getId(); + } + if(types) { + // print the whole type, but not *its* type + out << ":"; + n.getType().toStream(out, -1, false, language::output::LANG_AST); + } + + return out; + } + + out << '(' << n.getKind(); + if(n.getMetaKind() == kind::metakind::CONSTANT) { + // constant + out << ' '; + kind::metakind::NodeValueConstPrinter::toStream(out, n); + } else { + // operator + if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { + out << ' '; + if(toDepth != 0) { + n.getOperator().toStream(out, toDepth < 0 ? toDepth : toDepth - 1, + types, language::output::LANG_AST); + } else { + out << "(...)"; + } + } + for(TNode::iterator i = n.begin(), + iend = n.end(); + i != iend; + ++i) { + if(i != iend) { + out << ' '; + } + if(toDepth != 0) { + (*i).toStream(out, toDepth < 0 ? toDepth : toDepth - 1, + types, language::output::LANG_AST); + } else { + out << "(...)"; + } + } + } + out << ')'; + + return out; +}/* AstPrinter::toStream() */ + +}/* CVC4::printer::ast namespace */ +}/* CVC4::printer namespace */ +}/* CVC4 namespace */ + diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h new file mode 100644 index 000000000..0851aef6c --- /dev/null +++ b/src/printer/ast/ast_printer.h @@ -0,0 +1,42 @@ +/********************* */ +/*! \file ast_printer.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief The pretty-printer interface for the AST output language + ** + ** The pretty-printer interface for the AST output language. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PRINTER__AST_PRINTER_H +#define __CVC4__PRINTER__AST_PRINTER_H + +#include <iostream> + +#include "printer/printer.h" + +namespace CVC4 { +namespace printer { +namespace ast { + +class AstPrinter : public CVC4::Printer { +public: + std::ostream& toStream(std::ostream& out, TNode n, int toDepth, bool types) const; +};/* class AstPrinter */ + +}/* CVC4::printer::ast namespace */ +}/* CVC4::printer namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PRINTER__AST_PRINTER_H */ + diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp new file mode 100644 index 000000000..aebaf7ae5 --- /dev/null +++ b/src/printer/cvc/cvc_printer.cpp @@ -0,0 +1,37 @@ +/********************* */ +/*! \file cvc_printer.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief The pretty-printer interface for the CVC output language + ** + ** The pretty-printer interface for the CVC output language. + **/ + +#include "printer/cvc/cvc_printer.h" + +#include <iostream> + +using namespace std; + +namespace CVC4 { +namespace printer { +namespace cvc { + +std::ostream& CvcPrinter::toStream(std::ostream& out, TNode n, + int toDepth, bool types) const { + return out; +}/* CvcPrinter::toStream() */ + +}/* CVC4::printer::cvc namespace */ +}/* CVC4::printer namespace */ +}/* CVC4 namespace */ + diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h new file mode 100644 index 000000000..53889a989 --- /dev/null +++ b/src/printer/cvc/cvc_printer.h @@ -0,0 +1,42 @@ +/********************* */ +/*! \file cvc_printer.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief The pretty-printer interface for the CVC output language + ** + ** The pretty-printer interface for the CVC output language. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PRINTER__CVC_PRINTER_H +#define __CVC4__PRINTER__CVC_PRINTER_H + +#include <iostream> + +#include "printer/printer.h" + +namespace CVC4 { +namespace printer { +namespace cvc { + +class CvcPrinter : public CVC4::Printer { +public: + std::ostream& toStream(std::ostream& out, TNode n, int toDepth, bool types) const; +};/* class CvcPrinter */ + +}/* CVC4::printer::cvc namespace */ +}/* CVC4::printer namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PRINTER__CVC_PRINTER_H */ + diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp new file mode 100644 index 000000000..a2a9b3378 --- /dev/null +++ b/src/printer/printer.cpp @@ -0,0 +1,50 @@ +/********************* */ +/*! \file printer.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Base of the pretty-printer interface + ** + ** Base of the pretty-printer interface. + **/ + +#include "printer/printer.h" + +#include "util/language.h" + +#include "printer/smt/smt_printer.h" +#include "printer/smt2/smt2_printer.h" +#include "printer/cvc/cvc_printer.h" +#include "printer/ast/ast_printer.h" + +namespace CVC4 { + +Printer* Printer::d_printers[language::output::LANG_MAX]; + +Printer* Printer::makePrinter(OutputLanguage lang) { + using namespace CVC4::language::output; + + switch(lang) { + case LANG_SMTLIB: + //return new printer::smt::SmtPrinter; + case LANG_SMTLIB_V2: + return new printer::smt2::Smt2Printer; + case LANG_CVC4: + //return new printer::cvc::CvcPrinter; + case LANG_AST: + return new printer::ast::AstPrinter; + default: + Unhandled(lang); + } +}/* Printer::makePrinter() */ + +}/* CVC4 namespace */ + diff --git a/src/printer/printer.h b/src/printer/printer.h new file mode 100644 index 000000000..2532725ae --- /dev/null +++ b/src/printer/printer.h @@ -0,0 +1,53 @@ +/********************* */ +/*! \file printer.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Base of the pretty-printer interface + ** + ** Base of the pretty-printer interface. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PRINTER__PRINTER_H +#define __CVC4__PRINTER__PRINTER_H + +#include "util/language.h" +#include "expr/node.h" + +namespace CVC4 { + +class Printer { + /** Printers for each OutputLanguage */ + static Printer* d_printers[language::output::LANG_MAX]; + + /** Make a Printer for a given OutputLanguage */ + static Printer* makePrinter(OutputLanguage lang); + +public: + /** Get the Printer for a given OutputLanguage */ + static Printer* getPrinter(OutputLanguage lang) { + if(d_printers[lang] == NULL) { + d_printers[lang] = makePrinter(lang); + } + return d_printers[lang]; + } + + /** Write a Node out to a stream with this Printer. */ + virtual std::ostream& toStream(std::ostream& out, TNode n, + int toDepth, bool types) const = 0; +};/* class Printer */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__PRINTER__PRINTER_H */ + diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp new file mode 100644 index 000000000..6040c133b --- /dev/null +++ b/src/printer/smt/smt_printer.cpp @@ -0,0 +1,37 @@ +/********************* */ +/*! \file smt_printer.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief The pretty-printer interface for the SMT output language + ** + ** The pretty-printer interface for the SMT output language. + **/ + +#include "printer/smt/smt_printer.h" + +#include <iostream> + +using namespace std; + +namespace CVC4 { +namespace printer { +namespace smt { + +std::ostream& SmtPrinter::toStream(std::ostream& out, TNode n, + int toDepth, bool types) const { + return out; +}/* SmtPrinter::toStream() */ + +}/* CVC4::printer::smt namespace */ +}/* CVC4::printer namespace */ +}/* CVC4 namespace */ + diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt/smt_printer.h new file mode 100644 index 000000000..e503ca8f0 --- /dev/null +++ b/src/printer/smt/smt_printer.h @@ -0,0 +1,42 @@ +/********************* */ +/*! \file smt_printer.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief The pretty-printer interface for the SMT output language + ** + ** The pretty-printer interface for the SMT output language. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PRINTER__SMT_PRINTER_H +#define __CVC4__PRINTER__SMT_PRINTER_H + +#include <iostream> + +#include "printer/printer.h" + +namespace CVC4 { +namespace printer { +namespace smt { + +class SmtPrinter : public CVC4::Printer { +public: + std::ostream& toStream(std::ostream& out, TNode n, int toDepth, bool types) const; +};/* class SmtPrinter */ + +}/* CVC4::printer::smt namespace */ +}/* CVC4::printer namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PRINTER__SMT_PRINTER_H */ + diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp new file mode 100644 index 000000000..c8c4bfc20 --- /dev/null +++ b/src/printer/smt2/smt2_printer.cpp @@ -0,0 +1,234 @@ +/********************* */ +/*! \file smt2_printer.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief The pretty-printer interface for the SMT2 output language + ** + ** The pretty-printer interface for the SMT2 output language. + **/ + +#include "printer/smt2/smt2_printer.h" + +#include <iostream> + +using namespace std; + +namespace CVC4 { +namespace printer { +namespace smt2 { + +void printBvParameterizedOp(std::ostream& out, TNode n); + +std::ostream& Smt2Printer::toStream(std::ostream& out, TNode n, + int toDepth, bool types) const { + // null + if(n.getKind() == kind::NULL_EXPR) { + out << "null"; + return out; + } + + // variable + if(n.getMetaKind() == kind::metakind::VARIABLE) { + string s; + if(n.getAttribute(expr::VarNameAttr(), s)) { + out << s; + } else { + if(n.getKind() == kind::VARIABLE) { + out << "var_"; + } else { + out << n.getKind() << '_'; + } + out << n.getId(); + } + if(types) { + // print the whole type, but not *its* type + out << ":"; + n.getType().toStream(out, -1, false, language::output::LANG_SMTLIB_V2); + } + + return out; + } + + // constant + if(n.getMetaKind() == kind::metakind::CONSTANT) { + switch(n.getKind()) { + case kind::BITVECTOR_TYPE: + out << "(_ BitVec " << n.getConst<BitVectorSize>().size << ")"; + break; + case kind::CONST_BITVECTOR: { + const BitVector& bv = n.getConst<BitVector>(); + const Integer& x = bv.getValue(); + out << "#b"; + unsigned n = bv.getSize(); + while(n-- > 0) { + out << (x.testBit(n) ? '1' : '0'); + } + break; + } + default: + // fall back on whatever operator<< does on underlying type; we + // might luck out and be SMT-LIB v2 compliant + kind::metakind::NodeValueConstPrinter::toStream(out, n); + } + + return out; + } + + bool stillNeedToPrintParams = true; + // operator + out << '('; + switch(n.getKind()) { + // builtin theory + case kind::EQUAL: out << "= "; break; + case kind::DISTINCT: out << "distinct "; 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 << "implies "; break; + case kind::OR: out << "or "; break; + case kind::XOR: out << "xor "; break; + case kind::ITE: out << "ite "; break; + + // uf theory + case kind::APPLY_UF: break; + case kind::SORT_TYPE: 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; + + // arrays theory + case kind::SELECT: out << "select "; break; + case kind::STORE: out << "store "; break; + + // bv theory + case kind::BITVECTOR_CONCAT: out << "concat "; break; + case kind::BITVECTOR_AND: out << "bvand "; break; + case kind::BITVECTOR_OR: out << "bvor "; break; + case kind::BITVECTOR_XOR: out << "bvxor "; break; + case kind::BITVECTOR_NOT: out << "bvnot "; break; + case kind::BITVECTOR_NAND: out << "bvnand "; break; + case kind::BITVECTOR_NOR: out << "bvnor "; break; + case kind::BITVECTOR_XNOR: out << "bvxnor "; break; + case kind::BITVECTOR_COMP: out << "bvcomp "; break; + case kind::BITVECTOR_MULT: out << "bvmul "; break; + case kind::BITVECTOR_PLUS: out << "bvadd "; break; + case kind::BITVECTOR_SUB: out << "bvsub "; break; + case kind::BITVECTOR_NEG: out << "bvneg "; break; + case kind::BITVECTOR_UDIV: out << "bvudiv "; break; + case kind::BITVECTOR_UREM: out << "bvurem "; break; + case kind::BITVECTOR_SDIV: out << "bvsdiv "; break; + case kind::BITVECTOR_SREM: out << "bvsrem "; break; + case kind::BITVECTOR_SMOD: out << "bvsmod "; break; + case kind::BITVECTOR_SHL: out << "bvshl "; break; + case kind::BITVECTOR_LSHR: out << "bvlshr "; break; + case kind::BITVECTOR_ASHR: out << "bvashr "; break; + case kind::BITVECTOR_ULT: out << "bvult "; break; + case kind::BITVECTOR_ULE: out << "bvule "; break; + case kind::BITVECTOR_UGT: out << "bvugt "; break; + case kind::BITVECTOR_UGE: out << "bvuge "; break; + case kind::BITVECTOR_SLT: out << "bvslt "; break; + case kind::BITVECTOR_SLE: out << "bvsle "; break; + case kind::BITVECTOR_SGT: out << "bvsgt "; break; + case kind::BITVECTOR_SGE: out << "bvsge "; break; + + case kind::BITVECTOR_EXTRACT: + case kind::BITVECTOR_REPEAT: + case kind::BITVECTOR_ZERO_EXTEND: + case kind::BITVECTOR_SIGN_EXTEND: + case kind::BITVECTOR_ROTATE_LEFT: + case kind::BITVECTOR_ROTATE_RIGHT: + printBvParameterizedOp(out, n); + out << ' '; + stillNeedToPrintParams = false; + break; + + default: + // fall back on however the kind prints itself; this probably + // won't be SMT-LIB v2 compliant, but it will be clear from the + // output that support for the kind needs to be added here. + out << n.getKind() << ' '; + } + if(n.getMetaKind() == kind::metakind::PARAMETERIZED && + stillNeedToPrintParams) { + if(toDepth != 0) { + n.getOperator().toStream(out, toDepth < 0 ? toDepth : toDepth - 1, + types, language::output::LANG_SMTLIB_V2); + } else { + out << "(...)"; + } + } + for(TNode::iterator i = n.begin(), + iend = n.end(); + i != iend; ) { + if(toDepth != 0) { + (*i).toStream(out, toDepth < 0 ? toDepth : toDepth - 1, + types, language::output::LANG_SMTLIB_V2); + } else { + out << "(...)"; + } + if(++i != iend) { + out << ' '; + } + } + out << ')'; + + return out; +}/* Smt2Printer::toStream() */ + +void printBvParameterizedOp(std::ostream& out, TNode n) { + out << "(_ "; + switch(n.getKind()) { + case kind::BITVECTOR_EXTRACT: { + BitVectorExtract p = n.getOperator().getConst<BitVectorExtract>(); + out << "extract " << p.high << " " << p.low; + break; + } + case kind::BITVECTOR_REPEAT: + out << "repeat " + << n.getOperator().getConst<BitVectorRepeat>().repeatAmount; + break; + case kind::BITVECTOR_ZERO_EXTEND: + out << "zero_extend " + << n.getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount; + break; + case kind::BITVECTOR_SIGN_EXTEND: + out << "sign_extend " + << n.getOperator().getConst<BitVectorSignExtend>().signExtendAmount; + break; + case kind::BITVECTOR_ROTATE_LEFT: + out << "rotate_left " + << n.getOperator().getConst<BitVectorRotateLeft>().rotateLeftAmount; + break; + case kind::BITVECTOR_ROTATE_RIGHT: + out << "rotate_right " + << n.getOperator().getConst<BitVectorRotateRight>().rotateRightAmount; + break; + default: + Unhandled(n.getKind()); + } + out << ")"; +} + +}/* CVC4::printer::smt2 namespace */ +}/* CVC4::printer namespace */ +}/* CVC4 namespace */ diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h new file mode 100644 index 000000000..7cd88f0ff --- /dev/null +++ b/src/printer/smt2/smt2_printer.h @@ -0,0 +1,42 @@ +/********************* */ +/*! \file smt2_printer.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief The pretty-printer interface for the SMT2 output language + ** + ** The pretty-printer interface for the SMT2 output language. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PRINTER__SMT2_PRINTER_H +#define __CVC4__PRINTER__SMT2_PRINTER_H + +#include <iostream> + +#include "printer/printer.h" + +namespace CVC4 { +namespace printer { +namespace smt2 { + +class Smt2Printer : public CVC4::Printer { +public: + std::ostream& toStream(std::ostream& out, TNode n, int toDepth, bool types) const; +};/* class Smt2Printer */ + +}/* CVC4::printer::smt2 namespace */ +}/* CVC4::printer namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PRINTER__SMT2_PRINTER_H */ + diff --git a/src/theory/bv/theory_bv_rewrite_rules.cpp b/src/theory/bv/theory_bv_rewrite_rules.cpp index 637a4269d..d2fb621f9 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.cpp +++ b/src/theory/bv/theory_bv_rewrite_rules.cpp @@ -51,9 +51,10 @@ Node CoreRewriteRules::ConcatFlatten::apply(Node node) { } } - Debug("bitvector") << "ConcatFlatten(" << node << ") => " << result << endl; + Node resultNode = result; + Debug("bitvector") << "ConcatFlatten(" << node << ") => " << resultNode << endl; - return result; + return resultNode; } bool CoreRewriteRules::ConcatExtractMerge::applies(Node node) { diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 51239cbbb..d1bfafb00 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -122,7 +122,11 @@ public: unsigned getSize() const { return d_size; } -}; + + const Integer& getValue() const { + return d_value; + } +};/* class BitVector */ inline BitVector::BitVector(const std::string& num, unsigned base) { AlwaysAssert( base == 2 || base == 16 ); diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 21f6c7581..d13c946de 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -50,7 +50,7 @@ private: */ //const mpz_class& get_mpz() const { return d_value; } const cln::cl_I& get_cl_I() const { return d_value; } - + /** * Constructs an Integer by copying a GMP C++ primitive. */ @@ -219,6 +219,16 @@ public: return equal_hashcode(d_value); } + /** + * Returns true iff bit n is set. + * + * @param n the bit to test (0 == least significant bit) + * @return true if bit n is set in this integer; false otherwise + */ + bool testBit(unsigned n) const { + return cln::logbitp(n, d_value); + } + friend class CVC4::Rational; };/* class Integer */ @@ -235,4 +245,3 @@ inline std::ostream& operator<<(std::ostream& os, const Integer& n) { }/* CVC4 namespace */ #endif /* __CVC4__INTEGER_H */ - diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 72a653545..13bed50b3 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -155,6 +155,16 @@ public: return gmpz_hash(d_value.get_mpz_t()); } + /** + * Returns true iff bit n is set. + * + * @param n the bit to test (0 == least significant bit) + * @return true if bit n is set in this integer; false otherwise + */ + bool testBit(unsigned n) const { + return mpz_tstbit(d_value.get_mpz_t(), n); + } + friend class CVC4::Rational; };/* class Integer */ @@ -171,4 +181,3 @@ inline std::ostream& operator<<(std::ostream& os, const Integer& n) { }/* CVC4 namespace */ #endif /* __CVC4__INTEGER_H */ - diff --git a/src/util/language.h b/src/util/language.h index 5446357c4..fdd2a382d 100644 --- a/src/util/language.h +++ b/src/util/language.h @@ -37,7 +37,7 @@ enum Language { /** Auto-detect the language */ LANG_AUTO = -1, - // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,999] + // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9] // AND SHOULD CORRESPOND IN PLACEMENT WITH OUTPUTLANGUAGE // // EVEN IF A LANGUAGE ISN'T CURRENTLY SUPPORTED AS AN INPUT OR @@ -49,15 +49,20 @@ enum Language { /** The SMTLIB v2 input language */ LANG_SMTLIB_V2, /** The CVC4 input language */ - LANG_CVC4 + LANG_CVC4, - // START INPUT-ONLY LANGUAGES AT ENUM VALUE 1000 + // START INPUT-ONLY LANGUAGES AT ENUM VALUE 10 // THESE ARE IN PRINCIPLE NOT POSSIBLE OUTPUT LANGUAGES + /** LANG_MAX is > any valid InputLanguage id */ + LANG_MAX };/* enum Language */ inline std::ostream& operator<<(std::ostream& out, Language lang) { switch(lang) { + case LANG_AUTO: + out << "LANG_AUTO"; + break; case LANG_SMTLIB: out << "LANG_SMTLIB"; break; @@ -67,9 +72,6 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { case LANG_CVC4: out << "LANG_CVC4"; break; - case LANG_AUTO: - out << "LANG_AUTO"; - break; default: out << "undefined_input_language"; } @@ -83,7 +85,7 @@ namespace output { enum Language { // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0 - // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,999] + // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9] // AND SHOULD CORRESPOND IN PLACEMENT WITH INPUTLANGUAGE // // EVEN IF A LANGUAGE ISN'T CURRENTLY SUPPORTED AS AN INPUT OR @@ -97,12 +99,14 @@ enum Language { /** The CVC4 output language */ LANG_CVC4 = input::LANG_CVC4, - // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 1000 + // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10 // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES /** The AST output language */ - LANG_AST = 1000 + LANG_AST = 10, + /** LANG_MAX is > any valid OutputLanguage id */ + LANG_MAX };/* enum Language */ inline std::ostream& operator<<(std::ostream& out, Language lang) { @@ -117,7 +121,7 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { out << "LANG_CVC4"; break; case LANG_AST: - out << "LANG_AUTO"; + out << "LANG_AST"; break; default: out << "undefined_output_language"; diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 46fb82546..49c9b7952 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -570,57 +570,6 @@ public: #endif /* CVC4_ASSERTIONS */ } - void testToStream() { - /* inline void toStream(std::ostream& out) const { - d_ev->toStream(out); - } - */ - - NodeBuilder<K> a(specKind); - NodeBuilder<K> b(specKind); - NodeBuilder<K> c(NOT); - string astr, bstr, cstr; - stringstream astream, bstream, cstream; - - push_back(a, K / 2); - push_back(b, K / 2); - push_back(c, 1); - - a.toStream(astream); - b.toStream(bstream); - c.toStream(cstream); - - astr = astream.str(); - bstr = bstream.str(); - cstr = cstream.str(); - - TS_ASSERT_EQUALS(astr, bstr); - TS_ASSERT_DIFFERS(astr, cstr); - - Node n = a; n = b; n = c;// avoid warning on clear() - a.clear(specKind); - b.clear(specKind); - c.clear(specKind); - astream.flush(); - bstream.flush(); - cstream.flush(); - - push_back(a,2*K); - push_back(b,2*K); - push_back(c,2*K+1); - - a.toStream(astream); - b.toStream(bstream); - c.toStream(cstream); - - astr = astream.str(); - bstr = bstream.str(); - cstr = cstream.str(); - - TS_ASSERT_EQUALS(astr, bstr); - TS_ASSERT_DIFFERS(astr, cstr); - } - void testLeftistBuilding() { NodeBuilder<> nb; diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h index 57ae247ac..f4bd1f8b8 100644 --- a/test/unit/util/integer_black.h +++ b/test/unit/util/integer_black.h @@ -294,4 +294,46 @@ public: TS_ASSERT_EQUALS( Integer(1000), Integer(10).pow(3) ); TS_ASSERT_EQUALS( Integer(-1000), Integer(-10).pow(3) ); } + + void testTestBit() { + TS_ASSERT( ! Integer(0).testBit(6) ); + TS_ASSERT( ! Integer(0).testBit(5) ); + TS_ASSERT( ! Integer(0).testBit(4) ); + TS_ASSERT( ! Integer(0).testBit(3) ); + TS_ASSERT( ! Integer(0).testBit(2) ); + TS_ASSERT( ! Integer(0).testBit(1) ); + TS_ASSERT( ! Integer(0).testBit(0) ); + + TS_ASSERT( Integer(-1).testBit(6) ); + TS_ASSERT( Integer(-1).testBit(5) ); + TS_ASSERT( Integer(-1).testBit(4) ); + TS_ASSERT( Integer(-1).testBit(3) ); + TS_ASSERT( Integer(-1).testBit(2) ); + TS_ASSERT( Integer(-1).testBit(1) ); + TS_ASSERT( Integer(-1).testBit(0) ); + + TS_ASSERT( ! Integer(10).testBit(6) ); + TS_ASSERT( ! Integer(10).testBit(5) ); + TS_ASSERT( ! Integer(10).testBit(4) ); + TS_ASSERT( Integer(10).testBit(3) ); + TS_ASSERT( ! Integer(10).testBit(2) ); + TS_ASSERT( Integer(10).testBit(1) ); + TS_ASSERT( ! Integer(10).testBit(0) ); + + TS_ASSERT( ! Integer(14).testBit(6) ); + TS_ASSERT( ! Integer(14).testBit(5) ); + TS_ASSERT( ! Integer(14).testBit(4) ); + TS_ASSERT( Integer(14).testBit(3) ); + TS_ASSERT( Integer(14).testBit(2) ); + TS_ASSERT( Integer(14).testBit(1) ); + TS_ASSERT( ! Integer(14).testBit(0) ); + + TS_ASSERT( Integer(64).testBit(6) ); + TS_ASSERT( ! Integer(64).testBit(5) ); + TS_ASSERT( ! Integer(64).testBit(4) ); + TS_ASSERT( ! Integer(64).testBit(3) ); + TS_ASSERT( ! Integer(64).testBit(2) ); + TS_ASSERT( ! Integer(64).testBit(1) ); + TS_ASSERT( ! Integer(64).testBit(0) ); + } }; |