diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-12 12:31:43 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-12 19:31:43 +0000 |
commit | 7ec30058750611786b1b597816c8a23e28bb5812 (patch) | |
tree | e59b1de0078dc04d3a9c212cf9e6ebfd70cbb7f4 /src/smt | |
parent | 7361b587e9a1b717dfa906d02f66feb6896e80dd (diff) |
Refactor and update copyright headers. (#6316)
Diffstat (limited to 'src/smt')
77 files changed, 1106 insertions, 1058 deletions
diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp index 804a93401..7e29e4849 100644 --- a/src/smt/abduction_solver.cpp +++ b/src/smt/abduction_solver.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file abduction_solver.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 The solver for abduction queries - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * The solver for abduction queries. + */ #include "smt/abduction_solver.h" diff --git a/src/smt/abduction_solver.h b/src/smt/abduction_solver.h index eee6f52cd..e8a97c043 100644 --- a/src/smt/abduction_solver.h +++ b/src/smt/abduction_solver.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file abduction_solver.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Aina Niemetz, 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 The solver for abduction queries - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Aina Niemetz, 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. + * **************************************************************************** + * + * The solver for abduction queries. + */ #include "cvc4_private.h" diff --git a/src/smt/abstract_values.cpp b/src/smt/abstract_values.cpp index fc978d39b..81c7af16b 100644 --- a/src/smt/abstract_values.cpp +++ b/src/smt/abstract_values.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file abstract_values.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Utility for constructing and maintaining abstract values. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Utility for constructing and maintaining abstract values. + */ #include "smt/abstract_values.h" diff --git a/src/smt/abstract_values.h b/src/smt/abstract_values.h index 125be2511..843adbb22 100644 --- a/src/smt/abstract_values.h +++ b/src/smt/abstract_values.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file abstract_values.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Utility for constructing and maintaining abstract values. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Utility for constructing and maintaining abstract values. + */ #include "cvc4_private.h" diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index bfb14e2c4..d873f31bb 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file assertions.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Andres Noetzli, 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 The module for storing assertions for an SMT engine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Andres Noetzli, 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. + * **************************************************************************** + * + * The module for storing assertions for an SMT engine. + */ #include "smt/assertions.h" diff --git a/src/smt/assertions.h b/src/smt/assertions.h index 157d063f4..3603c0df6 100644 --- a/src/smt/assertions.h +++ b/src/smt/assertions.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file assertions.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, 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 module for storing assertions for an SMT engine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Morgan Deters, 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 module for storing assertions for an SMT engine. + */ #include "cvc4_private.h" diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index b84bc3e64..ebc8f46a1 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file check_models.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, 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 Utility for constructing and maintaining abstract values. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Morgan Deters, 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. + * **************************************************************************** + * + * Utility for constructing and maintaining abstract values. + */ #include "smt/check_models.h" diff --git a/src/smt/check_models.h b/src/smt/check_models.h index 997857515..f2c7b50ba 100644 --- a/src/smt/check_models.h +++ b/src/smt/check_models.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file check_models.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer - ** 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 Utility for checking models - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * Utility for checking models. + */ #include "cvc4_private.h" diff --git a/src/smt/command.cpp b/src/smt/command.cpp index a8d9afdfa..5585ab48f 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file command.cpp - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Abdalrhman Mohamed, 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 Implementation of command objects. - ** - ** Implementation of command objects. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Abdalrhman Mohamed, 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. + * **************************************************************************** + * + * Implementation of command objects. + */ #include "smt/command.h" diff --git a/src/smt/command.h b/src/smt/command.h index d28c0975d..9ef09abec 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1,21 +1,21 @@ -/********************* */ -/*! \file command.h - ** \verbatim - ** Top contributors (to current version): - ** Abdalrhman Mohamed, 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 Implementation of the command pattern on SmtEngines. - ** - ** Implementation of the command pattern on SmtEngines. Command - ** objects are generated by the parser (typically) to implement the - ** commands in parsed input (see Parser::parseNextCommand()), or by - ** client code. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Abdalrhman Mohamed, Tim King, 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 of the command pattern on SmtEngines. + * + * Command objects are generated by the parser (typically) to implement the + * commands in parsed input (see Parser::parseNextCommand()), or by client + * code. + */ #include "cvc4_public.h" diff --git a/src/smt/defined_function.h b/src/smt/defined_function.h index 6ad0b73c7..ab225b095 100644 --- a/src/smt/defined_function.h +++ b/src/smt/defined_function.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file defined_function.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Defined function data structure - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Defined function data structure. + */ #include "cvc4_private.h" diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp index 73f26dc92..f5ebd3c5b 100644 --- a/src/smt/dump.cpp +++ b/src/smt/dump.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file dump.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, 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 Dump utility classes and functions - ** - ** Dump utility classes and functions. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, 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. + * **************************************************************************** + * + * Dump utility classes and functions. + */ #include "smt/dump.h" diff --git a/src/smt/dump.h b/src/smt/dump.h index 6e14fc59f..a56529fe3 100644 --- a/src/smt/dump.h +++ b/src/smt/dump.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file dump.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli, Abdalrhman Mohamed - ** 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 Dump utility classes and functions - ** - ** Dump utility classes and functions. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Andres Noetzli, Abdalrhman Mohamed + * + * 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. + * **************************************************************************** + * + * Dump utility classes and functions. + */ #include "cvc4_private.h" diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp index 4b7f0b056..83ff8e6b9 100644 --- a/src/smt/dump_manager.cpp +++ b/src/smt/dump_manager.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file dump_manager.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer, 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 Implementation of the dump manager. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer, 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. + * **************************************************************************** + * + * Implementation of the dump manager. + */ #include "smt/dump_manager.h" diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h index 2b1644bef..de9a8ba2e 100644 --- a/src/smt/dump_manager.h +++ b/src/smt/dump_manager.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file dump_manager.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Gereon Kremer - ** 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 dump manager of the SmtEngine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Morgan Deters, Gereon Kremer + * + * 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 dump manager of the SmtEngine. + */ #include "cvc4_private.h" diff --git a/src/smt/env.cpp b/src/smt/env.cpp index e88710628..38e93f38e 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -1,17 +1,18 @@ -/********************* */ -/*! \file env.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 Smt Environment, main access to global utilities available to - ** internal code. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Smt Environment, main access to global utilities available to + * internal code. + */ #include "smt/env.h" diff --git a/src/smt/env.h b/src/smt/env.h index c22044338..d13cd7a71 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -1,17 +1,18 @@ -/********************* */ -/*! \file env.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 Smt Environment, main access to global utilities available to - ** internal code - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Smt Environment, main access to global utilities available to + * internal code + */ #include "cvc4_public.h" diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp index 59597b97f..0c5cf6ad5 100644 --- a/src/smt/expand_definitions.cpp +++ b/src/smt/expand_definitions.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file expand_definitions.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, 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 Implementation of expand definitions for an SMT engine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Andres Noetzli, 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. + * **************************************************************************** + * + * Implementation of expand definitions for an SMT engine. + */ #include "smt/expand_definitions.h" diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h index a3d70542b..7a05d6a3a 100644 --- a/src/smt/expand_definitions.h +++ b/src/smt/expand_definitions.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file expand_definitions.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer - ** 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 module for processing assertions for an SMT engine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer + * + * 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 module for processing assertions for an SMT engine. + */ #include "cvc4_private.h" diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index 7b75ea2ed..48d81a91f 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file interpolation_solver.cpp - ** \verbatim - ** Top contributors (to current version): - ** Ying Sheng, Andrew Reynolds, Abdalrhman Mohamed - ** 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 solver for interpolation queries - **/ +/****************************************************************************** + * Top contributors (to current version): + * Ying Sheng, 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. + * **************************************************************************** + * + * The solver for interpolation queries. + */ #include "smt/interpolation_solver.h" diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h index 62f469970..e5480e6dc 100644 --- a/src/smt/interpolation_solver.h +++ b/src/smt/interpolation_solver.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file interpolation_solver.h - ** \verbatim - ** Top contributors (to current version): - ** Ying Sheng, Andrew Reynolds, 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 The solver for interpolation queries - **/ +/****************************************************************************** + * Top contributors (to current version): + * Ying Sheng, 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. + * **************************************************************************** + * + * The solver for interpolation queries. + */ #include "cvc4_private.h" diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp index e7ea9bb40..a3c271fc5 100644 --- a/src/smt/listeners.cpp +++ b/src/smt/listeners.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file listeners.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Abdalrhman Mohamed - ** 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 Implements listener classes for SMT engine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Abdalrhman Mohamed + * + * 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. + * **************************************************************************** + * + * Implements listener classes for SMT engine. + */ #include "smt/listeners.h" diff --git a/src/smt/listeners.h b/src/smt/listeners.h index 2ca8b8ad8..afc81c047 100644 --- a/src/smt/listeners.h +++ b/src/smt/listeners.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file listeners.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Abdalrhman Mohamed, 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 Listener classes for SMT engine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Abdalrhman Mohamed, 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. + * **************************************************************************** + * + * Listener classes for SMT engine. + */ #include "cvc4_private.h" diff --git a/src/smt/logic_exception.h b/src/smt/logic_exception.h index e9f747313..df08b5734 100644 --- a/src/smt/logic_exception.h +++ b/src/smt/logic_exception.h @@ -1,21 +1,19 @@ -/********************* */ -/*! \file logic_exception.h - ** \verbatim - ** Top contributors (to current version): - ** 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 An exception that is thrown when a feature is used outside - ** the logic that CVC4 is currently using - ** - ** \brief An exception that is thrown when a feature is used outside - ** the logic that CVC4 is currently using (for example, a quantifier - ** is used while running in a quantifier-free logic). - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * An exception that is thrown when a feature is used outside + * the logic that CVC4 is currently using (for example, a quantifier + * is used while running in a quantifier-free logic). + */ #include "cvc4_public.h" diff --git a/src/smt/managed_ostreams.cpp b/src/smt/managed_ostreams.cpp index 6962ef495..b0f9aef21 100644 --- a/src/smt/managed_ostreams.cpp +++ b/src/smt/managed_ostreams.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file managed_ostreams.cpp - ** \verbatim - ** Top contributors (to current version): - ** Tim King, 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 Wrappers to handle memory management of ostreams. - ** - ** This file contains wrappers to handle special cases of managing memory - ** related to ostreams. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, 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. + * **************************************************************************** + * + * Wrappers to handle memory management of ostreams. + * + * This file contains wrappers to handle special cases of managing memory + * related to ostreams. + */ #include "smt/managed_ostreams.h" diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h index 9737979ea..d519fc826 100644 --- a/src/smt/managed_ostreams.h +++ b/src/smt/managed_ostreams.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file managed_ostreams.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Mathias Preiner, Gereon Kremer - ** 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 Wrappers to handle memory management of ostreams. - ** - ** This file contains wrappers to handle special cases of managing memory - ** related to ostreams. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Mathias Preiner, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * Wrappers to handle memory management of ostreams. + * + * This file contains wrappers to handle special cases of managing memory + * related to ostreams. + */ #include "cvc4_private.h" diff --git a/src/smt/model.cpp b/src/smt/model.cpp index a3742b652..cf6a90f12 100644 --- a/src/smt/model.cpp +++ b/src/smt/model.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file model.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 implementation of Model class - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Implementation of Model class. + */ #include "smt/model.h" diff --git a/src/smt/model.h b/src/smt/model.h index 1dd65a6b9..b6d0b1644 100644 --- a/src/smt/model.h +++ b/src/smt/model.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file model.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Model class - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Model class. + */ #include "cvc4_private.h" diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp index 64769a2ad..04613f848 100644 --- a/src/smt/model_blocker.cpp +++ b/src/smt/model_blocker.cpp @@ -1,17 +1,17 @@ -/********************* */ -/*! \file model_blocker.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Implementation of utility for blocking models. - ** - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Implementation of utility for blocking models. + */ #include "smt/model_blocker.h" diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h index 6ef9b0662..a6a8ea31d 100644 --- a/src/smt/model_blocker.h +++ b/src/smt/model_blocker.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file model_blocker.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Gereon Kremer - ** 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 Utility for blocking the current model - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mathias Preiner, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * Utility for blocking the current model. + */ #include "cvc4_private.h" diff --git a/src/smt/model_core_builder.cpp b/src/smt/model_core_builder.cpp index f16c93e62..5b6df3c1a 100644 --- a/src/smt/model_core_builder.cpp +++ b/src/smt/model_core_builder.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file model_core_builder.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Implementation of utility for building model cores - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Implementation of utility for building model cores. + */ #include "smt/model_core_builder.h" diff --git a/src/smt/model_core_builder.h b/src/smt/model_core_builder.h index 05e9b804e..fac456484 100644 --- a/src/smt/model_core_builder.h +++ b/src/smt/model_core_builder.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file model_core_builder.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Utility for building model cores - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Utility for building model cores. + */ #include "cvc4_private.h" diff --git a/src/smt/node_command.cpp b/src/smt/node_command.cpp index 61d380b72..b3e747ecb 100644 --- a/src/smt/node_command.cpp +++ b/src/smt/node_command.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file node_command.cpp - ** \verbatim - ** Top contributors (to current version): - ** Abdalrhman Mohamed, Yoni Zohar, 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 of NodeCommand functions. - ** - ** Implementation of NodeCommand functions. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Abdalrhman Mohamed, Yoni Zohar, 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 of NodeCommand functions. + */ #include "smt/node_command.h" diff --git a/src/smt/node_command.h b/src/smt/node_command.h index 87bb713c6..af59bb195 100644 --- a/src/smt/node_command.h +++ b/src/smt/node_command.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file node_command.h - ** \verbatim - ** Top contributors (to current version): - ** Abdalrhman Mohamed - ** 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 Datastructures used for printing commands internally. - ** - ** Datastructures used for printing commands internally. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Abdalrhman Mohamed + * + * 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. + * **************************************************************************** + * + * Datastructures used for printing commands internally. + */ #include "cvc4_private.h" diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index 70fa0f28c..f854ec402 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file optimization_solver.cpp - ** \verbatim - ** Top contributors (to current version): - ** Michael Chang, Yancheng Ou - ** 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 solver for optimization queries - **/ +/****************************************************************************** + * Top contributors (to current version): + * Michael Chang, Yancheng Ou, 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 solver for optimization queries. + */ #include "smt/optimization_solver.h" diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h index edbbcbde1..9d075e5de 100644 --- a/src/smt/optimization_solver.h +++ b/src/smt/optimization_solver.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file optimization_solver.h - ** \verbatim - ** Top contributors (to current version): - ** Michael Chang, Yancheng Ou - ** 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 solver for optimization queries - **/ +/****************************************************************************** + * Top contributors (to current version): + * Michael Chang, Yancheng Ou, 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 solver for optimization queries. + */ #include "cvc4_private.h" @@ -70,7 +71,7 @@ enum class OptResult * - the optimization target node, * - whether it's maximize/minimize * - and whether it's signed for BitVectors - **/ + */ class Objective { public: diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp index 0a7a0c54a..2c732fa9d 100644 --- a/src/smt/options_manager.cpp +++ b/src/smt/options_manager.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file options_manager.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Module for managing options of an SmtEngine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Module for managing options of an SmtEngine. + */ #include "smt/options_manager.h" diff --git a/src/smt/options_manager.h b/src/smt/options_manager.h index 89f5acd6a..4705b4273 100644 --- a/src/smt/options_manager.h +++ b/src/smt/options_manager.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file options_manager.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Gereon Kremer - ** 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 Module for managing options of an SmtEngine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Tim King, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * Module for managing options of an SmtEngine. + */ #ifndef CVC5__SMT__OPTIONS_MANAGER_H #define CVC5__SMT__OPTIONS_MANAGER_H diff --git a/src/smt/output_manager.cpp b/src/smt/output_manager.cpp index a01c7a6a9..6395a4c2c 100644 --- a/src/smt/output_manager.cpp +++ b/src/smt/output_manager.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file output_manager.cpp - ** \verbatim - ** Top contributors (to current version): - ** Abdalrhman Mohamed - ** 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 of OutputManager functions. - ** - ** Implementation of OutputManager functions. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Abdalrhman Mohamed, 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 of OutputManager functions. + */ #include "smt/output_manager.h" diff --git a/src/smt/output_manager.h b/src/smt/output_manager.h index 668daae0b..bb7645f75 100644 --- a/src/smt/output_manager.h +++ b/src/smt/output_manager.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file output_manager.h - ** \verbatim - ** Top contributors (to current version): - ** Abdalrhman Mohamed - ** 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 output manager for the SmtEngine. - ** - ** The output manager provides helper functions for printing commands - ** internally. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Abdalrhman Mohamed + * + * 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 output manager for the SmtEngine. + * + * The output manager provides helper functions for printing commands + * internally. + */ #ifndef CVC5__SMT__OUTPUT_MANAGER_H #define CVC5__SMT__OUTPUT_MANAGER_H diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp index 016f60cfc..ea5d28a23 100644 --- a/src/smt/preprocess_proof_generator.cpp +++ b/src/smt/preprocess_proof_generator.cpp @@ -1,17 +1,18 @@ -/********************* */ -/*! \file preprocess_proof_generator.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer - ** 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 implementation of the module for proofs for preprocessing in an - ** SMT engine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer + * + * 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 implementation of the module for proofs for preprocessing in an + * SMT engine. + */ #include "smt/preprocess_proof_generator.h" diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h index a9d5bd2b6..1bd03d7f5 100644 --- a/src/smt/preprocess_proof_generator.h +++ b/src/smt/preprocess_proof_generator.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file preprocess_proof_generator.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer - ** 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 module for proofs for preprocessing in an SMT engine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer + * + * 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 module for proofs for preprocessing in an SMT engine. + */ #include "cvc4_private.h" diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index 28f393704..859eb84fc 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file preprocessor.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Abdalrhman Mohamed - ** 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 preprocessor of the SMT engine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Morgan Deters, 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 preprocessor of the SMT engine. + */ #include "smt/preprocessor.h" diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h index 40b1b1278..e0fa39593 100644 --- a/src/smt/preprocessor.h +++ b/src/smt/preprocessor.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file preprocessor.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Justin Xu - ** 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 preprocessor of the SmtEngine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Morgan Deters, Justin Xu + * + * 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 preprocessor of the SmtEngine. + */ #include "cvc4_private.h" diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 29651211c..2c97d9413 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file process_assertions.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Yoni Zohar - ** 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 of module for processing assertions for an SMT engine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Morgan Deters, 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. + * **************************************************************************** + * + * Implementation of module for processing assertions for an SMT engine. + */ #include "smt/process_assertions.h" diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h index e3f5ae3a3..5931899d9 100644 --- a/src/smt/process_assertions.h +++ b/src/smt/process_assertions.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file process_assertions.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, 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 module for processing assertions for an SMT engine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer, 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. + * **************************************************************************** + * + * The module for processing assertions for an SMT engine. + */ #include "cvc4_private.h" diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 549f10008..b06590918 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_manager.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, Gereon Kremer - ** 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 proof manager of the SMT engine - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, Diego Della Rocca de Camargos + * + * 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 proof manager of the SMT engine. + */ #include "smt/proof_manager.h" diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h index 32f3f73d9..0345991d2 100644 --- a/src/smt/proof_manager.h +++ b/src/smt/proof_manager.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_manager.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer, 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 The proof manager of SmtEngine - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer, 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. + * **************************************************************************** + * + * The proof manager of SmtEngine. + */ #include "cvc4_private.h" diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 19ca089d3..105376719 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_post_processor.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Implementation of module for processing proof nodes - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, 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. + * **************************************************************************** + * + * Implementation of module for processing proof nodes. + */ #include "smt/proof_post_processor.h" diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h index 2459270c0..f5379290e 100644 --- a/src/smt/proof_post_processor.h +++ b/src/smt/proof_post_processor.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_post_processor.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 The module for processing proof nodes - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, Gereon Kremer + * + * 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 module for processing proof nodes. + */ #include "cvc4_private.h" diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index 436d6618d..2f9b89d06 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file quant_elim_solver.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 solver for quantifier elimination queries - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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 solver for quantifier elimination queries. + */ #include "smt/quant_elim_solver.h" diff --git a/src/smt/quant_elim_solver.h b/src/smt/quant_elim_solver.h index cf3be1ec3..06f12ced9 100644 --- a/src/smt/quant_elim_solver.h +++ b/src/smt/quant_elim_solver.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file quant_elim_solver.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 The solver for quantifier elimination queries - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * The solver for quantifier elimination queries. + */ #include "cvc4_private.h" diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 6a5ed52d0..0a8819c4b 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file set_defaults.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Andres Noetzli, 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 Implementation of setting default options. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Andres Noetzli, 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. + * **************************************************************************** + * + * Implementation of setting default options. + */ #include "smt/set_defaults.h" diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h index d3d82774c..6e77b488c 100644 --- a/src/smt/set_defaults.h +++ b/src/smt/set_defaults.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file set_defaults.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 Method for setting the default options of an SMT engine. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Method for setting the default options of an SMT engine. + */ #ifndef CVC5__SMT__SET_DEFAULTS_H #define CVC5__SMT__SET_DEFAULTS_H diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index bb14232bb..3a67b7bf3 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file smt_engine.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Abdalrhman Mohamed - ** 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 main entry point into the CVC4 library's SMT interface - ** - ** The main entry point into the CVC4 library's SMT interface. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Morgan Deters, Abdalrhman Mohamed + * + * 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 main entry point into the cvc5 library's SMT interface. + */ #include "smt/smt_engine.h" diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index df5c69613..63ba5f831 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file smt_engine.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, 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 SmtEngine: the main public entry point of libcvc4. - ** - ** SmtEngine: the main public entry point of libcvc4. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Morgan Deters, 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. + * **************************************************************************** + * + * SmtEngine: the main public entry point of libcvc5. + */ #include "cvc4_public.h" diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp index aa349d980..1164bc1b5 100644 --- a/src/smt/smt_engine_scope.cpp +++ b/src/smt/smt_engine_scope.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file smt_engine_scope.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, 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 one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, 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 lengthier description here ]] + * \todo document this file + */ #include "smt/smt_engine_scope.h" diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h index e00c4fcb1..46efac90a 100644 --- a/src/smt/smt_engine_scope.h +++ b/src/smt/smt_engine_scope.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file smt_engine_scope.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Andres Noetzli, 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 one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include "cvc4_private.h" diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp index c8f23f7f8..cabaf8823 100644 --- a/src/smt/smt_engine_state.cpp +++ b/src/smt/smt_engine_state.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file smt_engine_state.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Ying Sheng - ** 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 Utility for maintaining the state of the SMT engine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Morgan Deters, Ying Sheng + * + * 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. + * **************************************************************************** + * + * Utility for maintaining the state of the SMT engine. + */ #include "smt/smt_engine_state.h" diff --git a/src/smt/smt_engine_state.h b/src/smt/smt_engine_state.h index 0e02a5605..284771cc5 100644 --- a/src/smt/smt_engine_state.h +++ b/src/smt/smt_engine_state.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file smt_engine_state.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Ying Sheng, 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 Utility for maintaining the state of the SMT engine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Ying Sheng, 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. + * **************************************************************************** + * + * Utility for maintaining the state of the SMT engine. + */ #include "cvc4_private.h" diff --git a/src/smt/smt_engine_stats.cpp b/src/smt/smt_engine_stats.cpp index b0de2d8b3..5147c046a 100644 --- a/src/smt/smt_engine_stats.cpp +++ b/src/smt/smt_engine_stats.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file smt_engine_stats.cpp - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Andrew Reynolds, 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 Implementation of statistics for SMT engine - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Gereon Kremer, 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 of statistics for SMT engine. + */ #include "smt/smt_engine_stats.h" diff --git a/src/smt/smt_engine_stats.h b/src/smt/smt_engine_stats.h index b3fd5a1b7..fa95709d8 100644 --- a/src/smt/smt_engine_stats.h +++ b/src/smt/smt_engine_stats.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file smt_engine_stats.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, 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 Statistics for SMT engine - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Andrew Reynolds, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * Statistics for SMT engine. + */ #include "cvc4_private.h" diff --git a/src/smt/smt_mode.cpp b/src/smt/smt_mode.cpp index db21e53c4..2ac8bcdea 100644 --- a/src/smt/smt_mode.cpp +++ b/src/smt/smt_mode.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file smt_mode.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 Enumeration type for the mode of an SmtEngine. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Enumeration type for the mode of an SmtEngine. + */ #include "smt/smt_mode.h" diff --git a/src/smt/smt_mode.h b/src/smt/smt_mode.h index 47cb15eb6..8061a2e21 100644 --- a/src/smt/smt_mode.h +++ b/src/smt/smt_mode.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file smt_mode.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Ying Sheng, 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 Enumeration type for the mode of an SmtEngine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Ying Sheng, 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. + * **************************************************************************** + * + * Enumeration type for the mode of an SmtEngine. + */ #include "cvc4_public.h" diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 3a1c6b12c..fbb679cf7 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file smt_solver.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Aina Niemetz, 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 The solver for SMT queries in an SmtEngine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Aina Niemetz, 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. + * **************************************************************************** + * + * The solver for SMT queries in an SmtEngine. + */ #include "smt/smt_solver.h" diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h index 06f576445..e4493eedf 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_solver.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file smt_solver.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, 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 solver for SMT queries in an SmtEngine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Morgan Deters, 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 solver for SMT queries in an SmtEngine. + */ #include "cvc4_private.h" diff --git a/src/smt/smt_statistics_registry.cpp b/src/smt/smt_statistics_registry.cpp index dd5ed470c..db437526a 100644 --- a/src/smt/smt_statistics_registry.cpp +++ b/src/smt/smt_statistics_registry.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file smt_statistics_registry.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 Accessor for the SmtEngine's StatisticsRegistry. - ** - ** Accessor for the SmtEngine's StatisticsRegistry. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Accessor for the SmtEngine's StatisticsRegistry. + */ #include "smt/smt_statistics_registry.h" diff --git a/src/smt/smt_statistics_registry.h b/src/smt/smt_statistics_registry.h index 97bdde703..cafb9e62a 100644 --- a/src/smt/smt_statistics_registry.h +++ b/src/smt/smt_statistics_registry.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file smt_statistics_registry.h - ** \verbatim - ** Top contributors (to current version): - ** 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 Accessor for the SmtEngine's StatisticsRegistry. - ** - ** Accessor for the SmtEngine's StatisticsRegistry. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Accessor for the SmtEngine's StatisticsRegistry. + */ #include "cvc4_private.h" diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 022691a12..00598534f 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file sygus_solver.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, Abdalrhman Mohamed - ** 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 solver for sygus queries - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, Abdalrhman Mohamed + * + * 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 solver for SyGuS queries. + */ #include "smt/sygus_solver.h" diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h index 8e6f08b75..f701419d9 100644 --- a/src/smt/sygus_solver.h +++ b/src/smt/sygus_solver.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file sygus_solver.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, Abdalrhman Mohamed - ** 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 solver for sygus queries - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, Abdalrhman Mohamed + * + * 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 solver for SyGuS queries. + */ #include "cvc4_private.h" diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 262c46870..823511b02 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file term_formula_removal.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Dejan Jovanovic, Mudathir Mohamed - ** 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 Removal of term formulas - ** - ** Removal of term formulas. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Dejan Jovanovic, Mudathir Mohamed + * + * 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. + * **************************************************************************** + * + * Removal of term formulas. + */ #include "smt/term_formula_removal.h" #include <vector> diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index d2d3bf6fd..65f4bdb7a 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file term_formula_removal.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Dejan Jovanovic, 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 Removal of term formulas - ** - ** Removal of term formulas. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Dejan Jovanovic, 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. + * **************************************************************************** + * + * Removal of term formulas. + */ #include "cvc4_private.h" diff --git a/src/smt/unsat_core_manager.cpp b/src/smt/unsat_core_manager.cpp index 976e7ea6c..df8f2f9d9 100644 --- a/src/smt/unsat_core_manager.cpp +++ b/src/smt/unsat_core_manager.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file unsat_core_manager.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 Implementation of the unsat core manager of SmtEngine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Implementation of the unsat core manager of SmtEngine. + */ #include "unsat_core_manager.h" diff --git a/src/smt/unsat_core_manager.h b/src/smt/unsat_core_manager.h index ac87bbe6e..6bfcec9f8 100644 --- a/src/smt/unsat_core_manager.h +++ b/src/smt/unsat_core_manager.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file unsat_core_manager.h - ** \verbatim - ** Top contributors (to current version): - ** 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 The unsat core manager of SmtEngine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * The unsat core manager of SmtEngine. + */ #include "cvc4_private.h" diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h index b1cb855c6..8bb230982 100644 --- a/src/smt/update_ostream.h +++ b/src/smt/update_ostream.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file update_ostream.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, 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): + * Tim King, 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 + */ #include "cvc4_private.h" diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp index 2ae39a664..c7e3d3280 100644 --- a/src/smt/witness_form.cpp +++ b/src/smt/witness_form.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file witness_form.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 The module for managing witness form conversion in proofs - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * The module for managing witness form conversion in proofs. + */ #include "smt/witness_form.h" diff --git a/src/smt/witness_form.h b/src/smt/witness_form.h index 37f672e57..938fc40d1 100644 --- a/src/smt/witness_form.h +++ b/src/smt/witness_form.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file witness_form.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 The module for managing witness form conversion in proofs - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * The module for managing witness form conversion in proofs. + */ #include "cvc4_private.h" |