src/theory/care_graph.h

   1 /*********************                                                        */
   2 /*! \file care_graph.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King
   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
  11  **
  12  ** \brief The care graph datastructure.
  13  **
  14  ** The care graph datastructure.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__THEORY__CARE_GRAPH_H
  20 #define __CVC4__THEORY__CARE_GRAPH_H
  21
  22 #include <set>
  23
  24 #include "expr/kind.h"  // For TheoryId.
  25 #include "expr/node.h"
  26
  27 namespace CVC4 {
  28 namespace theory {
  29
  30 /**
  31  * A (ordered) pair of terms a theory cares about.
  32  */
  33 struct CarePair {
  34   const TNode a, b;
  35   const TheoryId theory;
  36
  37   CarePair(TNode a, TNode b, TheoryId theory)
  38       : a(a < b ? a : b), b(a < b ? b : a), theory(theory) {}
  39
  40   bool operator==(const CarePair& other) const {
  41     return (theory == other.theory) && (a == other.a) && (b == other.b);
  42   }
  43
  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;
  49     return b < other.b;
  50   }
  51
  52 }; /* struct CarePair */
  53
  54 /**
  55  * A set of care pairs.
  56  */
  57 typedef std::set<CarePair> CareGraph;
  58
  59 }  // namespace theory
  60 }  // namespace CVC4
  61
  62 #endif /* __CVC4__THEORY__CARE_GRAPH_H */