diff options
| -rw-r--r-- | src/expr/kind_template.h | 6 | ||||
| -rw-r--r-- | src/expr/metakind_template.h | 10 | ||||
| -rwxr-xr-x | src/expr/mkkind | 2 | ||||
| -rw-r--r-- | src/expr/node_builder.h | 2 | ||||
| -rw-r--r-- | src/prop/cnf_stream.h | 1 | ||||
| -rw-r--r-- | src/theory/arith/unate_propagator.cpp | 2 | ||||
| -rw-r--r-- | src/theory/arith/unate_propagator.h | 2 | ||||
| -rw-r--r-- | src/util/congruence_closure.h | 4 |
8 files changed, 14 insertions, 15 deletions
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 718fd58f4..3b1232772 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -28,10 +28,10 @@ namespace CVC4 { namespace kind { enum Kind_t { - UNDEFINED_KIND = -1, /*! undefined */ - NULL_EXPR, /*! Null kind */ + UNDEFINED_KIND = -1, /**< undefined */ + NULL_EXPR, /**< Null kind */ ${kind_decls} - LAST_KIND + LAST_KIND /**< marks the upper-bound of this enumeration */ };/* enum Kind_t */ diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index c4604d40e..515b7978c 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -96,11 +96,11 @@ struct NodeValueCompare { * mean, see src/theory/builtin/kinds. */ enum MetaKind_t { - INVALID = -1, /*! special node non-kinds like NULL_EXPR or LAST_KIND */ - VARIABLE, /*! special node kinds: no operator */ - OPERATOR, /*! operators that get "inlined" */ - PARAMETERIZED, /*! parameterized ops (like APPLYs) that carry extra data */ - CONSTANT /*! constants */ + INVALID = -1, /**< special node non-kinds like NULL_EXPR or LAST_KIND */ + VARIABLE, /**< special node kinds: no operator */ + OPERATOR, /**< operators that get "inlined" */ + PARAMETERIZED, /**< parameterized ops (like APPLYs) that carry extra data */ + CONSTANT /**< constants */ };/* enum MetaKind_t */ }/* CVC4::kind::metakind namespace */ diff --git a/src/expr/mkkind b/src/expr/mkkind index a417b7871..ab80224eb 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -106,7 +106,7 @@ function register_kind { nc=$2 comment=$3 - kind_decls="${kind_decls} $r, /*! $comment */ + kind_decls="${kind_decls} $r, /**< $comment */ " kind_printers="${kind_printers} case $r: out << \"$r\"; break; " diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index cc8c780a8..3b9c41973 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -136,7 +136,7 @@ ** Regarding the backing store (typically on the stack): the file ** below provides the template: ** - ** template <unsigned nchild_thresh> class NodeBuilder; + ** template < unsigned nchild_thresh > class NodeBuilder; ** ** The default: ** diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index b35f3eafe..9d152a915 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -147,7 +147,6 @@ protected: * Caches the pair of the node and the literal corresponding to the * translation. * @param node the node - * @param lit the literal */ bool hasLiteral(TNode node) const; diff --git a/src/theory/arith/unate_propagator.cpp b/src/theory/arith/unate_propagator.cpp index 38bc06555..6e442ded9 100644 --- a/src/theory/arith/unate_propagator.cpp +++ b/src/theory/arith/unate_propagator.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file arith_propagator.cpp +/*! \file unate_propagator.cpp ** \verbatim ** Original author: taking ** Major contributors: none diff --git a/src/theory/arith/unate_propagator.h b/src/theory/arith/unate_propagator.h index 88020b52b..1aab795cb 100644 --- a/src/theory/arith/unate_propagator.h +++ b/src/theory/arith/unate_propagator.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file arith_propagator.h +/*! \file unate_propagator.h ** \verbatim ** Original author: taking ** Major contributors: none diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h index 4d50eb712..96e367e48 100644 --- a/src/util/congruence_closure.h +++ b/src/util/congruence_closure.h @@ -178,8 +178,8 @@ class CongruenceClosure { CareSet d_careSet; // === STATISTICS === - AverageStat d_explanationLength;/*! average explanation length */ - IntStat d_newSkolemVars;/*! new vars created */ + AverageStat d_explanationLength;/**< average explanation length */ + IntStat d_newSkolemVars;/**< new vars created */ static inline bool isCongruenceOperator(Kind k) { return isInCongruenceOperatorList<CongruenceOperatorList>(k); |