diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-03 00:31:47 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-03 00:31:47 +0000 |
commit | a101d3298691265ee4cf72bed1ca59cd60318839 (patch) | |
tree | f445dfe10bc6d3cf983609afc1217e3d1be2ddeb /src/include | |
parent | 6b9eec8b8b03e6c67c73aa931001949f06fea5fb (diff) |
commit of project structure including autotools support
Diffstat (limited to 'src/include')
-rw-r--r-- | src/include/Makefile.am | 14 | ||||
-rw-r--r-- | src/include/assert.h | 24 | ||||
-rw-r--r-- | src/include/attr_type.h | 28 | ||||
-rw-r--r-- | src/include/command.h | 20 | ||||
-rw-r--r-- | src/include/expr.h | 54 | ||||
-rw-r--r-- | src/include/expr_attribute.h | 84 | ||||
-rw-r--r-- | src/include/expr_builder.h | 131 | ||||
-rw-r--r-- | src/include/expr_manager.h | 68 | ||||
-rw-r--r-- | src/include/expr_value.h | 71 | ||||
-rw-r--r-- | src/include/kind.h | 24 | ||||
-rw-r--r-- | src/include/parser.h | 17 | ||||
-rw-r--r-- | src/include/sat.h | 17 | ||||
-rw-r--r-- | src/include/unique_id.h | 33 | ||||
-rw-r--r-- | src/include/vc.h | 25 |
14 files changed, 610 insertions, 0 deletions
diff --git a/src/include/Makefile.am b/src/include/Makefile.am new file mode 100644 index 000000000..fa37abd9a --- /dev/null +++ b/src/include/Makefile.am @@ -0,0 +1,14 @@ +EXTRA_DIST = \ + assert.h \ + attr_type.h \ + command.h + expr_attribute.h \ + expr_builder.h \ + expr.h \ + expr_manager.h \ + expr_value.h \ + kind.h \ + parser.h \ + sat.h \ + unique_id.h \ + vc.h diff --git a/src/include/assert.h b/src/include/assert.h new file mode 100644 index 000000000..473cd21f1 --- /dev/null +++ b/src/include/assert.h @@ -0,0 +1,24 @@ +/********************* -*- C++ -*- */ +/** assert.h + ** This file is part of the CVC4 prototype. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_ASSERT_H +#define __CVC4_ASSERT_H + +#include <cassert> + +#ifdef DEBUG +// the __builtin_expect() helps us if assert is built-in or a macro +# define cvc4assert(x) assert(__builtin_expect((x), 1)) +#else +// TODO: use a compiler annotation when assertions are off ? +// (to improve optimization) +# define cvc4assert(x) +#endif /* DEBUG */ + +#endif /* __CVC4_ASSERT_H */ diff --git a/src/include/attr_type.h b/src/include/attr_type.h new file mode 100644 index 000000000..a546d7dab --- /dev/null +++ b/src/include/attr_type.h @@ -0,0 +1,28 @@ +/********************* -*- C++ -*- */ +/** attr_type.h + ** This file is part of the CVC4 prototype. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_ATTR_TYPE_H +#define __CVC4_ATTR_TYPE_H + +namespace CVC4 { + +// 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 value_type Type;//Expr? + static const Type_attr marker; +}; + +AttributeTable<Type_attr> + +} /* CVC4 namespace */ + +#endif /* __CVC4_ATTR_TYPE_H */ diff --git a/src/include/command.h b/src/include/command.h new file mode 100644 index 000000000..45b59a95b --- /dev/null +++ b/src/include/command.h @@ -0,0 +1,20 @@ +/********************* -*- C++ -*- */ +/** command.h + ** This file is part of the CVC4 prototype. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_COMMAND_H +#define __CVC4_COMMAND_H + +namespace CVC4 { + +class Command { // distinct from Exprs +}; + +} /* CVC4 namespace */ + +#endif /* __CVC4_COMMAND_H */ diff --git a/src/include/expr.h b/src/include/expr.h new file mode 100644 index 000000000..5e3559fd7 --- /dev/null +++ b/src/include/expr.h @@ -0,0 +1,54 @@ +/********************* -*- C++ -*- */ +/** expr.h + ** This file is part of the CVC4 prototype. + ** + ** Reference-counted encapsulation of a pointer to an expression. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_EXPR_H +#define __CVC4_EXPR_H + +namespace CVC4 { + +class ExprValue; + +/** + * Encapsulation of an ExprValue pointer. The reference count is + * maintained in the ExprValue. + */ +class Expr { + /** 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*); + + /** Destructor. Decrements the reference count and, if zero, + * collects the ExprValue. */ + ~Expr(); + +public: + /** Access to the encapsulated expression. + * @return the encapsulated expression. */ + ExprValue* operator->(); + + /** Const access to the encapsulated expressoin. + * @return the encapsulated expression [const]. */ + const ExprValue* operator->() const; + +};/* class Expr */ + +} /* CVC4 namespace */ + +#endif /* __CVC4_EXPR_H */ diff --git a/src/include/expr_attribute.h b/src/include/expr_attribute.h new file mode 100644 index 000000000..b5f7dfe13 --- /dev/null +++ b/src/include/expr_attribute.h @@ -0,0 +1,84 @@ +/********************* -*- C++ -*- */ +/** expr_attribute.h + ** This file is part of the CVC4 prototype. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_EXPR_ATTRIBUTE_H +#define __CVC4_EXPR_ATTRIBUTE_H + +namespace CVC4 { + +template <class value_type> +class AttrTables; + +// global (or TSS) +extern CDMap<uint_64t> g_hash_bool; +extern CDMap<uint_64t> g_hash_int; +extern CDMap<Expr> g_hash_expr; +extern CDMap<void*> g_hash_ptr; + +template <> +class AttrTable<bool> { +public: + class BitAccessor { + uint64_t& d_word; + unsigned d_bit; + public: + BitAccessor& operator=(bool b); + // continue... + }; + + // bool specialization + static CDMap<uint_64t> *s_hash; + + template <class Attr> + BitAccessor& find(Expr e, const Attr&); + + template <class Attr> + bool find(Expr e, const Attr&) const; +}; + +template <> +class AttrTable<uint_64t> { +public: + // int(egral) specialization + static CDMap<uint64_t> *s_hash; + uint_64t& find(x); + uint_64t& find(x) 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; + find(x) +}; + +template <> AttrTable<bool>::s_hash = &g_hash_bool; +template <> AttrTable<uint_64t>::s_hash = &g_hash_int; +template <> AttrTable<Expr>::s_hash = &g_hash_expr; +template <> AttrTable<void*>::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 */ diff --git a/src/include/expr_builder.h b/src/include/expr_builder.h new file mode 100644 index 000000000..2e9bf49a4 --- /dev/null +++ b/src/include/expr_builder.h @@ -0,0 +1,131 @@ +/********************* -*- C++ -*- */ +/** expr_builder.h + ** This file is part of the CVC4 prototype. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_EXPR_BUILDER_H +#define __CVC4_EXPR_BUILDER_H + +namespace CVC4 { + +class AndExprBuilder; +class OrExprBuilder; +class PlusExprBuilder; +class MinusExprBuilder; +class MultExprBuilder; + +class ExprBuilder { + ExprManager* d_em; + + Kind d_kind; + + // TODO: store some flags here and install into attribute map when + // the expr is created? (we'd have to do that since we don't know + // it's hash code yet) + + // initially false, when you extract the Expr this is set and you can't + // extract another + bool d_used; + + unsigned d_nchildren; + union { + Expr u_arr[10]; + vector<Expr> u_vec; + } d_children; + +public: + + // 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); + + ExprBuilder& operator!() const { return notExpr(); } + ExprBuilder& operator&&(const Expr& right) const { return andExpr(right); } + ExprBuilder& operator||(const Expr& right) const { return orExpr(right); } + + // "Stream" expression constructor syntax + ExprBuilder& operator<<(const Op& op); + ExprBuilder& operator<<(const Expr& child); + + // For pushing sequences of children + ExprBuilder& append(const 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 */ diff --git a/src/include/expr_manager.h b/src/include/expr_manager.h new file mode 100644 index 000000000..f49235831 --- /dev/null +++ b/src/include/expr_manager.h @@ -0,0 +1,68 @@ +/********************* -*- C++ -*- */ +/** expr_manager.h + ** This file is part of the CVC4 prototype. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_EXPR_MANAGER_H +#define __CVC4_EXPR_MANAGER_H + +namespace CVC4 { + +class ExprManager { + static __thread ExprManager* current; + +public: + static ExprManager* currentEM() { return d_current; } + + // general expression-builders + Expr build(Kind kind); + Expr build(Kind kind, Expr child1); + Expr build(Kind kind, Expr child1, Expr child2); + Expr build(Kind kind, Expr child1, Expr child2, Expr child3); + Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); + Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5); + Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6); + Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7); + Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8); + Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9); + Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9, Expr child10); + // N-ary version + Expr build(Kind kind, vector<Expr> children); + + // these use the current EM + static Expr build(Kind kind) + { currentEM()->build(kind); } + static Expr build(Kind kind, Expr child1); + { currentEM()->build(kind, child1); } + static Expr build(Kind kind, Expr child1, Expr child2); + { currentEM()->build(kind, child1, child2); } + static Expr build(Kind kind, Expr child1, Expr child2, Expr child3); + { currentEM()->build(kind, child1, child2, child3); } + static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); + { currentEM()->build(kind, child1, child2, child3, child4); } + static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5); + { currentEM()->build(kind, child1, child2, child3, child4, child5); } + static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6); + { currentEM()->build(kind, child1, child2, child3, child4, child5, child6); } + static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7); + { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7); } + static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8); + { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7, child8); } + static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9); + { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7, child8, child9); } + static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9, Expr child10); + { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7, child8, child9, child10); } + // N-ary version + static Expr build(Kind kind, vector<Expr> children) + { currentEM()->build(kind, children); } + + // do we want a varargs one? perhaps not.. +}; + +} /* CVC4 namespace */ + +#endif /* __CVC4_EXPR_MANAGER_H */ diff --git a/src/include/expr_value.h b/src/include/expr_value.h new file mode 100644 index 000000000..ca12b8e03 --- /dev/null +++ b/src/include/expr_value.h @@ -0,0 +1,71 @@ +/********************* +/** expr_value.h + ** This file is part of the CVC4 prototype. + ** + ** 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 + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_EXPR_VALUE_H +#define __CVC4_EXPR_VALUE_H + +#include "expr.h" + +namespace CVC4 { + +/** + * This is an ExprValue. + */ +class ExprValue { + // 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]; + +public: + /** Hash this expression. + * @return the hash value of this expression. */ + unsigned hash() const; + + /** Convert to (wrap in) an Expr. + * @return an Expr pointing to this expression. */ + operator Expr(); + + // 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 */ diff --git a/src/include/kind.h b/src/include/kind.h new file mode 100644 index 000000000..26a3dd607 --- /dev/null +++ b/src/include/kind.h @@ -0,0 +1,24 @@ +/********************* -*- C++ -*- */ +/** expr_manager.h + ** This file is part of the CVC4 prototype. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_EXPR_MANAGER_H +#define __CVC4_EXPR_MANAGER_H + +namespace CVC4 { + +enum Kind { + AND, + OR, + XOR, + NOT, + PLUS, + MINUS, + UMINUS, + +}; diff --git a/src/include/parser.h b/src/include/parser.h new file mode 100644 index 000000000..0cfc89a28 --- /dev/null +++ b/src/include/parser.h @@ -0,0 +1,17 @@ +/********************* -*- C++ -*- */ +/** parser.h + ** This file is part of the CVC4 prototype. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_PARSER_H +#define __CVC4_PARSER_H + +namespace CVC4 { + +} /* CVC4 namespace */ + +#endif /* __CVC4_PARSER_H */ diff --git a/src/include/sat.h b/src/include/sat.h new file mode 100644 index 000000000..13578ec8d --- /dev/null +++ b/src/include/sat.h @@ -0,0 +1,17 @@ +/********************* -*- C++ -*- */ +/** sat.h + ** This file is part of the CVC4 prototype. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_SAT_H +#define __CVC4_SAT_H + +namespace CVC4 { + +} /* CVC4 namespace */ + +#endif /* __CVC4_SAT_H */ diff --git a/src/include/unique_id.h b/src/include/unique_id.h new file mode 100644 index 000000000..55fa24e51 --- /dev/null +++ b/src/include/unique_id.h @@ -0,0 +1,33 @@ +/********************* -*- C++ -*- */ +/** unique_id.h + ** This file is part of the CVC4 prototype. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_UNIQUE_ID_H +#define __CVC4_UNIQUE_ID_H + +namespace CVC4 { + +// NOTE that UniqueID is intended for startup registration; it +// shouldn't be used in multi-threaded contexts. + +template <class T> +class UniqueID { + static unsigned s_topID; + const unsigned d_thisID; + +public: + UniqueID() : d_thisID( s_topID++ ) { } + operator unsigned() const { return d_thisID; } +}; + +template <class T> +unsigned UniqueID<T>::s_topID = 0; + +} /* CVC4 namespace */ + +#endif /* __CVC4_UNIQUE_ID_H */ diff --git a/src/include/vc.h b/src/include/vc.h new file mode 100644 index 000000000..d4b293a28 --- /dev/null +++ b/src/include/vc.h @@ -0,0 +1,25 @@ +/********************* -*- C++ -*- */ +/** vc.h + ** This file is part of the CVC4 prototype. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_VC_H +#define __CVC4_VC_H + +/* TODO provide way of querying whether you fall into a fragment / + * returning what fragment you're in */ + +namespace CVC4 { + +class ValidityChecker { +public: + void doCommand(Command); +}; + +} /* CVC4 namespace */ + +#endif /* __CVC4_VC_H */ |