+AM_CXXFLAGS = -Wall
+
AUTOMAKE_OPTIONS = foreign
ACLOCAL_AMFLAGS = -I config
-INCLUDES = -I@srcdir@/include
+INCLUDES = -I@srcdir@/include -I@srcdir@
SUBDIRS = core parser sat
sat/minisat/libminisat.a
EXTRA_DIST = \
- include/assert.h \
- include/attr_type.h \
- include/command.h
- include/expr_attribute.h \
- include/expr_builder.h \
- include/expr.h \
- include/expr_manager.h \
- include/expr_value.h \
- include/kind.h \
- include/parser.h \
- include/sat.h \
- include/unique_id.h \
- include/vc.h
-
+ include/cvc4.h \
+ include/cvc4_expr.h
-INCLUDES = -I@srcdir@/../include
+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++ -*- */
+/** assert.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_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.
+ ** 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++ -*- */
+/** command.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_COMMAND_H
+#define __CVC4_COMMAND_H
+
+namespace CVC4 {
+
+class Command { // distinct from Exprs
+};
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4_COMMAND_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** context.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_CONTEXT_H
+#define __CVC4_CONTEXT_H
+
+namespace CVC4 {
+
+class Context;
+
+class ContextManager {
+public:
+ void switchContext(Context);
+ Context snapshot();
+};/* class ContextManager */
+
+class ContextObject {
+public:
+ void snapshot();
+ void restore();
+};/* class ContextObject */
+
+template <class T>
+class CDO;
+
+template <class T>
+class CDMap;
+
+template <class T>
+class CDList;
+
+template <class T>
+class CDSet;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_CONTEXT_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** debug.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_DEBUG_H
+#define __CVC4_DEBUG_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_DEBUG_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** decision_engine.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_DECISION_ENGINE_H
+#define __CVC4_DECISION_ENGINE_H
+
+#include "core/literal.h"
+
+namespace CVC4 {
+
+// In terms of abstraction, this is below (and provides services to)
+// PropEngine.
+
+/**
+ * A decision mechanism for the next decision.
+ */
+class DecisionEngine {
+public:
+ /**
+ * Get the next decision.
+ */
+ virtual Literal nextDecision() = 0;
+
+ // TODO: design decision: decision engine should be notified of
+ // propagated lits, and also why(?) (so that it can make decisions
+ // based on the utility of various theories and various theory
+ // literals). How? Maybe TheoryEngine has a backdoor into
+ // DecisionEngine "behind the back" of the PropEngine?
+
+};/* class DecisionEngine */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_DECISION_ENGINE_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** 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_EXCEPTION_H
+#define __CVC4_EXCEPTION_H
+
+#include <string>
+#include <iostream>
+
+namespace CVC4 {
+
+ class Exception {
+ protected:
+ std::string d_msg;
+ public:
+ // Constructors
+ Exception(): d_msg("Unknown exception") { }
+ Exception(const std::string& msg): d_msg(msg) { }
+ Exception(const char* msg): d_msg(msg) { }
+ // Destructor
+ virtual ~Exception() { }
+ // NON-VIRTUAL METHODs for setting and printing the error message
+ void setMessage(const std::string& msg) { d_msg = msg; }
+ // Printing: feel free to redefine toString(). When inherited,
+ // it's recommended that this method print the type of exception
+ // before the actual message.
+ virtual std::string toString() const { return d_msg; }
+ // No need to overload operator<< for the inherited classes
+ friend std::ostream& operator<<(std::ostream& os, const Exception& e);
+
+ }; // end of class Exception
+
+ inline std::ostream& operator<<(std::ostream& os, const Exception& e) {
+ return os << e.toString();
+ }
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_EXCEPTION_H */
** Reference-counted encapsulation of a pointer to an expression.
**/
-#include "expr.h"
-#include "expr_value.h"
-#include "expr_builder.h"
+#include "cvc4_expr.h"
+#include "core/expr_value.h"
+#include "core/expr_builder.h"
namespace CVC4 {
--- /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 */
** Expression manager implementation.
**/
-#include <vector>
-#include "expr.h"
-#include "kind.h"
+#include "core/expr_builder.h"
+#include "core/expr_manager.h"
+#include "core/cvc4_expr.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); }
- */
-};
+__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 */
** reference count on ExprValue instances and
**/
-#include "expr_value.h"
+#include "core/expr_value.h"
namespace CVC4 {
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;
}
--- /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++ -*- */
+/** literal.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_LITERAL_H
+#define __CVC4_LITERAL_H
+
+namespace CVC4 {
+
+class Literal;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_LITERAL_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** model.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_MODEL_H
+#define __CVC4_MODEL_H
+
+namespace CVC4 {
+
+class Model {
+};/* class Model */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_MODEL_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
+/********************* -*- C++ -*- */
+/** prop_engine.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_PROP_ENGINE_H
+#define __CVC4_PROP_ENGINE_H
+
+#include "core/cvc4_expr.h"
+#include "core/decision_engine.h"
+#include "core/theory_engine.h"
+
+namespace CVC4 {
+
+// In terms of abstraction, this is below (and provides services to)
+// Prover and above (and requires the services of) a specific
+// propositional solver, DPLL or otherwise.
+
+class PropEngine {
+ DecisionEngine* d_de;
+
+public:
+ /**
+ * Create a PropEngine with a particular decision and theory engine.
+ */
+ PropEngine(DecisionEngine*, TheoryEngine*);
+
+ /**
+ * Converts to CNF if necessary.
+ */
+ void solve(Expr);
+
+};/* class PropEngine */
+
+}
+
+#endif /* __CVC4_PROP_ENGINE_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** prover.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_PROVER_H
+#define __CVC4_PROVER_H
+
+#include <vector>
+#include "core/cvc4_expr.h"
+#include "core/result.h"
+#include "core/model.h"
+
+// In terms of abstraction, this is below (and provides services to)
+// ValidityChecker and above (and requires the services of)
+// PropEngine.
+
+namespace CVC4 {
+
+// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
+// hood): use a type parameter and have check() delegate, or subclass
+// Prover and override check()?
+//
+// Probably better than that is to have a configuration object that
+// indicates which passes are desired. The configuration occurs
+// elsewhere (and can even occur at runtime). A simple "pass manager"
+// of sorts determines check()'s behavior.
+//
+// The CNF conversion can go on in PropEngine.
+
+class Prover {
+ /** Current set of assertions. */
+ // TODO: make context-aware to handle user-level push/pop.
+ std::vector<Expr> d_assertList;
+
+private:
+ /**
+ * Pre-process an Expr. This is expected to be highly-variable,
+ * with a lot of "source-level configurability" to add multiple
+ * passes over the Expr. TODO: may need to specify a LEVEL of
+ * preprocessing (certain contexts need more/less ?).
+ */
+ void preprocess(Expr);
+
+ /**
+ * Adds a formula to the current context.
+ */
+ void addFormula(Expr);
+
+ /**
+ * Full check of consistency in current context. Returns true iff
+ * consistent.
+ */
+ Result check();
+
+ /**
+ * Quick check of consistency in current context: calls
+ * processAssertionList() then look for inconsistency (based only on
+ * that).
+ */
+ Result quickCheck();
+
+ /**
+ * Process the assertion list: for literals and conjunctions of
+ * literals, assert to T-solver.
+ */
+ void processAssertionList();
+
+public:
+ /**
+ * Add a formula to the current context: preprocess, do per-theory
+ * setup, use processAssertionList(), asserting to T-solver for
+ * literals and conjunction of literals. Returns false iff
+ * inconsistent.
+ */
+ Result assert(Expr);
+
+ /**
+ * Add a formula to the current context and call check(). Returns
+ * true iff consistent.
+ */
+ Result query(Expr);
+
+ /**
+ * Simplify a formula without doing "much" work. Requires assist
+ * from the SAT Engine.
+ */
+ Expr simplify(Expr);
+
+ /**
+ * Get a (counter)model (only if preceded by a SAT or INVALID query.
+ */
+ Model getModel();
+
+ /**
+ * Push a user-level context.
+ */
+ void push();
+
+ /**
+ * Pop a user-level context. Throws an exception if nothing to pop.
+ */
+ void pop();
+};/* class Prover */
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4_PROVER_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** result.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_RESULT_H
+#define __CVC4_RESULT_H
+
+namespace CVC4 {
+
+// TODO: perhaps best to templatize Result on its Kind (SAT/Validity),
+// but this requires doing the same for Prover and needs discussion.
+
+// TODO: subclass to provide models, etc. This is really just
+// intended as a three-valued response code.
+
+/**
+ * Three-valued, immutable SMT result, with optional explanation.
+ */
+class Result {
+public:
+ enum SAT {
+ UNSAT = 0,
+ SAT = 1,
+ SAT_UNKNOWN = 2
+ };
+
+ enum Validity {
+ INVALID = 0,
+ VALID = 1,
+ VALIDITY_UNKNOWN = 2
+ };
+
+ enum UnknownExplanation {
+ REQUIRES_FULL_CHECK,
+ INCOMPLETE,
+ TIMEOUT,
+ BAIL,
+ OTHER
+ };
+
+private:
+ enum SAT d_sat;
+ enum Validity d_validity;
+ enum { TYPE_SAT, TYPE_VALIDITY } d_which;
+
+public:
+ Result(enum SAT);
+ Result(enum Validity);
+
+ enum SAT isSAT();
+ enum Validity isValid();
+ enum UnknownExplanation whyUnknown();
+
+};/* class Result */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_RESULT_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** sat.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_SAT_H
+#define __CVC4_SAT_H
+
+namespace CVC4 {
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4_SAT_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** theory.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_THEORY_H
+#define __CVC4_THEORY_H
+
+#include "core/cvc4_expr.h"
+#include "core/literal.h"
+
+namespace CVC4 {
+
+/**
+ * Base class for T-solvers. Abstract DPLL(T).
+ */
+class Theory {
+public:
+ /**
+ * Subclasses of Theory may add additional efforts. DO NOT CHECK
+ * equality with one of these values (e.g. if STANDARD xxx) but
+ * rather use range checks (or use the helper functions below).
+ * Normally we call QUICK_CHECK or STANDARD; at the leaves we call
+ * with MAX_EFFORT.
+ */
+ enum Effort {
+ MIN_EFFORT = 0,
+ QUICK_CHECK = 10,
+ STANDARD = 50,
+ FULL_EFFORT = 100
+ };/* enum Effort */
+
+ // TODO add compiler annotation "constant function" here
+ static bool minEffortOnly(Effort e) { return e == MIN_EFFORT; }
+ static bool quickCheckOrMore(Effort e) { return e >= QUICK_CHECK; }
+ static bool quickCheckOnly(Effort e) { return e >= QUICK_CHECK && e < STANDARD; }
+ static bool standardEffortOrMore(Effort e) { return e >= STANDARD; }
+ static bool standardEffortOnly(Effort e) { return e >= STANDARD && e < FULL_EFFORT; }
+ static bool fullEffort(Effort e) { return e >= FULL_EFFORT; }
+
+ /**
+ * Prepare for an Expr.
+ */
+ virtual void setup(Expr) = 0;
+
+ /**
+ * Assert a literal in the current context.
+ */
+ virtual void assert(Literal) = 0;
+
+ /**
+ * Check the current assignment's consistency. Return false iff inconsistent.
+ */
+ virtual bool check(Effort level = FULL_EFFORT) = 0;
+
+ /**
+ * T-propagate new literal assignments in the current context.
+ */
+ // TODO design decision: instead of returning a set of literals
+ // here, perhaps we have an interface back into the prop engine
+ // where we assert directly. we might sometimes unknowingly assert
+ // something clearly inconsistent (esp. in a parallel context).
+ // This would allow the PropEngine to cancel our further work since
+ // we're already inconsistent---also could strategize dynamically on
+ // whether enough theory prop work has occurred.
+ virtual void propagate(Effort level = FULL_EFFORT) = 0;
+
+ /**
+ * Return an explanation for the literal (which was previously propagated by this theory)..
+ */
+ virtual Expr explain(Literal) = 0;
+
+};/* class Theory */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_THEORY_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** theory_engine.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_THEORY_ENGINE_H
+#define __CVC4_THEORY_ENGINE_H
+
+namespace CVC4 {
+
+// In terms of abstraction, this is below (and provides services to)
+// PropEngine.
+
+/**
+ * This is essentially an abstraction for a collection of theories. A
+ * TheoryEngine provides services to a PropEngine, making various
+ * T-solvers look like a single unit to the propositional part of
+ * CVC4.
+ */
+class TheoryEngine {
+public:
+};/* class TheoryEngine */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_THEORY_ENGINE_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** unique_id.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_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++ -*- */
-/** assert.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_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.
- ** 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 "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++ -*- */
-/** command.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_COMMAND_H
-#define __CVC4_COMMAND_H
-
-namespace CVC4 {
-
-class Command { // distinct from Exprs
-};
-
-} /* CVC4 namespace */
-
-#endif /* __CVC4_COMMAND_H */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** context.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_CONTEXT_H
-#define __CVC4_CONTEXT_H
-
-namespace CVC4 {
-
-class Context;
-
-class ContextManager {
-public:
- void switchContext(Context);
- Context snapshot();
-};/* class ContextManager */
-
-class ContextObject {
-public:
- void snapshot();
- void restore();
-};/* class ContextObject */
-
-template <class T>
-class CDO;
-
-template <class T>
-class CDMap;
-
-template <class T>
-class CDList;
-
-template <class T>
-class CDSet;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_CONTEXT_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** vc.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_VC_H
+#define __CVC4_VC_H
+
+#include "command.h"
+#include "cvc4_expr.h"
+
+/* TODO provide way of querying whether you fall into a fragment /
+ * returning what fragment you're in */
+
+// In terms of abstraction, this is below (and provides services to)
+// users using the library interface, and also the parser for the main
+// CVC4 binary. It is above (and requires the services of) the Prover
+// class.
+
+namespace CVC4 {
+
+/**
+ * User-visible (library) interface to CVC4.
+ */
+class ValidityChecker {
+ // on entry to the validity checker interface, need to set up
+ // current state (ExprManager::d_current etc.)
+public:
+ void doCommand(Command);
+
+ void query(Expr);
+};
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4_VC_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** expr.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.
+ **
+ ** Reference-counted encapsulation of a pointer to an expression.
+ **/
+
+#ifndef __CVC4_EXPR_H
+#define __CVC4_EXPR_H
+
+#include <vector>
+#include <stdint.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*);
+
+public:
+ Expr(const Expr&);
+
+ /** Destructor. Decrements the reference count and, if zero,
+ * collects the ExprValue. */
+ ~Expr();
+
+ Expr& operator=(const Expr&);
+
+ /** Access to the encapsulated expression.
+ * @return the encapsulated expression. */
+ ExprValue* operator->();
+
+ /** Const access to the encapsulated expression.
+ * @return the encapsulated expression [const]. */
+ const ExprValue* operator->() const;
+
+ uint64_t hash() const;
+
+ Expr eqExpr(const Expr& right) const;
+ Expr notExpr() const;
+ Expr negate() const; // avoid double-negatives
+ Expr andExpr(const Expr& right) const;
+ Expr orExpr(const Expr& right) const;
+ Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const;
+ Expr iffExpr(const Expr& right) const;
+ Expr impExpr(const Expr& right) const;
+ Expr xorExpr(const Expr& right) const;
+ Expr skolemExpr(int i) const;
+ Expr substExpr(const std::vector<Expr>& oldTerms,
+ const std::vector<Expr>& newTerms) const;
+
+ static Expr null() { return s_null; }
+
+ friend class ExprBuilder;
+};/* class Expr */
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4_EXPR_H */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** debug.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_DEBUG_H
-#define __CVC4_DEBUG_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_DEBUG_H */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** decision_engine.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_DECISION_ENGINE_H
-#define __CVC4_DECISION_ENGINE_H
-
-#include "literal.h"
-
-namespace CVC4 {
-
-// In terms of abstraction, this is below (and provides services to)
-// PropEngine.
-
-/**
- * A decision mechanism for the next decision.
- */
-class DecisionEngine {
-public:
- /**
- * Get the next decision.
- */
- virtual Literal nextDecision() = 0;
-
- // TODO: design decision: decision engine should be notified of
- // propagated lits, and also why(?) (so that it can make decisions
- // based on the utility of various theories and various theory
- // literals). How? Maybe TheoryEngine has a backdoor into
- // DecisionEngine "behind the back" of the PropEngine?
-
-};/* class DecisionEngine */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_DECISION_ENGINE_H */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** 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_EXCEPTION_H
-#define __CVC4_EXCEPTION_H
-
-#include <string>
-#include <iostream>
-
-namespace CVC4 {
-
- class Exception {
- protected:
- std::string d_msg;
- public:
- // Constructors
- Exception(): d_msg("Unknown exception") { }
- Exception(const std::string& msg): d_msg(msg) { }
- Exception(const char* msg): d_msg(msg) { }
- // Destructor
- virtual ~Exception() { }
- // NON-VIRTUAL METHODs for setting and printing the error message
- void setMessage(const std::string& msg) { d_msg = msg; }
- // Printing: feel free to redefine toString(). When inherited,
- // it's recommended that this method print the type of exception
- // before the actual message.
- virtual std::string toString() const { return d_msg; }
- // No need to overload operator<< for the inherited classes
- friend std::ostream& operator<<(std::ostream& os, const Exception& e);
-
- }; // end of class Exception
-
- inline std::ostream& operator<<(std::ostream& os, const Exception& e) {
- return os << e.toString();
- }
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_EXCEPTION_H */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** expr.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.
- **
- ** Reference-counted encapsulation of a pointer to an expression.
- **/
-
-#ifndef __CVC4_EXPR_H
-#define __CVC4_EXPR_H
-
-#include <vector>
-#include <stdint.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*);
-
-public:
- Expr(const Expr&);
-
- /** Destructor. Decrements the reference count and, if zero,
- * collects the ExprValue. */
- ~Expr();
-
- Expr& operator=(const Expr&);
-
- /** Access to the encapsulated expression.
- * @return the encapsulated expression. */
- ExprValue* operator->();
-
- /** Const access to the encapsulated expression.
- * @return the encapsulated expression [const]. */
- const ExprValue* operator->() const;
-
- uint64_t hash() const;
-
- Expr eqExpr(const Expr& right) const;
- Expr notExpr() const;
- Expr negate() const; // avoid double-negatives
- Expr andExpr(const Expr& right) const;
- Expr orExpr(const Expr& right) const;
- Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const;
- Expr iffExpr(const Expr& right) const;
- Expr impExpr(const Expr& right) const;
- Expr xorExpr(const Expr& right) const;
- Expr skolemExpr(int i) const;
- Expr substExpr(const std::vector<Expr>& oldTerms,
- const std::vector<Expr>& newTerms) const;
-
- static Expr null() { return s_null; }
-};/* class Expr */
-
-} /* CVC4 namespace */
-
-#endif /* __CVC4_EXPR_H */
+++ /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 "config.h"
-#include "context.h"
-#include "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.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 "expr_manager.h"
-#include "kind.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 {
- ExprValue* u_arr[10];
- std::vector<Expr>* u_vec;
- } d_children;
-
-public:
-
- ExprBuilder();
- ExprBuilder(const Expr&);
- ExprBuilder(const 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.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 "expr.h"
-#include "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.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 "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];
-
- 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 {
- AND,
- OR,
- XOR,
- NOT,
- PLUS,
- MINUS,
- ITE,
- IFF,
- SKOLEM,
- SUBST
-};/* enum Kind */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_KIND_H */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** literal.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_LITERAL_H
-#define __CVC4_LITERAL_H
-
-namespace CVC4 {
-
-class Literal;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_LITERAL_H */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** model.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_MODEL_H
-#define __CVC4_MODEL_H
-
-namespace CVC4 {
-
-class Model {
-};/* class Model */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_MODEL_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 "exception.h"
-#include "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 "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
-/********************* -*- C++ -*- */
-/** prop_engine.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_PROP_ENGINE_H
-#define __CVC4_PROP_ENGINE_H
-
-#include "expr.h"
-#include "decision_engine.h"
-#include "theory_engine.h"
-
-namespace CVC4 {
-
-// In terms of abstraction, this is below (and provides services to)
-// Prover and above (and requires the services of) a specific
-// propositional solver, DPLL or otherwise.
-
-class PropEngine {
- DecisionEngine* d_de;
-
-public:
- /**
- * Create a PropEngine with a particular decision and theory engine.
- */
- PropEngine(DecisionEngine*, TheoryEngine*);
-
- /**
- * Converts to CNF if necessary.
- */
- void solve(Expr);
-
-};/* class PropEngine */
-
-}
-
-#endif /* __CVC4_PROP_ENGINE_H */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** prover.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_PROVER_H
-#define __CVC4_PROVER_H
-
-#include <vector>
-#include "expr.h"
-#include "result.h"
-#include "model.h"
-
-// In terms of abstraction, this is below (and provides services to)
-// ValidityChecker and above (and requires the services of)
-// PropEngine.
-
-namespace CVC4 {
-
-// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
-// hood): use a type parameter and have check() delegate, or subclass
-// Prover and override check()?
-//
-// Probably better than that is to have a configuration object that
-// indicates which passes are desired. The configuration occurs
-// elsewhere (and can even occur at runtime). A simple "pass manager"
-// of sorts determines check()'s behavior.
-//
-// The CNF conversion can go on in PropEngine.
-
-class Prover {
- /** Current set of assertions. */
- // TODO: make context-aware to handle user-level push/pop.
- std::vector<Expr> d_assertList;
-
-private:
- /**
- * Pre-process an Expr. This is expected to be highly-variable,
- * with a lot of "source-level configurability" to add multiple
- * passes over the Expr. TODO: may need to specify a LEVEL of
- * preprocessing (certain contexts need more/less ?).
- */
- void preprocess(Expr);
-
- /**
- * Adds a formula to the current context.
- */
- void addFormula(Expr);
-
- /**
- * Full check of consistency in current context. Returns true iff
- * consistent.
- */
- Result check();
-
- /**
- * Quick check of consistency in current context: calls
- * processAssertionList() then look for inconsistency (based only on
- * that).
- */
- Result quickCheck();
-
- /**
- * Process the assertion list: for literals and conjunctions of
- * literals, assert to T-solver.
- */
- void processAssertionList();
-
-public:
- /**
- * Add a formula to the current context: preprocess, do per-theory
- * setup, use processAssertionList(), asserting to T-solver for
- * literals and conjunction of literals. Returns false iff
- * inconsistent.
- */
- Result assert(Expr);
-
- /**
- * Add a formula to the current context and call check(). Returns
- * true iff consistent.
- */
- Result query(Expr);
-
- /**
- * Simplify a formula without doing "much" work. Requires assist
- * from the SAT Engine.
- */
- Expr simplify(Expr);
-
- /**
- * Get a (counter)model (only if preceded by a SAT or INVALID query.
- */
- Model getModel();
-
- /**
- * Push a user-level context.
- */
- void push();
-
- /**
- * Pop a user-level context. Throws an exception if nothing to pop.
- */
- void pop();
-};/* class Prover */
-
-} /* CVC4 namespace */
-
-#endif /* __CVC4_PROVER_H */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** result.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_RESULT_H
-#define __CVC4_RESULT_H
-
-namespace CVC4 {
-
-// TODO: perhaps best to templatize Result on its Kind (SAT/Validity),
-// but this requires doing the same for Prover and needs discussion.
-
-// TODO: subclass to provide models, etc. This is really just
-// intended as a three-valued response code.
-
-/**
- * Three-valued, immutable SMT result, with optional explanation.
- */
-class Result {
-public:
- enum SAT {
- UNSAT = 0,
- SAT = 1,
- SAT_UNKNOWN = 2
- };
-
- enum Validity {
- INVALID = 0,
- VALID = 1,
- VALIDITY_UNKNOWN = 2
- };
-
- enum UnknownExplanation {
- REQUIRES_FULL_CHECK,
- INCOMPLETE,
- TIMEOUT,
- BAIL,
- OTHER
- };
-
-private:
- enum SAT d_sat;
- enum Validity d_validity;
- enum { TYPE_SAT, TYPE_VALIDITY } d_which;
-
-public:
- Result(enum SAT);
- Result(enum Validity);
-
- enum SAT isSAT();
- enum Validity isValid();
- enum UnknownExplanation whyUnknown();
-
-};/* class Result */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_RESULT_H */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** sat.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_SAT_H
-#define __CVC4_SAT_H
-
-namespace CVC4 {
-
-} /* CVC4 namespace */
-
-#endif /* __CVC4_SAT_H */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** theory.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_THEORY_H
-#define __CVC4_THEORY_H
-
-#include "expr.h"
-#include "literal.h"
-
-namespace CVC4 {
-
-/**
- * Base class for T-solvers. Abstract DPLL(T).
- */
-class Theory {
-public:
- /**
- * Subclasses of Theory may add additional efforts. DO NOT CHECK
- * equality with one of these values (e.g. if STANDARD xxx) but
- * rather use range checks (or use the helper functions below).
- * Normally we call QUICK_CHECK or STANDARD; at the leaves we call
- * with MAX_EFFORT.
- */
- enum Effort {
- MIN_EFFORT = 0,
- QUICK_CHECK = 10,
- STANDARD = 50,
- FULL_EFFORT = 100
- };/* enum Effort */
-
- // TODO add compiler annotation "constant function" here
- static bool minEffortOnly(Effort e) { return e == MIN_EFFORT; }
- static bool quickCheckOrMore(Effort e) { return e >= QUICK_CHECK; }
- static bool quickCheckOnly(Effort e) { return e >= QUICK_CHECK && e < STANDARD; }
- static bool standardEffortOrMore(Effort e) { return e >= STANDARD; }
- static bool standardEffortOnly(Effort e) { return e >= STANDARD && e < FULL_EFFORT; }
- static bool fullEffort(Effort e) { return e >= FULL_EFFORT; }
-
- /**
- * Prepare for an Expr.
- */
- virtual void setup(Expr) = 0;
-
- /**
- * Assert a literal in the current context.
- */
- virtual void assert(Literal) = 0;
-
- /**
- * Check the current assignment's consistency. Return false iff inconsistent.
- */
- virtual bool check(Effort level = FULL_EFFORT) = 0;
-
- /**
- * T-propagate new literal assignments in the current context.
- */
- // TODO design decision: instead of returning a set of literals
- // here, perhaps we have an interface back into the prop engine
- // where we assert directly. we might sometimes unknowingly assert
- // something clearly inconsistent (esp. in a parallel context).
- // This would allow the PropEngine to cancel our further work since
- // we're already inconsistent---also could strategize dynamically on
- // whether enough theory prop work has occurred.
- virtual void propagate(Effort level = FULL_EFFORT) = 0;
-
- /**
- * Return an explanation for the literal (which was previously propagated by this theory)..
- */
- virtual Expr explain(Literal) = 0;
-
-};/* class Theory */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_THEORY_H */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** theory_engine.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_THEORY_ENGINE_H
-#define __CVC4_THEORY_ENGINE_H
-
-namespace CVC4 {
-
-// In terms of abstraction, this is below (and provides services to)
-// PropEngine.
-
-/**
- * This is essentially an abstraction for a collection of theories. A
- * TheoryEngine provides services to a PropEngine, making various
- * T-solvers look like a single unit to the propositional part of
- * CVC4.
- */
-class TheoryEngine {
-public:
-};/* class TheoryEngine */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_THEORY_ENGINE_H */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** unique_id.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_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.
- ** 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_VC_H
-#define __CVC4_VC_H
-
-#include "command.h"
-#include "expr.h"
-
-/* TODO provide way of querying whether you fall into a fragment /
- * returning what fragment you're in */
-
-// In terms of abstraction, this is below (and provides services to)
-// users using the library interface, and also the parser for the main
-// CVC4 binary. It is above (and requires the services of) the Prover
-// class.
-
-namespace CVC4 {
-
-/**
- * User-visible (library) interface to CVC4.
- */
-class ValidityChecker {
- // on entry to the validity checker interface, need to set up
- // current state (ExprManager::d_current etc.)
-public:
- void doCommand(Command);
-
- void query(Expr);
-};
-
-} /* CVC4 namespace */
-
-#endif /* __CVC4_VC_H */
-INCLUDES = -I@srcdir@/../include
+INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CXXFLAGS = -Wall
noinst_LIBRARIES = libparser.a
#include <iostream>
#include <sstream>
-#include "expr.h"
+#include "cvc4_expr.h"
#include "exception.h"
namespace CVC4 {
-INCLUDES = -I@srcdir@/../include
+INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CXXFLAGS = -Wall
SUBDIRS = minisat
projects / cvc5.git / commitdiff