diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-06-04 18:55:22 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-06-04 18:55:22 +0000 |
commit | a460f751e8345e61c4989386765d84bb76fe37d6 (patch) | |
tree | 08bc3c035b5bd8f220853e06dc90fb939c55b2ed /src/parser | |
parent | febba49895125f4f3489e7dff283a000ae9965b3 (diff) |
** 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.
Diffstat (limited to 'src/parser')
28 files changed, 184 insertions, 86 deletions
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 9d75dd31f..fdaa83b04 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -1,5 +1,6 @@ /********************* */ -/** input.cpp +/*! \file antlr_input.cpp + ** \verbatim ** Original author: cconway ** Major contributors: none ** 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 A super-class for ANTLR-generated input language parsers. ** ** A super-class for ANTLR-generated input language parsers **/ diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index 642dc9654..d2d885ce0 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -1,14 +1,17 @@ /********************* */ -/** input.h +/*! \file antlr_input.h + ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): 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. + ** information.\endverbatim + ** + ** \brief Base for ANTLR parser classes. ** ** Base for ANTLR parser classes. **/ diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp index d25d7b66b..b647842fa 100644 --- a/src/parser/antlr_input_imports.cpp +++ b/src/parser/antlr_input_imports.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file antlr_input_imports.cpp + ** \verbatim + ** Original author: cconway + ** 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 + ** + ** rief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + /* * The functions in this file are based on implementations in libantlr3c, * with only minor CVC4-specific changes. diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp index 53b56dcdd..adc0505db 100644 --- a/src/parser/bounded_token_buffer.cpp +++ b/src/parser/bounded_token_buffer.cpp @@ -1,14 +1,17 @@ /********************* */ -/** bounded_token_buffer.h +/*! \file bounded_token_buffer.cpp + ** \verbatim ** Original author: cconway - ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Major contributors: none + ** Minor contributors (to current version): mdeters ** 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. + ** information.\endverbatim + ** + ** \brief An ANTLR3 bounded token stream implementation. ** ** An ANTLR3 bounded token stream implementation. ** This code is largely based on the original token buffer implementation diff --git a/src/parser/bounded_token_buffer.h b/src/parser/bounded_token_buffer.h index 663e5b403..9634f016b 100644 --- a/src/parser/bounded_token_buffer.h +++ b/src/parser/bounded_token_buffer.h @@ -1,14 +1,17 @@ /********************* */ -/** bounded_token_buffer.h +/*! \file bounded_token_buffer.h + ** \verbatim ** Original author: cconway - ** Major contributors: mdeters + ** 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. + ** information.\endverbatim + ** + ** \brief An ANTLR3 bounded token stream. ** ** An ANTLR3 bounded token stream. The stream has a bounded ** lookahead/behind k. Calling LT(i) with i > k or i < -k will raise diff --git a/src/parser/bounded_token_factory.cpp b/src/parser/bounded_token_factory.cpp index c9f9b66e7..5f42f0f29 100644 --- a/src/parser/bounded_token_factory.cpp +++ b/src/parser/bounded_token_factory.cpp @@ -1,14 +1,17 @@ /********************* */ -/** bounded_token_factory.cpp +/*! \file bounded_token_factory.cpp + ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** 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. + ** information.\endverbatim + ** + ** \brief An ANTLR3 bounded token factory implementation. ** ** An ANTLR3 bounded token factory implementation. **/ diff --git a/src/parser/bounded_token_factory.h b/src/parser/bounded_token_factory.h index faf289ef4..4d510c9e3 100644 --- a/src/parser/bounded_token_factory.h +++ b/src/parser/bounded_token_factory.h @@ -1,5 +1,6 @@ /********************* */ -/** bounded_token_factory.h +/*! \file bounded_token_factory.h + ** \verbatim ** Original author: cconway ** Major contributors: mdeters ** 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 An ANTLR3 bounded token factory. ** ** An ANTLR3 bounded token factory. The factory has a fixed number of ** tokens that are re-used as parsing proceeds. Only use this factory diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index a53604efa..0f44e692a 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1,14 +1,17 @@ /* ******************* */ -/* Cvc.g +/*! \file Cvc.g + ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Minor contributors (to current version): dejan, mdeters ** 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. + ** information.\endverbatim + ** + ** \brief Parser for CVC-LIB input language. ** ** Parser for CVC-LIB input language. **/ diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp index 4a8551a7a..2b99f9a87 100644 --- a/src/parser/cvc/cvc_input.cpp +++ b/src/parser/cvc/cvc_input.cpp @@ -1,14 +1,17 @@ /********************* */ -/** cvc_input.cpp +/*! \file cvc_input.cpp + ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** 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. + ** information.\endverbatim + ** + ** \brief [[ Add file-specific comments here ]]. ** ** [[ Add file-specific comments here ]] **/ diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index 82c31813b..64c6beea7 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -1,14 +1,17 @@ /********************* */ -/** cvc_input.h +/*! \file cvc_input.h + ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** 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. + ** information.\endverbatim + ** + ** \brief [[ Add file-specific comments here ]]. ** ** [[ Add file-specific comments here ]] **/ diff --git a/src/parser/input.cpp b/src/parser/input.cpp index a900765b5..2c4671b93 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -1,14 +1,17 @@ /********************* */ -/** input.cpp - ** Original author: cconway - ** Major contributors: none +/*! \file input.cpp + ** \verbatim + ** Original author: dejan + ** Major contributors: mdeters, cconway ** 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. + ** information.\endverbatim + ** + ** \brief A super-class for input language parsers. ** ** A super-class for input language parsers **/ diff --git a/src/parser/input.h b/src/parser/input.h index 926ebe156..ceec1c8bd 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -1,14 +1,17 @@ /********************* */ -/** input.h +/*! \file input.h + ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** 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. + ** information.\endverbatim + ** + ** \brief Base for parser inputs. ** ** Base for parser inputs. **/ diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp index a87ba9cf8..7748a1cca 100644 --- a/src/parser/memory_mapped_input_buffer.cpp +++ b/src/parser/memory_mapped_input_buffer.cpp @@ -1,14 +1,17 @@ /********************* */ -/** memory_mapped_input_buffer.cpp +/*! \file memory_mapped_input_buffer.cpp + ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** 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. + ** information.\endverbatim + ** + ** \brief [[ Add file-specific comments here ]]. ** ** [[ Add file-specific comments here ]] **/ diff --git a/src/parser/memory_mapped_input_buffer.h b/src/parser/memory_mapped_input_buffer.h index c63ec5407..18618a090 100644 --- a/src/parser/memory_mapped_input_buffer.h +++ b/src/parser/memory_mapped_input_buffer.h @@ -1,5 +1,6 @@ /********************* */ -/** memory_mapped_input_buffer.h +/*! \file memory_mapped_input_buffer.h + ** \verbatim ** Original author: cconway ** Major contributors: mdeters ** 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 ANTLR input buffer from a memory-mapped file. ** ** ANTLR input buffer from a memory-mapped file. **/ diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 286867e84..2bad12e2c 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -1,14 +1,17 @@ /********************* */ -/** parser.cpp - ** Original author: cconway - ** Major contributors: dejan, mdeters +/*! \file parser.cpp + ** \verbatim + ** Original author: dejan + ** Major contributors: mdeters, cconway ** 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. + ** information.\endverbatim + ** + ** \brief Parser state implementation. ** ** Parser state implementation. **/ diff --git a/src/parser/parser.h b/src/parser/parser.h index e6e5a2250..3e10f632f 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -1,14 +1,17 @@ /********************* */ -/** parser.h +/*! \file parser.h + ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Minor contributors (to current version): mdeters, 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. + ** information.\endverbatim + ** + ** \brief A collection of state for use by parser implementations. ** ** A collection of state for use by parser implementations. **/ diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 4e4b0309f..3b62cbc57 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -1,5 +1,6 @@ /********************* */ -/** parser_builder.cpp +/*! \file parser_builder.cpp + ** \verbatim ** Original author: cconway ** Major contributors: none ** 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 A builder for parsers. ** ** A builder for parsers. **/ diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 92b44a82d..ed1ab807b 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -1,5 +1,6 @@ /********************* */ -/** parser_builder.h +/*! \file parser_builder.h + ** \verbatim ** Original author: cconway ** Major contributors: none ** 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 A builder for parsers. ** ** A builder for parsers. **/ diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index dfca01ce2..2ae38622d 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -1,5 +1,6 @@ /********************* */ -/** parser_exception.h +/*! \file parser_exception.h + ** \verbatim ** Original author: mdeters ** Major contributors: cconway ** 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 Exception class for parse errors. ** ** Exception class for parse errors. **/ diff --git a/src/parser/parser_options.h b/src/parser/parser_options.h index 51d28e51d..85994c52c 100644 --- a/src/parser/parser_options.h +++ b/src/parser/parser_options.h @@ -1,5 +1,6 @@ /********************* */ -/** parser_options.h +/*! \file parser_options.h + ** \verbatim ** Original author: cconway ** Major contributors: mdeters ** 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 [[ Add file-specific comments here ]]. ** ** [[ Add file-specific comments here ]] **/ diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index c11f350a6..4247dba7a 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -1,14 +1,17 @@ /* ******************* */ -/* Smt.g +/*! \file Smt.g + ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: dejan + ** Minor contributors (to current version): mdeters, taking ** 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. + ** information.\endverbatim + ** + ** \brief Parser for SMT-LIB input language. ** ** Parser for SMT-LIB input language. **/ @@ -60,7 +63,6 @@ namespace CVC4 { @parser::postinclude { #include "expr/expr.h" #include "expr/kind.h" -#include "expr/metakind.h" #include "expr/type.h" #include "parser/antlr_input.h" #include "parser/parser.h" @@ -171,7 +173,7 @@ annotatedFormula[CVC4::Expr& expr] /* Unary AND/OR can be replaced with the argument. It just so happens expr should already by the only argument. */ Assert( expr == args[0] ); - } else if( CVC4::kind::metakind::isAssociative(kind) && + } else if( CVC4::kind::isAssociative(kind) && args.size() > EXPR_MANAGER->maxArity(kind) ) { /* Special treatment for associative operators with lots of children */ expr = EXPR_MANAGER->mkAssociative(kind,args); diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt/smt_input.cpp index 7c8bf19dd..c19eca080 100644 --- a/src/parser/smt/smt_input.cpp +++ b/src/parser/smt/smt_input.cpp @@ -1,14 +1,17 @@ /********************* */ -/** smt_input.cpp +/*! \file smt_input.cpp + ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** 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. + ** information.\endverbatim + ** + ** \brief [[ Add file-specific comments here ]]. ** ** [[ Add file-specific comments here ]] **/ diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h index 1d3f87668..42581ec1c 100644 --- a/src/parser/smt/smt_input.h +++ b/src/parser/smt/smt_input.h @@ -1,5 +1,6 @@ /********************* */ -/** smt_input.h +/*! \file smt_input.h + ** \verbatim ** Original author: cconway ** Major contributors: mdeters ** 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 [[ Add file-specific comments here ]]. ** ** [[ Add file-specific comments here ]] **/ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 11ce111a6..37612901e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1,14 +1,17 @@ /* ******************* */ -/* Smt2.g +/*! \file Smt2.g + ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Minor contributors (to current version): mdeters, taking ** 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. + ** information.\endverbatim + ** + ** \brief Parser for SMT-LIB v2 input language. ** ** Parser for SMT-LIB v2 input language. **/ @@ -74,7 +77,6 @@ namespace CVC4 { @parser::postinclude { #include "expr/expr.h" #include "expr/kind.h" -#include "expr/metakind.h" #include "expr/type.h" #include "parser/antlr_input.h" #include "parser/parser.h" @@ -210,7 +212,7 @@ term[CVC4::Expr& expr] /* Unary AND/OR can be replaced with the argument. It just so happens expr should already by the only argument. */ Assert( expr == args[0] ); - } else if( CVC4::kind::metakind::isAssociative(kind) && + } else if( CVC4::kind::isAssociative(kind) && args.size() > EXPR_MANAGER->maxArity(kind) ) { /* Special treatment for associative operators with lots of children */ expr = EXPR_MANAGER->mkAssociative(kind,args); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 5cf902260..2776bff7e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1,14 +1,17 @@ /********************* */ -/** smt2.h +/*! \file smt2.cpp + ** \verbatim ** Original author: cconway - ** Major contributors: + ** 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. + ** information.\endverbatim + ** + ** \brief Definitions of SMT2 constants. ** ** Definitions of SMT2 constants. **/ diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 0e057db68..b54fe82e9 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -1,14 +1,17 @@ /********************* */ -/** smt2.h +/*! \file smt2.h + ** \verbatim ** Original author: cconway - ** Major contributors: + ** 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. + ** information.\endverbatim + ** + ** \brief Definitions of SMT2 constants. ** ** Definitions of SMT2 constants. **/ diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index 5150ba010..829d6a5f8 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -1,14 +1,17 @@ /********************* */ -/** smt2_input.cpp +/*! \file smt2_input.cpp + ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** 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. + ** information.\endverbatim + ** + ** \brief [[ Add file-specific comments here ]]. ** ** [[ Add file-specific comments here ]] **/ diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index 962e2a987..1fa8cff1c 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -1,14 +1,17 @@ /********************* */ -/** smt2_input.h +/*! \file smt2_input.h + ** \verbatim ** Original author: cconway - ** Major contributors: mdeters + ** 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. + ** information.\endverbatim + ** + ** \brief [[ Add file-specific comments here ]]. ** ** [[ Add file-specific comments here ]] **/ |