This removes infrastructure for stream property related to printing type annotations on all variables.
This is towards refactoring the printers.
namespace expr {
const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc();
-const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc();
const int ExprDag::s_iosIndex = std::ios_base::xalloc();
-
-
ExprSetDepth::ExprSetDepth(long depth) : d_depth(depth) {}
void ExprSetDepth::applyDepth(std::ostream& out) {
ExprSetDepth::setDepth(d_out, d_oldDepth);
}
-
-ExprPrintTypes::ExprPrintTypes(bool printTypes) : d_printTypes(printTypes) {}
-
-void ExprPrintTypes::applyPrintTypes(std::ostream& out) {
- out.iword(s_iosIndex) = d_printTypes;
-}
-
-bool ExprPrintTypes::getPrintTypes(std::ostream& out) {
- return out.iword(s_iosIndex);
-}
-
-void ExprPrintTypes::setPrintTypes(std::ostream& out, bool printTypes) {
- out.iword(s_iosIndex) = printTypes;
-}
-
-ExprPrintTypes::Scope::Scope(std::ostream& out, bool printTypes)
- : d_out(out),
- d_oldPrintTypes(ExprPrintTypes::getPrintTypes(out)) {
- ExprPrintTypes::setPrintTypes(out, printTypes);
-}
-
-ExprPrintTypes::Scope::~Scope() {
- ExprPrintTypes::setPrintTypes(d_out, d_oldPrintTypes);
-}
-
ExprDag::ExprDag(bool dag) : d_dag(dag ? 1 : 0) {}
ExprDag::ExprDag(int dag) : d_dag(dag < 0 ? 0 : dag) {}
return out;
}
-std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) {
- pt.applyPrintTypes(out);
- return out;
-}
-
std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) {
sd.applyDepth(out);
return out;
long d_depth;
};/* class ExprSetDepth */
-/**
- * IOStream manipulator to print type ascriptions or not.
- *
- * // let a, b, c, and d be variables of sort U
- * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
- * out << e;
- *
- * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
- */
-class CVC4_PUBLIC ExprPrintTypes {
-public:
- /**
- * Construct a ExprPrintTypes with the given setting.
- */
- ExprPrintTypes(bool printTypes);
-
- void applyPrintTypes(std::ostream& out);
-
- static bool getPrintTypes(std::ostream& out);
-
- static void setPrintTypes(std::ostream& out, bool printTypes);
-
- /**
- * Set the print-types state on the output stream for the current
- * stack scope. This makes sure the old state is reset on the
- * stream after normal OR exceptional exit from the scope, using the
- * RAII C++ idiom.
- */
- class Scope {
- public:
- Scope(std::ostream& out, bool printTypes);
- ~Scope();
-
- private:
- std::ostream& d_out;
- bool d_oldPrintTypes;
- };/* class ExprPrintTypes::Scope */
-
- private:
- /**
- * The allocated index in ios_base for our setting.
- */
- static const int s_iosIndex;
-
- /**
- * When this manipulator is used, the setting is stored here.
- */
- bool d_printTypes;
-};/* class ExprPrintTypes */
-
/**
* IOStream manipulator to print expressions as a dag (or not).
*/
*/
std::ostream& operator<<(std::ostream& out, ExprDag d) CVC4_PUBLIC;
-
-/**
- * Sets the default print-types setting when pretty-printing an Expr
- * to an ostream. Use like this:
- *
- * // let out be an ostream, e an Expr
- * out << Expr::printtypes(true) << e << endl;
- *
- * The setting stays permanently (until set again) with the stream.
- */
-std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) CVC4_PUBLIC;
-
/**
* Sets the default depth when pretty-printing a Expr to an ostream.
* Use like this:
return expr::hasFreeVar(*d_node);
}
-void Expr::toStream(std::ostream& out, int depth, bool types, size_t dag,
- OutputLanguage language) const {
+void Expr::toStream(std::ostream& out,
+ int depth,
+ size_t dag,
+ OutputLanguage language) const
+{
ExprManagerScope ems(*this);
- d_node->toStream(out, depth, types, dag, language);
+ d_node->toStream(out, depth, dag, language);
}
Node Expr::getNode() const { return *d_node; }
* @param out the stream to serialize this expression to
* @param toDepth the depth to which to print this expression, or -1
* to print it fully
- * @param types set to true to ascribe types to the output
- * expressions (might break language compliance, but good for
- * debugging expressions)
* @param dag the dagification threshold to use (0 == off)
* @param language the language in which to output
*/
- void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
+ void toStream(std::ostream& out,
+ int toDepth = -1,
+ size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const;
/**
* @param out the stream to serialize this node to
* @param toDepth the depth to which to print this expression, or -1 to
* print it fully
- * @param types set to true to ascribe types to the output expressions
- * (might break language compliance, but good for debugging expressions)
* @param language the language in which to output
*/
inline void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
size_t dagThreshold = 1,
OutputLanguage language = language::output::LANG_AUTO) const
{
assertTNodeNotExpired();
- d_nv->toStream(out, toDepth, types, dagThreshold, language);
+ d_nv->toStream(out, toDepth, dagThreshold, language);
}
/**
*/
typedef expr::ExprSetDepth setdepth;
- /**
- * IOStream manipulator to print type ascriptions or not.
- *
- * // let a, b, c, and d be variables of sort U
- * Node n = nm->mkNode(OR, a, b, nm->mkNode(AND, c, nm->mkNode(NOT, d)))
- * out << n;
- *
- * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
- */
- typedef expr::ExprPrintTypes printtypes;
-
/**
* IOStream manipulator to print expressions as DAGs (or not).
*/
inline std::ostream& operator<<(std::ostream& out, TNode n) {
n.toStream(out,
Node::setdepth::getDepth(out),
- Node::printtypes::getPrintTypes(out),
Node::dag::getDag(out),
Node::setlanguage::getLanguage(out));
return out;
*/
static void __attribute__((used)) debugPrintNode(const NodeTemplate<true>& n) {
Warning() << Node::setdepth(-1)
- << Node::printtypes(false)
<< Node::dag(true)
<< Node::setlanguage(language::output::LANG_AST)
<< n << std::endl;
}
static void __attribute__((used)) debugPrintNodeNoDag(const NodeTemplate<true>& n) {
Warning() << Node::setdepth(-1)
- << Node::printtypes(false)
<< Node::dag(false)
<< Node::setlanguage(language::output::LANG_AST)
<< n << std::endl;
static void __attribute__((used)) debugPrintTNode(const NodeTemplate<false>& n) {
Warning() << Node::setdepth(-1)
- << Node::printtypes(false)
<< Node::dag(true)
<< Node::setlanguage(language::output::LANG_AST)
<< n << std::endl;
}
static void __attribute__((used)) debugPrintTNodeNoDag(const NodeTemplate<false>& n) {
Warning() << Node::setdepth(-1)
- << Node::printtypes(false)
<< Node::dag(false)
<< Node::setlanguage(language::output::LANG_AST)
<< n << std::endl;
OutputLanguage outlang = (this == &null()) ? language::output::LANG_AUTO
: options::outputLanguage();
- toStream(ss, -1, false, false, outlang);
+ toStream(ss, -1, false, outlang);
return ss.str();
}
-void NodeValue::toStream(std::ostream& out, int toDepth, bool types, size_t dag,
- OutputLanguage language) const {
+void NodeValue::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
// Ensure that this node value is live for the length of this call.
// It really breaks things badly if we don't have a nonzero ref
// count, even just for printing.
RefCountGuard guard(this);
- Printer::getPrinter(language)->toStream(out, TNode(this), toDepth, types,
- dag);
+ Printer::getPrinter(language)->toStream(out, TNode(this), toDepth, dag);
}
void NodeValue::printAst(std::ostream& out, int ind) const {
void toStream(std::ostream& out,
int toDepth = -1,
- bool types = false,
size_t dag = 1,
OutputLanguage = language::output::LANG_AUTO) const;
inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) {
nv.toStream(out,
Node::setdepth::getDepth(out),
- Node::printtypes::getPrintTypes(out),
Node::dag::getDag(out),
Node::setlanguage::getLanguage(out));
return out;
*/
static void __attribute__((used)) debugPrintNodeValue(const expr::NodeValue* nv) {
Warning() << Node::setdepth(-1)
- << Node::printtypes(false)
<< Node::dag(true)
<< Node::setlanguage(language::output::LANG_AST)
<< *nv << std::endl;
}
static void __attribute__((used)) debugPrintNodeValueNoDag(const expr::NodeValue* nv) {
Warning() << Node::setdepth(-1)
- << Node::printtypes(false)
<< Node::dag(false)
<< Node::setlanguage(language::output::LANG_AST)
<< *nv << std::endl;
std::string TypeNode::toString() const {
std::stringstream ss;
OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage();
- d_nv->toStream(ss, -1, false, 0, outlang);
+ d_nv->toStream(ss, -1, 0, outlang);
return ss.str();
}
* @param language the language in which to output
*/
inline void toStream(std::ostream& out, OutputLanguage language = language::output::LANG_AUTO) const {
- d_nv->toStream(out, -1, false, 0, language);
+ d_nv->toStream(out, -1, 0, language);
}
/**
*/
static void __attribute__((used)) debugPrintTypeNode(const TypeNode& n) {
Warning() << Node::setdepth(-1)
- << Node::printtypes(false)
<< Node::dag(true)
<< Node::setlanguage(language::output::LANG_AST)
<< n << std::endl;
}
static void __attribute__((used)) debugPrintTypeNodeNoDag(const TypeNode& n) {
Warning() << Node::setdepth(-1)
- << Node::printtypes(false)
<< Node::dag(false)
<< Node::setlanguage(language::output::LANG_AST)
<< n << std::endl;
read_only = true
help = "dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)"
-[[option]]
- name = "printExprTypes"
- category = "regular"
- long = "print-expr-types"
- type = "bool"
- default = "false"
- read_only = true
- help = "print types with variables when printing exprs"
-
[[option]]
name = "typeChecking"
category = "regular"
#include "api/cvc4cpp.h"
#include "base/output.h"
#include "expr/expr.h"
-#include "expr/expr_iomanip.h"
#include "expr/kind.h"
#include "expr/type.h"
#include "options/options.h"
for (size_t j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
{
const api::DatatypeConstructor& ctor = dt[j];
- expr::ExprPrintTypes::Scope pts(Debug("parser-idt"), true);
api::Term constructor = ctor.getConstructorTerm();
Debug("parser-idt") << "+ define " << constructor << std::endl;
string constructorName = ctor.getName();
namespace printer {
namespace ast {
-void AstPrinter::toStream(
- std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const
+void AstPrinter::toStream(std::ostream& out,
+ TNode n,
+ int toDepth,
+ size_t dag) const
{
if(dag != 0) {
DagificationVisitor dv(dag);
} else {
first = false;
}
- toStream(out, (*i).second, toDepth, types, false);
+ toStream(out, (*i).second, toDepth, false);
out << " := ";
- toStream(out, (*i).first, toDepth, types, false);
+ toStream(out, (*i).first, toDepth, false);
}
out << " IN ";
}
Node body = dv.getDagifiedBody();
- toStream(out, body, toDepth, types);
+ toStream(out, body, toDepth);
if(!lets.empty()) {
out << ')';
}
} else {
- toStream(out, n, toDepth, types);
+ toStream(out, n, toDepth);
}
}
-void AstPrinter::toStream(std::ostream& out,
- TNode n,
- int toDepth,
- bool types) const
+void AstPrinter::toStream(std::ostream& out, TNode n, int toDepth) const
{
// null
if(n.getKind() == kind::NULL_EXPR) {
} else {
out << "var_" << n.getId();
}
- if(types) {
- // print the whole type, but not *its* type
- out << ":";
- n.getType().toStream(out, language::output::LANG_AST);
- }
-
return;
}
if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
out << ' ';
if(toDepth != 0) {
- toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types);
+ toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1);
} else {
out << "(...)";
}
out << ' ';
}
if(toDepth != 0) {
- toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, types);
+ toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1);
} else {
out << "(...)";
}
void toStream(std::ostream& out,
TNode n,
int toDepth,
- bool types,
size_t dag) const override;
void toStream(std::ostream& out, const CommandStatus* s) const override;
void toStream(std::ostream& out, const smt::Model& m) const override;
std::ostream& out, const std::vector<Command*>& sequence) const override;
private:
- void toStream(std::ostream& out, TNode n, int toDepth, bool types) const;
+ void toStream(std::ostream& out, TNode n, int toDepth) const;
void toStream(std::ostream& out,
const smt::Model& m,
const NodeCommand* c) const override;
namespace printer {
namespace cvc {
-void CvcPrinter::toStream(
- std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const
+void CvcPrinter::toStream(std::ostream& out,
+ TNode n,
+ int toDepth,
+ size_t dag) const
{
if(dag != 0) {
DagificationVisitor dv(dag);
} else {
first = false;
}
- toStream(out, (*i).second, toDepth, types, false);
+ toStream(out, (*i).second, toDepth, false);
out << " = ";
- toStream(out, (*i).first, toDepth, types, false);
+ toStream(out, (*i).first, toDepth, false);
}
out << " IN ";
}
Node body = dv.getDagifiedBody();
- toStream(out, body, toDepth, types, false);
+ toStream(out, body, toDepth, false);
} else {
- toStream(out, n, toDepth, types, false);
+ toStream(out, n, toDepth, false);
}
}
}
}
-void CvcPrinter::toStream(
- std::ostream& out, TNode n, int depth, bool types, bool bracket) const
+void CvcPrinter::toStream(std::ostream& out,
+ TNode n,
+ int depth,
+ bool bracket) const
{
if (depth == 0) {
out << "(...)";
}
out << n.getId();
}
- if(types) {
- // print the whole type, but not *its* type
- out << ":";
- n.getType().toStream(out, language::output::LANG_CVC4);
- }
return;
}
if(n.isNullaryOp()) {
break;
case kind::ITE:
out << "IF ";
- toStream(out, n[0], depth, types, true);
+ toStream(out, n[0], depth, true);
out << " THEN ";
- toStream(out, n[1], depth, types, true);
+ toStream(out, n[1], depth, true);
out << " ELSE ";
- toStream(out, n[2], depth, types, true);
+ toStream(out, n[2], depth, true);
out << " ENDIF";
return;
break;
if (i > 0) {
out << ", ";
}
- toStream(out, n[i], depth, types, false);
+ toStream(out, n[i], depth, false);
}
out << ']';
return;
break;
case kind::LAMBDA:
out << "(LAMBDA";
- toStream(out, n[0], depth, types, true);
+ toStream(out, n[0], depth, true);
out << ": ";
- toStream(out, n[1], depth, types, true);
+ toStream(out, n[1], depth, true);
out << ")";
return;
break;
case kind::WITNESS:
out << "(WITNESS";
- toStream(out, n[0], depth, types, false);
+ toStream(out, n[0], depth, false);
out << " : ";
- toStream(out, n[1], depth, types, false);
+ toStream(out, n[1], depth, false);
out << ')';
return;
case kind::DISTINCT:
// distinct not supported directly, blast it away with the rewriter
- toStream(out, theory::Rewriter::rewrite(n), depth, types, true);
+ toStream(out, theory::Rewriter::rewrite(n), depth, true);
return;
case kind::SORT_TYPE:
{
break;
// UF
- case kind::APPLY_UF:
- toStream(op, n.getOperator(), depth, types, false);
- break;
+ case kind::APPLY_UF: toStream(op, n.getOperator(), depth, false); break;
case kind::CARDINALITY_CONSTRAINT:
case kind::COMBINED_CARDINALITY_CONSTRAINT:
out << "CARDINALITY_CONSTRAINT";
if (i > 1) {
out << ", ";
}
- toStream(out, n[i - 1], depth, types, false);
+ toStream(out, n[i - 1], depth, false);
}
if (n.getNumChildren() > 2) {
out << ')';
}
}
out << " -> ";
- toStream(out, n[n.getNumChildren() - 1], depth, types, false);
+ toStream(out, n[n.getNumChildren() - 1], depth, false);
return;
break;
return;
break;
case kind::APPLY_TYPE_ASCRIPTION: {
- toStream(out, n[0], depth, types, false);
- out << "::";
-
TypeNode t = n.getOperator().getConst<AscriptionType>().getType();
- out << (t.isFunctionLike() ? t.getRangeType() : t);
+ toStream(out, n[0], depth, false);
+ out << "::";
+ TypeNode t = n.getOperator().getConst<AscriptionType>().getType();
+ out << (t.isFunctionLike() ? t.getRangeType() : t);
}
return;
break;
out << ", ";
}
out << recCons[i].getName() << " := ";
- toStream(out, n[i], depth, types, false);
+ toStream(out, n[i], depth, false);
}
out << " #)";
return;
}
else
{
- toStream(op, n.getOperator(), depth, types, false);
+ toStream(op, n.getOperator(), depth, false);
if (n.getNumChildren() == 0)
{
// for datatype constants d, we print "d" and not "d()"
Node opn = n.getOperator();
if (!t.isDatatype())
{
- toStream(op, opn, depth, types, false);
+ toStream(op, opn, depth, false);
}
else if (t.isTuple() || t.isRecord())
{
- toStream(out, n[0], depth, types, true);
+ toStream(out, n[0], depth, true);
out << '.';
const DType& dt = t.getDType();
if (t.isTuple())
}
else
{
- toStream(out, opn, depth, types, false);
+ toStream(out, opn, depth, false);
}
return;
}else{
- toStream(op, opn, depth, types, false);
+ toStream(op, opn, depth, false);
}
}
break;
op << "is_";
unsigned cindex = DType::indexOf(n.getOperator());
const DType& dt = DType::datatypeOf(n.getOperator());
- toStream(op, dt[cindex].getConstructor(), depth, types, false);
+ toStream(op, dt[cindex].getConstructor(), depth, false);
}
break;
case kind::CONSTRUCTOR_TYPE:
if(i > 0) {
out << ", ";
}
- toStream(out, n[i], depth, types, false);
+ toStream(out, n[i], depth, false);
}
if(n.getNumChildren() > 2) {
out << ')';
}
out << " -> ";
}
- toStream(out, n[n.getNumChildren() - 1], depth, types, false);
+ toStream(out, n[n.getNumChildren() - 1], depth, false);
return;
case kind::TESTER_TYPE:
- toStream(out, n[0], depth, types, false);
+ toStream(out, n[0], depth, false);
out << " -> BOOLEAN";
return;
break;
case kind::TUPLE_UPDATE:
- toStream(out, n[0], depth, types, true);
+ toStream(out, n[0], depth, true);
out << " WITH ." << n.getOperator().getConst<TupleUpdate>().getIndex() << " := ";
- toStream(out, n[1], depth, types, true);
+ toStream(out, n[1], depth, true);
return;
break;
case kind::RECORD_UPDATE:
- toStream(out, n[0], depth, types, true);
+ toStream(out, n[0], depth, true);
out << " WITH ." << n.getOperator().getConst<RecordUpdate>().getField() << " := ";
- toStream(out, n[1], depth, types, true);
+ toStream(out, n[1], depth, true);
return;
break;
// ARRAYS
case kind::ARRAY_TYPE:
out << "ARRAY ";
- toStream(out, n[0], depth, types, false);
+ toStream(out, n[0], depth, false);
out << " OF ";
- toStream(out, n[1], depth, types, false);
+ toStream(out, n[1], depth, false);
return;
break;
case kind::SELECT:
- toStream(out, n[0], depth, types, true);
+ toStream(out, n[0], depth, true);
out << '[';
- toStream(out, n[1], depth, types, false);
+ toStream(out, n[1], depth, false);
out << ']';
return;
break;
out << '(';
}
TNode x = stk.top();
- toStream(out, x[0], depth, types, false);
+ toStream(out, x[0], depth, false);
out << " WITH [";
- toStream(out, x[1], depth, types, false);
+ toStream(out, x[1], depth, false);
out << "] := ";
- toStream(out, x[2], depth, types, false);
+ toStream(out, x[2], depth, false);
stk.pop();
while(!stk.empty()) {
x = stk.top();
out << ", [";
- toStream(out, x[1], depth, types, false);
+ toStream(out, x[1], depth, false);
out << "] := ";
- toStream(out, x[2], depth, types, false);
+ toStream(out, x[2], depth, false);
stk.pop();
}
if (bracket) {
else
{
// ignore, there is no to-real in CVC language
- toStream(out, n[0], depth, types, false);
+ toStream(out, n[0], depth, false);
}
return;
}
case kind::DIVISIBLE:
out << "DIVISIBLE(";
- toStream(out, n[0], depth, types, false);
+ toStream(out, n[0], depth, false);
out << ", " << n.getOperator().getConst<Divisible>().k << ")";
return;
out << "BVPLUS(";
out << BitVectorType(n.getType().toType()).getSize();
out << ',';
- toStream(out, n[child], depth, types, false);
+ toStream(out, n[child], depth, false);
out << ',';
++child;
}
out << "BVPLUS(";
out << BitVectorType(n.getType().toType()).getSize();
out << ',';
- toStream(out, n[child], depth, types, false);
+ toStream(out, n[child], depth, false);
out << ',';
- toStream(out, n[child + 1], depth, types, false);
+ toStream(out, n[child + 1], depth, false);
while (child > 0) {
out << ')';
--child;
Assert(n.getType().isBitVector());
out << BitVectorType(n.getType().toType()).getSize();
out << ',';
- toStream(out, n[0], depth, types, false);
+ toStream(out, n[0], depth, false);
out << ',';
- toStream(out, n[1], depth, types, false);
+ toStream(out, n[1], depth, false);
out << ')';
return;
break;
out << "BVMULT(";
out << BitVectorType(n.getType().toType()).getSize();
out << ',';
- toStream(out, n[child], depth, types, false);
+ toStream(out, n[child], depth, false);
out << ',';
++child;
}
out << "BVMULT(";
out << BitVectorType(n.getType().toType()).getSize();
out << ',';
- toStream(out, n[child], depth, types, false);
+ toStream(out, n[child], depth, false);
out << ',';
- toStream(out, n[child + 1], depth, types, false);
+ toStream(out, n[child + 1], depth, false);
while (child > 0) {
out << ')';
--child;
break;
case kind::BITVECTOR_REPEAT:
out << "BVREPEAT(";
- toStream(out, n[0], depth, types, false);
+ toStream(out, n[0], depth, false);
out << ", " << n.getOperator().getConst<BitVectorRepeat>() << ')';
return;
break;
case kind::BITVECTOR_ZERO_EXTEND:
out << "BVZEROEXTEND(";
- toStream(out, n[0], depth, types, false);
+ toStream(out, n[0], depth, false);
out << ", " << n.getOperator().getConst<BitVectorZeroExtend>() << ')';
return;
break;
case kind::BITVECTOR_SIGN_EXTEND:
out << "SX(";
- toStream(out, n[0], depth, types, false);
+ toStream(out, n[0], depth, false);
out << ", " << BitVectorType(n.getType().toType()).getSize() << ')';
return;
break;
case kind::BITVECTOR_ROTATE_LEFT:
out << "BVROTL(";
- toStream(out, n[0], depth, types, false);
+ toStream(out, n[0], depth, false);
out << ", " << n.getOperator().getConst<BitVectorRotateLeft>() << ')';
return;
break;
case kind::BITVECTOR_ROTATE_RIGHT:
out << "BVROTR(";
- toStream(out, n[0], depth, types, false);
+ toStream(out, n[0], depth, false);
out << ", " << n.getOperator().getConst<BitVectorRotateRight>() << ')';
return;
break;
// SETS
case kind::SET_TYPE:
out << "SET OF ";
- toStream(out, n[0], depth, types, false);
+ toStream(out, n[0], depth, false);
return;
break;
case kind::UNION:
break;
case kind::SINGLETON:
out << "{";
- toStream(out, n[0], depth, types, false);
+ toStream(out, n[0], depth, false);
out << "}";
return;
break;
}
out << '{';
size_t i = 0;
- toStream(out, n[i++], depth, types, false);
+ toStream(out, n[i++], depth, false);
for(;i+1 < n.getNumChildren(); ++i) {
out << ", ";
- toStream(out, n[i], depth, types, false);
+ toStream(out, n[i], depth, false);
}
out << "} | ";
- toStream(out, n[i], depth, types, true);
+ toStream(out, n[i], depth, true);
if(bracket) {
out << ')';
}
}
case kind::CARD: {
out << "CARD(";
- toStream(out, n[0], depth, types, false);
+ toStream(out, n[0], depth, false);
out << ")";
return;
break;
// Quantifiers
case kind::FORALL:
out << "(FORALL";
- toStream(out, n[0], depth, types, false);
+ toStream(out, n[0], depth, false);
out << " : ";
- toStream(out, n[1], depth, types, false);
+ toStream(out, n[1], depth, false);
out << ')';
// TODO: user patterns?
return;
case kind::EXISTS:
out << "(EXISTS";
- toStream(out, n[0], depth, types, false);
+ toStream(out, n[0], depth, false);
out << " : ";
- toStream(out, n[1], depth, types, false);
+ toStream(out, n[1], depth, false);
out << ')';
// TODO: user patterns?
return;
if(i > 0) {
out << ", ";
}
- toStream(out, n[i], -1, true, false); // ascribe types
+ toStream(out, n[i], -1, false);
+ out << ":";
+ n[i].getType().toStream(out, language::output::LANG_CVC4);
}
out << ')';
return;
out << ", ";
}
}
- toStream(out, n[i], depth, types, opType == INFIX);
+ toStream(out, n[i], depth, opType == INFIX);
}
switch (opType) {
void toStream(std::ostream& out,
TNode n,
int toDepth,
- bool types,
size_t dag) const override;
void toStream(std::ostream& out, const CommandStatus* s) const override;
void toStream(std::ostream& out, const smt::Model& m) const override;
std::ostream& out, const std::vector<Command*>& sequence) const override;
private:
- void toStream(
- std::ostream& out, TNode n, int toDepth, bool types, bool bracket) const;
+ void toStream(std::ostream& out, TNode n, int toDepth, bool bracket) const;
void toStream(std::ostream& out,
const smt::Model& m,
const NodeCommand* c) const override;
virtual void toStream(std::ostream& out,
TNode n,
int toDepth,
- bool types,
size_t dag) const = 0;
/** Write a CommandStatus out to a stream with this Printer. */
bool decimal,
Variant v);
-void Smt2Printer::toStream(
- std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const
+void Smt2Printer::toStream(std::ostream& out,
+ TNode n,
+ int toDepth,
+ size_t dag) const
{
if(dag != 0) {
DagificationVisitor dv(dag);
theory::SubstitutionMap::const_iterator i_end = lets.end();
for(; i != i_end; ++ i) {
out << "(let ((";
- toStream(out, (*i).second, toDepth, types, TypeNode::null());
+ toStream(out, (*i).second, toDepth, TypeNode::null());
out << ' ';
- toStream(out, (*i).first, toDepth, types, TypeNode::null());
+ toStream(out, (*i).first, toDepth, TypeNode::null());
out << ")) ";
}
}
Node body = dv.getDagifiedBody();
- toStream(out, body, toDepth, types, TypeNode::null());
+ toStream(out, body, toDepth, TypeNode::null());
if(!lets.empty()) {
theory::SubstitutionMap::const_iterator i = lets.begin();
theory::SubstitutionMap::const_iterator i_end = lets.end();
}
}
} else {
- toStream(out, n, toDepth, types, TypeNode::null());
+ toStream(out, n, toDepth, TypeNode::null());
}
}
void Smt2Printer::toStream(std::ostream& out,
TNode n,
int toDepth,
- bool types,
TypeNode force_nt) const
{
// null
if(n.getNumChildren() != 0) {
for(unsigned i = 0; i < n.getNumChildren(); ++i) {
out << ' ';
- toStream(out, n[i], toDepth, types, TypeNode::null());
+ toStream(out, n[i], toDepth, TypeNode::null());
}
out << ')';
}
<< smtKindString(is_int ? kind::TO_INTEGER : kind::DIVISION,
d_variant)
<< " ";
- toStream(out, type_asc_arg, toDepth, types, TypeNode::null());
+ toStream(out, type_asc_arg, toDepth, TypeNode::null());
if (!is_int)
{
out << " 1";
toStream(out,
type_asc_arg,
toDepth < 0 ? toDepth : toDepth - 1,
- types,
TypeNode::null());
out << " " << force_nt << ")";
}
}
out << n.getId();
}
- if (types)
- {
- // print the whole type, but not *its* type
- out << ":";
- n.getType().toStream(out, language::output::LANG_SMTLIB_V2_5);
- }
-
return;
}
for (Node nc : n)
{
out << " ";
- toStream(out, nc, toDepth, types, TypeNode::null());
+ toStream(out, nc, toDepth, TypeNode::null());
}
out << ")";
return;
args.insert(args.begin(), head[1]);
head = head[0];
}
- toStream(out, head, toDepth, types, TypeNode::null());
+ toStream(out, head, toDepth, TypeNode::null());
for (unsigned i = 0, size = args.size(); i < size; ++i)
{
out << " ";
- toStream(out, args[i], toDepth, types, TypeNode::null());
+ toStream(out, args[i], toDepth, TypeNode::null());
}
out << ")";
}
case kind::LAMBDA: out << smtKindString(k, d_variant) << " "; break;
case kind::MATCH:
out << smtKindString(k, d_variant) << " ";
- toStream(out, n[0], toDepth, types, TypeNode::null());
+ toStream(out, n[0], toDepth, TypeNode::null());
out << " (";
for (size_t i = 1, nchild = n.getNumChildren(); i < nchild; i++)
{
{
out << " ";
}
- toStream(out, n[i], toDepth, types, TypeNode::null());
+ toStream(out, n[i], toDepth, TypeNode::null());
}
out << "))";
return;
case kind::MATCH_BIND_CASE:
// ignore the binder
- toStream(out, n[1], toDepth, types, TypeNode::null());
+ toStream(out, n[1], toDepth, TypeNode::null());
out << " ";
- toStream(out, n[2], toDepth, types, TypeNode::null());
+ toStream(out, n[2], toDepth, TypeNode::null());
out << ")";
return;
case kind::MATCH_CASE:
for (TNode::iterator i = n.begin(), iend = n.end(); i != iend;)
{
out << '(';
- toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, types, 0);
+ toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, 0);
out << ' ';
out << (*i).getType();
out << ')';
toStream(out,
dt[cindex].getConstructor(),
toDepth < 0 ? toDepth : toDepth - 1,
- types,
TypeNode::null());
out << ")";
}else{
toStream(out,
dt[cindex].getConstructor(),
toDepth < 0 ? toDepth : toDepth - 1,
- types,
TypeNode::null());
}
}else{
- toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null());
+ toStream(out,
+ n.getOperator(),
+ toDepth < 0 ? toDepth : toDepth - 1,
+ TypeNode::null());
}
} else {
out << "(...)";
Node cn = n[i];
std::map< unsigned, TypeNode >::iterator itfc = force_child_type.find( i );
if( itfc!=force_child_type.end() ){
- toStream(out, cn, toDepth < 0 ? toDepth : toDepth - c, types, itfc->second);
+ toStream(out, cn, toDepth < 0 ? toDepth : toDepth - c, itfc->second);
}else{
- toStream(out, cn, toDepth < 0 ? toDepth : toDepth - c, types, TypeNode::null());
+ toStream(
+ out, cn, toDepth < 0 ? toDepth : toDepth - c, TypeNode::null());
}
} else {
out << "(...)";
out << "(define-fun " << n << " " << val[0] << " "
<< n.getType().getRangeType() << " ";
// call toStream and force its type to be proper
- toStream(out, val[1], -1, false, n.getType().getRangeType());
+ toStream(out, val[1], -1, n.getType().getRangeType());
out << ")" << endl;
}
else
}
out << "(define-fun " << n << " () " << n.getType() << " ";
// call toStream and force its type to be proper
- toStream(out, val, -1, false, n.getType());
+ toStream(out, val, -1, n.getType());
out << ")" << endl;
}
}
void toStream(std::ostream& out,
TNode n,
int toDepth,
- bool types,
size_t dag) const override;
void toStream(std::ostream& out, const CommandStatus* s) const override;
void toStream(std::ostream& out, const smt::Model& m) const override;
std::ostream& out, const std::vector<Command*>& sequence) const override;
private:
- void toStream(
- std::ostream& out, TNode n, int toDepth, bool types, TypeNode nt) const;
+ void toStream(std::ostream& out, TNode n, int toDepth, TypeNode nt) const;
void toStream(std::ostream& out,
const smt::Model& m,
const NodeCommand* c) const override;
namespace printer {
namespace tptp {
-void TptpPrinter::toStream(
- std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const
+void TptpPrinter::toStream(std::ostream& out,
+ TNode n,
+ int toDepth,
+ size_t dag) const
{
- n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
+ n.toStream(out, toDepth, dag, language::output::LANG_SMTLIB_V2_5);
}/* TptpPrinter::toStream() */
void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const
void toStream(std::ostream& out,
TNode n,
int toDepth,
- bool types,
size_t dag) const override;
void toStream(std::ostream& out, const CommandStatus* s) const override;
void toStream(std::ostream& out, const smt::Model& m) const override;
{
c.toStream(out,
Node::setdepth::getDepth(out),
- Node::printtypes::getPrintTypes(out),
Node::dag::getDag(out),
Node::setlanguage::getLanguage(out));
return out;
void EmptyCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void EchoCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void AssertCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void PushCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void PopCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void CheckSatCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void CheckSatAssumingCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void QueryCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void DeclareSygusVarCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void SynthFunCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void SygusConstraintCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void SygusInvConstraintCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void CheckSynthCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void ResetCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void ResetAssertionsCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void QuitCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void CommentCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void CommandSequence::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void DeclarationSequence::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void DeclareFunctionCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void DeclareSortCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void DefineSortCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void DefineFunctionCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void DefineNamedFunctionCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void DefineFunctionRecCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void SetUserAttributeCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void SimplifyCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void GetValueCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void GetAssignmentCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void GetModelCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void BlockModelCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void BlockModelValuesCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void GetProofCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void GetInstantiationsCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void GetSynthSolutionCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void GetInterpolCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void GetAbductCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void GetQuantifierEliminationCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void GetUnsatAssumptionsCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void GetUnsatCoreCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void GetAssertionsCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void SetBenchmarkStatusCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void SetBenchmarkLogicCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void SetInfoCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void GetInfoCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void SetOptionCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void GetOptionCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void SetExpressionNameCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
void DatatypeDeclarationCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
+
size_t dag,
OutputLanguage language) const
{
virtual void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const = 0;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class AssertCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class PushCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class PopCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class DeclareFunctionCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class DeclareSortCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class DefineSortCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class DefineNamedFunctionCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class QueryCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class SimplifyCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class GetValueCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class GetAssignmentCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class BlockModelCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class GetProofCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class GetQuantifierEliminationCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class GetAssertionsCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class SetBenchmarkStatusCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class SetBenchmarkLogicCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class SetInfoCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class GetInfoCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class SetOptionCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class GetOptionCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class SetExpressionNameCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class DatatypeDeclarationCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class ResetCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class ResetAssertionsCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class QuitCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class CommentCommand */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class CommandSequence */
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
+
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
};
{
nc.toStream(out,
Node::setdepth::getDepth(out),
- Node::printtypes::getPrintTypes(out),
Node::dag::getDag(out),
Node::setlanguage::getLanguage(out));
return out;
void DeclareFunctionNodeCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
size_t dag,
OutputLanguage language) const
{
void DeclareTypeNodeCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
size_t dag,
OutputLanguage language) const
{
void DeclareDatatypeNodeCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
size_t dag,
OutputLanguage language) const
{
void DefineFunctionNodeCommand::toStream(std::ostream& out,
int toDepth,
- bool types,
size_t dag,
OutputLanguage language) const
{
virtual void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const = 0;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
NodeCommand* clone() const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
NodeCommand* clone() const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
NodeCommand* clone() const override;
void toStream(
std::ostream& out,
int toDepth = -1,
- bool types = false,
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
NodeCommand* clone() const override;
{
notifySetOption(options::defaultDagThresh.getName());
}
- if (opts->wasSetByUser(options::printExprTypes))
- {
- notifySetOption(options::printExprTypes.getName());
- }
if (opts->wasSetByUser(options::dumpModeString))
{
notifySetOption(options::dumpModeString.getName());
Warning.getStream() << expr::ExprDag(dag);
Dump.getStream() << expr::ExprDag(dag);
}
- else if (key == options::printExprTypes.getName())
- {
- bool value = (*d_options)[options::printExprTypes];
- Debug.getStream() << expr::ExprPrintTypes(value);
- Trace.getStream() << expr::ExprPrintTypes(value);
- Notice.getStream() << expr::ExprPrintTypes(value);
- Chat.getStream() << expr::ExprPrintTypes(value);
- Message.getStream() << expr::ExprPrintTypes(value);
- Warning.getStream() << expr::ExprPrintTypes(value);
- // intentionally exclude Dump stream from this list
- }
else if (key == options::dumpModeString.getName())
{
const std::string& value = (*d_options)[options::dumpModeString];
ChannelSettings(std::ostream& out)
: d_dagSetting(expr::ExprDag::getDag(out)),
d_exprDepthSetting(expr::ExprSetDepth::getDepth(out)),
- d_printtypesSetting(expr::ExprPrintTypes::getPrintTypes(out)),
d_languageSetting(language::SetLanguage::getLanguage(out))
{}
void apply(std::ostream& out) {
out << expr::ExprDag(d_dagSetting);
out << expr::ExprSetDepth(d_exprDepthSetting);
- out << expr::ExprPrintTypes(d_printtypesSetting);
out << language::SetLanguage(d_languageSetting);
}
private:
const int d_dagSetting;
const size_t d_exprDepthSetting;
- const bool d_printtypesSetting;
const OutputLanguage d_languageSetting;
}; /* class ChannelSettings */
TS_ASSERT(sstr.str() == "(AND w (OR x y) z)");
sstr.str(string());
- o.toStream(sstr, -1, false, 0);
+ o.toStream(sstr, -1, 0);
TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
sstr.str(string());
projects / cvc5.git / commitdiff