--- /dev/null
+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
+
--- /dev/null
+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
--- /dev/null
+2009-11-02 Morgan Deters <mdeters@morgandeters.com>
+
+ * Active prototyping ongoing
--- /dev/null
+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
--- /dev/null
+AUTOMAKE_OPTIONS = foreign
+ACLOCAL_AMFLAGS = -I m4
+
+SUBDIRS = src doc
--- /dev/null
+This is a prerelease version of CVC4; distribution is restricted.
+
+-- Morgan Deters <mdeters@cs.nyu.edu> Mon, 02 Nov 2009 17:54:27 -0500
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+#!/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
--- /dev/null
+# -*- 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
--- /dev/null
+INCLUDES = -I@srcdir@/include
--- /dev/null
+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
--- /dev/null
+/********************* -*- 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 */
--- /dev/null
+/********************* -*- 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 */
--- /dev/null
+/********************* -*- 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 */
--- /dev/null
+/********************* -*- 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 */
--- /dev/null
+/********************* -*- 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 */
--- /dev/null
+/********************* -*- 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 */
--- /dev/null
+/********************* -*- 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 */
--- /dev/null
+/*********************
+/** 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 */
--- /dev/null
+/********************* -*- 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,
+
+};
--- /dev/null
+/********************* -*- 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 */
--- /dev/null
+/********************* -*- 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 */
--- /dev/null
+/********************* -*- 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 */
--- /dev/null
+/********************* -*- 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 */
projects / cvc5.git / commitdiff