summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rwxr-xr-xconfigure4
-rw-r--r--configure.ac2
-rw-r--r--src/Makefile.am4
-rw-r--r--src/Makefile.in7
-rw-r--r--src/context/Makefile.am3
-rw-r--r--src/context/Makefile.in12
-rw-r--r--src/expr/Makefile.am8
-rw-r--r--src/expr/Makefile.in17
-rw-r--r--src/expr/attr_var_name.h36
-rw-r--r--src/expr/expr_attribute.h2
-rw-r--r--src/main/Makefile.am5
-rw-r--r--src/main/Makefile.in14
-rw-r--r--src/main/main.cpp18
-rw-r--r--src/prop/minisat/Makefile.am17
-rw-r--r--src/prop/minisat/Makefile.in17
-rw-r--r--src/smt/Makefile.am3
-rw-r--r--src/smt/Makefile.in12
-rw-r--r--src/theory/Makefile.am14
-rw-r--r--src/theory/Makefile.in381
-rw-r--r--src/theory/theory.cpp16
-rw-r--r--src/theory/theory_engine.cpp16
-rw-r--r--src/theory/uf/Makefile.am7
-rw-r--r--src/theory/uf/Makefile.in417
-rw-r--r--src/util/Assert.cpp2
-rw-r--r--src/util/Assert.h8
25 files changed, 948 insertions, 94 deletions
diff --git a/configure b/configure
index 61a9f64f9..ae26d8ef1 100755
--- a/configure
+++ b/configure
@@ -16374,7 +16374,7 @@ if test "$user_ldflags" = no; then
LDFLAGS="$CVC4LDFLAGS"
fi
-ac_config_files="$ac_config_files Makefile.builds Makefile contrib/Makefile doc/Makefile src/Makefile src/expr/Makefile src/smt/Makefile src/main/Makefile src/prop/minisat/Makefile src/prop/Makefile src/util/Makefile src/context/Makefile src/parser/Makefile src/parser/cvc/Makefile src/parser/smt/Makefile src/theory/Makefile test/Makefile test/regress/Makefile test/unit/Makefile"
+ac_config_files="$ac_config_files Makefile.builds Makefile contrib/Makefile doc/Makefile src/Makefile src/expr/Makefile src/smt/Makefile src/main/Makefile src/prop/minisat/Makefile src/prop/Makefile src/util/Makefile src/context/Makefile src/parser/Makefile src/parser/cvc/Makefile src/parser/smt/Makefile src/theory/Makefile src/theory/uf/Makefile test/Makefile test/regress/Makefile test/unit/Makefile"
cat >confcache <<\_ACEOF
@@ -17471,6 +17471,7 @@ do
"src/parser/cvc/Makefile") CONFIG_FILES="$CONFIG_FILES src/parser/cvc/Makefile" ;;
"src/parser/smt/Makefile") CONFIG_FILES="$CONFIG_FILES src/parser/smt/Makefile" ;;
"src/theory/Makefile") CONFIG_FILES="$CONFIG_FILES src/theory/Makefile" ;;
+ "src/theory/uf/Makefile") CONFIG_FILES="$CONFIG_FILES src/theory/uf/Makefile" ;;
"test/Makefile") CONFIG_FILES="$CONFIG_FILES test/Makefile" ;;
"test/regress/Makefile") CONFIG_FILES="$CONFIG_FILES test/regress/Makefile" ;;
"test/unit/Makefile") CONFIG_FILES="$CONFIG_FILES test/unit/Makefile" ;;
@@ -19035,7 +19036,6 @@ CPPFLAGS : $CPPFLAGS
CXXFLAGS : $CXXFLAGS
LDFLAGS : $LDFLAGS
-
Library releases : $CVC4_LIBRARY_RELEASE_CODE
libcvc4 version : $CVC4_LIBRARY_VERSION
libcvc4parser version: $CVC4_PARSER_LIBRARY_VERSION
diff --git a/configure.ac b/configure.ac
index 5c6629ca5..7ba7a2b67 100644
--- a/configure.ac
+++ b/configure.ac
@@ -348,6 +348,7 @@ AC_CONFIG_FILES([
src/parser/cvc/Makefile
src/parser/smt/Makefile
src/theory/Makefile
+ src/theory/uf/Makefile
test/Makefile
test/regress/Makefile
test/unit/Makefile
@@ -387,7 +388,6 @@ CPPFLAGS : $CPPFLAGS
CXXFLAGS : $CXXFLAGS
LDFLAGS : $LDFLAGS
-
Library releases : $CVC4_LIBRARY_RELEASE_CODE
libcvc4 version : $CVC4_LIBRARY_VERSION
libcvc4parser version: $CVC4_PARSER_LIBRARY_VERSION
diff --git a/src/Makefile.am b/src/Makefile.am
index 4ea07ea95..1db9d9ecf 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -32,8 +32,8 @@ libcvc4_la_LIBADD = \
@builddir@/context/libcontext.la \
@builddir@/prop/libprop.la \
@builddir@/prop/minisat/libminisat.la \
- @builddir@/smt/libsmt.la
-# @builddir@/theory/libtheory.la
+ @builddir@/smt/libsmt.la \
+ @builddir@/theory/libtheory.la
publicheaders = \
include/cvc4_config.h
diff --git a/src/Makefile.in b/src/Makefile.in
index a651482e6..fb902f2ce 100644
--- a/src/Makefile.in
+++ b/src/Makefile.in
@@ -76,7 +76,8 @@ LTLIBRARIES = $(lib_LTLIBRARIES)
libcvc4_la_DEPENDENCIES = @builddir@/util/libutil.la \
@builddir@/expr/libexpr.la @builddir@/context/libcontext.la \
@builddir@/prop/libprop.la \
- @builddir@/prop/minisat/libminisat.la @builddir@/smt/libsmt.la
+ @builddir@/prop/minisat/libminisat.la @builddir@/smt/libsmt.la \
+ @builddir@/theory/libtheory.la
am_libcvc4_la_OBJECTS =
libcvc4_la_OBJECTS = $(am_libcvc4_la_OBJECTS)
libcvc4_la_LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) \
@@ -299,9 +300,9 @@ libcvc4_la_LIBADD = \
@builddir@/context/libcontext.la \
@builddir@/prop/libprop.la \
@builddir@/prop/minisat/libminisat.la \
- @builddir@/smt/libsmt.la
+ @builddir@/smt/libsmt.la \
+ @builddir@/theory/libtheory.la
-# @builddir@/theory/libtheory.la
publicheaders = \
include/cvc4_config.h
diff --git a/src/context/Makefile.am b/src/context/Makefile.am
index d1e0d3c4b..eac088a9f 100644
--- a/src/context/Makefile.am
+++ b/src/context/Makefile.am
@@ -5,4 +5,5 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libcontext.la
libcontext_la_SOURCES = \
- context.cpp
+ context.cpp \
+ context.h
diff --git a/src/context/Makefile.in b/src/context/Makefile.in
index 99c69fa92..a7a000c3e 100644
--- a/src/context/Makefile.in
+++ b/src/context/Makefile.in
@@ -67,6 +67,15 @@ CXXLD = $(CXX)
CXXLINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
--mode=link $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) \
$(LDFLAGS) -o $@
+COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \
+ $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+LTCOMPILE = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+ --mode=compile $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
+ $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+CCLD = $(CC)
+LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+ --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \
+ $(LDFLAGS) -o $@
SOURCES = $(libcontext_la_SOURCES)
DIST_SOURCES = $(libcontext_la_SOURCES)
ETAGS = etags
@@ -211,7 +220,8 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden
AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libcontext.la
libcontext_la_SOURCES = \
- context.cpp
+ context.cpp \
+ context.h
all: all-am
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index df3c34094..630850387 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -5,6 +5,14 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libexpr.la
libexpr_la_SOURCES = \
+ attr_type.h \
+ attr_var_name.h \
+ expr.h \
+ expr_builder.h \
+ expr_value.h \
+ expr_manager.h \
+ expr_attribute.h \
+ kind.h \
expr.cpp \
expr_builder.cpp \
expr_manager.cpp \
diff --git a/src/expr/Makefile.in b/src/expr/Makefile.in
index 5dc5c677d..9d410cea8 100644
--- a/src/expr/Makefile.in
+++ b/src/expr/Makefile.in
@@ -68,6 +68,15 @@ CXXLD = $(CXX)
CXXLINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
--mode=link $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) \
$(LDFLAGS) -o $@
+COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \
+ $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+LTCOMPILE = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+ --mode=compile $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
+ $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+CCLD = $(CC)
+LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+ --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \
+ $(LDFLAGS) -o $@
SOURCES = $(libexpr_la_SOURCES)
DIST_SOURCES = $(libexpr_la_SOURCES)
ETAGS = etags
@@ -212,6 +221,14 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden
AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libexpr.la
libexpr_la_SOURCES = \
+ attr_type.h \
+ attr_var_name.h \
+ expr.h \
+ expr_builder.h \
+ expr_value.h \
+ expr_manager.h \
+ expr_attribute.h \
+ kind.h \
expr.cpp \
expr_builder.cpp \
expr_manager.cpp \
diff --git a/src/expr/attr_var_name.h b/src/expr/attr_var_name.h
new file mode 100644
index 000000000..a0780d575
--- /dev/null
+++ b/src/expr/attr_var_name.h
@@ -0,0 +1,36 @@
+/********************* -*- C++ -*- */
+/** attr_type.h
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ **/
+
+#ifndef __CVC4__EXPR__ATTR_VAR_NAME_H
+#define __CVC4__EXPR__ATTR_VAR_NAME_H
+
+#include "expr_attribute.h"
+
+namespace CVC4 {
+namespace expr {
+
+class VarName;
+
+// an "attribute type" for types
+// this is essentially a traits structure
+class VarName_attr {
+public:
+ enum { hash_value = 11 }; // could use typeid but then different on different machines/compiles
+ typedef Type value_type;//Expr?
+ static const Type_attr marker;
+};
+
+extern AttrTable<Type_attr> type_table;
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR__ATTR_TYPE_H */
diff --git a/src/expr/expr_attribute.h b/src/expr/expr_attribute.h
index 03140c4eb..b68a9d19d 100644
--- a/src/expr/expr_attribute.h
+++ b/src/expr/expr_attribute.h
@@ -12,8 +12,6 @@
#ifndef __CVC4__EXPR__EXPR_ATTRIBUTE_H
#define __CVC4__EXPR__EXPR_ATTRIBUTE_H
-// TODO WARNING this file needs work !
-
#include <stdint.h>
#include "config.h"
#include "context/context.h"
diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index 0992a434a..6b8ea928c 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -7,7 +7,10 @@ bin_PROGRAMS = cvc4
cvc4_SOURCES = \
main.cpp \
getopt.cpp \
- util.cpp
+ util.cpp \
+ main.h \
+ usage.h \
+ about.h
cvc4_LDADD = \
../parser/libcvc4parser.la \
diff --git a/src/main/Makefile.in b/src/main/Makefile.in
index 2df8a3368..6498610be 100644
--- a/src/main/Makefile.in
+++ b/src/main/Makefile.in
@@ -69,6 +69,15 @@ CXXLD = $(CXX)
CXXLINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
--mode=link $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) \
$(LDFLAGS) -o $@
+COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \
+ $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+LTCOMPILE = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+ --mode=compile $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
+ $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+CCLD = $(CC)
+LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+ --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \
+ $(LDFLAGS) -o $@
SOURCES = $(cvc4_SOURCES)
DIST_SOURCES = $(cvc4_SOURCES)
ETAGS = etags
@@ -214,7 +223,10 @@ AM_CPPFLAGS =
cvc4_SOURCES = \
main.cpp \
getopt.cpp \
- util.cpp
+ util.cpp \
+ main.h \
+ usage.h \
+ about.h
cvc4_LDADD = \
../parser/libcvc4parser.la \
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 8b59e6013..d9d3988f1 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -84,16 +84,26 @@ int main(int argc, char *argv[]) {
Warning.setStream(CVC4::null_os);
}
- const char* fname = inputFromStdin ? argv[firstArgIndex] : "stdin";
+ const char* fname;
+ istream* in;
+ ifstream* file;
+ if(inputFromStdin) {
+ fname = "stdin";
+ in = &cin;
+ } else {
+ fname = argv[firstArgIndex];
+ file = new ifstream(fname);
+ in = file;
+ }
// Create the parser
Parser* parser;
switch(options.lang) {
case Options::LANG_SMTLIB:
- parser = new SmtParser(&exprMgr, cin, fname);
+ parser = new SmtParser(&exprMgr, *in, fname);
break;
case Options::LANG_CVC4:
- parser = new CvcParser(&exprMgr, cin, fname);
+ parser = new CvcParser(&exprMgr, *in, fname);
break;
case Options::LANG_AUTO:
cerr << "Auto language detection not supported yet." << endl;
@@ -117,6 +127,8 @@ int main(int argc, char *argv[]) {
// Remove the parser
delete parser;
+
+ delete file;
} catch(OptionException& e) {
if(options.smtcomp_mode)
cout << "unknown" << endl;
diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am
index cef9a4c1e..f066f8669 100644
--- a/src/prop/minisat/Makefile.am
+++ b/src/prop/minisat/Makefile.am
@@ -8,7 +8,15 @@ libminisat_la_SOURCES = \
core/Solver.h \
core/SolverTypes.h \
simp/SimpSolver.C \
- simp/SimpSolver.h
+ simp/SimpSolver.h \
+ mtl/Alg.h \
+ mtl/BasicHeap.h \
+ mtl/BoxedVec.h \
+ mtl/Heap.h \
+ mtl/Map.h \
+ mtl/Queue.h \
+ mtl/Sort.h \
+ mtl/Vec.h
EXTRA_DIST = \
core/Main.C \
@@ -17,11 +25,4 @@ EXTRA_DIST = \
simp/Makefile \
README \
LICENSE \
- mtl/Heap.h \
- mtl/Map.h \
- mtl/Queue.h \
- mtl/Alg.h \
- mtl/Sort.h \
- mtl/BasicHeap.h \
- mtl/BoxedVec.h \
mtl/template.mk
diff --git a/src/prop/minisat/Makefile.in b/src/prop/minisat/Makefile.in
index 646389c80..e77369348 100644
--- a/src/prop/minisat/Makefile.in
+++ b/src/prop/minisat/Makefile.in
@@ -224,7 +224,15 @@ libminisat_la_SOURCES = \
core/Solver.h \
core/SolverTypes.h \
simp/SimpSolver.C \
- simp/SimpSolver.h
+ simp/SimpSolver.h \
+ mtl/Alg.h \
+ mtl/BasicHeap.h \
+ mtl/BoxedVec.h \
+ mtl/Heap.h \
+ mtl/Map.h \
+ mtl/Queue.h \
+ mtl/Sort.h \
+ mtl/Vec.h
EXTRA_DIST = \
core/Main.C \
@@ -233,13 +241,6 @@ EXTRA_DIST = \
simp/Makefile \
README \
LICENSE \
- mtl/Heap.h \
- mtl/Map.h \
- mtl/Queue.h \
- mtl/Alg.h \
- mtl/Sort.h \
- mtl/BasicHeap.h \
- mtl/BoxedVec.h \
mtl/template.mk
all: all-am
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index b8fc81961..b3637b6d9 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -5,4 +5,5 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libsmt.la
libsmt_la_SOURCES = \
- smt_engine.cpp
+ smt_engine.cpp \
+ smt_engine.h
diff --git a/src/smt/Makefile.in b/src/smt/Makefile.in
index c318c2fc1..c3c47037d 100644
--- a/src/smt/Makefile.in
+++ b/src/smt/Makefile.in
@@ -67,6 +67,15 @@ CXXLD = $(CXX)
CXXLINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
--mode=link $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) \
$(LDFLAGS) -o $@
+COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \
+ $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+LTCOMPILE = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+ --mode=compile $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
+ $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+CCLD = $(CC)
+LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+ --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \
+ $(LDFLAGS) -o $@
SOURCES = $(libsmt_la_SOURCES)
DIST_SOURCES = $(libsmt_la_SOURCES)
ETAGS = etags
@@ -211,7 +220,8 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden
AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libsmt.la
libsmt_la_SOURCES = \
- smt_engine.cpp
+ smt_engine.cpp \
+ smt_engine.h
all: all-am
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index 60d11ba88..f8e9908c9 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -2,9 +2,15 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/..
AM_CXXFLAGS = -Wall -fvisibility=hidden
AM_CPPFLAGS = -D__BUILDING_CVC4LIB
-#noinst_LTLIBRARIES = libtheory.la
+noinst_LTLIBRARIES = libtheory.la
-#libtheory_la_LIBADD =
-# @builddir@/uf/libuf.la
+libtheory_la_SOURCES = \
+ theory_engine.h \
+ theory_engine.cpp \
+ theory.h \
+ theory.cpp
-#SUBDIRS = uf
+libtheory_la_LIBADD = \
+ @builddir@/uf/libuf.la
+
+SUBDIRS = uf
diff --git a/src/theory/Makefile.in b/src/theory/Makefile.in
index a7424237d..15b0f0b21 100644
--- a/src/theory/Makefile.in
+++ b/src/theory/Makefile.in
@@ -14,6 +14,7 @@
# PARTICULAR PURPOSE.
@SET_MAKE@
+
VPATH = @srcdir@
pkgdatadir = $(datadir)/@PACKAGE@
pkgincludedir = $(includedir)/@PACKAGE@
@@ -49,9 +50,75 @@ mkinstalldirs = $(install_sh) -d
CONFIG_HEADER = $(top_builddir)/config.h
CONFIG_CLEAN_FILES =
CONFIG_CLEAN_VPATH_FILES =
-SOURCES =
-DIST_SOURCES =
+LTLIBRARIES = $(noinst_LTLIBRARIES)
+libtheory_la_DEPENDENCIES = @builddir@/uf/libuf.la
+am_libtheory_la_OBJECTS = theory_engine.lo theory.lo
+libtheory_la_OBJECTS = $(am_libtheory_la_OBJECTS)
+DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
+depcomp = $(SHELL) $(top_srcdir)/config/depcomp
+am__depfiles_maybe = depfiles
+am__mv = mv -f
+CXXCOMPILE = $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
+ $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS)
+LTCXXCOMPILE = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+ --mode=compile $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
+ $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS)
+CXXLD = $(CXX)
+CXXLINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+ --mode=link $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) \
+ $(LDFLAGS) -o $@
+COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \
+ $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+LTCOMPILE = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+ --mode=compile $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
+ $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+CCLD = $(CC)
+LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+ --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \
+ $(LDFLAGS) -o $@
+SOURCES = $(libtheory_la_SOURCES)
+DIST_SOURCES = $(libtheory_la_SOURCES)
+RECURSIVE_TARGETS = all-recursive check-recursive dvi-recursive \
+ html-recursive info-recursive install-data-recursive \
+ install-dvi-recursive install-exec-recursive \
+ install-html-recursive install-info-recursive \
+ install-pdf-recursive install-ps-recursive install-recursive \
+ installcheck-recursive installdirs-recursive pdf-recursive \
+ ps-recursive uninstall-recursive
+RECURSIVE_CLEAN_TARGETS = mostlyclean-recursive clean-recursive \
+ distclean-recursive maintainer-clean-recursive
+AM_RECURSIVE_TARGETS = $(RECURSIVE_TARGETS:-recursive=) \
+ $(RECURSIVE_CLEAN_TARGETS:-recursive=) tags TAGS ctags CTAGS \
+ distdir
+ETAGS = etags
+CTAGS = ctags
+DIST_SUBDIRS = $(SUBDIRS)
DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST)
+am__relativize = \
+ dir0=`pwd`; \
+ sed_first='s,^\([^/]*\)/.*$$,\1,'; \
+ sed_rest='s,^[^/]*/*,,'; \
+ sed_last='s,^.*/\([^/]*\)$$,\1,'; \
+ sed_butlast='s,/*[^/]*$$,,'; \
+ while test -n "$$dir1"; do \
+ first=`echo "$$dir1" | sed -e "$$sed_first"`; \
+ if test "$$first" != "."; then \
+ if test "$$first" = ".."; then \
+ dir2=`echo "$$dir0" | sed -e "$$sed_last"`/"$$dir2"; \
+ dir0=`echo "$$dir0" | sed -e "$$sed_butlast"`; \
+ else \
+ first2=`echo "$$dir2" | sed -e "$$sed_first"`; \
+ if test "$$first2" = "$$first"; then \
+ dir2=`echo "$$dir2" | sed -e "$$sed_rest"`; \
+ else \
+ dir2="../$$dir2"; \
+ fi; \
+ dir0="$$dir0"/"$$first"; \
+ fi; \
+ fi; \
+ dir1=`echo "$$dir1" | sed -e "$$sed_rest"`; \
+ done; \
+ reldir="$$dir2"
ACLOCAL = @ACLOCAL@
AMTAR = @AMTAR@
ANTLR = @ANTLR@
@@ -189,9 +256,21 @@ top_srcdir = @top_srcdir@
INCLUDES = -I@srcdir@/../include -I@srcdir@/..
AM_CXXFLAGS = -Wall -fvisibility=hidden
AM_CPPFLAGS = -D__BUILDING_CVC4LIB
-all: all-am
+noinst_LTLIBRARIES = libtheory.la
+libtheory_la_SOURCES = \
+ theory_engine.h \
+ theory_engine.cpp \
+ theory.h \
+ theory.cpp
+
+libtheory_la_LIBADD = \
+ @builddir@/uf/libuf.la
+
+SUBDIRS = uf
+all: all-recursive
.SUFFIXES:
+.SUFFIXES: .cpp .lo .o .obj
$(srcdir)/Makefile.in: $(srcdir)/Makefile.am $(am__configure_deps)
@for dep in $?; do \
case '$(am__configure_deps)' in \
@@ -223,17 +302,187 @@ $(ACLOCAL_M4): $(am__aclocal_m4_deps)
cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
$(am__aclocal_m4_deps):
+clean-noinstLTLIBRARIES:
+ -test -z "$(noinst_LTLIBRARIES)" || rm -f $(noinst_LTLIBRARIES)
+ @list='$(noinst_LTLIBRARIES)'; for p in $$list; do \
+ dir="`echo $$p | sed -e 's|/[^/]*$$||'`"; \
+ test "$$dir" != "$$p" || dir=.; \
+ echo "rm -f \"$${dir}/so_locations\""; \
+ rm -f "$${dir}/so_locations"; \
+ done
+libtheory.la: $(libtheory_la_OBJECTS) $(libtheory_la_DEPENDENCIES)
+ $(CXXLINK) $(libtheory_la_OBJECTS) $(libtheory_la_LIBADD) $(LIBS)
+
+mostlyclean-compile:
+ -rm -f *.$(OBJEXT)
+
+distclean-compile:
+ -rm -f *.tab.c
+
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/theory.Plo@am__quote@
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/theory_engine.Plo@am__quote@
+
+.cpp.o:
+@am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
+@am__fastdepCXX_TRUE@ $(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Po
+@AMDEP_TRUE@@am__fastdepCXX_FALSE@ source='$<' object='$@' libtool=no @AMDEPBACKSLASH@
+@AMDEP_TRUE@@am__fastdepCXX_FALSE@ DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
+@am__fastdepCXX_FALSE@ $(CXXCOMPILE) -c -o $@ $<
+
+.cpp.obj:
+@am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ `$(CYGPATH_W) '$<'`
+@am__fastdepCXX_TRUE@ $(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Po
+@AMDEP_TRUE@@am__fastdepCXX_FALSE@ source='$<' object='$@' libtool=no @AMDEPBACKSLASH@
+@AMDEP_TRUE@@am__fastdepCXX_FALSE@ DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
+@am__fastdepCXX_FALSE@ $(CXXCOMPILE) -c -o $@ `$(CYGPATH_W) '$<'`
+
+.cpp.lo:
+@am__fastdepCXX_TRUE@ $(LTCXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
+@am__fastdepCXX_TRUE@ $(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Plo
+@AMDEP_TRUE@@am__fastdepCXX_FALSE@ source='$<' object='$@' libtool=yes @AMDEPBACKSLASH@
+@AMDEP_TRUE@@am__fastdepCXX_FALSE@ DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
+@am__fastdepCXX_FALSE@ $(LTCXXCOMPILE) -c -o $@ $<
+
mostlyclean-libtool:
-rm -f *.lo
clean-libtool:
-rm -rf .libs _libs
+
+# This directory's subdirectories are mostly independent; you can cd
+# into them and run `make' without going through this Makefile.
+# To change the values of `make' variables: instead of editing Makefiles,
+# (1) if the variable is set in `config.status', edit `config.status'
+# (which will cause the Makefiles to be regenerated when you run `make');
+# (2) otherwise, pass the desired values on the `make' command line.
+$(RECURSIVE_TARGETS):
+ @failcom='exit 1'; \
+ for f in x $$MAKEFLAGS; do \
+ case $$f in \
+ *=* | --[!k]*);; \
+ *k*) failcom='fail=yes';; \
+ esac; \
+ done; \
+ dot_seen=no; \
+ target=`echo $@ | sed s/-recursive//`; \
+ list='$(SUBDIRS)'; for subdir in $$list; do \
+ echo "Making $$target in $$subdir"; \
+ if test "$$subdir" = "."; then \
+ dot_seen=yes; \
+ local_target="$$target-am"; \
+ else \
+ local_target="$$target"; \
+ fi; \
+ ($(am__cd) $$subdir && $(MAKE) $(AM_MAKEFLAGS) $$local_target) \
+ || eval $$failcom; \
+ done; \
+ if test "$$dot_seen" = "no"; then \
+ $(MAKE) $(AM_MAKEFLAGS) "$$target-am" || exit 1; \
+ fi; test -z "$$fail"
+
+$(RECURSIVE_CLEAN_TARGETS):
+ @failcom='exit 1'; \
+ for f in x $$MAKEFLAGS; do \
+ case $$f in \
+ *=* | --[!k]*);; \
+ *k*) failcom='fail=yes';; \
+ esac; \
+ done; \
+ dot_seen=no; \
+ case "$@" in \
+ distclean-* | maintainer-clean-*) list='$(DIST_SUBDIRS)' ;; \
+ *) list='$(SUBDIRS)' ;; \
+ esac; \
+ rev=''; for subdir in $$list; do \
+ if test "$$subdir" = "."; then :; else \
+ rev="$$subdir $$rev"; \
+ fi; \
+ done; \
+ rev="$$rev ."; \
+ target=`echo $@ | sed s/-recursive//`; \
+ for subdir in $$rev; do \
+ echo "Making $$target in $$subdir"; \
+ if test "$$subdir" = "."; then \
+ local_target="$$target-am"; \
+ else \
+ local_target="$$target"; \
+ fi; \
+ ($(am__cd) $$subdir && $(MAKE) $(AM_MAKEFLAGS) $$local_target) \
+ || eval $$failcom; \
+ done && test -z "$$fail"
+tags-recursive:
+ list='$(SUBDIRS)'; for subdir in $$list; do \
+ test "$$subdir" = . || ($(am__cd) $$subdir && $(MAKE) $(AM_MAKEFLAGS) tags); \
+ done
+ctags-recursive:
+ list='$(SUBDIRS)'; for subdir in $$list; do \
+ test "$$subdir" = . || ($(am__cd) $$subdir && $(MAKE) $(AM_MAKEFLAGS) ctags); \
+ done
+
+ID: $(HEADERS) $(SOURCES) $(LISP) $(TAGS_FILES)
+ list='$(SOURCES) $(HEADERS) $(LISP) $(TAGS_FILES)'; \
+ unique=`for i in $$list; do \
+ if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
+ done | \
+ $(AWK) '{ files[$$0] = 1; nonempty = 1; } \
+ END { if (nonempty) { for (i in files) print i; }; }'`; \
+ mkid -fID $$unique
tags: TAGS
-TAGS:
+TAGS: tags-recursive $(HEADERS) $(SOURCES) $(TAGS_DEPENDENCIES) \
+ $(TAGS_FILES) $(LISP)
+ set x; \
+ here=`pwd`; \
+ if ($(ETAGS) --etags-include --version) >/dev/null 2>&1; then \
+ include_option=--etags-include; \
+ empty_fix=.; \
+ else \
+ include_option=--include; \
+ empty_fix=; \
+ fi; \
+ list='$(SUBDIRS)'; for subdir in $$list; do \
+ if test "$$subdir" = .; then :; else \
+ test ! -f $$subdir/TAGS || \
+ set "$$@" "$$include_option=$$here/$$subdir/TAGS"; \
+ fi; \
+ done; \
+ list='$(SOURCES) $(HEADERS) $(LISP) $(TAGS_FILES)'; \
+ unique=`for i in $$list; do \
+ if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
+ done | \
+ $(AWK) '{ files[$$0] = 1; nonempty = 1; } \
+ END { if (nonempty) { for (i in files) print i; }; }'`; \
+ shift; \
+ if test -z "$(ETAGS_ARGS)$$*$$unique"; then :; else \
+ test -n "$$unique" || unique=$$empty_fix; \
+ if test $$# -gt 0; then \
+ $(ETAGS) $(ETAGSFLAGS) $(AM_ETAGSFLAGS) $(ETAGS_ARGS) \
+ "$$@" $$unique; \
+ else \
+ $(ETAGS) $(ETAGSFLAGS) $(AM_ETAGSFLAGS) $(ETAGS_ARGS) \
+ $$unique; \
+ fi; \
+ fi
ctags: CTAGS
-CTAGS:
-
+CTAGS: ctags-recursive $(HEADERS) $(SOURCES) $(TAGS_DEPENDENCIES) \
+ $(TAGS_FILES) $(LISP)
+ list='$(SOURCES) $(HEADERS) $(LISP) $(TAGS_FILES)'; \
+ unique=`for i in $$list; do \
+ if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
+ done | \
+ $(AWK) '{ files[$$0] = 1; nonempty = 1; } \
+ END { if (nonempty) { for (i in files) print i; }; }'`; \
+ test -z "$(CTAGS_ARGS)$$unique" \
+ || $(CTAGS) $(CTAGSFLAGS) $(AM_CTAGSFLAGS) $(CTAGS_ARGS) \
+ $$unique
+
+GTAGS:
+ here=`$(am__cd) $(top_builddir) && pwd` \
+ && $(am__cd) $(top_srcdir) \
+ && gtags -i $(GTAGS_ARGS) "$$here"
+
+distclean-tags:
+ -rm -f TAGS ID GTAGS GRTAGS GSYMS GPATH tags
distdir: $(DISTFILES)
@srcdirstrip=`echo "$(srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \
@@ -265,19 +514,48 @@ distdir: $(DISTFILES)
|| exit 1; \
fi; \
done
+ @list='$(DIST_SUBDIRS)'; for subdir in $$list; do \
+ if test "$$subdir" = .; then :; else \
+ test -d "$(distdir)/$$subdir" \
+ || $(MKDIR_P) "$(distdir)/$$subdir" \
+ || exit 1; \
+ fi; \
+ done
+ @list='$(DIST_SUBDIRS)'; for subdir in $$list; do \
+ if test "$$subdir" = .; then :; else \
+ dir1=$$subdir; dir2="$(distdir)/$$subdir"; \
+ $(am__relativize); \
+ new_distdir=$$reldir; \
+ dir1=$$subdir; dir2="$(top_distdir)"; \
+ $(am__relativize); \
+ new_top_distdir=$$reldir; \
+ echo " (cd $$subdir && $(MAKE) $(AM_MAKEFLAGS) top_distdir="$$new_top_distdir" distdir="$$new_distdir" \\"; \
+ echo " am__remove_distdir=: am__skip_length_check=: am__skip_mode_fix=: distdir)"; \
+ ($(am__cd) $$subdir && \
+ $(MAKE) $(AM_MAKEFLAGS) \
+ top_distdir="$$new_top_distdir" \
+ distdir="$$new_distdir" \
+ am__remove_distdir=: \
+ am__skip_length_check=: \
+ am__skip_mode_fix=: \
+ distdir) \
+ || exit 1; \
+ fi; \
+ done
check-am: all-am
-check: check-am
-all-am: Makefile
-installdirs:
-install: install-am
-install-exec: install-exec-am
-install-data: install-data-am
-uninstall: uninstall-am
+check: check-recursive
+all-am: Makefile $(LTLIBRARIES)
+installdirs: installdirs-recursive
+installdirs-am:
+install: install-recursive
+install-exec: install-exec-recursive
+install-data: install-data-recursive
+uninstall: uninstall-recursive
install-am: all-am
@$(MAKE) $(AM_MAKEFLAGS) install-exec-am install-data-am
-installcheck: installcheck-am
+installcheck: installcheck-recursive
install-strip:
$(MAKE) $(AM_MAKEFLAGS) INSTALL_PROGRAM="$(INSTALL_STRIP_PROGRAM)" \
install_sh_PROGRAM="$(INSTALL_STRIP_PROGRAM)" INSTALL_STRIP_FLAG=-s \
@@ -294,92 +572,95 @@ distclean-generic:
maintainer-clean-generic:
@echo "This command is intended for maintainers to use"
@echo "it deletes files that may require special tools to rebuild."
-clean: clean-am
+clean: clean-recursive
-clean-am: clean-generic clean-libtool mostlyclean-am
+clean-am: clean-generic clean-libtool clean-noinstLTLIBRARIES \
+ mostlyclean-am
-distclean: distclean-am
+distclean: distclean-recursive
+ -rm -rf ./$(DEPDIR)
-rm -f Makefile
-distclean-am: clean-am distclean-generic
+distclean-am: clean-am distclean-compile distclean-generic \
+ distclean-tags
-dvi: dvi-am
+dvi: dvi-recursive
dvi-am:
-html: html-am
+html: html-recursive
html-am:
-info: info-am
+info: info-recursive
info-am:
install-data-am:
-install-dvi: install-dvi-am
+install-dvi: install-dvi-recursive
install-dvi-am:
install-exec-am:
-install-html: install-html-am
+install-html: install-html-recursive
install-html-am:
-install-info: install-info-am
+install-info: install-info-recursive
install-info-am:
install-man:
-install-pdf: install-pdf-am
+install-pdf: install-pdf-recursive
install-pdf-am:
-install-ps: install-ps-am
+install-ps: install-ps-recursive
install-ps-am:
installcheck-am:
-maintainer-clean: maintainer-clean-am
+maintainer-clean: maintainer-clean-recursive
+ -rm -rf ./$(DEPDIR)
-rm -f Makefile
maintainer-clean-am: distclean-am maintainer-clean-generic
-mostlyclean: mostlyclean-am
+mostlyclean: mostlyclean-recursive
-mostlyclean-am: mostlyclean-generic mostlyclean-libtool
+mostlyclean-am: mostlyclean-compile mostlyclean-generic \
+ mostlyclean-libtool
-pdf: pdf-am
+pdf: pdf-recursive
pdf-am:
-ps: ps-am
+ps: ps-recursive
ps-am:
uninstall-am:
-.MAKE: install-am install-strip
-
-.PHONY: all all-am check check-am clean clean-generic clean-libtool \
- distclean distclean-generic distclean-libtool distdir dvi \
- dvi-am html html-am info info-am install install-am \
- install-data install-data-am install-dvi install-dvi-am \
- install-exec install-exec-am install-html install-html-am \
- install-info install-info-am install-man install-pdf \
- install-pdf-am install-ps install-ps-am install-strip \
- installcheck installcheck-am installdirs maintainer-clean \
- maintainer-clean-generic mostlyclean mostlyclean-generic \
- mostlyclean-libtool pdf pdf-am ps ps-am uninstall uninstall-am
-
-
-#noinst_LTLIBRARIES = libtheory.la
-
-#libtheory_la_LIBADD =
-# @builddir@/uf/libuf.la
+.MAKE: $(RECURSIVE_CLEAN_TARGETS) $(RECURSIVE_TARGETS) ctags-recursive \
+ install-am install-strip tags-recursive
+
+.PHONY: $(RECURSIVE_CLEAN_TARGETS) $(RECURSIVE_TARGETS) CTAGS GTAGS \
+ all all-am check check-am clean clean-generic clean-libtool \
+ clean-noinstLTLIBRARIES ctags ctags-recursive distclean \
+ distclean-compile distclean-generic distclean-libtool \
+ distclean-tags distdir dvi dvi-am html html-am info info-am \
+ install install-am install-data install-data-am install-dvi \
+ install-dvi-am install-exec install-exec-am install-html \
+ install-html-am install-info install-info-am install-man \
+ install-pdf install-pdf-am install-ps install-ps-am \
+ install-strip installcheck installcheck-am installdirs \
+ installdirs-am maintainer-clean maintainer-clean-generic \
+ mostlyclean mostlyclean-compile mostlyclean-generic \
+ mostlyclean-libtool pdf pdf-am ps ps-am tags tags-recursive \
+ uninstall uninstall-am
-#SUBDIRS = uf
# Tell versions [3.59,3.63) of GNU make to not export all variables.
# Otherwise a system limit (for SysV at least) may be exceeded.
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
new file mode 100644
index 000000000..024d192e6
--- /dev/null
+++ b/src/theory/theory.cpp
@@ -0,0 +1,16 @@
+/********************* -*- C++ -*- */
+/** theory.cpp
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ **/
+
+#include "theory/theory.h"
+
+namespace CVC4 {
+
+}/* CVC4 namespace */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
new file mode 100644
index 000000000..6d0b9d91d
--- /dev/null
+++ b/src/theory/theory_engine.cpp
@@ -0,0 +1,16 @@
+/********************* -*- C++ -*- */
+/** theory_engine.cpp
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ **/
+
+#include "theory/theory_engine.h"
+
+namespace CVC4 {
+
+}/* CVC4 namespace */
diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am
new file mode 100644
index 000000000..11c9f536e
--- /dev/null
+++ b/src/theory/uf/Makefile.am
@@ -0,0 +1,7 @@
+INCLUDES = -I@srcdir@/../../include -I@srcdir@/../..
+AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CPPFLAGS = -D__BUILDING_CVC4LIB
+
+noinst_LTLIBRARIES = libuf.la
+
+libuf_la_SOURCES =
diff --git a/src/theory/uf/Makefile.in b/src/theory/uf/Makefile.in
new file mode 100644
index 000000000..d80103452
--- /dev/null
+++ b/src/theory/uf/Makefile.in
@@ -0,0 +1,417 @@
+# Makefile.in generated by automake 1.11 from Makefile.am.
+# @configure_input@
+
+# Copyright (C) 1994, 1995, 1996, 1997, 1998, 1999, 2000, 2001, 2002,
+# 2003, 2004, 2005, 2006, 2007, 2008, 2009 Free Software Foundation,
+# Inc.
+# This Makefile.in is free software; the Free Software Foundation
+# gives unlimited permission to copy and/or distribute it,
+# with or without modifications, as long as this notice is preserved.
+
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY, to the extent permitted by law; without
+# even the implied warranty of MERCHANTABILITY or FITNESS FOR A
+# PARTICULAR PURPOSE.
+
+@SET_MAKE@
+
+VPATH = @srcdir@
+pkgdatadir = $(datadir)/@PACKAGE@
+pkgincludedir = $(includedir)/@PACKAGE@
+pkglibdir = $(libdir)/@PACKAGE@
+pkglibexecdir = $(libexecdir)/@PACKAGE@
+am__cd = CDPATH="$${ZSH_VERSION+.}$(PATH_SEPARATOR)" && cd
+install_sh_DATA = $(install_sh) -c -m 644
+install_sh_PROGRAM = $(install_sh) -c
+install_sh_SCRIPT = $(install_sh) -c
+INSTALL_HEADER = $(INSTALL_DATA)
+transform = $(program_transform_name)
+NORMAL_INSTALL = :
+PRE_INSTALL = :
+POST_INSTALL = :
+NORMAL_UNINSTALL = :
+PRE_UNINSTALL = :
+POST_UNINSTALL = :
+build_triplet = @build@
+host_triplet = @host@
+target_triplet = @target@
+subdir = src/theory/uf
+DIST_COMMON = $(srcdir)/Makefile.am $(srcdir)/Makefile.in
+ACLOCAL_M4 = $(top_srcdir)/aclocal.m4
+am__aclocal_m4_deps = $(top_srcdir)/config/antlr.m4 \
+ $(top_srcdir)/config/libtool.m4 \
+ $(top_srcdir)/config/ltoptions.m4 \
+ $(top_srcdir)/config/ltsugar.m4 \
+ $(top_srcdir)/config/ltversion.m4 \
+ $(top_srcdir)/config/lt~obsolete.m4 $(top_srcdir)/configure.ac
+am__configure_deps = $(am__aclocal_m4_deps) $(CONFIGURE_DEPENDENCIES) \
+ $(ACLOCAL_M4)
+mkinstalldirs = $(install_sh) -d
+CONFIG_HEADER = $(top_builddir)/config.h
+CONFIG_CLEAN_FILES =
+CONFIG_CLEAN_VPATH_FILES =
+LTLIBRARIES = $(noinst_LTLIBRARIES)
+libuf_la_LIBADD =
+am_libuf_la_OBJECTS =
+libuf_la_OBJECTS = $(am_libuf_la_OBJECTS)
+DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
+COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \
+ $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+LTCOMPILE = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+ --mode=compile $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
+ $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+CCLD = $(CC)
+LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+ --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \
+ $(LDFLAGS) -o $@
+SOURCES = $(libuf_la_SOURCES)
+DIST_SOURCES = $(libuf_la_SOURCES)
+DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST)
+ACLOCAL = @ACLOCAL@
+AMTAR = @AMTAR@
+ANTLR = @ANTLR@
+ANTLR_INCLUDES = @ANTLR_INCLUDES@
+ANTLR_LDFLAGS = @ANTLR_LDFLAGS@
+AR = @AR@
+AS = @AS@
+AUTOCONF = @AUTOCONF@
+AUTOHEADER = @AUTOHEADER@
+AUTOMAKE = @AUTOMAKE@
+AWK = @AWK@
+CC = @CC@
+CCDEPMODE = @CCDEPMODE@
+CFLAGS = @CFLAGS@
+CPP = @CPP@
+CPPFLAGS = @CPPFLAGS@
+CVC4_LIBRARY_RELEASE_CODE = @CVC4_LIBRARY_RELEASE_CODE@
+CVC4_LIBRARY_VERSION = @CVC4_LIBRARY_VERSION@
+CVC4_PARSER_LIBRARY_VERSION = @CVC4_PARSER_LIBRARY_VERSION@
+CXX = @CXX@
+CXXCPP = @CXXCPP@
+CXXDEPMODE = @CXXDEPMODE@
+CXXFLAGS = @CXXFLAGS@
+CXXTESTGEN = @CXXTESTGEN@
+CYGPATH_W = @CYGPATH_W@
+DEFS = @DEFS@
+DEPDIR = @DEPDIR@
+DLLTOOL = @DLLTOOL@
+DOXYGEN = @DOXYGEN@
+DSYMUTIL = @DSYMUTIL@
+DUMPBIN = @DUMPBIN@
+ECHO_C = @ECHO_C@
+ECHO_N = @ECHO_N@
+ECHO_T = @ECHO_T@
+EGREP = @EGREP@
+EXEEXT = @EXEEXT@
+FGREP = @FGREP@
+GREP = @GREP@
+INSTALL = @INSTALL@
+INSTALL_DATA = @INSTALL_DATA@
+INSTALL_PROGRAM = @INSTALL_PROGRAM@
+INSTALL_SCRIPT = @INSTALL_SCRIPT@
+INSTALL_STRIP_PROGRAM = @INSTALL_STRIP_PROGRAM@
+LD = @LD@
+LDFLAGS = @LDFLAGS@
+LIBOBJS = @LIBOBJS@
+LIBS = @LIBS@
+LIBTOOL = @LIBTOOL@
+LIPO = @LIPO@
+LN_S = @LN_S@
+LTLIBOBJS = @LTLIBOBJS@
+MAKEINFO = @MAKEINFO@
+MKDIR_P = @MKDIR_P@
+NM = @NM@
+NMEDIT = @NMEDIT@
+OBJDUMP = @OBJDUMP@
+OBJEXT = @OBJEXT@
+OTOOL = @OTOOL@
+OTOOL64 = @OTOOL64@
+PACKAGE = @PACKAGE@
+PACKAGE_BUGREPORT = @PACKAGE_BUGREPORT@
+PACKAGE_NAME = @PACKAGE_NAME@
+PACKAGE_STRING = @PACKAGE_STRING@
+PACKAGE_TARNAME = @PACKAGE_TARNAME@
+PACKAGE_URL = @PACKAGE_URL@
+PACKAGE_VERSION = @PACKAGE_VERSION@
+PATH_SEPARATOR = @PATH_SEPARATOR@
+PERL = @PERL@
+RANLIB = @RANLIB@
+SED = @SED@
+SET_MAKE = @SET_MAKE@
+SHELL = @SHELL@
+STRIP = @STRIP@
+TEST_CPPFLAGS = @TEST_CPPFLAGS@
+TEST_CXXFLAGS = @TEST_CXXFLAGS@
+TEST_LDFLAGS = @TEST_LDFLAGS@
+VERSION = @VERSION@
+abs_builddir = @abs_builddir@
+abs_srcdir = @abs_srcdir@
+abs_top_builddir = @abs_top_builddir@
+abs_top_srcdir = @abs_top_srcdir@
+ac_ct_CC = @ac_ct_CC@
+ac_ct_CXX = @ac_ct_CXX@
+ac_ct_DUMPBIN = @ac_ct_DUMPBIN@
+am__include = @am__include@
+am__leading_dot = @am__leading_dot@
+am__quote = @am__quote@
+am__tar = @am__tar@
+am__untar = @am__untar@
+bindir = @bindir@
+build = @build@
+build_alias = @build_alias@
+build_cpu = @build_cpu@
+build_os = @build_os@
+build_vendor = @build_vendor@
+builddir = @builddir@
+datadir = @datadir@
+datarootdir = @datarootdir@
+docdir = @docdir@
+dvidir = @dvidir@
+exec_prefix = @exec_prefix@
+host = @host@
+host_alias = @host_alias@
+host_cpu = @host_cpu@
+host_os = @host_os@
+host_vendor = @host_vendor@
+htmldir = @htmldir@
+includedir = @includedir@
+infodir = @infodir@
+install_sh = @install_sh@
+libdir = @libdir@
+libexecdir = @libexecdir@
+localedir = @localedir@
+localstatedir = @localstatedir@
+lt_ECHO = @lt_ECHO@
+mandir = @mandir@
+mkdir_p = @mkdir_p@
+oldincludedir = @oldincludedir@
+pdfdir = @pdfdir@
+prefix = @prefix@
+program_transform_name = @program_transform_name@
+psdir = @psdir@
+sbindir = @sbindir@
+sharedstatedir = @sharedstatedir@
+srcdir = @srcdir@
+sysconfdir = @sysconfdir@
+target = @target@
+target_alias = @target_alias@
+target_cpu = @target_cpu@
+target_os = @target_os@
+target_vendor = @target_vendor@
+top_build_prefix = @top_build_prefix@
+top_builddir = @top_builddir@
+top_srcdir = @top_srcdir@
+INCLUDES = -I@srcdir@/../../include -I@srcdir@/../..
+AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CPPFLAGS = -D__BUILDING_CVC4LIB
+noinst_LTLIBRARIES = libuf.la
+libuf_la_SOURCES =
+all: all-am
+
+.SUFFIXES:
+$(srcdir)/Makefile.in: $(srcdir)/Makefile.am $(am__configure_deps)
+ @for dep in $?; do \
+ case '$(am__configure_deps)' in \
+ *$$dep*) \
+ ( cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh ) \
+ && { if test -f $@; then exit 0; else break; fi; }; \
+ exit 1;; \
+ esac; \
+ done; \
+ echo ' cd $(top_srcdir) && $(AUTOMAKE) --foreign src/theory/uf/Makefile'; \
+ $(am__cd) $(top_srcdir) && \
+ $(AUTOMAKE) --foreign src/theory/uf/Makefile
+.PRECIOUS: Makefile
+Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status
+ @case '$?' in \
+ *config.status*) \
+ cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh;; \
+ *) \
+ echo ' cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe)'; \
+ cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe);; \
+ esac;
+
+$(top_builddir)/config.status: $(top_srcdir)/configure $(CONFIG_STATUS_DEPENDENCIES)
+ cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
+
+$(top_srcdir)/configure: $(am__configure_deps)
+ cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
+$(ACLOCAL_M4): $(am__aclocal_m4_deps)
+ cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
+$(am__aclocal_m4_deps):
+
+clean-noinstLTLIBRARIES:
+ -test -z "$(noinst_LTLIBRARIES)" || rm -f $(noinst_LTLIBRARIES)
+ @list='$(noinst_LTLIBRARIES)'; for p in $$list; do \
+ dir="`echo $$p | sed -e 's|/[^/]*$$||'`"; \
+ test "$$dir" != "$$p" || dir=.; \
+ echo "rm -f \"$${dir}/so_locations\""; \
+ rm -f "$${dir}/so_locations"; \
+ done
+libuf.la: $(libuf_la_OBJECTS) $(libuf_la_DEPENDENCIES)
+ $(LINK) $(libuf_la_OBJECTS) $(libuf_la_LIBADD) $(LIBS)
+
+mostlyclean-compile:
+ -rm -f *.$(OBJEXT)
+
+distclean-compile:
+ -rm -f *.tab.c
+
+mostlyclean-libtool:
+ -rm -f *.lo
+
+clean-libtool:
+ -rm -rf .libs _libs
+tags: TAGS
+TAGS:
+
+ctags: CTAGS
+CTAGS:
+
+
+distdir: $(DISTFILES)
+ @srcdirstrip=`echo "$(srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \
+ topsrcdirstrip=`echo "$(top_srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \
+ list='$(DISTFILES)'; \
+ dist_files=`for file in $$list; do echo $$file; done | \
+ sed -e "s|^$$srcdirstrip/||;t" \
+ -e "s|^$$topsrcdirstrip/|$(top_builddir)/|;t"`; \
+ case $$dist_files in \
+ */*) $(MKDIR_P) `echo "$$dist_files" | \
+ sed '/\//!d;s|^|$(distdir)/|;s,/[^/]*$$,,' | \
+ sort -u` ;; \
+ esac; \
+ for file in $$dist_files; do \
+ if test -f $$file || test -d $$file; then d=.; else d=$(srcdir); fi; \
+ if test -d $$d/$$file; then \
+ dir=`echo "/$$file" | sed -e 's,/[^/]*$$,,'`; \
+ if test -d "$(distdir)/$$file"; then \
+ find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \
+ fi; \
+ if test -d $(srcdir)/$$file && test $$d != $(srcdir); then \
+ cp -fpR $(srcdir)/$$file "$(distdir)$$dir" || exit 1; \
+ find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \
+ fi; \
+ cp -fpR $$d/$$file "$(distdir)$$dir" || exit 1; \
+ else \
+ test -f "$(distdir)/$$file" \
+ || cp -p $$d/$$file "$(distdir)/$$file" \
+ || exit 1; \
+ fi; \
+ done
+check-am: all-am
+check: check-am
+all-am: Makefile $(LTLIBRARIES)
+installdirs:
+install: install-am
+install-exec: install-exec-am
+install-data: install-data-am
+uninstall: uninstall-am
+
+install-am: all-am
+ @$(MAKE) $(AM_MAKEFLAGS) install-exec-am install-data-am
+
+installcheck: installcheck-am
+install-strip:
+ $(MAKE) $(AM_MAKEFLAGS) INSTALL_PROGRAM="$(INSTALL_STRIP_PROGRAM)" \
+ install_sh_PROGRAM="$(INSTALL_STRIP_PROGRAM)" INSTALL_STRIP_FLAG=-s \
+ `test -z '$(STRIP)' || \
+ echo "INSTALL_PROGRAM_ENV=STRIPPROG='$(STRIP)'"` install
+mostlyclean-generic:
+
+clean-generic:
+
+distclean-generic:
+ -test -z "$(CONFIG_CLEAN_FILES)" || rm -f $(CONFIG_CLEAN_FILES)
+ -test . = "$(srcdir)" || test -z "$(CONFIG_CLEAN_VPATH_FILES)" || rm -f $(CONFIG_CLEAN_VPATH_FILES)
+
+maintainer-clean-generic:
+ @echo "This command is intended for maintainers to use"
+ @echo "it deletes files that may require special tools to rebuild."
+clean: clean-am
+
+clean-am: clean-generic clean-libtool clean-noinstLTLIBRARIES \
+ mostlyclean-am
+
+distclean: distclean-am
+ -rm -f Makefile
+distclean-am: clean-am distclean-compile distclean-generic
+
+dvi: dvi-am
+
+dvi-am:
+
+html: html-am
+
+html-am:
+
+info: info-am
+
+info-am:
+
+install-data-am:
+
+install-dvi: install-dvi-am
+
+install-dvi-am:
+
+install-exec-am:
+
+install-html: install-html-am
+
+install-html-am:
+
+install-info: install-info-am
+
+install-info-am:
+
+install-man:
+
+install-pdf: install-pdf-am
+
+install-pdf-am:
+
+install-ps: install-ps-am
+
+install-ps-am:
+
+installcheck-am:
+
+maintainer-clean: maintainer-clean-am
+ -rm -f Makefile
+maintainer-clean-am: distclean-am maintainer-clean-generic
+
+mostlyclean: mostlyclean-am
+
+mostlyclean-am: mostlyclean-compile mostlyclean-generic \
+ mostlyclean-libtool
+
+pdf: pdf-am
+
+pdf-am:
+
+ps: ps-am
+
+ps-am:
+
+uninstall-am:
+
+.MAKE: install-am install-strip
+
+.PHONY: all all-am check check-am clean clean-generic clean-libtool \
+ clean-noinstLTLIBRARIES distclean distclean-compile \
+ distclean-generic distclean-libtool distdir dvi dvi-am html \
+ html-am info info-am install install-am install-data \
+ install-data-am install-dvi install-dvi-am install-exec \
+ install-exec-am install-html install-html-am install-info \
+ install-info-am install-man install-pdf install-pdf-am \
+ install-ps install-ps-am install-strip installcheck \
+ installcheck-am installdirs maintainer-clean \
+ maintainer-clean-generic mostlyclean mostlyclean-compile \
+ mostlyclean-generic mostlyclean-libtool pdf pdf-am ps ps-am \
+ uninstall uninstall-am
+
+
+# Tell versions [3.59,3.63) of GNU make to not export all variables.
+# Otherwise a system limit (for SysV at least) may be exceeded.
+.NOEXPORT:
diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp
index 799af12ab..a86e2021a 100644
--- a/src/util/Assert.cpp
+++ b/src/util/Assert.cpp
@@ -28,7 +28,7 @@ void AssertionException::construct(const char* header, const char* extra,
va_list args) {
// try building the exception msg with a smallish buffer first,
// then with a larger one if sprintf tells us to.
- int n = 256;
+ int n = 512;
char* buf;
for(;;) {
diff --git a/src/util/Assert.h b/src/util/Assert.h
index 3da76c5db..c3b81727c 100644
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -137,15 +137,15 @@ public:
#define AlwaysAssert(cond, msg...) \
do { \
if(EXPECT_FALSE( ! (cond) )) { \
- throw AssertionException(#cond, __FUNCTION__, __FILE__, __LINE__, ## msg); \
+ throw AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
} \
} while(0)
#define Unreachable(msg...) \
- throw UnreachableCodeException(__FUNCTION__, __FILE__, __LINE__, ## msg)
+ throw UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
#define Unhandled(msg...) \
- throw UnhandledCaseException(__FUNCTION__, __FILE__, __LINE__, ## msg)
+ throw UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
#define IllegalArgument(arg, msg...) \
- throw IllegalArgumentException(#arg, __FUNCTION__, __FILE__, __LINE__, ## msg)
+ throw IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
#ifdef CVC4_ASSERTIONS
# define Assert(cond, msg...) AlwaysAssert(cond, ## msg)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback