1 /********************* */
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-2020 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
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "cvc4_private.h"
20 #ifndef CVC4__THEORY__FP__THEORY_FP_H
21 #define CVC4__THEORY__FP__THEORY_FP_H
26 #include "context/cdo.h"
27 #include "theory/fp/theory_fp_rewriter.h"
28 #include "theory/theory.h"
29 #include "theory/uf/equality_engine.h"
37 class TheoryFp
: public Theory
40 /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
41 TheoryFp(context::Context
* c
,
42 context::UserContext
* u
,
45 const LogicInfo
& logicInfo
,
46 ProofNodeManager
* pnm
= nullptr);
48 //--------------------------------- initialization
49 /** Get the official theory rewriter of this theory. */
50 TheoryRewriter
* getTheoryRewriter() override
;
52 * Returns true if we need an equality engine. If so, we initialize the
53 * information regarding how it should be setup. For details, see the
54 * documentation in Theory::needsEqualityEngine.
56 bool needsEqualityEngine(EeSetupInfo
& esi
) override
;
57 /** Finish initialization. */
58 void finishInit() override
;
59 //--------------------------------- end initialization
61 TrustNode
expandDefinition(Node node
) override
;
63 void preRegisterTerm(TNode node
) override
;
65 TrustNode
ppRewrite(TNode node
) override
;
67 //--------------------------------- standard check
68 /** Do we need a check call at last call effort? */
69 bool needsCheckLastEffort() override
;
70 /** Post-check, called after the fact queue of the theory is processed. */
71 void postCheck(Effort level
) override
;
72 /** Pre-notify fact, return true if processed. */
73 bool preNotifyFact(TNode atom
,
77 bool isInternal
) override
;
78 //--------------------------------- end standard check
80 Node
getModelValue(TNode var
) override
;
81 bool collectModelInfo(TheoryModel
* m
,
82 const std::set
<Node
>& relevantTerms
) override
;
84 * Collect model values in m based on the relevant terms given by
87 bool collectModelValues(TheoryModel
* m
,
88 const std::set
<Node
>& relevantTerms
) override
;
90 std::string
identify() const override
{ return "THEORY_FP"; }
92 TrustNode
explain(TNode n
) override
;
95 using PairTypeNodeHashFunction
= PairHashFunction
<TypeNode
,
98 TypeNodeHashFunction
>;
99 /** Uninterpreted functions for undefined cases of non-total operators. */
100 using ComparisonUFMap
=
101 context::CDHashMap
<TypeNode
, Node
, TypeNodeHashFunction
>;
102 /** Uninterpreted functions for lazy handling of conversions. */
103 using ConversionUFMap
= context::
104 CDHashMap
<std::pair
<TypeNode
, TypeNode
>, Node
, PairTypeNodeHashFunction
>;
105 using ConversionAbstractionMap
= ComparisonUFMap
;
106 using AbstractionMap
= context::CDHashMap
<Node
, Node
, NodeHashFunction
>;
108 /** Equality engine. */
109 class NotifyClass
: public eq::EqualityEngineNotify
{
111 TheoryFp
& d_theorySolver
;
114 NotifyClass(TheoryFp
& solver
) : d_theorySolver(solver
) {}
115 bool eqNotifyTriggerPredicate(TNode predicate
, bool value
) override
;
116 bool eqNotifyTriggerTermEquality(TheoryId tag
,
119 bool value
) override
;
120 void eqNotifyConstantTermMerge(TNode t1
, TNode t2
) override
;
121 void eqNotifyNewClass(TNode t
) override
{}
122 void eqNotifyMerge(TNode t1
, TNode t2
) override
{}
123 void eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
) override
{}
127 NotifyClass d_notification
;
129 /** General utility. */
130 void registerTerm(TNode node
);
131 bool isRegistered(TNode node
);
133 context::CDHashSet
<Node
, NodeHashFunction
> d_registeredTerms
;
135 /** The word-blaster. Translates FP -> BV. */
136 std::unique_ptr
<FpConverter
> d_conv
;
138 bool d_expansionRequested
;
140 void convertAndEquateTerm(TNode node
);
142 /** Interaction with the rest of the solver **/
143 void handleLemma(Node node
);
145 * Called when literal node is inferred by the equality engine. This
146 * propagates node on the output channel.
148 bool propagateLit(TNode node
);
150 * Called when two constants t1 and t2 merge in the equality engine. This
151 * sends a conflict on the output channel.
153 void conflictEqConstantMerge(TNode t1
, TNode t2
);
155 bool refineAbstraction(TheoryModel
* m
, TNode abstract
, TNode concrete
);
165 Node
abstractRealToFloat(Node
);
166 Node
abstractFloatToReal(Node
);
169 context::CDO
<Node
> d_conflictNode
;
171 ComparisonUFMap d_minMap
;
172 ComparisonUFMap d_maxMap
;
173 ConversionUFMap d_toUBVMap
;
174 ConversionUFMap d_toSBVMap
;
175 ComparisonUFMap d_toRealMap
;
176 ConversionAbstractionMap d_realToFloatMap
;
177 ConversionAbstractionMap d_floatToRealMap
;
178 AbstractionMap d_abstractionMap
; // abstract -> original
180 /** The theory rewriter for this theory. */
181 TheoryFpRewriter d_rewriter
;
182 /** A (default) theory state object */
184 }; /* class TheoryFp */
187 } // namespace theory
190 #endif /* CVC4__THEORY__FP__THEORY_FP_H */