diff options
Diffstat (limited to 'src/theory/quantifiers')
18 files changed, 55 insertions, 41 deletions
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 080550a16..28485a979 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -2,6 +2,8 @@ /*! \file bounded_integers.cpp ** \verbatim ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters + ** 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 diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h index 3da938d31..972bdb2ec 100644 --- a/src/theory/quantifiers/bounded_integers.h +++ b/src/theory/quantifiers/bounded_integers.h @@ -1,13 +1,16 @@ /********************* */ /*! \file bounded_integers.h -** \verbatim -** Original author: Andrew Reynolds -** 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 This class manages integer bounds for quantifiers + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters + ** 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 + ** + ** [[ Add lengthier description here ]] + ** \todo document this file **/ #include "cvc4_private.h" diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 42b49cf01..783f6284d 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -2,7 +2,7 @@ /*! \file candidate_generator.cpp ** \verbatim ** Original author: Morgan Deters - ** Major contributors: none + ** Major contributors: Andrew Reynolds ** 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 diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h index 402a29848..a87c24596 100644 --- a/src/theory/quantifiers/candidate_generator.h +++ b/src/theory/quantifiers/candidate_generator.h @@ -2,7 +2,7 @@ /*! \file candidate_generator.h ** \verbatim ** Original author: Morgan Deters - ** Major contributors: none + ** Major contributors: Andrew Reynolds ** 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 diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index fa4961352..bda124e96 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -2,8 +2,8 @@ /*! \file first_order_model.cpp ** \verbatim ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Major contributors: none + ** Minor contributors (to current version): Morgan Deters ** 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 diff --git a/src/theory/quantifiers/first_order_reasoning.cpp b/src/theory/quantifiers/first_order_reasoning.cpp index ebfb55f08..a696af3c2 100644 --- a/src/theory/quantifiers/first_order_reasoning.cpp +++ b/src/theory/quantifiers/first_order_reasoning.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file first_order_reasoning.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: none + ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters ** 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/src/theory/quantifiers/first_order_reasoning.h b/src/theory/quantifiers/first_order_reasoning.h index 5f217050c..6bc5c21c1 100644 --- a/src/theory/quantifiers/first_order_reasoning.h +++ b/src/theory/quantifiers/first_order_reasoning.h @@ -1,11 +1,11 @@ /********************* */ /*! \file first_order_reasoning.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: none + ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters ** 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/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index c22d903f9..2f32ec5e6 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -2,6 +2,8 @@ /*! \file full_model_check.cpp ** \verbatim ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters + ** 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 diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index abe05d3c7..606392831 100644 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -2,6 +2,8 @@ /*! \file full_model_check.h ** \verbatim ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters + ** 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 diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 4fe4072a3..6cc446e35 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Andrew Reynolds ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): Tim King ** 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 diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 821beeae0..c70c90b29 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Andrew Reynolds ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): Tim King ** 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 diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index b079ae75c..b079ae75c 100755..100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index c4345f828..c4345f828 100755..100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 107a99014..441ab029c 100755..100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -1,7 +1,9 @@ /********************* */ -/*! \file bounded_integers.cpp +/*! \file rewrite_engine.cpp ** \verbatim ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters + ** 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 diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index 2d9d751c2..a9a2f9b46 100755..100644 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -1,13 +1,16 @@ /********************* */ -/*! \file bounded_integers.h -** \verbatim -** Original author: Andrew Reynolds -** 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 This class manages integer bounds for quantifiers +/*! \file rewrite_engine.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters + ** 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 + ** + ** [[ Add lengthier description here ]] + ** \todo document this file **/ #include "cvc4_private.h" diff --git a/src/theory/quantifiers/symmetry_breaking.cpp b/src/theory/quantifiers/symmetry_breaking.cpp index 507a50838..66a3ac79f 100755..100644 --- a/src/theory/quantifiers/symmetry_breaking.cpp +++ b/src/theory/quantifiers/symmetry_breaking.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file symmetry_breaking.cpp ** \verbatim - ** Original author: ajreynol + ** Original author: Andrew Reynolds ** 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/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h index 7f6855fea..d7d9e0f6f 100755..100644 --- a/src/theory/quantifiers/symmetry_breaking.h +++ b/src/theory/quantifiers/symmetry_breaking.h @@ -1,11 +1,11 @@ /********************* */ /*! \file symmetry_breaking.h ** \verbatim - ** Original author: ajreynol + ** Original author: Andrew Reynolds ** 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 + ** 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/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 066282c2c..e72242fe9 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -2,8 +2,8 @@ /*! \file theory_quantifiers.cpp ** \verbatim ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Dejan Jovanovic, Andrew Reynolds + ** Major contributors: Andrew Reynolds + ** Minor contributors (to current version): Dejan Jovanovic ** 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 |