libexpr_la_SOURCES = \
attr_type.h \
attr_var_name.h \
- expr.h \
- expr_builder.h \
+ node.h \
+ node_builder.h \
expr_value.h \
- expr_manager.h \
- expr_attribute.h \
+ node_manager.h \
+ node_attribute.h \
kind.h \
- expr.cpp \
- expr_builder.cpp \
- expr_manager.cpp \
+ node.cpp \
+ node_builder.cpp \
+ node_manager.cpp \
expr_value.cpp
CONFIG_CLEAN_VPATH_FILES =
LTLIBRARIES = $(noinst_LTLIBRARIES)
libexpr_la_LIBADD =
-am_libexpr_la_OBJECTS = expr.lo expr_builder.lo expr_manager.lo \
+am_libexpr_la_OBJECTS = node.lo node_builder.lo node_manager.lo \
expr_value.lo
libexpr_la_OBJECTS = $(am_libexpr_la_OBJECTS)
DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
libexpr_la_SOURCES = \
attr_type.h \
attr_var_name.h \
- expr.h \
- expr_builder.h \
+ node.h \
+ node_builder.h \
expr_value.h \
- expr_manager.h \
- expr_attribute.h \
+ node_manager.h \
+ node_attribute.h \
kind.h \
- expr.cpp \
- expr_builder.cpp \
- expr_manager.cpp \
+ node.cpp \
+ node_builder.cpp \
+ node_manager.cpp \
expr_value.cpp
all: all-am
distclean-compile:
-rm -f *.tab.c
-@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr.Plo@am__quote@
-@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr_builder.Plo@am__quote@
-@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr_manager.Plo@am__quote@
@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr_value.Plo@am__quote@
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node.Plo@am__quote@
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node_builder.Plo@am__quote@
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node_manager.Plo@am__quote@
.cpp.o:
@am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
class Type_attr {
public:
enum { hash_value = 11 }; // could use typeid but then different on different machines/compiles
- typedef Type value_type;//Expr?
+ typedef Type value_type;//Node?
static const Type_attr marker;
};
class VarName_attr {
public:
enum { hash_value = 11 }; // could use typeid but then different on different machines/compiles
- typedef Type value_type;//Expr?
+ typedef Type value_type;//Node?
static const Type_attr marker;
};
+++ /dev/null
-/********************* -*- C++ -*- */
-/** expr.cpp
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- ** Reference-counted encapsulation of a pointer to an expression.
- **/
-
-#include "expr/expr.h"
-#include "expr_value.h"
-#include "expr_builder.h"
-#include "util/Assert.h"
-
-using namespace CVC4::expr;
-
-namespace CVC4 {
-
-ExprValue ExprValue::s_null;
-
-Expr Expr::s_null(&ExprValue::s_null);
-
-bool Expr::isNull() const {
- return d_ev == &ExprValue::s_null;
-}
-
-Expr::Expr() :
- d_ev(&ExprValue::s_null) {
- // No refcount needed
-}
-
-Expr::Expr(ExprValue* ev)
- : d_ev(ev) {
- Assert(d_ev != NULL, "Expecting a non-NULL evpression value!");
- d_ev->inc();
-}
-
-Expr::Expr(const Expr& e) {
- Assert(e.d_ev != NULL, "Expecting a non-NULL evpression value!");
- d_ev = e.d_ev;
- d_ev->inc();
-}
-
-Expr::~Expr() {
- 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) {
- Assert(d_ev != NULL, "Expecting a non-NULL evpression value!");
- if(this != &e && d_ev != e.d_ev) {
- d_ev->dec();
- d_ev = e.d_ev;
- d_ev->inc();
- }
- return *this;
-}
-
-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 ExprManager::currentEM()->mkExpr(EQUAL, *this, right);
-}
-
-Expr Expr::notExpr() const {
- 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 ExprManager::currentEM()->mkExpr(AND, *this, right);
-}
-
-Expr Expr::orExpr(const Expr& right) const {
- return ExprManager::currentEM()->mkExpr(OR, *this, right);
-}
-
-Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const {
- return ExprManager::currentEM()->mkExpr(ITE, *this, thenpart, elsepart);
-}
-
-Expr Expr::iffExpr(const Expr& right) const {
- return ExprManager::currentEM()->mkExpr(IFF, *this, right);
-}
-
-Expr Expr::impExpr(const Expr& right) const {
- return ExprManager::currentEM()->mkExpr(IMPLIES, *this, right);
-}
-
-Expr Expr::xorExpr(const Expr& right) const {
- return ExprManager::currentEM()->mkExpr(XOR, *this, right);
-}
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** cvc4_expr.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- ** Reference-counted encapsulation of a pointer to an expression.
- **/
-
-#ifndef __CVC4__EXPR_H
-#define __CVC4__EXPR_H
-
-#include <vector>
-#include <iostream>
-#include <stdint.h>
-
-#include "cvc4_config.h"
-#include "expr/kind.h"
-
-namespace CVC4 {
- class Expr;
-}/* CVC4 namespace */
-
-namespace CVC4 {
-
-inline std::ostream& operator<<(std::ostream&, const Expr&) CVC4_PUBLIC;
-
-class ExprManager;
-
-namespace expr {
- class ExprValue;
-}/* CVC4::expr namespace */
-
-using CVC4::expr::ExprValue;
-
-/**
- * Encapsulation of an ExprValue pointer. The reference count is
- * maintained in the ExprValue.
- */
-class CVC4_PUBLIC Expr {
-
- friend class ExprValue;
-
- /** A convenient null-valued encapsulated pointer */
- static Expr s_null;
-
- /** The referenced ExprValue */
- ExprValue* d_ev;
-
- /** This constructor is reserved for use by the Expr package; one
- * must construct an Expr using one of the build mechanisms of the
- * Expr package.
- *
- * Increments the reference count. */
- explicit Expr(ExprValue*);
-
- 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. */
- Expr();
-
- Expr(const Expr&);
-
- /** Destructor. Decrements the reference count and, if zero,
- * collects the ExprValue. */
- ~Expr();
-
- bool operator==(const Expr& e) const { return d_ev == e.d_ev; }
- bool operator!=(const Expr& e) const { return d_ev != e.d_ev; }
-
- /**
- * 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;
-
- Expr& operator=(const Expr&);
-
- uint64_t hash() const;
-
- Expr eqExpr(const Expr& right) const;
- Expr notExpr() const;
- Expr negate() const; // avoid double-negatives
- Expr andExpr(const Expr& right) const;
- Expr orExpr(const Expr& right) const;
- Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const;
- Expr iffExpr(const Expr& right) const;
- Expr impExpr(const Expr& right) const;
- Expr xorExpr(const Expr& right) const;
-
- Expr plusExpr(const Expr& right) const;
- Expr uMinusExpr() const;
- Expr multExpr(const Expr& right) const;
-
- inline Kind getKind() const;
-
- inline size_t numChildren() const;
-
- static Expr null() { return s_null; }
-
- typedef Expr* iterator;
- typedef Expr const* const_iterator;
-
- inline iterator begin();
- inline iterator end();
- inline const_iterator begin() const;
- inline const_iterator end() const;
-
- void toString(std::ostream&) const;
-
- bool isNull() const;
-
-};/* class Expr */
-
-}/* CVC4 namespace */
-
-#include "expr/expr_value.h"
-
-namespace CVC4 {
-
-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;
-}
-
-inline Kind Expr::getKind() const {
- return Kind(d_ev->d_kind);
-}
-
-inline void Expr::toString(std::ostream& out) const {
- if(d_ev)
- d_ev->toString(out);
- else out << "null";
-}
-
-inline Expr::iterator Expr::begin() {
- return d_ev->begin();
-}
-
-inline Expr::iterator Expr::end() {
- return d_ev->end();
-}
-
-inline Expr::const_iterator Expr::begin() const {
- return d_ev->begin();
-}
-
-inline Expr::const_iterator Expr::end() const {
- return d_ev->end();
-}
-
-inline size_t Expr::numChildren() const {
- return d_ev->d_nchildren;
-}
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__EXPR_H */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** expr_attribute.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4__EXPR__EXPR_ATTRIBUTE_H
-#define __CVC4__EXPR__EXPR_ATTRIBUTE_H
-
-#include <stdint.h>
-#include "config.h"
-#include "context/context.h"
-#include "expr/expr.h"
-
-namespace CVC4 {
-namespace expr {
-
-template <class value_type>
-class AttrTables;
-
-// global (or TSS)
-extern CDMap<uint64_t> g_hash_bool;
-extern CDMap<uint64_t> g_hash_int;
-extern CDMap<Expr> g_hash_expr;
-extern CDMap<void*> g_hash_ptr;
-
-template <class T>
-class AttrTable;
-
-template <>
-class AttrTable<bool> {
-public:
- class BitAccessor {
- uint64_t& d_word;
- unsigned d_bit;
- public:
- BitAccessor& operator=(bool b);
- // continue...
- };
-
- // bool specialization
- static CDMap<uint64_t> *s_hash;
-
- template <class Attr>
- BitAccessor& find(Expr e, const Attr&);
-
- template <class Attr>
- bool find(Expr e, const Attr&) const;
-};
-
-template <>
-class AttrTable<uint64_t> {
-public:
- // int(egral) specialization
- static CDMap<uint64_t> *s_hash;
- uint64_t& find(Expr);
- uint64_t& find(Expr) const;
-};
-
-template <class T>
-class AttrTable<T*> {
- // pointer specialization
- static CDMap<void*> *s_hash;
-public:
-};
-
-template <>
-class AttrTable<Expr> {
-public:
- // Expr specialization
- static CDMap<Expr> *s_hash;
- Expr find(Expr);
-};
-
-CDMap<uint64_t>* AttrTable<bool>::s_hash = &g_hash_bool;
-CDMap<uint64_t>* AttrTable<uint64_t>::s_hash = &g_hash_int;
-CDMap<Expr>* AttrTable<Expr>::s_hash = &g_hash_expr;
-
-template <class T>
-CDMap<void*>* AttrTable<T*>::s_hash = &g_hash_ptr;
-
-template <class Attr>
-class AttributeTable {
- typedef typename Attr::value_type value_type;
-
- AttrTable<value_type>& d_table;
-
-};
-
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__EXPR__EXPR_ATTRIBUTE_H */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** expr_builder.cpp
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#include "expr_builder.h"
-#include "expr_manager.h"
-#include "expr_value.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(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) {
- d_children.u_arr[0] = e.d_ev->inc();;
-}
-
-ExprBuilder& ExprBuilder::reset(const ExprValue* ev) {
- this->~ExprBuilder();
- d_kind = Kind(ev->d_kind);
- d_used = false;
- d_nchildren = ev->d_nchildren;
- for(Expr::const_iterator i = ev->begin(); i != ev->end(); ++i)
- addChild(i->d_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) {
- Assert( !d_used );
-
- if(d_nchildren > nchild_thresh) {
- 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));
- } else {
- ev_iterator j = d_children.u_arr;
- 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, 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) {
- d_children.u_arr[0] = e.d_ev->inc();
-}
-
-ExprBuilder::~ExprBuilder() {
- if(d_nchildren > nchild_thresh) {
- delete d_children.u_vec;
- } else {
- ev_iterator i = d_children.u_arr;
- ev_iterator i_end = d_children.u_arr + d_nchildren;
- for(; i != i_end ; ++i) {
- (*i)->dec();
- }
- }
-}
-
-// Compound expression constructors
-ExprBuilder& ExprBuilder::eqExpr(const Expr& right) {
- Assert( d_kind != UNDEFINED_KIND );
- if(EXPECT_TRUE( d_kind != EQUAL )) {
- collapse();
- d_kind = EQUAL;
- }
- addChild(right);
- return *this;
-}
-
-ExprBuilder& ExprBuilder::notExpr() {
- Assert( d_kind != UNDEFINED_KIND );
- collapse();
- d_kind = NOT;
- return *this;
-}
-
-// avoid double-negatives
-ExprBuilder& ExprBuilder::negate() {
- if(EXPECT_FALSE( d_kind == NOT ))
- return reset(d_children.u_arr[0]); Assert( d_kind != UNDEFINED_KIND );
- collapse();
- d_kind = NOT;
- return *this;
-}
-
-ExprBuilder& ExprBuilder::andExpr(const Expr& right) {
- Assert( d_kind != UNDEFINED_KIND );
- if(d_kind != AND) {
- collapse();
- d_kind = AND;
- }
- addChild(right);
- return *this;
-}
-
-ExprBuilder& ExprBuilder::orExpr(const Expr& right) {
- Assert( d_kind != UNDEFINED_KIND );
- if(EXPECT_TRUE( d_kind != OR )) {
- collapse();
- d_kind = OR;
- }
- addChild(right);
- return *this;
-}
-
-ExprBuilder& ExprBuilder::iteExpr(const Expr& thenpart, const Expr& elsepart) {
- Assert( d_kind != UNDEFINED_KIND );
- collapse();
- d_kind = ITE;
- addChild(thenpart);
- addChild(elsepart);
- return *this;
-}
-
-ExprBuilder& ExprBuilder::iffExpr(const Expr& right) {
- Assert( d_kind != UNDEFINED_KIND );
- if(EXPECT_TRUE( d_kind != IFF )) {
- collapse();
- d_kind = IFF;
- }
- addChild(right);
- return *this;
-}
-
-ExprBuilder& ExprBuilder::impExpr(const Expr& right) {
- Assert( d_kind != UNDEFINED_KIND );
- collapse();
- d_kind = IMPLIES;
- addChild(right);
- return *this;
-}
-
-ExprBuilder& ExprBuilder::xorExpr(const Expr& right) {
- Assert( d_kind != UNDEFINED_KIND );
- if(EXPECT_TRUE( d_kind != XOR )) {
- collapse();
- d_kind = XOR;
- }
- addChild(right);
- return *this;
-}
-
-// "Stream" expression constructor syntax
-ExprBuilder& ExprBuilder::operator<<(const Kind& op) {
- d_kind = op;
- return *this;
-}
-
-ExprBuilder& ExprBuilder::operator<<(const Expr& child) {
- addChild(child);
- return *this;
-}
-
-/**
- * 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> ();
- v->reserve(nchild_thresh + 5);
- ExprValue** i = d_children.u_arr;
- ExprValue** i_end = i + nchild_thresh;
- for(;i != i_end; ++ i) {
- v->push_back(Expr(*i));
- (*i)->dec();
- }
- v->push_back(Expr(ev));
- 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(Expr(ev));
- // ++d_nchildren; no need for this
- } else {
- 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> ();
- v->reserve(nchild_thresh + 5);
- //
- Unreachable();// unimplemented
- }
- return *this;
-}
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** expr_builder.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4__EXPR_BUILDER_H
-#define __CVC4__EXPR_BUILDER_H
-
-#include <vector>
-#include <cstdlib>
-
-#include "expr_manager.h"
-#include "kind.h"
-#include "util/Assert.h"
-
-namespace CVC4 {
-
-class AndExprBuilder;
-class OrExprBuilder;
-class PlusExprBuilder;
-class MinusExprBuilder;
-class MultExprBuilder;
-
-class ExprBuilder {
- ExprManager* d_em;
-
- Kind d_kind;
-
- // initially false, when you extract the Expr this is set and you can't
- // extract another
- bool d_used;
-
- static const unsigned nchild_thresh = 10;
-
- unsigned d_nchildren;
- union {
- ExprValue* u_arr[nchild_thresh];
- std::vector<Expr>* u_vec;
- } d_children;
-
- void addChild(const Expr& e) { addChild(e.d_ev); }
- void addChild(ExprValue*);
- ExprBuilder& collapse();
-
- typedef ExprValue** ev_iterator;
- typedef ExprValue const** const_ev_iterator;
-
- ev_iterator ev_begin() {
- return d_children.u_arr;
- }
-
- ev_iterator ev_end() {
- return d_children.u_arr + d_nchildren;
- }
-
- ExprBuilder& reset(const ExprValue*);
-
-public:
-
- ExprBuilder();
- ExprBuilder(Kind k);
- ExprBuilder(const Expr&);
- ExprBuilder(const ExprBuilder&);
-
- ExprBuilder(ExprManager*);
- ExprBuilder(ExprManager*, Kind k);
- ExprBuilder(ExprManager*, const Expr&);
- ExprBuilder(ExprManager*, const ExprBuilder&);
-
- ~ExprBuilder();
-
- // Compound expression constructors
- ExprBuilder& eqExpr(const Expr& right);
- ExprBuilder& notExpr();
- ExprBuilder& negate(); // avoid double-negatives
- ExprBuilder& andExpr(const Expr& right);
- ExprBuilder& orExpr(const Expr& right);
- ExprBuilder& iteExpr(const Expr& thenpart, const Expr& elsepart);
- ExprBuilder& iffExpr(const Expr& right);
- ExprBuilder& impExpr(const Expr& right);
- ExprBuilder& xorExpr(const Expr& right);
-
- /* TODO design: these modify ExprBuilder */
- ExprBuilder& operator!() { return notExpr(); }
- ExprBuilder& operator&&(const Expr& right) { return andExpr(right); }
- ExprBuilder& operator||(const Expr& right) { return orExpr(right); }
-
- // "Stream" expression constructor syntax
- ExprBuilder& operator<<(const Kind& op);
- ExprBuilder& operator<<(const Expr& child);
-
- // For pushing sequences of children
- ExprBuilder& append(const std::vector<Expr>& children) { return append(children.begin(), children.end()); }
- ExprBuilder& append(Expr child) { return append(&child, (&child) + 1); }
- template <class Iterator> ExprBuilder& append(const Iterator& begin, const Iterator& end);
-
- operator Expr();// not const
-
- AndExprBuilder operator&&(Expr);
- OrExprBuilder operator||(Expr);
- PlusExprBuilder operator+ (Expr);
- PlusExprBuilder operator- (Expr);
- MultExprBuilder operator* (Expr);
-
- friend class AndExprBuilder;
- friend class OrExprBuilder;
- friend class PlusExprBuilder;
- friend class MultExprBuilder;
-};/* class ExprBuilder */
-
-class AndExprBuilder {
- ExprBuilder d_eb;
-
-public:
-
- AndExprBuilder(const ExprBuilder& eb) : d_eb(eb) {
- if(d_eb.d_kind != AND) {
- d_eb.collapse();
- d_eb.d_kind = AND;
- }
- }
-
- AndExprBuilder& operator&&(Expr);
- OrExprBuilder operator||(Expr);
-
- operator ExprBuilder() { return d_eb; }
-
-};/* class AndExprBuilder */
-
-class OrExprBuilder {
- ExprBuilder d_eb;
-
-public:
-
- OrExprBuilder(const ExprBuilder& eb) : d_eb(eb) {
- if(d_eb.d_kind != OR) {
- d_eb.collapse();
- d_eb.d_kind = OR;
- }
- }
-
- AndExprBuilder operator&&(Expr);
- OrExprBuilder& operator||(Expr);
-
- operator ExprBuilder() { return d_eb; }
-
-};/* class OrExprBuilder */
-
-class PlusExprBuilder {
- ExprBuilder d_eb;
-
-public:
-
- PlusExprBuilder(const ExprBuilder& eb) : d_eb(eb) {
- if(d_eb.d_kind != PLUS) {
- d_eb.collapse();
- d_eb.d_kind = PLUS;
- }
- }
-
- PlusExprBuilder& operator+(Expr);
- PlusExprBuilder& operator-(Expr);
- MultExprBuilder operator*(Expr);
-
- operator ExprBuilder() { return d_eb; }
-
-};/* class PlusExprBuilder */
-
-class MultExprBuilder {
- ExprBuilder d_eb;
-
-public:
-
- MultExprBuilder(const ExprBuilder& eb) : d_eb(eb) {
- if(d_eb.d_kind != MULT) {
- d_eb.collapse();
- d_eb.d_kind = MULT;
- }
- }
-
- PlusExprBuilder operator+(Expr);
- PlusExprBuilder operator-(Expr);
- MultExprBuilder& operator*(Expr);
-
- operator ExprBuilder() { return d_eb; }
-
-};/* class MultExprBuilder */
-
-template <class Iterator>
-inline ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) {
- for(Iterator i = begin; i != end; ++i)
- addChild(*i);
- return *this;
-}
-
-// not const
-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 {
- if(d_nchildren <= nchild_thresh) {
- 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;
- 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 {
- 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;
- for(std::vector<Expr>::iterator i = d_children.u_vec->begin(); i != d_children.u_vec->end(); ++i)
- ev->d_children[nc++] = Expr(*i);
- }
- }
-
- ev->d_nchildren = d_nchildren;
- ev->d_kind = d_kind;
- ev->d_id = ExprValue::next_id++;// FIXME multithreading
- ev->d_rc = 0;
- Expr e(ev);
-
- return d_em->lookup(hash, e);
-}
-
-inline AndExprBuilder ExprBuilder::operator&&(Expr e) {
- return AndExprBuilder(*this) && e;
-}
-
-inline OrExprBuilder ExprBuilder::operator||(Expr e) {
- return OrExprBuilder(*this) || e;
-}
-
-inline PlusExprBuilder ExprBuilder::operator+ (Expr e) {
- return PlusExprBuilder(*this) + e;
-}
-
-inline PlusExprBuilder ExprBuilder::operator- (Expr e) {
- return PlusExprBuilder(*this) - e;
-}
-
-inline MultExprBuilder ExprBuilder::operator* (Expr e) {
- return MultExprBuilder(*this) * e;
-}
-
-inline AndExprBuilder& AndExprBuilder::operator&&(Expr e) {
- d_eb.append(e);
- return *this;
-}
-
-inline OrExprBuilder AndExprBuilder::operator||(Expr e) {
- return OrExprBuilder(d_eb.collapse()) || e;
-}
-
-inline AndExprBuilder OrExprBuilder::operator&&(Expr e) {
- return AndExprBuilder(d_eb.collapse()) && e;
-}
-
-inline OrExprBuilder& OrExprBuilder::operator||(Expr e) {
- d_eb.append(e);
- return *this;
-}
-
-inline PlusExprBuilder& PlusExprBuilder::operator+(Expr e) {
- d_eb.append(e);
- return *this;
-}
-
-inline PlusExprBuilder& PlusExprBuilder::operator-(Expr e) {
- d_eb.append(e.negate());
- return *this;
-}
-
-inline MultExprBuilder PlusExprBuilder::operator*(Expr e) {
- return MultExprBuilder(d_eb.collapse()) * e;
-}
-
-inline PlusExprBuilder MultExprBuilder::operator+(Expr e) {
- return MultExprBuilder(d_eb.collapse()) + e;
-}
-
-inline PlusExprBuilder MultExprBuilder::operator-(Expr e) {
- return MultExprBuilder(d_eb.collapse()) - e;
-}
-
-inline MultExprBuilder& MultExprBuilder::operator*(Expr e) {
- d_eb.append(e);
- return *this;
-}
-
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__EXPR_BUILDER_H */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** expr_manager.cpp
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- ** Expression manager implementation.
- **/
-
-#include "expr_builder.h"
-#include "expr_manager.h"
-#include "expr/expr.h"
-
-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
- std::vector<Expr> v;
- v.push_back(e);
- d_hash.insert(std::make_pair(hash, v));
- return e;
- } else {
- for(std::vector<Expr>::iterator j = i->second.begin(); j != i->second.end(); ++j) {
- if(e.getKind() != j->getKind())
- continue;
-
- if(e.numChildren() != j->numChildren())
- continue;
-
- 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)
- break;
- }
-
- if(c1 != e.end() || c2 != j->end())
- continue;
-
- return *j;
- }
- // didn't find it, insert
- std::vector<Expr> v;
- v.push_back(e);
- d_hash.insert(std::make_pair(hash, v));
- return e;
- }
-}
-
-// general expression-builders
-
-Expr ExprManager::mkExpr(Kind kind) {
- return ExprBuilder(this, kind);
-}
-
-Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
- return ExprBuilder(this, kind) << child1;
-}
-
-Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
- return ExprBuilder(this, kind) << child1 << child2;
-}
-
-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, 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, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4, const Expr& child5) {
- return ExprBuilder(this, kind) << child1 << child2 << child3 << child4 << child5;
-}
-
-// N-ary version
-Expr ExprManager::mkExpr(Kind kind, std::vector<Expr> children) {
- return ExprBuilder(this, kind).append(children);
-}
-
-Expr ExprManager::mkVar() {
- return ExprBuilder(this, VARIABLE);
-}
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** expr_manager.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4__EXPR_MANAGER_H
-#define __CVC4__EXPR_MANAGER_H
-
-#include <vector>
-#include <map>
-
-#include "expr/expr.h"
-#include "kind.h"
-
-namespace CVC4 {
-
-namespace expr {
- class ExprBuilder;
-}/* CVC4::expr namespace */
-
-class CVC4_PUBLIC ExprManager {
- static __thread ExprManager* s_current;
-
- friend class CVC4::ExprBuilder;
-
- typedef std::map<uint64_t, std::vector<Expr> > hash_t;
- hash_t d_hash;
-
- Expr lookup(uint64_t hash, const Expr& e);
-
-public:
- static ExprManager* currentEM() { return s_current; }
-
- // general expression-builders
- Expr mkExpr(Kind kind);
- 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);
-
- // variables are special, because duplicates are permitted
- Expr mkVar();
-
- // TODO: these use the current EM (but must be renamed)
- /*
- static Expr mkExpr(Kind kind)
- { currentEM()->mkExpr(kind); }
- static Expr mkExpr(Kind kind, Expr child1);
- { currentEM()->mkExpr(kind, child1); }
- static Expr mkExpr(Kind kind, Expr child1, Expr child2);
- { currentEM()->mkExpr(kind, child1, child2); }
- static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3);
- { currentEM()->mkExpr(kind, child1, child2, child3); }
- static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
- { currentEM()->mkExpr(kind, child1, child2, child3, child4); }
- static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5);
- { currentEM()->mkExpr(kind, child1, child2, child3, child4, child5); }
- */
-
- // do we want a varargs one? perhaps not..
-};
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__EXPR_MANAGER_H */
** An expression node.
**
** Instances of this class are generally referenced through
- ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the
+ ** cvc4::Node rather than by pointer; cvc4::Node maintains the
** reference count on ExprValue instances and
**/
** An expression node.
**
** Instances of this class are generally referenced through
- ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the
+ ** cvc4::Node rather than by pointer; cvc4::Node maintains the
** reference count on ExprValue instances and
**/
/* this must be above the check for __CVC4__EXPR__EXPR_VALUE_H */
/* to resolve a circular dependency */
-#include "expr/expr.h"
+#include "expr/node.h"
#ifndef __CVC4__EXPR__EXPR_VALUE_H
#define __CVC4__EXPR__EXPR_VALUE_H
namespace CVC4 {
-class Expr;
-class ExprBuilder;
+class Node;
+class NodeBuilder;
namespace expr {
/** The ID (0 is reserved for the null value) */
unsigned d_id : 32;
- /** The expression's reference count. @see cvc4::Expr. */
+ /** The expression's reference count. @see cvc4::Node. */
unsigned d_rc : 8;
/** Kind of the expression */
unsigned d_nchildren : 16;
/** Variable number of child nodes */
- Expr d_children[0];
+ Node d_children[0];
// todo add exprMgr ref in debug case
- friend class CVC4::Expr;
- friend class CVC4::ExprBuilder;
+ friend class CVC4::Node;
+ friend class CVC4::NodeBuilder;
ExprValue* inc();
ExprValue* dec();
/**
* 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
+ * root hash. The iterator should be either over a range of Node or pointers
* to ExprValue.
* @param hash the initial value for the hash
* @param begin the begining of the range
// Iterator support
- typedef Expr* iterator;
- typedef Expr const* const_iterator;
+ typedef Node* iterator;
+ typedef Node const* const_iterator;
iterator begin();
iterator end();
--- /dev/null
+/********************* -*- C++ -*- */
+/** expr.cpp
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ ** Reference-counted encapsulation of a pointer to an expression.
+ **/
+
+#include "expr/node.h"
+#include "expr/expr_value.h"
+#include "expr/node_builder.h"
+#include "util/Assert.h"
+
+using namespace CVC4::expr;
+
+namespace CVC4 {
+
+ExprValue ExprValue::s_null;
+
+Node Node::s_null(&ExprValue::s_null);
+
+bool Node::isNull() const {
+ return d_ev == &ExprValue::s_null;
+}
+
+Node::Node() :
+ d_ev(&ExprValue::s_null) {
+ // No refcount needed
+}
+
+Node::Node(ExprValue* ev)
+ : d_ev(ev) {
+ Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
+ d_ev->inc();
+}
+
+Node::Node(const Node& e) {
+ Assert(e.d_ev != NULL, "Expecting a non-NULL expression value!");
+ d_ev = e.d_ev;
+ d_ev->inc();
+}
+
+Node::~Node() {
+ Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
+ d_ev->dec();
+}
+
+void Node::assignExprValue(ExprValue* ev) {
+ d_ev = ev;
+ d_ev->inc();
+}
+
+Node& Node::operator=(const Node& e) {
+ Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
+ if(this != &e && d_ev != e.d_ev) {
+ d_ev->dec();
+ d_ev = e.d_ev;
+ d_ev->inc();
+ }
+ return *this;
+}
+
+ExprValue const* Node::operator->() const {
+ Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
+ return d_ev;
+}
+
+uint64_t Node::hash() const {
+ Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
+ return d_ev->hash();
+}
+
+Node Node::eqExpr(const Node& right) const {
+ return NodeManager::currentEM()->mkExpr(EQUAL, *this, right);
+}
+
+Node Node::notExpr() const {
+ return NodeManager::currentEM()->mkExpr(NOT, *this);
+}
+
+// FIXME: What does this do and why?
+Node Node::negate() const { // avoid double-negatives
+ return NodeBuilder(*this).negate();
+}
+
+
+Node Node::andExpr(const Node& right) const {
+ return NodeManager::currentEM()->mkExpr(AND, *this, right);
+}
+
+Node Node::orExpr(const Node& right) const {
+ return NodeManager::currentEM()->mkExpr(OR, *this, right);
+}
+
+Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const {
+ return NodeManager::currentEM()->mkExpr(ITE, *this, thenpart, elsepart);
+}
+
+Node Node::iffExpr(const Node& right) const {
+ return NodeManager::currentEM()->mkExpr(IFF, *this, right);
+}
+
+Node Node::impExpr(const Node& right) const {
+ return NodeManager::currentEM()->mkExpr(IMPLIES, *this, right);
+}
+
+Node Node::xorExpr(const Node& right) const {
+ return NodeManager::currentEM()->mkExpr(XOR, *this, right);
+}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* -*- C++ -*- */
+/** cvc4_expr.h
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ ** Reference-counted encapsulation of a pointer to an expression.
+ **/
+
+#ifndef __CVC4__EXPR_H
+#define __CVC4__EXPR_H
+
+#include <vector>
+#include <iostream>
+#include <stdint.h>
+
+#include "cvc4_config.h"
+#include "expr/kind.h"
+
+namespace CVC4 {
+ class Node;
+}/* CVC4 namespace */
+
+namespace CVC4 {
+
+inline std::ostream& operator<<(std::ostream&, const Node&) CVC4_PUBLIC;
+
+class NodeManager;
+
+namespace expr {
+ class ExprValue;
+}/* CVC4::expr namespace */
+
+using CVC4::expr::ExprValue;
+
+/**
+ * Encapsulation of an ExprValue pointer. The reference count is
+ * maintained in the ExprValue.
+ */
+class CVC4_PUBLIC Node {
+
+ friend class ExprValue;
+
+ /** A convenient null-valued encapsulated pointer */
+ static Node s_null;
+
+ /** The referenced ExprValue */
+ ExprValue* d_ev;
+
+ /** This constructor is reserved for use by the Node package; one
+ * must construct an Node using one of the build mechanisms of the
+ * Node package.
+ *
+ * Increments the reference count. */
+ explicit Node(ExprValue*);
+
+ friend class NodeBuilder;
+ friend class NodeManager;
+
+ /** 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. */
+ Node();
+
+ Node(const Node&);
+
+ /** Destructor. Decrements the reference count and, if zero,
+ * collects the ExprValue. */
+ ~Node();
+
+ bool operator==(const Node& e) const { return d_ev == e.d_ev; }
+ bool operator!=(const Node& e) const { return d_ev != e.d_ev; }
+
+ /**
+ * 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 Node& e) const;
+
+ Node& operator=(const Node&);
+
+ uint64_t hash() const;
+
+ Node eqExpr(const Node& right) const;
+ Node notExpr() const;
+ Node negate() const; // avoid double-negatives
+ Node andExpr(const Node& right) const;
+ Node orExpr(const Node& right) const;
+ Node iteExpr(const Node& thenpart, const Node& elsepart) const;
+ Node iffExpr(const Node& right) const;
+ Node impExpr(const Node& right) const;
+ Node xorExpr(const Node& right) const;
+
+ Node plusExpr(const Node& right) const;
+ Node uMinusExpr() const;
+ Node multExpr(const Node& right) const;
+
+ inline Kind getKind() const;
+
+ inline size_t numChildren() const;
+
+ static Node null() { return s_null; }
+
+ typedef Node* iterator;
+ typedef Node const* const_iterator;
+
+ inline iterator begin();
+ inline iterator end();
+ inline const_iterator begin() const;
+ inline const_iterator end() const;
+
+ void toString(std::ostream&) const;
+
+ bool isNull() const;
+
+};/* class Node */
+
+}/* CVC4 namespace */
+
+#include "expr/expr_value.h"
+
+namespace CVC4 {
+
+inline bool Node::operator<(const Node& e) const {
+ return d_ev->d_id < e.d_ev->d_id;
+}
+
+inline std::ostream& operator<<(std::ostream& out, const Node& e) {
+ e.toString(out);
+ return out;
+}
+
+inline Kind Node::getKind() const {
+ return Kind(d_ev->d_kind);
+}
+
+inline void Node::toString(std::ostream& out) const {
+ if(d_ev)
+ d_ev->toString(out);
+ else out << "null";
+}
+
+inline Node::iterator Node::begin() {
+ return d_ev->begin();
+}
+
+inline Node::iterator Node::end() {
+ return d_ev->end();
+}
+
+inline Node::const_iterator Node::begin() const {
+ return d_ev->begin();
+}
+
+inline Node::const_iterator Node::end() const {
+ return d_ev->end();
+}
+
+inline size_t Node::numChildren() const {
+ return d_ev->d_nchildren;
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** expr_attribute.h
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ **/
+
+#ifndef __CVC4__EXPR__EXPR_ATTRIBUTE_H
+#define __CVC4__EXPR__EXPR_ATTRIBUTE_H
+
+#include <stdint.h>
+#include "config.h"
+#include "context/context.h"
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace expr {
+
+template <class value_type>
+class AttrTables;
+
+// global (or TSS)
+extern CDMap<uint64_t> g_hash_bool;
+extern CDMap<uint64_t> g_hash_int;
+extern CDMap<Node> g_hash_expr;
+extern CDMap<void*> g_hash_ptr;
+
+template <class T>
+class AttrTable;
+
+template <>
+class AttrTable<bool> {
+public:
+ class BitAccessor {
+ uint64_t& d_word;
+ unsigned d_bit;
+ public:
+ BitAccessor& operator=(bool b);
+ // continue...
+ };
+
+ // bool specialization
+ static CDMap<uint64_t> *s_hash;
+
+ template <class Attr>
+ BitAccessor& find(Node e, const Attr&);
+
+ template <class Attr>
+ bool find(Node e, const Attr&) const;
+};
+
+template <>
+class AttrTable<uint64_t> {
+public:
+ // int(egral) specialization
+ static CDMap<uint64_t> *s_hash;
+ uint64_t& find(Node);
+ uint64_t& find(Node) const;
+};
+
+template <class T>
+class AttrTable<T*> {
+ // pointer specialization
+ static CDMap<void*> *s_hash;
+public:
+};
+
+template <>
+class AttrTable<Node> {
+public:
+ // Node specialization
+ static CDMap<Node> *s_hash;
+ Node find(Node);
+};
+
+CDMap<uint64_t>* AttrTable<bool>::s_hash = &g_hash_bool;
+CDMap<uint64_t>* AttrTable<uint64_t>::s_hash = &g_hash_int;
+CDMap<Node>* AttrTable<Node>::s_hash = &g_hash_expr;
+
+template <class T>
+CDMap<void*>* AttrTable<T*>::s_hash = &g_hash_ptr;
+
+template <class Attr>
+class AttributeTable {
+ typedef typename Attr::value_type value_type;
+
+ AttrTable<value_type>& d_table;
+
+};
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR__EXPR_ATTRIBUTE_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** expr_builder.cpp
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ **/
+
+#include "expr/node_builder.h"
+#include "expr/node_manager.h"
+#include "expr/expr_value.h"
+#include "util/output.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+NodeBuilder::NodeBuilder() :
+ d_em(NodeManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false),
+ d_nchildren(0) {
+}
+
+NodeBuilder::NodeBuilder(Kind k) :
+ d_em(NodeManager::currentEM()), d_kind(k), d_used(false), d_nchildren(0) {
+}
+
+NodeBuilder::NodeBuilder(const Node& e) :
+ d_em(NodeManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) {
+ d_children.u_arr[0] = e.d_ev->inc();;
+}
+
+NodeBuilder& NodeBuilder::reset(const ExprValue* ev) {
+ this->~NodeBuilder();
+ d_kind = Kind(ev->d_kind);
+ d_used = false;
+ d_nchildren = ev->d_nchildren;
+ for(Node::const_iterator i = ev->begin(); i != ev->end(); ++i)
+ addChild(i->d_ev);
+ return *this;
+}
+
+NodeBuilder::NodeBuilder(const NodeBuilder& 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<Node> ();
+ 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));
+ } else {
+ ev_iterator j = d_children.u_arr;
+ 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();
+ }
+}
+
+NodeBuilder::NodeBuilder(NodeManager* em) :
+ d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(0) {
+}
+
+NodeBuilder::NodeBuilder(NodeManager* em, Kind k) :
+ d_em(em), d_kind(k), d_used(false), d_nchildren(0) {
+}
+
+NodeBuilder::NodeBuilder(NodeManager* em, const Node& e) :
+ d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) {
+ d_children.u_arr[0] = e.d_ev->inc();
+}
+
+NodeBuilder::~NodeBuilder() {
+ if(d_nchildren > nchild_thresh) {
+ delete d_children.u_vec;
+ } else {
+ ev_iterator i = d_children.u_arr;
+ ev_iterator i_end = d_children.u_arr + d_nchildren;
+ for(; i != i_end ; ++i) {
+ (*i)->dec();
+ }
+ }
+}
+
+// Compound expression constructors
+NodeBuilder& NodeBuilder::eqExpr(const Node& right) {
+ Assert( d_kind != UNDEFINED_KIND );
+ if(EXPECT_TRUE( d_kind != EQUAL )) {
+ collapse();
+ d_kind = EQUAL;
+ }
+ addChild(right);
+ return *this;
+}
+
+NodeBuilder& NodeBuilder::notExpr() {
+ Assert( d_kind != UNDEFINED_KIND );
+ collapse();
+ d_kind = NOT;
+ return *this;
+}
+
+// avoid double-negatives
+NodeBuilder& NodeBuilder::negate() {
+ if(EXPECT_FALSE( d_kind == NOT ))
+ return reset(d_children.u_arr[0]); Assert( d_kind != UNDEFINED_KIND );
+ collapse();
+ d_kind = NOT;
+ return *this;
+}
+
+NodeBuilder& NodeBuilder::andExpr(const Node& right) {
+ Assert( d_kind != UNDEFINED_KIND );
+ if(d_kind != AND) {
+ collapse();
+ d_kind = AND;
+ }
+ addChild(right);
+ return *this;
+}
+
+NodeBuilder& NodeBuilder::orExpr(const Node& right) {
+ Assert( d_kind != UNDEFINED_KIND );
+ if(EXPECT_TRUE( d_kind != OR )) {
+ collapse();
+ d_kind = OR;
+ }
+ addChild(right);
+ return *this;
+}
+
+NodeBuilder& NodeBuilder::iteExpr(const Node& thenpart, const Node& elsepart) {
+ Assert( d_kind != UNDEFINED_KIND );
+ collapse();
+ d_kind = ITE;
+ addChild(thenpart);
+ addChild(elsepart);
+ return *this;
+}
+
+NodeBuilder& NodeBuilder::iffExpr(const Node& right) {
+ Assert( d_kind != UNDEFINED_KIND );
+ if(EXPECT_TRUE( d_kind != IFF )) {
+ collapse();
+ d_kind = IFF;
+ }
+ addChild(right);
+ return *this;
+}
+
+NodeBuilder& NodeBuilder::impExpr(const Node& right) {
+ Assert( d_kind != UNDEFINED_KIND );
+ collapse();
+ d_kind = IMPLIES;
+ addChild(right);
+ return *this;
+}
+
+NodeBuilder& NodeBuilder::xorExpr(const Node& right) {
+ Assert( d_kind != UNDEFINED_KIND );
+ if(EXPECT_TRUE( d_kind != XOR )) {
+ collapse();
+ d_kind = XOR;
+ }
+ addChild(right);
+ return *this;
+}
+
+// "Stream" expression constructor syntax
+NodeBuilder& NodeBuilder::operator<<(const Kind& op) {
+ d_kind = op;
+ return *this;
+}
+
+NodeBuilder& NodeBuilder::operator<<(const Node& child) {
+ addChild(child);
+ return *this;
+}
+
+/**
+ * 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 NodeBuilder::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<Node>* v = new vector<Node> ();
+ v->reserve(nchild_thresh + 5);
+ ExprValue** i = d_children.u_arr;
+ ExprValue** i_end = i + nchild_thresh;
+ for(;i != i_end; ++ i) {
+ v->push_back(Node(*i));
+ (*i)->dec();
+ }
+ v->push_back(Node(ev));
+ 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(Node(ev));
+ // ++d_nchildren; no need for this
+ } else {
+ Debug("expr") << "under thresh " << d_nchildren
+ << " < " << nchild_thresh << endl;
+ d_children.u_arr[d_nchildren ++] = ev->inc();
+ }
+}
+
+NodeBuilder& NodeBuilder::collapse() {
+ if(d_nchildren == nchild_thresh) {
+ vector<Node>* v = new vector<Node> ();
+ v->reserve(nchild_thresh + 5);
+ //
+ Unreachable();// unimplemented
+ }
+ return *this;
+}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* -*- C++ -*- */
+/** expr_builder.h
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ **/
+
+#ifndef __CVC4__EXPR_BUILDER_H
+#define __CVC4__EXPR_BUILDER_H
+
+#include <vector>
+#include <cstdlib>
+
+#include "expr/node_manager.h"
+#include "expr/kind.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+
+class AndExprBuilder;
+class OrExprBuilder;
+class PlusExprBuilder;
+class MinusExprBuilder;
+class MultExprBuilder;
+
+class NodeBuilder {
+ NodeManager* d_em;
+
+ Kind d_kind;
+
+ // initially false, when you extract the Node this is set and you can't
+ // extract another
+ bool d_used;
+
+ static const unsigned nchild_thresh = 10;
+
+ unsigned d_nchildren;
+ union {
+ ExprValue* u_arr[nchild_thresh];
+ std::vector<Node>* u_vec;
+ } d_children;
+
+ void addChild(const Node& e) { addChild(e.d_ev); }
+ void addChild(ExprValue*);
+ NodeBuilder& collapse();
+
+ typedef ExprValue** ev_iterator;
+ typedef ExprValue const** const_ev_iterator;
+
+ ev_iterator ev_begin() {
+ return d_children.u_arr;
+ }
+
+ ev_iterator ev_end() {
+ return d_children.u_arr + d_nchildren;
+ }
+
+ NodeBuilder& reset(const ExprValue*);
+
+public:
+
+ NodeBuilder();
+ NodeBuilder(Kind k);
+ NodeBuilder(const Node&);
+ NodeBuilder(const NodeBuilder&);
+
+ NodeBuilder(NodeManager*);
+ NodeBuilder(NodeManager*, Kind k);
+ NodeBuilder(NodeManager*, const Node&);
+ NodeBuilder(NodeManager*, const NodeBuilder&);
+
+ ~NodeBuilder();
+
+ // Compound expression constructors
+ NodeBuilder& eqExpr(const Node& right);
+ NodeBuilder& notExpr();
+ NodeBuilder& negate(); // avoid double-negatives
+ NodeBuilder& andExpr(const Node& right);
+ NodeBuilder& orExpr(const Node& right);
+ NodeBuilder& iteExpr(const Node& thenpart, const Node& elsepart);
+ NodeBuilder& iffExpr(const Node& right);
+ NodeBuilder& impExpr(const Node& right);
+ NodeBuilder& xorExpr(const Node& right);
+
+ /* TODO design: these modify NodeBuilder */
+ NodeBuilder& operator!() { return notExpr(); }
+ NodeBuilder& operator&&(const Node& right) { return andExpr(right); }
+ NodeBuilder& operator||(const Node& right) { return orExpr(right); }
+
+ // "Stream" expression constructor syntax
+ NodeBuilder& operator<<(const Kind& op);
+ NodeBuilder& operator<<(const Node& child);
+
+ // For pushing sequences of children
+ NodeBuilder& append(const std::vector<Node>& children) { return append(children.begin(), children.end()); }
+ NodeBuilder& append(Node child) { return append(&child, (&child) + 1); }
+ template <class Iterator> NodeBuilder& append(const Iterator& begin, const Iterator& end);
+
+ operator Node();// not const
+
+ AndExprBuilder operator&&(Node);
+ OrExprBuilder operator||(Node);
+ PlusExprBuilder operator+ (Node);
+ PlusExprBuilder operator- (Node);
+ MultExprBuilder operator* (Node);
+
+ friend class AndExprBuilder;
+ friend class OrExprBuilder;
+ friend class PlusExprBuilder;
+ friend class MultExprBuilder;
+};/* class NodeBuilder */
+
+class AndExprBuilder {
+ NodeBuilder d_eb;
+
+public:
+
+ AndExprBuilder(const NodeBuilder& eb) : d_eb(eb) {
+ if(d_eb.d_kind != AND) {
+ d_eb.collapse();
+ d_eb.d_kind = AND;
+ }
+ }
+
+ AndExprBuilder& operator&&(Node);
+ OrExprBuilder operator||(Node);
+
+ operator NodeBuilder() { return d_eb; }
+
+};/* class AndExprBuilder */
+
+class OrExprBuilder {
+ NodeBuilder d_eb;
+
+public:
+
+ OrExprBuilder(const NodeBuilder& eb) : d_eb(eb) {
+ if(d_eb.d_kind != OR) {
+ d_eb.collapse();
+ d_eb.d_kind = OR;
+ }
+ }
+
+ AndExprBuilder operator&&(Node);
+ OrExprBuilder& operator||(Node);
+
+ operator NodeBuilder() { return d_eb; }
+
+};/* class OrExprBuilder */
+
+class PlusExprBuilder {
+ NodeBuilder d_eb;
+
+public:
+
+ PlusExprBuilder(const NodeBuilder& eb) : d_eb(eb) {
+ if(d_eb.d_kind != PLUS) {
+ d_eb.collapse();
+ d_eb.d_kind = PLUS;
+ }
+ }
+
+ PlusExprBuilder& operator+(Node);
+ PlusExprBuilder& operator-(Node);
+ MultExprBuilder operator*(Node);
+
+ operator NodeBuilder() { return d_eb; }
+
+};/* class PlusExprBuilder */
+
+class MultExprBuilder {
+ NodeBuilder d_eb;
+
+public:
+
+ MultExprBuilder(const NodeBuilder& eb) : d_eb(eb) {
+ if(d_eb.d_kind != MULT) {
+ d_eb.collapse();
+ d_eb.d_kind = MULT;
+ }
+ }
+
+ PlusExprBuilder operator+(Node);
+ PlusExprBuilder operator-(Node);
+ MultExprBuilder& operator*(Node);
+
+ operator NodeBuilder() { return d_eb; }
+
+};/* class MultExprBuilder */
+
+template <class Iterator>
+inline NodeBuilder& NodeBuilder::append(const Iterator& begin, const Iterator& end) {
+ for(Iterator i = begin; i != end; ++i)
+ addChild(*i);
+ return *this;
+}
+
+// not const
+inline NodeBuilder::operator Node() {
+ 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 {
+ if(d_nchildren <= nchild_thresh) {
+ hash = ExprValue::computeHash<ev_iterator>(d_kind, ev_begin(), ev_end());
+ void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Node));
+ ev = new (space) ExprValue;
+ size_t nc = 0;
+ 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 {
+ hash = ExprValue::computeHash<std::vector<Node>::const_iterator>(d_kind, d_children.u_vec->begin(), d_children.u_vec->end());
+ void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Node));
+ ev = new (space) ExprValue;
+ size_t nc = 0;
+ for(std::vector<Node>::iterator i = d_children.u_vec->begin(); i != d_children.u_vec->end(); ++i)
+ ev->d_children[nc++] = Node(*i);
+ }
+ }
+
+ ev->d_nchildren = d_nchildren;
+ ev->d_kind = d_kind;
+ ev->d_id = ExprValue::next_id++;// FIXME multithreading
+ ev->d_rc = 0;
+ Node e(ev);
+
+ return d_em->lookup(hash, e);
+}
+
+inline AndExprBuilder NodeBuilder::operator&&(Node e) {
+ return AndExprBuilder(*this) && e;
+}
+
+inline OrExprBuilder NodeBuilder::operator||(Node e) {
+ return OrExprBuilder(*this) || e;
+}
+
+inline PlusExprBuilder NodeBuilder::operator+ (Node e) {
+ return PlusExprBuilder(*this) + e;
+}
+
+inline PlusExprBuilder NodeBuilder::operator- (Node e) {
+ return PlusExprBuilder(*this) - e;
+}
+
+inline MultExprBuilder NodeBuilder::operator* (Node e) {
+ return MultExprBuilder(*this) * e;
+}
+
+inline AndExprBuilder& AndExprBuilder::operator&&(Node e) {
+ d_eb.append(e);
+ return *this;
+}
+
+inline OrExprBuilder AndExprBuilder::operator||(Node e) {
+ return OrExprBuilder(d_eb.collapse()) || e;
+}
+
+inline AndExprBuilder OrExprBuilder::operator&&(Node e) {
+ return AndExprBuilder(d_eb.collapse()) && e;
+}
+
+inline OrExprBuilder& OrExprBuilder::operator||(Node e) {
+ d_eb.append(e);
+ return *this;
+}
+
+inline PlusExprBuilder& PlusExprBuilder::operator+(Node e) {
+ d_eb.append(e);
+ return *this;
+}
+
+inline PlusExprBuilder& PlusExprBuilder::operator-(Node e) {
+ d_eb.append(e.negate());
+ return *this;
+}
+
+inline MultExprBuilder PlusExprBuilder::operator*(Node e) {
+ return MultExprBuilder(d_eb.collapse()) * e;
+}
+
+inline PlusExprBuilder MultExprBuilder::operator+(Node e) {
+ return MultExprBuilder(d_eb.collapse()) + e;
+}
+
+inline PlusExprBuilder MultExprBuilder::operator-(Node e) {
+ return MultExprBuilder(d_eb.collapse()) - e;
+}
+
+inline MultExprBuilder& MultExprBuilder::operator*(Node e) {
+ d_eb.append(e);
+ return *this;
+}
+
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR_BUILDER_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** expr_manager.cpp
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ ** Expression manager implementation.
+ **/
+
+#include "node_builder.h"
+#include "node_manager.h"
+#include "expr/node.h"
+
+namespace CVC4 {
+
+__thread NodeManager* NodeManager::s_current = 0;
+
+Node NodeManager::lookup(uint64_t hash, const Node& 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
+ std::vector<Node> v;
+ v.push_back(e);
+ d_hash.insert(std::make_pair(hash, v));
+ return e;
+ } else {
+ for(std::vector<Node>::iterator j = i->second.begin(); j != i->second.end(); ++j) {
+ if(e.getKind() != j->getKind())
+ continue;
+
+ if(e.numChildren() != j->numChildren())
+ continue;
+
+ Node::const_iterator c1 = e.begin();
+ Node::iterator c2 = j->begin();
+ for(; c1 != e.end() && c2 != j->end(); ++c1, ++c2) {
+ if(c1->d_ev != c2->d_ev)
+ break;
+ }
+
+ if(c1 != e.end() || c2 != j->end())
+ continue;
+
+ return *j;
+ }
+ // didn't find it, insert
+ std::vector<Node> v;
+ v.push_back(e);
+ d_hash.insert(std::make_pair(hash, v));
+ return e;
+ }
+}
+
+// general expression-builders
+
+Node NodeManager::mkExpr(Kind kind) {
+ return NodeBuilder(this, kind);
+}
+
+Node NodeManager::mkExpr(Kind kind, const Node& child1) {
+ return NodeBuilder(this, kind) << child1;
+}
+
+Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2) {
+ return NodeBuilder(this, kind) << child1 << child2;
+}
+
+Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3) {
+ return NodeBuilder(this, kind) << child1 << child2 << child3;
+}
+
+Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4) {
+ return NodeBuilder(this, kind) << child1 << child2 << child3 << child4;
+}
+
+Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5) {
+ return NodeBuilder(this, kind) << child1 << child2 << child3 << child4 << child5;
+}
+
+// N-ary version
+Node NodeManager::mkExpr(Kind kind, std::vector<Node> children) {
+ return NodeBuilder(this, kind).append(children);
+}
+
+Node NodeManager::mkVar() {
+ return NodeBuilder(this, VARIABLE);
+}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* -*- C++ -*- */
+/** expr_manager.h
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ **/
+
+#ifndef __CVC4__EXPR_MANAGER_H
+#define __CVC4__EXPR_MANAGER_H
+
+#include <vector>
+#include <map>
+
+#include "node.h"
+#include "kind.h"
+
+namespace CVC4 {
+
+namespace expr {
+ class ExprBuilder;
+}/* CVC4::expr namespace */
+
+class CVC4_PUBLIC NodeManager {
+ static __thread NodeManager* s_current;
+
+ friend class CVC4::NodeBuilder;
+
+ typedef std::map<uint64_t, std::vector<Node> > hash_t;
+ hash_t d_hash;
+
+ Node lookup(uint64_t hash, const Node& e);
+
+public:
+ static NodeManager* currentEM() { return s_current; }
+
+ // general expression-builders
+ Node mkExpr(Kind kind);
+ Node mkExpr(Kind kind, const Node& child1);
+ Node mkExpr(Kind kind, const Node& child1, const Node& child2);
+ Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3);
+ Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4);
+ Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5);
+ // N-ary version
+ Node mkExpr(Kind kind, std::vector<Node> children);
+
+ // variables are special, because duplicates are permitted
+ Node mkVar();
+
+ // TODO: these use the current EM (but must be renamed)
+ /*
+ static Node mkExpr(Kind kind)
+ { currentEM()->mkExpr(kind); }
+ static Node mkExpr(Kind kind, Node child1);
+ { currentEM()->mkExpr(kind, child1); }
+ static Node mkExpr(Kind kind, Node child1, Node child2);
+ { currentEM()->mkExpr(kind, child1, child2); }
+ static Node mkExpr(Kind kind, Node child1, Node child2, Node child3);
+ { currentEM()->mkExpr(kind, child1, child2, child3); }
+ static Node mkExpr(Kind kind, Node child1, Node child2, Node child3, Node child4);
+ { currentEM()->mkExpr(kind, child1, child2, child3, child4); }
+ static Node mkExpr(Kind kind, Node child1, Node child2, Node child3, Node child4, Node child5);
+ { currentEM()->mkExpr(kind, child1, child2, child3, child4, child5); }
+ */
+
+ // do we want a varargs one? perhaps not..
+};
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR_MANAGER_H */
#include "parser/parser.h"
#include "parser/smt/smt_parser.h"
#include "parser/cvc/cvc_parser.h"
-#include "expr/expr_manager.h"
+#include "expr/node_manager.h"
#include "smt/smt_engine.h"
#include "util/command.h"
#include "util/output.h"
throw new Exception("Too many input files specified.");
// Create the expression manager
- ExprManager exprMgr;
+ NodeManager exprMgr;
// Create the SmtEngine
SmtEngine smt(&exprMgr, &options);
#include <iostream>
#include "antlr_parser.h"
-#include "expr/expr_manager.h"
#include "util/output.h"
using namespace std;
antlr::LLkParser(lexer, k) {
}
-Expr AntlrParser::getVariable(std::string var_name) {
- Expr e = d_var_symbol_table.getObject(var_name);
+Node AntlrParser::getVariable(std::string var_name) {
+ Node e = d_var_symbol_table.getObject(var_name);
Debug("parser") << "getvar " << var_name << " gives " << e << endl;
return e;
}
-Expr AntlrParser::getTrueExpr() const {
+Node AntlrParser::getTrueExpr() const {
return d_expr_manager->mkExpr(TRUE);
}
-Expr AntlrParser::getFalseExpr() const {
+Node AntlrParser::getFalseExpr() const {
return d_expr_manager->mkExpr(FALSE);
}
-Expr AntlrParser::newExpression(Kind kind, const Expr& child) {
+Node AntlrParser::newExpression(Kind kind, const Node& child) {
return d_expr_manager->mkExpr(kind, child);
}
-Expr AntlrParser::newExpression(Kind kind, const Expr& child_1, const Expr& child_2) {
+Node AntlrParser::newExpression(Kind kind, const Node& child_1, const Node& child_2) {
return d_expr_manager->mkExpr(kind, child_1, child_2);
}
-Expr AntlrParser::newExpression(Kind kind, const std::vector<Expr>& children) {
+Node AntlrParser::newExpression(Kind kind, const std::vector<Node>& children) {
return d_expr_manager->mkExpr(kind, children);
}
void AntlrParser::addExtraSorts(const std::vector<std::string>& extra_sorts) {
}
-void AntlrParser::setExpressionManager(ExprManager* em) {
+void AntlrParser::setExpressionManager(NodeManager* em) {
d_expr_manager = em;
}
LT(0).get()->getColumn());
}
-Expr AntlrParser::createPrecedenceExpr(const vector<Expr>& exprs, const vector<
+Node AntlrParser::createPrecedenceExpr(const vector<Node>& exprs, const vector<
Kind>& kinds) {
return createPrecedenceExpr(exprs, kinds, 0, exprs.size() - 1);
}
return pivot;
}
-Expr AntlrParser::createPrecedenceExpr(const std::vector<Expr>& exprs,
+Node AntlrParser::createPrecedenceExpr(const std::vector<Node>& exprs,
const std::vector<Kind>& kinds,
unsigned start_index, unsigned end_index) {
if(start_index == end_index)
unsigned pivot = findPivot(kinds, start_index, end_index - 1);
- Expr child_1 = createPrecedenceExpr(exprs, kinds, start_index, pivot);
- Expr child_2 = createPrecedenceExpr(exprs, kinds, pivot + 1, end_index);
+ Node child_1 = createPrecedenceExpr(exprs, kinds, start_index, pivot);
+ Node child_2 = createPrecedenceExpr(exprs, kinds, pivot + 1, end_index);
return d_expr_manager->mkExpr(kinds[pivot], child_1, child_2);
}
#include <antlr/LLkParser.hpp>
#include <antlr/SemanticException.hpp>
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
#include "util/command.h"
#include "util/Assert.h"
#include "parser/symbol_table.h"
* Set's the expression manager to use when creating/managing expression.
* @param expr_manager the expression manager
*/
- void setExpressionManager(ExprManager* expr_manager);
+ void setExpressionManager(NodeManager* expr_manager);
protected:
* @param var_name the name of the variable
* @return the variable expression
*/
- Expr getVariable(std::string var_name);
+ Node getVariable(std::string var_name);
/**
* Types of symbols.
* Returns the true expression.
* @return the true expression
*/
- Expr getTrueExpr() const;
+ Node getTrueExpr() const;
/**
* Returns the false expression.
* @return the false expression
*/
- Expr getFalseExpr() const;
+ Node getFalseExpr() const;
/**
* Creates a new unary CVC4 expression using the expression manager.
* @param kind the kind of the expression
* @param child the child
*/
- Expr newExpression(Kind kind, const Expr& child);
+ Node newExpression(Kind kind, const Node& child);
/**
* Creates a new binary CVC4 expression using the expression manager.
* @param kind the kind of the expression
* @param children the children of the expression
*/
- Expr newExpression(Kind kind, const Expr& child_1, const Expr& child_2);
+ Node newExpression(Kind kind, const Node& child_1, const Node& child_2);
/**
* Creates a new CVC4 expression using the expression manager.
* @param kind the kind of the expression
* @param children the children of the expression
*/
- Expr newExpression(Kind kind, const std::vector<Expr>& children);
+ Node newExpression(Kind kind, const std::vector<Node>& children);
/**
* Creates a new expression based on the given string of expressions and kinds.
* The expression is created so that it respects the kinds precedence table.
*/
- Expr createPrecedenceExpr(const std::vector<Expr>& exprs, const std::vector<Kind>& kinds);
+ Node createPrecedenceExpr(const std::vector<Node>& exprs, const std::vector<Kind>& kinds);
/**
* Creates a new predicated over the given sorts.
* Creates a new expression based on the given string of expressions and kinds.
* The expression is created so that it respects the kinds precedence table.
*/
- Expr createPrecedenceExpr(const std::vector<Expr>& exprs, const std::vector<Kind>& kinds, unsigned start_index, unsigned end_index);
+ Node createPrecedenceExpr(const std::vector<Node>& exprs, const std::vector<Kind>& kinds, unsigned start_index, unsigned end_index);
/** The status of the benchmark */
BenchmarkStatus d_benchmark_status;
/** The expression manager */
- ExprManager* d_expr_manager;
+ NodeManager* d_expr_manager;
/** The symbol table lookup */
- SymbolTable<Expr> d_var_symbol_table;
+ SymbolTable<Node> d_var_symbol_table;
};
std::ostream& operator<<(std::ostream& out, AntlrParser::BenchmarkStatus status);
return cmd;
}
-Expr CvcParser::parseNextExpression() throw(ParserException) {
- Expr result;
+Node CvcParser::parseNextExpression() throw(ParserException) {
+ Node result;
if(!done()) {
try {
result = d_antlr_parser->formula();
delete d_antlr_lexer;
}
-CvcParser::CvcParser(ExprManager*em, istream& input, const char* file_name) :
+CvcParser::CvcParser(NodeManager*em, istream& input, const char* file_name) :
Parser(em), d_input(input) {
if(!d_input) {
throw ParserException(string("Read error") +
*/
command returns [CVC4::Command* cmd = 0]
{
- Expr f;
+ Node f;
vector<string> ids;
}
: ASSERT f = formula { cmd = new AssertCommand(f); }
: BOOLEAN
;
-formula returns [CVC4::Expr formula]
+formula returns [CVC4::Node formula]
: formula = bool_formula
;
-bool_formula returns [CVC4::Expr formula]
+bool_formula returns [CVC4::Node formula]
{
- vector<Expr> formulas;
+ vector<Node> formulas;
vector<Kind> kinds;
- Expr f1, f2;
+ Node f1, f2;
Kind k;
}
: f1 = primary_bool_formula { formulas.push_back(f1); }
}
;
-primary_bool_formula returns [CVC4::Expr formula]
+primary_bool_formula returns [CVC4::Node formula]
: formula = bool_atom
| NOT formula = primary_bool_formula { formula = newExpression(CVC4::NOT, formula); }
| LPAREN formula = bool_formula RPAREN
| IFF { kind = CVC4::IFF; }
;
-bool_atom returns [CVC4::Expr atom]
+bool_atom returns [CVC4::Node atom]
{
string p;
}
* @param input the input stream to parse
* @param file_name the name of the file (for diagnostic output)
*/
- CvcParser(ExprManager* em, std::istream& input, const char* file_name = "");
+ CvcParser(NodeManager* em, std::istream& input, const char* file_name = "");
/**
* Destructor.
* Parses the next complete expression of the stream.
* @return the expression parsed
*/
- Expr parseNextExpression() throw(ParserException);
+ Node parseNextExpression() throw(ParserException);
protected:
namespace CVC4 {
namespace parser {
-Parser::Parser(ExprManager* em) :
+Parser::Parser(NodeManager* em) :
d_expr_manager(em), d_done(false) {
}
namespace CVC4 {
// Forward declarations
-class Expr;
+class Node;
class Command;
-class ExprManager;
+class NodeManager;
namespace parser {
* Construct the parser that uses the given expression manager.
* @param em the expression manager.
*/
- Parser(ExprManager* em);
+ Parser(NodeManager* em);
/**
* Destructor.
/**
* Parse the next expression of the stream
*/
- virtual Expr parseNextExpression() throw (ParserException) = 0;
+ virtual Node parseNextExpression() throw (ParserException) = 0;
/**
* Check if we are done -- either the end of input has been reached.
void setDone(bool done = true);
/** Expression manager the parser will be using */
- ExprManager* d_expr_manager;
+ NodeManager* d_expr_manager;
/** Are we done */
bool d_done;
return cmd;
}
-Expr SmtParser::parseNextExpression() throw(ParserException) {
- Expr result;
+Node SmtParser::parseNextExpression() throw(ParserException) {
+ Node result;
if(!done()) {
try {
result = d_antlr_parser->an_formula();
delete d_antlr_lexer;
}
-SmtParser::SmtParser(ExprManager* em, istream& input, const char* file_name) :
+SmtParser::SmtParser(NodeManager* em, istream& input, const char* file_name) :
Parser(em), d_input(input) {
if(!d_input) {
throw ParserException(string("Read error") +
/**
* Matches a propositional atom from the input.
*/
-prop_atom returns [CVC4::Expr atom]
+prop_atom returns [CVC4::Node atom]
{
std::string p;
}
* enclosed in brackets. The prop_atom rule from the original SMT grammar is inlined
* here in order to get rid of the ugly antlr non-determinism warrnings.
*/
-an_atom returns [CVC4::Expr atom]
+an_atom returns [CVC4::Node atom]
: atom = prop_atom
;
/**
* Matches an annotated formula.
*/
-an_formula returns [CVC4::Expr formula]
+an_formula returns [CVC4::Node formula]
{
Kind kind;
- vector<Expr> children;
+ vector<Node> children;
}
: formula = an_atom
| LPAREN kind = connective an_formulas[children] RPAREN { formula = newExpression(kind, children); }
;
-an_formulas[std::vector<Expr>& formulas]
+an_formulas[std::vector<Node>& formulas]
{
- Expr f;
+ Node f;
}
: ( f = an_formula { formulas.push_back(f); } )+
;
bench_attribute returns [ Command* smt_command = 0]
{
BenchmarkStatus b_status = SMT_UNKNOWN;
- Expr formula;
+ Node formula;
vector<string> sorts;
}
: C_LOGIC IDENTIFIER
* @param input the input stream to parse
* @param file_name the name of the file (for diagnostic output)
*/
- SmtParser(ExprManager* em, std::istream& input, const char* file_name = "");
+ SmtParser(NodeManager* em, std::istream& input, const char* file_name = "");
/**
* Destructor.
* Parses the next complete expression of the stream.
* @return the expression parsed
*/
- Expr parseNextExpression() throw(ParserException);
+ Node parseNextExpression() throw(ParserException);
protected:
#include <stack>
#include <ext/hash_map>
-#include "expr/expr.h"
-
namespace __gnu_cxx {
template<>
struct hash<std::string> {
d_de(de), d_te(te), d_sat() {
}
-void PropEngine::addVars(Expr e) {
+void PropEngine::addVars(Node e) {
Debug("prop") << "adding vars to " << e << endl;
- for(Expr::iterator i = e.begin(); i != e.end(); ++i) {
+ for(Node::iterator i = e.begin(); i != e.end(); ++i) {
Debug("prop") << "expr " << *i << endl;
if(i->getKind() == VARIABLE) {
if(d_vars.find(*i) == d_vars.end()) {
}
}
-static void doAtom(SimpSolver* minisat, map<Expr, Var>* vars, Expr e, vec<Lit>* c) {
+static void doAtom(SimpSolver* minisat, map<Node, Var>* vars, Node e, vec<Lit>* c) {
if(e.getKind() == VARIABLE) {
- map<Expr, Var>::iterator v = vars->find(e);
+ map<Node, Var>::iterator v = vars->find(e);
Assert(v != vars->end());
c->push(Lit(v->second, false));
return;
}
if(e.getKind() == NOT) {
Assert(e.numChildren() == 1);
- Expr child = *e.begin();
+ Node child = *e.begin();
Assert(child.getKind() == VARIABLE);
- map<Expr, Var>::iterator v = vars->find(child);
+ map<Node, Var>::iterator v = vars->find(child);
Assert(v != vars->end());
c->push(Lit(v->second, true));
return;
Unhandled();
}
-static void doClause(SimpSolver* minisat, map<Expr, Var>* vars, map<Var, Expr>* varsReverse, Expr e) {
+static void doClause(SimpSolver* minisat, map<Node, Var>* vars, map<Var, Node>* varsReverse, Node e) {
vec<Lit> c;
Debug("prop") << " " << e << endl;
if(e.getKind() == VARIABLE || e.getKind() == NOT) {
doAtom(minisat, vars, e, &c);
} else {
Assert(e.getKind() == OR);
- for(Expr::iterator i = e.begin(); i != e.end(); ++i) {
+ for(Node::iterator i = e.begin(); i != e.end(); ++i) {
Debug("prop") << " " << *i << endl;
doAtom(minisat, vars, *i, &c);
}
minisat->addClause(c);
}
-void PropEngine::solve(Expr e) {
+void PropEngine::solve(Node e) {
Debug("prop") << "SOLVING " << e << endl;
addVars(e);
if(e.getKind() == AND) {
Debug("prop") << "AND" << endl;
- for(Expr::iterator i = e.begin(); i != e.end(); ++i)
+ for(Node::iterator i = e.begin(); i != e.end(); ++i)
doClause(&d_sat, &d_vars, &d_varsReverse, *i);
} else doClause(&d_sat, &d_vars, &d_varsReverse, e);
#define __CVC4__PROP_ENGINE_H
#include "cvc4_config.h"
-#include "expr/expr.h"
+#include "expr/node.h"
#include "util/decision_engine.h"
#include "theory/theory_engine.h"
#include "prop/minisat/simp/SimpSolver.h"
DecisionEngine &d_de;
TheoryEngine &d_te;
CVC4::prop::minisat::SimpSolver d_sat;
- std::map<Expr, CVC4::prop::minisat::Var> d_vars;
- std::map<CVC4::prop::minisat::Var, Expr> d_varsReverse;
+ std::map<Node, CVC4::prop::minisat::Var> d_vars;
+ std::map<CVC4::prop::minisat::Var, Node> d_varsReverse;
- void addVars(Expr);
+ void addVars(Node);
public:
/**
/**
* Converts to CNF if necessary.
*/
- void solve(Expr);
+ void solve(Node);
};/* class PropEngine */
c->invoke(this);
}
-Expr SmtEngine::preprocess(Expr e) {
+Node SmtEngine::preprocess(Node e) {
return e;
}
void SmtEngine::processAssertionList() {
- for(std::vector<Expr>::iterator i = d_assertions.begin();
+ for(std::vector<Node>::iterator i = d_assertions.begin();
i != d_assertions.end();
++i)
d_expr = d_expr.isNull() ? *i : d_em->mkExpr(AND, d_expr, *i);
return Result(Result::VALIDITY_UNKNOWN);
}
-void SmtEngine::addFormula(Expr e) {
+void SmtEngine::addFormula(Node e) {
d_assertions.push_back(e);
}
-Result SmtEngine::checkSat(Expr e) {
+Result SmtEngine::checkSat(Node e) {
e = preprocess(e);
addFormula(e);
return check();
}
-Result SmtEngine::query(Expr e) {
+Result SmtEngine::query(Node e) {
e = preprocess(e);
addFormula(e);
return check();
}
-Result SmtEngine::assertFormula(Expr e) {
+Result SmtEngine::assertFormula(Node e) {
e = preprocess(e);
addFormula(e);
return quickCheck();
#include <vector>
#include "cvc4_config.h"
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
#include "util/result.h"
#include "util/model.h"
#include "util/options.h"
class SmtEngine {
/** Current set of assertions. */
// TODO: make context-aware to handle user-level push/pop.
- std::vector<Expr> d_assertions;
+ std::vector<Node> d_assertions;
/** Our expression manager */
- ExprManager *d_em;
+ NodeManager *d_em;
/** User-level options */
Options *d_opts;
/** Expression built-up for handing off to the propagation engine */
- Expr d_expr;
+ Node d_expr;
/** The decision engine */
DecisionEngine d_de;
PropEngine d_prop;
/**
- * Pre-process an Expr. This is expected to be highly-variable,
+ * Pre-process an Node. This is expected to be highly-variable,
* with a lot of "source-level configurability" to add multiple
- * passes over the Expr. TODO: may need to specify a LEVEL of
+ * passes over the Node. TODO: may need to specify a LEVEL of
* preprocessing (certain contexts need more/less ?).
*/
- Expr preprocess(Expr);
+ Node preprocess(Node);
/**
* Adds a formula to the current context.
*/
- void addFormula(Expr);
+ void addFormula(Node);
/**
* Full check of consistency in current context. Returns true iff
/*
* Construct an SmtEngine with the given expression manager and user options.
*/
- SmtEngine(ExprManager* em, Options* opts) throw() :
+ SmtEngine(NodeManager* em, Options* opts) throw() :
d_em(em),
d_opts(opts),
- d_expr(Expr::null()),
+ d_expr(Node::null()),
d_de(),
d_te(),
d_prop(d_de, d_te) {
* literals and conjunction of literals. Returns false iff
* inconsistent.
*/
- Result assertFormula(Expr);
+ Result assertFormula(Node);
/**
* Add a formula to the current context and call check(). Returns
* true iff consistent.
*/
- Result query(Expr);
+ Result query(Node);
/**
* Add a formula to the current context and call check(). Returns
* true iff consistent.
*/
- Result checkSat(Expr);
+ Result checkSat(Node);
/**
* Simplify a formula without doing "much" work. Requires assist
* from the SAT Engine.
*/
- Expr simplify(Expr);
+ Node simplify(Node);
/**
* Get a (counter)model (only if preceded by a SAT or INVALID query.
#ifndef __CVC4__THEORY__THEORY_H
#define __CVC4__THEORY__THEORY_H
-#include "expr/expr.h"
+#include "expr/node.h"
#include "util/literal.h"
namespace CVC4 {
static bool fullEffort(Effort e) { return e >= FULL_EFFORT; }
/**
- * Prepare for an Expr.
+ * Prepare for an Node.
*/
- virtual void setup(Expr) = 0;
+ virtual void setup(Node) = 0;
/**
* Assert a literal in the current context.
/**
* Return an explanation for the literal (which was previously propagated by this theory)..
*/
- virtual Expr explain(Literal) = 0;
+ virtual Node explain(Literal) = 0;
};/* class Theory */
#include "util/command.h"
#include "smt/smt_engine.h"
-#include "expr/expr.h"
+#include "expr/node.h"
#include "util/result.h"
using namespace std;
void EmptyCommand::invoke(SmtEngine* smt_engine) {
}
-AssertCommand::AssertCommand(const Expr& e) :
+AssertCommand::AssertCommand(const Node& e) :
d_expr(e) {
}
CheckSatCommand::CheckSatCommand() {
}
-CheckSatCommand::CheckSatCommand(const Expr& e) :
+CheckSatCommand::CheckSatCommand(const Node& e) :
d_expr(e) {
}
smt_engine->checkSat(d_expr);
}
-QueryCommand::QueryCommand(const Expr& e) :
+QueryCommand::QueryCommand(const Node& e) :
d_expr(e) {
}
#include <iostream>
#include "cvc4_config.h"
-#include "expr/expr.h"
+#include "expr/node.h"
namespace CVC4 {
class SmtEngine;
class Command;
- class Expr;
+ class Node;
}/* CVC4 namespace */
namespace CVC4 {
class CVC4_PUBLIC AssertCommand : public Command {
protected:
- Expr d_expr;
+ Node d_expr;
public:
- AssertCommand(const Expr& e);
+ AssertCommand(const Node& e);
void invoke(CVC4::SmtEngine* smt_engine);
void toString(std::ostream& out) const;
};/* class AssertCommand */
class CVC4_PUBLIC CheckSatCommand : public Command {
public:
CheckSatCommand();
- CheckSatCommand(const Expr& e);
+ CheckSatCommand(const Node& e);
void invoke(SmtEngine* smt);
void toString(std::ostream& out) const;
protected:
- Expr d_expr;
+ Node d_expr;
};/* class CheckSatCommand */
class CVC4_PUBLIC QueryCommand : public Command {
public:
- QueryCommand(const Expr& e);
+ QueryCommand(const Node& e);
void invoke(SmtEngine* smt);
void toString(std::ostream& out) const;
protected:
- Expr d_expr;
+ Node d_expr;
};/* class QueryCommand */
-/* Black box testing of CVC4::Expr. */
+/* Black box testing of CVC4::Node. */
#include <cxxtest/TestSuite.h>
public:
void testNull() {
- Expr::s_null;
+ Node::s_null;
}
void testCopyCtor() {
- Expr e(Expr::s_null);
+ Node e(Node::s_null);
}
};
-/* White box testing of CVC4::Expr. */
+/* White box testing of CVC4::Node. */
#include <cxxtest/TestSuite.h>
public:
void testNull() {
- Expr::s_null;
+ Node::s_null;
}
void testCopyCtor() {
- Expr e(Expr::s_null);
+ Node e(Node::s_null);
}
};
projects / cvc5.git / commitdiff