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

Line Exec Source
1
/*********************                                                        */
2
/*! \file ee_manager.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 Utilities for management of equality engines.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__EE_MANAGER__H
18
#define CVC4__THEORY__EE_MANAGER__H
19
20
#include <map>
21
#include <memory>
22
23
#include "theory/ee_setup_info.h"
24
#include "theory/theory.h"
25
#include "theory/uf/equality_engine.h"
26
27
namespace CVC4 {
28
29
class TheoryEngine;
30
31
namespace theory {
32
33
class SharedSolver;
34
35
/**
36
 * This is (theory-agnostic) information associated with the management of
37
 * an equality engine for a single theory. This information is maintained
38
 * by the manager class below.
39
 *
40
 * Currently, this simply is the equality engine itself, for memory
41
 * management purposes.
42
 */
43
116922
struct EeTheoryInfo
44
{
45
116961
  EeTheoryInfo() : d_usedEe(nullptr) {}
46
  /** Equality engine that is used (if it exists) */
47
  eq::EqualityEngine* d_usedEe;
48
  /** Equality engine allocated specifically for this theory (if it exists) */
49
  std::unique_ptr<eq::EqualityEngine> d_allocEe;
50
};
51
52
/** Virtual base class for equality engine managers */
53
class EqEngineManager
54
{
55
 public:
56
   /**
57
   * @param te Reference to the theory engine
58
   * @param sharedSolver The shared solver that is being used in combination
59
   * with this equality engine manager
60
    */
61
  EqEngineManager(TheoryEngine& te, SharedSolver& shs);
62
8994
  virtual ~EqEngineManager() {}
63
  /**
64
   * Initialize theories, called during TheoryEngine::finishInit after theory
65
   * objects have been created but prior to their final initialization. This
66
   * sets up equality engines for all theories.
67
   *
68
   * This method is context-independent, and is applied once during
69
   * the lifetime of TheoryEngine (during finishInit).
70
   */
71
  virtual void initializeTheories() = 0;
72
  /**
73
   * Get the equality engine theory information for theory with the given id.
74
   */
75
  const EeTheoryInfo* getEeTheoryInfo(TheoryId tid) const;
76
77
  /** Allocate equality engine that is context-dependent on c with info esi */
78
  eq::EqualityEngine* allocateEqualityEngine(EeSetupInfo& esi,
79
                                             context::Context* c);
80
  /**
81
   * Notify this class that we are about to terminate with a model. This method
82
   * is for debugging only.
83
   *
84
   * @param incomplete Whether we are answering "unknown" instead of "sat".
85
   */
86
  virtual void notifyModel(bool incomplete) {}
87
88
 protected:
89
  /** Reference to the theory engine */
90
  TheoryEngine& d_te;
91
  /** Reference to the shared solver */
92
  SharedSolver& d_sharedSolver;
93
  /** Information related to the equality engine, per theory. */
94
  std::map<TheoryId, EeTheoryInfo> d_einfo;
95
};
96
97
}  // namespace theory
98
}  // namespace CVC4
99
100
#endif /* CVC4__THEORY__EE_MANAGER__H */