src/theory/care_graph.h

   1 /*********************                                                        */
   2 /*! \file care_graph.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Dejan Jovanovic, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 d_a, d_b;
  35   const TheoryId d_theory;
  36
  37   CarePair(TNode a, TNode b, TheoryId theory)
  38       : d_a(a < b ? a : b), d_b(a < b ? b : a), d_theory(theory)
  39   {
  40   }
  41
  42   bool operator==(const CarePair& other) const {
  43     return (d_theory == other.d_theory) && (d_a == other.d_a)
  44            && (d_b == other.d_b);
  45   }
  46
  47   bool operator<(const CarePair& other) const {
  48     if (d_theory < other.d_theory) return true;
  49     if (d_theory > other.d_theory) return false;
  50     if (d_a < other.d_a) return true;
  51     if (d_a > other.d_a) return false;
  52     return d_b < other.d_b;
  53   }
  54
  55 }; /* struct CarePair */
  56
  57 /**
  58  * A set of care pairs.
  59  */
  60 typedef std::set<CarePair> CareGraph;
  61
  62 }  // namespace theory
  63 }  // namespace CVC4
  64
  65 #endif /* CVC4__THEORY__CARE_GRAPH_H */