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"
-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
@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
@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
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 */
${getConst_instantiations}
-#line 659 "${template}"
+#line 676 "${template}"
namespace expr {
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
}
}
+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);
}
}
+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
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.
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
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;
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);
}
}
-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 */
#include "expr/kind.h"
#include "expr/metakind.h"
#include "util/language.h"
+#include "printer/printer.h"
#include <sstream>
using namespace std;
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 {
--- /dev/null
+topdir = ../..
+srcdir = src/printer
+
+include $(topdir)/Makefile.subdir
--- /dev/null
+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
--- /dev/null
+/********************* */
+/*! \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 */
+
--- /dev/null
+/********************* */
+/*! \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 */
+
--- /dev/null
+/********************* */
+/*! \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 */
+
--- /dev/null
+/********************* */
+/*! \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 */
+
--- /dev/null
+/********************* */
+/*! \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 */
+
--- /dev/null
+/********************* */
+/*! \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 */
+
--- /dev/null
+/********************* */
+/*! \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 */
+
--- /dev/null
+/********************* */
+/*! \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 */
+
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 */
+
}
}
- 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) {
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 );
*/
//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.
*/
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 */
}/* CVC4 namespace */
#endif /* __CVC4__INTEGER_H */
-
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 */
}/* CVC4 namespace */
#endif /* __CVC4__INTEGER_H */
-
/** 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
/** 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;
case LANG_CVC4:
out << "LANG_CVC4";
break;
- case LANG_AUTO:
- out << "LANG_AUTO";
- break;
default:
out << "undefined_input_language";
}
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
/** 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) {
out << "LANG_CVC4";
break;
case LANG_AST:
- out << "LANG_AUTO";
+ out << "LANG_AST";
break;
default:
out << "undefined_output_language";
#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;
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) );
+ }
};
projects / cvc5.git / commitdiff