GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/ee_manager_distributed.h Lines: 4 9 44.4 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ee_manager_distributed.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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 Management of a distributed approach for equality engines over
13
 ** all theories.
14
 **/
15
16
#include "cvc4_private.h"
17
18
#ifndef CVC4__THEORY__EE_MANAGER_DISTRIBUTED__H
19
#define CVC4__THEORY__EE_MANAGER_DISTRIBUTED__H
20
21
#include <memory>
22
23
#include "theory/ee_manager.h"
24
25
namespace CVC4 {
26
namespace theory {
27
28
namespace eq {
29
class EqualityEngine;
30
}
31
32
/**
33
 * The (distributed) equality engine manager. This encapsulates an architecture
34
 * in which all theories maintain their own copy of an equality engine.
35
 *
36
 * This class is not responsible for actually initializing equality engines in
37
 * theories (since this class does not have access to the internals of Theory).
38
 * Instead, it is only responsible for the construction of the equality
39
 * engine objects themselves. TheoryEngine is responsible for querying this
40
 * class during finishInit() to determine the equality engines to pass to each
41
 * theories based on getEeTheoryInfo.
42
 *
43
 * This class is also responsible for setting up the master equality engine,
44
 * which is used as a special communication channel to quantifiers engine (e.g.
45
 * for ensuring quantifiers E-matching is aware of terms from all theories).
46
 */
47
class EqEngineManagerDistributed : public EqEngineManager
48
{
49
 public:
50
  EqEngineManagerDistributed(TheoryEngine& te, SharedSolver& shs);
51
  ~EqEngineManagerDistributed();
52
  /**
53
   * Initialize theories. This method allocates unique equality engines
54
   * per theories and connects them to a master equality engine.
55
   */
56
  void initializeTheories() override;
57
  /** Notify model */
58
  void notifyModel(bool incomplete) override;
59
60
 private:
61
  /** notify class for master equality engine */
62
12102
  class MasterNotifyClass : public theory::eq::EqualityEngineNotify
63
  {
64
   public:
65
6054
    MasterNotifyClass(QuantifiersEngine* qe) : d_quantEngine(qe) {}
66
    /**
67
     * Called when a new equivalence class is created in the master equality
68
     * engine.
69
     */
70
    void eqNotifyNewClass(TNode t) override;
71
72
    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
73
    {
74
      return true;
75
    }
76
    bool eqNotifyTriggerTermEquality(TheoryId tag,
77
                                     TNode t1,
78
                                     TNode t2,
79
                                     bool value) override
80
    {
81
      return true;
82
    }
83
8270
    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {}
84
5258163
    void eqNotifyMerge(TNode t1, TNode t2) override {}
85
    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
86
87
   private:
88
    /** Pointer to quantifiers engine */
89
    QuantifiersEngine* d_quantEngine;
90
  };
91
  /** The master equality engine notify class */
92
  std::unique_ptr<MasterNotifyClass> d_masterEENotify;
93
  /** The master equality engine. */
94
  std::unique_ptr<eq::EqualityEngine> d_masterEqualityEngine;
95
  /** The equality engine of the shared solver / shared terms database. */
96
  std::unique_ptr<eq::EqualityEngine> d_stbEqualityEngine;
97
};
98
99
}  // namespace theory
100
}  // namespace CVC4
101
102
#endif /* CVC4__THEORY__EE_MANAGER_DISTRIBUTED__H */