1 /********************* */
2 /*! \file theory_bv.cpp
4 ** Top contributors (to current version):
5 ** Mathias Preiner, Andrew Reynolds, Martin Brain
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 ** [[ Add lengthier description here ]]
13 ** \todo document this file
16 #include "theory/bv/theory_bv.h"
18 #include "options/bv_options.h"
19 #include "theory/bv/bv_solver_lazy.h"
20 #include "theory/bv/theory_bv_utils.h"
26 TheoryBV::TheoryBV(context::Context
* c
,
27 context::UserContext
* u
,
30 const LogicInfo
& logicInfo
,
31 ProofNodeManager
* pnm
,
33 : Theory(THEORY_BV
, c
, u
, out
, valuation
, logicInfo
, pnm
, name
),
38 d_state(c
, u
, valuation
),
39 d_inferMgr(*this, d_state
, pnm
)
41 d_internal
.reset(new BVSolverLazy(*this, c
, u
, pnm
, name
));
42 d_theoryState
= &d_state
;
43 d_inferManager
= &d_inferMgr
;
46 TheoryBV::~TheoryBV() {}
48 TheoryRewriter
* TheoryBV::getTheoryRewriter() { return &d_rewriter
; }
50 bool TheoryBV::needsEqualityEngine(EeSetupInfo
& esi
)
52 return d_internal
->needsEqualityEngine(esi
);
55 void TheoryBV::finishInit()
57 // these kinds are semi-evaluated in getModelValue (applications of this
58 // kind are treated as variables)
59 getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV
);
60 getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM
);
61 d_internal
->finishInit();
64 Node
TheoryBV::getUFDivByZero(Kind k
, unsigned width
)
66 NodeManager
* nm
= NodeManager::currentNM();
67 if (k
== kind::BITVECTOR_UDIV
)
69 if (d_ufDivByZero
.find(width
) == d_ufDivByZero
.end())
71 // lazily create the function symbols
72 std::ostringstream os
;
73 os
<< "BVUDivByZero_" << width
;
75 nm
->mkSkolem(os
.str(),
76 nm
->mkFunctionType(nm
->mkBitVectorType(width
),
77 nm
->mkBitVectorType(width
)),
79 NodeManager::SKOLEM_EXACT_NAME
);
80 d_ufDivByZero
[width
] = divByZero
;
82 return d_ufDivByZero
[width
];
84 else if (k
== kind::BITVECTOR_UREM
)
86 if (d_ufRemByZero
.find(width
) == d_ufRemByZero
.end())
88 std::ostringstream os
;
89 os
<< "BVURemByZero_" << width
;
91 nm
->mkSkolem(os
.str(),
92 nm
->mkFunctionType(nm
->mkBitVectorType(width
),
93 nm
->mkBitVectorType(width
)),
95 NodeManager::SKOLEM_EXACT_NAME
);
96 d_ufRemByZero
[width
] = divByZero
;
98 return d_ufRemByZero
[width
];
104 TrustNode
TheoryBV::expandDefinition(Node node
)
106 Debug("bitvector-expandDefinition")
107 << "TheoryBV::expandDefinition(" << node
<< ")" << std::endl
;
110 switch (node
.getKind())
112 case kind::BITVECTOR_SDIV
:
113 case kind::BITVECTOR_SREM
:
114 case kind::BITVECTOR_SMOD
:
115 ret
= TheoryBVRewriter::eliminateBVSDiv(node
);
118 case kind::BITVECTOR_UDIV
:
119 case kind::BITVECTOR_UREM
:
121 NodeManager
* nm
= NodeManager::currentNM();
122 unsigned width
= node
.getType().getBitVectorSize();
124 if (options::bitvectorDivByZeroConst())
126 Kind kind
= node
.getKind() == kind::BITVECTOR_UDIV
127 ? kind::BITVECTOR_UDIV_TOTAL
128 : kind::BITVECTOR_UREM_TOTAL
;
129 ret
= nm
->mkNode(kind
, node
[0], node
[1]);
133 TNode num
= node
[0], den
= node
[1];
134 Node den_eq_0
= nm
->mkNode(kind::EQUAL
, den
, utils::mkZero(width
));
135 Node divTotalNumDen
= nm
->mkNode(node
.getKind() == kind::BITVECTOR_UDIV
136 ? kind::BITVECTOR_UDIV_TOTAL
137 : kind::BITVECTOR_UREM_TOTAL
,
140 Node divByZero
= getUFDivByZero(node
.getKind(), width
);
141 Node divByZeroNum
= nm
->mkNode(kind::APPLY_UF
, divByZero
, num
);
142 ret
= nm
->mkNode(kind::ITE
, den_eq_0
, divByZeroNum
, divTotalNumDen
);
148 if (!ret
.isNull() && node
!= ret
)
150 return TrustNode::mkTrustRewrite(node
, ret
, nullptr);
152 return TrustNode::null();
155 void TheoryBV::preRegisterTerm(TNode node
)
157 d_internal
->preRegisterTerm(node
);
160 bool TheoryBV::preCheck(Effort e
) { return d_internal
->preCheck(e
); }
162 bool TheoryBV::needsCheckLastEffort()
164 return d_internal
->needsCheckLastEffort();
167 bool TheoryBV::collectModelValues(TheoryModel
* m
, const std::set
<Node
>& termSet
)
169 return d_internal
->collectModelValues(m
, termSet
);
172 void TheoryBV::propagate(Effort e
) { return d_internal
->propagate(e
); }
174 Theory::PPAssertStatus
TheoryBV::ppAssert(TNode in
,
175 SubstitutionMap
& outSubstitutions
)
177 return d_internal
->ppAssert(in
, outSubstitutions
);
180 TrustNode
TheoryBV::ppRewrite(TNode t
) { return d_internal
->ppRewrite(t
); }
182 void TheoryBV::presolve() { d_internal
->presolve(); }
184 TrustNode
TheoryBV::explain(TNode node
) { return d_internal
->explain(node
); }
186 void TheoryBV::notifySharedTerm(TNode t
)
188 d_internal
->notifySharedTerm(t
);
189 // temporary, will be built into Theory::addSharedTerm
190 if (d_equalityEngine
!= nullptr)
192 d_equalityEngine
->addTriggerTerm(t
, THEORY_BV
);
196 void TheoryBV::ppStaticLearn(TNode in
, NodeBuilder
<>& learned
)
198 d_internal
->ppStaticLearn(in
, learned
);
201 bool TheoryBV::applyAbstraction(const std::vector
<Node
>& assertions
,
202 std::vector
<Node
>& new_assertions
)
204 return d_internal
->applyAbstraction(assertions
, new_assertions
);
208 } // namespace theory