+++ /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++ -*- */
-/** 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++ -*- */
-/** 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 */
+++ /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++ -*- */
-/** 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++ -*- */
-/** 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++ -*- */
+/** 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++ -*- */
+/** 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++ -*- */
+/** 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
+// SmtEngine 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 SmtEngine {
+ /** 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 SmtEngine */
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4_PROVER_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++ -*- */
+/** 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++ -*- */
+/** 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 */
--- /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++ -*- */
+/** 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++ -*- */
+/** 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 */
projects / cvc5.git / commitdiff