summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/cnf_stream.cpp12
-rw-r--r--src/prop/cnf_stream.h12
-rw-r--r--src/prop/prop_engine.cpp12
-rw-r--r--src/prop/prop_engine.h12
-rw-r--r--src/prop/registrar.h12
-rw-r--r--src/prop/sat_solver.h12
-rw-r--r--src/prop/sat_solver_factory.cpp12
-rw-r--r--src/prop/sat_solver_factory.h12
-rw-r--r--src/prop/sat_solver_types.h12
-rw-r--r--src/prop/theory_proxy.cpp12
-rw-r--r--src/prop/theory_proxy.h12
11 files changed, 66 insertions, 66 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 7409c7222..aa1fc9587 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file cnf_stream.cpp
** \verbatim
- ** Original author: Tim King
- ** Major contributors: Morgan Deters, Dejan Jovanovic
- ** Minor contributors (to current version): Kshitij Bansal, Liana Hadarean, Christopher L. Conway, Andrew Reynolds
+ ** Top contributors (to current version):
+ ** Dejan Jovanovic, Liana Hadarean, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief A CNF converter that takes in asserts and has the side effect
** of given an equisatisfiable stream of assertions to PropEngine.
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 32e2205a1..cf9d519a7 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file cnf_stream.h
** \verbatim
- ** Original author: Tim King
- ** Major contributors: Morgan Deters, Dejan Jovanovic
- ** Minor contributors (to current version): Clark Barrett, Liana Hadarean, Christopher L. Conway, Andrew Reynolds
+ ** Top contributors (to current version):
+ ** Dejan Jovanovic, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief This class transforms a sequence of formulas into clauses.
**
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index ab9ee6588..54cf4c457 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file prop_engine.cpp
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): Clark Barrett, Liana Hadarean, Kshitij Bansal, Christopher L. Conway, Tim King
+ ** Top contributors (to current version):
+ ** Morgan Deters, Dejan Jovanovic, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief Implementation of the propositional engine of CVC4
**
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index c1c433b05..b9ce7ca7e 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file prop_engine.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): Clark Barrett, Liana Hadarean, Christopher L. Conway, Kshitij Bansal, Tim King
+ ** Top contributors (to current version):
+ ** Morgan Deters, Dejan Jovanovic, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief The PropEngine (propositional engine); main interface point
** between CVC4's SMT infrastructure and the SAT solver
diff --git a/src/prop/registrar.h b/src/prop/registrar.h
index b6dd021ab..bd8088921 100644
--- a/src/prop/registrar.h
+++ b/src/prop/registrar.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file registrar.h
** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: Tim King, Morgan Deters
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King, Liana Hadarean
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief Class to encapsulate preregistration duties
**
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 99e981220..92696ae25 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file sat_solver.h
** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters, Liana Hadarean
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Dejan Jovanovic, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief SAT Solver.
**
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index c131ca475..092ec72f2 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file sat_solver_factory.cpp
** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Tim King
- ** Minor contributors (to current version): Morgan Deters, Liana Hadarean
+ ** Top contributors (to current version):
+ ** Dejan Jovanovic, Tim King, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief SAT Solver creation facility.
**
diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h
index 6a3053a18..7cc23a8e8 100644
--- a/src/prop/sat_solver_factory.h
+++ b/src/prop/sat_solver_factory.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file sat_solver_factory.h
** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: none
- ** Minor contributors (to current version): Liana Hadarean, Morgan Deters
+ ** Top contributors (to current version):
+ ** Dejan Jovanovic, Tim King, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief SAT Solver.
**
diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h
index c47c2b67b..557f9af65 100644
--- a/src/prop/sat_solver_types.h
+++ b/src/prop/sat_solver_types.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file sat_solver_types.h
** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters, Liana Hadarean, Kshitij Bansal
+ ** Top contributors (to current version):
+ ** Dejan Jovanovic, Kshitij Bansal, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief This class transforms a sequence of formulas into clauses.
**
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 268a90cf6..4a4515eb9 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file theory_proxy.cpp
** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Kshitij Bansal, Morgan Deters
- ** Minor contributors (to current version): Clark Barrett, Christopher L. Conway, Tim King, Liana Hadarean
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King, Liana Hadarean
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief [[ Add one-line brief description here ]]
**
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 0e2b885d9..88c6ca94a 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file theory_proxy.h
** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Liana Hadarean, Kshitij Bansal, Morgan Deters
- ** Minor contributors (to current version): Christopher L. Conway, Tim King
+ ** Top contributors (to current version):
+ ** Tim King, Morgan Deters, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief SAT Solver.
**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback