diff options
| -rw-r--r-- | AUTHORS | 8 | ||||
| -rw-r--r-- | COPYING | 7 | ||||
| -rw-r--r-- | ChangeLog | 3 | ||||
| -rw-r--r-- | INSTALL | 9 | ||||
| -rw-r--r-- | Makefile.am | 4 | ||||
| -rw-r--r-- | NEWS | 3 | ||||
| -rw-r--r-- | README | 13 | ||||
| -rw-r--r-- | README.emacs | 18 | ||||
| -rwxr-xr-x | autogen.sh | 11 | ||||
| -rw-r--r-- | configure.ac | 35 | ||||
| -rw-r--r-- | doc/Makefile.am | 0 | ||||
| -rw-r--r-- | src/Makefile.am | 1 | ||||
| -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 |
26 files changed, 722 insertions, 0 deletions
diff --git a/AUTHORS b/AUTHORS new file mode 100644 index 000000000..7e42f3804 --- /dev/null +++ b/AUTHORS @@ -0,0 +1,8 @@ +The core authors and designers of CVC4 are: + +Clark Barrett <barrett@cs.nyu.edu>, New York University +Christopher Conway <cconway@cs.nyu.edu>, New York University +Morgan Deters <mdeters@cs.nyu.edu>, New York University +Tim King <taking@cs.nyu.edu>, New York University +Dejan Jovanovic <dejan@cs.nyu.edu>, New York University + diff --git a/COPYING b/COPYING new file mode 100644 index 000000000..bbfaa5258 --- /dev/null +++ b/COPYING @@ -0,0 +1,7 @@ +CVC4 is copyright (C) 2009 the ACSys research group at the Courant +Institute for Mathematical Sciences, New York University. +All rights reserved. + +This is a prerelease version; distribution is restricted. + +-- Morgan Deters <mdeters@cs.nyu.edu> Mon, 02 Nov 2009 17:54:27 -0500 diff --git a/ChangeLog b/ChangeLog new file mode 100644 index 000000000..630e398d4 --- /dev/null +++ b/ChangeLog @@ -0,0 +1,3 @@ +2009-11-02 Morgan Deters <mdeters@morgandeters.com> + + * Active prototyping ongoing diff --git a/INSTALL b/INSTALL new file mode 100644 index 000000000..be1290c3c --- /dev/null +++ b/INSTALL @@ -0,0 +1,9 @@ +To build, use the top-level script "autogen.sh" to invoke various +autotools. You'll need reasonably new automake, autoconf, and libtool +installed. Then ./configure && make as usual. + +To build a source release, use "make dist"; this will include the +configure script and all the bits of automake/autoconf/libtool that +are necessary for an independent install. + +-- Morgan Deters <mdeters@cs.nyu.edu> Mon, 02 Nov 2009 17:54:27 -0500 diff --git a/Makefile.am b/Makefile.am new file mode 100644 index 000000000..a60337f29 --- /dev/null +++ b/Makefile.am @@ -0,0 +1,4 @@ +AUTOMAKE_OPTIONS = foreign +ACLOCAL_AMFLAGS = -I m4 + +SUBDIRS = src doc @@ -0,0 +1,3 @@ +This is a prerelease version of CVC4; distribution is restricted. + +-- Morgan Deters <mdeters@cs.nyu.edu> Mon, 02 Nov 2009 17:54:27 -0500 @@ -0,0 +1,13 @@ +This is a prerelease version of CVC4; distribution is restricted. + +For a suggestion of editing CVC4 code with emacs, see README.emacs. + +To build, use the top-level script "autogen.sh" to invoke various +autotools. You'll need reasonably new automake, autoconf, and libtool +installed. Then ./configure && make as usual. + +To build a source release, use "make dist"; this will include the +configure script and all the bits of automake/autoconf/libtool that +are necessary for an independent install. + +-- Morgan Deters <mdeters@cs.nyu.edu> Mon, 02 Nov 2009 18:28:47 -0500 diff --git a/README.emacs b/README.emacs new file mode 100644 index 000000000..277424230 --- /dev/null +++ b/README.emacs @@ -0,0 +1,18 @@ +To match the CVC4 coding style, drop the following in your ~/.emacs, +replacing "/home/mdeters/cvc4.*" in the last line with a regexp +describing your usual cvc4 editing location(s): + + +; CVC4 mode +(defun cvc4-c++-editing-mode () + "C++ mode with adjusted defaults for use with editing CVC4 code." + (interactive) + (message "CVC4 variant of C++ mode activated.") + (c++-mode) + (setq c-basic-offset 2) + (c-set-offset 'innamespace 0) + (setq indent-tabs-mode nil)) +(setq auto-mode-alist (cons '("/home/mdeters/cvc4.*/.*\\.\\(cc\\|cpp\\|h\\|hh\\|hpp\\)$" . cvc4-c++-editing-mode) auto-mode-alist)) + + +-- Morgan Deters <mdeters@cs.nyu.edu> Mon, 02 Nov 2009 18:19:22 -0500 diff --git a/autogen.sh b/autogen.sh new file mode 100755 index 000000000..612c5c204 --- /dev/null +++ b/autogen.sh @@ -0,0 +1,11 @@ +#!/bin/sh -ex + +cd "$(dirname "$0")" +mkdir -p m4 +libtoolize --copy +autoheader -I m4 +touch NEWS README AUTHORS ChangeLog +touch stamp-h +aclocal -I m4 +autoconf -I m4 +automake -ac --foreign diff --git a/configure.ac b/configure.ac new file mode 100644 index 000000000..d55e72eed --- /dev/null +++ b/configure.ac @@ -0,0 +1,35 @@ +# -*- Autoconf -*- +# Process this file with autoconf to produce a configure script. + +AC_PREREQ([2.63]) +AC_INIT([src/include/vc.h]) +AM_INIT_AUTOMAKE(cvc4, prerelease) +AC_CONFIG_MACRO_DIR([m4]) +AC_CONFIG_HEADERS([config.h]) + +# Checks for programs. +AC_PROG_CC +AC_PROG_CXX +AC_PROG_INSTALL +AC_PROG_LIBTOOL + +# Checks for libraries. +AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP not found, see http://gmplib.org/])]) + +# Checks for header files. + +# Checks for typedefs, structures, and compiler characteristics. +AC_HEADER_STDBOOL +AC_TYPE_UINT16_T +AC_TYPE_UINT32_T +AC_TYPE_UINT64_T + +# Checks for library functions. + +AC_CONFIG_FILES([ + Makefile + doc/Makefile + src/Makefile + src/include/Makefile +]) +AC_OUTPUT diff --git a/doc/Makefile.am b/doc/Makefile.am new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/doc/Makefile.am diff --git a/src/Makefile.am b/src/Makefile.am new file mode 100644 index 000000000..11fef4d27 --- /dev/null +++ b/src/Makefile.am @@ -0,0 +1 @@ +INCLUDES = -I@srcdir@/include 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 */ |