#include "base/map_util.h"
#include "expr/node.h"
-#include "options/bv_options.h"
#include "smt/smt_statistics_registry.h"
#include "theory/rewriter.h"
#include "theory/theory.h"
using namespace CVC4::theory;
BoolToBV::BoolToBV(PreprocessingPassContext* preprocContext)
- : PreprocessingPass(preprocContext, "bool-to-bv"), d_statistics(){};
+ : PreprocessingPass(preprocContext, "bool-to-bv"), d_statistics()
+{
+ d_boolToBVMode = options::boolToBitvector();
+};
PreprocessingPassResult BoolToBV::applyInternal(
AssertionPipeline* assertionsToPreprocess)
NodeManager::currentResourceManager()->spendResource(
ResourceManager::Resource::PreprocessStep);
- unsigned size = assertionsToPreprocess->size();
- for (unsigned i = 0; i < size; ++i)
+ size_t size = assertionsToPreprocess->size();
+
+ if (d_boolToBVMode == options::BoolToBVMode::ALL)
+ {
+ for (size_t i = 0; i < size; ++i)
+ {
+ Node newAssertion = lowerAssertion((*assertionsToPreprocess)[i], true);
+ assertionsToPreprocess->replace(i, Rewriter::rewrite(newAssertion));
+ }
+ }
+ else
{
- assertionsToPreprocess->replace(
- i, Rewriter::rewrite(lowerAssertion((*assertionsToPreprocess)[i])));
+ Assert(d_boolToBVMode == options::BoolToBVMode::ITE);
+ for (size_t i = 0; i < size; ++i)
+ {
+ assertionsToPreprocess->replace(
+ i, Rewriter::rewrite(lowerIte((*assertionsToPreprocess)[i])));
+ }
}
return PreprocessingPassResult::NO_CONFLICT;
}
+void BoolToBV::updateCache(TNode n, TNode rebuilt)
+{
+ // check more likely case first
+ if ((n.getKind() != kind::ITE) || !n[1].getType().isBitVector())
+ {
+ d_lowerCache[n] = rebuilt;
+ }
+ else
+ {
+ d_iteBVLowerCache[n] = rebuilt;
+ }
+}
+
Node BoolToBV::fromCache(TNode n) const
{
- if (d_lowerCache.find(n) != d_lowerCache.end())
+ // check more likely case first
+ if (n.getKind() != kind::ITE)
{
- return d_lowerCache.find(n)->second;
+ if (d_lowerCache.find(n) != d_lowerCache.end())
+ {
+ return d_lowerCache.at(n);
+ }
+ }
+ else
+ {
+ if (d_iteBVLowerCache.find(n) != d_iteBVLowerCache.end())
+ {
+ return d_iteBVLowerCache.at(n);
+ }
}
return n;
}
+inline bool BoolToBV::inCache(const Node& n) const
+{
+ return (ContainsKey(d_lowerCache, n) || ContainsKey(d_iteBVLowerCache, n));
+}
+
bool BoolToBV::needToRebuild(TNode n) const
{
// check if any children were rebuilt
for (const Node& nn : n)
{
- if (ContainsKey(d_lowerCache, nn))
+ if (inCache(nn))
{
return true;
}
return false;
}
-Node BoolToBV::lowerAssertion(const TNode& a)
+Node BoolToBV::lowerAssertion(const TNode& assertion, bool allowIteIntroduction)
{
- bool optionITE = options::boolToBitvector() == options::BoolToBVMode::ITE;
- NodeManager* nm = NodeManager::currentNM();
- std::vector<TNode> visit;
- visit.push_back(a);
+ // first try to lower all the children
+ for (const Node& c : assertion)
+ {
+ lowerNode(c, allowIteIntroduction);
+ }
+
+ // now try lowering the assertion, but don't force it with an ITE (even in mode all)
+ lowerNode(assertion, false);
+ Node newAssertion = fromCache(assertion);
+ TypeNode newAssertionType = newAssertion.getType();
+ if (newAssertionType.isBitVector())
+ {
+ Assert(newAssertionType.getBitVectorSize() == 1);
+ newAssertion = NodeManager::currentNM()->mkNode(
+ kind::EQUAL, newAssertion, bv::utils::mkOne(1));
+ newAssertionType = newAssertion.getType();
+ }
+ Assert(newAssertionType.isBoolean());
+ return newAssertion;
+}
+
+Node BoolToBV::lowerNode(const TNode& node, bool allowIteIntroduction)
+{
+ std::vector<TNode> to_visit;
+ to_visit.push_back(node);
std::unordered_set<TNode, TNodeHashFunction> visited;
- // for ite mode, keeps track of whether you're in an ite condition
- // for all mode, unused
- std::unordered_set<TNode, TNodeHashFunction> ite_cond;
- while (!visit.empty())
+ while (!to_visit.empty())
{
- TNode n = visit.back();
- visit.pop_back();
+ TNode n = to_visit.back();
+ to_visit.pop_back();
- int numChildren = n.getNumChildren();
- Kind k = n.getKind();
- Debug("bool-to-bv") << "BoolToBV::lowerAssertion Post-traversal with " << n
- << " and visited = " << ContainsKey(visited, n)
+ Debug("bool-to-bv") << "BoolToBV::lowerNode: Post-order traversal with "
+ << n << " and visited = " << ContainsKey(visited, n)
<< std::endl;
// Mark as visited
- /* Optimization: if it's a leaf, don't need to wait to do the work */
- if (!ContainsKey(visited, n) && (numChildren > 0))
+ if (ContainsKey(visited, n))
+ {
+ visit(n, allowIteIntroduction);
+ }
+ else
{
visited.insert(n);
- visit.push_back(n);
+ to_visit.push_back(n);
// insert children in reverse order so that they're processed in order
- // important for rewriting which sorts by node id
- for (int i = numChildren - 1; i >= 0; --i)
+ // important for rewriting which sorts by node id
+ // NOTE: size_t is unsigned, so using underflow for termination condition
+ size_t numChildren = n.getNumChildren();
+ for (size_t i = numChildren - 1; i < numChildren; --i)
{
- visit.push_back(n[i]);
- }
-
- if (optionITE)
- {
- // check for ite-conditions
- if (k == kind::ITE)
- {
- ite_cond.insert(n[0]);
- }
- else if (ContainsKey(ite_cond, n))
- {
- // being part of an ite condition is inherited from the parent
- ite_cond.insert(n.begin(), n.end());
- }
+ to_visit.push_back(n[i]);
}
}
- /* Optimization for ite mode */
- else if (optionITE && !ContainsKey(ite_cond, n) && !needToRebuild(n))
- {
- Debug("bool-to-bv")
- << "BoolToBV::lowerAssertion Skipping because don't need to rebuild: "
- << n << std::endl;
- // in ite mode, if you've already visited the node but it's not
- // in an ite condition and doesn't need to be rebuilt, then
- // don't need to do anything
- continue;
- }
- else
- {
- lowerNode(n);
- }
}
- if (fromCache(a).getType().isBitVector())
- {
- return nm->mkNode(kind::EQUAL, fromCache(a), bv::utils::mkOne(1));
- }
- else
- {
- Assert(a == fromCache(a));
- return a;
- }
+ return fromCache(node);
}
-void BoolToBV::lowerNode(const TNode& n)
+void BoolToBV::visit(const TNode& n, bool allowIteIntroduction)
{
- NodeManager* nm = NodeManager::currentNM();
Kind k = n.getKind();
- bool all_bv = true;
- // check if it was able to convert all children to bitvectors
- for (const Node& nn : n)
+ // easy case -- just replace boolean constant
+ if (k == kind::CONST_BOOLEAN)
{
- all_bv = all_bv && fromCache(nn).getType().isBitVector();
- if (!all_bv)
- {
- break;
- }
- }
-
- if (!all_bv || (n.getNumChildren() == 0))
- {
- if ((options::boolToBitvector() == options::BoolToBVMode::ALL)
- && n.getType().isBoolean())
- {
- if (k == kind::CONST_BOOLEAN)
- {
- d_lowerCache[n] = (n == bv::utils::mkTrue()) ? bv::utils::mkOne(1)
- : bv::utils::mkZero(1);
- }
- else
- {
- d_lowerCache[n] =
- nm->mkNode(kind::ITE, n, bv::utils::mkOne(1), bv::utils::mkZero(1));
- }
-
- Debug("bool-to-bv") << "BoolToBV::lowerNode " << n << " =>\n"
- << fromCache(n) << std::endl;
- ++(d_statistics.d_numTermsForcedLowered);
- return;
- }
- else
- {
- // invariant
- // either one of the children is not a bit-vector or bool
- // i.e. something that can't be 'forced' to a bitvector
- // or it's in 'ite' mode which will give up on bools that
- // can't be converted easily
-
- Debug("bool-to-bv") << "BoolToBV::lowerNode skipping: " << n << std::endl;
- return;
- }
+ updateCache(n,
+ (n == bv::utils::mkTrue()) ? bv::utils::mkOne(1)
+ : bv::utils::mkZero(1));
+ return;
}
+ NodeManager* nm = NodeManager::currentNM();
Kind new_kind = k;
switch (k)
{
default: break;
}
+ // check if it's safe to lower or rebuild the node
+ // Note: might have to rebuild to keep changes to children, even if this node
+ // isn't being lowered
+
+ // it's safe to lower if all the children are bit-vectors
+ bool safe_to_lower =
+ (new_kind != k); // don't need to lower at all if kind hasn't changed
+
+ // it's safe to rebuild if rebuilding doesn't change any of the types of the
+ // children
+ bool safe_to_rebuild = true;
+
+ for (const Node& nn : n)
+ {
+ safe_to_lower = safe_to_lower && fromCache(nn).getType().isBitVector();
+ safe_to_rebuild = safe_to_rebuild && (fromCache(nn).getType() == nn.getType());
+
+ // if it's already not safe to do either, stop checking
+ if (!safe_to_lower && !safe_to_rebuild)
+ {
+ break;
+ }
+ }
+
+ Debug("bool-to-bv") << "safe_to_lower = " << safe_to_lower
+ << ", safe_to_rebuild = " << safe_to_rebuild << std::endl;
+
+ if (new_kind != k && safe_to_lower)
+ {
+ // lower to BV
+ rebuildNode(n, new_kind);
+ return;
+ }
+ else if (new_kind != k && allowIteIntroduction && fromCache(n).getType().isBoolean())
+ {
+ // lower to BV using an ITE
+
+ if (safe_to_rebuild && needToRebuild(n))
+ {
+ // need to rebuild to keep changes made to descendants
+ rebuildNode(n, k);
+ }
+
+ updateCache(n,
+ nm->mkNode(kind::ITE,
+ fromCache(n),
+ bv::utils::mkOne(1),
+ bv::utils::mkZero(1)));
+ Debug("bool-to-bv") << "BoolToBV::visit forcing " << n
+ << " =>\n"
+ << fromCache(n) << std::endl;
+ ++(d_statistics.d_numIntroducedItes);
+ return;
+ }
+ else if (safe_to_rebuild && needToRebuild(n))
+ {
+ // rebuild to incorporate changes to children
+ Assert(k == new_kind);
+ rebuildNode(n, k);
+ }
+ else if (allowIteIntroduction && fromCache(n).getType().isBoolean())
+ {
+ // force booleans (which haven't already been converted) to bit-vector
+ // needed to maintain the invariant that all boolean children
+ // have been converted (even constants and variables) when forcing
+ // with ITE introductions
+ updateCache(
+ n, nm->mkNode(kind::ITE, n, bv::utils::mkOne(1), bv::utils::mkZero(1)));
+ Debug("bool-to-bv") << "BoolToBV::visit forcing " << n
+ << " =>\n"
+ << fromCache(n) << std::endl;
+ ++(d_statistics.d_numIntroducedItes);
+ }
+ else
+ {
+ // do nothing
+ Debug("bool-to-bv") << "BoolToBV::visit skipping: " << n
+ << std::endl;
+ }
+}
+
+Node BoolToBV::lowerIte(const TNode& node)
+{
+ std::vector<TNode> visit;
+ visit.push_back(node);
+ std::unordered_set<TNode, TNodeHashFunction> visited;
+
+ while (!visit.empty())
+ {
+ TNode n = visit.back();
+ visit.pop_back();
+
+ Debug("bool-to-bv") << "BoolToBV::lowerIte: Post-order traversal with " << n
+ << " and visited = " << ContainsKey(visited, n)
+ << std::endl;
+
+ // Look for ITEs and mark visited
+ if (!ContainsKey(visited, n))
+ {
+ if ((n.getKind() == kind::ITE) && n[1].getType().isBitVector())
+ {
+ Debug("bool-to-bv") << "BoolToBV::lowerIte: adding " << n[0]
+ << " to set of ite conditions" << std::endl;
+ // don't force in this case -- forcing only introduces more ITEs
+ Node loweredNode = lowerNode(n, false);
+ // some of the lowered nodes might appear elsewhere but not in an ITE
+ // reset the cache to prevent lowering them
+ // the bit-vector ITEs are still tracked in d_iteBVLowerCache though
+ d_lowerCache.clear();
+ }
+ else
+ {
+ visit.push_back(n);
+ visited.insert(n);
+ // insert in reverse order so that they're processed in order
+ for (int i = n.getNumChildren() - 1; i >= 0; --i)
+ {
+ visit.push_back(n[i]);
+ }
+ }
+ }
+ else if (needToRebuild(n))
+ {
+ // Note: it's always safe to rebuild here, because we've only lowered
+ // ITEs of type bit-vector to BITVECTOR_ITE
+ rebuildNode(n, n.getKind());
+ }
+ else
+ {
+ Debug("bool-to-bv")
+ << "BoolToBV::lowerIte Skipping because don't need to rebuild: " << n
+ << std::endl;
+ }
+ }
+ return fromCache(node);
+}
+
+void BoolToBV::rebuildNode(const TNode& n, Kind new_kind)
+{
+ Kind k = n.getKind();
+ NodeManager* nm = NodeManager::currentNM();
NodeBuilder<> builder(new_kind);
- if ((options::boolToBitvector() == options::BoolToBVMode::ALL)
- && (new_kind != k))
+
+ Debug("bool-to-bv") << "BoolToBV::rebuildNode with " << n
+ << " and new_kind = " << kindToString(new_kind)
+ << std::endl;
+
+ if ((d_boolToBVMode == options::BoolToBVMode::ALL) && (new_kind != k))
{
++(d_statistics.d_numTermsLowered);
}
}
// special case IMPLIES because needs to be rewritten
- if (k == kind::IMPLIES)
+ if ((k == kind::IMPLIES) && (new_kind != k))
{
builder << nm->mkNode(kind::BITVECTOR_NOT, fromCache(n[0]));
builder << fromCache(n[1]);
}
}
- Debug("bool-to-bv") << "BoolToBV::lowerNode " << n << " =>\n"
+ Debug("bool-to-bv") << "BoolToBV::rebuildNode " << n << " =>\n"
<< builder << std::endl;
- d_lowerCache[n] = builder.constructNode();
+ updateCache(n, builder.constructNode());
}
BoolToBV::Statistics::Statistics()
: d_numIteToBvite("preprocessing::passes::BoolToBV::NumIteToBvite", 0),
d_numTermsLowered("preprocessing::passes:BoolToBV::NumTermsLowered", 0),
- d_numTermsForcedLowered(
+ d_numIntroducedItes(
"preprocessing::passes::BoolToBV::NumTermsForcedLowered", 0)
{
smtStatisticsRegistry()->registerStat(&d_numIteToBvite);
// because it might discard rebuilt nodes if it fails to
// convert a bool to width-one bit-vector (never forces)
smtStatisticsRegistry()->registerStat(&d_numTermsLowered);
- smtStatisticsRegistry()->registerStat(&d_numTermsForcedLowered);
+ smtStatisticsRegistry()->registerStat(&d_numIntroducedItes);
}
}
if (options::boolToBitvector() == options::BoolToBVMode::ALL)
{
smtStatisticsRegistry()->unregisterStat(&d_numTermsLowered);
- smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLowered);
+ smtStatisticsRegistry()->unregisterStat(&d_numIntroducedItes);
}
}
#ifndef CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
#define CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
+#include "options/bv_options.h"
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "theory/bv/theory_bv_utils.h"
{
IntStat d_numIteToBvite;
IntStat d_numTermsLowered;
- IntStat d_numTermsForcedLowered;
+ IntStat d_numIntroducedItes;
Statistics();
~Statistics();
};
- /* Takes an assertion and tries to create more bit-vector structure */
- Node lowerAssertion(const TNode& a);
+ /** Takes an assertion and attempts to create more bit-vector structure
+ by replacing boolean operators with bit-vector operators.
- /* Tries to lower one node to a width-one bit-vector */
- void lowerNode(const TNode& n);
+ It passes the allowIteIntroduction argument down to lowerNode, however it
+ never allows ite introduction in the top-level assertion. There's no point
+ forcing the assertion to be a bit-vector when it will just be converted
+ back into a boolean.
+ */
+ Node lowerAssertion(const TNode& node, bool allowIteIntroduction = false);
+
+ /** Traverses subterms to turn booleans into bit-vectors using visit
+ * Passes the allowIteIntroduction argument to visit
+ * Returns the lowered node
+ */
+ Node lowerNode(const TNode& node, bool allowIteIntroduction = false);
+
+ /** Tries to lower one node to a width-one bit-vector
+ * Caches the result if successful
+ *
+ * allowIteIntroduction = true causes booleans to be converted to bit-vectors
+ * using an ITE this is only used by mode ALL currently, but could
+ * conceivably be used in new modes.
+ */
+ void visit(const TNode& n, bool allowIteIntroduction = false);
+
+ /* Traverses formula looking for ITEs to lower to BITVECTOR_ITE using
+ * lowerNode*/
+ Node lowerIte(const TNode& node);
+
+ /** Rebuilds node using the provided kind
+ * Note: The provided kind is not necessarily different from the
+ * existing one, but still might need to be rebuilt because
+ * of subterms
+ */
+ void rebuildNode(const TNode& n, Kind new_kind);
+
+ /** Updates the cache, the cache is actually supported by two maps
+ one for ITEs and one for everything else
+
+ This is necessary so that when in ITE mode, the regular cache
+ can be cleared to prevent lowering boolean operators that are
+ not in an ITE
+ */
+ void updateCache(TNode n, TNode rebuilt);
/* Returns cached node if it exists, otherwise returns the node */
Node fromCache(TNode n) const;
- /** Checks if any of the nodes children were rebuilt,
+ /* Checks both caches for membership */
+ bool inCache(const Node& n) const;
+
+ /** Checks if any of the node's children were rebuilt,
* in which case n needs to be rebuilt as well
*/
bool needToRebuild(TNode n) const;
Statistics d_statistics;
- /* Keeps track of lowered nodes */
+ /** Keeps track of lowered ITEs
+ Note: it only keeps mappings for ITEs of type bit-vector.
+ Other ITEs will be in the d_lowerCache
+ */
+ std::unordered_map<Node, Node, NodeHashFunction> d_iteBVLowerCache;
+
+ /** Keeps track of other lowered nodes
+ -- will be cleared periodically in ITE mode
+ */
std::unordered_map<Node, Node, NodeHashFunction> d_lowerCache;
+
+ /** Stores the bool-to-bv mode option */
+ options::BoolToBVMode d_boolToBVMode;
}; // class BoolToBV
} // namespace passes
projects / cvc5.git / commitdiff