diff options
Diffstat (limited to 'src/theory/arith')
151 files changed, 275 insertions, 273 deletions
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index 49cf9fe0a..152146cdf 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Aina Niemetz, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h index 2c7400a35..58e115b81 100644 --- a/src/theory/arith/approx_simplex.h +++ b/src/theory/arith/approx_simplex.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 @@ -15,7 +15,6 @@ ** \todo document this file **/ - #include "cvc4_private.h" #pragma once diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index 5fb11d77f..fa6fd108c 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Aina Niemetz, Piotr Trojanek ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h index 5aa22d8e5..e1e27884d 100644 --- a/src/theory/arith/arith_ite_utils.h +++ b/src/theory/arith/arith_ite_utils.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Mathias Preiner, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/arith_msum.cpp b/src/theory/arith/arith_msum.cpp index a2b3d41d5..83b8b67c2 100644 --- a/src/theory/arith/arith_msum.cpp +++ b/src/theory/arith/arith_msum.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/arith_msum.h b/src/theory/arith/arith_msum.h index bdc0d85de..f7470d4e0 100644 --- a/src/theory/arith/arith_msum.h +++ b/src/theory/arith/arith_msum.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp index f4f9df43c..0c1923448 100644 --- a/src/theory/arith/arith_preprocess.cpp +++ b/src/theory/arith/arith_preprocess.cpp @@ -2,9 +2,9 @@ /*! \file arith_preprocess.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h index e1f43db1b..69cc02bb9 100644 --- a/src/theory/arith/arith_preprocess.h +++ b/src/theory/arith/arith_preprocess.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index a990b426f..170e2d0f4 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 396395e1f..9bf88dfe6 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Dejan Jovanovic, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/arith_state.cpp b/src/theory/arith/arith_state.cpp index c2533723a..1c41ecf81 100644 --- a/src/theory/arith/arith_state.cpp +++ b/src/theory/arith/arith_state.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/arith_state.h b/src/theory/arith/arith_state.h index b3c299433..ffb4a2abc 100644 --- a/src/theory/arith/arith_state.h +++ b/src/theory/arith/arith_state.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index f4016d032..b7169df1f 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index 9c78942b1..2b74e6005 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Dejan Jovanovic, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp index fc34d2a6d..f9051328c 100644 --- a/src/theory/arith/arith_utilities.cpp +++ b/src/theory/arith/arith_utilities.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Alex Ozdemir, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 55bbe67cc..e4d6bd0ee 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/arithvar.cpp b/src/theory/arith/arithvar.cpp index 7dab58531..59253e87c 100644 --- a/src/theory/arith/arithvar.cpp +++ b/src/theory/arith/arithvar.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 @@ -15,7 +15,6 @@ ** \todo document this file **/ - #include "theory/arith/arithvar.h" #include <limits> #include <set> diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h index 815b70d6d..dd5ea70d9 100644 --- a/src/theory/arith/arithvar.h +++ b/src/theory/arith/arithvar.h @@ -4,19 +4,19 @@ ** Top contributors (to current version): ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 Defines ArithVar which is the internal representation of variables in arithmetic + ** \brief Defines ArithVar which is the internal representation of variables in + ** arithmetic ** ** This defines ArithVar which is the internal representation of variables in ** arithmetic. This is a typedef from Index to ArithVar. ** This file also provides utilities for ArithVars. **/ - #include "cvc4_private.h" #pragma once diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h index a73146042..f01b0c7ac 100644 --- a/src/theory/arith/arithvar_node_map.h +++ b/src/theory/arith/arithvar_node_map.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp index 61715df9b..efcb96325 100644 --- a/src/theory/arith/attempt_solution_simplex.cpp +++ b/src/theory/arith/attempt_solution_simplex.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Aina Niemetz, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h index b41b634c3..b7266a1e2 100644 --- a/src/theory/arith/attempt_solution_simplex.h +++ b/src/theory/arith/attempt_solution_simplex.h @@ -4,15 +4,16 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 is an implementation of the Simplex Module for the Simplex for DPLL(T) - ** decision procedure. + ** \brief This is an implementation of the Simplex Module for the Simplex for + ** DPLL(T) decision procedure. ** - ** This implements the Simplex module for the Simpelx for DPLL(T) decision procedure. + ** This implements the Simplex module for the Simpelx for DPLL(T) decision + ** procedure. ** See the Simplex for DPLL(T) technical report for more background.(citation?) ** This shares with the theory a Tableau, and a PartialModel that: ** - satisfies the equalities in the Tableau, and @@ -21,26 +22,27 @@ ** Further, we require being told when a basic variable updates its value. ** ** During the Simplex search we maintain a queue of variables. - ** The queue is required to contain all of the basic variables that voilate their bounds. + ** The queue is required to contain all of the basic variables that voilate + ** their bounds. ** As elimination from the queue is more efficient to be done lazily, - ** we do not maintain that the queue of variables needs to be only basic variables or only - ** variables that satisfy their bounds. + ** we do not maintain that the queue of variables needs to be only basic + ** variables or only variables that satisfy their bounds. ** ** The simplex procedure roughly follows Alberto's thesis. (citation?) - ** There is one round of selecting using a heuristic pivoting rule. (See PreferenceFunction - ** Documentation for the available options.) - ** The non-basic variable is the one that appears in the fewest pivots. (Bruno says that - ** Leonardo invented this first.) + ** There is one round of selecting using a heuristic pivoting rule. + ** (See PreferenceFunction Documentation for the available options.) + ** The non-basic variable is the one that appears in the fewest pivots. + ** (Bruno says that Leonardo invented this first.) ** After this, Bland's pivot rule is invoked. ** ** During this proccess, we periodically inspect the queue of variables to ** 1) remove now extraneous extries, - ** 2) detect conflicts that are "waiting" on the queue but may not be detected by the - ** current queue heuristics, and + ** 2) detect conflicts that are "waiting" on the queue but may not be detected + ** by the current queue heuristics, and ** 3) detect multiple conflicts. ** - ** Conflicts are greedily slackened to use the weakest bounds that still produce the - ** conflict. + ** Conflicts are greedily slackened to use the weakest bounds that still + ** produce the conflict. ** ** Extra things tracked atm: (Subject to change at Tim's whims) ** - A superset of all of the newly pivoted variables. @@ -48,7 +50,6 @@ ** These are theory valid and are currently turned into lemmas **/ - #include "cvc4_private.h" #pragma once diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h index d1044f36b..cb9053669 100644 --- a/src/theory/arith/bound_counts.h +++ b/src/theory/arith/bound_counts.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/bound_inference.cpp b/src/theory/arith/bound_inference.cpp index 29be87d7b..d2adc94af 100644 --- a/src/theory/arith/bound_inference.cpp +++ b/src/theory/arith/bound_inference.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/bound_inference.h b/src/theory/arith/bound_inference.h index 9d78d88c9..dc32ff179 100644 --- a/src/theory/arith/bound_inference.h +++ b/src/theory/arith/bound_inference.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp index e1cb1c3ca..84bfafcc8 100644 --- a/src/theory/arith/callbacks.cpp +++ b/src/theory/arith/callbacks.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Haniel Barbosa, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h index 796a93ea4..9fbe3b90f 100644 --- a/src/theory/arith/callbacks.h +++ b/src/theory/arith/callbacks.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Mathias Preiner, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 @@ -15,7 +15,6 @@ ** \todo document this file **/ - #pragma once #include "expr/node.h" diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 03dc28d6a..636cebe5f 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Alex Ozdemir, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 8b4d49f90..f2aef815f 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Alex Ozdemir, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 02580083b..70106b14c 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Alex Ozdemir, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 70b2cad20..6a73d69d2 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -4,12 +4,13 @@ ** Top contributors (to current version): ** Tim King, Alex Ozdemir, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 Defines Constraint and ConstraintDatabase which is the internal representation of variables in arithmetic + ** \brief Defines Constraint and ConstraintDatabase which is the internal + ** representation of variables in arithmetic ** ** This file defines Constraint and ConstraintDatabase. ** A Constraint is the internal representation of literals in TheoryArithmetic. @@ -36,15 +37,16 @@ ** - Whether a constraint, be be used in explanations sent to the context ** ** Looking up constraints: - ** - All of the Constraints with associated nodes in the ConstraintDatabase can - ** be accessed via a single hashtable lookup until the Constraint is removed. + ** - All of the Constraints with associated nodes in the ConstraintDatabase + ** can be accessed via a single hashtable lookup until the Constraint is + ** removed. ** - Nodes that have not been associated to a constraints can be ** inserted/associated to existing nodes in O(log n) time. ** ** Implications: ** - A Constraint can be used to find unate implications. - ** - A unate implication is an implication based purely on the ArithVar matching - ** and the DeltaRational value. + ** - A unate implication is an implication based purely on the ArithVar + ** matching and the DeltaRational value. ** (implies (<= x c) (<= x d)) given c <= d ** - This is done using the iterator into the sorted set of constraints. ** - Given a tight constraint and previous tightest constraint, this will @@ -58,16 +60,17 @@ ** Internals: ** - Constraints are pointers to ConstraintValues. ** - Undefined Constraints are NullConstraint. - ** ** Assumption vs. Assertion: ** - An assertion is anything on the theory d_fact queue. ** This includes any thing propagated and returned to the fact queue. - ** These can be used in external conflicts and propagations of earlier proofs. + ** These can be used in external conflicts and propagations of earlier + ** proofs. ** - An assumption is anything on the theory d_fact queue that has no further ** explanation i.e. this theory did not propagate it. ** - To set something an assumption, first set it as being as assertion. - ** - Internal assumptions have no explanations and must be regressed out of the proof. + ** - Internal assumptions have no explanations and must be regressed out of the + ** proof. **/ #include "cvc4_private.h" diff --git a/src/theory/arith/constraint_forward.h b/src/theory/arith/constraint_forward.h index 515c5cfc0..9a42b8a97 100644 --- a/src/theory/arith/constraint_forward.h +++ b/src/theory/arith/constraint_forward.h @@ -4,16 +4,18 @@ ** Top contributors (to current version): ** Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 Forward declarations of the ConstraintValue and ConstraintDatabase classes. + ** \brief Forward declarations of the ConstraintValue and ConstraintDatabase + ** classes. ** - ** This is the forward declarations of the ConstraintValue and ConstraintDatabase - ** and the typedef for Constraint. This is used to break circular dependencies and - ** minimize interaction between header files. + ** This is the forward declarations of the ConstraintValue and + ** ConstraintDatabase and the typedef for Constraint. + ** This is used to break circular dependencies and minimize interaction + ** between header files. **/ #ifndef CVC4__THEORY__ARITH__CONSTRAINT_FORWARD_H diff --git a/src/theory/arith/cut_log.cpp b/src/theory/arith/cut_log.cpp index 73c589599..89165b45e 100644 --- a/src/theory/arith/cut_log.cpp +++ b/src/theory/arith/cut_log.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h index 12d8da991..f6f974fca 100644 --- a/src/theory/arith/cut_log.h +++ b/src/theory/arith/cut_log.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters, Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 @@ -15,7 +15,6 @@ ** \todo document this file **/ - #include "cvc4_private.h" #pragma once diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp index 8107136c3..b7f641338 100644 --- a/src/theory/arith/delta_rational.cpp +++ b/src/theory/arith/delta_rational.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 @@ -15,7 +15,6 @@ ** \todo document this file **/ - #include "theory/arith/delta_rational.h" #include <sstream> diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index 41a9bddd3..ce0a2cffd 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 15faf58bf..2c06967c4 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Mathias Preiner, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index 186816f1e..571c64a78 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp index 5d4bc9b1e..3784ec79b 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Aina Niemetz, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/dual_simplex.h b/src/theory/arith/dual_simplex.h index f87b4e9c1..174a91c75 100644 --- a/src/theory/arith/dual_simplex.h +++ b/src/theory/arith/dual_simplex.h @@ -4,15 +4,16 @@ ** Top contributors (to current version): ** Tim King, Mathias Preiner, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 is an implementation of the Simplex Module for the Simplex for DPLL(T) - ** decision procedure. + ** \brief This is an implementation of the Simplex Module for the Simplex for + ** DPLL(T) decision procedure. ** - ** This implements the Simplex module for the Simpelx for DPLL(T) decision procedure. + ** This implements the Simplex module for the Simpelx for DPLL(T) decision + ** procedure. ** See the Simplex for DPLL(T) technical report for more background.(citation?) ** This shares with the theory a Tableau, and a PartialModel that: ** - satisfies the equalities in the Tableau, and @@ -21,26 +22,27 @@ ** Further, we require being told when a basic variable updates its value. ** ** During the Simplex search we maintain a queue of variables. - ** The queue is required to contain all of the basic variables that voilate their bounds. + ** The queue is required to contain all of the basic variables that voilate + ** their bounds. ** As elimination from the queue is more efficient to be done lazily, - ** we do not maintain that the queue of variables needs to be only basic variables or only - ** variables that satisfy their bounds. + ** we do not maintain that the queue of variables needs to be only basic + ** variables or only variables that satisfy their bounds. ** ** The simplex procedure roughly follows Alberto's thesis. (citation?) - ** There is one round of selecting using a heuristic pivoting rule. (See PreferenceFunction - ** Documentation for the available options.) - ** The non-basic variable is the one that appears in the fewest pivots. (Bruno says that - ** Leonardo invented this first.) + ** There is one round of selecting using a heuristic pivoting rule. + ** (See PreferenceFunction Documentation for the available options.) + ** The non-basic variable is the one that appears in the fewest pivots. + ** (Bruno says that Leonardo invented this first.) ** After this, Bland's pivot rule is invoked. ** ** During this proccess, we periodically inspect the queue of variables to ** 1) remove now extraneous extries, - ** 2) detect conflicts that are "waiting" on the queue but may not be detected by the - ** current queue heuristics, and + ** 2) detect conflicts that are "waiting" on the queue but may not be detected + ** by the current queue heuristics, and ** 3) detect multiple conflicts. ** - ** Conflicts are greedily slackened to use the weakest bounds that still produce the - ** conflict. + ** Conflicts are greedily slackened to use the weakest bounds that still + ** produce the conflict. ** ** Extra things tracked atm: (Subject to change at Tim's whims) ** - A superset of all of the newly pivoted variables. diff --git a/src/theory/arith/error_set.cpp b/src/theory/arith/error_set.cpp index 8e98f2d8d..9c88ccfad 100644 --- a/src/theory/arith/error_set.cpp +++ b/src/theory/arith/error_set.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h index 568be40d5..34d695f8a 100644 --- a/src/theory/arith/error_set.h +++ b/src/theory/arith/error_set.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Mathias Preiner, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 @@ -15,7 +15,6 @@ ** \todo document this file **/ - #include "cvc4_private.h" #pragma once diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index 8cb249c46..c85c3df2a 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Aina Niemetz, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h index e001d98d4..658f7c23e 100644 --- a/src/theory/arith/fc_simplex.h +++ b/src/theory/arith/fc_simplex.h @@ -4,15 +4,16 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 is an implementation of the Simplex Module for the Simplex for DPLL(T) - ** decision procedure. + ** \brief This is an implementation of the Simplex Module for the Simplex for + ** DPLL(T)decision procedure. ** - ** This implements the Simplex module for the Simpelx for DPLL(T) decision procedure. + ** This implements the Simplex module for the Simpelx for DPLL(T) decision + ** procedure. ** See the Simplex for DPLL(T) technical report for more background.(citation?) ** This shares with the theory a Tableau, and a PartialModel that: ** - satisfies the equalities in the Tableau, and @@ -21,26 +22,27 @@ ** Further, we require being told when a basic variable updates its value. ** ** During the Simplex search we maintain a queue of variables. - ** The queue is required to contain all of the basic variables that voilate their bounds. + ** The queue is required to contain all of the basic variables that voilate + ** their bounds. ** As elimination from the queue is more efficient to be done lazily, - ** we do not maintain that the queue of variables needs to be only basic variables or only - ** variables that satisfy their bounds. + ** we do not maintain that the queue of variables needs to be only basic + ** variables or only variables that satisfy their bounds. ** ** The simplex procedure roughly follows Alberto's thesis. (citation?) - ** There is one round of selecting using a heuristic pivoting rule. (See PreferenceFunction - ** Documentation for the available options.) - ** The non-basic variable is the one that appears in the fewest pivots. (Bruno says that - ** Leonardo invented this first.) + ** There is one round of selecting using a heuristic pivoting rule. + ** (See PreferenceFunction Documentation for the available options.) + ** The non-basic variable is the one that appears in the fewest pivots. + ** (Bruno says that Leonardo invented this first.) ** After this, Bland's pivot rule is invoked. ** ** During this proccess, we periodically inspect the queue of variables to ** 1) remove now extraneous extries, - ** 2) detect conflicts that are "waiting" on the queue but may not be detected by the - ** current queue heuristics, and + ** 2) detect conflicts that are "waiting" on the queue but may not be detected + ** by the current queue heuristics, and ** 3) detect multiple conflicts. ** - ** Conflicts are greedily slackened to use the weakest bounds that still produce the - ** conflict. + ** Conflicts are greedily slackened to use the weakest bounds that still + ** produce the conflict. ** ** Extra things tracked atm: (Subject to change at Tim's whims) ** - A superset of all of the newly pivoted variables. diff --git a/src/theory/arith/infer_bounds.cpp b/src/theory/arith/infer_bounds.cpp index ec80ca0d4..0475e2472 100644 --- a/src/theory/arith/infer_bounds.cpp +++ b/src/theory/arith/infer_bounds.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/infer_bounds.h b/src/theory/arith/infer_bounds.h index bfed35252..e1eb786d0 100644 --- a/src/theory/arith/infer_bounds.h +++ b/src/theory/arith/infer_bounds.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp index c2001686b..c4281f0bd 100644 --- a/src/theory/arith/inference_manager.cpp +++ b/src/theory/arith/inference_manager.cpp @@ -2,9 +2,9 @@ /*! \file inference_manager.cpp ** \verbatim ** Top contributors (to current version): - ** Gereon Kremer, Mathias Preiner + ** Gereon Kremer, Makai Mann, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h index f033c4a5c..80cb62201 100644 --- a/src/theory/arith/inference_manager.h +++ b/src/theory/arith/inference_manager.h @@ -2,9 +2,9 @@ /*! \file inference_manager.h ** \verbatim ** Top contributors (to current version): - ** Gereon Kremer + ** Gereon Kremer, Makai Mann ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index 765061e8d..943f3216e 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Mathias Preiner, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index beac70f64..3cfbfe5db 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -4,12 +4,13 @@ ** Top contributors (to current version): ** Tim King, Mathias Preiner, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 module maintains the relationship between a Tableau and PartialModel. + ** \brief This module maintains the relationship between a Tableau and + ** PartialModel. ** ** This shares with the theory a Tableau, and a PartialModel that: ** - satisfies the equalities in the Tableau, and @@ -24,7 +25,6 @@ ** using both the Tableau and PartialModel. **/ - #include "cvc4_private.h" #pragma once diff --git a/src/theory/arith/matrix.cpp b/src/theory/arith/matrix.cpp index 7b6d478fa..fb8c02379 100644 --- a/src/theory/arith/matrix.cpp +++ b/src/theory/arith/matrix.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 @@ -15,7 +15,6 @@ ** \todo document this file **/ - #include "theory/arith/matrix.h" using namespace std; diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h index ab9122755..09fdc2e91 100644 --- a/src/theory/arith/matrix.h +++ b/src/theory/arith/matrix.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Mathias Preiner, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp index 04165c289..c4ecfbbfa 100644 --- a/src/theory/arith/nl/cad/cdcac.cpp +++ b/src/theory/arith/nl/cad/cdcac.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h index ada6286f7..15230d14c 100644 --- a/src/theory/arith/nl/cad/cdcac.h +++ b/src/theory/arith/nl/cad/cdcac.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/cad/cdcac_utils.cpp b/src/theory/arith/nl/cad/cdcac_utils.cpp index e58ba3730..24bad8d60 100644 --- a/src/theory/arith/nl/cad/cdcac_utils.cpp +++ b/src/theory/arith/nl/cad/cdcac_utils.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/cad/cdcac_utils.h b/src/theory/arith/nl/cad/cdcac_utils.h index 153341c7e..dad9bbd7a 100644 --- a/src/theory/arith/nl/cad/cdcac_utils.h +++ b/src/theory/arith/nl/cad/cdcac_utils.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/cad/constraints.cpp b/src/theory/arith/nl/cad/constraints.cpp index f0a214919..028a61833 100644 --- a/src/theory/arith/nl/cad/constraints.cpp +++ b/src/theory/arith/nl/cad/constraints.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/cad/constraints.h b/src/theory/arith/nl/cad/constraints.h index 10079e9bb..f0a3fbe25 100644 --- a/src/theory/arith/nl/cad/constraints.h +++ b/src/theory/arith/nl/cad/constraints.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/cad/projections.cpp b/src/theory/arith/nl/cad/projections.cpp index 8d33bf794..5d72f5a2e 100644 --- a/src/theory/arith/nl/cad/projections.cpp +++ b/src/theory/arith/nl/cad/projections.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/cad/projections.h b/src/theory/arith/nl/cad/projections.h index 3820716c2..9302cb7f2 100644 --- a/src/theory/arith/nl/cad/projections.h +++ b/src/theory/arith/nl/cad/projections.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/cad/proof_checker.cpp b/src/theory/arith/nl/cad/proof_checker.cpp index 24c4b813c..45c43e2aa 100644 --- a/src/theory/arith/nl/cad/proof_checker.cpp +++ b/src/theory/arith/nl/cad/proof_checker.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/cad/proof_checker.h b/src/theory/arith/nl/cad/proof_checker.h index d10ce2e1b..f13e6f4a3 100644 --- a/src/theory/arith/nl/cad/proof_checker.h +++ b/src/theory/arith/nl/cad/proof_checker.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp index ebf1ab25e..62d3c03ff 100644 --- a/src/theory/arith/nl/cad/proof_generator.cpp +++ b/src/theory/arith/nl/cad/proof_generator.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h index 055de98fe..72f0f766b 100644 --- a/src/theory/arith/nl/cad/proof_generator.h +++ b/src/theory/arith/nl/cad/proof_generator.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/cad/variable_ordering.cpp b/src/theory/arith/nl/cad/variable_ordering.cpp index 4897ed6b7..958191fe1 100644 --- a/src/theory/arith/nl/cad/variable_ordering.cpp +++ b/src/theory/arith/nl/cad/variable_ordering.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/cad/variable_ordering.h b/src/theory/arith/nl/cad/variable_ordering.h index 4954e0e46..43e85b3cb 100644 --- a/src/theory/arith/nl/cad/variable_ordering.h +++ b/src/theory/arith/nl/cad/variable_ordering.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index efc5c465a..c72c9d48d 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h index 7d0346eab..3a7d5159a 100644 --- a/src/theory/arith/nl/cad_solver.h +++ b/src/theory/arith/nl/cad_solver.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/ext/constraint.cpp b/src/theory/arith/nl/ext/constraint.cpp index f395ee2d4..452368640 100644 --- a/src/theory/arith/nl/ext/constraint.cpp +++ b/src/theory/arith/nl/ext/constraint.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/ext/constraint.h b/src/theory/arith/nl/ext/constraint.h index 7b7c604bf..2f439f65e 100644 --- a/src/theory/arith/nl/ext/constraint.h +++ b/src/theory/arith/nl/ext/constraint.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp index 7e77efb16..c7841748f 100644 --- a/src/theory/arith/nl/ext/ext_state.cpp +++ b/src/theory/arith/nl/ext/ext_state.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Gereon Kremer, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h index 285189ccc..46ccaeb14 100644 --- a/src/theory/arith/nl/ext/ext_state.h +++ b/src/theory/arith/nl/ext/ext_state.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp index 09cfd7410..f64fc8feb 100644 --- a/src/theory/arith/nl/ext/factoring_check.cpp +++ b/src/theory/arith/nl/ext/factoring_check.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Gereon Kremer, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/ext/factoring_check.h b/src/theory/arith/nl/ext/factoring_check.h index fa0f8239a..c8d27ec27 100644 --- a/src/theory/arith/nl/ext/factoring_check.h +++ b/src/theory/arith/nl/ext/factoring_check.h @@ -2,9 +2,9 @@ /*! \file factoring_check.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer + ** Gereon Kremer, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/ext/monomial.cpp b/src/theory/arith/nl/ext/monomial.cpp index 0b46cc88e..a0d388dca 100644 --- a/src/theory/arith/nl/ext/monomial.cpp +++ b/src/theory/arith/nl/ext/monomial.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/ext/monomial.h b/src/theory/arith/nl/ext/monomial.h index a1cc8d7ff..19f855233 100644 --- a/src/theory/arith/nl/ext/monomial.h +++ b/src/theory/arith/nl/ext/monomial.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp index ad6fd36b8..2c25a6e29 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp +++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Gereon Kremer, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.h b/src/theory/arith/nl/ext/monomial_bounds_check.h index 9977d7534..103e2725f 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.h +++ b/src/theory/arith/nl/ext/monomial_bounds_check.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Gereon Kremer, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp index d970bd95d..3f62d0afb 100644 --- a/src/theory/arith/nl/ext/monomial_check.cpp +++ b/src/theory/arith/nl/ext/monomial_check.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Gereon Kremer, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h index 05908ecc7..b964f00a4 100644 --- a/src/theory/arith/nl/ext/monomial_check.h +++ b/src/theory/arith/nl/ext/monomial_check.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Gereon Kremer, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/ext/proof_checker.cpp b/src/theory/arith/nl/ext/proof_checker.cpp index e3e26cb65..e88e08aaf 100644 --- a/src/theory/arith/nl/ext/proof_checker.cpp +++ b/src/theory/arith/nl/ext/proof_checker.cpp @@ -2,9 +2,9 @@ /*! \file proof_checker.cpp ** \verbatim ** Top contributors (to current version): - ** Gereon Kremer + ** Gereon Kremer, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/ext/proof_checker.h b/src/theory/arith/nl/ext/proof_checker.h index 88df46110..d53b674b2 100644 --- a/src/theory/arith/nl/ext/proof_checker.h +++ b/src/theory/arith/nl/ext/proof_checker.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp index 5bcdb801d..09954bf19 100644 --- a/src/theory/arith/nl/ext/split_zero_check.cpp +++ b/src/theory/arith/nl/ext/split_zero_check.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/ext/split_zero_check.h b/src/theory/arith/nl/ext/split_zero_check.h index 0e7ad0999..bee2fe405 100644 --- a/src/theory/arith/nl/ext/split_zero_check.h +++ b/src/theory/arith/nl/ext/split_zero_check.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp index 2d04c2b5c..254151283 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.cpp +++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp @@ -2,9 +2,9 @@ /*! \file tangent_plane_check.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer, Tim King + ** Gereon Kremer, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/ext/tangent_plane_check.h b/src/theory/arith/nl/ext/tangent_plane_check.h index 84b6c0ba4..e0656789b 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.h +++ b/src/theory/arith/nl/ext/tangent_plane_check.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/ext_theory_callback.cpp b/src/theory/arith/nl/ext_theory_callback.cpp index ee12d17d6..214d2a51a 100644 --- a/src/theory/arith/nl/ext_theory_callback.cpp +++ b/src/theory/arith/nl/ext_theory_callback.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Tianyi Liang ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/ext_theory_callback.h b/src/theory/arith/nl/ext_theory_callback.h index 66c1ebc94..f1ad3df20 100644 --- a/src/theory/arith/nl/ext_theory_callback.h +++ b/src/theory/arith/nl/ext_theory_callback.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index 5e34aebc7..7272bb6e3 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -2,9 +2,9 @@ /*! \file iand_solver.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Yoni Zohar, Gereon Kremer + ** Andrew Reynolds, Makai Mann, Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h index 044a37abc..e484252f2 100644 --- a/src/theory/arith/nl/iand_solver.h +++ b/src/theory/arith/nl/iand_solver.h @@ -2,9 +2,9 @@ /*! \file iand_solver.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Yoni Zohar, Gereon Kremer + ** Andrew Reynolds, Makai Mann, Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp index 652f0eec7..cb3a03aed 100644 --- a/src/theory/arith/nl/iand_utils.cpp +++ b/src/theory/arith/nl/iand_utils.cpp @@ -2,9 +2,9 @@ /*! \file iand_utils.cpp ** \verbatim ** Top contributors (to current version): - ** Yoni Zohar + ** Yoni Zohar, Makai Mann, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/iand_utils.h b/src/theory/arith/nl/iand_utils.h index 4c1de0196..15ccab231 100644 --- a/src/theory/arith/nl/iand_utils.h +++ b/src/theory/arith/nl/iand_utils.h @@ -2,9 +2,9 @@ /*! \file iand_utils.h ** \verbatim ** Top contributors (to current version): - ** Yoni Zohar + ** Yoni Zohar, Makai Mann, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/icp/candidate.cpp b/src/theory/arith/nl/icp/candidate.cpp index 5dc2443d0..df894ee12 100644 --- a/src/theory/arith/nl/icp/candidate.cpp +++ b/src/theory/arith/nl/icp/candidate.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/icp/candidate.h b/src/theory/arith/nl/icp/candidate.h index 4a52456ff..5d8c2b2d0 100644 --- a/src/theory/arith/nl/icp/candidate.h +++ b/src/theory/arith/nl/icp/candidate.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/icp/contraction_origins.cpp b/src/theory/arith/nl/icp/contraction_origins.cpp index 858915537..a076dbdb0 100644 --- a/src/theory/arith/nl/icp/contraction_origins.cpp +++ b/src/theory/arith/nl/icp/contraction_origins.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/icp/contraction_origins.h b/src/theory/arith/nl/icp/contraction_origins.h index 360641704..bef6b2848 100644 --- a/src/theory/arith/nl/icp/contraction_origins.h +++ b/src/theory/arith/nl/icp/contraction_origins.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp index 7d698a221..5b505b070 100644 --- a/src/theory/arith/nl/icp/icp_solver.cpp +++ b/src/theory/arith/nl/icp/icp_solver.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h index 9b41ed6e0..85b2e86c6 100644 --- a/src/theory/arith/nl/icp/icp_solver.h +++ b/src/theory/arith/nl/icp/icp_solver.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/icp/intersection.cpp b/src/theory/arith/nl/icp/intersection.cpp index b5fedb7eb..3dc0ca815 100644 --- a/src/theory/arith/nl/icp/intersection.cpp +++ b/src/theory/arith/nl/icp/intersection.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/icp/intersection.h b/src/theory/arith/nl/icp/intersection.h index db14184b0..1670a8f68 100644 --- a/src/theory/arith/nl/icp/intersection.h +++ b/src/theory/arith/nl/icp/intersection.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/icp/interval.h b/src/theory/arith/nl/icp/interval.h index 01968e70f..ff4bbfcac 100644 --- a/src/theory/arith/nl/icp/interval.h +++ b/src/theory/arith/nl/icp/interval.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/nl_lemma_utils.cpp b/src/theory/arith/nl/nl_lemma_utils.cpp index 1589341ed..d7785dbc9 100644 --- a/src/theory/arith/nl/nl_lemma_utils.cpp +++ b/src/theory/arith/nl/nl_lemma_utils.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h index b782b33d7..6f3ef077a 100644 --- a/src/theory/arith/nl/nl_lemma_utils.h +++ b/src/theory/arith/nl/nl_lemma_utils.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Gereon Kremer, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index 9255d3349..dae13318c 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Gereon Kremer, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h index 4d5585545..f907963c1 100644 --- a/src/theory/arith/nl/nl_model.h +++ b/src/theory/arith/nl/nl_model.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Gereon Kremer, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index f269f1d69..38243823b 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Gereon Kremer, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 6a38021a0..47d62e607 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Gereon Kremer, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp index 67cfd5807..ebd528616 100644 --- a/src/theory/arith/nl/poly_conversion.cpp +++ b/src/theory/arith/nl/poly_conversion.cpp @@ -2,9 +2,9 @@ /*! \file poly_conversion.cpp ** \verbatim ** Top contributors (to current version): - ** Gereon Kremer + ** Gereon Kremer, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h index 94ed5e318..47a66d5f1 100644 --- a/src/theory/arith/nl/poly_conversion.h +++ b/src/theory/arith/nl/poly_conversion.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/stats.cpp b/src/theory/arith/nl/stats.cpp index ee12f941e..c707dd9bc 100644 --- a/src/theory/arith/nl/stats.cpp +++ b/src/theory/arith/nl/stats.cpp @@ -2,9 +2,9 @@ /*! \file stats.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/stats.h b/src/theory/arith/nl/stats.h index fab4de35a..94e1882b3 100644 --- a/src/theory/arith/nl/stats.h +++ b/src/theory/arith/nl/stats.h @@ -2,9 +2,9 @@ /*! \file stats.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/strategy.cpp b/src/theory/arith/nl/strategy.cpp index 90ab14ac5..5d6eeea9e 100644 --- a/src/theory/arith/nl/strategy.cpp +++ b/src/theory/arith/nl/strategy.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/strategy.h b/src/theory/arith/nl/strategy.h index 1f7b85b60..3540f9ad1 100644 --- a/src/theory/arith/nl/strategy.h +++ b/src/theory/arith/nl/strategy.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index 74766926b..68d5a5f31 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h index ddef4faf7..76b14022f 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.h +++ b/src/theory/arith/nl/transcendental/exponential_solver.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/transcendental/proof_checker.cpp b/src/theory/arith/nl/transcendental/proof_checker.cpp index e09c8509a..223db8355 100644 --- a/src/theory/arith/nl/transcendental/proof_checker.cpp +++ b/src/theory/arith/nl/transcendental/proof_checker.cpp @@ -2,9 +2,9 @@ /*! \file proof_checker.cpp ** \verbatim ** Top contributors (to current version): - ** Gereon Kremer + ** Gereon Kremer, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/transcendental/proof_checker.h b/src/theory/arith/nl/transcendental/proof_checker.h index 2634d70b1..b00c1811c 100644 --- a/src/theory/arith/nl/transcendental/proof_checker.h +++ b/src/theory/arith/nl/transcendental/proof_checker.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index 11852ac3a..0e5c09a2f 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h index a009df09b..0b2e9d920 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.h +++ b/src/theory/arith/nl/transcendental/sine_solver.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp index f45b906bc..ced202308 100644 --- a/src/theory/arith/nl/transcendental/taylor_generator.cpp +++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp @@ -2,9 +2,9 @@ /*! \file taylor_generator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer, Tim King + ** Gereon Kremer, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/transcendental/taylor_generator.h b/src/theory/arith/nl/transcendental/taylor_generator.h index 0e1248f7c..7cb03cd7c 100644 --- a/src/theory/arith/nl/transcendental/taylor_generator.h +++ b/src/theory/arith/nl/transcendental/taylor_generator.h @@ -2,9 +2,9 @@ /*! \file taylor_generator.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer + ** Gereon Kremer, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index d1355c746..c6b929fec 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Gereon Kremer, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h index 343f303d1..290e74322 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.h +++ b/src/theory/arith/nl/transcendental/transcendental_solver.h @@ -2,9 +2,9 @@ /*! \file transcendental_solver.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer, Tim King + ** Andrew Reynolds, Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index ae8c1eea7..438cc7047 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -2,9 +2,9 @@ /*! \file transcendental_state.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer + ** Gereon Kremer, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h index d0678fb9a..33994fa3a 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.h +++ b/src/theory/arith/nl/transcendental/transcendental_state.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Gereon Kremer, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index ed02a8d4e..537a39a77 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Gereon Kremer, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index ea20de71d..bf8ec6c58 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters, Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index 8aaab3f69..6a9a130ca 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -2,9 +2,9 @@ /*! \file operator_elim.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Andres Noetzli, Morgan Deters + ** Andrew Reynolds, Andres Noetzli, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h index 49638d9fb..6dc535444 100644 --- a/src/theory/arith/operator_elim.h +++ b/src/theory/arith/operator_elim.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Andres Noetzli, Martin Brain ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index bf86c7e86..32c61e815 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index 1606be73b..ec682b948 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp index a28eb02df..80a8a888f 100644 --- a/src/theory/arith/proof_checker.cpp +++ b/src/theory/arith/proof_checker.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Alex Ozdemir ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/proof_checker.h b/src/theory/arith/proof_checker.h index 720fba34a..8d2a94215 100644 --- a/src/theory/arith/proof_checker.h +++ b/src/theory/arith/proof_checker.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Alex Ozdemir ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/proof_macros.h b/src/theory/arith/proof_macros.h index 6f24d3601..dfb3ddad8 100644 --- a/src/theory/arith/proof_macros.h +++ b/src/theory/arith/proof_macros.h @@ -2,9 +2,9 @@ /*! \file proof_macros.h ** \verbatim ** Top contributors (to current version): - ** Alex Ozdemir + ** Alex Ozdemir, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/rewrites.cpp b/src/theory/arith/rewrites.cpp index 870d009d2..f2eef7013 100644 --- a/src/theory/arith/rewrites.cpp +++ b/src/theory/arith/rewrites.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/rewrites.h b/src/theory/arith/rewrites.h index 48913e8cf..6b5e8fc9f 100644 --- a/src/theory/arith/rewrites.h +++ b/src/theory/arith/rewrites.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index d0a7f7fc4..c383c3a85 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 @@ -15,7 +15,6 @@ ** \todo document this file **/ - #include "base/output.h" #include "options/arith_options.h" #include "theory/arith/constraint.h" diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index e34696cb5..d1f891676 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -2,17 +2,18 @@ /*! \file simplex.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Mathias Preiner, Clark Barrett + ** Tim King, Mathias Preiner, Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 is an implementation of the Simplex Module for the Simplex for DPLL(T) - ** decision procedure. + ** \brief This is an implementation of the Simplex Module for the Simplex for + ** DPLL(T) decision procedure. ** - ** This implements the Simplex module for the Simpelx for DPLL(T) decision procedure. + ** This implements the Simplex module for the Simpelx for DPLL(T) decision + ** procedure. ** See the Simplex for DPLL(T) technical report for more background.(citation?) ** This shares with the theory a Tableau, and a PartialModel that: ** - satisfies the equalities in the Tableau, and @@ -21,26 +22,27 @@ ** Further, we require being told when a basic variable updates its value. ** ** During the Simplex search we maintain a queue of variables. - ** The queue is required to contain all of the basic variables that voilate their bounds. + ** The queue is required to contain all of the basic variables that voilate + ** their bounds. ** As elimination from the queue is more efficient to be done lazily, - ** we do not maintain that the queue of variables needs to be only basic variables or only - ** variables that satisfy their bounds. + ** we do not maintain that the queue of variables needs to be only basic + *( variables or only variables that satisfy their bounds. ** ** The simplex procedure roughly follows Alberto's thesis. (citation?) - ** There is one round of selecting using a heuristic pivoting rule. (See PreferenceFunction - ** Documentation for the available options.) - ** The non-basic variable is the one that appears in the fewest pivots. (Bruno says that - ** Leonardo invented this first.) + ** There is one round of selecting using a heuristic pivoting rule. + ** (See PreferenceFunction Documentation for the available options.) + ** The non-basic variable is the one that appears in the fewest pivots. + ** (Bruno says that Leonardo invented this first.) ** After this, Bland's pivot rule is invoked. ** ** During this proccess, we periodically inspect the queue of variables to ** 1) remove now extraneous extries, - ** 2) detect conflicts that are "waiting" on the queue but may not be detected by the - ** current queue heuristics, and + ** 2) detect conflicts that are "waiting" on the queue but may not be detected + ** by the current queue heuristics, and ** 3) detect multiple conflicts. ** - ** Conflicts are greedily slackened to use the weakest bounds that still produce the - ** conflict. + ** Conflicts are greedily slackened to use the weakest bounds that still + ** produce the conflict. ** ** Extra things tracked atm: (Subject to change at Tim's whims) ** - A superset of all of the newly pivoted variables. @@ -48,7 +50,6 @@ ** These are theory valid and are currently turned into lemmas **/ - #include "cvc4_private.h" #pragma once diff --git a/src/theory/arith/simplex_update.cpp b/src/theory/arith/simplex_update.cpp index a1431a78d..98bf07ccf 100644 --- a/src/theory/arith/simplex_update.cpp +++ b/src/theory/arith/simplex_update.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 @@ -14,7 +14,6 @@ ** This implements the UpdateInfo. **/ - #include "theory/arith/simplex_update.h" #include "theory/arith/constraint.h" diff --git a/src/theory/arith/simplex_update.h b/src/theory/arith/simplex_update.h index b6792c265..f8a6bf957 100644 --- a/src/theory/arith/simplex_update.h +++ b/src/theory/arith/simplex_update.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 @@ -24,7 +24,6 @@ ** using both the Tableau and PartialModel. **/ - #include "cvc4_private.h" #pragma once diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index 796cd9412..d47dba70f 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Aina Niemetz, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h index b6df9b488..5febe1bb0 100644 --- a/src/theory/arith/soi_simplex.h +++ b/src/theory/arith/soi_simplex.h @@ -4,15 +4,16 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 is an implementation of the Simplex Module for the Simplex for DPLL(T) - ** decision procedure. + ** \brief This is an implementation of the Simplex Module for the Simplex for + ** DPLL(T) decision procedure. ** - ** This implements the Simplex module for the Simpelx for DPLL(T) decision procedure. + ** This implements the Simplex module for the Simpelx for DPLL(T) decision + ** procedure. ** See the Simplex for DPLL(T) technical report for more background.(citation?) ** This shares with the theory a Tableau, and a PartialModel that: ** - satisfies the equalities in the Tableau, and @@ -21,26 +22,27 @@ ** Further, we require being told when a basic variable updates its value. ** ** During the Simplex search we maintain a queue of variables. - ** The queue is required to contain all of the basic variables that voilate their bounds. + ** The queue is required to contain all of the basic variables that voilate + ** their bounds. ** As elimination from the queue is more efficient to be done lazily, - ** we do not maintain that the queue of variables needs to be only basic variables or only - ** variables that satisfy their bounds. + ** we do not maintain that the queue of variables needs to be only basic + ** variables or only variables that satisfy their bounds. ** ** The simplex procedure roughly follows Alberto's thesis. (citation?) - ** There is one round of selecting using a heuristic pivoting rule. (See PreferenceFunction - ** Documentation for the available options.) - ** The non-basic variable is the one that appears in the fewest pivots. (Bruno says that - ** Leonardo invented this first.) + ** There is one round of selecting using a heuristic pivoting rule. + ** (See PreferenceFunction Documentation for the available options.) + ** The non-basic variable is the one that appears in the fewest pivots. + ** (Bruno says that Leonardo invented this first.) ** After this, Bland's pivot rule is invoked. ** ** During this proccess, we periodically inspect the queue of variables to ** 1) remove now extraneous extries, - ** 2) detect conflicts that are "waiting" on the queue but may not be detected by the - ** current queue heuristics, and + ** 2) detect conflicts that are "waiting" on the queue but may not be detected + ** by the current queue heuristics, and ** 3) detect multiple conflicts. ** - ** Conflicts are greedily slackened to use the weakest bounds that still produce the - ** conflict. + ** Conflicts are greedily slackened to use the weakest bounds that still + ** produce the conflict. ** ** Extra things tracked atm: (Subject to change at Tim's whims) ** - A superset of all of the newly pivoted variables. diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index a61ce4529..1d57a40dd 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index f6b7f4704..9ee33d7b6 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/tableau_sizes.cpp b/src/theory/arith/tableau_sizes.cpp index e4e6c91d0..4b699a019 100644 --- a/src/theory/arith/tableau_sizes.cpp +++ b/src/theory/arith/tableau_sizes.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/tableau_sizes.h b/src/theory/arith/tableau_sizes.h index 76914e04a..16e58bb2e 100644 --- a/src/theory/arith/tableau_sizes.h +++ b/src/theory/arith/tableau_sizes.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 @@ -15,7 +15,6 @@ ** \todo document this file **/ - #include "cvc4_private.h" #pragma once diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 2638fa3ae..42cd16efc 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Alex Ozdemir ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index eb53687ff..1a41c9301 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Gereon Kremer ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 940e04013..4ce077547 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Alex Ozdemir, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 818393cc7..583ff8dee 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -2,9 +2,9 @@ /*! \file theory_arith_private.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Andrew Reynolds, Morgan Deters + ** Tim King, Andrew Reynolds, Alex Ozdemir ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 0fed2dafd..fbf31e6e2 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -2,9 +2,9 @@ /*! \file theory_arith_type_rules.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Dejan Jovanovic, Christopher L. Conway + ** Andrew Reynolds, Gereon Kremer, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h index 60291f44d..a9e35cdc3 100644 --- a/src/theory/arith/type_enumerator.h +++ b/src/theory/arith/type_enumerator.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2021 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 |