summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2010-02-26 21:44:42 +0000
committerMorgan Deters <mdeters@gmail.com>2010-02-26 21:44:42 +0000
commit14c22833d05f632eb40eb68cc3c68345d891005c (patch)
treec596c6e91442a3393611e88b10dec3871992a207 /src/theory
parent3311e8276fb6221d9e100be2b1eec88d8f119fef (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/theory')
-rw-r--r--src/theory/Makefile.am6
-rw-r--r--src/theory/arith/theory_arith.h28
-rw-r--r--src/theory/arith/theory_def.h23
-rw-r--r--src/theory/arrays/Makefile4
-rw-r--r--src/theory/arrays/Makefile.am12
-rw-r--r--src/theory/arrays/kinds0
-rw-r--r--src/theory/arrays/theory_arrays.h45
-rw-r--r--src/theory/arrays/theory_def.h32
-rw-r--r--src/theory/booleans/theory_bool.h27
-rw-r--r--src/theory/booleans/theory_def.h23
-rw-r--r--src/theory/bv/Makefile4
-rw-r--r--src/theory/bv/Makefile.am12
-rw-r--r--src/theory/bv/kinds0
-rw-r--r--src/theory/bv/theory_bv.h45
-rw-r--r--src/theory/bv/theory_def.h24
-rw-r--r--src/theory/output_channel.h2
-rw-r--r--src/theory/theory.h7
-rw-r--r--src/theory/theory_engine.h17
-rw-r--r--src/theory/theoryof_table_prologue.h2
-rw-r--r--src/theory/uf/ecdata.h2
-rw-r--r--src/theory/uf/theory_def.h31
-rw-r--r--src/theory/uf/theory_uf.cpp2
-rw-r--r--src/theory/uf/theory_uf.h7
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback