#include "theory/bv/theory_bv_utils.h"
#include "theory/theory_model.h"
+#include <unordered_set>
using namespace CVC4::context;
using namespace CVC4::prop;
namespace theory {
namespace bv {
+/* ------------------------------------------------------------------------- */
+
+namespace {
+
+/* Collect all variables under a given a node. */
+void collectVariables(TNode node, utils::NodeSet& vars)
+{
+ std::vector<TNode> stack;
+ std::unordered_set<TNode, TNodeHashFunction> visited;
+
+ stack.push_back(node);
+ while (!stack.empty())
+ {
+ Node n = stack.back();
+ stack.pop_back();
+
+ if (vars.find(n) != vars.end()) continue;
+ if (visited.find(n) != visited.end()) continue;
+ visited.insert(n);
+
+ if (Theory::isLeafOf(n, THEORY_BV) && n.getKind() != kind::CONST_BITVECTOR)
+ {
+ vars.insert(n);
+ continue;
+ }
+ stack.insert(stack.end(), n.begin(), n.end());
+ }
+}
+
+};
+
+/* ------------------------------------------------------------------------- */
bool hasExpensiveBVOperators(TNode fact);
Node mergeExplanations(const std::vector<Node>& expls);
EqualityStatus AlgebraicSolver::getEqualityStatus(TNode a, TNode b) {
return EQUALITY_UNKNOWN;
}
+
bool AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel)
{
Debug("bitvector-model") << "AlgebraicSolver::collectModelInfo\n";
TNode subst = Rewriter::rewrite(d_modelMap->apply(current));
Debug("bitvector-model") << " " << current << " => " << subst << "\n";
values[i] = subst;
- utils::collectVariables(subst, leaf_vars);
+ collectVariables(subst, leaf_vars);
}
Debug("bitvector-model") << "Model:\n";
/* ------------------------------------------------------------------------- */
-void collectVariables(TNode node, NodeSet& vars)
-{
- if (vars.find(node) != vars.end()) return;
-
- if (Theory::isLeafOf(node, THEORY_BV)
- && node.getKind() != kind::CONST_BITVECTOR)
- {
- vars.insert(node);
- return;
- }
- for (unsigned i = 0; i < node.getNumChildren(); ++i)
- {
- collectVariables(node[i], vars);
- }
-}
-
-/* ------------------------------------------------------------------------- */
-
}/* CVC4::theory::bv::utils namespace */
}/* CVC4::theory::bv namespace */
}/* CVC4::theory namespace */
/*! \file theory_bv_utils.h
** \verbatim
** Top contributors (to current version):
- ** Aina Niemetz, Dejan Jovanovic, Morgan Deters
+ ** Aina Niemetz, Dejan Jovanovic, Tim King
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
const std::vector<uint32_t>& v2,
std::vector<uint32_t>& intersection);
-/* Collect all variables under a given a node. */
-void collectVariables(TNode node, NodeSet& vars);
-
}
}
}