diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/expr.cpp | 47 | ||||
-rw-r--r-- | src/expr/expr.h | 43 | ||||
-rw-r--r-- | src/expr/expr_builder.cpp | 106 | ||||
-rw-r--r-- | src/expr/expr_builder.h | 24 | ||||
-rw-r--r-- | src/expr/expr_manager.cpp | 13 | ||||
-rw-r--r-- | src/expr/expr_manager.h | 10 | ||||
-rw-r--r-- | src/expr/expr_value.cpp | 7 | ||||
-rw-r--r-- | src/expr/expr_value.h | 18 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 2 | ||||
-rw-r--r-- | src/util/command.cpp | 2 | ||||
-rw-r--r-- | src/util/command.h | 2 |
11 files changed, 162 insertions, 112 deletions
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index e88189bcc..fa273dfa5 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -13,6 +13,7 @@ #include "expr/expr.h" #include "expr_value.h" #include "expr_builder.h" +#include "util/Assert.h" using namespace CVC4::expr; @@ -33,70 +34,82 @@ Expr::Expr() : Expr::Expr(ExprValue* ev) : d_ev(ev) { - if(d_ev != 0) - d_ev->inc(); + Assert(d_ev != NULL, "Expecting a non-NULL evpression value!"); + d_ev->inc(); } Expr::Expr(const Expr& e) { - if((d_ev = e.d_ev) && d_ev != 0) - d_ev->inc(); + Assert(e.d_ev != NULL, "Expecting a non-NULL evpression value!"); + d_ev = e.d_ev; + d_ev->inc(); } Expr::~Expr() { - if(d_ev) - d_ev->dec(); + Assert(d_ev != NULL, "Expecting a non-NULL evpression value!"); + d_ev->dec(); +} + +void Expr::assignExprValue(ExprValue* ev) { + d_ev = ev; + d_ev->inc(); } Expr& Expr::operator=(const Expr& e) { - if(d_ev) + Assert(d_ev != NULL, "Expecting a non-NULL evpression value!"); + if(this != &e && d_ev != e.d_ev) { d_ev->dec(); - if((d_ev = e.d_ev)) + d_ev = e.d_ev; d_ev->inc(); + } return *this; } -ExprValue* Expr::operator->() const { +ExprValue const* Expr::operator->() const { + Assert(d_ev != NULL, "Expecting a non-NULL evpression value!"); return d_ev; } uint64_t Expr::hash() const { + Assert(d_ev != NULL, "Expecting a non-NULL evpression value!"); return d_ev->hash(); } Expr Expr::eqExpr(const Expr& right) const { - return ExprBuilder(*this).eqExpr(right); + return ExprManager::currentEM()->mkExpr(EQUAL, *this, right); } Expr Expr::notExpr() const { - return ExprBuilder(*this).notExpr(); + return ExprManager::currentEM()->mkExpr(NOT, *this); } +// FIXME: What does this do and why? Expr Expr::negate() const { // avoid double-negatives return ExprBuilder(*this).negate(); } + Expr Expr::andExpr(const Expr& right) const { - return ExprBuilder(*this).andExpr(right); + return ExprManager::currentEM()->mkExpr(AND, *this, right); } Expr Expr::orExpr(const Expr& right) const { - return ExprBuilder(*this).orExpr(right); + return ExprManager::currentEM()->mkExpr(OR, *this, right); } Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const { - return ExprBuilder(*this).iteExpr(thenpart, elsepart); + return ExprManager::currentEM()->mkExpr(ITE, *this, thenpart, elsepart); } Expr Expr::iffExpr(const Expr& right) const { - return ExprBuilder(*this).iffExpr(right); + return ExprManager::currentEM()->mkExpr(IFF, *this, right); } Expr Expr::impExpr(const Expr& right) const { - return ExprBuilder(*this).impExpr(right); + return ExprManager::currentEM()->mkExpr(IMPLIES, *this, right); } Expr Expr::xorExpr(const Expr& right) const { - return ExprBuilder(*this).xorExpr(right); + return ExprManager::currentEM()->mkExpr(XOR, *this, right); } }/* CVC4 namespace */ diff --git a/src/expr/expr.h b/src/expr/expr.h index 013888baa..7440974d8 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -26,7 +26,7 @@ namespace CVC4 { namespace CVC4 { -inline std::ostream& operator<<(std::ostream&, CVC4::Expr) CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream&, const Expr&) CVC4_PUBLIC; class ExprManager; @@ -41,6 +41,9 @@ using CVC4::expr::ExprValue; * maintained in the ExprValue. */ class CVC4_PUBLIC Expr { + + friend class ExprValue; + /** A convenient null-valued encapsulated pointer */ static Expr s_null; @@ -57,6 +60,19 @@ class CVC4_PUBLIC Expr { friend class ExprBuilder; friend class ExprManager; + /** Access to the encapsulated expression. + * @return the encapsulated expression. */ + ExprValue const* operator->() const; + + /** + * 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 are + * doing. + * + * @param ev the expression value to assign + */ + void assignExprValue(ExprValue* ev); + public: /** Default constructor, makes a null expression. */ @@ -70,13 +86,14 @@ public: bool operator==(const Expr& e) const { return d_ev == e.d_ev; } bool operator!=(const Expr& e) const { return d_ev != e.d_ev; } - bool operator<(const Expr& e) const { return d_ev < e.d_ev; }// for map key - Expr& operator=(const Expr&); + /** + * We compare by expression ids so, keeping things deterministic and having + * that subexpressions have to be smaller than the enclosing expressions. + */ + inline bool operator<(const Expr& e) const; - /** Access to the encapsulated expression. - * @return the encapsulated expression. */ - ExprValue* operator->() const; + Expr& operator=(const Expr&); uint64_t hash() const; @@ -105,8 +122,8 @@ public: inline iterator begin(); inline iterator end(); - inline iterator begin() const; - inline iterator end() const; + inline const_iterator begin() const; + inline const_iterator end() const; void toString(std::ostream&) const; @@ -120,7 +137,11 @@ public: namespace CVC4 { -inline std::ostream& operator<<(std::ostream& out, CVC4::Expr e) { +inline bool Expr::operator<(const Expr& e) const { + return d_ev->d_id < e.d_ev->d_id; +} + +inline std::ostream& operator<<(std::ostream& out, const Expr& e) { e.toString(out); return out; } @@ -143,11 +164,11 @@ inline Expr::iterator Expr::end() { return d_ev->end(); } -inline Expr::iterator Expr::begin() const { +inline Expr::const_iterator Expr::begin() const { return d_ev->begin(); } -inline Expr::iterator Expr::end() const { +inline Expr::const_iterator Expr::end() const { return d_ev->end(); } diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp index 4de22f987..10152a338 100644 --- a/src/expr/expr_builder.cpp +++ b/src/expr/expr_builder.cpp @@ -12,20 +12,24 @@ #include "expr_builder.h" #include "expr_manager.h" #include "expr_value.h" -#include "util/Assert.h" #include "util/output.h" using namespace std; namespace CVC4 { -ExprBuilder::ExprBuilder() : d_em(ExprManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(0) {} +ExprBuilder::ExprBuilder() : + d_em(ExprManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), + d_nchildren(0) { +} -ExprBuilder::ExprBuilder(Kind k) : d_em(ExprManager::currentEM()), d_kind(k), d_used(false), d_nchildren(0) {} +ExprBuilder::ExprBuilder(Kind k) : + d_em(ExprManager::currentEM()), d_kind(k), d_used(false), d_nchildren(0) { +} -ExprBuilder::ExprBuilder(const Expr& e) : d_em(ExprManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) { - ExprValue *v = e->inc(); - d_children.u_arr[0] = v; +ExprBuilder::ExprBuilder(const Expr& e) : + d_em(ExprManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) { + d_children.u_arr[0] = e.d_ev->inc();; } ExprBuilder& ExprBuilder::reset(const ExprValue* ev) { @@ -38,36 +42,45 @@ ExprBuilder& ExprBuilder::reset(const ExprValue* ev) { return *this; } -ExprBuilder::ExprBuilder(const ExprBuilder& eb) : d_em(eb.d_em), d_kind(eb.d_kind), d_used(eb.d_used), d_nchildren(eb.d_nchildren) { +ExprBuilder::ExprBuilder(const ExprBuilder& eb) : + d_em(eb.d_em), d_kind(eb.d_kind), d_used(eb.d_used), + d_nchildren(eb.d_nchildren) { Assert( !d_used ); if(d_nchildren > nchild_thresh) { - d_children.u_vec = new vector<Expr>(); + d_children.u_vec = new vector<Expr> (); d_children.u_vec->reserve(d_nchildren + 5); - copy(eb.d_children.u_vec->begin(), eb.d_children.u_vec->end(), back_inserter(*d_children.u_vec)); + copy(eb.d_children.u_vec->begin(), eb.d_children.u_vec->end(), + back_inserter(*d_children.u_vec)); } else { ev_iterator j = d_children.u_arr; - for(ExprValue* const* i = eb.d_children.u_arr; i != eb.d_children.u_arr + eb.d_nchildren; ++i, ++j) + ExprValue* const * i = eb.d_children.u_arr; + ExprValue* const * i_end = i + eb.d_nchildren; + for(; i != i_end; ++i, ++j) *j = (*i)->inc(); } } -ExprBuilder::ExprBuilder(ExprManager* em) : d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(0) { +ExprBuilder::ExprBuilder(ExprManager* em) : + d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(0) { } -ExprBuilder::ExprBuilder(ExprManager* em, Kind k) : d_em(em), d_kind(k), d_used(false), d_nchildren(0) { +ExprBuilder::ExprBuilder(ExprManager* em, Kind k) : + d_em(em), d_kind(k), d_used(false), d_nchildren(0) { } -ExprBuilder::ExprBuilder(ExprManager* em, const Expr& e) : d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) { - ExprValue *v = e->inc(); - d_children.u_arr[0] = v; +ExprBuilder::ExprBuilder(ExprManager* em, const Expr& e) : + d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) { + d_children.u_arr[0] = e.d_ev->inc(); } ExprBuilder::~ExprBuilder() { if(d_nchildren > nchild_thresh) { delete d_children.u_vec; } else { - for(ev_iterator i = d_children.u_arr; i != d_children.u_arr + d_nchildren; ++i) { + ev_iterator i = d_children.u_arr; + ev_iterator i_end = d_children.u_arr + d_nchildren; + for(; i != i_end ; ++i) { (*i)->dec(); } } @@ -94,8 +107,7 @@ ExprBuilder& ExprBuilder::notExpr() { // avoid double-negatives ExprBuilder& ExprBuilder::negate() { if(EXPECT_FALSE( d_kind == NOT )) - return reset(d_children.u_arr[0]); - Assert( d_kind != UNDEFINED_KIND ); + return reset(d_children.u_arr[0]); Assert( d_kind != UNDEFINED_KIND ); collapse(); d_kind = NOT; return *this; @@ -169,39 +181,27 @@ ExprBuilder& ExprBuilder::operator<<(const Expr& child) { return *this; } -void ExprBuilder::addChild(const Expr& e) { - Debug("expr") << "adding child E " << e << endl; - if(d_nchildren == nchild_thresh) { - Debug("expr") << "reached thresh " << nchild_thresh << ", copying" << endl; - vector<Expr>* v = new vector<Expr>(); - v->reserve(nchild_thresh + 5); - for(ExprValue** i = d_children.u_arr; i != d_children.u_arr + nchild_thresh; ++i) { - v->push_back(Expr(*i)); - (*i)->dec(); - } - v->push_back(e); - d_children.u_vec = v; - ++d_nchildren; - } else if(d_nchildren > nchild_thresh) { - Debug("expr") << "over thresh " << d_nchildren << " > " << nchild_thresh << endl; - d_children.u_vec->push_back(e); - ++d_nchildren; - } else { - Debug("expr") << "under thresh " << d_nchildren << " < " << nchild_thresh << endl; - ExprValue *ev = e.d_ev; - d_children.u_arr[d_nchildren] = ev; - ev->inc(); - ++d_nchildren; - } -} - +/** + * We keep the children either: + * (a) In the array of expression values if the number of children is less than + * nchild_thresh. Hence (last else) we increase the reference count. + * (b) If the number of children reaches the nchild_thresh, we allocate a vector + * for the children. Children are now expressions, so we also decrement the + * reference count for each child. + * (c) Otherwise we just add to the end of the vector. + */ void ExprBuilder::addChild(ExprValue* ev) { + Assert(d_nchildren <= nchild_thresh || + d_nchildren == d_children.u_vec->size(), + "children count doesn't reflect the size of the vector!"); Debug("expr") << "adding child ev " << ev << endl; if(d_nchildren == nchild_thresh) { Debug("expr") << "reached thresh " << nchild_thresh << ", copying" << endl; - vector<Expr>* v = new vector<Expr>(); + vector<Expr>* v = new vector<Expr> (); v->reserve(nchild_thresh + 5); - for(ExprValue** i = d_children.u_arr; i != d_children.u_arr + nchild_thresh; ++i) { + ExprValue** i = d_children.u_arr; + ExprValue** i_end = i + nchild_thresh; + for(;i != i_end; ++ i) { v->push_back(Expr(*i)); (*i)->dec(); } @@ -209,20 +209,20 @@ void ExprBuilder::addChild(ExprValue* ev) { d_children.u_vec = v; ++d_nchildren; } else if(d_nchildren > nchild_thresh) { - Debug("expr") << "over thresh " << d_nchildren << " > " << nchild_thresh << endl; + Debug("expr") << "over thresh " << d_nchildren + << " > " << nchild_thresh << endl; d_children.u_vec->push_back(Expr(ev)); - ++d_nchildren; + // ++d_nchildren; no need for this } else { - Debug("expr") << "under thresh " << d_nchildren << " < " << nchild_thresh << endl; - d_children.u_arr[d_nchildren] = ev; - ev->inc(); - ++d_nchildren; + Debug("expr") << "under thresh " << d_nchildren + << " < " << nchild_thresh << endl; + d_children.u_arr[d_nchildren ++] = ev->inc(); } } ExprBuilder& ExprBuilder::collapse() { if(d_nchildren == nchild_thresh) { - vector<Expr>* v = new vector<Expr>(); + vector<Expr>* v = new vector<Expr> (); v->reserve(nchild_thresh + 5); // Unreachable();// unimplemented diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h index d70acb1fb..34e34bf6e 100644 --- a/src/expr/expr_builder.h +++ b/src/expr/expr_builder.h @@ -17,6 +17,7 @@ #include "expr_manager.h" #include "kind.h" +#include "util/Assert.h" namespace CVC4 { @@ -43,7 +44,7 @@ class ExprBuilder { std::vector<Expr>* u_vec; } d_children; - void addChild(const Expr&); + void addChild(const Expr& e) { addChild(e.d_ev); } void addChild(ExprValue*); ExprBuilder& collapse(); @@ -203,26 +204,27 @@ inline ExprBuilder::operator Expr() { ExprValue *ev; uint64_t hash; + Assert(d_kind != UNDEFINED_KIND, "Can't make an expression of an undefined kind!"); + // variables are permitted to be duplicates (from POV of the expression manager) if(d_kind == VARIABLE) { ev = new ExprValue; hash = reinterpret_cast<uint64_t>(ev); } else { - hash = d_kind; - if(d_nchildren <= nchild_thresh) { - for(ev_iterator i = ev_begin(); i != ev_end(); ++i) - hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ (*i)->hash(); - + hash = ExprValue::computeHash<ev_iterator>(d_kind, ev_begin(), ev_end()); void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Expr)); ev = new (space) ExprValue; size_t nc = 0; - for(ev_iterator i = ev_begin(); i != ev_end(); ++i) - ev->d_children[nc++] = Expr(*i); + ev_iterator i = ev_begin(); + ev_iterator i_end = ev_end(); + for(; i != i_end; ++i) { + // The expressions in the allocated children are all 0, so we must + // construct it withouth using an assignment operator + ev->d_children[nc++].assignExprValue(*i); + } } else { - for(std::vector<Expr>::iterator i = d_children.u_vec->begin(); i != d_children.u_vec->end(); ++i) - hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ (*i)->hash(); - + hash = ExprValue::computeHash<std::vector<Expr>::const_iterator>(d_kind, d_children.u_vec->begin(), d_children.u_vec->end()); void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Expr)); ev = new (space) ExprValue; size_t nc = 0; diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index 9b7697e4f..3b5347301 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -19,6 +19,7 @@ namespace CVC4 { __thread ExprManager* ExprManager::s_current = 0; Expr ExprManager::lookup(uint64_t hash, const Expr& e) { + Assert(this != NULL, "Woops, we have a bad expression manager!"); hash_t::iterator i = d_hash.find(hash); if(i == d_hash.end()) { // insert @@ -34,7 +35,7 @@ Expr ExprManager::lookup(uint64_t hash, const Expr& e) { if(e.numChildren() != j->numChildren()) continue; - Expr::iterator c1 = e.begin(); + Expr::const_iterator c1 = e.begin(); Expr::iterator c2 = j->begin(); for(; c1 != e.end() && c2 != j->end(); ++c1, ++c2) { if(c1->d_ev != c2->d_ev) @@ -60,23 +61,23 @@ Expr ExprManager::mkExpr(Kind kind) { return ExprBuilder(this, kind); } -Expr ExprManager::mkExpr(Kind kind, Expr child1) { +Expr ExprManager::mkExpr(Kind kind, const Expr& child1) { return ExprBuilder(this, kind) << child1; } -Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) { +Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) { return ExprBuilder(this, kind) << child1 << child2; } -Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3) { +Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3) { return ExprBuilder(this, kind) << child1 << child2 << child3; } -Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4) { +Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4) { return ExprBuilder(this, kind) << child1 << child2 << child3 << child4; } -Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5) { +Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4, const Expr& child5) { return ExprBuilder(this, kind) << child1 << child2 << child3 << child4 << child5; } diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index d311445f3..542d1040d 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -39,11 +39,11 @@ public: // general expression-builders Expr mkExpr(Kind kind); - Expr mkExpr(Kind kind, Expr child1); - Expr mkExpr(Kind kind, Expr child1, Expr child2); - Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3); - Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); - Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5); + Expr mkExpr(Kind kind, const Expr& child1); + Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2); + Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3); + Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4); + Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4, const Expr& child5); // N-ary version Expr mkExpr(Kind kind, std::vector<Expr> children); diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp index 250803281..17f3b64c3 100644 --- a/src/expr/expr_value.cpp +++ b/src/expr/expr_value.cpp @@ -25,12 +25,7 @@ ExprValue::ExprValue() : } uint64_t ExprValue::hash() const { - uint64_t hash = d_kind; - - for(const_iterator i = begin(); i != end(); ++i) - hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ i->hash(); - - return hash; + return computeHash<const_iterator>(d_kind, begin(), end()); } ExprValue* ExprValue::inc() { diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h index 18ad84073..b334e1c2d 100644 --- a/src/expr/expr_value.h +++ b/src/expr/expr_value.h @@ -74,6 +74,22 @@ class ExprValue { /** Private default constructor for the null value. */ ExprValue(); + /** + * Computes the hash over the given iterator span of children, and the + * root hash. The iterator should be either over a range of Expr or pointers + * to ExprValue. + * @param hash the initial value for the hash + * @param begin the begining of the range + * @param end the end of the range + * @return the hash value + */ + template<typename const_iterator_type> + static uint64_t computeHash(uint64_t hash, const_iterator_type begin, const_iterator_type end) { + for(const_iterator_type i = begin; i != end; ++i) + hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ (*i)->getId(); + return hash; + } + public: /** Hash this expression. * @return the hash value of this expression. */ @@ -94,6 +110,8 @@ public: const_iterator rbegin() const; const_iterator rend() const; + unsigned getId() const { return d_id; } + unsigned getKind() const { return (Kind) d_kind; } void CVC4_PUBLIC toString(std::ostream& out) const; }; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 412c0f3af..2e895cdc0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -27,7 +27,7 @@ void SmtEngine::processAssertionList() { for(std::vector<Expr>::iterator i = d_assertions.begin(); i != d_assertions.end(); ++i) - d_expr = d_expr.isNull() ? *i : d_expr.andExpr(*i); + d_expr = d_expr.isNull() ? *i : d_em->mkExpr(AND, d_expr, *i); } Result SmtEngine::check() { diff --git a/src/util/command.cpp b/src/util/command.cpp index c78fbc089..ed6b61703 100644 --- a/src/util/command.cpp +++ b/src/util/command.cpp @@ -14,7 +14,7 @@ using namespace std; namespace CVC4 { -ostream& operator<<(ostream& out, const CVC4::Command& c) { +ostream& operator<<(ostream& out, const Command& c) { c.toString(out); return out; } diff --git a/src/util/command.h b/src/util/command.h index 501aa31e0..31acbc43b 100644 --- a/src/util/command.h +++ b/src/util/command.h @@ -25,7 +25,7 @@ namespace CVC4 { namespace CVC4 { -std::ostream& operator<<(std::ostream&, const CVC4::Command&) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC; class CVC4_PUBLIC Command { public: |