fixes for "make dist" and "make doc", minor cleanups

9 files changed, 29 insertions, 18 deletions

diff --git a/config/doxygen.cfg b/config/doxygen.cfg
index f0598e0c4..65d3c3103 100644
--- a/config/doxygen.cfg
+++ b/config/doxygen.cfg
@@ -225,7 +225,7 @@ EXTENSION_MAPPING      =
 # func(std::string) {}). This also make the inheritance and collaboration
 # diagrams that involve STL classes more complete and accurate.
 
-BUILTIN_STL_SUPPORT    = NO
+BUILTIN_STL_SUPPORT    = YES
 
 # If you use Microsoft's C++/CLI language, you should set this option to YES to
 # enable parsing support.
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 712273473..eb67277a1 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -394,7 +394,7 @@ public:
 
   /** Returns the maximum arity of the given kind. */
   static unsigned maxArity(Kind kind);
-};
+};/* class ExprManager */
 
 ${mkConst_instantiations}
 
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 2e7e3ca3d..b2f76b39d 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -164,12 +164,17 @@ class CVC4_PUBLIC Parser {
 
 protected:
   /**
-   * Create a parser state. NOTE: The parser takes "ownership" of the given
+   * Create a parser state.
+   *
+   * @attention The parser takes "ownership" of the given
    * input and will delete it on destruction.
    *
    * @param exprManager the expression manager to use when creating expressions
    * @param input the parser input
    * @param strictMode whether to incorporate strict(er) compliance checks
+   * @param parseOnly whether we are parsing only (and therefore certain checks
+   * need not be performed, like those about unimplemented features, @see
+   * unimplementedFeature())
    */
   Parser(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b8f8a522f..c381ba5bd 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -87,7 +87,7 @@ public:
  * This is an inelegant solution, but for the present, it will work.
  * The point of this is to separate the public and private portions of
  * the SmtEngine class, so that smt_engine.h doesn't
- * #include "expr/node.h", which is a private CVC4 header (and can lead
+ * include "expr/node.h", which is a private CVC4 header (and can lead
  * to linking errors due to the improper inlining of non-visible symbols
  * into user code!).
  *
diff --git a/src/theory/datatypes/explanation_manager.cpp b/src/theory/datatypes/explanation_manager.cpp
index 06f7bb29e..10ee9bf64 100644
--- a/src/theory/datatypes/explanation_manager.cpp
+++ b/src/theory/datatypes/explanation_manager.cpp
@@ -1,11 +1,11 @@
-#include "theory/datatypes/explanation_manager.h"

-

+#include "theory/datatypes/explanation_manager.h"
+
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::context;
 using namespace CVC4::theory;
-using namespace CVC4::theory::datatypes;

+using namespace CVC4::theory::datatypes;
 
 void ProofManager::setExplanation( Node n, Node jn, unsigned r ) 
 { 
diff --git a/src/util/propositional_query.h b/src/util/propositional_query.h
index f520f142d..2d269e801 100644
--- a/src/util/propositional_query.h
+++ b/src/util/propositional_query.h
@@ -40,22 +40,22 @@ public:
   /**
    * Returns whether a node q is propositionally satisfiable.
    *
-   * @params q Node to be checked for satisfiability.
-   * @params e A number representing the effort to use between 0 (minimum effort),
+   * @param q Node to be checked for satisfiability.
+   * @param e A number representing the effort to use between 0 (minimum effort),
    *  and 1 (maximum effort).
-   * @precondition q is a ground formula.
-   * @precondition effort is between 0 and 1.
+   * @pre q is a ground formula.
+   * @pre effort is between 0 and 1.
    */
   static Result isSatisfiable(TNode q);
 
   /**
    * Returns whether a node q is a propositional tautology.
    *
-   * @params q Node to be checked for satisfiability.
-   * @params e A number representing the effort to use between 0 (minimum effort),
+   * @param q Node to be checked for satisfiability.
+   * @param e A number representing the effort to use between 0 (minimum effort),
    *  and 1 (maximum effort).
-   * @precondition q is a ground formula.
-   * @precondition effort is between 0 and 1.
+   * @pre q is a ground formula.
+   * @pre effort is between 0 and 1.
    */
   static Result isTautology(TNode q);
 
diff --git a/src/util/recursion_breaker.h b/src/util/recursion_breaker.h
index 6573e9b64..1146a4429 100644
--- a/src/util/recursion_breaker.h
+++ b/src/util/recursion_breaker.h
@@ -18,6 +18,7 @@
  ** A breadcrumb trail is left, and a function can query the breaker
  ** to see if recursion has occurred.  For example:
  **
+ ** @code
  **   int foo(int x) {
  **     RecursionBreaker<int> breaker("foo", x);
  **     if(breaker.isRecursion()) {
@@ -33,6 +34,7 @@
  **     cout << "x == " << x << ", y == " << y << " ==> " << z << endl;
  **     return z;
  **   }
+ ** @endcode
  **
  ** Recursion occurs after a while in this example, and the recursion
  ** is broken by the RecursionBreaker.
diff --git a/src/util/trans_closure.h b/src/util/trans_closure.h
index c7538bc41..951a32a63 100644
--- a/src/util/trans_closure.h
+++ b/src/util/trans_closure.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file transitive_closure.h
+/*! \file trans_closure.h
  ** \verbatim
  ** Original author: barrett
  ** Major contributors: none
diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am
index 8faebddad..86a6b031c 100644
--- a/test/regress/regress0/uflra/Makefile.am
+++ b/test/regress/regress0/uflra/Makefile.am
@@ -6,7 +6,8 @@ MAKEFLAGS = -k
 # put it below in "TESTS +="
 
 # Regression tests for SMT inputs
-SMT_TESTS = pb_real_10_0100_10_10.smt \
+SMT_TESTS = \
+	pb_real_10_0100_10_10.smt \
 	pb_real_10_0100_10_11.smt \
 	pb_real_10_0100_10_15.smt \
 	pb_real_10_0100_10_16.smt \
@@ -14,7 +15,6 @@ SMT_TESTS = pb_real_10_0100_10_10.smt \
 	pb_real_10_0200_10_22.smt \
 	pb_real_10_0200_10_26.smt \
 	pb_real_10_0200_10_29.smt
-	
 
 # Regression tests for SMT2 inputs
 SMT2_TESTS =
@@ -27,6 +27,10 @@ BUG_TESTS =
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
+# Necessary to get automake's attention when splitting TESTS into
+# SMT_TESTS, SMT2_TESTS, etc..
+EXTRA_DIST = $(TESTS)
+
 # synonyms for "check" in this directory
 .PHONY: regress regress0 test
 regress regress0 test: check