Merge from cudd branch. This mostly just adds support for linking

against cudd libraries, the propositional_query class (in util/),
which uses cudd if it's available (and otherwise answers UNKNOWN for
all queries), and the arith theory support for it (currently disabled
per Tim's request, so he can clean it up).

Other changes include:

* contrib/debug-keys - script to print all used keys under Debug(), Trace()
* test/regress/run_regression - minor fix (don't export a variable)
* configure.ac - replace a comment removed by dejan's google perf commit
* some minor copyright/documentation updates, and minor changes to source
  text to make 'clang --analyze' happy.

5 files changed, 37 insertions, 4 deletions

diff --git a/contrib/addsourcedir b/contrib/addsourcedir
index ef6aedd15..00357cadf 100755
--- a/contrib/addsourcedir
+++ b/contrib/addsourcedir
@@ -2,7 +2,7 @@
 #
 # addsourcedir
 # Morgan Deters <mdeters@cs.nyu.edu> for the CVC4 project
-# Copyright (c) 2010  The CVC4 Project
+# Copyright (c) 2010, 2011  The CVC4 Project
 #
 # usage: addsourcedir paths...
 #
diff --git a/contrib/configure-in-place b/contrib/configure-in-place
index 09771676e..9da584d36 100755
--- a/contrib/configure-in-place
+++ b/contrib/configure-in-place
@@ -2,7 +2,7 @@
 #
 # configure-in-place
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010  The CVC4 Project
+# Copyright (c) 2010, 2011  The CVC4 Project
 #
 # usage: configure-in-place [ arguments... ]
 #
diff --git a/contrib/debug-keys b/contrib/debug-keys
new file mode 100755
index 000000000..6d2804974
--- /dev/null
+++ b/contrib/debug-keys
@@ -0,0 +1,33 @@
+#!/bin/bash
+#
+# Lists the Trace() and Debug() keys used in sources.
+#
+# e.g. if Debug("uf") occurs in the sources, then "uf" is printed by this script.
+
+if [ "$1" = "-h" -o "$1" = "-help" -o "$1" = "-?" -o "$1" = "--help" ]; then
+  echo "usage: `basename $0` [dirs...]" >&2
+  echo "This utility will print all Debug("foo") and Trace("foo") keys."
+  echo "With optional dirs..., use dirs instead of top-level \"src\"." >&2
+  exit 1
+fi
+
+if [ $# -eq 0 ]; then
+  cd `dirname "$0"`/..
+
+  if ! [ -d src ]; then
+    echo "`basename $0`: not in CVC4 directory tree?!" >&2
+    exit 1
+  fi
+
+  set src
+fi
+
+echo "Trace and debug flags used in $*:"
+
+while [ $# -gt 0 ]; do
+  dir="$1"
+  shift
+
+  test -r "$dir" && grep -r --exclude-dir=.svn '\(Debug\|Trace\)\(\.isOn\)\?("[^"]\+")' "$dir" | sed 's,.*\(Debug\|Trace\)\(\.isOn\)\?("\([^"]\+\)").*,\3,' | sort -u
+done | sort -u
+
diff --git a/contrib/dimacs_to_smt.pl b/contrib/dimacs_to_smt.pl
index 6c1e0eeea..701768119 100755
--- a/contrib/dimacs_to_smt.pl
+++ b/contrib/dimacs_to_smt.pl
@@ -1,7 +1,7 @@
 #!/usr/bin/perl -w
 # DIMACS to SMT
 # Morgan Deters
-# Copyright (c) 2009, 2010  The CVC4 Project
+# Copyright (c) 2009, 2010, 2011  The CVC4 Project
 
 use strict;
 
diff --git a/contrib/get-authors b/contrib/get-authors
index dbe878d6b..ef6abff8e 100755
--- a/contrib/get-authors
+++ b/contrib/get-authors
@@ -2,7 +2,7 @@
 #
 # get-authors
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2009, 2010  The CVC4 Project
+# Copyright (c) 2009, 2010, 2011  The CVC4 Project
 #
 # usage: get-authors [ files... ]
 #