diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/arith_activity.h | 19 | ||||
-rw-r--r-- | src/theory/arith/arith_constants.h | 2 | ||||
-rw-r--r-- | src/theory/arith/arith_propagator.cpp | 19 | ||||
-rw-r--r-- | src/theory/arith/arith_propagator.h | 19 | ||||
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/arith_rewriter.h | 2 | ||||
-rw-r--r-- | src/theory/arith/arith_utilities.h | 2 | ||||
-rw-r--r-- | src/theory/arith/basic.h | 2 | ||||
-rw-r--r-- | src/theory/arith/delta_rational.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/delta_rational.h | 2 | ||||
-rw-r--r-- | src/theory/arith/ordered_bounds_list.h | 19 | ||||
-rw-r--r-- | src/theory/arith/partial_model.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/partial_model.h | 2 | ||||
-rw-r--r-- | src/theory/arith/slack.h | 2 | ||||
-rw-r--r-- | src/theory/arith/tableau.h | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_type_rules.h | 5 |
17 files changed, 91 insertions, 14 deletions
diff --git a/src/theory/arith/arith_activity.h b/src/theory/arith/arith_activity.h index 1dc0e900b..f347105e3 100644 --- a/src/theory/arith/arith_activity.h +++ b/src/theory/arith/arith_activity.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file arith_activity.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 "cvc4_private.h" diff --git a/src/theory/arith/arith_constants.h b/src/theory/arith/arith_constants.h index c34e86191..4a8fec56f 100644 --- a/src/theory/arith/arith_constants.h +++ b/src/theory/arith/arith_constants.h @@ -2,7 +2,7 @@ /*! \file arith_constants.h ** \verbatim ** Original author: taking - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/arith/arith_propagator.cpp b/src/theory/arith/arith_propagator.cpp index e40575054..c5068c9fb 100644 --- a/src/theory/arith/arith_propagator.cpp +++ b/src/theory/arith/arith_propagator.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file arith_propagator.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 "theory/arith/arith_propagator.h" #include "theory/arith/arith_utilities.h" diff --git a/src/theory/arith/arith_propagator.h b/src/theory/arith/arith_propagator.h index a623517fb..7ffcec747 100644 --- a/src/theory/arith/arith_propagator.h +++ b/src/theory/arith/arith_propagator.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file arith_propagator.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 "cvc4_private.h" diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 5c2a1e996..9cd65b2d9 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 704b57ca6..38c72d38d 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -2,7 +2,7 @@ /*! \file arith_rewriter.h ** \verbatim ** Original author: taking - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index dcfedb7e8..fa3356c60 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -2,7 +2,7 @@ /*! \file arith_utilities.h ** \verbatim ** Original author: taking - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/arith/basic.h b/src/theory/arith/basic.h index 963f2b969..11f0f71f0 100644 --- a/src/theory/arith/basic.h +++ b/src/theory/arith/basic.h @@ -2,7 +2,7 @@ /*! \file basic.h ** \verbatim ** Original author: taking - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp index 55e6b3dc9..f6a460fee 100644 --- a/src/theory/arith/delta_rational.cpp +++ b/src/theory/arith/delta_rational.cpp @@ -2,7 +2,7 @@ /*! \file delta_rational.cpp ** \verbatim ** Original author: taking - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index 78d5fb665..26212ec66 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -2,7 +2,7 @@ /*! \file delta_rational.h ** \verbatim ** Original author: taking - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/arith/ordered_bounds_list.h b/src/theory/arith/ordered_bounds_list.h index d21283afa..4393a382e 100644 --- a/src/theory/arith/ordered_bounds_list.h +++ b/src/theory/arith/ordered_bounds_list.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file ordered_bounds_list.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 "cvc4_private.h" diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index bd2d5d61e..18993c748 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index 44631fdef..bd945002e 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/arith/slack.h b/src/theory/arith/slack.h index 5cf391e64..87bf83e32 100644 --- a/src/theory/arith/slack.h +++ b/src/theory/arith/slack.h @@ -2,7 +2,7 @@ /*! \file slack.h ** \verbatim ** Original author: taking - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index f270dacb4..7f414db66 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index cb9dc85f7..5d719aa6f 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): dejan + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 9b22b14bb..9fb30bdb4 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -1,8 +1,9 @@ /********************* */ -/*! \file theory_arith_type_rules.cpp +/*! \file theory_arith_type_rules.h ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences |