-Node BVSolverBitblast::getValue(TNode node)
-{
- if (d_invalidateModelCache.get())
- {
- d_modelCache.clear();
- }
- d_invalidateModelCache.set(false);
-
- std::vector<TNode> visit;
-
- TNode cur;
- visit.push_back(node);
- do
- {
- cur = visit.back();
- visit.pop_back();
-
- auto it = d_modelCache.find(cur);
- if (it != d_modelCache.end() && !it->second.isNull())
- {
- continue;
- }
-
- if (d_bitblaster->hasBBTerm(cur))
- {
- Node value = getValueFromSatSolver(cur, false);
- if (value.isConst())
- {
- d_modelCache[cur] = value;
- continue;
- }
- }
- if (Theory::isLeafOf(cur, theory::THEORY_BV))
- {
- Node value = getValueFromSatSolver(cur, true);
- d_modelCache[cur] = value;
- continue;
- }
-
- if (it == d_modelCache.end())
- {
- visit.push_back(cur);
- d_modelCache.emplace(cur, Node());
- visit.insert(visit.end(), cur.begin(), cur.end());
- }
- else if (it->second.isNull())
- {
- NodeBuilder nb(cur.getKind());
- if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
- {
- nb << cur.getOperator();
- }
-
- std::unordered_map<Node, Node>::iterator iit;
- for (const TNode& child : cur)
- {
- iit = d_modelCache.find(child);
- Assert(iit != d_modelCache.end());
- Assert(iit->second.isConst());
- nb << iit->second;
- }
- it->second = Rewriter::rewrite(nb.constructNode());
- }
- } while (!visit.empty());
-
- auto it = d_modelCache.find(node);
- Assert(it != d_modelCache.end());
- return it->second;
-}
-