diff options
Diffstat (limited to 'src/preprocessing/passes/bool_to_bv.cpp')
| -rw-r--r-- | src/preprocessing/passes/bool_to_bv.cpp | 200 |
1 files changed, 200 insertions, 0 deletions
diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp new file mode 100644 index 000000000..511f09a71 --- /dev/null +++ b/src/preprocessing/passes/bool_to_bv.cpp @@ -0,0 +1,200 @@ +/********************* */ +/*! \file bool_to_bv.cpp + ** \verbatim + ** Top contributors (to current version): + ** Liana Hadarean, Aina Niemetz, Clark Barrett + ** 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. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The BoolToBv preprocessing pass + ** + **/ + +#include "preprocessing/passes/bool_to_bv.h" + +#include <string> +#include <unordered_map> +#include <vector> + +#include "expr/node.h" +#include "smt/smt_statistics_registry.h" +#include "theory/rewriter.h" +#include "theory/theory.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { +using namespace CVC4::theory; + +BoolToBV::BoolToBV(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "bool-to-bv"), + d_lowerCache(), + d_one(bv::utils::mkOne(1)), + d_zero(bv::utils::mkZero(1)), + d_statistics(){}; + +PreprocessingPassResult BoolToBV::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + NodeManager::currentResourceManager()->spendResource( + options::preprocessStep()); + std::vector<Node> new_assertions; + lowerBoolToBv(assertionsToPreprocess->ref(), new_assertions); + for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) + { + assertionsToPreprocess->replace(i, Rewriter::rewrite(new_assertions[i])); + } + return PreprocessingPassResult::NO_CONFLICT; +} + +void BoolToBV::addToLowerCache(TNode term, Node new_term) +{ + Assert(new_term != Node()); + Assert(!hasLowerCache(term)); + d_lowerCache[term] = new_term; +} + +Node BoolToBV::getLowerCache(TNode term) const +{ + Assert(hasLowerCache(term)); + return d_lowerCache.find(term)->second; +} + +bool BoolToBV::hasLowerCache(TNode term) const +{ + return d_lowerCache.find(term) != d_lowerCache.end(); +} + +Node BoolToBV::lowerNode(TNode current, bool topLevel) +{ + Node result; + NodeManager* nm = NodeManager::currentNM(); + if (hasLowerCache(current)) + { + result = getLowerCache(current); + } + else + { + if (current.getNumChildren() == 0) + { + if (current.getKind() == kind::CONST_BOOLEAN) + { + result = (current == bv::utils::mkTrue()) ? d_one : d_zero; + } + else + { + result = current; + } + } + else + { + Kind kind = current.getKind(); + Kind new_kind = kind; + switch (kind) + { + case kind::EQUAL: new_kind = kind::BITVECTOR_COMP; break; + case kind::AND: new_kind = kind::BITVECTOR_AND; break; + case kind::OR: new_kind = kind::BITVECTOR_OR; break; + case kind::NOT: new_kind = kind::BITVECTOR_NOT; break; + case kind::XOR: new_kind = kind::BITVECTOR_XOR; break; + case kind::ITE: + if (current.getType().isBitVector() || current.getType().isBoolean()) + { + new_kind = kind::BITVECTOR_ITE; + } + break; + case kind::BITVECTOR_ULT: new_kind = kind::BITVECTOR_ULTBV; break; + case kind::BITVECTOR_SLT: new_kind = kind::BITVECTOR_SLTBV; break; + case kind::BITVECTOR_ULE: + case kind::BITVECTOR_UGT: + case kind::BITVECTOR_UGE: + case kind::BITVECTOR_SLE: + case kind::BITVECTOR_SGT: + case kind::BITVECTOR_SGE: + // Should have been removed by rewriting. + Unreachable(); + default: break; + } + NodeBuilder<> builder(new_kind); + if (kind != new_kind) + { + ++(d_statistics.d_numTermsLowered); + } + if (current.getMetaKind() == kind::metakind::PARAMETERIZED) + { + builder << current.getOperator(); + } + Node converted; + if (new_kind == kind::ITE) + { + // Special-case ITE because need condition to be Boolean. + converted = lowerNode(current[0], true); + builder << converted; + converted = lowerNode(current[1]); + builder << converted; + converted = lowerNode(current[2]); + builder << converted; + } + else + { + for (unsigned i = 0; i < current.getNumChildren(); ++i) + { + converted = lowerNode(current[i]); + builder << converted; + } + } + result = builder; + } + if (result.getType().isBoolean()) + { + ++(d_statistics.d_numTermsForcedLowered); + result = nm->mkNode(kind::ITE, result, d_one, d_zero); + } + addToLowerCache(current, result); + } + if (topLevel) + { + result = nm->mkNode(kind::EQUAL, result, d_one); + } + Assert(result != Node()); + Debug("bool-to-bv") << "BoolToBV::lowerNode " << current << " => \n" + << result << "\n"; + return result; +} + +void BoolToBV::lowerBoolToBv(const std::vector<Node>& assertions, + std::vector<Node>& new_assertions) +{ + for (unsigned i = 0; i < assertions.size(); ++i) + { + Node new_assertion = lowerNode(assertions[i], true); + new_assertions.push_back(new_assertion); + Trace("bool-to-bv") << " " << assertions[i] << " => " << new_assertions[i] + << "\n"; + } +} + +BoolToBV::Statistics::Statistics() + : d_numTermsLowered("preprocessing::passes::BoolToBV::NumTermsLowered", 0), + d_numAtomsLowered("preprocessing::passes::BoolToBV::NumAtomsLowered", 0), + d_numTermsForcedLowered( + "preprocessing::passes::BoolToBV::NumTermsForcedLowered", 0) +{ + smtStatisticsRegistry()->registerStat(&d_numTermsLowered); + smtStatisticsRegistry()->registerStat(&d_numAtomsLowered); + smtStatisticsRegistry()->registerStat(&d_numTermsForcedLowered); +} + +BoolToBV::Statistics::~Statistics() +{ + smtStatisticsRegistry()->unregisterStat(&d_numTermsLowered); + smtStatisticsRegistry()->unregisterStat(&d_numAtomsLowered); + smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLowered); +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 |