1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
|
/******************************************************************************
* Top contributors (to current version):
* Andrew Reynolds, Martin Brain, Aina Niemetz
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
* in the top-level source directory and their institutional affiliations.
* All rights reserved. See the file COPYING in the top-level source
* directory for licensing information.
* ****************************************************************************
*
* Theory of floating-point arithmetic.
*/
#include "cvc5_private.h"
#ifndef CVC5__THEORY__FP__THEORY_FP_H
#define CVC5__THEORY__FP__THEORY_FP_H
#include <string>
#include <utility>
#include "context/cdhashset.h"
#include "context/cdo.h"
#include "theory/fp/theory_fp_rewriter.h"
#include "theory/theory.h"
#include "theory/theory_inference_manager.h"
#include "theory/theory_state.h"
#include "theory/uf/equality_engine.h"
namespace cvc5 {
namespace theory {
namespace fp {
class FpConverter;
class TheoryFp : public Theory
{
public:
/** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
TheoryFp(context::Context* c,
context::UserContext* u,
OutputChannel& out,
Valuation valuation,
const LogicInfo& logicInfo,
ProofNodeManager* pnm = nullptr);
//--------------------------------- initialization
/** Get the official theory rewriter of this theory. */
TheoryRewriter* getTheoryRewriter() override;
/** get the proof checker of this theory */
ProofRuleChecker* getProofChecker() override;
/**
* Returns true if we need an equality engine. If so, we initialize the
* information regarding how it should be setup. For details, see the
* documentation in Theory::needsEqualityEngine.
*/
bool needsEqualityEngine(EeSetupInfo& esi) override;
/** Finish initialization. */
void finishInit() override;
//--------------------------------- end initialization
void preRegisterTerm(TNode node) override;
TrustNode ppRewrite(TNode node, std::vector<SkolemLemma>& lems) override;
//--------------------------------- standard check
/** Do we need a check call at last call effort? */
bool needsCheckLastEffort() override;
/** Post-check, called after the fact queue of the theory is processed. */
void postCheck(Effort level) override;
/** Pre-notify fact, return true if processed. */
bool preNotifyFact(TNode atom,
bool pol,
TNode fact,
bool isPrereg,
bool isInternal) override;
//--------------------------------- end standard check
Node getModelValue(TNode var) override;
bool collectModelInfo(TheoryModel* m,
const std::set<Node>& relevantTerms) override;
/**
* Collect model values in m based on the relevant terms given by
* relevantTerms.
*/
bool collectModelValues(TheoryModel* m,
const std::set<Node>& relevantTerms) override;
std::string identify() const override { return "THEORY_FP"; }
TrustNode explain(TNode n) override;
protected:
using ConversionAbstractionMap = context::CDHashMap<TypeNode, Node>;
using AbstractionMap = context::CDHashMap<Node, Node>;
/** Equality engine. */
class NotifyClass : public eq::EqualityEngineNotify {
protected:
TheoryFp& d_theorySolver;
public:
NotifyClass(TheoryFp& solver) : d_theorySolver(solver) {}
bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
bool eqNotifyTriggerTermEquality(TheoryId tag,
TNode t1,
TNode t2,
bool value) override;
void eqNotifyConstantTermMerge(TNode t1, TNode t2) override;
void eqNotifyNewClass(TNode t) override {}
void eqNotifyMerge(TNode t1, TNode t2) override {}
void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
};
friend NotifyClass;
NotifyClass d_notification;
/** General utility. */
void registerTerm(TNode node);
bool isRegistered(TNode node);
context::CDHashSet<Node> d_registeredTerms;
/** The word-blaster. Translates FP -> BV. */
std::unique_ptr<FpConverter> d_conv;
bool d_expansionRequested;
void convertAndEquateTerm(TNode node);
/** Interaction with the rest of the solver **/
void handleLemma(Node node, InferenceId id = InferenceId::UNKNOWN);
/**
* Called when literal node is inferred by the equality engine. This
* propagates node on the output channel.
*/
bool propagateLit(TNode node);
/**
* Called when two constants t1 and t2 merge in the equality engine. This
* sends a conflict on the output channel.
*/
void conflictEqConstantMerge(TNode t1, TNode t2);
bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete);
Node abstractRealToFloat(Node);
Node abstractFloatToReal(Node);
private:
ConversionAbstractionMap d_realToFloatMap;
ConversionAbstractionMap d_floatToRealMap;
AbstractionMap d_abstractionMap; // abstract -> original
/** The theory rewriter for this theory. */
TheoryFpRewriter d_rewriter;
/** A (default) theory state object */
TheoryState d_state;
/** A (default) inference manager */
TheoryInferenceManager d_im;
}; /* class TheoryFp */
} // namespace fp
} // namespace theory
} // namespace cvc5
#endif /* CVC5__THEORY__FP__THEORY_FP_H */
|
