** Context class and context manager.
**/
+#include "cvc4_private.h"
+
#ifndef __CVC4__CONTEXT__CONTEXT_H
#define __CVC4__CONTEXT__CONTEXT_H
** for use by ContextManager.
**/
+#include "cvc4_private.h"
+
#ifndef __CVC4__CONTEXT__CONTEXT_MM_H
#define __CVC4__CONTEXT__CONTEXT_MM_H
** Node attributes.
**/
+#include "cvc4_private.h"
+
/* There are strong constraints on ordering of declarations of
* attributes and nodes due to template use */
#include "expr/node.h"
const BooleanType* ExprManager::booleanType() const {
NodeManagerScope nms(d_nodeManager);
- d_nodeManager->booleanType();
+ return d_nodeManager->booleanType();
}
const KindType* ExprManager::kindType() const {
NodeManagerScope nms(d_nodeManager);
- d_nodeManager->kindType();
+ return d_nodeManager->kindType();
}
Expr ExprManager::mkExpr(Kind kind) {
#include "cvc4_config.h"
#include "expr/kind.h"
-#include "expr/node_manager.h"
#include <vector>
namespace CVC4 {
class FunctionType;
class KindType;
class SmtEngine;
+class NodeManager;
class CVC4_PUBLIC ExprManager {
}/* CVC4 namespace */
-#include "expr/expr.h"
-
-namespace CVC4 {
-
-/**
- * A wrapper (essentially) for NodeManagerScope. Without this, we'd
- * need Expr to be a friend of ExprManager.
- */
-class ExprManagerScope {
- NodeManagerScope d_nms;
-public:
- inline ExprManagerScope(const Expr& e) :
- d_nms(e.getExprManager() == NULL ?
- NodeManager::currentNM() : e.getExprManager()->getNodeManager()) {
- }
-};
-
-}/* CVC4 namespace */
-
#endif /* __CVC4__EXPR_MANAGER_H */
** Reference-counted encapsulation of a pointer to node information.
**/
+#include "cvc4_private.h"
+
#include "expr/node_value.h"
#ifndef __CVC4__NODE_H
* to find the symbol, and use it, which is the first standard this code needs
* to meet. A cleaner solution is welcomed.
*/
-static void CVC4_PUBLIC debugPrintNode(const NodeTemplate<true>& n) {
+static void __attribute__((used)) debugPrintNode(const NodeTemplate<true>& n) {
n.printAst(Warning(), 0);
Warning().flush();
}
-static void CVC4_PUBLIC debugPrintTNode(const NodeTemplate<false>& n) {
+static void __attribute__((used)) debugPrintTNode(const NodeTemplate<false>& n) {
n.printAst(Warning(), 0);
Warning().flush();
}
** A builder interface for nodes.
**/
+#include "cvc4_private.h"
+
/* strong dependency; make sure node is included first */
#include "node.h"
** A manager for Nodes.
**/
+#include "cvc4_private.h"
+
/* circular dependency; force node.h first */
#include "expr/attribute.h"
#include "expr/node.h"
#include <ext/hash_set>
#include "expr/kind.h"
+#include "expr/expr.h"
namespace __gnu_cxx {
template<>
}
};
+/**
+ * A wrapper (essentially) for NodeManagerScope. Without this, we'd
+ * need Expr to be a friend of ExprManager.
+ */
+class ExprManagerScope {
+ NodeManagerScope d_nms;
+public:
+ inline ExprManagerScope(const Expr& e) :
+ d_nms(e.getExprManager() == NULL ?
+ NodeManager::currentNM() : e.getExprManager()->getNodeManager()) {
+ }
+};
+
template <class AttrKind>
inline typename AttrKind::value_type NodeManager::getAttribute(TNode n,
const AttrKind&) const {
** reference count on NodeValue instances and
**/
-/* this must be above the check for __CVC4__EXPR__NODE_VALUE_H */
-/* to resolve a circular dependency */
-//#include "expr/node.h"
+#include "cvc4_private.h"
#ifndef __CVC4__EXPR__NODE_VALUE_H
#define __CVC4__EXPR__NODE_VALUE_H
/**
* Class encapsulating CVC4 expression types.
*/
-class Type {
+class CVC4_PUBLIC Type {
public:
/** Comparision for equality */
bool operator==(const Type& t) const;
--- /dev/null
+/********************* */
+/** cvc4_private.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** #inclusion of this file marks a header as private and generates a
+ ** warning when the file is included improperly.
+ **/
+
+#ifndef __CVC4_PRIVATE_H
+#define __CVC4_PRIVATE_H
+
+#if ! (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST))
+# warning A private CVC4 header was included when not building the library or private unit test code.
+#endif /* ! (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) */
+
+#endif /* __CVC4_PRIVATE_H */
--- /dev/null
+/********************* */
+/** cvc4parser_private.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** #inclusion of this file marks a header as private and generates a
+ ** warning when the file is included improperly.
+ **/
+
+#ifndef __CVC4PARSER_PRIVATE_H
+#define __CVC4PARSER_PRIVATE_H
+
+#if ! (defined(__BUILDING_CVC4PARSERLIB) || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST))
+# warning A private CVC4 parser header was included when not building the parser library or private unit test code.
+#endif /* ! (__BUILDING_CVC4PARSERLIB || __BUILDING_CVC4PARSERLIB_UNIT_TEST) */
+
+#endif /* __CVC4PARSER_PRIVATE_H */
** Base for ANTLR parser classes.
**/
-#ifndef CVC4_PARSER_H_
-#define CVC4_PARSER_H_
+#include "cvc4parser_private.h"
+
+#ifndef __CVC4__PARSER__ANTLR_PARSER_H
+#define __CVC4__PARSER__ANTLR_PARSER_H
#include <vector>
#include <string>
Expr getSymbol(const std::string& var_name, SymbolType type);
};
-
-
-
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-#endif /* CVC4_PARSER_H_ */
+#endif /* __CVC4__PARSER__ANTLR_PARSER_H */
** A symbol table for the parsers' use.
**/
+#include "cvc4parser_private.h"
+
#ifndef __CVC4__PARSER__SYMBOL_TABLE_H
#define __CVC4__PARSER__SYMBOL_TABLE_H
** A type for describing possible CNF conversions.
**/
+#include "cvc4_private.h"
+
#ifndef __CVC4__CNF_CONVERSION_H
#define __CVC4__CNF_CONVERSION_H
** internals such as the representation and translation of
**/
+#include "cvc4_private.h"
+
#ifndef __CVC4__CNF_STREAM_H
#define __CVC4__CNF_STREAM_H
-
#include "expr/node.h"
#include "prop/sat.h"
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
+#include "cvc4_private.h"
+
#ifndef __CVC4__PROP__MINISAT__SOLVER_H
#define __CVC4__PROP__MINISAT__SOLVER_H
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
+#include "cvc4_private.h"
+
#ifndef __CVC4__PROP__MINISAT__SOLVERTYPES_H
#define __CVC4__PROP__MINISAT__SOLVERTYPES_H
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
+#include "cvc4_private.h"
+
#ifndef __CVC4__PROP__MINISAT__SIMP_SOLVER_H
#define __CVC4__PROP__MINISAT__SIMP_SOLVER_H
** between CVC4's SMT infrastructure and the SAT solver.
**/
+#include "cvc4_private.h"
+
#ifndef __CVC4__PROP_ENGINE_H
#define __CVC4__PROP_ENGINE_H
** SAT Solver.
**/
+#include "cvc4_private.h"
+
#ifndef __CVC4__PROP__SAT_H
#define __CVC4__PROP__SAT_H
#include "expr/expr_manager.h"
#include "util/result.h"
#include "util/model.h"
-#include "util/decision_engine.h"
+
+#include "expr/node.h"
// In terms of abstraction, this is below (and provides services to)
// ValidityChecker and above (and requires the services of)
namespace CVC4 {
+namespace context {
+ class Context;
+}
+
class Command;
class Options;
class TheoryEngine;
+class DecisionEngine;
namespace prop {
class PropEngine;
libtheory_la_LIBADD = \
@builddir@/booleans/libbooleans.la \
@builddir@/uf/libuf.la \
- @builddir@/arith/libarith.la
+ @builddir@/arith/libarith.la \
+ @builddir@/arrays/libarrays.la \
+ @builddir@/bv/libbv.la
EXTRA_DIST = \
@srcdir@/theoryof_table.h \
dist-hook: @srcdir@/theoryof_table.h
MAINTAINERCLEANFILES = @srcdir@/theoryof_table.h
-SUBDIRS = booleans uf arith
+SUBDIRS = booleans uf arith arrays bv
+/********************* */
+/** theory_arith.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** Arithmetic theory.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__THEORY_ARITH_H
+#define __CVC4__THEORY__ARITH__THEORY_ARITH_H
+
#include "theory/theory.h"
+#include "context/context.h"
namespace CVC4 {
namespace theory {
void explain(TNode n, Effort e) { Unimplemented(); }
};
-}
-}
-}
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+#endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_H */
+/********************* */
+/** theory_def.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** Definition for TheoryARITH (for purposes of linking to the
+ ** theory-code-finding mechanisms in the parent directory).
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__THEORY_DEF_H
+#define __CVC4__THEORY__ARITH__THEORY_DEF_H
+
#include "theory/arith/theory_arith.h"
namespace CVC4 {
}
}
}
+
+#endif /* __CVC4__THEORY__ARITH__THEORY_DEF_H */
--- /dev/null
+topdir = ../../..
+srcdir = src/theory/arrays
+
+include $(topdir)/Makefile.subdir
--- /dev/null
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../../include -I@srcdir@/../..
+AM_CXXFLAGS = -Wall -fvisibility=hidden
+
+noinst_LTLIBRARIES = libarrays.la
+
+libarrays_la_SOURCES = \
+ theory_def.h \
+ theory_arrays.h
+
+EXTRA_DIST = kinds
--- /dev/null
+/********************* */
+/** theory_arrays.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** Theory of arrays.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
+#define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
+
+#include "theory/theory.h"
+#include "context/context.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+class TheoryArrays : public TheoryImpl<TheoryArrays> {
+public:
+ TheoryArrays(context::Context* c, OutputChannel& out) :
+ TheoryImpl<TheoryArrays>(c, out) {
+ }
+
+ void preRegisterTerm(TNode n) { Unimplemented(); }
+ void registerTerm(TNode n) { Unimplemented(); }
+ void check(Effort e) { Unimplemented(); }
+ void propagate(Effort e) { Unimplemented(); }
+ void explain(TNode n, Effort e) { Unimplemented(); }
+};
+
+}/* CVC4::theory::arrays namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H */
--- /dev/null
+/********************* */
+/** theory_def.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** Definition for TheoryARRAYS (for purposes of linking to the
+ ** theory-code-finding mechanisms in the parent directory).
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARRAYS__THEORY_DEF_H
+#define __CVC4__THEORY__ARRAYS__THEORY_DEF_H
+
+#include "theory/arrays/theory_arrays.h"
+
+namespace CVC4 {
+ namespace theory {
+ namespace arrays {
+ typedef TheoryArrays TheoryARRAYS;
+ }
+ }
+}
+
+#endif /* __CVC4__THEORY__ARRAYS__THEORY_DEF_H */
+/********************* */
+/** theory_bool.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** The theory of booleans.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BOOLEANS__THEORY_BOOL_H
+#define __CVC4__THEORY__BOOLEANS__THEORY_BOOL_H
+
#include "theory/theory.h"
#include "context/context.h"
void explain(TNode n, Effort e) { Unimplemented(); }
};
-}
-}
-}
+}/* CVC4::theory::booleans namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+#endif /* __CVC4__THEORY__BOOLEANS__THEORY_BOOL_H */
+/********************* */
+/** theory_def.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** Definition for TheoryBOOLEANS (for purposes of linking to the
+ ** theory-code-finding mechanisms in the parent directory).
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BOOLEANS__THEORY_DEF_H
+#define __CVC4__THEORY__BOOLEANS__THEORY_DEF_H
+
#include "theory/booleans/theory_bool.h"
namespace CVC4 {
}
}
}
+
+#endif /* __CVC4__THEORY__BOOLEANS__THEORY_DEF_H */
--- /dev/null
+topdir = ../../..
+srcdir = src/theory/bv
+
+include $(topdir)/Makefile.subdir
--- /dev/null
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../../include -I@srcdir@/../..
+AM_CXXFLAGS = -Wall -fvisibility=hidden
+
+noinst_LTLIBRARIES = libbv.la
+
+libbv_la_SOURCES = \
+ theory_def.h \
+ theory_bv.h
+
+EXTRA_DIST = kinds
--- /dev/null
+/********************* */
+/** theory_bv.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** Bitvector theory.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BV__THEORY_BV_H
+#define __CVC4__THEORY__BV__THEORY_BV_H
+
+#include "theory/theory.h"
+#include "context/context.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+class TheoryBV : public TheoryImpl<TheoryBV> {
+public:
+ TheoryBV(context::Context* c, OutputChannel& out) :
+ TheoryImpl<TheoryBV>(c, out) {
+ }
+
+ void preRegisterTerm(TNode n) { Unimplemented(); }
+ void registerTerm(TNode n) { Unimplemented(); }
+ void check(Effort e) { Unimplemented(); }
+ void propagate(Effort e) { Unimplemented(); }
+ void explain(TNode n, Effort e) { Unimplemented(); }
+};
+
+}/* CVC4::theory::bv namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__BV__THEORY_BV_H */
--- /dev/null
+/********************* */
+/** theory_def.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** Definition for TheoryBV (for purposes of linking to the
+ ** theory-code-finding mechanisms in the parent directory).
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BV__THEORY_DEF_H
+#define __CVC4__THEORY__BV__THEORY_DEF_H
+
+#include "theory/bv/theory_bv.h"
+
+#endif /* __CVC4__THEORY__BV__THEORY_DEF_H */
** The theory output channel interface.
**/
+#include "cvc4_private.h"
+
#ifndef __CVC4__THEORY__OUTPUT_CHANNEL_H
#define __CVC4__THEORY__OUTPUT_CHANNEL_H
** Base of the theory interface.
**/
+#include "cvc4_private.h"
+
#ifndef __CVC4__THEORY__THEORY_H
#define __CVC4__THEORY__THEORY_H
template <class T>
Node TheoryImpl<T>::get() {
- Warning.printf("testing %s == %s\n", typeid(*this).name(), typeid(T).name());
- /*Assert(typeid(*this) == typeid(T),
- "Improper Theory inheritance chain detected.");*/
+ Assert(typeid(*this) == typeid(T),
+ "Improper Theory inheritance chain detected.");
Assert( !d_facts.empty(),
"Theory::get() called with assertion queue empty!" );
** The theory engine.
**/
+#include "cvc4_private.h"
+
#ifndef __CVC4__THEORY_ENGINE_H
#define __CVC4__THEORY_ENGINE_H
#include "expr/node.h"
#include "theory/theory.h"
-#include "theory/uf/theory_uf.h"
#include "theory/theoryof_table.h"
+#include "theory/booleans/theory_bool.h"
+#include "theory/uf/theory_uf.h"
+#include "theory/arith/theory_arith.h"
+#include "theory/arrays/theory_arrays.h"
+#include "theory/bv/theory_bv.h"
+
namespace CVC4 {
class SmtEngine;
theory::booleans::TheoryBool d_bool;
theory::uf::TheoryUF d_uf;
theory::arith::TheoryArith d_arith;
+ theory::arrays::TheoryArrays d_arrays;
+ theory::bv::TheoryBV d_bv;
public:
d_theoryOut(),
d_bool(ctxt, d_theoryOut),
d_uf(ctxt, d_theoryOut),
- d_arith(ctxt, d_theoryOut) {
+ d_arith(ctxt, d_theoryOut),
+ d_arrays(ctxt, d_theoryOut),
+ d_bv(ctxt, d_theoryOut) {
d_theoryOut.setEngine(*this);
theoryOfTable.registerTheory(&d_bool);
theoryOfTable.registerTheory(&d_uf);
theoryOfTable.registerTheory(&d_arith);
+ theoryOfTable.registerTheory(&d_arrays);
+ theoryOfTable.registerTheory(&d_bv);
}
/**
** The theoryOf table.
**/
+#include "cvc4_private.h"
+
#ifndef __CVC4__THEORY__THEORYOF_TABLE_H
#define __CVC4__THEORY__THEORYOF_TABLE_H
** Currently keeps a context dependent watch list.
**/
+#include "cvc4_private.h"
+
#ifndef __CVC4__THEORY__UF__ECDATA_H
#define __CVC4__THEORY__UF__ECDATA_H
-namespace CVC4 {
- namespace theory {
- namespace uf {
- class TheoryUF;
- }
- }
-}
+/********************* */
+/** theory_def.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** Definition for TheoryUF (for purposes of linking to the
+ ** theory-code-finding mechanisms in the parent directory).
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__UF__THEORY_DEF_H
+#define __CVC4__THEORY__UF__THEORY_DEF_H
+
+#include "theory/uf/theory_uf.h"
+
+#endif /* __CVC4__THEORY__UF__THEORY_DEF_H */
void TheoryUF::registerTerm(TNode n){
d_registered.push_back(n);
+#ifdef CVC4_DEBUG
n.printAst(Warning());
+#endif /* CVC4_DEBUG */
ECData* ecN;
**
**/
+#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__THEORY_UF_H
-#define __CVC4__THEORY__THEORY_UF_H
+#ifndef __CVC4__THEORY__UF__THEORY_UF_H
+#define __CVC4__THEORY__UF__THEORY_UF_H
#include "expr/node.h"
#include "expr/attribute.h"
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__THEORY_UF_H */
+#endif /* __CVC4__THEORY__UF__THEORY_UF_H */
** A decision engine for CVC4.
**/
+#include "cvc4_private.h"
+
#ifndef __CVC4__DECISION_ENGINE_H
#define __CVC4__DECISION_ENGINE_H
/**
* A decision mechanism for the next decision.
*/
-class CVC4_PUBLIC DecisionEngine {
+class DecisionEngine {
public:
/**
* Destructor.
namespace CVC4 {
-class Model {
+class CVC4_PUBLIC Model {
};/* class Model */
}/* CVC4 namespace */
namespace CVC4 {
-struct Options {
+struct CVC4_PUBLIC Options {
std::string binary_name;
/**
* Three-valued, immutable SMT result, with optional explanation.
*/
-class Result {
+class CVC4_PUBLIC Result {
public:
enum SAT {
UNSAT = 0,
** A mechanism for getting a compile-time unique ID.
**/
+#include "cvc4_private.h"
+
#ifndef __CVC4__UNIQUE_ID_H
#define __CVC4__UNIQUE_ID_H
AM_CXXFLAGS = $(TEST_CXXFLAGS)
AM_LDFLAGS = $(TEST_LDFLAGS)
-AM_CXXFLAGS_WHITE = -fno-access-control
-AM_CXXFLAGS_BLACK =
+AM_CXXFLAGS_WHITE = -fno-access-control -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST
+AM_CXXFLAGS_BLACK = -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST
AM_CXXFLAGS_PUBLIC =
AM_LDFLAGS_WHITE = \
@abs_top_builddir@/src/parser/libcvc4parser_noinst.la \
// d_context->pop();
}
+ // test at different sizes. this triggers grow() behavior differently.
+ // grow() is completely broken in revision 256; fix forthcoming by Tim
+ void testCDList10() { listTest(10); }
+ void testCDList15() { listTest(15); }
+ void testCDList20() { listTest(20); }
+ void testCDList35() { listTest(35); }
+ void testCDList50() { listTest(50); }
+ void testCDList99() { listTest(99); }
+
+ void listTest(int N) {
+ CDList<int> list(d_context);
+
+ TS_ASSERT(list.empty());
+ for(int i = 0; i < N; ++i) {
+ TS_ASSERT(list.size() == i);
+ list.push_back(i);
+ TS_ASSERT(!list.empty());
+ TS_ASSERT(list.back() == i);
+ int i2 = 0;
+ for(CDList<int>::const_iterator j = list.begin();
+ j != list.end();
+ ++j) {
+ TS_ASSERT(*j == i2++);
+ }
+ }
+ TS_ASSERT(list.size() == N);
+
+ for(int i = 0; i < N; ++i) {
+ TS_ASSERT(list[i] == i);
+ }
+ }
+
void tearDown() {
delete d_context;
}
projects / cvc5.git / commitdiff