diff options
Diffstat (limited to 'src/parser/smt2')
-rw-r--r-- | src/parser/smt2/Smt2.g | 12 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 13 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 12 | ||||
-rw-r--r-- | src/parser/smt2/smt2_input.cpp | 12 | ||||
-rw-r--r-- | src/parser/smt2/smt2_input.h | 12 | ||||
-rw-r--r-- | src/parser/smt2/sygus_input.cpp | 12 | ||||
-rw-r--r-- | src/parser/smt2/sygus_input.h | 12 |
7 files changed, 43 insertions, 42 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 0526ba66d..38163c579 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1,13 +1,13 @@ /* ******************* */ /*! \file Smt2.g ** \verbatim - ** Original author: Christopher L. Conway - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): Dejan Jovanovic, Kshitij Bansal, Tianyi Liang, Francois Bobot, Andrew Reynolds + ** Top contributors (to current version): + ** Morgan Deters, Andrew Reynolds, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Parser for SMT-LIB v2 input language ** diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index e3fbe36f2..ebad90583 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file smt2.cpp ** \verbatim - ** Original author: Christopher L. Conway - ** Major contributors: Kshitij Bansal, Morgan Deters - ** Minor contributors (to current version): Andrew Reynolds, Clark Barrett, Tianyi Liang + ** Top contributors (to current version): + ** Andrew Reynolds, Kshitij Bansal, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Definitions of SMT2 constants. ** @@ -226,6 +226,7 @@ void Smt2::addTheory(Theory theory) { addOperator(kind::MEMBER, "member"); addOperator(kind::SINGLETON, "singleton"); addOperator(kind::INSERT, "insert"); + addOperator(kind::CARD, "card"); break; case THEORY_DATATYPES: diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 7cf92f008..1ae2c9dd7 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -1,13 +1,13 @@ /********************* */ /*! \file smt2.h ** \verbatim - ** Original author: Christopher L. Conway - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): Tianyi Liang, Kshitij Bansal + ** Top contributors (to current version): + ** Morgan Deters, Andrew Reynolds, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Definitions of SMT2 constants. ** diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index cea6db278..7aa4c3441 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file smt2_input.cpp ** \verbatim - ** Original author: Christopher L. Conway - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Christopher L. Conway, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add file-specific comments here ]]. ** diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index 9a07ddc08..0ed88393f 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -1,13 +1,13 @@ /********************* */ /*! \file smt2_input.h ** \verbatim - ** Original author: Christopher L. Conway - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Christopher L. Conway, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add file-specific comments here ]]. ** diff --git a/src/parser/smt2/sygus_input.cpp b/src/parser/smt2/sygus_input.cpp index e4f36b3df..5b20e0a9a 100644 --- a/src/parser/smt2/sygus_input.cpp +++ b/src/parser/smt2/sygus_input.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file sygus_input.cpp ** \verbatim - ** Original author: Christopher L. Conway - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add file-specific comments here ]]. ** diff --git a/src/parser/smt2/sygus_input.h b/src/parser/smt2/sygus_input.h index 1f0078076..50bc973e9 100644 --- a/src/parser/smt2/sygus_input.h +++ b/src/parser/smt2/sygus_input.h @@ -1,13 +1,13 @@ /********************* */ /*! \file sygus_input.h ** \verbatim - ** Original author: Christopher L. Conway - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add file-specific comments here ]]. ** |