diff options
52 files changed, 483 insertions, 65 deletions
diff --git a/src/context/context.h b/src/context/context.h index a12eb11a5..6462cccaa 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -13,6 +13,8 @@ ** Context class and context manager. **/ +#include "cvc4_private.h" + #ifndef __CVC4__CONTEXT__CONTEXT_H #define __CVC4__CONTEXT__CONTEXT_H diff --git a/src/context/context_mm.h b/src/context/context_mm.h index c51498979..c4e5aba4f 100644 --- a/src/context/context_mm.h +++ b/src/context/context_mm.h @@ -14,6 +14,8 @@ ** for use by ContextManager. **/ +#include "cvc4_private.h" + #ifndef __CVC4__CONTEXT__CONTEXT_MM_H #define __CVC4__CONTEXT__CONTEXT_MM_H diff --git a/src/expr/attribute.h b/src/expr/attribute.h index d7514d50c..522427c03 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -13,6 +13,8 @@ ** 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" diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index 993bf3483..232a903e9 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -40,12 +40,12 @@ ExprManager::~ExprManager() { 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) { diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index 3ea1b581a..67fa0664a 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -18,7 +18,6 @@ #include "cvc4_config.h" #include "expr/kind.h" -#include "expr/node_manager.h" #include <vector> namespace CVC4 { @@ -29,6 +28,7 @@ class BooleanType; class FunctionType; class KindType; class SmtEngine; +class NodeManager; class CVC4_PUBLIC ExprManager { @@ -126,24 +126,5 @@ private: }/* 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 */ diff --git a/src/expr/node.h b/src/expr/node.h index 25f0b7453..fe2016747 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -13,6 +13,8 @@ ** Reference-counted encapsulation of a pointer to node information. **/ +#include "cvc4_private.h" + #include "expr/node_value.h" #ifndef __CVC4__NODE_H @@ -690,12 +692,12 @@ template<bool ref_count> * 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(); } diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 03936c89a..c1b2a87d2 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -13,6 +13,8 @@ ** A builder interface for nodes. **/ +#include "cvc4_private.h" + /* strong dependency; make sure node is included first */ #include "node.h" diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 9d2b0947e..00fcf52c4 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -13,6 +13,8 @@ ** A manager for Nodes. **/ +#include "cvc4_private.h" + /* circular dependency; force node.h first */ #include "expr/attribute.h" #include "expr/node.h" @@ -25,6 +27,7 @@ #include <ext/hash_set> #include "expr/kind.h" +#include "expr/expr.h" namespace __gnu_cxx { template<> @@ -155,6 +158,19 @@ public: } }; +/** + * 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 { diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 85b8a6d60..e8435df26 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -17,9 +17,7 @@ ** 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 diff --git a/src/expr/type.h b/src/expr/type.h index 77994eec5..7009ed504 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -28,7 +28,7 @@ class NodeManager; /** * Class encapsulating CVC4 expression types. */ -class Type { +class CVC4_PUBLIC Type { public: /** Comparision for equality */ bool operator==(const Type& t) const; diff --git a/src/include/cvc4_private.h b/src/include/cvc4_private.h new file mode 100644 index 000000000..df5dd4a0b --- /dev/null +++ b/src/include/cvc4_private.h @@ -0,0 +1,24 @@ +/********************* */ +/** 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 */ diff --git a/src/include/cvc4parser_private.h b/src/include/cvc4parser_private.h new file mode 100644 index 000000000..72d942ef0 --- /dev/null +++ b/src/include/cvc4parser_private.h @@ -0,0 +1,24 @@ +/********************* */ +/** 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 */ diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index 3fd94f82b..8f1f3fa1d 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -13,8 +13,10 @@ ** 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> @@ -342,10 +344,7 @@ private: Expr getSymbol(const std::string& var_name, SymbolType type); }; - - - }/* CVC4::parser namespace */ }/* CVC4 namespace */ -#endif /* CVC4_PARSER_H_ */ +#endif /* __CVC4__PARSER__ANTLR_PARSER_H */ diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h index 1f43dbda6..bfa38ec28 100644 --- a/src/parser/symbol_table.h +++ b/src/parser/symbol_table.h @@ -13,6 +13,8 @@ ** A symbol table for the parsers' use. **/ +#include "cvc4parser_private.h" + #ifndef __CVC4__PARSER__SYMBOL_TABLE_H #define __CVC4__PARSER__SYMBOL_TABLE_H diff --git a/src/prop/cnf_conversion.h b/src/prop/cnf_conversion.h index 4ddfd3c06..d66e721db 100644 --- a/src/prop/cnf_conversion.h +++ b/src/prop/cnf_conversion.h @@ -13,6 +13,8 @@ ** A type for describing possible CNF conversions. **/ +#include "cvc4_private.h" + #ifndef __CVC4__CNF_CONVERSION_H #define __CVC4__CNF_CONVERSION_H diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 83a6aa68f..da3f7b1ed 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -19,10 +19,11 @@ ** 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" diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 5e51e5f5a..44499246e 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, 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 diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h index 8860693e6..fd6a78ab0 100644 --- a/src/prop/minisat/core/SolverTypes.h +++ b/src/prop/minisat/core/SolverTypes.h @@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, 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 diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index f9e9b0387..223b21998 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, 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 diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 4ea5e3b78..f57161fde 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -14,6 +14,8 @@ ** between CVC4's SMT infrastructure and the SAT solver. **/ +#include "cvc4_private.h" + #ifndef __CVC4__PROP_ENGINE_H #define __CVC4__PROP_ENGINE_H diff --git a/src/prop/sat.h b/src/prop/sat.h index a9696162a..65752f20b 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -13,6 +13,8 @@ ** SAT Solver. **/ +#include "cvc4_private.h" + #ifndef __CVC4__PROP__SAT_H #define __CVC4__PROP__SAT_H diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index afb62fe6a..594676416 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -23,7 +23,8 @@ #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) @@ -31,9 +32,14 @@ namespace CVC4 { +namespace context { + class Context; +} + class Command; class Options; class TheoryEngine; +class DecisionEngine; namespace prop { class PropEngine; diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 951dbeb78..d71ae842f 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -15,7 +15,9 @@ libtheory_la_SOURCES = \ 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 \ @@ -36,4 +38,4 @@ BUILT_SOURCES = @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 diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 5b596afd4..973651f7a 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -1,4 +1,25 @@ +/********************* */ +/** 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 { @@ -17,7 +38,8 @@ public: void explain(TNode n, Effort e) { Unimplemented(); } }; -} -} -} +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ +#endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_H */ diff --git a/src/theory/arith/theory_def.h b/src/theory/arith/theory_def.h index 9b01a458e..da4239724 100644 --- a/src/theory/arith/theory_def.h +++ b/src/theory/arith/theory_def.h @@ -1,3 +1,24 @@ +/********************* */ +/** 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 { @@ -7,3 +28,5 @@ namespace CVC4 { } } } + +#endif /* __CVC4__THEORY__ARITH__THEORY_DEF_H */ diff --git a/src/theory/arrays/Makefile b/src/theory/arrays/Makefile new file mode 100644 index 000000000..bce529db0 --- /dev/null +++ b/src/theory/arrays/Makefile @@ -0,0 +1,4 @@ +topdir = ../../.. +srcdir = src/theory/arrays + +include $(topdir)/Makefile.subdir diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am new file mode 100644 index 000000000..af3a28b3b --- /dev/null +++ b/src/theory/arrays/Makefile.am @@ -0,0 +1,12 @@ +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 diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/src/theory/arrays/kinds diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h new file mode 100644 index 000000000..ec3b88ccd --- /dev/null +++ b/src/theory/arrays/theory_arrays.h @@ -0,0 +1,45 @@ +/********************* */ +/** 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 */ diff --git a/src/theory/arrays/theory_def.h b/src/theory/arrays/theory_def.h new file mode 100644 index 000000000..68eec69e8 --- /dev/null +++ b/src/theory/arrays/theory_def.h @@ -0,0 +1,32 @@ +/********************* */ +/** 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 */ diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index 26e5a69fb..5196bb018 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -1,3 +1,23 @@ +/********************* */ +/** 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" @@ -18,7 +38,8 @@ public: void explain(TNode n, Effort e) { Unimplemented(); } }; -} -} -} +}/* CVC4::theory::booleans namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ +#endif /* __CVC4__THEORY__BOOLEANS__THEORY_BOOL_H */ diff --git a/src/theory/booleans/theory_def.h b/src/theory/booleans/theory_def.h index 37aacb353..626431593 100644 --- a/src/theory/booleans/theory_def.h +++ b/src/theory/booleans/theory_def.h @@ -1,3 +1,24 @@ +/********************* */ +/** 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 { @@ -7,3 +28,5 @@ namespace CVC4 { } } } + +#endif /* __CVC4__THEORY__BOOLEANS__THEORY_DEF_H */ diff --git a/src/theory/bv/Makefile b/src/theory/bv/Makefile new file mode 100644 index 000000000..797408368 --- /dev/null +++ b/src/theory/bv/Makefile @@ -0,0 +1,4 @@ +topdir = ../../.. +srcdir = src/theory/bv + +include $(topdir)/Makefile.subdir diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am new file mode 100644 index 000000000..54622bf9a --- /dev/null +++ b/src/theory/bv/Makefile.am @@ -0,0 +1,12 @@ +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 diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/src/theory/bv/kinds diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h new file mode 100644 index 000000000..fbb62545d --- /dev/null +++ b/src/theory/bv/theory_bv.h @@ -0,0 +1,45 @@ +/********************* */ +/** 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 */ diff --git a/src/theory/bv/theory_def.h b/src/theory/bv/theory_def.h new file mode 100644 index 000000000..e16adb94a --- /dev/null +++ b/src/theory/bv/theory_def.h @@ -0,0 +1,24 @@ +/********************* */ +/** 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 */ diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index efd2911ef..54fa71808 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -13,6 +13,8 @@ ** The theory output channel interface. **/ +#include "cvc4_private.h" + #ifndef __CVC4__THEORY__OUTPUT_CHANNEL_H #define __CVC4__THEORY__OUTPUT_CHANNEL_H diff --git a/src/theory/theory.h b/src/theory/theory.h index f5b1e9b44..efa67d6c4 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -13,6 +13,8 @@ ** Base of the theory interface. **/ +#include "cvc4_private.h" + #ifndef __CVC4__THEORY__THEORY_H #define __CVC4__THEORY__THEORY_H @@ -282,9 +284,8 @@ protected: 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!" ); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 7d630f667..076ea4d2d 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -13,14 +13,21 @@ ** 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; @@ -70,6 +77,8 @@ class TheoryEngine { 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: @@ -81,11 +90,15 @@ 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); } /** diff --git a/src/theory/theoryof_table_prologue.h b/src/theory/theoryof_table_prologue.h index 5f8c28723..47fd2d9b2 100644 --- a/src/theory/theoryof_table_prologue.h +++ b/src/theory/theoryof_table_prologue.h @@ -13,6 +13,8 @@ ** The theoryOf table. **/ +#include "cvc4_private.h" + #ifndef __CVC4__THEORY__THEORYOF_TABLE_H #define __CVC4__THEORY__THEORYOF_TABLE_H diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/ecdata.h index 9b87aa6cb..5bb3a57bd 100644 --- a/src/theory/uf/ecdata.h +++ b/src/theory/uf/ecdata.h @@ -14,6 +14,8 @@ ** Currently keeps a context dependent watch list. **/ +#include "cvc4_private.h" + #ifndef __CVC4__THEORY__UF__ECDATA_H #define __CVC4__THEORY__UF__ECDATA_H diff --git a/src/theory/uf/theory_def.h b/src/theory/uf/theory_def.h index 8e3f5e9f1..b5cdda4ec 100644 --- a/src/theory/uf/theory_def.h +++ b/src/theory/uf/theory_def.h @@ -1,7 +1,24 @@ -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 */ diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 0c58d45e4..0c0559bb0 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -43,7 +43,9 @@ void TheoryUF::preRegisterTerm(TNode n){ void TheoryUF::registerTerm(TNode n){ d_registered.push_back(n); +#ifdef CVC4_DEBUG n.printAst(Warning()); +#endif /* CVC4_DEBUG */ ECData* ecN; diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 34b6719d7..6efdf27c0 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -13,9 +13,10 @@ ** **/ +#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" @@ -150,4 +151,4 @@ typedef expr::Attribute<EquivClass, ECData* /*, ECCleanupFcn*/> ECAttr; } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__THEORY_UF_H */ +#endif /* __CVC4__THEORY__UF__THEORY_UF_H */ diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h index 72943ee99..ac9fc5ffd 100644 --- a/src/util/decision_engine.h +++ b/src/util/decision_engine.h @@ -13,6 +13,8 @@ ** A decision engine for CVC4. **/ +#include "cvc4_private.h" + #ifndef __CVC4__DECISION_ENGINE_H #define __CVC4__DECISION_ENGINE_H @@ -27,7 +29,7 @@ namespace CVC4 { /** * A decision mechanism for the next decision. */ -class CVC4_PUBLIC DecisionEngine { +class DecisionEngine { public: /** * Destructor. diff --git a/src/util/model.h b/src/util/model.h index 65c919dd2..d2a51e447 100644 --- a/src/util/model.h +++ b/src/util/model.h @@ -18,7 +18,7 @@ namespace CVC4 { -class Model { +class CVC4_PUBLIC Model { };/* class Model */ }/* CVC4 namespace */ diff --git a/src/util/options.h b/src/util/options.h index 404700a85..d2b19a20b 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -22,7 +22,7 @@ namespace CVC4 { -struct Options { +struct CVC4_PUBLIC Options { std::string binary_name; diff --git a/src/util/result.h b/src/util/result.h index 49ba7c697..7557cece8 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -29,7 +29,7 @@ namespace CVC4 { /** * Three-valued, immutable SMT result, with optional explanation. */ -class Result { +class CVC4_PUBLIC Result { public: enum SAT { UNSAT = 0, diff --git a/src/util/unique_id.h b/src/util/unique_id.h index 244b8a5dd..54e56da96 100644 --- a/src/util/unique_id.h +++ b/src/util/unique_id.h @@ -13,6 +13,8 @@ ** A mechanism for getting a compile-time unique ID. **/ +#include "cvc4_private.h" + #ifndef __CVC4__UNIQUE_ID_H #define __CVC4__UNIQUE_ID_H diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 5290381c3..f3f23a400 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -38,8 +38,8 @@ AM_CPPFLAGS = \ 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 \ diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h index 4084c91fc..64ad2d7f7 100644 --- a/test/unit/context/context_black.h +++ b/test/unit/context/context_black.h @@ -57,6 +57,38 @@ public: // 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; } |