diff options
Diffstat (limited to 'examples')
27 files changed, 241 insertions, 54 deletions
diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java index fcf1485af..07652a6fb 100644 --- a/examples/SimpleVC.java +++ b/examples/SimpleVC.java @@ -1,11 +1,11 @@ /********************* */ /*! \file SimpleVC.java ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/examples/SimpleVCCompat.java b/examples/SimpleVCCompat.java index 78ad8ae78..5719b75ce 100644 --- a/examples/SimpleVCCompat.java +++ b/examples/SimpleVCCompat.java @@ -1,11 +1,11 @@ /********************* */ /*! \file SimpleVCCompat.java ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp index a0c43142d..db886216a 100644 --- a/examples/api/bitvectors.cpp +++ b/examples/api/bitvectors.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file bitvectors.cpp ** \verbatim - ** Original author: lianah - ** Major contributors: none + ** Original author: Liana Hadarean <lianahady@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** 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 8363da46c..8e1d3320e 100644 --- a/examples/api/bitvectors_and_arrays.cpp +++ b/examples/api/bitvectors_and_arrays.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file bitvectors_and_arrays.cpp ** \verbatim - ** Original author: lianah - ** Major contributors: none + ** Original author: Liana Hadarean <lianahady@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** 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 6350b78fa..978f4ec53 100644 --- a/examples/api/combination.cpp +++ b/examples/api/combination.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file combination.cpp ** \verbatim - ** Original author: taking + ** Original author: Tim King <taking@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** 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 324883f46..ef6d565e2 100644 --- a/examples/api/helloworld.cpp +++ b/examples/api/helloworld.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file helloworld.cpp ** \verbatim - ** Original author: taking + ** Original author: Tim King <taking@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** 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 db236475d..3aff4b275 100644 --- a/examples/api/java/BitVectors.java +++ b/examples/api/java/BitVectors.java @@ -1,11 +1,11 @@ /********************* */ /*! \file BitVectors.java ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** 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 23009428c..27fe54c3f 100644 --- a/examples/api/java/BitVectorsAndArrays.java +++ b/examples/api/java/BitVectorsAndArrays.java @@ -1,11 +1,11 @@ /********************* */ /*! \file BitVectorsAndArrays.java ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** 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 0af8da640..df45f7327 100644 --- a/examples/api/java/Combination.java +++ b/examples/api/java/Combination.java @@ -1,11 +1,11 @@ /********************* */ /*! \file Combination.java ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** 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 33f6740c8..10a0f9753 100644 --- a/examples/api/java/HelloWorld.java +++ b/examples/api/java/HelloWorld.java @@ -1,11 +1,11 @@ /********************* */ /*! \file HelloWorld.java ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** 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 8b09bd688..fdefd12d3 100644 --- a/examples/api/java/LinearArith.java +++ b/examples/api/java/LinearArith.java @@ -1,11 +1,11 @@ /********************* */ /*! \file LinearArith.java ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** 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 3a5470914..8aafdea21 100644 --- a/examples/api/java/PipedInput.java +++ b/examples/api/java/PipedInput.java @@ -1,10 +1,10 @@ /********************* */ /*! \file PipedInput.java ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. + ** This file is part of the CVC4 project. ** Copyright (c) 2009-2013 New York University and The University of Iowa ** 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 960567d74..a21b6192f 100644 --- a/examples/api/linear_arith.cpp +++ b/examples/api/linear_arith.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file linear_arith.cpp ** \verbatim - ** Original author: taking + ** Original author: Tim King <taking@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/examples/hashsmt/sha1.hpp b/examples/hashsmt/sha1.hpp index a6ac011f1..dda6ecd7f 100644 --- a/examples/hashsmt/sha1.hpp +++ b/examples/hashsmt/sha1.hpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file sha1.hpp + ** \verbatim + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** 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 + **/ + // boost/uuid/sha1.hpp header file ----------------------------------------------// // Copyright 2007 Andy Tompkins. diff --git a/examples/hashsmt/sha1smt.cpp b/examples/hashsmt/sha1smt.cpp index 97b79a7d0..772575a4d 100644 --- a/examples/hashsmt/sha1smt.cpp +++ b/examples/hashsmt/sha1smt.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file sha1smt.cpp + ** \verbatim + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** 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 + **/ + /* * sha1smt.cpp * diff --git a/examples/hashsmt/word.cpp b/examples/hashsmt/word.cpp index c6cb8caf2..b663cb0fa 100644 --- a/examples/hashsmt/word.cpp +++ b/examples/hashsmt/word.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file word.cpp + ** \verbatim + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: none + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** 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 + **/ + /* * word.cpp * diff --git a/examples/hashsmt/word.h b/examples/hashsmt/word.h index e8d6053c0..054e75593 100644 --- a/examples/hashsmt/word.h +++ b/examples/hashsmt/word.h @@ -1,3 +1,20 @@ +/********************* */ +/*! \file word.h + ** \verbatim + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: none + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** 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 + **/ + /* * word.h * diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp index d38da7616..b9ed25f38 100644 --- a/examples/nra-translate/normalize.cpp +++ b/examples/nra-translate/normalize.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file normalize.cpp + ** \verbatim + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: none + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** 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 + **/ + #include <string> #include <iostream> #include <typeinfo> diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp index 0ccf9d669..632ff9c20 100644 --- a/examples/nra-translate/smt2info.cpp +++ b/examples/nra-translate/smt2info.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file smt2info.cpp + ** \verbatim + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: none + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** 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 + **/ + #include <string> #include <iostream> #include <typeinfo> diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp index 6fcf5c565..cf6383d13 100644 --- a/examples/nra-translate/smt2todreal.cpp +++ b/examples/nra-translate/smt2todreal.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file smt2todreal.cpp + ** \verbatim + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: none + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** 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 + **/ + #include <string> #include <iostream> #include <typeinfo> diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp index b44339309..3941442e7 100644 --- a/examples/nra-translate/smt2toisat.cpp +++ b/examples/nra-translate/smt2toisat.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file smt2toisat.cpp + ** \verbatim + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: none + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** 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 + **/ + #include <string> #include <iostream> #include <typeinfo> diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp index bfee27310..a53f53609 100644 --- a/examples/nra-translate/smt2tomathematica.cpp +++ b/examples/nra-translate/smt2tomathematica.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file smt2tomathematica.cpp + ** \verbatim + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: none + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** 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 + **/ + #include <string> #include <iostream> #include <typeinfo> diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp index fc43c4c7b..c4aeb8f6a 100644 --- a/examples/nra-translate/smt2toqepcad.cpp +++ b/examples/nra-translate/smt2toqepcad.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file smt2toqepcad.cpp + ** \verbatim + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: none + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** 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 + **/ + #include <string> #include <iostream> #include <typeinfo> diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp index b2717c157..105585171 100644 --- a/examples/nra-translate/smt2toredlog.cpp +++ b/examples/nra-translate/smt2toredlog.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file smt2toredlog.cpp + ** \verbatim + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: none + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** 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 + **/ + #include <string> #include <iostream> #include <typeinfo> diff --git a/examples/simple_vc_compat_c.c b/examples/simple_vc_compat_c.c index 0980e8dfa..49c0016bc 100644 --- a/examples/simple_vc_compat_c.c +++ b/examples/simple_vc_compat_c.c @@ -1,11 +1,11 @@ /********************* */ /*! \file simple_vc_compat_c.c ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/examples/simple_vc_compat_cxx.cpp b/examples/simple_vc_compat_cxx.cpp index f0b378b21..9974d3a92 100644 --- a/examples/simple_vc_compat_cxx.cpp +++ b/examples/simple_vc_compat_cxx.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file simple_vc_compat_cxx.cpp ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** 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 f016c5306..097c0e1cf 100644 --- a/examples/simple_vc_cxx.cpp +++ b/examples/simple_vc_cxx.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file simple_vc_cxx.cpp ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** |