diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/propositional_query.h | 16 | ||||
-rw-r--r-- | src/util/recursion_breaker.h | 2 | ||||
-rw-r--r-- | src/util/trans_closure.h | 2 |
3 files changed, 11 insertions, 9 deletions
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 |