From a460f751e8345e61c4989386765d84bb76fe37d6 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 4 Jun 2010 18:55:22 +0000 Subject: ** Don't fear the files-changed list, almost all changes are in the ** ** file-level documentation at the top of the sources. ** This is the "make bugzilla stop bugging me" bugfix commit. * Remove BackedNodeBuilder<> and collapse NodeBuilder<> hierarchy. Updated documentation in the file. Resolves bug #99. * Convenience NodeBuilders (PlusNodeBuilder, OrNodeBuilder, etc.) moved into a separate file. Partially resolves bug #100. * Moved isAssociative(Kind) into kind.h (and into the CVC4::kind namespace) instead of metakind.h (where it was in CVC4::metakind). This clears up a warning (private #inclusion) from the SMT and SMT2 parsers, and maybe makes more sense anyways, since this is based on the kind (and not the metakind) of an operator. * Documentation improvement; doxygen top-level \file gestures, \brief gestures for files, etc. Changed contrib/update-copyright.pl for this change, and post-processed to add \brief. Resolves bug #98. * Removed ExprManager::mkExpr(Kind) and NodeManager::mkNode(Kind). They no longer made sense. Resolves bug #91. --- src/theory/arith/arith_constants.h | 19 +++++++++++++++++++ src/theory/arith/arith_rewriter.cpp | 19 +++++++++++++++++++ src/theory/arith/arith_rewriter.h | 19 +++++++++++++++++++ src/theory/arith/arith_utilities.h | 21 ++++++++++++++++++--- src/theory/arith/basic.h | 19 +++++++++++++++++++ src/theory/arith/delta_rational.cpp | 19 +++++++++++++++++++ src/theory/arith/delta_rational.h | 19 +++++++++++++++++++ src/theory/arith/normal.h | 19 +++++++++++++++++++ src/theory/arith/partial_model.cpp | 19 +++++++++++++++++++ src/theory/arith/partial_model.h | 19 +++++++++++++++++++ src/theory/arith/slack.h | 19 +++++++++++++++++++ src/theory/arith/tableau.h | 19 +++++++++++++++++++ src/theory/arith/theory_arith.cpp | 19 +++++++++++++++++++ src/theory/arith/theory_arith.h | 7 +++++-- src/theory/arith/theory_arith_type_rules.h | 9 +++++++-- 15 files changed, 258 insertions(+), 7 deletions(-) (limited to 'src/theory/arith') diff --git a/src/theory/arith/arith_constants.h b/src/theory/arith/arith_constants.h index 775db3ae0..c34e86191 100644 --- a/src/theory/arith/arith_constants.h +++ b/src/theory/arith/arith_constants.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file arith_constants.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "expr/node.h" diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 312e1c6ea..19980cd20 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file arith_rewriter.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "theory/arith/arith_rewriter.h" #include "theory/arith/arith_utilities.h" diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 6388c7031..704b57ca6 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file arith_rewriter.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "expr/node.h" #include "util/rational.h" diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 297def3c7..dcfedb7e8 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -1,10 +1,25 @@ - - +/********************* */ +/*! \file arith_utilities.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ #ifndef __CVC4__THEORY__ARITH__ARITH_UTILITIES_H #define __CVC4__THEORY__ARITH__ARITH_UTILITIES_H - #include "util/rational.h" #include "expr/node.h" diff --git a/src/theory/arith/basic.h b/src/theory/arith/basic.h index 0f1cb07dc..963f2b969 100644 --- a/src/theory/arith/basic.h +++ b/src/theory/arith/basic.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file basic.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "expr/node.h" #include "expr/attribute.h" diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp index 0c94b1d08..55e6b3dc9 100644 --- a/src/theory/arith/delta_rational.cpp +++ b/src/theory/arith/delta_rational.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file delta_rational.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "theory/arith/delta_rational.h" diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index 4b6e06bc5..c37c65241 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file delta_rational.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "cvc4_private.h" #include "util/integer.h" diff --git a/src/theory/arith/normal.h b/src/theory/arith/normal.h index 0dbd7355a..12b2a5e71 100644 --- a/src/theory/arith/normal.h +++ b/src/theory/arith/normal.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file normal.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #ifndef __CVC4__THEORY__ARITH__NORMAL_H #define __CVC4__THEORY__ARITH__NORMAL_H diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index 33c690276..2d65f0640 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file partial_model.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "theory/arith/partial_model.h" #include "util/output.h" diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index 57996a510..36567e86e 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file partial_model.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "context/context.h" #include "context/cdmap.h" diff --git a/src/theory/arith/slack.h b/src/theory/arith/slack.h index 37595fda5..5cf391e64 100644 --- a/src/theory/arith/slack.h +++ b/src/theory/arith/slack.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file slack.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + namespace CVC4 { namespace theory { diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 76d8aa4f3..e43b48c66 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file tableau.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "expr/node.h" #include "expr/attribute.h" diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 3ca3245dd..e99a3e823 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file theory_arith.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): dejan + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "expr/node.h" #include "expr/kind.h" #include "expr/metakind.h" diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index ade63b6c9..c6b555bf8 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -1,5 +1,6 @@ /********************* */ -/** theory_arith.h +/*! \file theory_arith.h + ** \verbatim ** Original author: mdeters ** Major contributors: taking ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Arithmetic theory. ** ** Arithmetic theory. **/ diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index b21ed0d6f..a995f90af 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -1,5 +1,6 @@ /********************* */ -/** theory_arith_type_rules.cpp +/*! \file theory_arith_type_rules.cpp + ** \verbatim ** Original author: dejan ** Major contributors: none ** This file is part of the CVC4 prototype. @@ -7,7 +8,11 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief [[ Add brief comments here ]] + ** + ** [[ Add file-specific comments here ]] **/ #include "cvc4_private.h" -- cgit v1.2.3