diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-26 21:44:42 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-26 21:44:42 +0000 |
commit | 14c22833d05f632eb40eb68cc3c68345d891005c (patch) | |
tree | c596c6e91442a3393611e88b10dec3871992a207 /src | |
parent | 3311e8276fb6221d9e100be2b1eec88d8f119fef (diff) |
* test/unit/context/context_black.h: Test CDList<>. In particular,
test behavior of grow(), which was previously very broken, fixed by
Tim earlier this afternoon.
* add the notion of a "private header". Private header files (those
not intended for distribution) should now #include "cvc4_private.h"
(or "cvc4parser_private.h" for the parser code). When not actually
building libcvc4 (resp. libcvc4parser), or associated unit tests, a
warning is emitted by the preprocessor. This should make it easier
to notice (and disentangle early) any unwanted public/private
mixing. Currently the warning identifies a couple places where we
need to fix things.
* added directory infrastructure for arrays and BV theories.
* the Theory inheritance hierarchy makes some assumptions about the
way inheritance is done. These are checked at runtime when
CVC4_ASSERTIONS is on. See src/theory/theory.h's TheoryImpl<>
definition for details.
* src/theory/booleans/theory_bool.h, src/theory/booleans/theory_def.h,
src/theory/arith/theory_arith.h, src/theory/arith/theory_def.h,
src/theory/uf/theory_uf.h, src/theory/uf/theory_def.h,
src/parser/antlr_parser.h: minor code formatting fixes as per
policy.
* src/theory/uf/theory_uf.cpp: fix for non-debug builds.
* src/util/options.h, src/util/model.h, src/util/result.h,
src/expr/type.h: make CVC4_PUBLIC.
* src/util/decision_engine.h: no longer CVC4_PUBLIC.
* src/expr/expr_manager.cpp: ExprManager::booleanType() and
ExprManager::kindType() weren't returning a value ?! Fixed.
* src/expr/expr_manager.h, src/expr/node_manager.h: ExprManager no
longer depends on NodeManager (public/private interface mixing).
ExprManagerScope is an internal implementation detail, and is moved
to node_manager.h.
* src/expr/node.h: mark gdb debug routines as "used" so that GCC
always emits code for them (even though its static analysis shows
they're unused).
Diffstat (limited to 'src')
50 files changed, 449 insertions, 63 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 |