* public/private code untangled (smt/smt_engine.h no longer #includes

  expr/node.h).  This removes the warnings we had during compilation,
  and heads off a number of potential linking errors due to improper
  inlining of private (library-only) stuff in client (out-of-library)
  code.

* "configure" now takes some options as part of a "bare-option" build
  type (e.g., "./configure debug-coverage" or "./configure production-muzzle").

* split cdo.h, cdlist.h, cdmap.h, and cdset.h from context.h

* split cdlist_black unit test from context_black

* implement CDMap<>.

* give ExprManagers ownership of the context (and have SmtEngine share
  that one)

* fix main driver to properly report file-not-found

* fix MemoryMappedInputBuffer class to report reasons for
  "errno"-returned system errors

* src/expr/attribute.h: context-dependent attribute kinds now
  supported

* test/unit/expr/node_white.h: context-dependent attribute tests

* src/prop/cnf_conversion.h and associated parts of src/util/options.h
  and src/main/getopt.cpp: obsolete command-line option, removed.

* src/util/Assert.h: assertions are now somewhat more useful (in debug
  builds, anyway) during stack unwinding.

* test/unit/theory/theory_black.h: test context-dependent behavior of
  registerTerm() attribute for theories

* src/expr/node_builder.h: formatting, fixes for arithmetic
  convenience node builders, check memory allocations

* test/unit/expr/node_builder_black.h: add tessts for addition,
  subtraction, unary minus, and multiplication convenience node
  builders

* src/expr/attribute.h: more comments

* (various) code formatting, comment cleanup, added throws specifier
  to some destructors

* contrib/code-checker: prototype perl script to test (some) code policy

* contrib/indent-settings: command line for GNU indent to indent using
  CVC4 style (sort of; this is a work in progress)

* COPYING: legal stuff

* DESIGN_QUESTIONS: obsolete, removed

1 files changed, 96 insertions, 0 deletions

diff --git a/contrib/code-checker b/contrib/code-checker
new file mode 100755
index 000000000..a40dc61af
--- /dev/null
+++ b/contrib/code-checker
@@ -0,0 +1,96 @@
+#!/usr/bin/perl -w
+
+use strict;
+
+while($#ARGV >= 0) {
+  my %FP;
+  my $file = shift @ARGV;
+
+  local $/ = undef;
+
+  open(FP, $file) || die "can't read $file";
+  print "checking $file...\n";
+  binmode FP;
+  my $buf = <FP>;
+  close FP;
+
+  print "file named incorrectly; use *.h: $file\n" if $file =~ /\.(hpp|H|hh)$/;
+  print "file named incorrectly; use *.cpp: $file\n" if $file =~ /\.(C|cc)$/;
+  if($file =~ /\.(h|hpp|H)$/) {
+    check_as_header($buf);
+  } elsif($file =~ /\.(h|cpp|C)$/) {
+    check_as_source($buf);
+  } else {
+    die "$file not checked (unknown type of file)";
+  }
+  open(FP, "cpp -nostdinc \"$file\" 2>/dev/null |") || die "can't cpp $file";
+  binmode FP;
+  $buf = <FP>;
+  close FP;
+
+  if($file =~ /\.(h|hpp|H)$/) {
+    check_as_header_cpp($buf);
+  } elsif($file =~ /\.(h|cpp|C)$/) {
+    check_as_source_cpp($buf);
+  } else {
+    die "$file not checked (unknown type of file)";
+  }
+}
+
+sub check_as_any {
+  my($buf) = @_;
+
+  print "no file head comment\n" unless $buf =~ m,^/*\*\*\*,;
+}
+
+sub check_as_header {
+  my($buf) = @_;
+  check_as_any($buf);
+}
+
+sub check_as_source {
+  my($buf) = @_;
+  check_as_any($buf);
+}
+
+sub check_as_any_cpp {
+  my($buf) = @_;
+
+  print "need space between tokens ) and {\n" if $buf =~ /\)\{/;
+  print "need space between tokens 'const' and {\n" if $buf =~ /\bconst\{/;
+  print "need space between tokens ) and 'const'\n" if $buf =~ /\)const\b/;
+  print "need space between tokens 'template' and <\n" if $buf =~ /\btemplate</;
+  print "need space between tokens } and 'else'\n" if $buf =~ /\}else\b/;
+  print "need space between tokens 'else' and {\n" if $buf =~ /\belse\{/;
+  print "need space between tokens 'do' and {\n" if $buf =~ /\bdo\{/;
+  print "need space between tokens } and 'while'\n" if $buf =~ /\}while\b/;
+
+  print "no space permitted before ;\n" if $buf =~ /\s+;/;
+  print "no space permitted between tokens 'if' and (\n" if $buf =~ /\bif\s\(/;
+  print "no space permitted between tokens 'while' and (\n" if $buf =~ /\bwhile\s\(/;
+  print "no space permitted between tokens 'for' and (\n" if $buf =~ /\bfor\s\(/;
+
+  my $code = $buf;
+  $code =~ s,\\.,.,g;
+  $code =~ s,"[^"]*","",g;
+
+  #print "'if' blocks must be braced, '{' should be last character on block opening line\n" if $code =~ /\bif\b.*[^{]\s*$/m;
+  #print "'while' blocks must be braced, '{' should be last character on block opening line\n" if $code =~ /\bwhile\b.*[^{]\s*$/m;
+  #print "'for' blocks must be braced, '{' should be last character on block opening line\n" if $code =~ /\bfor\b.*[^{]\s*$/m;
+  print "'else' cannot start a line (should follow preceding '}')\n" if $code =~ /^\s+else\b/m;
+}
+
+sub check_as_header_cpp {
+  my($buf) = @_;
+  check_as_any_cpp($buf);
+}
+
+sub check_as_source_cpp {
+  my($buf) = @_;
+  check_as_any_cpp($buf);
+}
+
+## Local Variables:
+## perl-indent-level: 2
+## perl-brace-offset: 0
+## End: