diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-03-08 23:27:03 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-09 07:27:03 +0000 |
commit | b302cb1f92aae1c0954c86065469e5c2b7206e74 (patch) | |
tree | f2b4cad1effdfe8041f00f23b6fe255b0c4004bb /src/theory/arith/constraint.h | |
parent | 86ce1c18f8ea7a397a8b12405a196b126e82b648 (diff) |
Update copyright headers to 2021. (#6081)
Diffstat (limited to 'src/theory/arith/constraint.h')
-rw-r--r-- | src/theory/arith/constraint.h | 21 |
1 files changed, 12 insertions, 9 deletions
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" |