diff options
Diffstat (limited to 'src/parser')
41 files changed, 673 insertions, 661 deletions
diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt index 08dafe65c..26472740e 100644 --- a/src/parser/CMakeLists.txt +++ b/src/parser/CMakeLists.txt @@ -1,12 +1,16 @@ -##################### -## CMakeLists.txt -## Top contributors (to current version): -## Mathias Preiner, Aina Niemetz, Andrew Reynolds -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. +############################################################################### +# Top contributors (to current version): +# Mathias Preiner, Gereon Kremer, Aina Niemetz +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# The build system configuration. ## find_package(ANTLR3 3.4 REQUIRED) diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 8a96fec11..7690d8962 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file antlr_input.cpp - ** \verbatim - ** Top contributors (to current version): - ** Christopher L. Conway, Kshitij Bansal, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A super-class for ANTLR-generated input language parsers. - ** - ** A super-class for ANTLR-generated input language parsers - **/ +/****************************************************************************** + * Top contributors (to current version): + * Christopher L. Conway, Kshitij Bansal, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A super-class for ANTLR-generated input language parsers. + */ #include "parser/antlr_input.h" diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index 8f763911c..fea0837e4 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file antlr_input.h - ** \verbatim - ** Top contributors (to current version): - ** Christopher L. Conway, Tim King, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Base for ANTLR parser classes. - ** - ** Base for ANTLR parser classes. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Christopher L. Conway, Tim King, Morgan Deters + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Base for ANTLR parser classes. + */ #ifndef CVC5__PARSER__ANTLR_INPUT_H #define CVC5__PARSER__ANTLR_INPUT_H diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp index bceaa5586..738f4c6e2 100644 --- a/src/parser/antlr_input_imports.cpp +++ b/src/parser/antlr_input_imports.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file antlr_input_imports.cpp - ** \verbatim - ** Top contributors (to current version): - ** Christopher L. Conway, Francois Bobot, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. 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 - **/ +/****************************************************************************** + * Top contributors (to current version): + * Christopher L. Conway, Francois Bobot, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ 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, diff --git a/src/parser/antlr_line_buffered_input.cpp b/src/parser/antlr_line_buffered_input.cpp index bd4c910f9..0657f6c7e 100644 --- a/src/parser/antlr_line_buffered_input.cpp +++ b/src/parser/antlr_line_buffered_input.cpp @@ -1,32 +1,31 @@ -/********************* */ -/*! \file antlr_line_buffered_input.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A custom ANTLR input stream that reads from the input stream lazily - ** - ** WARNING: edits to this and related files should be done carefully due to the - *interaction with ANTLR internals. - ** - ** This overwrites the _LA and the consume functions of the ANTLR input stream - ** to use a LineBuffer instead of accessing a buffer. The lines are kept in - ** memory to make sure that existing tokens remain valid (tokens store pointers - ** to the corresponding input). We do not overwrite mark(), etc. - *because - ** we can use the line number and the position within that line to index into - *the - ** line buffer and the default markers already store and restore that - ** information. The line buffer guarantees that lines are consecutive in - ** memory, so ANTLR3_INPUT_STREAM::getLineBuf() should work as intended and - ** tokens themselves are consecutive in memory (we are assuming that tokens - ** are not split across multiple lines). - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Andres Noetzli, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A custom ANTLR input stream that reads from the input stream lazily + * + * WARNING: Edits to this and related files should be done carefully due to the + * interaction with ANTLR internals. + * + * This overwrites the _LA and the consume functions of the ANTLR input stream + * to use a LineBuffer instead of accessing a buffer. The lines are kept in + * memory to make sure that existing tokens remain valid (tokens store pointers + * to the corresponding input). We do not overwrite mark(), etc. because + * we can use the line number and the position within that line to index into + * the line buffer and the default markers already store and restore that + * information. The line buffer guarantees that lines are consecutive in + * memory, so ANTLR3_INPUT_STREAM::getLineBuf() should work as intended and + * tokens themselves are consecutive in memory (we are assuming that tokens + * are not split across multiple lines). + */ #include "parser/antlr_line_buffered_input.h" diff --git a/src/parser/antlr_line_buffered_input.h b/src/parser/antlr_line_buffered_input.h index ca6831e5e..faf9d16da 100644 --- a/src/parser/antlr_line_buffered_input.h +++ b/src/parser/antlr_line_buffered_input.h @@ -1,24 +1,25 @@ -/********************* */ -/*! \file antlr_line_buffered_input.h - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, Morgan Deters, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A custom ANTLR input stream that reads from the input stream lazily - ** - ** By default, ANTLR expects the whole input to be in a single, consecutive - ** buffer. When doing incremental solving and the input is coming from the - ** standard input, this is problematic because CVC4 might receive new input - ** based on the result of solving the existing input. - ** - ** This file overwrites the _LA and the consume functions of the input streamto - ** achieve that and stores the lines received so far in a LineBuffer. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, Morgan Deters, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A custom ANTLR input stream that reads from the input stream lazily + * + * By default, ANTLR expects the whole input to be in a single, consecutive + * buffer. When doing incremental solving and the input is coming from the + * standard input, this is problematic because CVC4 might receive new input + * based on the result of solving the existing input. + * + * This file overwrites the _LA and the consume functions of the input streamto + * achieve that and stores the lines received so far in a LineBuffer. + */ #include "cvc4parser_private.h" diff --git a/src/parser/antlr_tracing.h b/src/parser/antlr_tracing.h index e001512e6..cd1066383 100644 --- a/src/parser/antlr_tracing.h +++ b/src/parser/antlr_tracing.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file antlr_tracing.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Mathias Preiner, Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. 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 - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Mathias Preiner, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #ifndef CVC5__PARSER__ANTLR_TRACING_H #define CVC5__PARSER__ANTLR_TRACING_H diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp index af4ee4d41..3e1d4f625 100644 --- a/src/parser/bounded_token_buffer.cpp +++ b/src/parser/bounded_token_buffer.cpp @@ -1,20 +1,20 @@ -/********************* */ -/*! \file bounded_token_buffer.cpp - ** \verbatim - ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing 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 - ** in libantlr3c, by Jim Idle. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Christopher L. Conway, Tim King, Morgan Deters + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * An ANTLR3 bounded token stream implementation. + * + * This code is largely based on the original token buffer implementation + * in libantlr3c, by Jim Idle. + */ /// \file /// Default implementation of CommonTokenStream diff --git a/src/parser/bounded_token_buffer.h b/src/parser/bounded_token_buffer.h index 48db57df5..f190e82cf 100644 --- a/src/parser/bounded_token_buffer.h +++ b/src/parser/bounded_token_buffer.h @@ -1,27 +1,27 @@ -/********************* */ -/*! \file bounded_token_buffer.h - ** \verbatim - ** Top contributors (to current version): - ** Christopher L. Conway, Mathias Preiner, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing 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 - ** an exception. Only use this factory if you *know* that the grammar - ** has bounded lookahead (e.g., if you've set the k parameter in the - ** parser. - ** - ** NOTE: ANTLR3 puts "hidden" tokens into this buffer too, so - ** pathological inputs can exceed the k token lookahead, even if - ** your grammar really is LL(k). Be sure that irrelevant tokens - ** are SKIP()'d and not "hidden". - **/ +/****************************************************************************** + * Top contributors (to current version): + * Christopher L. Conway, Mathias Preiner, Morgan Deters + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * An ANTLR3 bounded token stream. + * + * The stream has a bounded lookahead/behind k. Calling LT(i) with i > k or + * i < k will raise an exception. Only use this factory if you *know* that the + * grammar has bounded lookahead (e.g., if you've set the k parameter in the + * parser. + * + * NOTE: ANTLR3 puts "hidden" tokens into this buffer too, so pathological + * inputs can exceed the k token lookahead, even if your grammar really + * is LL(k). Be sure that irrelevant tokens are SKIP()'d and not + * "hidden". + */ #include "cvc4parser_private.h" diff --git a/src/parser/bounded_token_factory.cpp b/src/parser/bounded_token_factory.cpp index aceff0de4..432bb04ef 100644 --- a/src/parser/bounded_token_factory.cpp +++ b/src/parser/bounded_token_factory.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file bounded_token_factory.cpp - ** \verbatim - ** Top contributors (to current version): - ** Christopher L. Conway - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief An ANTLR3 bounded token factory implementation. - ** - ** An ANTLR3 bounded token factory implementation. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Christopher L. Conway + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * An ANTLR3 bounded token factory implementation. + */ #include <antlr3input.h> #include <antlr3commontoken.h> diff --git a/src/parser/bounded_token_factory.h b/src/parser/bounded_token_factory.h index 1de4fee5d..9211ef47c 100644 --- a/src/parser/bounded_token_factory.h +++ b/src/parser/bounded_token_factory.h @@ -1,21 +1,20 @@ -/********************* */ -/*! \file bounded_token_factory.h - ** \verbatim - ** Top contributors (to current version): - ** Christopher L. Conway, Mathias Preiner, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing 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 - ** if you *know* that the number of active tokens will be bounded - ** (e.g., if you're using a bounded token stream). - **/ +/****************************************************************************** + * Top contributors (to current version): + * Christopher L. Conway, Mathias Preiner, Morgan Deters + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * An ANTLR3 bounded token factory. + * + * The factory has a fixed number of tokens that are re-used as parsing + * proceeds. Only use this factory if you *know* that the number of active + * tokens will be bounded (e.g., if you're using a bounded token stream). + */ #include "cvc4parser_private.h" diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 7b036fff4..f78426eda 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1,18 +1,17 @@ -/* ******************* */ -/*! \file Cvc.g - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Christopher L. Conway - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Parser for CVC presentation input language - ** - ** Parser for CVC presentation input language. - **/ +/* **************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Andrew Reynolds, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Parser for CVC presentation input language. + */ grammar Cvc; @@ -509,13 +508,15 @@ api::Term addNots(api::Solver* s, size_t n, api::Term e) { }/* @parser::members */ @header { -/** - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information. - **/ +/* **************************************************************************** + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + */ }/* @header */ @lexer::includes { diff --git a/src/parser/cvc/cvc.cpp b/src/parser/cvc/cvc.cpp index a115fa276..0f87e42cd 100644 --- a/src/parser/cvc/cvc.cpp +++ b/src/parser/cvc/cvc.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file cvc.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The parser class for the CVC language. - ** - ** The parser class for the CVC language. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The parser class for the CVC language. + */ #include "parser/cvc/cvc.h" #include "smt/command.h" diff --git a/src/parser/cvc/cvc.h b/src/parser/cvc/cvc.h index bfd9fdcfc..d9866603c 100644 --- a/src/parser/cvc/cvc.h +++ b/src/parser/cvc/cvc.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file cvc.h - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The parser class for the CVC language. - ** - ** The parser class for the CVC language. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The parser class for the CVC language. + */ #include "cvc4parser_private.h" diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp index f746c5f05..1592e06fb 100644 --- a/src/parser/cvc/cvc_input.cpp +++ b/src/parser/cvc/cvc_input.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file cvc_input.cpp - ** \verbatim - ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add file-specific comments here ]]. - ** - ** [[ Add file-specific comments here ]] - **/ +/****************************************************************************** + * Top contributors (to current version): + * Christopher L. Conway, Morgan Deters, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + */ #include "parser/cvc/cvc_input.h" diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index e7b8640e4..30991ea2b 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -1,18 +1,19 @@ -/********************* */ -/*! \file cvc_input.h - ** \verbatim - ** Top contributors (to current version): - ** Christopher L. Conway, Mathias Preiner, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add file-specific comments here ]]. - ** - ** [[ Add file-specific comments here ]] - **/ +/****************************************************************************** + * Top contributors (to current version): + * Christopher L. Conway, Mathias Preiner, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + */ #include "cvc4parser_private.h" diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 8c9519022..cfb418fbe 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file input.cpp - ** \verbatim - ** Top contributors (to current version): - ** Christopher L. Conway, Tim King, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A super-class for input language parsers. - ** - ** A super-class for input language parsers - **/ +/****************************************************************************** + * Top contributors (to current version): + * Christopher L. Conway, Tim King, Morgan Deters + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A super-class for input language parsers + */ // This must be included first. #include "parser/antlr_input.h" diff --git a/src/parser/input.h b/src/parser/input.h index a4b537821..b4128b5c2 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file input.h - ** \verbatim - ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Base for parser inputs. - ** - ** Base for parser inputs. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Christopher L. Conway, Morgan Deters, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Base for parser inputs. + */ #include "cvc4parser_public.h" diff --git a/src/parser/line_buffer.cpp b/src/parser/line_buffer.cpp index 694478d38..f8c31bc54 100644 --- a/src/parser/line_buffer.cpp +++ b/src/parser/line_buffer.cpp @@ -1,18 +1,22 @@ -/********************* */ -/*! \file line_buffer.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, Mathias Preiner, Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The LineBuffer class stores lines from an input stream - ** - ** For each line, the class allocates a separate buffer. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, Mathias Preiner, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The LineBuffer class stores lines from an input stream + * + * Each line is guaranteed to be consecutive in memory. The content in + * the line buffer can be addressed using line number and the position + * + * For each line, the class allocates a separate buffer. + */ #include "parser/line_buffer.h" diff --git a/src/parser/line_buffer.h b/src/parser/line_buffer.h index 10a9e06ac..15ce9a8a1 100644 --- a/src/parser/line_buffer.h +++ b/src/parser/line_buffer.h @@ -1,20 +1,21 @@ -/********************* */ -/*! \file line_buffer.h - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The LineBuffer class stores lines from an input stream - ** - ** Each line is guaranteed to be consecutive in memory. The content in - ** the line buffer can be addressed using line number and the position - ** within the line. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The LineBuffer class stores lines from an input stream + * + * Each line is guaranteed to be consecutive in memory. The content in + * the line buffer can be addressed using line number and the position + * within the line. + */ #include "cvc4parser_private.h" diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp index b1f1b8924..44e85bc90 100644 --- a/src/parser/memory_mapped_input_buffer.cpp +++ b/src/parser/memory_mapped_input_buffer.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file memory_mapped_input_buffer.cpp - ** \verbatim - ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add file-specific comments here ]]. - ** - ** [[ Add file-specific comments here ]] - **/ +/****************************************************************************** + * Top contributors (to current version): + * Christopher L. Conway, Morgan Deters, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add file-specific comments here ]]. + * + * [[ Add file-specific comments here ]] + */ #include <fcntl.h> #include <stdio.h> diff --git a/src/parser/memory_mapped_input_buffer.h b/src/parser/memory_mapped_input_buffer.h index 69f229796..9db4c3d49 100644 --- a/src/parser/memory_mapped_input_buffer.h +++ b/src/parser/memory_mapped_input_buffer.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file memory_mapped_input_buffer.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Mathias Preiner, Christopher L. Conway - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief ANTLR input buffer from a memory-mapped file. - ** - ** ANTLR input buffer from a memory-mapped file. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Mathias Preiner, Christopher L. Conway + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * ANTLR input buffer from a memory-mapped file. + */ #include "cvc4parser_private.h" diff --git a/src/parser/parse_op.cpp b/src/parser/parse_op.cpp index 0d024da61..3f7df3794 100644 --- a/src/parser/parse_op.cpp +++ b/src/parser/parse_op.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file parse_op.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implementation for parsed operators - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation for parsed operators. + */ #include "parser/parse_op.h" diff --git a/src/parser/parse_op.h b/src/parser/parse_op.h index f862c178d..aed05769a 100644 --- a/src/parser/parse_op.h +++ b/src/parser/parse_op.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file parse_op.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Definitions of parsed operators. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Definitions of parsed operators. + */ #include "cvc4parser_public.h" diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index b4e4639ba..84c1e66f3 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file parser.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Christopher L. Conway - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Parser state implementation. - ** - ** Parser state implementation. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Morgan Deters, Christopher L. Conway + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Parser state implementation. + */ #include "parser/parser.h" diff --git a/src/parser/parser.h b/src/parser/parser.h index 210e53ccf..6f7c5f569 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file parser.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Christopher L. Conway - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A collection of state for use by parser implementations. - ** - ** A collection of state for use by parser implementations. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Morgan Deters, Christopher L. Conway + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A collection of state for use by parser implementations. + */ #include "cvc4parser_public.h" diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 933be7a51..ad3b69f7e 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file parser_builder.cpp - ** \verbatim - ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A builder for parsers. - ** - ** A builder for parsers. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Christopher L. Conway, Morgan Deters, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A builder for parsers. + */ // This must be included first. #include "parser/parser_builder.h" diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index db2cc0a7e..521628262 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file parser_builder.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Christopher L. Conway, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A builder for parsers. - ** - ** A builder for parsers. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Christopher L. Conway, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A builder for parsers. + */ #include "cvc4parser_public.h" diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index a2f614dc7..70e3edda3 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file parser_exception.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Morgan Deters, Christopher L. Conway - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Exception class for parse errors. - ** - ** Exception class for parse errors. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Morgan Deters, Christopher L. Conway + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Exception class for parse errors. + */ #include "cvc4parser_public.h" diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 66800ff53..16eba8fb3 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1,18 +1,17 @@ -/* ******************* */ -/*! \file Smt2.g - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Christopher L. Conway - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Parser for SMT-LIB v2 input language - ** - ** Parser for SMT-LIB v2 input language. - **/ +/* **************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Morgan Deters, Christopher L. Conway + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Parser for SMT-LIB v2 input language. + */ grammar Smt2; @@ -30,13 +29,15 @@ options { }/* options */ @header { -/** - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information. - **/ +/* **************************************************************************** + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + */ }/* @header */ @lexer::includes { diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index c35582550..19b343a66 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file smt2.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Andres Noetzli, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Definitions of SMT2 constants. - ** - ** Definitions of SMT2 constants. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Andres Noetzli, Morgan Deters + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Definitions of SMT2 constants. + */ #include "parser/smt2/smt2.h" #include <algorithm> diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 8ac1c14cc..166ddeb2d 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file smt2.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Andres Noetzli, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Definitions of SMT2 constants. - ** - ** Definitions of SMT2 constants. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Andres Noetzli, Morgan Deters + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Definitions of SMT2 constants. + */ #include "cvc4parser_private.h" diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index 650d97299..90b2087fa 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file smt2_input.cpp - ** \verbatim - ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add file-specific comments here ]]. - ** - ** [[ Add file-specific comments here ]] - **/ +/****************************************************************************** + * Top contributors (to current version): + * Christopher L. Conway, Andrew Reynolds, Morgan Deters + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add file-specific comments here ]] + */ #include "parser/smt2/smt2_input.h" diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index 78b2cf051..1668e101f 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -1,18 +1,19 @@ -/********************* */ -/*! \file smt2_input.h - ** \verbatim - ** Top contributors (to current version): - ** Christopher L. Conway, Mathias Preiner, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add file-specific comments here ]]. - ** - ** [[ Add file-specific comments here ]] - **/ +/****************************************************************************** + * Top contributors (to current version): + * Christopher L. Conway, Mathias Preiner, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add file-specific comments here ]] + */ #include "cvc4parser_private.h" diff --git a/src/parser/smt2/sygus_input.cpp b/src/parser/smt2/sygus_input.cpp index cc605b842..85288b647 100644 --- a/src/parser/smt2/sygus_input.cpp +++ b/src/parser/smt2/sygus_input.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file sygus_input.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add file-specific comments here ]]. - ** - ** [[ Add file-specific comments here ]] - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Andrew Reynolds, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add file-specific comments here ]] + */ #include "parser/smt2/sygus_input.h" diff --git a/src/parser/smt2/sygus_input.h b/src/parser/smt2/sygus_input.h index 96b3f1eed..93e40253d 100644 --- a/src/parser/smt2/sygus_input.h +++ b/src/parser/smt2/sygus_input.h @@ -1,18 +1,19 @@ -/********************* */ -/*! \file sygus_input.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Mathias Preiner, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add file-specific comments here ]]. - ** - ** [[ Add file-specific comments here ]] - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Mathias Preiner, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add file-specific comments here ]] + */ #include "cvc4parser_private.h" diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 0f21cdb20..3932b8f7d 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -1,19 +1,19 @@ -/* ******************* */ -/*! \file Tptp.g - ** \verbatim - ** Top contributors (to current version): - ** Haniel Barbosa, Francois Bobot, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Parser for TPTP input language. - ** - ** Parser for TPTP input language. - ** cf. http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Documents&File=SyntaxBNF - **/ +/* **************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa, Francois Bobot, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Parser for TPTP input language. + * + * cf. http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Documents&File=SyntaxBNF + */ grammar Tptp; @@ -31,13 +31,15 @@ options { }/* options */ @header { -/** - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information. - **/ +/* **************************************************************************** + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + */ }/* @header */ @lexer::includes { diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 0283554bc..01b4c1165 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file tptp.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Francois Bobot, Haniel Barbosa - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Definition of TPTP parser. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Francois Bobot, Haniel Barbosa + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Definition of TPTP parser. + */ // Do not #include "parser/antlr_input.h" directly. Rely on the header. #include "parser/tptp/tptp.h" diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 41203a809..65b2240af 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file tptp.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Francois Bobot, Haniel Barbosa - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Definition of TPTP parser - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Francois Bobot, Haniel Barbosa + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Definition of TPTP parser. + */ #include "parser/antlr_input.h" // Needs to go first. diff --git a/src/parser/tptp/tptp_input.cpp b/src/parser/tptp/tptp_input.cpp index 9e2943c47..3bf6ad958 100644 --- a/src/parser/tptp/tptp_input.cpp +++ b/src/parser/tptp/tptp_input.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file tptp_input.cpp - ** \verbatim - ** Top contributors (to current version): - ** Francois Bobot, Morgan Deters, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add file-specific comments here ]]. - ** - ** [[ Add file-specific comments here ]] - **/ +/****************************************************************************** + * Top contributors (to current version): + * Francois Bobot, Morgan Deters, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add file-specific comments here ]] + */ #include "parser/tptp/tptp_input.h" diff --git a/src/parser/tptp/tptp_input.h b/src/parser/tptp/tptp_input.h index a4d33b3cb..b9a8e2d0f 100644 --- a/src/parser/tptp/tptp_input.h +++ b/src/parser/tptp/tptp_input.h @@ -1,18 +1,19 @@ -/********************* */ -/*! \file tptp_input.h - ** \verbatim - ** Top contributors (to current version): - ** Francois Bobot, Mathias Preiner, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add file-specific comments here ]]. - ** - ** [[ Add file-specific comments here ]] - **/ +/****************************************************************************** + * Top contributors (to current version): + * Francois Bobot, Mathias Preiner, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add file-specific comments here ]] + */ #include "cvc4parser_private.h" |