diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/expr_manager_template.h | 2 | ||||
-rw-r--r-- | src/parser/parser.h | 7 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/datatypes/explanation_manager.cpp | 6 | ||||
-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 |
7 files changed, 22 insertions, 15 deletions
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 |