+++ /dev/null
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall
-
-noinst_LIBRARIES = libcore.a
-
-libcore_a_SOURCES = \
- expr.cpp \
- expr_builder.cpp \
- expr_manager.cpp \
- expr_value.cpp
+++ /dev/null
-/********************* -*- C++ -*- */
-/** attr_type.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_ATTR_TYPE_H
-#define __CVC4_ATTR_TYPE_H
-
-#include "core/expr_attribute.h"
-
-namespace CVC4 {
-
-class Type;
-
-// an "attribute type" for types
-// this is essentially a traits structure
-class Type_attr {
-public:
- enum { hash_value = 11 }; // could use typeid but then different on different machines/compiles
- typedef Type value_type;//Expr?
- static const Type_attr marker;
-};
-
-extern AttrTable<Type_attr> type_table;
-
-} /* CVC4 namespace */
-
-#endif /* __CVC4_ATTR_TYPE_H */
+++ /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 "cvc4_expr.h"
-#include "core/expr_value.h"
-#include "core/expr_builder.h"
-
-namespace CVC4 {
-
-Expr Expr::s_null(0);
-
-Expr::Expr(ExprValue* ev)
- : d_ev(ev) {
- // FIXME: thread-safety
- ++d_ev->d_rc;
-}
-
-Expr::Expr(const Expr& e) {
- // FIXME: thread-safety
- if((d_ev = e.d_ev))
- ++d_ev->d_rc;
-}
-
-Expr::~Expr() {
- // FIXME: thread-safety
- --d_ev->d_rc;
-}
-
-Expr& Expr::operator=(const Expr& e) {
- // FIXME: thread-safety
- if(d_ev)
- --d_ev->d_rc;
- if((d_ev = e.d_ev))
- ++d_ev->d_rc;
- return *this;
-}
-
-ExprValue* Expr::operator->() {
- return d_ev;
-}
-
-const ExprValue* Expr::operator->() const {
- return d_ev;
-}
-
-uint64_t Expr::hash() const {
- return d_ev->hash();
-}
-
-Expr Expr::eqExpr(const Expr& right) const {
- return ExprBuilder(*this).eqExpr(right);
-}
-
-Expr Expr::notExpr() const {
- return ExprBuilder(*this).notExpr();
-}
-
-Expr Expr::negate() const { // avoid double-negatives
- return ExprBuilder(*this).negate();
-}
-
-Expr Expr::andExpr(const Expr& right) const {
- return ExprBuilder(*this).andExpr(right);
-}
-
-Expr Expr::orExpr(const Expr& right) const {
- return ExprBuilder(*this).orExpr(right);
-}
-
-Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const {
- return ExprBuilder(*this).iteExpr(thenpart, elsepart);
-}
-
-Expr Expr::iffExpr(const Expr& right) const {
- return ExprBuilder(*this).iffExpr(right);
-}
-
-Expr Expr::impExpr(const Expr& right) const {
- return ExprBuilder(*this).impExpr(right);
-}
-
-Expr Expr::xorExpr(const Expr& right) const {
- return ExprBuilder(*this).xorExpr(right);
-}
-
-Expr Expr::skolemExpr(int i) const {
- return ExprBuilder(*this).skolemExpr(i);
-}
-
-Expr Expr::substExpr(const std::vector<Expr>& oldTerms,
- const std::vector<Expr>& newTerms) const {
- return ExprBuilder(*this).substExpr(oldTerms, newTerms);
-}
-
-} /* CVC4 namespace */
+++ /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_ATTRIBUTE_H
-#define __CVC4_EXPR_ATTRIBUTE_H
-
-// TODO WARNING this file needs work !
-
-#include <stdint.h>
-#include "core/config.h"
-#include "core/context.h"
-#include "core/cvc4_expr.h"
-
-namespace CVC4 {
-
-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 namespace */
-
-#endif /* __CVC4_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 "core/expr_builder.h"
-#include "core/expr_manager.h"
-#include "core/expr_value.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) {
- ExprValue *v = e->inc();
- d_children.u_arr[0] = v;
-}
-
-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) {
- cvc4assert(!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 {
- iterator j = d_children.u_arr;
- for(iterator i = eb.d_children.u_arr; i != eb.d_children.u_arr + eb.d_nchildren; ++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&) : 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() {
- if(d_nchildren > nchild_thresh) {
- delete d_children.u_vec;
- } else {
- for(iterator i = d_children.u_arr; i != d_children.u_arr + d_nchildren; ++i) {
- *i
- }
- }
-}
-
-// Compound expression constructors
-ExprBuilder& ExprBuilder::eqExpr(const Expr& right) {
- if(d_kind != UNDEFINED_KIND && d_kind != EQUAL)
- collapse();
- d_kind = EQUAL;
- return *this;
-}
-
-ExprBuilder& ExprBuilder::notExpr() {
-}
-
-// avoid double-negatives
-ExprBuilder& ExprBuilder::negate() {
-}
-
-ExprBuilder& ExprBuilder::andExpr(const Expr& right) {
-}
-
-ExprBuilder& ExprBuilder::orExpr(const Expr& right) {
-}
-
-ExprBuilder& ExprBuilder::iteExpr(const Expr& thenpart, const Expr& elsepart) {
-}
-
-ExprBuilder& ExprBuilder::iffExpr(const Expr& right) {
-}
-
-ExprBuilder& ExprBuilder::impExpr(const Expr& right) {
-}
-
-ExprBuilder& ExprBuilder::xorExpr(const Expr& right) {
-}
-
-ExprBuilder& ExprBuilder::skolemExpr(int i) {
-}
-
-ExprBuilder& ExprBuilder::substExpr(const std::vector<Expr>& oldTerms,
- const std::vector<Expr>& newTerms) {
-}
-
-// "Stream" expression constructor syntax
-ExprBuilder& ExprBuilder::operator<<(const Kind& op) {
-}
-
-ExprBuilder& ExprBuilder::operator<<(const Expr& child) {
-}
-
-template <class Iterator>
-ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) {
-}
-
-void ExprBuilder::addChild(const Expr& e) {
- if(d_nchildren == nchild_thresh) {
- vector<Expr>* v = new vector<Expr>();
- v->reserve(nchild_thresh + 5);
-
- }
- return *this;
-}
-
-void ExprBuilder::collapse() {
- if(d_nchildren == nchild_thresh) {
- vector<Expr>* v = new vector<Expr>();
- v->reserve(nchild_thresh + 5);
-
- }
- return *this;
-}
-
-// not const
-ExprBuilder::operator Expr() {
-}
-
-AndExprBuilder ExprBuilder::operator&&(Expr) {
-}
-
-OrExprBuilder ExprBuilder::operator||(Expr) {
-}
-
-PlusExprBuilder ExprBuilder::operator+ (Expr) {
-}
-
-PlusExprBuilder ExprBuilder::operator- (Expr) {
-}
-
-MultExprBuilder ExprBuilder::operator* (Expr) {
-}
-
-} /* 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 "core/expr_manager.h"
-#include "core/kind.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();
- void collapse();
-
-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);
- ExprBuilder& skolemExpr(int i);
- ExprBuilder& substExpr(const std::vector<Expr>& oldTerms,
- const std::vector<Expr>& newTerms);
- /*
- ExprBuilder& substExpr(const ExprHashMap<Expr>& oldToNew);
- */
-
- /* 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()); }
- 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);
-
-};/* class ExprBuilder */
-
-class AndExprBuilder {
- ExprManager* d_em;
-
-public:
-
- AndExprBuilder& operator&&(Expr);
- OrExprBuilder operator||(Expr);
-
- operator ExprBuilder();
-
-};/* class AndExprBuilder */
-
-class OrExprBuilder {
- ExprManager* d_em;
-
-public:
-
- AndExprBuilder operator&&(Expr);
- OrExprBuilder& operator||(Expr);
-
- operator ExprBuilder();
-
-};/* class OrExprBuilder */
-
-class PlusExprBuilder {
- ExprManager* d_em;
-
-public:
-
- PlusExprBuilder& operator+(Expr);
- PlusExprBuilder& operator-(Expr);
- MultExprBuilder operator*(Expr);
-
- operator ExprBuilder();
-
-};/* class PlusExprBuilder */
-
-class MultExprBuilder {
- ExprManager* d_em;
-
-public:
-
- PlusExprBuilder operator+(Expr);
- PlusExprBuilder operator-(Expr);
- MultExprBuilder& operator*(Expr);
-
- operator ExprBuilder();
-
-};/* class MultExprBuilder */
-
-} /* 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 "core/expr_builder.h"
-#include "core/expr_manager.h"
-#include "core/cvc4_expr.h"
-
-namespace CVC4 {
-
-__thread ExprManager* ExprManager::s_current = 0;
-
-// general expression-builders
-
-Expr ExprManager::mkExpr(Kind kind) {
- return ExprBuilder(this, kind);
-}
-
-Expr ExprManager::mkExpr(Kind kind, Expr child1) {
- return ExprBuilder(this, kind) << child1;
-}
-
-Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) {
- return ExprBuilder(this, kind) << child1 << child2;
-}
-
-Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3) {
- return ExprBuilder(this, kind) << child1 << child2 << child3;
-}
-
-Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, 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) {
- 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);
-}
-
-} /* 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 "cvc4_expr.h"
-#include "core/kind.h"
-
-namespace CVC4 {
-
-class ExprManager {
- static __thread ExprManager* s_current;
-
-public:
- static ExprManager* currentEM() { return s_current; }
-
- // 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);
- // N-ary version
- Expr mkExpr(Kind kind, std::vector<Expr> children);
-
- // 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 */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** expr_value.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.
- **
- ** An expression node.
- **
- ** Instances of this class are generally referenced through
- ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the
- ** reference count on ExprValue instances and
- **/
-
-#include "core/expr_value.h"
-
-namespace CVC4 {
-
-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;
-}
-
-ExprValue* ExprValue::inc() {
- // FIXME multithreading
- if(d_rc < MAX_RC)
- ++d_rc;
- return this;
-}
-
-ExprValue* ExprValue::dec() {
- // FIXME multithreading
- if(d_rc < MAX_RC)
- if(--d_rc == 0) {
- // FIXME gc
- return 0;
- }
- return this;
-}
-
-ExprValue::iterator ExprValue::begin() {
- return d_children;
-}
-
-ExprValue::iterator ExprValue::end() {
- return d_children + d_nchildren;
-}
-
-ExprValue::iterator ExprValue::rbegin() {
- return d_children + d_nchildren - 1;
-}
-
-ExprValue::iterator ExprValue::rend() {
- return d_children - 1;
-}
-
-ExprValue::const_iterator ExprValue::begin() const {
- return d_children;
-}
-
-ExprValue::const_iterator ExprValue::end() const {
- return d_children + d_nchildren;
-}
-
-ExprValue::const_iterator ExprValue::rbegin() const {
- return d_children + d_nchildren - 1;
-}
-
-ExprValue::const_iterator ExprValue::rend() const {
- return d_children - 1;
-}
-
-} /* CVC4 namespace */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** expr_value.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.
- **
- ** An expression node.
- **
- ** Instances of this class are generally referenced through
- ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the
- ** reference count on ExprValue instances and
- **/
-
-#ifndef __CVC4_EXPR_VALUE_H
-#define __CVC4_EXPR_VALUE_H
-
-#include <stdint.h>
-#include "cvc4_expr.h"
-
-namespace CVC4 {
-
-/**
- * This is an ExprValue.
- */
-class ExprValue {
- /** Maximum reference count possible. Used for sticky
- * reference-counting. Should be (1 << num_bits(d_rc)) - 1 */
- static const unsigned MAX_RC = 255;
-
- // this header fits into one 64-bit word
-
- /** The ID */
- unsigned d_id : 32;
-
- /** The expression's reference count. @see cvc4::Expr. */
- unsigned d_rc : 8;
-
- /** Kind of the expression */
- unsigned d_kind : 8;
-
- /** Number of children */
- unsigned d_nchildren : 16;
-
- /** Variable number of child nodes */
- Expr d_children[0];
-
- friend class Expr;
-
-public:
- /** Hash this expression.
- * @return the hash value of this expression. */
- uint64_t hash() const;
-
- // Iterator support
-
- typedef Expr* iterator;
- typedef Expr const* const_iterator;
-
- iterator begin();
- iterator end();
- iterator rbegin();
- iterator rend();
-
- const_iterator begin() const;
- const_iterator end() const;
- const_iterator rbegin() const;
- const_iterator rend() const;
-};
-
-} /* CVC4 namespace */
-
-#endif /* __CVC4_EXPR_VALUE_H */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** kind.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_KIND_H
-#define __CVC4_KIND_H
-
-namespace CVC4 {
-
-// TODO: create this file (?) from theory solver headers so that we
-// have a collection of kinds from all. This file is mainly a
-// placeholder for design & development work.
-
-enum Kind {
- UNDEFINED_KIND = -1,
- EQUAL,
- AND,
- OR,
- XOR,
- NOT,
- PLUS,
- MINUS,
- ITE,
- IFF,
- SKOLEM,
- SUBST
-};/* enum Kind */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_KIND_H */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** parser.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.
- **
- ** Parser abstraction.
- **/
-
-#ifndef __CVC4_PARSER_H
-#define __CVC4_PARSER_H
-
-#include "core/exception.h"
-#include "core/lang.h"
-
-namespace CVC4 {
-
- class ValidityChecker;
- class Expr;
-
- // Internal parser state and other data
- class ParserData;
-
- class Parser {
- private:
- ParserData* d_data;
- // Internal methods for constructing and destroying the actual parser
- void initParser();
- void deleteParser();
- public:
- // Constructors
- Parser(ValidityChecker* vc, InputLanguage lang,
- // The 'interactive' flag is ignored when fileName != ""
- bool interactive = true,
- const std::string& fileName = "");
- Parser(ValidityChecker* vc, InputLanguage lang, std::istream& is,
- bool interactive = false);
- // Destructor
- ~Parser();
- // Read the next command.
- Expr next();
- // Check if we are done (end of input has been reached)
- bool done() const;
- // The same check can be done by using the class Parser's value as
- // a Boolean
- operator bool() const { return done(); }
- void printLocation(std::ostream & out) const;
- // Reset any local data that depends on validity checker
- void reset();
- }; // end of class Parser
-
- // The global pointer to ParserTemp. Each instance of class Parser
- // sets this pointer before any calls to the lexer. We do it this
- // way because flex and bison use global vars, and we want each
- // Parser object to appear independent.
- class ParserTemp;
- extern ParserTemp* parserTemp;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_PARSER_H */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** parser_exception.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.
- **
- ** Exception class.
- **/
-
-#ifndef __CVC4_PARSER_EXCEPTION_H
-#define __CVC4_PARSER_EXCEPTION_H
-
-#include "core/exception.h"
-#include <string>
-#include <iostream>
-
-namespace CVC4 {
-
- class ParserException: public Exception {
- public:
- // Constructors
- ParserException() { }
- ParserException(const std::string& msg): Exception(msg) { }
- ParserException(const char* msg): Exception(msg) { }
- // Destructor
- virtual ~ParserException() { }
- virtual std::string toString() const {
- return "Parse Error: " + d_msg;
- }
- }; // end of class ParserException
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_PARSER_EXCEPTION_H */
--- /dev/null
+INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CXXFLAGS = -Wall
+
+noinst_LIBRARIES = libcore.a
+
+libcore_a_SOURCES = \
+ expr.cpp \
+ expr_builder.cpp \
+ expr_manager.cpp \
+ expr_value.cpp
--- /dev/null
+/********************* -*- C++ -*- */
+/** attr_type.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_ATTR_TYPE_H
+#define __CVC4_ATTR_TYPE_H
+
+#include "core/expr_attribute.h"
+
+namespace CVC4 {
+
+class Type;
+
+// an "attribute type" for types
+// this is essentially a traits structure
+class Type_attr {
+public:
+ enum { hash_value = 11 }; // could use typeid but then different on different machines/compiles
+ typedef Type value_type;//Expr?
+ static const Type_attr marker;
+};
+
+extern AttrTable<Type_attr> type_table;
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4_ATTR_TYPE_H */
--- /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 "cvc4_expr.h"
+#include "core/expr_value.h"
+#include "core/expr_builder.h"
+
+namespace CVC4 {
+
+Expr Expr::s_null(0);
+
+Expr::Expr(ExprValue* ev)
+ : d_ev(ev) {
+ // FIXME: thread-safety
+ ++d_ev->d_rc;
+}
+
+Expr::Expr(const Expr& e) {
+ // FIXME: thread-safety
+ if((d_ev = e.d_ev))
+ ++d_ev->d_rc;
+}
+
+Expr::~Expr() {
+ // FIXME: thread-safety
+ --d_ev->d_rc;
+}
+
+Expr& Expr::operator=(const Expr& e) {
+ // FIXME: thread-safety
+ if(d_ev)
+ --d_ev->d_rc;
+ if((d_ev = e.d_ev))
+ ++d_ev->d_rc;
+ return *this;
+}
+
+ExprValue* Expr::operator->() {
+ return d_ev;
+}
+
+const ExprValue* Expr::operator->() const {
+ return d_ev;
+}
+
+uint64_t Expr::hash() const {
+ return d_ev->hash();
+}
+
+Expr Expr::eqExpr(const Expr& right) const {
+ return ExprBuilder(*this).eqExpr(right);
+}
+
+Expr Expr::notExpr() const {
+ return ExprBuilder(*this).notExpr();
+}
+
+Expr Expr::negate() const { // avoid double-negatives
+ return ExprBuilder(*this).negate();
+}
+
+Expr Expr::andExpr(const Expr& right) const {
+ return ExprBuilder(*this).andExpr(right);
+}
+
+Expr Expr::orExpr(const Expr& right) const {
+ return ExprBuilder(*this).orExpr(right);
+}
+
+Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const {
+ return ExprBuilder(*this).iteExpr(thenpart, elsepart);
+}
+
+Expr Expr::iffExpr(const Expr& right) const {
+ return ExprBuilder(*this).iffExpr(right);
+}
+
+Expr Expr::impExpr(const Expr& right) const {
+ return ExprBuilder(*this).impExpr(right);
+}
+
+Expr Expr::xorExpr(const Expr& right) const {
+ return ExprBuilder(*this).xorExpr(right);
+}
+
+Expr Expr::skolemExpr(int i) const {
+ return ExprBuilder(*this).skolemExpr(i);
+}
+
+Expr Expr::substExpr(const std::vector<Expr>& oldTerms,
+ const std::vector<Expr>& newTerms) const {
+ return ExprBuilder(*this).substExpr(oldTerms, newTerms);
+}
+
+} /* CVC4 namespace */
--- /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_ATTRIBUTE_H
+#define __CVC4_EXPR_ATTRIBUTE_H
+
+// TODO WARNING this file needs work !
+
+#include <stdint.h>
+#include "core/config.h"
+#include "core/context.h"
+#include "core/cvc4_expr.h"
+
+namespace CVC4 {
+
+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 namespace */
+
+#endif /* __CVC4_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 "core/expr_builder.h"
+#include "core/expr_manager.h"
+#include "core/expr_value.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) {
+ ExprValue *v = e->inc();
+ d_children.u_arr[0] = v;
+}
+
+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) {
+ cvc4assert(!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 {
+ iterator j = d_children.u_arr;
+ for(iterator i = eb.d_children.u_arr; i != eb.d_children.u_arr + eb.d_nchildren; ++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&) : 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() {
+ if(d_nchildren > nchild_thresh) {
+ delete d_children.u_vec;
+ } else {
+ for(iterator i = d_children.u_arr; i != d_children.u_arr + d_nchildren; ++i) {
+ *i
+ }
+ }
+}
+
+// Compound expression constructors
+ExprBuilder& ExprBuilder::eqExpr(const Expr& right) {
+ if(d_kind != UNDEFINED_KIND && d_kind != EQUAL)
+ collapse();
+ d_kind = EQUAL;
+ return *this;
+}
+
+ExprBuilder& ExprBuilder::notExpr() {
+}
+
+// avoid double-negatives
+ExprBuilder& ExprBuilder::negate() {
+}
+
+ExprBuilder& ExprBuilder::andExpr(const Expr& right) {
+}
+
+ExprBuilder& ExprBuilder::orExpr(const Expr& right) {
+}
+
+ExprBuilder& ExprBuilder::iteExpr(const Expr& thenpart, const Expr& elsepart) {
+}
+
+ExprBuilder& ExprBuilder::iffExpr(const Expr& right) {
+}
+
+ExprBuilder& ExprBuilder::impExpr(const Expr& right) {
+}
+
+ExprBuilder& ExprBuilder::xorExpr(const Expr& right) {
+}
+
+ExprBuilder& ExprBuilder::skolemExpr(int i) {
+}
+
+ExprBuilder& ExprBuilder::substExpr(const std::vector<Expr>& oldTerms,
+ const std::vector<Expr>& newTerms) {
+}
+
+// "Stream" expression constructor syntax
+ExprBuilder& ExprBuilder::operator<<(const Kind& op) {
+}
+
+ExprBuilder& ExprBuilder::operator<<(const Expr& child) {
+}
+
+template <class Iterator>
+ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) {
+}
+
+void ExprBuilder::addChild(const Expr& e) {
+ if(d_nchildren == nchild_thresh) {
+ vector<Expr>* v = new vector<Expr>();
+ v->reserve(nchild_thresh + 5);
+
+ }
+ return *this;
+}
+
+void ExprBuilder::collapse() {
+ if(d_nchildren == nchild_thresh) {
+ vector<Expr>* v = new vector<Expr>();
+ v->reserve(nchild_thresh + 5);
+
+ }
+ return *this;
+}
+
+// not const
+ExprBuilder::operator Expr() {
+}
+
+AndExprBuilder ExprBuilder::operator&&(Expr) {
+}
+
+OrExprBuilder ExprBuilder::operator||(Expr) {
+}
+
+PlusExprBuilder ExprBuilder::operator+ (Expr) {
+}
+
+PlusExprBuilder ExprBuilder::operator- (Expr) {
+}
+
+MultExprBuilder ExprBuilder::operator* (Expr) {
+}
+
+} /* 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 "core/expr_manager.h"
+#include "core/kind.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();
+ void collapse();
+
+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);
+ ExprBuilder& skolemExpr(int i);
+ ExprBuilder& substExpr(const std::vector<Expr>& oldTerms,
+ const std::vector<Expr>& newTerms);
+ /*
+ ExprBuilder& substExpr(const ExprHashMap<Expr>& oldToNew);
+ */
+
+ /* 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()); }
+ 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);
+
+};/* class ExprBuilder */
+
+class AndExprBuilder {
+ ExprManager* d_em;
+
+public:
+
+ AndExprBuilder& operator&&(Expr);
+ OrExprBuilder operator||(Expr);
+
+ operator ExprBuilder();
+
+};/* class AndExprBuilder */
+
+class OrExprBuilder {
+ ExprManager* d_em;
+
+public:
+
+ AndExprBuilder operator&&(Expr);
+ OrExprBuilder& operator||(Expr);
+
+ operator ExprBuilder();
+
+};/* class OrExprBuilder */
+
+class PlusExprBuilder {
+ ExprManager* d_em;
+
+public:
+
+ PlusExprBuilder& operator+(Expr);
+ PlusExprBuilder& operator-(Expr);
+ MultExprBuilder operator*(Expr);
+
+ operator ExprBuilder();
+
+};/* class PlusExprBuilder */
+
+class MultExprBuilder {
+ ExprManager* d_em;
+
+public:
+
+ PlusExprBuilder operator+(Expr);
+ PlusExprBuilder operator-(Expr);
+ MultExprBuilder& operator*(Expr);
+
+ operator ExprBuilder();
+
+};/* class MultExprBuilder */
+
+} /* 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 "core/expr_builder.h"
+#include "core/expr_manager.h"
+#include "core/cvc4_expr.h"
+
+namespace CVC4 {
+
+__thread ExprManager* ExprManager::s_current = 0;
+
+// general expression-builders
+
+Expr ExprManager::mkExpr(Kind kind) {
+ return ExprBuilder(this, kind);
+}
+
+Expr ExprManager::mkExpr(Kind kind, Expr child1) {
+ return ExprBuilder(this, kind) << child1;
+}
+
+Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) {
+ return ExprBuilder(this, kind) << child1 << child2;
+}
+
+Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3) {
+ return ExprBuilder(this, kind) << child1 << child2 << child3;
+}
+
+Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, 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) {
+ 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);
+}
+
+} /* 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 "cvc4_expr.h"
+#include "core/kind.h"
+
+namespace CVC4 {
+
+class ExprManager {
+ static __thread ExprManager* s_current;
+
+public:
+ static ExprManager* currentEM() { return s_current; }
+
+ // 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);
+ // N-ary version
+ Expr mkExpr(Kind kind, std::vector<Expr> children);
+
+ // 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 */
--- /dev/null
+/********************* -*- C++ -*- */
+/** expr_value.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.
+ **
+ ** An expression node.
+ **
+ ** Instances of this class are generally referenced through
+ ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the
+ ** reference count on ExprValue instances and
+ **/
+
+#include "core/expr_value.h"
+
+namespace CVC4 {
+
+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;
+}
+
+ExprValue* ExprValue::inc() {
+ // FIXME multithreading
+ if(d_rc < MAX_RC)
+ ++d_rc;
+ return this;
+}
+
+ExprValue* ExprValue::dec() {
+ // FIXME multithreading
+ if(d_rc < MAX_RC)
+ if(--d_rc == 0) {
+ // FIXME gc
+ return 0;
+ }
+ return this;
+}
+
+ExprValue::iterator ExprValue::begin() {
+ return d_children;
+}
+
+ExprValue::iterator ExprValue::end() {
+ return d_children + d_nchildren;
+}
+
+ExprValue::iterator ExprValue::rbegin() {
+ return d_children + d_nchildren - 1;
+}
+
+ExprValue::iterator ExprValue::rend() {
+ return d_children - 1;
+}
+
+ExprValue::const_iterator ExprValue::begin() const {
+ return d_children;
+}
+
+ExprValue::const_iterator ExprValue::end() const {
+ return d_children + d_nchildren;
+}
+
+ExprValue::const_iterator ExprValue::rbegin() const {
+ return d_children + d_nchildren - 1;
+}
+
+ExprValue::const_iterator ExprValue::rend() const {
+ return d_children - 1;
+}
+
+} /* CVC4 namespace */
--- /dev/null
+/********************* -*- C++ -*- */
+/** expr_value.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.
+ **
+ ** An expression node.
+ **
+ ** Instances of this class are generally referenced through
+ ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the
+ ** reference count on ExprValue instances and
+ **/
+
+#ifndef __CVC4_EXPR_VALUE_H
+#define __CVC4_EXPR_VALUE_H
+
+#include <stdint.h>
+#include "cvc4_expr.h"
+
+namespace CVC4 {
+
+/**
+ * This is an ExprValue.
+ */
+class ExprValue {
+ /** Maximum reference count possible. Used for sticky
+ * reference-counting. Should be (1 << num_bits(d_rc)) - 1 */
+ static const unsigned MAX_RC = 255;
+
+ // this header fits into one 64-bit word
+
+ /** The ID */
+ unsigned d_id : 32;
+
+ /** The expression's reference count. @see cvc4::Expr. */
+ unsigned d_rc : 8;
+
+ /** Kind of the expression */
+ unsigned d_kind : 8;
+
+ /** Number of children */
+ unsigned d_nchildren : 16;
+
+ /** Variable number of child nodes */
+ Expr d_children[0];
+
+ friend class Expr;
+
+public:
+ /** Hash this expression.
+ * @return the hash value of this expression. */
+ uint64_t hash() const;
+
+ // Iterator support
+
+ typedef Expr* iterator;
+ typedef Expr const* const_iterator;
+
+ iterator begin();
+ iterator end();
+ iterator rbegin();
+ iterator rend();
+
+ const_iterator begin() const;
+ const_iterator end() const;
+ const_iterator rbegin() const;
+ const_iterator rend() const;
+};
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4_EXPR_VALUE_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** kind.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_KIND_H
+#define __CVC4_KIND_H
+
+namespace CVC4 {
+
+// TODO: create this file (?) from theory solver headers so that we
+// have a collection of kinds from all. This file is mainly a
+// placeholder for design & development work.
+
+enum Kind {
+ UNDEFINED_KIND = -1,
+ EQUAL,
+ AND,
+ OR,
+ XOR,
+ NOT,
+ PLUS,
+ MINUS,
+ ITE,
+ IFF,
+ SKOLEM,
+ SUBST
+};/* enum Kind */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_KIND_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** parser.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.
+ **
+ ** Parser abstraction.
+ **/
+
+#ifndef __CVC4_PARSER_H
+#define __CVC4_PARSER_H
+
+#include "core/exception.h"
+#include "core/lang.h"
+
+namespace CVC4 {
+
+ class ValidityChecker;
+ class Expr;
+
+ // Internal parser state and other data
+ class ParserData;
+
+ class Parser {
+ private:
+ ParserData* d_data;
+ // Internal methods for constructing and destroying the actual parser
+ void initParser();
+ void deleteParser();
+ public:
+ // Constructors
+ Parser(ValidityChecker* vc, InputLanguage lang,
+ // The 'interactive' flag is ignored when fileName != ""
+ bool interactive = true,
+ const std::string& fileName = "");
+ Parser(ValidityChecker* vc, InputLanguage lang, std::istream& is,
+ bool interactive = false);
+ // Destructor
+ ~Parser();
+ // Read the next command.
+ Expr next();
+ // Check if we are done (end of input has been reached)
+ bool done() const;
+ // The same check can be done by using the class Parser's value as
+ // a Boolean
+ operator bool() const { return done(); }
+ void printLocation(std::ostream & out) const;
+ // Reset any local data that depends on validity checker
+ void reset();
+ }; // end of class Parser
+
+ // The global pointer to ParserTemp. Each instance of class Parser
+ // sets this pointer before any calls to the lexer. We do it this
+ // way because flex and bison use global vars, and we want each
+ // Parser object to appear independent.
+ class ParserTemp;
+ extern ParserTemp* parserTemp;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_PARSER_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** parser_exception.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.
+ **
+ ** Exception class.
+ **/
+
+#ifndef __CVC4_PARSER_EXCEPTION_H
+#define __CVC4_PARSER_EXCEPTION_H
+
+#include "core/exception.h"
+#include <string>
+#include <iostream>
+
+namespace CVC4 {
+
+ class ParserException: public Exception {
+ public:
+ // Constructors
+ ParserException() { }
+ ParserException(const std::string& msg): Exception(msg) { }
+ ParserException(const char* msg): Exception(msg) { }
+ // Destructor
+ virtual ~ParserException() { }
+ virtual std::string toString() const {
+ return "Parse Error: " + d_msg;
+ }
+ }; // end of class ParserException
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_PARSER_EXCEPTION_H */
projects / cvc5.git / commitdiff