diff options
Diffstat (limited to 'examples')
67 files changed, 280 insertions, 205 deletions
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index dde43d825..d253c9779 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -1,3 +1,13 @@ +##################### +## CMakeLists.txt +## Top contributors (to current version): +## Aina Niemetz, Mathias Preiner, Andres Noetzli +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 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. +## cmake_minimum_required(VERSION 3.4) project(cvc4-examples) diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java index 81e7a1f64..0972d4019 100644 --- a/examples/SimpleVC.java +++ b/examples/SimpleVC.java @@ -5,7 +5,7 @@ ** Morgan Deters, Aina Niemetz, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/SimpleVC.py b/examples/SimpleVC.py index 50c52868b..088ab7514 100755..100644 --- a/examples/SimpleVC.py +++ b/examples/SimpleVC.py @@ -1,4 +1,14 @@ #! /usr/bin/python +##################### +## SimpleVC.py +## Top contributors (to current version): +## Morgan Deters, Aina Niemetz, Andres Noetzli +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 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. +## ##! \file SimpleVC.py ### \verbatim ### Original author: mdeters diff --git a/examples/api/CMakeLists.txt b/examples/api/CMakeLists.txt index bd6361b5c..cbf5fee7b 100644 --- a/examples/api/CMakeLists.txt +++ b/examples/api/CMakeLists.txt @@ -1,3 +1,13 @@ +##################### +## CMakeLists.txt +## Top contributors (to current version): +## Mathias Preiner, Abdalrhman Mohamed, Aina Niemetz +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 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. +## set(CVC4_EXAMPLES_API bitvectors bitvectors_and_arrays diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp index ab1e8ce07..2e0874b77 100644 --- a/examples/api/bitvectors.cpp +++ b/examples/api/bitvectors.cpp @@ -2,10 +2,10 @@ /*! \file bitvectors.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Makai Mann + ** Aina Niemetz, Liana Hadarean, Makai Mann ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/bitvectors_and_arrays.cpp b/examples/api/bitvectors_and_arrays.cpp index 2c98d4f8a..2096c379e 100644 --- a/examples/api/bitvectors_and_arrays.cpp +++ b/examples/api/bitvectors_and_arrays.cpp @@ -2,10 +2,10 @@ /*! \file bitvectors_and_arrays.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz + ** Aina Niemetz, Liana Hadarean ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp index 817ed6f65..191bb83bd 100644 --- a/examples/api/combination.cpp +++ b/examples/api/combination.cpp @@ -2,10 +2,10 @@ /*! \file combination.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Andrew Reynolds + ** Aina Niemetz, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp index dd2c2695d..00c0b9810 100644 --- a/examples/api/datatypes.cpp +++ b/examples/api/datatypes.cpp @@ -2,10 +2,10 @@ /*! \file datatypes.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Andrew Reynolds, Makai Mann + ** Aina Niemetz, Morgan Deters, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/extract.cpp b/examples/api/extract.cpp index 6ff0db10d..42baca4bc 100644 --- a/examples/api/extract.cpp +++ b/examples/api/extract.cpp @@ -2,10 +2,10 @@ /*! \file extract.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Makai Mann + ** Aina Niemetz, Makai Mann, Clark Barrett ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/helloworld.cpp b/examples/api/helloworld.cpp index 873947522..f7cb3908d 100644 --- a/examples/api/helloworld.cpp +++ b/examples/api/helloworld.cpp @@ -2,10 +2,10 @@ /*! \file helloworld.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz + ** Aina Niemetz, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java index e340a0b91..5f2950a0e 100644 --- a/examples/api/java/BitVectors.java +++ b/examples/api/java/BitVectors.java @@ -5,7 +5,7 @@ ** Morgan Deters, Liana Hadarean, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/java/BitVectorsAndArrays.java b/examples/api/java/BitVectorsAndArrays.java index 6adb2a61d..64eb3c5db 100644 --- a/examples/api/java/BitVectorsAndArrays.java +++ b/examples/api/java/BitVectorsAndArrays.java @@ -5,7 +5,7 @@ ** Morgan Deters, Liana Hadarean, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt index 0afcec0e4..ce01c2ea9 100644 --- a/examples/api/java/CMakeLists.txt +++ b/examples/api/java/CMakeLists.txt @@ -1,3 +1,13 @@ +##################### +## CMakeLists.txt +## Top contributors (to current version): +## Andres Noetzli, Aina Niemetz, Mathias Preiner +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 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. +## set(EXAMPLES_API_JAVA ## disabled until bindings for the new API are in place (issue #2284) # BitVectors diff --git a/examples/api/java/CVC4Streams.java b/examples/api/java/CVC4Streams.java index 0ee3f98b2..e16a9f3f3 100644 --- a/examples/api/java/CVC4Streams.java +++ b/examples/api/java/CVC4Streams.java @@ -5,7 +5,7 @@ ** Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java index 915aed78b..47828085e 100644 --- a/examples/api/java/Combination.java +++ b/examples/api/java/Combination.java @@ -5,7 +5,7 @@ ** Morgan Deters, Tim King, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/java/Datatypes.java b/examples/api/java/Datatypes.java index 5c9b0ef72..3eb64ed7d 100644 --- a/examples/api/java/Datatypes.java +++ b/examples/api/java/Datatypes.java @@ -2,10 +2,10 @@ /*! \file Datatypes.java ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Andres Noetzli + ** Morgan Deters, Andres Noetzli, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/java/Exceptions.java b/examples/api/java/Exceptions.java index f6b9d557c..dfe5e63fe 100644 --- a/examples/api/java/Exceptions.java +++ b/examples/api/java/Exceptions.java @@ -5,7 +5,7 @@ ** Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/java/FloatingPointArith.java b/examples/api/java/FloatingPointArith.java index c296a3fb1..fd8e7dd2d 100644 --- a/examples/api/java/FloatingPointArith.java +++ b/examples/api/java/FloatingPointArith.java @@ -5,7 +5,7 @@ ** Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/java/HelloWorld.java b/examples/api/java/HelloWorld.java index 86e0c4da3..cff384803 100644 --- a/examples/api/java/HelloWorld.java +++ b/examples/api/java/HelloWorld.java @@ -5,7 +5,7 @@ ** Morgan Deters, Tim King, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/java/LinearArith.java b/examples/api/java/LinearArith.java index 474a481f2..a363477d2 100644 --- a/examples/api/java/LinearArith.java +++ b/examples/api/java/LinearArith.java @@ -5,7 +5,7 @@ ** Morgan Deters, Tim King, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/java/PipedInput.java b/examples/api/java/PipedInput.java index 42bea34cc..1642991a3 100644 --- a/examples/api/java/PipedInput.java +++ b/examples/api/java/PipedInput.java @@ -5,7 +5,7 @@ ** Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/java/Relations.java b/examples/api/java/Relations.java index f5c5db8a7..10d172332 100644 --- a/examples/api/java/Relations.java +++ b/examples/api/java/Relations.java @@ -5,7 +5,7 @@ ** Mudathir Mohamed, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/java/Statistics.java b/examples/api/java/Statistics.java index 1f5264b5f..ac7e9ce13 100644 --- a/examples/api/java/Statistics.java +++ b/examples/api/java/Statistics.java @@ -5,7 +5,7 @@ ** Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/java/Strings.java b/examples/api/java/Strings.java index 1d5594c67..24c1fa7dc 100644 --- a/examples/api/java/Strings.java +++ b/examples/api/java/Strings.java @@ -5,7 +5,7 @@ ** Tianyi Liang, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/java/UnsatCores.java b/examples/api/java/UnsatCores.java index 648e7f1d3..5713d98fe 100644 --- a/examples/api/java/UnsatCores.java +++ b/examples/api/java/UnsatCores.java @@ -5,7 +5,7 @@ ** Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp index c60e17f85..2d6636d0f 100644 --- a/examples/api/linear_arith.cpp +++ b/examples/api/linear_arith.cpp @@ -2,10 +2,10 @@ /*! \file linear_arith.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz + ** Aina Niemetz, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/python/CMakeLists.txt b/examples/api/python/CMakeLists.txt index 0da960513..04bb8a818 100644 --- a/examples/api/python/CMakeLists.txt +++ b/examples/api/python/CMakeLists.txt @@ -1,3 +1,13 @@ +##################### +## CMakeLists.txt +## Top contributors (to current version): +## Andres Noetzli +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 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. +## set(EXAMPLES_API_PYTHON bitvectors_and_arrays bitvectors diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py index f12e79541..c370e50be 100755..100644 --- a/examples/api/python/bitvectors.py +++ b/examples/api/python/bitvectors.py @@ -1,19 +1,19 @@ #!/usr/bin/env python - ##################### -#! \file bitvectors.py - ## \verbatim - ## Top contributors (to current version): - ## Makai Mann, Aina Niemetz - ## This file is part of the CVC4 project. - ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ## in the top-level source directory) and their institutional affiliations. - ## All rights reserved. See the file COPYING in the top-level source - ## directory for licensing information.\endverbatim - ## - ## \brief A simple demonstration of the solving capabilities of the CVC4 - ## bit-vector solver through the Python API. This is a direct translation - ## of bitvectors-new.cpp. +## bitvectors.py +## Top contributors (to current version): +## Makai Mann, Aina Niemetz +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS +## in the top-level source directory and their institutional affiliations. +## All rights reserved. See the file COPYING in the top-level source +## directory for licensing information. +## +## A simple demonstration of the solving capabilities of the CVC4 +## bit-vector solver through the Python API. This is a direct translation +## of bitvectors-new.cpp. +## + import pycvc4 from pycvc4 import kinds diff --git a/examples/api/python/bitvectors_and_arrays.py b/examples/api/python/bitvectors_and_arrays.py index 7e3d8f478..be88f690e 100755..100644 --- a/examples/api/python/bitvectors_and_arrays.py +++ b/examples/api/python/bitvectors_and_arrays.py @@ -1,19 +1,19 @@ #!/usr/bin/env python - ##################### -#! \file bitvectors_and_arrays.py - ## \verbatim - ## Top contributors (to current version): - ## Makai Mann - ## This file is part of the CVC4 project. - ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ## in the top-level source directory) and their institutional affiliations. - ## All rights reserved. See the file COPYING in the top-level source - ## directory for licensing information.\endverbatim - ## - ## \brief A simple demonstration of the solving capabilities of the CVC4 - ## bit-vector and array solvers through the Python API. This is a direct - ## translation of bitvectors_and_arrays-new.cpp. +## bitvectors_and_arrays.py +## Top contributors (to current version): +## Makai Mann +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS +## in the top-level source directory and their institutional affiliations. +## All rights reserved. See the file COPYING in the top-level source +## directory for licensing information. +## +## A simple demonstration of the solving capabilities of the CVC4 +## bit-vector and array solvers through the Python API. This is a direct +## translation of bitvectors_and_arrays-new.cpp. +## + import pycvc4 from pycvc4 import kinds diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py index bae2b6ef9..253365c9d 100755..100644 --- a/examples/api/python/combination.py +++ b/examples/api/python/combination.py @@ -1,19 +1,19 @@ #!/usr/bin/env python - ##################### -#! \file combination.py - ## \verbatim - ## Top contributors (to current version): - ## Makai Mann, Aina Niemetz - ## This file is part of the CVC4 project. - ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ## in the top-level source directory) and their institutional affiliations. - ## All rights reserved. See the file COPYING in the top-level source - ## directory for licensing information.\endverbatim - ## - ## \brief A simple demonstration of the solving capabilities of the CVC4 - ## combination solver through the Python API. This is a direct translation - ## of combination-new.cpp. +## combination.py +## Top contributors (to current version): +## Makai Mann, Aina Niemetz, Andrew Reynolds +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS +## in the top-level source directory and their institutional affiliations. +## All rights reserved. See the file COPYING in the top-level source +## directory for licensing information. +## +## A simple demonstration of the solving capabilities of the CVC4 +## combination solver through the Python API. This is a direct translation +## of combination-new.cpp. +## + import pycvc4 from pycvc4 import kinds diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py index 1a67f5661..8ae2c29fd 100755..100644 --- a/examples/api/python/datatypes.py +++ b/examples/api/python/datatypes.py @@ -1,19 +1,18 @@ #!/usr/bin/env python - ##################### -#! \file datatypes.py - ## \verbatim - ## Top contributors (to current version): - ## Makai Mann - ## This file is part of the CVC4 project. - ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ## in the top-level source directory) and their institutional affiliations. - ## All rights reserved. See the file COPYING in the top-level source - ## directory for licensing information.\endverbatim - ## - ## \brief A simple demonstration of the solving capabilities of the CVC4 - ## datatypes solver through the Python API. This is a direct translation - ## of datatypes-new.cpp. +## datatypes.py +## Top contributors (to current version): +## Makai Mann, Andrew Reynolds, Aina Niemetz +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 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. +## +## \brief A simple demonstration of the solving capabilities of the CVC4 +## datatypes solver through the Python API. This is a direct translation +## of datatypes-new.cpp. +## import pycvc4 from pycvc4 import kinds diff --git a/examples/api/python/exceptions.py b/examples/api/python/exceptions.py index 27f068011..97b186b26 100644 --- a/examples/api/python/exceptions.py +++ b/examples/api/python/exceptions.py @@ -1,20 +1,19 @@ #!/usr/bin/env python - ##################### -## \file exceptions.py -## \verbatim +## exceptions.py ## Top contributors (to current version): ## Andres Noetzli ## This file is part of the CVC4 project. ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS -## in the top-level source directory) and their institutional affiliations. +## 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 +## directory for licensing information. ## -## \brief Catching CVC4 exceptions with the legacy Python API. +## Catching CVC4 exceptions with the legacy Python API. ## ## A simple demonstration of catching CVC4 execptions with the legacy Python ## API. +## import pycvc4 from pycvc4 import kinds diff --git a/examples/api/python/extract.py b/examples/api/python/extract.py index 2b8714739..dfe339003 100755..100644 --- a/examples/api/python/extract.py +++ b/examples/api/python/extract.py @@ -1,19 +1,18 @@ #!/usr/bin/env python - ##################### -#! \file extract.py - ## \verbatim - ## Top contributors (to current version): - ## Makai Mann, Aina Niemetz - ## This file is part of the CVC4 project. - ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ## in the top-level source directory) and their institutional affiliations. - ## All rights reserved. See the file COPYING in the top-level source - ## directory for licensing information.\endverbatim - ## - ## \brief A simple demonstration of the solving capabilities of the CVC4 - ## bit-vector solver through the Python API. This is a direct translation - ## of extract-new.cpp. +## extract.py +## Top contributors (to current version): +## Makai Mann, Aina Niemetz +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS +## in the top-level source directory and their institutional affiliations. +## All rights reserved. See the file COPYING in the top-level source +## directory for licensing information. +## +## A simple demonstration of the solving capabilities of the CVC4 +## bit-vector solver through the Python API. This is a direct translation +## of extract-new.cpp. +## from pycvc4 import Solver from pycvc4.kinds import BVExtract, Equal diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py index 6fb595e34..bee23b2c7 100755..100644 --- a/examples/api/python/floating_point.py +++ b/examples/api/python/floating_point.py @@ -1,19 +1,18 @@ #!/usr/bin/env python - ##################### -#! \file floating_point.py - ## \verbatim - ## Top contributors (to current version): - ## Eva Darulova, Makai Mann - ## This file is part of the CVC4 project. - ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ## in the top-level source directory) and their institutional affiliations. - ## All rights reserved. See the file COPYING in the top-level source - ## directory for licensing information.\endverbatim - ## - ## \brief A simple demonstration of the solving capabilities of the CVC4 - ## floating point solver through the Python API contributed by Eva - ## Darulova. This requires building CVC4 with symfpu. +## floating_point.py +## Top contributors (to current version): +## Makai Mann, Andres Noetzli +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS +## in the top-level source directory and their institutional affiliations. +## All rights reserved. See the file COPYING in the top-level source +## directory for licensing information. +## +## A simple demonstration of the solving capabilities of the CVC4 +## floating point solver through the Python API contributed by Eva +## Darulova. This requires building CVC4 with symfpu. +## import pycvc4 from pycvc4 import kinds diff --git a/examples/api/python/helloworld.py b/examples/api/python/helloworld.py index 5607d7f83..2d05822e5 100755..100644 --- a/examples/api/python/helloworld.py +++ b/examples/api/python/helloworld.py @@ -1,17 +1,17 @@ #!/usr/bin/env python - ##################### -#! \file helloworld.py -## \verbatim +## helloworld.py ## Top contributors (to current version): ## Makai Mann, Aina Niemetz ## This file is part of the CVC4 project. -## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS -## in the top-level source directory) and their institutional affiliations. +## Copyright (c) 2009-2020 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 +## directory for licensing information. +## +## A very simple CVC4 tutorial example, adapted from helloworld-new.cpp ## -## \brief A very simple CVC4 tutorial example, adapted from helloworld-new.cpp + import pycvc4 from pycvc4 import kinds diff --git a/examples/api/python/linear_arith.py b/examples/api/python/linear_arith.py index bab9680b3..f85171150 100755..100644 --- a/examples/api/python/linear_arith.py +++ b/examples/api/python/linear_arith.py @@ -1,19 +1,19 @@ #!/usr/bin/env python - ##################### -#! \file linear_arith.py -## \verbatim +## linear_arith.py ## Top contributors (to current version): ## Makai Mann, Aina Niemetz ## This file is part of the CVC4 project. -## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS -## in the top-level source directory) and their institutional affiliations. +## Copyright (c) 2009-2020 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 +## directory for licensing information. ## -## \brief A simple demonstration of the solving capabilities of the CVC4 +## A simple demonstration of the solving capabilities of the CVC4 ## linear arithmetic solver through the Python API. This is a direct ## translation of linear_arith-new.cpp. +## + import pycvc4 from pycvc4 import kinds diff --git a/examples/api/python/sequences.py b/examples/api/python/sequences.py index 4498e5153..1b0c34f44 100644 --- a/examples/api/python/sequences.py +++ b/examples/api/python/sequences.py @@ -1,19 +1,19 @@ #!/usr/bin/env python - ##################### -#! \file sequences.py -## \verbatim +## sequences.py ## Top contributors (to current version): -## Andres Noetzli +## Andres Noetzli, Makai Mann ## This file is part of the CVC4 project. ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS -## in the top-level source directory) and their institutional affiliations. +## 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 +## directory for licensing information. ## -## \brief A simple demonstration of the solving capabilities of the CVC4 +## A simple demonstration of the solving capabilities of the CVC4 ## strings solver through the Python API. This is a direct translation ## of sequences.cpp. +## + import pycvc4 from pycvc4 import kinds diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py index b69c56b56..99a8d4c40 100755..100644 --- a/examples/api/python/sets.py +++ b/examples/api/python/sets.py @@ -1,19 +1,19 @@ #!/usr/bin/env python - ##################### -#! \file sets.py -## \verbatim +## sets.py ## Top contributors (to current version): ## Makai Mann, Aina Niemetz ## This file is part of the CVC4 project. -## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS -## in the top-level source directory) and their institutional affiliations. +## Copyright (c) 2009-2020 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 +## directory for licensing information. ## ## \brief A simple demonstration of the solving capabilities of the CVC4 ## sets solver through the Python API. This is a direct translation ## of sets-new.cpp. +## + import pycvc4 from pycvc4 import kinds diff --git a/examples/api/python/strings.py b/examples/api/python/strings.py index 58a6f6508..c007b4bb5 100755..100644 --- a/examples/api/python/strings.py +++ b/examples/api/python/strings.py @@ -1,19 +1,19 @@ #!/usr/bin/env python - ##################### -#! \file strings.py -## \verbatim +## strings.py ## Top contributors (to current version): -## Makai Mann +## Makai Mann, Andres Noetzli ## This file is part of the CVC4 project. -## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS -## in the top-level source directory) and their institutional affiliations. +## Copyright (c) 2009-2020 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 +## directory for licensing information. ## -## \brief A simple demonstration of the solving capabilities of the CVC4 +## A simple demonstration of the solving capabilities of the CVC4 ## strings solver through the Python API. This is a direct translation ## of strings-new.cpp. +## + import pycvc4 from pycvc4 import kinds diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py index 25090bd8f..d331c9f9e 100644 --- a/examples/api/python/sygus-fun.py +++ b/examples/api/python/sygus-fun.py @@ -1,19 +1,19 @@ #!/usr/bin/env python ##################### -#! \file sygus-fun.py -## \verbatim +## sygus-fun.py ## Top contributors (to current version): -## Yoni Zohar -## This file is part of the CVC4 project. +## Yoni Zohar, Andres Noetzli ## Copyright (c) 2009-2018 by the authors listed in the file AUTHkinds.OrS -## in the top-level source directory) and their institutional affiliations. +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 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 +## directory for licensing information. ## -## \brief A simple demonstration of the solving capabilities of the CVC4 +## A simple demonstration of the solving capabilities of the CVC4 ## sygus solver through the Python API. This is a direct ## translation of sygus-fun.cpp. -##################### +## import copy import pycvc4 diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py index efba88286..7a8f89c68 100644 --- a/examples/api/python/sygus-grammar.py +++ b/examples/api/python/sygus-grammar.py @@ -1,18 +1,19 @@ #!/usr/bin/env python ##################### -#! \file sygus-grammar.py -## \verbatim +## sygus-grammar.py ## Top contributors (to current version): ## Yoni Zohar ## This file is part of the CVC4 project. -## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS -## in the top-level source directory) and their institutional affiliations. +## Copyright (c) 2009-2020 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 +## directory for licensing information. ## -## \brief A simple demonstration of the solving capabilities of the CVC4 +## A simple demonstration of the solving capabilities of the CVC4 ## sygus solver through the Python API. This is a direct ## translation of sygus-grammar.cpp. +## + import copy import pycvc4 from pycvc4 import kinds diff --git a/examples/api/python/sygus-inv.py b/examples/api/python/sygus-inv.py index cb21e1849..f71091371 100644 --- a/examples/api/python/sygus-inv.py +++ b/examples/api/python/sygus-inv.py @@ -1,20 +1,18 @@ #!/usr/bin/env python - ##################### -#! \file sygus-inv.py -## \verbatim +## sygus-inv.py ## Top contributors (to current version): ## Yoni Zohar ## This file is part of the CVC4 project. -## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS -## in the top-level source directory) and their institutional affiliations. +## Copyright (c) 2009-2020 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 +## directory for licensing information. ## -## \brief A simple demonstration of the solving capabilities of the CVC4 +## A simple demonstration of the solving capabilities of the CVC4 ## sygus solver through the Python API. This is a direct ## translation of sygus-inv.cpp . -##################### +## import pycvc4 from pycvc4 import kinds diff --git a/examples/api/sequences.cpp b/examples/api/sequences.cpp index 53bb584ce..3783d35c4 100644 --- a/examples/api/sequences.cpp +++ b/examples/api/sequences.cpp @@ -2,10 +2,10 @@ /*! \file sequences.cpp ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli + ** Andres Noetzli, Aina Niemetz, Tianyi Liang ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp index aa70b4ee4..9e0c0a2af 100644 --- a/examples/api/sets.cpp +++ b/examples/api/sets.cpp @@ -2,10 +2,10 @@ /*! \file sets.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz + ** Aina Niemetz, Kshitij Bansal ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp index cd2a60cb1..ad8df9ffa 100644 --- a/examples/api/strings.cpp +++ b/examples/api/strings.cpp @@ -2,10 +2,10 @@ /*! \file strings.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz + ** Aina Niemetz, Tianyi Liang, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/sygus-fun.cpp b/examples/api/sygus-fun.cpp index 1d1794a1a..b85529554 100644 --- a/examples/api/sygus-fun.cpp +++ b/examples/api/sygus-fun.cpp @@ -5,7 +5,7 @@ ** Abdalrhman Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/sygus-grammar.cpp b/examples/api/sygus-grammar.cpp index cc139d2e5..4cfbe84fa 100644 --- a/examples/api/sygus-grammar.cpp +++ b/examples/api/sygus-grammar.cpp @@ -5,7 +5,7 @@ ** Abdalrhman Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/api/sygus-inv.cpp b/examples/api/sygus-inv.cpp index 3638a78db..710265113 100644 --- a/examples/api/sygus-inv.cpp +++ b/examples/api/sygus-inv.cpp @@ -5,7 +5,7 @@ ** Abdalrhman Mohamed ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/hashsmt/CMakeLists.txt b/examples/hashsmt/CMakeLists.txt index 39e503a81..48eec6022 100644 --- a/examples/hashsmt/CMakeLists.txt +++ b/examples/hashsmt/CMakeLists.txt @@ -1,3 +1,13 @@ +##################### +## CMakeLists.txt +## Top contributors (to current version): +## Mathias Preiner, Aina Niemetz +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 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. +## if(Boost_FOUND) cvc4_add_example(sha1_inversion "sha1_inversion.cpp word.cpp" "hashsmt" diff --git a/examples/hashsmt/sha1.hpp b/examples/hashsmt/sha1.hpp index 0d7da9e8b..b1a0aec0e 100644 --- a/examples/hashsmt/sha1.hpp +++ b/examples/hashsmt/sha1.hpp @@ -5,7 +5,7 @@ ** Dejan Jovanovic, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/hashsmt/sha1_collision.cpp b/examples/hashsmt/sha1_collision.cpp index 1a89058a7..dcf46c01f 100644 --- a/examples/hashsmt/sha1_collision.cpp +++ b/examples/hashsmt/sha1_collision.cpp @@ -5,7 +5,7 @@ ** Dejan Jovanovic, Aina Niemetz, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp index e9d967b96..cd05f2eef 100644 --- a/examples/hashsmt/sha1_inversion.cpp +++ b/examples/hashsmt/sha1_inversion.cpp @@ -5,7 +5,7 @@ ** Dejan Jovanovic, Aina Niemetz, Andres Noetzli ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/hashsmt/word.cpp b/examples/hashsmt/word.cpp index f44dec6b8..641fd80fa 100644 --- a/examples/hashsmt/word.cpp +++ b/examples/hashsmt/word.cpp @@ -5,7 +5,7 @@ ** Dejan Jovanovic, Tim King, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/hashsmt/word.h b/examples/hashsmt/word.h index 9674a66ce..f5d33a9f4 100644 --- a/examples/hashsmt/word.h +++ b/examples/hashsmt/word.h @@ -5,7 +5,7 @@ ** Dejan Jovanovic ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/nra-translate/CMakeLists.txt b/examples/nra-translate/CMakeLists.txt index e83825e24..6c751bd5e 100644 --- a/examples/nra-translate/CMakeLists.txt +++ b/examples/nra-translate/CMakeLists.txt @@ -1,3 +1,13 @@ +##################### +## CMakeLists.txt +## Top contributors (to current version): +## Aina Niemetz, Mathias Preiner +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 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. +## set(EXAMPLES_NRA_TRANSLATE_BIN_DIR ${EXAMPLES_BIN_DIR}/nra-translate) set(CVC4_EXAMPLES_NRA_TRANSLATE diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp index 84cdfe6c4..033def34a 100644 --- a/examples/nra-translate/normalize.cpp +++ b/examples/nra-translate/normalize.cpp @@ -5,7 +5,7 @@ ** Dejan Jovanovic, Aina Niemetz, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp index ac325e57d..385d749d4 100644 --- a/examples/nra-translate/smt2info.cpp +++ b/examples/nra-translate/smt2info.cpp @@ -5,7 +5,7 @@ ** Dejan Jovanovic, Aina Niemetz, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp index f09a0abce..7607f370f 100644 --- a/examples/nra-translate/smt2todreal.cpp +++ b/examples/nra-translate/smt2todreal.cpp @@ -5,7 +5,7 @@ ** Dejan Jovanovic, Tim King, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp index 8094aae36..62b9a32d3 100644 --- a/examples/nra-translate/smt2toisat.cpp +++ b/examples/nra-translate/smt2toisat.cpp @@ -5,7 +5,7 @@ ** Dejan Jovanovic, Andrew Reynolds, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp index ccc1e558b..675ebe0d3 100644 --- a/examples/nra-translate/smt2tomathematica.cpp +++ b/examples/nra-translate/smt2tomathematica.cpp @@ -5,7 +5,7 @@ ** Dejan Jovanovic, Andrew Reynolds, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp index 9e42418f9..9af41d750 100644 --- a/examples/nra-translate/smt2toqepcad.cpp +++ b/examples/nra-translate/smt2toqepcad.cpp @@ -5,7 +5,7 @@ ** Dejan Jovanovic, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp index 0d84aec13..4eb2985c4 100644 --- a/examples/nra-translate/smt2toredlog.cpp +++ b/examples/nra-translate/smt2toredlog.cpp @@ -5,7 +5,7 @@ ** Dejan Jovanovic, Andrew Reynolds, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/sets-translate/CMakeLists.txt b/examples/sets-translate/CMakeLists.txt index 5487a2fcf..6859b444b 100644 --- a/examples/sets-translate/CMakeLists.txt +++ b/examples/sets-translate/CMakeLists.txt @@ -1,3 +1,13 @@ +##################### +## CMakeLists.txt +## Top contributors (to current version): +## Aina Niemetz, Mathias Preiner +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 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. +## if(Boost_FOUND) cvc4_add_example(sets2arrays "sets_translate.cpp" "sets-translate" diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp index 5db33892f..e9ddddf7f 100644 --- a/examples/sets-translate/sets_translate.cpp +++ b/examples/sets-translate/sets_translate.cpp @@ -2,10 +2,10 @@ /*! \file sets_translate.cpp ** \verbatim ** Top contributors (to current version): - ** Kshitij Bansal, Tim King, Aina Niemetz + ** Kshitij Bansal, Andres Noetzli, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp index 64c2b12c1..49a4f576e 100644 --- a/examples/simple_vc_cxx.cpp +++ b/examples/simple_vc_cxx.cpp @@ -2,10 +2,10 @@ /*! \file simple_vc_cxx.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Aina Niemetz + ** Andres Noetzli, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp index 4d5767ebb..7596b4771 100644 --- a/examples/simple_vc_quant_cxx.cpp +++ b/examples/simple_vc_quant_cxx.cpp @@ -2,10 +2,10 @@ /*! \file simple_vc_quant_cxx.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andres Noetzli, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** diff --git a/examples/translator.cpp b/examples/translator.cpp index a76eda4b8..a76fa7e1d 100644 --- a/examples/translator.cpp +++ b/examples/translator.cpp @@ -5,7 +5,7 @@ ** Morgan Deters, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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 ** |