diff options
Diffstat (limited to 'test/api/ouroborous.cpp')
-rw-r--r-- | test/api/ouroborous.cpp | 51 |
1 files changed, 26 insertions, 25 deletions
diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp index 96698b4d2..d4aeaf427 100644 --- a/test/api/ouroborous.cpp +++ b/test/api/ouroborous.cpp @@ -1,28 +1,29 @@ -/********************* */ -/*! \file ouroborous.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Morgan Deters, Christopher L. Conway - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief "Ouroborous" test: does CVC4 read its own output? - ** - ** The "Ouroborous" test, named after the serpent that swallows its - ** own tail, ensures that CVC4 can parse some input, output it again - ** (in any of its languages) and then parse it again. The result of - ** the first parse must be equal to the result of the second parse; - ** both strings and expressions are compared for equality. - ** - ** To add a new test, simply add a call to runTestString() under - ** runTest(), below. If you don't specify an input language, - ** LANG_SMTLIB_V2 is used. If your example depends on variables, - ** you'll need to declare them in the "declarations" global, just - ** below, in SMT-LIBv2 form (but they're good for all languages). - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * "Ouroborous" test: does CVC4 read its own output? + * + * The "Ouroborous" test, named after the serpent that swallows its + * own tail, ensures that CVC4 can parse some input, output it again + * (in any of its languages) and then parse it again. The result of + * the first parse must be equal to the result of the second parse; + * both strings and expressions are compared for equality. + * + * To add a new test, simply add a call to runTestString() under + * runTest(), below. If you don't specify an input language, + * LANG_SMTLIB_V2 is used. If your example depends on variables, + * you'll need to declare them in the "declarations" global, just + * below, in SMT-LIBv2 form (but they're good for all languages). + */ #include <cassert> #include <iostream> |