diff options
Diffstat (limited to 'src/theory/bv')
23 files changed, 56 insertions, 102 deletions
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index 08bd3475a..a6cd0af29 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -3,11 +3,9 @@ ** \verbatim ** Original author: lianah ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): barrett, dejan, mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 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/src/theory/bv/bitblast_strategies.h b/src/theory/bv/bitblast_strategies.h index 5b53678dd..749a4c21f 100644 --- a/src/theory/bv/bitblast_strategies.h +++ b/src/theory/bv/bitblast_strategies.h @@ -3,11 +3,9 @@ ** \verbatim ** Original author: lianah ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): dejan, mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 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/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index 4aa52e24c..19f80bb44 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -2,12 +2,10 @@ /*! \file bitblaster.cpp ** \verbatim ** Original author: lianah - ** Major contributors: none - ** Minor contributors (to current version): none + ** Major contributors: dejan + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 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/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h index 3aee0ee1a..792f9d169 100644 --- a/src/theory/bv/bitblaster.h +++ b/src/theory/bv/bitblaster.h @@ -3,11 +3,9 @@ ** \verbatim ** Original author: lianah ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters, dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 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/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 98b809d85..4dbba0797 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -5,9 +5,7 @@ ** Major contributors: dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 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/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index e28ec188d..e113048b8 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -3,11 +3,9 @@ ** \verbatim ** Original author: dejan ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): lianah, mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 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/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index a2c77c9f5..3396d813b 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -2,12 +2,10 @@ /*! \file bv_subtheory_bitblast.h ** \verbatim ** Original author: dejan - ** Major contributors: none - ** Minor contributors (to current version): none + ** Major contributors: mdeters + ** Minor contributors (to current version): lianah ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 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/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp index 56a490747..17f3acdd1 100644 --- a/src/theory/bv/bv_subtheory_eq.cpp +++ b/src/theory/bv/bv_subtheory_eq.cpp @@ -1,13 +1,11 @@ /********************* */ /*! \file bv_subtheory_eq.cpp ** \verbatim - ** Original author: lianah - ** Major contributors: dejan - ** Minor contributors (to current version): none + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): lianah ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 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/src/theory/bv/bv_subtheory_eq.h b/src/theory/bv/bv_subtheory_eq.h index 24d9669db..91ad1599b 100644 --- a/src/theory/bv/bv_subtheory_eq.h +++ b/src/theory/bv/bv_subtheory_eq.h @@ -1,13 +1,11 @@ /********************* */ /*! \file bv_subtheory_eq.h ** \verbatim - ** Original author: lianah - ** Major contributors: dejan - ** Minor contributors (to current version): none + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): lianah, mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 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/src/theory/bv/cd_set_collection.h b/src/theory/bv/cd_set_collection.h index 1f15bffa8..e4bcbca47 100644 --- a/src/theory/bv/cd_set_collection.h +++ b/src/theory/bv/cd_set_collection.h @@ -5,9 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 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/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 1c5b08546..e82a2c75c 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -2,12 +2,10 @@ /*! \file theory_bv.cpp ** \verbatim ** Original author: dejan - ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Major contributors: mdeters, lianah + ** Minor contributors (to current version): barrett, ajreynol ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 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/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 36a542878..933fd8700 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -2,12 +2,10 @@ /*! \file theory_bv.h ** \verbatim ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): none + ** Major contributors: dejan, lianah + ** Minor contributors (to current version): barrett, ajreynol ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 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/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index ccc281d6f..f9650932e 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -3,11 +3,9 @@ ** \verbatim ** Original author: dejan ** Major contributors: lianah - ** Minor contributors (to current version): mdeters + ** Minor contributors (to current version): barrett, mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 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/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h index 005be88a8..d7d7c9670 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h +++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h @@ -3,11 +3,9 @@ ** \verbatim ** Original author: lianah ** Major contributors: barrett - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 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/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h index 2ccd0fbda..b44c72f74 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_core.h +++ b/src/theory/bv/theory_bv_rewrite_rules_core.h @@ -3,11 +3,9 @@ ** \verbatim ** Original author: dejan ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Minor contributors (to current version): mdeters, barrett, lianah ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 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/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 39e5bc599..6b3d0f770 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -2,12 +2,10 @@ /*! \file theory_bv_rewrite_rules_normalization.h ** \verbatim ** Original author: lianah - ** Major contributors: none - ** Minor contributors (to current version): none + ** Major contributors: barrett + ** Minor contributors (to current version): dejan, mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 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/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index 48df9492d..94983e03a 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -3,11 +3,9 @@ ** \verbatim ** Original author: lianah ** Major contributors: barrett - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 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/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 272b56ae9..a2fd9ee19 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -2,12 +2,10 @@ /*! \file theory_bv_rewrite_rules_simplification.h ** \verbatim ** Original author: lianah - ** Major contributors: none - ** Minor contributors (to current version): + ** Major contributors: barrett + ** Minor contributors (to current version): mdeters, dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 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/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index f41a64ac4..a8941aac2 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -2,12 +2,10 @@ /*! \file theory_bv_rewriter.cpp ** \verbatim ** Original author: dejan - ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Major contributors: lianah + ** Minor contributors (to current version): taking, mdeters, barrett ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 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/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 853ccdc32..c50a3bbe0 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -2,12 +2,10 @@ /*! \file theory_bv_rewriter.h ** \verbatim ** Original author: dejan - ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Major contributors: mdeters, lianah + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 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/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 8d8c31fa1..d34e45c63 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -2,12 +2,10 @@ /*! \file theory_bv_type_rules.h ** \verbatim ** Original author: dejan - ** Major contributors: mdeters, cconway + ** Major contributors: lianah, mdeters, cconway ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 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/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index d20107958..3f59be86d 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -2,12 +2,10 @@ /*! \file theory_bv_utils.h ** \verbatim ** Original author: dejan - ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Major contributors: mdeters, lianah + ** Minor contributors (to current version): barrett ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 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/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h index 2f8f713f8..ff9b8af7c 100644 --- a/src/theory/bv/type_enumerator.h +++ b/src/theory/bv/type_enumerator.h @@ -5,9 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** Copyright (c) 2009-2012 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** |