From a101d3298691265ee4cf72bed1ca59cd60318839 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 3 Nov 2009 00:31:47 +0000 Subject: [PATCH] commit of project structure including autotools support --- AUTHORS | 8 +++ COPYING | 7 ++ ChangeLog | 3 + INSTALL | 9 +++ Makefile.am | 4 ++ NEWS | 3 + README | 13 ++++ README.emacs | 18 +++++ autogen.sh | 11 +++ configure.ac | 35 ++++++++++ doc/Makefile.am | 0 src/Makefile.am | 1 + src/include/Makefile.am | 14 ++++ src/include/assert.h | 24 +++++++ src/include/attr_type.h | 28 ++++++++ src/include/command.h | 20 ++++++ src/include/expr.h | 54 +++++++++++++++ src/include/expr_attribute.h | 84 ++++++++++++++++++++++ src/include/expr_builder.h | 131 +++++++++++++++++++++++++++++++++++ src/include/expr_manager.h | 68 ++++++++++++++++++ src/include/expr_value.h | 71 +++++++++++++++++++ src/include/kind.h | 24 +++++++ src/include/parser.h | 17 +++++ src/include/sat.h | 17 +++++ src/include/unique_id.h | 33 +++++++++ src/include/vc.h | 25 +++++++ 26 files changed, 722 insertions(+) create mode 100644 AUTHORS create mode 100644 COPYING create mode 100644 ChangeLog create mode 100644 INSTALL create mode 100644 Makefile.am create mode 100644 NEWS create mode 100644 README create mode 100644 README.emacs create mode 100755 autogen.sh create mode 100644 configure.ac create mode 100644 doc/Makefile.am create mode 100644 src/Makefile.am create mode 100644 src/include/Makefile.am create mode 100644 src/include/assert.h create mode 100644 src/include/attr_type.h create mode 100644 src/include/command.h create mode 100644 src/include/expr.h create mode 100644 src/include/expr_attribute.h create mode 100644 src/include/expr_builder.h create mode 100644 src/include/expr_manager.h create mode 100644 src/include/expr_value.h create mode 100644 src/include/kind.h create mode 100644 src/include/parser.h create mode 100644 src/include/sat.h create mode 100644 src/include/unique_id.h create mode 100644 src/include/vc.h 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 , New York University +Christopher Conway , New York University +Morgan Deters , New York University +Tim King , New York University +Dejan Jovanovic , 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 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 + + * 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 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 diff --git a/NEWS b/NEWS new file mode 100644 index 000000000..860c27633 --- /dev/null +++ b/NEWS @@ -0,0 +1,3 @@ +This is a prerelease version of CVC4; distribution is restricted. + +-- Morgan Deters Mon, 02 Nov 2009 17:54:27 -0500 diff --git a/README b/README new file mode 100644 index 000000000..b6b20aba8 --- /dev/null +++ b/README @@ -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 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 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 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 + +#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 + +} /* 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 AttrTables; + +// global (or TSS) +extern CDMap g_hash_bool; +extern CDMap g_hash_int; +extern CDMap g_hash_expr; +extern CDMap g_hash_ptr; + +template <> +class AttrTable { +public: + class BitAccessor { + uint64_t& d_word; + unsigned d_bit; + public: + BitAccessor& operator=(bool b); + // continue... + }; + + // bool specialization + static CDMap *s_hash; + + template + BitAccessor& find(Expr e, const Attr&); + + template + bool find(Expr e, const Attr&) const; +}; + +template <> +class AttrTable { +public: + // int(egral) specialization + static CDMap *s_hash; + uint_64t& find(x); + uint_64t& find(x) const; +}; + +template +class AttrTable { + // pointer specialization + static CDMap *s_hash; +public: +}; + +template <> +class AttrTable { +public: + // Expr specialization + static CDMap *s_hash; + find(x) +}; + +template <> AttrTable::s_hash = &g_hash_bool; +template <> AttrTable::s_hash = &g_hash_int; +template <> AttrTable::s_hash = &g_hash_expr; +template <> AttrTable::s_hash = &g_hash_ptr; + +template +class AttributeTable { + typedef typename Attr::value_type value_type; + + AttrTable& 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 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& oldTerms, + const std::vector& newTerms); + ExprBuilder& substExpr(const ExprHashMap& 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& children) { return append(children.begin(), children.end()); } + template 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 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 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 UniqueID { + static unsigned s_topID; + const unsigned d_thisID; + +public: + UniqueID() : d_thisID( s_topID++ ) { } + operator unsigned() const { return d_thisID; } +}; + +template +unsigned UniqueID::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 */ -- 2.30.2