1 /********************* */
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief The care graph datastructure.
14 ** The care graph datastructure.
17 #include "cvc4_private.h"
19 #ifndef __CVC4__THEORY__CARE_GRAPH_H
20 #define __CVC4__THEORY__CARE_GRAPH_H
24 #include "expr/kind.h" // For TheoryId.
25 #include "expr/node.h"
31 * A (ordered) pair of terms a theory cares about.
35 const TheoryId theory
;
37 CarePair(TNode a
, TNode b
, TheoryId theory
)
38 : a(a
< b
? a
: b
), b(a
< b
? b
: a
), theory(theory
) {}
40 bool operator==(const CarePair
& other
) const {
41 return (theory
== other
.theory
) && (a
== other
.a
) && (b
== other
.b
);
44 bool operator<(const CarePair
& other
) const {
45 if (theory
< other
.theory
) return true;
46 if (theory
> other
.theory
) return false;
47 if (a
< other
.a
) return true;
48 if (a
> other
.a
) return false;
52 }; /* struct CarePair */
55 * A set of care pairs.
57 typedef std::set
<CarePair
> CareGraph
;
62 #endif /* __CVC4__THEORY__CARE_GRAPH_H */