GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/uf/theory_uf.h Lines: 18 19 94.7 %
Date: 2021-03-23 Branches: 30 62 48.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_uf.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Tim King
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 This is the interface to TheoryUF implementations
13
 **
14
 ** This is the interface to TheoryUF implementations.  All
15
 ** implementations of TheoryUF should inherit from this class.
16
 **/
17
18
#include "cvc4_private.h"
19
20
#ifndef CVC4__THEORY__UF__THEORY_UF_H
21
#define CVC4__THEORY__UF__THEORY_UF_H
22
23
#include "expr/node.h"
24
#include "expr/node_trie.h"
25
#include "theory/theory.h"
26
#include "theory/theory_eq_notify.h"
27
#include "theory/theory_state.h"
28
#include "theory/uf/proof_checker.h"
29
#include "theory/uf/symmetry_breaker.h"
30
#include "theory/uf/theory_uf_rewriter.h"
31
32
namespace CVC4 {
33
namespace theory {
34
namespace uf {
35
36
class CardinalityExtension;
37
class HoExtension;
38
39
class TheoryUF : public Theory {
40
 public:
41
8994
  class NotifyClass : public TheoryEqNotifyClass
42
  {
43
   public:
44
8997
    NotifyClass(TheoryInferenceManager& im, TheoryUF& uf)
45
8997
        : TheoryEqNotifyClass(im), d_uf(uf)
46
    {
47
8997
    }
48
49
229842
    void eqNotifyNewClass(TNode t) override
50
    {
51
459684
      Debug("uf-notify") << "NotifyClass::eqNotifyNewClass(" << t << ")"
52
229842
                         << std::endl;
53
229842
      d_uf.eqNotifyNewClass(t);
54
229842
    }
55
56
5533741
    void eqNotifyMerge(TNode t1, TNode t2) override
57
    {
58
11067482
      Debug("uf-notify") << "NotifyClass::eqNotifyMerge(" << t1 << ", " << t2
59
5533741
                         << ")" << std::endl;
60
5533741
      d_uf.eqNotifyMerge(t1, t2);
61
5533741
    }
62
63
996238
    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
64
    {
65
996238
      Debug("uf-notify") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << ")" << std::endl;
66
996238
      d_uf.eqNotifyDisequal(t1, t2, reason);
67
996238
    }
68
69
   private:
70
    /** Reference to the parent theory */
71
    TheoryUF& d_uf;
72
  };/* class TheoryUF::NotifyClass */
73
74
private:
75
  /** The associated cardinality extension (or nullptr if it does not exist) */
76
  std::unique_ptr<CardinalityExtension> d_thss;
77
  /** the higher-order solver extension (or nullptr if it does not exist) */
78
  std::unique_ptr<HoExtension> d_ho;
79
80
  /** node for true */
81
  Node d_true;
82
83
  /** All the function terms that the theory has seen */
84
  context::CDList<TNode> d_functionsTerms;
85
86
  /** Symmetry analyzer */
87
  SymmetryBreaker d_symb;
88
89
  /** called when a new equivalance class is created */
90
  void eqNotifyNewClass(TNode t);
91
92
  /** called when two equivalance classes have merged */
93
  void eqNotifyMerge(TNode t1, TNode t2);
94
95
  /** called when two equivalence classes are made disequal */
96
  void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
97
98
 public:
99
100
  /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
101
  TheoryUF(context::Context* c,
102
           context::UserContext* u,
103
           OutputChannel& out,
104
           Valuation valuation,
105
           const LogicInfo& logicInfo,
106
           ProofNodeManager* pnm = nullptr,
107
           std::string instanceName = "");
108
109
  ~TheoryUF();
110
111
  //--------------------------------- initialization
112
  /** get the official theory rewriter of this theory */
113
  TheoryRewriter* getTheoryRewriter() override;
114
  /**
115
   * Returns true if we need an equality engine. If so, we initialize the
116
   * information regarding how it should be setup. For details, see the
117
   * documentation in Theory::needsEqualityEngine.
118
   */
119
  bool needsEqualityEngine(EeSetupInfo& esi) override;
120
  /** finish initialization */
121
  void finishInit() override;
122
  //--------------------------------- end initialization
123
124
  //--------------------------------- standard check
125
  /** Do we need a check call at last call effort? */
126
  bool needsCheckLastEffort() override;
127
  /** Post-check, called after the fact queue of the theory is processed. */
128
  void postCheck(Effort level) override;
129
  /** Pre-notify fact, return true if processed. */
130
  bool preNotifyFact(TNode atom,
131
                     bool pol,
132
                     TNode fact,
133
                     bool isPrereg,
134
                     bool isInternal) override;
135
  /** Notify fact */
136
  void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
137
  //--------------------------------- end standard check
138
139
  /** Collect model values in m based on the relevant terms given by termSet */
140
  bool collectModelValues(TheoryModel* m,
141
                          const std::set<Node>& termSet) override;
142
143
  TrustNode ppRewrite(TNode node, std::vector<SkolemLemma>& lems) override;
144
  void preRegisterTerm(TNode term) override;
145
  TrustNode explain(TNode n) override;
146
147
148
  void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
149
  void presolve() override;
150
151
  void computeCareGraph() override;
152
153
  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
154
155
  std::string identify() const override { return "THEORY_UF"; }
156
 private:
157
  /** Explain why this literal is true by building an explanation */
158
  void explain(TNode literal, Node& exp);
159
160
  bool areCareDisequal(TNode x, TNode y);
161
  void addCarePairs(const TNodeTrie* t1,
162
                    const TNodeTrie* t2,
163
                    unsigned arity,
164
                    unsigned depth);
165
  /**
166
   * Is t a higher order type? A higher-order type is a function type having
167
   * an argument type that is also a function type. This is used for checking
168
   * logic exceptions.
169
   */
170
  bool isHigherOrderType(TypeNode tn);
171
  TheoryUfRewriter d_rewriter;
172
  /** Proof rule checker */
173
  UfProofRuleChecker d_ufProofChecker;
174
  /** A (default) theory state object */
175
  TheoryState d_state;
176
  /** A (default) inference manager */
177
  TheoryInferenceManager d_im;
178
  /** The notify class */
179
  NotifyClass d_notify;
180
  /** Cache for isHigherOrderType */
181
  std::map<TypeNode, bool> d_isHoType;
182
};/* class TheoryUF */
183
184
}/* CVC4::theory::uf namespace */
185
}/* CVC4::theory namespace */
186
}/* CVC4 namespace */
187
188
#endif /* CVC4__THEORY__UF__THEORY_UF_H */