diff options
Diffstat (limited to 'src/theory')
26 files changed, 123 insertions, 24 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 diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 106d1a8da..ab72a0a8c 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -2,8 +2,8 @@ /*! \file theory_arrays.cpp ** \verbatim ** Original author: barrett - ** Major contributors: - ** Minor contributors (to current version): + ** 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 diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 69498cfb2..7bc57bcfb 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -2,7 +2,7 @@ /*! \file theory_arrays.h ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: barrett ** 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/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h index 8843a38c1..b947cee10 100644 --- a/src/theory/booleans/theory_bool_type_rules.h +++ b/src/theory/booleans/theory_bool_type_rules.h @@ -1,8 +1,9 @@ /********************* */ -/*! \file theory_bool_type_rules.cpp +/*! \file theory_bool_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 diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 0f4fda1a6..19d6e268b 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -1,8 +1,9 @@ /********************* */ -/*! \file builtin_type_rules.cpp +/*! \file theory_builtin_type_rules.h ** \verbatim ** Original author: dejan ** Major contributors: mdeters + ** Minor contributors (to current version): taking ** 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/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 7dd6c3e60..7aaae7349 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -2,7 +2,7 @@ /*! \file theory_bv_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) diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 5e83d3728..ba46e18e2 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -2,7 +2,7 @@ /*! \file theory.cpp ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: taking ** 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/theory_engine.h b/src/theory/theory_engine.h index 79eec4301..865fd83a9 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -2,7 +2,7 @@ /*! \file theory_engine.h ** \verbatim ** Original author: mdeters - ** Major contributors: taking, dejan + ** Major contributors: dejan, taking ** Minor contributors (to current version): cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index cd0b4ef66..a7f6e98ae 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file theory_test_utils.h + ** \verbatim + ** Original author: taking + ** 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 + ** 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_public.h" diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 419e3d078..e77de7d33 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -2,7 +2,8 @@ /*! \file theory_uf_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 |