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

diff --git a/config/doxygen.cfg b/config/doxygen.cfg
index f0598e0c43162f9b3620e4e9179dd75c8a46f845..65d3c31030475678c56ecb785275200e49fc00c3 100644 (file)
--- 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 712273473f7f79ce7a6aabcea0d0b7ddf210dbda..eb67277a1579e5e29358b78e37caa5d83a9e2304 100644 (file)
--- 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 2e7e3ca3dd6d3421c3a0158e698801cf37b8fb14..b2f76b39dcb4df6fd45f62cfb5139de7562b10ac 100644 (file)
--- 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 b8f8a522f6760e9ada23b1f97333f99a8a8fec5a..c381ba5bda97a060404fa64966ec2a2cfb974064 100644 (file)
--- 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 06f7bb29e1aedfbb09b2d65a64d436720ec7dced..10ee9bf64e7a33e6c70a9803e41616b915d745ab 100644 (file)
--- a/src/theory/datatypes/explanation_manager.cpp
+++ b/src/theory/datatypes/explanation_manager.cpp
@@ -1,11 +1,11 @@
-#include "theory/datatypes/explanation_manager.h"\r
-\r
+#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;\r
+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 f520f142d66e34491f923abfe480a7def4580d1b..2d269e801dd2cff1bc632f13e1db102bedb9b2bf 100644 (file)
--- 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 6573e9b64b934330903aa802f45133730b840d98..1146a4429fab4fe431d62e0cda97f231ba826cc8 100644 (file)
--- 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 c7538bc415af355eab6cc6652ca6532c7c27349c..951a32a634e1b83b2a9bb801a52548af69676606 100644 (file)
--- 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 8faebddadc8f19192375ca2d9dc49371e23fada2..86a6b031c78bd5a1c22997c7f9423a1e889425fc 100644 (file)
--- 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