summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/expr/expr.cpp47
-rw-r--r--src/expr/expr.h43
-rw-r--r--src/expr/expr_builder.cpp106
-rw-r--r--src/expr/expr_builder.h24
-rw-r--r--src/expr/expr_manager.cpp13
-rw-r--r--src/expr/expr_manager.h10
-rw-r--r--src/expr/expr_value.cpp7
-rw-r--r--src/expr/expr_value.h18
-rw-r--r--src/smt/smt_engine.cpp2
-rw-r--r--src/util/command.cpp2
-rw-r--r--src/util/command.h2
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:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback