GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/fp/theory_fp.h Lines: 6 7 85.7 %
Date: 2021-03-22 Branches: 0 2 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_fp.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Martin Brain, Aina Niemetz
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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "cvc4_private.h"
19
20
#ifndef CVC4__THEORY__FP__THEORY_FP_H
21
#define CVC4__THEORY__FP__THEORY_FP_H
22
23
#include <string>
24
#include <utility>
25
26
#include "context/cdhashset.h"
27
#include "context/cdo.h"
28
#include "theory/fp/theory_fp_rewriter.h"
29
#include "theory/theory.h"
30
#include "theory/theory_inference_manager.h"
31
#include "theory/theory_state.h"
32
#include "theory/uf/equality_engine.h"
33
34
namespace CVC4 {
35
namespace theory {
36
namespace fp {
37
38
class FpConverter;
39
40
17984
class TheoryFp : public Theory
41
{
42
 public:
43
  /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
44
  TheoryFp(context::Context* c,
45
           context::UserContext* u,
46
           OutputChannel& out,
47
           Valuation valuation,
48
           const LogicInfo& logicInfo,
49
           ProofNodeManager* pnm = nullptr);
50
51
  //--------------------------------- initialization
52
  /** Get the official theory rewriter of this theory. */
53
  TheoryRewriter* getTheoryRewriter() override;
54
  /**
55
   * Returns true if we need an equality engine. If so, we initialize the
56
   * information regarding how it should be setup. For details, see the
57
   * documentation in Theory::needsEqualityEngine.
58
   */
59
  bool needsEqualityEngine(EeSetupInfo& esi) override;
60
  /** Finish initialization. */
61
  void finishInit() override;
62
  //--------------------------------- end initialization
63
64
  TrustNode expandDefinition(Node node) override;
65
66
  void preRegisterTerm(TNode node) override;
67
68
  TrustNode ppRewrite(TNode node, std::vector<SkolemLemma>& lems) override;
69
70
  //--------------------------------- standard check
71
  /** Do we need a check call at last call effort? */
72
  bool needsCheckLastEffort() override;
73
  /** Post-check, called after the fact queue of the theory is processed. */
74
  void postCheck(Effort level) override;
75
  /** Pre-notify fact, return true if processed. */
76
  bool preNotifyFact(TNode atom,
77
                     bool pol,
78
                     TNode fact,
79
                     bool isPrereg,
80
                     bool isInternal) override;
81
  //--------------------------------- end standard check
82
83
  Node getModelValue(TNode var) override;
84
  bool collectModelInfo(TheoryModel* m,
85
                        const std::set<Node>& relevantTerms) override;
86
  /**
87
   * Collect model values in m based on the relevant terms given by
88
   * relevantTerms.
89
   */
90
  bool collectModelValues(TheoryModel* m,
91
                          const std::set<Node>& relevantTerms) override;
92
93
  std::string identify() const override { return "THEORY_FP"; }
94
95
  TrustNode explain(TNode n) override;
96
97
 protected:
98
  using PairTypeNodeHashFunction = PairHashFunction<TypeNode,
99
                                                    TypeNode,
100
                                                    TypeNodeHashFunction,
101
                                                    TypeNodeHashFunction>;
102
  /** Uninterpreted functions for undefined cases of non-total operators. */
103
  using ComparisonUFMap =
104
      context::CDHashMap<TypeNode, Node, TypeNodeHashFunction>;
105
  /** Uninterpreted functions for lazy handling of conversions. */
106
  using ConversionUFMap = context::
107
      CDHashMap<std::pair<TypeNode, TypeNode>, Node, PairTypeNodeHashFunction>;
108
  using ConversionAbstractionMap = ComparisonUFMap;
109
  using AbstractionMap = context::CDHashMap<Node, Node, NodeHashFunction>;
110
111
  /** Equality engine. */
112
8992
  class NotifyClass : public eq::EqualityEngineNotify {
113
   protected:
114
    TheoryFp& d_theorySolver;
115
116
   public:
117
8995
    NotifyClass(TheoryFp& solver) : d_theorySolver(solver) {}
118
    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
119
    bool eqNotifyTriggerTermEquality(TheoryId tag,
120
                                     TNode t1,
121
                                     TNode t2,
122
                                     bool value) override;
123
    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override;
124
2927
    void eqNotifyNewClass(TNode t) override {}
125
1731
    void eqNotifyMerge(TNode t1, TNode t2) override {}
126
551
    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
127
  };
128
  friend NotifyClass;
129
130
  NotifyClass d_notification;
131
132
  /** General utility. */
133
  void registerTerm(TNode node);
134
  bool isRegistered(TNode node);
135
136
  context::CDHashSet<Node, NodeHashFunction> d_registeredTerms;
137
138
  /** The word-blaster. Translates FP -> BV. */
139
  std::unique_ptr<FpConverter> d_conv;
140
141
  bool d_expansionRequested;
142
143
  void convertAndEquateTerm(TNode node);
144
145
  /** Interaction with the rest of the solver **/
146
  void handleLemma(Node node, InferenceId id = InferenceId::UNKNOWN);
147
  /**
148
   * Called when literal node is inferred by the equality engine. This
149
   * propagates node on the output channel.
150
   */
151
  bool propagateLit(TNode node);
152
  /**
153
   * Called when two constants t1 and t2 merge in the equality engine. This
154
   * sends a conflict on the output channel.
155
   */
156
  void conflictEqConstantMerge(TNode t1, TNode t2);
157
158
  bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete);
159
160
  Node minUF(Node);
161
  Node maxUF(Node);
162
163
  Node toUBVUF(Node);
164
  Node toSBVUF(Node);
165
166
  Node toRealUF(Node);
167
168
  Node abstractRealToFloat(Node);
169
  Node abstractFloatToReal(Node);
170
171
 private:
172
173
  ComparisonUFMap d_minMap;
174
  ComparisonUFMap d_maxMap;
175
  ConversionUFMap d_toUBVMap;
176
  ConversionUFMap d_toSBVMap;
177
  ComparisonUFMap d_toRealMap;
178
  ConversionAbstractionMap d_realToFloatMap;
179
  ConversionAbstractionMap d_floatToRealMap;
180
  AbstractionMap d_abstractionMap;  // abstract -> original
181
182
  /** The theory rewriter for this theory. */
183
  TheoryFpRewriter d_rewriter;
184
  /** A (default) theory state object */
185
  TheoryState d_state;
186
  /** A (default) inference manager */
187
  TheoryInferenceManager d_im;
188
}; /* class TheoryFp */
189
190
}  // namespace fp
191
}  // namespace theory
192
}  // namespace CVC4
193
194
#endif /* CVC4__THEORY__FP__THEORY_FP_H */