From 7c143dc5d5a52664a3cecca5226df57269063162 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 22 Feb 2010 20:33:00 +0000 Subject: [PATCH] * configure.ac: Remove doc/ from search path for Makefile.ams * configure.ac, test/unit/Makefile.am: Resolved an issue where even when not testing, one unit test was built. * Re-ran contrib/update-copyright.pl on all source files to ensure consistent and correct header comments. * contrib/get-authors: Change definition of "minor contributor" to >= 10% of lines (rather than strictly greater than 10% of lines) --- configure.ac | 8 +++++++- contrib/get-authors | 2 +- src/context/context.h | 2 +- src/expr/attribute.h | 4 ++-- src/expr/expr.cpp | 4 ++-- src/expr/expr.h | 2 +- src/expr/expr_manager.cpp | 2 +- src/expr/expr_manager.h | 2 +- src/expr/node.cpp | 4 ++-- src/expr/node_manager.cpp | 4 ++-- src/expr/node_manager.h | 4 ++-- src/expr/soft_node.h | 6 +++--- src/expr/type.cpp | 4 ++-- src/expr/type.h | 4 ++-- src/main/getopt.cpp | 2 +- src/main/main.cpp | 2 +- src/main/usage.h | 2 +- src/parser/antlr_parser.cpp | 4 ++-- src/parser/cvc/cvc_parser.g | 4 ++-- src/parser/parser.cpp | 2 +- src/parser/parser.h | 2 +- src/parser/symbol_table.h | 2 +- src/prop/prop_engine.cpp | 4 ++-- src/prop/prop_engine.h | 4 ++-- src/prop/sat.h | 2 +- src/smt/smt_engine.cpp | 2 +- src/smt/smt_engine.h | 2 +- src/theory/theory.h | 2 +- src/theory/uf/ecdata.cpp | 15 +++++++++++++++ src/theory/uf/ecdata.h | 2 +- src/theory/uf/theory_uf.cpp | 15 +++++++++++++++ src/theory/uf/theory_uf.h | 15 +++++++++++++++ src/util/configuration.h | 2 +- src/util/options.h | 4 ++-- src/util/output.h | 2 +- test/unit/Makefile.am | 12 +++++++----- test/unit/parser/parser_black.h | 4 ++-- 37 files changed, 106 insertions(+), 53 deletions(-) diff --git a/configure.ac b/configure.ac index 8c1141b9d..d75ce6309 100644 --- a/configure.ac +++ b/configure.ac @@ -453,10 +453,16 @@ LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS" mk_include=include AC_SUBST(mk_include) +# CVC4_FALSE +# +# This is used to _always_ comment out rules in automake makefiles, but +# still trigger certain automake behavior; see test/unit/Makefile.am. +AM_CONDITIONAL([CVC4_FALSE], [false]) + AC_CONFIG_FILES([ Makefile.builds Makefile] - m4_esyscmd([find contrib/ doc/ src/ test/ -name Makefile.am | sort | sed 's,\.am$,,']) + m4_esyscmd([find contrib/ src/ test/ -name Makefile.am | sort | sed 's,\.am$,,']) ) AC_OUTPUT diff --git a/contrib/get-authors b/contrib/get-authors index a42f8a25b..40aaf6a6d 100755 --- a/contrib/get-authors +++ b/contrib/get-authors @@ -20,7 +20,7 @@ while [ $# -gt 0 ]; do ( while read lines author; do pct=$((100*$lines/$total_lines)) if [ "$author" != "$original_author" ]; then - if [ $pct -gt 10 ]; then + if [ $pct -ge 10 ]; then major_contributors="${major_contributors:+$major_contributors, }$author" else minor_contributors="${minor_contributors:+$minor_contributors, }$author" diff --git a/src/context/context.h b/src/context/context.h index 1af4480f9..403235bc9 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -2,7 +2,7 @@ /** context.h ** Original author: mdeters ** Major contributors: barrett - ** Minor contributors (to current version): dejan + ** Minor contributors (to current version): taking, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 1d2705240..54500d0d5 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -1,7 +1,7 @@ -/********************* -*- C++ -*- */ +/********************* */ /** attribute.h ** Original author: mdeters - ** Major contributors: dejan + ** 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) diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index 18c0fdbab..c29b7e448 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -1,8 +1,8 @@ /********************* */ /** expr.cpp ** Original author: dejan - ** Major contributors: taking - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/expr.h b/src/expr/expr.h index dd4d0e9d7..096094aff 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -2,7 +2,7 @@ /** expr.h ** Original author: dejan ** Major contributors: none - ** Minor contributors (to current version): mdeters, taking + ** Minor contributors (to current version): taking, mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index 506c118bc..71368c101 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -1,7 +1,7 @@ /********************* */ /** expr_manager.cpp ** Original author: dejan - ** Major contributors: mdeters + ** Major contributors: cconway, mdeters ** 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) diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index edfc18c8d..d84cf76be 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -1,7 +1,7 @@ /********************* */ /** expr_manager.h ** Original author: dejan - ** Major contributors: mdeters + ** Major contributors: cconway, mdeters ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 79490d58e..90dd86712 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -1,8 +1,8 @@ /********************* */ /** node.cpp ** Original author: mdeters - ** Major contributors: taking, dejan - ** Minor contributors (to current version): none + ** Major contributors: dejan + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 12a6d1732..c6aee3dea 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -1,8 +1,8 @@ /********************* */ /** node_manager.cpp ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): dejan + ** Major contributors: dejan + ** 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 diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 18a95f041..97f5ba9cd 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -1,8 +1,8 @@ /********************* */ /** node_manager.h ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): taking, dejan + ** Major contributors: dejan + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/soft_node.h b/src/expr/soft_node.h index fe71a4d1a..0bf9b47cf 100644 --- a/src/expr/soft_node.h +++ b/src/expr/soft_node.h @@ -1,8 +1,8 @@ -/********************* -*- C++ -*- */ +/********************* */ /** soft_node.h ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): taking + ** 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 diff --git a/src/expr/type.cpp b/src/expr/type.cpp index d4662d420..368a3fe44 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -1,5 +1,5 @@ -/********************* -*- C++ -*- */ -/** type.h +/********************* */ +/** type.cpp ** Original author: cconway ** Major contributors: none ** Minor contributors (to current version): none diff --git a/src/expr/type.h b/src/expr/type.h index 19d0c831e..fd485602e 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -1,8 +1,8 @@ -/********************* -*- C++ -*- */ +/********************* */ /** type.h ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 190f7bbf3..7ca889592 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -2,7 +2,7 @@ /** getopt.cpp ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): barrett, dejan + ** Minor contributors (to current version): barrett, dejan, cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/main/main.cpp b/src/main/main.cpp index 6ebe895a5..a12c69df7 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -2,7 +2,7 @@ /** main.cpp ** Original author: mdeters ** Major contributors: barrett, dejan - ** Minor contributors (to current version): none + ** Minor contributors (to current version): cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/main/usage.h b/src/main/usage.h index 9a8175e2a..6c44fef5a 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -2,7 +2,7 @@ /** usage.h ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index 30fb33a32..0fdde07ff 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -1,8 +1,8 @@ /********************* */ /** antlr_parser.cpp ** Original author: dejan - ** Major contributors: mdeters, cconway - ** Minor contributors (to current version): none + ** Major contributors: cconway + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 0cdf9f36b..bfdc4c0f2 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -1,8 +1,8 @@ /* ******************* */ /* cvc_parser.g ** Original author: dejan - ** Major contributors: mdeters - ** Minor contributors (to current version): cconway + ** Major contributors: cconway + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index b9e2d576e..84796f093 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -2,7 +2,7 @@ /** parser.cpp ** Original author: mdeters ** Major contributors: dejan - ** Minor contributors (to current version): none + ** Minor contributors (to current version): cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/parser.h b/src/parser/parser.h index 170e1af31..da2c630ca 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -2,7 +2,7 @@ /** parser.h ** Original author: mdeters ** Major contributors: dejan - ** Minor contributors (to current version): none + ** Minor contributors (to current version): cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h index d790a1c84..dd110c4c1 100644 --- a/src/parser/symbol_table.h +++ b/src/parser/symbol_table.h @@ -1,4 +1,4 @@ -/********************* -*- C++ -*- */ +/********************* */ /** symbol_table.h ** Original author: cconway ** Major contributors: dejan, mdeters diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 80a8819b9..5dd57610d 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -1,8 +1,8 @@ /********************* */ /** prop_engine.cpp ** Original author: mdeters - ** Major contributors: taking - ** Minor contributors (to current version): none + ** Major contributors: dejan + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 9aa1ecff8..d4007e73a 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -1,8 +1,8 @@ /********************* */ /** prop_engine.h ** Original author: mdeters - ** Major contributors: taking - ** Minor contributors (to current version): dejan + ** Major contributors: taking, dejan + ** 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 diff --git a/src/prop/sat.h b/src/prop/sat.h index 350537d8f..a9696162a 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -1,7 +1,7 @@ /********************* */ /** sat.h ** Original author: mdeters - ** Major contributors: none + ** Major contributors: dejan ** 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) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 36954ace4..bb3e8c058 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2,7 +2,7 @@ /** smt_engine.cpp ** Original author: mdeters ** Major contributors: dejan - ** Minor contributors (to current version): taking + ** 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 diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 0e7e951f8..838f9cd7a 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -2,7 +2,7 @@ /** smt_engine.h ** Original author: mdeters ** Major contributors: dejan - ** Minor contributors (to current version): taking + ** 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 diff --git a/src/theory/theory.h b/src/theory/theory.h index dffc99053..831a185f8 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -2,7 +2,7 @@ /** theory.h ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): dejan + ** Minor contributors (to current version): dejan, taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/uf/ecdata.cpp b/src/theory/uf/ecdata.cpp index a22faf61e..cb7add487 100644 --- a/src/theory/uf/ecdata.cpp +++ b/src/theory/uf/ecdata.cpp @@ -1,3 +1,18 @@ +/********************* */ +/** ecdata.cpp + ** Original author: taking + ** 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. + ** + ** [[ Add file-specific comments here ]] + **/ + #include "theory/uf/ecdata.h" using namespace CVC4; diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/ecdata.h index fd0855bee..c8303a245 100644 --- a/src/theory/uf/ecdata.h +++ b/src/theory/uf/ecdata.h @@ -1,7 +1,7 @@ /********************* */ /** ecdata.h ** Original author: taking - ** Major contributors: barrett + ** 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) diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 840c7b51e..1f4d80b9b 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -1,3 +1,18 @@ +/********************* */ +/** theory_uf.cpp + ** Original author: taking + ** 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. + ** + ** [[ Add file-specific comments here ]] + **/ + #include "theory/uf/theory_uf.h" #include "theory/uf/ecdata.h" diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 06b0ee4f8..0ab51ca2c 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -1,3 +1,18 @@ +/********************* */ +/** theory_uf.h + ** Original author: taking + ** 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. + ** + ** [[ Add file-specific comments here ]] + **/ + #ifndef __CVC4__THEORY__THEORY_UF_H #define __CVC4__THEORY__THEORY_UF_H diff --git a/src/util/configuration.h b/src/util/configuration.h index b761f1f22..20d00a5f8 100644 --- a/src/util/configuration.h +++ b/src/util/configuration.h @@ -2,7 +2,7 @@ /** configuration.h ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): taking + ** 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 diff --git a/src/util/options.h b/src/util/options.h index cad00a61b..404700a85 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -1,8 +1,8 @@ /********************* */ /** options.h ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): taking + ** Major contributors: cconway + ** Minor contributors (to current version): taking, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/output.h b/src/util/output.h index ad42416d8..d0db064f0 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -2,7 +2,7 @@ /** output.h ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index c145cf752..591a85202 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -51,11 +51,6 @@ EXTRA_DIST = \ no_cxxtest \ $(TEST_DEPS_DIST) -# without these here, LTCXXCOMPILE, CXXLINK, etc., aren't set :-( -noinst_LTLIBRARIES = libdummy.la -libdummy_la_SOURCES = expr/node_black.cpp -libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la - MOSTLYCLEANFILES = $(UNIT_TESTS) $(UNIT_TESTS:%=%.cpp) @mk_include@ @srcdir@/Makefile.tests @@ -88,6 +83,13 @@ EXTRA_DIST = \ endif +# trick automake into setting LTCXXCOMPILE, CXXLINK, etc. +if CVC4_FALSE +noinst_LTLIBRARIES = libdummy.la +libdummy_la_SOURCES = expr/node_black.cpp +libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la +endif + # synonyms for "check" .PHONY: regress test regress test: check diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index dbf434ed2..150d88306 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -1,8 +1,8 @@ /********************* */ /** parser_black.h ** Original author: cconway - ** Major contributors: dejan - ** Minor contributors (to current version): mdeters + ** Major contributors: none + ** Minor contributors (to current version): mdeters, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences -- 2.30.2