From 8b2d1d64b886db4cff74e2a7b1370841979001b2 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 10 Dec 2009 17:45:43 +0000 Subject: [PATCH] cleanups, assert work, add a stubbed uf theory, fix driver --- configure | 4 +- configure.ac | 2 +- src/Makefile.am | 4 +- src/Makefile.in | 7 +- src/context/Makefile.am | 3 +- src/context/Makefile.in | 12 +- src/expr/Makefile.am | 8 + src/expr/Makefile.in | 17 ++ src/expr/attr_var_name.h | 36 +++ src/expr/expr_attribute.h | 2 - src/main/Makefile.am | 5 +- src/main/Makefile.in | 14 +- src/main/main.cpp | 18 +- src/prop/minisat/Makefile.am | 17 +- src/prop/minisat/Makefile.in | 17 +- src/smt/Makefile.am | 3 +- src/smt/Makefile.in | 12 +- src/theory/Makefile.am | 14 +- src/theory/Makefile.in | 381 +++++++++++++++++++++++++++----- src/theory/theory.cpp | 16 ++ src/theory/theory_engine.cpp | 16 ++ src/theory/uf/Makefile.am | 7 + src/theory/uf/Makefile.in | 417 +++++++++++++++++++++++++++++++++++ src/util/Assert.cpp | 2 +- src/util/Assert.h | 8 +- 25 files changed, 948 insertions(+), 94 deletions(-) create mode 100644 src/expr/attr_var_name.h create mode 100644 src/theory/theory.cpp create mode 100644 src/theory/theory_engine.cpp create mode 100644 src/theory/uf/Makefile.am create mode 100644 src/theory/uf/Makefile.in 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_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 #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) -- 2.30.2