1 /********************* */
4 ** Top contributors (to current version):
5 ** Mathias Preiner, Andrew Reynolds, Tim King
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 Bitvector theory.
17 #include "cvc4_private.h"
19 #ifndef CVC4__THEORY__BV__THEORY_BV_H
20 #define CVC4__THEORY__BV__THEORY_BV_H
22 #include <unordered_map>
24 #include "theory/bv/theory_bv_rewriter.h"
25 #include "theory/theory.h"
26 #include "theory/theory_eq_notify.h"
34 class TheoryBV
: public Theory
36 /* BVSolverLazy accesses methods from theory in a way that is deprecated and
37 * will be removed in the future. For now we allow direct access. */
38 friend class BVSolverLazy
;
41 TheoryBV(context::Context
* c
,
42 context::UserContext
* u
,
45 const LogicInfo
& logicInfo
,
46 ProofNodeManager
* pnm
= nullptr,
47 std::string name
= "");
51 /** get the official theory rewriter of this theory */
52 TheoryRewriter
* getTheoryRewriter() override
;
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.
59 bool needsEqualityEngine(EeSetupInfo
& esi
) override
;
61 void finishInit() override
;
63 TrustNode
expandDefinition(Node node
) override
;
65 void preRegisterTerm(TNode n
) override
;
67 bool preCheck(Effort e
) override
;
69 void postCheck(Effort e
) override
;
71 bool preNotifyFact(TNode atom
,
75 bool isInternal
) override
;
77 void notifyFact(TNode atom
, bool pol
, TNode fact
, bool isInternal
) override
;
79 bool needsCheckLastEffort() override
;
81 void propagate(Effort e
) override
;
83 TrustNode
explain(TNode n
) override
;
85 /** Collect model values in m based on the relevant terms given by termSet */
86 bool collectModelValues(TheoryModel
* m
,
87 const std::set
<Node
>& termSet
) override
;
89 std::string
identify() const override
{ return std::string("TheoryBV"); }
91 PPAssertStatus
ppAssert(TrustNode in
,
92 TrustSubstitutionMap
& outSubstitutions
) override
;
94 TrustNode
ppRewrite(TNode t
) override
;
96 void ppStaticLearn(TNode in
, NodeBuilder
<>& learned
) override
;
98 void presolve() override
;
100 EqualityStatus
getEqualityStatus(TNode a
, TNode b
) override
;
102 /** Called by abstraction preprocessing pass. */
103 bool applyAbstraction(const std::vector
<Node
>& assertions
,
104 std::vector
<Node
>& new_assertions
);
107 void notifySharedTerm(TNode t
) override
;
110 * Return the UF symbol corresponding to division-by-zero for this particular
112 * @param k should be UREM or UDIV
113 * @param width bit-width
115 Node
getUFDivByZero(Kind k
, unsigned width
);
117 /** Internal BV solver. */
118 std::unique_ptr
<BVSolver
> d_internal
;
121 * Maps from bit-vector width to division-by-zero uninterpreted
124 std::unordered_map
<unsigned, Node
> d_ufDivByZero
;
125 std::unordered_map
<unsigned, Node
> d_ufRemByZero
;
127 /** The theory rewriter for this theory. */
128 TheoryBVRewriter d_rewriter
;
130 /** A (default) theory state object */
133 /** A (default) theory inference manager. */
134 TheoryInferenceManager d_im
;
136 /** The notify class for equality engine. */
137 TheoryEqNotifyClass d_notify
;
139 }; /* class TheoryBV */
142 } // namespace theory
145 #endif /* CVC4__THEORY__BV__THEORY_BV_H */