From 5707fbf2af8c3a941ce3249cf0cb3190a5b069e4 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 23 May 2011 23:15:25 +0000 Subject: [PATCH] fixes for "make dist" and "make doc", minor cleanups --- config/doxygen.cfg | 2 +- src/expr/expr_manager_template.h | 2 +- src/parser/parser.h | 7 ++++++- src/smt/smt_engine.cpp | 2 +- src/theory/datatypes/explanation_manager.cpp | 6 +++--- src/util/propositional_query.h | 16 ++++++++-------- src/util/recursion_breaker.h | 2 ++ src/util/trans_closure.h | 2 +- test/regress/regress0/uflra/Makefile.am | 8 ++++++-- 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 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 -- 2.30.2