diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/Makefile.am | 6 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 28 | ||||
-rw-r--r-- | src/theory/arith/theory_def.h | 23 | ||||
-rw-r--r-- | src/theory/arrays/Makefile | 4 | ||||
-rw-r--r-- | src/theory/arrays/Makefile.am | 12 | ||||
-rw-r--r-- | src/theory/arrays/kinds | 0 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 45 | ||||
-rw-r--r-- | src/theory/arrays/theory_def.h | 32 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool.h | 27 | ||||
-rw-r--r-- | src/theory/booleans/theory_def.h | 23 | ||||
-rw-r--r-- | src/theory/bv/Makefile | 4 | ||||
-rw-r--r-- | src/theory/bv/Makefile.am | 12 | ||||
-rw-r--r-- | src/theory/bv/kinds | 0 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 45 | ||||
-rw-r--r-- | src/theory/bv/theory_def.h | 24 | ||||
-rw-r--r-- | src/theory/output_channel.h | 2 | ||||
-rw-r--r-- | src/theory/theory.h | 7 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 17 | ||||
-rw-r--r-- | src/theory/theoryof_table_prologue.h | 2 | ||||
-rw-r--r-- | src/theory/uf/ecdata.h | 2 | ||||
-rw-r--r-- | src/theory/uf/theory_def.h | 31 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 2 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 7 |
23 files changed, 332 insertions, 23 deletions
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 */ |