From dfcf7dba0b2d8ad6eb9d8540e92804e70205b8fb Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 17 Dec 2009 21:05:15 +0000 Subject: [PATCH] update-copyright.pl now retrieves and incorporates author information from repository history; re-ran update-copyright.pl; cleaned up some things with make --- Makefile.subdir | 2 +- contrib/get-authors | 33 ++++++++++++++++++ contrib/update-copyright.pl | 24 ++++++++++--- src/context/context.cpp | 3 ++ src/context/context.h | 4 +++ src/context/context_mm.cpp | 3 ++ src/context/context_mm.h | 3 ++ src/expr/attr_type.h | 4 +++ src/expr/attr_var_name.h | 6 +++- src/expr/expr.cpp | 20 +++++++---- src/expr/expr.h | 20 +++++++---- src/expr/expr_manager.cpp | 15 ++++++++ src/expr/expr_manager.h | 20 +++++++---- src/expr/kind.h | 4 +++ src/expr/node.cpp | 3 ++ src/expr/node.h | 5 ++- src/expr/node_attribute.h | 6 +++- src/expr/node_builder.cpp | 3 ++ src/expr/node_builder.h | 4 +++ src/expr/node_manager.cpp | 3 ++ src/expr/node_manager.h | 4 +++ src/expr/node_value.cpp | 3 ++ src/expr/node_value.h | 3 ++ src/include/cvc4_config.h | 6 +++- src/main/about.h | 3 ++ src/main/getopt.cpp | 3 ++ src/main/main.cpp | 3 ++ src/main/main.h | 3 ++ src/main/usage.h | 3 ++ src/main/util.cpp | 3 ++ src/parser/antlr_parser.cpp | 15 ++++++++ src/parser/antlr_parser.h | 20 +++++++---- src/parser/cvc/cvc_parser.cpp | 3 ++ src/parser/cvc/cvc_parser.h | 3 ++ src/parser/parser.cpp | 3 ++ src/parser/parser.h | 3 ++ src/parser/parser_exception.h | 5 ++- src/parser/smt/smt_parser.cpp | 3 ++ src/parser/smt/smt_parser.h | 3 ++ src/parser/symbol_table.h | 4 +++ src/prop/prop_engine.cpp | 5 ++- src/prop/prop_engine.h | 5 +++ src/prop/sat.h | 4 +++ src/smt/smt_engine.cpp | 3 ++ src/smt/smt_engine.h | 4 +++ src/theory/theory.cpp | 4 +++ src/theory/theory.h | 4 +++ src/theory/theory_engine.cpp | 4 +++ src/theory/theory_engine.h | 4 +++ src/util/Assert.cpp | 3 ++ src/util/Assert.h | 3 ++ src/util/command.cpp | 15 ++++++++ src/util/command.h | 5 +++ src/util/debug.h | 18 +++++++--- src/util/decision_engine.cpp | 3 ++ src/util/decision_engine.h | 4 +++ src/util/exception.h | 7 ++-- src/util/literal.h | 4 +++ src/util/model.h | 4 +++ src/util/options.h | 5 ++- src/util/output.cpp | 3 ++ src/util/output.h | 3 ++ src/util/result.h | 4 +++ src/util/unique_id.h | 4 +++ test/unit/Makefile.am | 46 ++++++++++++++++--------- test/unit/Makefile.in | 45 +++++++++++++++--------- test/unit/expr/node_black.h | 15 +++++++- test/unit/expr/node_white.h | 15 +++++++- test/unit/parser/cvc/cvc_parser_black.h | 15 +++++++- 69 files changed, 461 insertions(+), 78 deletions(-) create mode 100755 contrib/get-authors diff --git a/Makefile.subdir b/Makefile.subdir index 590b3ea4e..6470510d9 100644 --- a/Makefile.subdir +++ b/Makefile.subdir @@ -4,7 +4,7 @@ builddir = $(topdir)/builds/$(CURRENT_BUILD)/$(srcdir) .PHONY: _default_build_ all _default_build_: all -%: +all %: @if test -e $(builddir); then \ echo cd $(builddir); \ cd $(builddir); \ diff --git a/contrib/get-authors b/contrib/get-authors new file mode 100755 index 000000000..a42f8a25b --- /dev/null +++ b/contrib/get-authors @@ -0,0 +1,33 @@ +#!/bin/sh +# +# get-authors +# Morgan Deters for CVC4 +# +# usage: get-authors [ files... ] +# +# This script uses svn to get the original author +# + +while [ $# -gt 0 ]; do + f=$1 + shift + original_author= + major_contributors= + minor_contributors= + total_lines=`wc -l "$f" | awk '{print$1}'` + original_author=`svn log -q --incremental "$f" | tail -1 | awk '{print$3}'` + svn blame "$f" | awk '{print$2}' | sort | uniq -c | sort -n | + ( while read lines author; do + pct=$((100*$lines/$total_lines)) + if [ "$author" != "$original_author" ]; then + if [ $pct -gt 10 ]; then + major_contributors="${major_contributors:+$major_contributors, }$author" + else + minor_contributors="${minor_contributors:+$minor_contributors, }$author" + fi + fi + done; \ + echo "$original_author" + echo "${major_contributors:-none}" + echo "${minor_contributors:-none}" ) +done diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl index 72bc006d7..1548e3fa6 100755 --- a/contrib/update-copyright.pl +++ b/contrib/update-copyright.pl @@ -1,5 +1,10 @@ #!/usr/bin/perl -w # +# update-copyright.pl +# Morgan Deters for CVC4 +# +# usage: update-copyright [ files/directories... ] +# # This script goes through a source directory rewriting the top bits of # source files to match a template (inline, below). For files with no # top comment, it adds a fresh one. @@ -50,12 +55,12 @@ EOF use strict; use Fcntl ':mode'; +my $dir = $0; +$dir =~ s,/[^/]+/*$,,; + my @searchdirs = (); if($#ARGV == -1) { - my $dir = $0; - $dir =~ s,/[^/]+/*$,,; - - (chdir($dir."/..") && -f "src/include/cvc4_expr.h") || die "can't find top-level source directory for CVC4"; + (chdir($dir."/..") && -f "src/include/cvc4_config.h") || die "can't find top-level source directory for CVC4"; my $pwd = `pwd`; chomp $pwd; print <', $outfile) || die "error opening $outfile for writing"; + open(my $AUTHOR, "$dir/get-authors " . $infile . '|'); + my $author = <$AUTHOR>; chomp $author; + my $major_contributors = <$AUTHOR>; chomp $major_contributors; + my $minor_contributors = <$AUTHOR>; chomp $minor_contributors; + close $AUTHOR; $_ = <$IN>; if(m,^(%{)?/\*\*\*\*\*,) { print "updating\n"; @@ -112,6 +122,9 @@ sub recurse { print $OUT "/********************* -*- C++ -*- */\n"; } print $OUT "/** $file\n"; + print $OUT " ** Original author: $author\n"; + print $OUT " ** Major contributors: $major_contributors\n"; + print $OUT " ** Minor contributors (to current version): $minor_contributors\n"; print $OUT $standard_template; print $OUT " **\n"; while(my $line = <$IN>) { @@ -126,6 +139,9 @@ sub recurse { print $OUT "/********************* -*- C++ -*- */\n"; } print $OUT "/** $file\n"; + print $OUT " ** Original author: $author\n"; + print $OUT " ** Major contributors: $major_contributors\n"; + print $OUT " ** Minor contributors (to current version): $minor_contributors\n"; print $OUT $standard_template; print $OUT " **\n"; print $OUT " ** [[ Add file-specific comments here ]]\n"; diff --git a/src/context/context.cpp b/src/context/context.cpp index 005c3bd6a..3635d0c07 100644 --- a/src/context/context.cpp +++ b/src/context/context.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** context.cpp + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/context/context.h b/src/context/context.h index 6cc36ae9b..68667c223 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** context.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** Context class and context manager. **/ #ifndef __CVC4__CONTEXT__CONTEXT_H diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp index 3b4089b25..d772b886f 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** context_mm.cpp + ** Original author: barrett + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/context/context_mm.h b/src/context/context_mm.h index d48cbedc0..eeaa0a2c8 100644 --- a/src/context/context_mm.h +++ b/src/context/context_mm.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** context_mm.h + ** Original author: barrett + ** Major contributors: none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h index 597be0fe7..7fa828237 100644 --- a/src/expr/attr_type.h +++ b/src/expr/attr_type.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** attr_type.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): dejan, taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** Node attribute describing the type of a node. **/ #ifndef __CVC4__EXPR__ATTR_TYPE_H diff --git a/src/expr/attr_var_name.h b/src/expr/attr_var_name.h index 13a2ec36f..a17a3ba18 100644 --- a/src/expr/attr_var_name.h +++ b/src/expr/attr_var_name.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ -/** attr_type.h +/** attr_var_name.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** The node attribute describing variable names. **/ #ifndef __CVC4__EXPR__ATTR_VAR_NAME_H diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index eacd1cb24..ee9334f3c 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -1,9 +1,17 @@ -/* - * expr.cpp - * - * Created on: Dec 10, 2009 - * Author: dejan - */ +/********************* -*- C++ -*- */ +/** expr.cpp + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): taking + ** 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. + ** + ** [[ Add file-specific comments here ]] + **/ #include "expr/expr.h" #include "expr/node.h" diff --git a/src/expr/expr.h b/src/expr/expr.h index a0a646900..447c35f77 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -1,9 +1,17 @@ -/* - * expr.h - * - * Created on: Dec 10, 2009 - * Author: dejan - */ +/********************* -*- C++ -*- */ +/** expr.h + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): taking, mdeters + ** 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. + ** + ** Public-facing expression interface. + **/ #ifndef __CVC4__EXPR_H #define __CVC4__EXPR_H diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index ea1649e12..ea1ade477 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -1,3 +1,18 @@ +/********************* -*- C++ -*- */ +/** expr_manager.cpp + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** 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. + ** + ** [[ Add file-specific comments here ]] + **/ + /* * expr_manager.cpp * diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index 645193ecf..ace8b2d1c 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -1,9 +1,17 @@ -/* - * expr_manager.h - * - * Created on: Dec 10, 2009 - * Author: dejan - */ +/********************* -*- C++ -*- */ +/** expr_manager.h + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): taking + ** 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. + ** + ** Public-facing expression manager interface. + **/ #ifndef __CVC4__EXPR_MANAGER_H #define __CVC4__EXPR_MANAGER_H diff --git a/src/expr/kind.h b/src/expr/kind.h index 624ab7337..ea9dbd662 100644 --- a/src/expr/kind.h +++ b/src/expr/kind.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** kind.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** Kinds of Nodes. **/ #ifndef __CVC4__KIND_H diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 334cf1b0e..9c73b982c 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** node.cpp + ** Original author: mdeters + ** Major contributors: dejan + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/node.h b/src/expr/node.h index aad0689bb..9bb138b21 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** node.h + ** Original author: mdeters + ** Major contributors: dejan + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,7 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** Reference-counted encapsulation of a pointer to an expression. + ** Reference-counted encapsulation of a pointer to node information. **/ #include "expr/node_value.h" diff --git a/src/expr/node_attribute.h b/src/expr/node_attribute.h index 0b759efb4..021e64649 100644 --- a/src/expr/node_attribute.h +++ b/src/expr/node_attribute.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ -/** expr_attribute.h +/** node_attribute.h + ** Original author: mdeters + ** Major contributors: dejan + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** Node attributes. **/ #ifndef __CVC4__EXPR__NODE_ATTRIBUTE_H diff --git a/src/expr/node_builder.cpp b/src/expr/node_builder.cpp index 0a36421f2..9e24fa280 100644 --- a/src/expr/node_builder.cpp +++ b/src/expr/node_builder.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** node_builder.cpp + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 63048c1ac..b974ecc67 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** node_builder.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** A builder interface for nodes. **/ #ifndef __CVC4__NODE_BUILDER_H diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 7e871d9c3..d752db88f 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** node_manager.cpp + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 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 643f09f11..827c6c1b7 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** node_manager.h + ** Original author: mdeters + ** Major contributors: dejan + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** A manager for Nodes. **/ #ifndef __CVC4__NODE_MANAGER_H diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 42b7b05e4..6724b0771 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** node_value.cpp + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 75c694ec9..352be7d27 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** node_value.h + ** Original author: mdeters + ** Major contributors: dejan + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/include/cvc4_config.h b/src/include/cvc4_config.h index f1877781f..9cf9a182b 100644 --- a/src/include/cvc4_config.h +++ b/src/include/cvc4_config.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** cvc4_config.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,7 +10,8 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** [[ Add file-specific comments here ]] + ** Macros that should be defined everywhere during the building of + ** the libraries and driver binary. **/ #ifndef __CVC4_CONFIG_H diff --git a/src/main/about.h b/src/main/about.h index 592c09551..ec6f3dced 100644 --- a/src/main/about.h +++ b/src/main/about.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** about.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 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 24c96f69a..c191b2a15 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** getopt.cpp + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): barrett, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 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 187a0f316..ba71b043f 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** main.cpp + ** Original author: mdeters + ** Major contributors: barrett, dejan + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/main/main.h b/src/main/main.h index 0141e2848..c44cd9d67 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** main.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): dejan, barrett ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 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 d48c1c96d..e9d8aa983 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** usage.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/main/util.cpp b/src/main/util.cpp index 94a295d54..9bb96d853 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** util.cpp + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 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 1baaf2139..c42415c54 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -1,3 +1,18 @@ +/********************* -*- C++ -*- */ +/** antlr_parser.cpp + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): cconway, mdeters + ** 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. + ** + ** [[ Add file-specific comments here ]] + **/ + /* * antlr_parser.cpp * diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index b2ef3f181..8a9dea5ad 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -1,9 +1,17 @@ -/* - * antlr_parser.h - * - * Created on: Nov 30, 2009 - * Author: dejan - */ +/********************* -*- C++ -*- */ +/** antlr_parser.h + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): mdeters, cconway + ** 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. + ** + ** Base for ANTLR parser classes. + **/ #ifndef CVC4_PARSER_H_ #define CVC4_PARSER_H_ diff --git a/src/parser/cvc/cvc_parser.cpp b/src/parser/cvc/cvc_parser.cpp index adeb5761d..57d5e6c96 100644 --- a/src/parser/cvc/cvc_parser.cpp +++ b/src/parser/cvc/cvc_parser.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** cvc_parser.cpp + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/cvc/cvc_parser.h b/src/parser/cvc/cvc_parser.h index 9cb6b7594..82d659566 100644 --- a/src/parser/cvc/cvc_parser.h +++ b/src/parser/cvc/cvc_parser.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** cvc_parser.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 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 8d4af5ba1..2ff409686 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** parser.cpp + ** Original author: mdeters + ** Major contributors: dejan + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 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 7755d65f0..b448cd2a6 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** parser.h + ** Original author: mdeters + ** Major contributors: dejan + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index b2cf8bc55..3504eeba2 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** parser_exception.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,7 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** Exception class. + ** Exception class for parse errors. **/ #ifndef __CVC4__PARSER__PARSER_EXCEPTION_H diff --git a/src/parser/smt/smt_parser.cpp b/src/parser/smt/smt_parser.cpp index 65d36690c..8c5773e32 100644 --- a/src/parser/smt/smt_parser.cpp +++ b/src/parser/smt/smt_parser.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** smt_parser.cpp + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/smt/smt_parser.h b/src/parser/smt/smt_parser.h index 6927888cf..21c278a37 100644 --- a/src/parser/smt/smt_parser.h +++ b/src/parser/smt/smt_parser.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** smt_parser.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): cconway, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 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 2c4f0e8b7..66d5727d6 100644 --- a/src/parser/symbol_table.h +++ b/src/parser/symbol_table.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** symbol_table.h + ** Original author: cconway + ** Major contributors: dejan, mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** A symbol table for the parsers' use. **/ #ifndef __CVC4__PARSER__SYMBOL_TABLE_H diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index caf87428b..ffd335453 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ -/** prop_engine.h +/** prop_engine.cpp + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 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 21a6669d7..6cb818d10 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** prop_engine.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,8 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** The PropEngine (proposiitonal engine); main interface point + ** between CVC4's SMT infrastructure and the SAT solver. **/ #ifndef __CVC4__PROP_ENGINE_H diff --git a/src/prop/sat.h b/src/prop/sat.h index 32ca9e983..9e216b126 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** sat.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** SAT Solver. **/ #ifndef __CVC4__PROP__SAT_H diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 23dc1153a..4c7f6a156 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** smt_engine.cpp + ** Original author: mdeters + ** Major contributors: dejan + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 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 edcbdcca3..98cffb6de 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** smt_engine.h + ** Original author: mdeters + ** Major contributors: dejan + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** SmtEngine: the main public entry point of libcvc4. **/ #ifndef __CVC4__SMT_ENGINE_H diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 024d192e6..c4b2b8d83 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** theory.cpp + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** Base for theory interface. **/ #include "theory/theory.h" diff --git a/src/theory/theory.h b/src/theory/theory.h index 21124375a..b695ca03d 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** theory.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** Base of the theory interface. **/ #ifndef __CVC4__THEORY__THEORY_H diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 6d0b9d91d..2289f2fea 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** theory_engine.cpp + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** The theory engine. **/ #include "theory/theory_engine.h" diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index d6d8691b2..65a317433 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** theory_engine.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** The theory engine. **/ #ifndef __CVC4__THEORY_ENGINE_H diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp index a86e2021a..337649039 100644 --- a/src/util/Assert.cpp +++ b/src/util/Assert.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** Assert.cpp + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/Assert.h b/src/util/Assert.h index 26a1ee7d4..49c97e9b6 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** Assert.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/command.cpp b/src/util/command.cpp index 3911897f5..5a5b766cb 100644 --- a/src/util/command.cpp +++ b/src/util/command.cpp @@ -1,3 +1,18 @@ +/********************* -*- C++ -*- */ +/** command.cpp + ** Original author: mdeters + ** Major contributors: dejan + ** Minor contributors (to current version): none + ** 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. + ** + ** [[ Add file-specific comments here ]] + **/ + /* * command.cpp * diff --git a/src/util/command.h b/src/util/command.h index 221c513f0..9cc009d01 100644 --- a/src/util/command.h +++ b/src/util/command.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** command.h + ** Original author: mdeters + ** Major contributors: dejan + ** Minor contributors (to current version): cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,8 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** Implementation of the command pattern on SmtEngines. Generated by + ** the parser. **/ #ifndef __CVC4__COMMAND_H diff --git a/src/util/debug.h b/src/util/debug.h index 14dc0fbd1..800106764 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** debug.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,20 +10,27 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** Debugging things. + ** + ** These are low-level assertions! Generally you should use + ** CVC4::Assert() instead (they throw an exception!). See + ** util/Assert.h. **/ #ifndef __CVC4__DEBUG_H #define __CVC4__DEBUG_H +#include "cvc4_config.h" + #include -#ifdef DEBUG +#ifdef CVC4_ASSERTIONS // the __builtin_expect() helps us if assert is built-in or a macro -# define cvc4assert(x) assert(__builtin_expect((x), 1)) +# define cvc4assert(x) assert(EXPECT_TRUE( x )) #else // TODO: use a compiler annotation when assertions are off ? // (to improve optimization) -# define cvc4assert(x) -#endif /* DEBUG */ +# define cvc4assert(x) /*EXPECT_TRUE( x )*/ +#endif /* CVC4_ASSERTIONS */ #endif /* __CVC4__DEBUG_H */ diff --git a/src/util/decision_engine.cpp b/src/util/decision_engine.cpp index ae79f920d..36f99f4ac 100644 --- a/src/util/decision_engine.cpp +++ b/src/util/decision_engine.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** decision_engine.cpp + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h index 3a093211c..58f9400b5 100644 --- a/src/util/decision_engine.h +++ b/src/util/decision_engine.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** decision_engine.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** A decision engine for CVC4. **/ #ifndef __CVC4__DECISION_ENGINE_H diff --git a/src/util/exception.h b/src/util/exception.h index d239f48de..8481a8504 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** exception.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,9 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** Exception class. - ** - ** As many paragraphs as you like. + ** CVC4's exception base class and some associated utilities. **/ #ifndef __CVC4__EXCEPTION_H diff --git a/src/util/literal.h b/src/util/literal.h index 3ec216a6a..921a9ef0d 100644 --- a/src/util/literal.h +++ b/src/util/literal.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** literal.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** A literal. **/ #ifndef __CVC4__LITERAL_H diff --git a/src/util/model.h b/src/util/model.h index cf006b3e1..b79032221 100644 --- a/src/util/model.h +++ b/src/util/model.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** model.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** A model. **/ #ifndef __CVC4__MODEL_H diff --git a/src/util/options.h b/src/util/options.h index 8d2d113a2..2bfbf675f 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** options.h + ** Original author: mdeters + ** Major contributors: dejan + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,7 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** [[ Add file-specific comments here ]] + ** Global (command-line or equivalent) tuning parameters. **/ #include diff --git a/src/util/output.cpp b/src/util/output.cpp index 103a3d61a..05c74918c 100644 --- a/src/util/output.cpp +++ b/src/util/output.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** output.cpp + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 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 43dfe8a40..57ce5f3ca 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** output.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/result.h b/src/util/result.h index 8d9b93a1e..87686d59c 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** result.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** Encapsulation of the result of a query. **/ #ifndef __CVC4__RESULT_H diff --git a/src/util/unique_id.h b/src/util/unique_id.h index 4ac80f772..633a544f0 100644 --- a/src/util/unique_id.h +++ b/src/util/unique_id.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** unique_id.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** A mechanism for getting a compile-time unique ID. **/ #ifndef __CVC4__UNIQUE_ID_H diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index d8f321f10..61eef32d5 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -1,23 +1,39 @@ +# all unit tests +UNIT_TESTS = \ + expr/node_white \ + expr/node_black \ + parser/cvc/cvc_parser_black \ + parser/smt/smt_parser_black + +# things that aren't tests but that tests rely on and need to +# go into the distribution +TEST_DEPENDENCIES = + if HAVE_CXXTESTGEN AM_CPPFLAGS = \ - -I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src" + -I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src" \ + $(TEST_CPPFLAGS) +AM_CXXFLAGS = $(TEST_CXXFLAGS) +AM_LDFLAGS = $(TEST_LDFLAGS) + AM_CXXFLAGS_WHITE = -fno-access-control AM_CXXFLAGS_BLACK = AM_CXXFLAGS_PUBLIC = AM_LDFLAGS_WHITE = \ - @abs_top_builddir@/src/parser/libcvc4parser_noinst.la \ - @abs_top_builddir@/src/libcvc4_noinst.la + @abs_top_builddir@/src/parser/libcvc4parser_noinst.la \ + @abs_top_builddir@/src/libcvc4_noinst.la AM_LDFLAGS_BLACK = \ - $(AM_LDFLAGS_WHITE) + @abs_top_builddir@/src/parser/libcvc4parser_noinst.la \ + @abs_top_builddir@/src/libcvc4_noinst.la AM_LDFLAGS_PUBLIC = \ - @abs_top_builddir@/src/libcvc4.la + @abs_top_builddir@/src/libcvc4.la -TESTS = \ - expr/node_white \ - expr/node_black \ - parser/cvc/cvc_parser_black \ - parser/smt/smt_parser_black +TESTS = $(UNIT_TESTS) + +EXTRA_DIST = \ + no_cxxtest \ + $(TEST_DEPENDENCIES) # without these here, LTCXXCOMPILE, CXXLINK, etc., aren't set :-( noinst_LTLIBRARIES = libdummy.la @@ -28,18 +44,12 @@ $(TESTS:%=%.cpp): %.cpp: %.h mkdir -p `dirname "$@"` @CXXTESTGEN@ --have-eh --have-std --error-printer -o "$@" "$<" $(filter %_white,$(TESTS)): %_white: %_white.cpp -# get these in here somehow -# $(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS) $(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo $< $(CXXLINK) $(AM_LDFLAGS_WHITE) $@.lo $(filter %_black,$(TESTS)): %_black: %_black.cpp -# get these in here somehow -# $(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS) $(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@.lo $< $(CXXLINK) $(AM_LDFLAGS_BLACK) $@.lo $(filter %_public,$(TESTS)): %_public: %_public.cpp -# get these in here somehow -# $(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS) $(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo $< $(CXXLINK) $(AM_LDFLAGS_PUBLIC) $@.lo @@ -50,4 +60,8 @@ else # force a user-visible failure for "make check" TESTS = no_cxxtest +EXTRA_DIST = \ + $(UNIT_TESTS) \ + $(TEST_DEPENDENCIES) + endif diff --git a/test/unit/Makefile.in b/test/unit/Makefile.in index 251ef2dfe..6e518d527 100644 --- a/test/unit/Makefile.in +++ b/test/unit/Makefile.in @@ -213,30 +213,49 @@ target_vendor = @target_vendor@ top_build_prefix = @top_build_prefix@ top_builddir = @top_builddir@ top_srcdir = @top_srcdir@ + +# all unit tests +UNIT_TESTS = \ + expr/node_white \ + expr/node_black \ + parser/cvc/cvc_parser_black \ + parser/smt/smt_parser_black + + +# things that aren't tests but that tests rely on and need to +# go into the distribution +TEST_DEPENDENCIES = @HAVE_CXXTESTGEN_TRUE@AM_CPPFLAGS = \ -@HAVE_CXXTESTGEN_TRUE@ -I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src" +@HAVE_CXXTESTGEN_TRUE@ -I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src" \ +@HAVE_CXXTESTGEN_TRUE@ $(TEST_CPPFLAGS) +@HAVE_CXXTESTGEN_TRUE@AM_CXXFLAGS = $(TEST_CXXFLAGS) +@HAVE_CXXTESTGEN_TRUE@AM_LDFLAGS = $(TEST_LDFLAGS) @HAVE_CXXTESTGEN_TRUE@AM_CXXFLAGS_WHITE = -fno-access-control @HAVE_CXXTESTGEN_TRUE@AM_CXXFLAGS_BLACK = @HAVE_CXXTESTGEN_TRUE@AM_CXXFLAGS_PUBLIC = @HAVE_CXXTESTGEN_TRUE@AM_LDFLAGS_WHITE = \ -@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/parser/libcvc4parser_noinst.la \ -@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/libcvc4_noinst.la +@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/parser/libcvc4parser_noinst.la \ +@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/libcvc4_noinst.la @HAVE_CXXTESTGEN_TRUE@AM_LDFLAGS_BLACK = \ -@HAVE_CXXTESTGEN_TRUE@ $(AM_LDFLAGS_WHITE) +@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/parser/libcvc4parser_noinst.la \ +@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/libcvc4_noinst.la @HAVE_CXXTESTGEN_TRUE@AM_LDFLAGS_PUBLIC = \ -@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/libcvc4.la +@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/libcvc4.la # force a user-visible failure for "make check" @HAVE_CXXTESTGEN_FALSE@TESTS = no_cxxtest -@HAVE_CXXTESTGEN_TRUE@TESTS = \ -@HAVE_CXXTESTGEN_TRUE@ expr/node_white \ -@HAVE_CXXTESTGEN_TRUE@ expr/node_black \ -@HAVE_CXXTESTGEN_TRUE@ parser/cvc/cvc_parser_black \ -@HAVE_CXXTESTGEN_TRUE@ parser/smt/smt_parser_black +@HAVE_CXXTESTGEN_TRUE@TESTS = $(UNIT_TESTS) +@HAVE_CXXTESTGEN_FALSE@EXTRA_DIST = \ +@HAVE_CXXTESTGEN_FALSE@ $(UNIT_TESTS) \ +@HAVE_CXXTESTGEN_FALSE@ $(TEST_DEPENDENCIES) + +@HAVE_CXXTESTGEN_TRUE@EXTRA_DIST = \ +@HAVE_CXXTESTGEN_TRUE@ no_cxxtest \ +@HAVE_CXXTESTGEN_TRUE@ $(TEST_DEPENDENCIES) # without these here, LTCXXCOMPILE, CXXLINK, etc., aren't set :-( @@ -629,18 +648,12 @@ uninstall-am: @HAVE_CXXTESTGEN_TRUE@ mkdir -p `dirname "$@"` @HAVE_CXXTESTGEN_TRUE@ @CXXTESTGEN@ --have-eh --have-std --error-printer -o "$@" "$<" @HAVE_CXXTESTGEN_TRUE@$(filter %_white,$(TESTS)): %_white: %_white.cpp -# get these in here somehow -# $(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS) @HAVE_CXXTESTGEN_TRUE@ $(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo $< @HAVE_CXXTESTGEN_TRUE@ $(CXXLINK) $(AM_LDFLAGS_WHITE) $@.lo @HAVE_CXXTESTGEN_TRUE@$(filter %_black,$(TESTS)): %_black: %_black.cpp -# get these in here somehow -# $(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS) @HAVE_CXXTESTGEN_TRUE@ $(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@.lo $< @HAVE_CXXTESTGEN_TRUE@ $(CXXLINK) $(AM_LDFLAGS_BLACK) $@.lo @HAVE_CXXTESTGEN_TRUE@$(filter %_public,$(TESTS)): %_public: %_public.cpp -# get these in here somehow -# $(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS) @HAVE_CXXTESTGEN_TRUE@ $(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo $< @HAVE_CXXTESTGEN_TRUE@ $(CXXLINK) $(AM_LDFLAGS_PUBLIC) $@.lo diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index c95900383..aa99c70c4 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -1,4 +1,17 @@ -/* Black box testing of CVC4::Node. */ +/********************* -*- C++ -*- */ +/** node_black.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): dejan + ** 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. + ** + ** Black box testing of CVC4::Node. + **/ #include diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index dd462fdd8..96a30e582 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -1,4 +1,17 @@ -/* White box testing of CVC4::Node. */ +/********************* -*- C++ -*- */ +/** node_white.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): dejan + ** 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. + ** + ** White box testing of CVC4::Node. + **/ #include diff --git a/test/unit/parser/cvc/cvc_parser_black.h b/test/unit/parser/cvc/cvc_parser_black.h index e99cce44d..4679d358c 100644 --- a/test/unit/parser/cvc/cvc_parser_black.h +++ b/test/unit/parser/cvc/cvc_parser_black.h @@ -1,4 +1,17 @@ -/* Black box testing of CVC4::parser::CvcParser. */ +/********************* -*- C++ -*- */ +/** cvc_parser_black.h + ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): none + ** 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. + ** + ** Black box testing of CVC4::parser::CvcParser. + **/ #include //#include -- 2.30.2