summaryrefslogtreecommitdiff
path: root/src/preprocessing/passes
diff options
context:
space:
mode:
Diffstat (limited to 'src/preprocessing/passes')
-rw-r--r--src/preprocessing/passes/bool_to_bv.cpp200
-rw-r--r--src/preprocessing/passes/bool_to_bv.h64
-rw-r--r--src/preprocessing/passes/bv_to_bool.cpp310
-rw-r--r--src/preprocessing/passes/bv_to_bool.h79
4 files changed, 653 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
diff --git a/src/preprocessing/passes/bool_to_bv.h b/src/preprocessing/passes/bool_to_bv.h
new file mode 100644
index 000000000..e85693d1c
--- /dev/null
+++ b/src/preprocessing/passes/bool_to_bv.h
@@ -0,0 +1,64 @@
+/********************* */
+/*! \file bool_to_bv.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Clark Barrett, Paul Meng
+ ** 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 "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
+#define __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
+
+#include "preprocessing/passes/bv_to_bool.h"
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class BoolToBV : public PreprocessingPass
+{
+ public:
+ BoolToBV(PreprocessingPassContext* preprocContext);
+
+ protected:
+ PreprocessingPassResult applyInternal(
+ AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+ struct Statistics
+ {
+ IntStat d_numTermsLowered;
+ IntStat d_numAtomsLowered;
+ IntStat d_numTermsForcedLowered;
+ Statistics();
+ ~Statistics();
+ };
+
+ void lowerBoolToBv(const std::vector<Node>& assertions,
+ std::vector<Node>& new_assertions);
+ void addToLowerCache(TNode term, Node new_term);
+ Node getLowerCache(TNode term) const;
+ bool hasLowerCache(TNode term) const;
+ Node lowerNode(TNode current, bool topLevel = false);
+ Statistics d_statistics;
+ NodeNodeMap d_lowerCache;
+ Node d_one;
+ Node d_zero;
+}; // class
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H */
diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp
new file mode 100644
index 000000000..b01a60031
--- /dev/null
+++ b/src/preprocessing/passes/bv_to_bool.cpp
@@ -0,0 +1,310 @@
+/********************* */
+/*! \file bv_to_bool.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 Preprocessing pass that lifts bit-vectors of size 1 to booleans.
+ **
+ ** Preprocessing pass that lifts bit-vectors of size 1 to booleans.
+ **/
+
+#include "preprocessing/passes/bv_to_bool.h"
+
+#include <string>
+#include <unordered_map>
+#include <vector>
+
+#include "expr/node.h"
+#include "theory/rewriter.h"
+#include "theory/theory.h"
+
+#include "smt/smt_statistics_registry.h"
+#include "smt_util/node_visitor.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using namespace std;
+using namespace CVC4::theory;
+
+BVToBool::BVToBool(PreprocessingPassContext* preprocContext)
+ : PreprocessingPass(preprocContext, "bv-to-bool"),
+ d_liftCache(),
+ d_boolCache(),
+ d_one(bv::utils::mkOne(1)),
+ d_zero(bv::utils::mkZero(1)),
+ d_statistics(){};
+
+PreprocessingPassResult BVToBool::applyInternal(
+ AssertionPipeline* assertionsToPreprocess)
+{
+ NodeManager::currentResourceManager()->spendResource(
+ options::preprocessStep());
+ std::vector<Node> new_assertions;
+ liftBvToBool(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 BVToBool::addToLiftCache(TNode term, Node new_term)
+{
+ Assert(new_term != Node());
+ Assert(!hasLiftCache(term));
+ Assert(term.getType() == new_term.getType());
+ d_liftCache[term] = new_term;
+}
+
+Node BVToBool::getLiftCache(TNode term) const
+{
+ Assert(hasLiftCache(term));
+ return d_liftCache.find(term)->second;
+}
+
+bool BVToBool::hasLiftCache(TNode term) const
+{
+ return d_liftCache.find(term) != d_liftCache.end();
+}
+
+void BVToBool::addToBoolCache(TNode term, Node new_term)
+{
+ Assert(new_term != Node());
+ Assert(!hasBoolCache(term));
+ Assert(bv::utils::getSize(term) == 1);
+ Assert(new_term.getType().isBoolean());
+ d_boolCache[term] = new_term;
+}
+
+Node BVToBool::getBoolCache(TNode term) const
+{
+ Assert(hasBoolCache(term));
+ return d_boolCache.find(term)->second;
+}
+
+bool BVToBool::hasBoolCache(TNode term) const
+{
+ return d_boolCache.find(term) != d_boolCache.end();
+}
+bool BVToBool::isConvertibleBvAtom(TNode node)
+{
+ Kind kind = node.getKind();
+ return (kind == kind::EQUAL && node[0].getType().isBitVector()
+ && node[0].getType().getBitVectorSize() == 1
+ && node[1].getType().isBitVector()
+ && node[1].getType().getBitVectorSize() == 1
+ && node[0].getKind() != kind::BITVECTOR_EXTRACT
+ && node[1].getKind() != kind::BITVECTOR_EXTRACT);
+}
+
+bool BVToBool::isConvertibleBvTerm(TNode node)
+{
+ if (!node.getType().isBitVector() || node.getType().getBitVectorSize() != 1)
+ return false;
+
+ Kind kind = node.getKind();
+
+ if (kind == kind::CONST_BITVECTOR || kind == kind::ITE
+ || kind == kind::BITVECTOR_AND
+ || kind == kind::BITVECTOR_OR
+ || kind == kind::BITVECTOR_NOT
+ || kind == kind::BITVECTOR_XOR
+ || kind == kind::BITVECTOR_COMP)
+ {
+ return true;
+ }
+
+ return false;
+}
+
+Node BVToBool::convertBvAtom(TNode node)
+{
+ Assert(node.getType().isBoolean() && node.getKind() == kind::EQUAL);
+ Assert(bv::utils::getSize(node[0]) == 1);
+ Assert(bv::utils::getSize(node[1]) == 1);
+ Node a = convertBvTerm(node[0]);
+ Node b = convertBvTerm(node[1]);
+ Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, b);
+ Debug("bv-to-bool") << "BVToBool::convertBvAtom " << node << " => " << result
+ << "\n";
+
+ ++(d_statistics.d_numAtomsLifted);
+ return result;
+}
+
+Node BVToBool::convertBvTerm(TNode node)
+{
+ Assert(node.getType().isBitVector()
+ && node.getType().getBitVectorSize() == 1);
+
+ if (hasBoolCache(node)) return getBoolCache(node);
+
+ NodeManager* nm = NodeManager::currentNM();
+
+ if (!isConvertibleBvTerm(node))
+ {
+ ++(d_statistics.d_numTermsForcedLifted);
+ Node result = nm->mkNode(kind::EQUAL, node, d_one);
+ addToBoolCache(node, result);
+ Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
+ << result << "\n";
+ return result;
+ }
+
+ if (node.getNumChildren() == 0)
+ {
+ Assert(node.getKind() == kind::CONST_BITVECTOR);
+ Node result = node == d_one ? bv::utils::mkTrue() : bv::utils::mkFalse();
+ // addToCache(node, result);
+ Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
+ << result << "\n";
+ return result;
+ }
+
+ ++(d_statistics.d_numTermsLifted);
+
+ Kind kind = node.getKind();
+ if (kind == kind::ITE)
+ {
+ Node cond = liftNode(node[0]);
+ Node true_branch = convertBvTerm(node[1]);
+ Node false_branch = convertBvTerm(node[2]);
+ Node result = nm->mkNode(kind::ITE, cond, true_branch, false_branch);
+ addToBoolCache(node, result);
+ Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
+ << result << "\n";
+ return result;
+ }
+
+ Kind new_kind;
+ // special case for XOR as it has to be binary
+ // while BITVECTOR_XOR can be n-ary
+ if (kind == kind::BITVECTOR_XOR)
+ {
+ new_kind = kind::XOR;
+ Node result = convertBvTerm(node[0]);
+ for (unsigned i = 1; i < node.getNumChildren(); ++i)
+ {
+ Node converted = convertBvTerm(node[i]);
+ result = nm->mkNode(kind::XOR, result, converted);
+ }
+ Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
+ << result << "\n";
+ return result;
+ }
+
+ if (kind == kind::BITVECTOR_COMP)
+ {
+ Node result = nm->mkNode(kind::EQUAL, node[0], node[1]);
+ addToBoolCache(node, result);
+ Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
+ << result << "\n";
+ return result;
+ }
+
+ switch (kind)
+ {
+ case kind::BITVECTOR_OR: new_kind = kind::OR; break;
+ case kind::BITVECTOR_AND: new_kind = kind::AND; break;
+ case kind::BITVECTOR_XOR: new_kind = kind::XOR; break;
+ case kind::BITVECTOR_NOT: new_kind = kind::NOT; break;
+ default: Unhandled();
+ }
+
+ NodeBuilder<> builder(new_kind);
+ for (unsigned i = 0; i < node.getNumChildren(); ++i)
+ {
+ builder << convertBvTerm(node[i]);
+ }
+
+ Node result = builder;
+ addToBoolCache(node, result);
+ Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => " << result
+ << "\n";
+ return result;
+}
+
+Node BVToBool::liftNode(TNode current)
+{
+ Node result;
+
+ if (hasLiftCache(current))
+ {
+ result = getLiftCache(current);
+ }
+ else if (isConvertibleBvAtom(current))
+ {
+ result = convertBvAtom(current);
+ addToLiftCache(current, result);
+ }
+ else
+ {
+ if (current.getNumChildren() == 0)
+ {
+ result = current;
+ }
+ else
+ {
+ NodeBuilder<> builder(current.getKind());
+ if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
+ {
+ builder << current.getOperator();
+ }
+ for (unsigned i = 0; i < current.getNumChildren(); ++i)
+ {
+ Node converted = liftNode(current[i]);
+ Assert(converted.getType() == current[i].getType());
+ builder << converted;
+ }
+ result = builder;
+ addToLiftCache(current, result);
+ }
+ }
+ Assert(result != Node());
+ Assert(result.getType() == current.getType());
+ Debug("bv-to-bool") << "BVToBool::liftNode " << current << " => \n"
+ << result << "\n";
+ return result;
+}
+
+void BVToBool::liftBvToBool(const std::vector<Node>& assertions,
+ std::vector<Node>& new_assertions)
+{
+ for (unsigned i = 0; i < assertions.size(); ++i)
+ {
+ Node new_assertion = liftNode(assertions[i]);
+ new_assertions.push_back(Rewriter::rewrite(new_assertion));
+ Trace("bv-to-bool") << " " << assertions[i] << " => " << new_assertions[i]
+ << "\n";
+ }
+}
+
+BVToBool::Statistics::Statistics()
+ : d_numTermsLifted("preprocessing::passes::BVToBool::NumTermsLifted", 0),
+ d_numAtomsLifted("preprocessing::passes::BVToBool::NumAtomsLifted", 0),
+ d_numTermsForcedLifted(
+ "preprocessing::passes::BVToBool::NumTermsForcedLifted", 0)
+{
+ smtStatisticsRegistry()->registerStat(&d_numTermsLifted);
+ smtStatisticsRegistry()->registerStat(&d_numAtomsLifted);
+ smtStatisticsRegistry()->registerStat(&d_numTermsForcedLifted);
+}
+
+BVToBool::Statistics::~Statistics()
+{
+ smtStatisticsRegistry()->unregisterStat(&d_numTermsLifted);
+ smtStatisticsRegistry()->unregisterStat(&d_numAtomsLifted);
+ smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLifted);
+}
+
+} // passes
+} // Preprocessing
+} // CVC4
diff --git a/src/preprocessing/passes/bv_to_bool.h b/src/preprocessing/passes/bv_to_bool.h
new file mode 100644
index 000000000..f772087e8
--- /dev/null
+++ b/src/preprocessing/passes/bv_to_bool.h
@@ -0,0 +1,79 @@
+/********************* */
+/*! \file bv_to_bool.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Clark Barrett, Paul Meng
+ ** 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 Preprocessing pass that lifts bit-vectors of size 1 to booleans.
+ **
+ ** Preprocessing pass that lifts bit-vectors of size 1 to booleans.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H
+#define __CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
+
+class BVToBool : public PreprocessingPass
+{
+
+ public:
+ BVToBool(PreprocessingPassContext* preprocContext);
+
+ protected:
+ PreprocessingPassResult applyInternal(
+ AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+ struct Statistics
+ {
+ IntStat d_numTermsLifted;
+ IntStat d_numAtomsLifted;
+ IntStat d_numTermsForcedLifted;
+ Statistics();
+ ~Statistics();
+ };
+ void addToBoolCache(TNode term, Node new_term);
+ Node getBoolCache(TNode term) const;
+ bool hasBoolCache(TNode term) const;
+
+ void addToLiftCache(TNode term, Node new_term);
+ Node getLiftCache(TNode term) const;
+ bool hasLiftCache(TNode term) const;
+
+ bool isConvertibleBvTerm(TNode node);
+ bool isConvertibleBvAtom(TNode node);
+ Node convertBvAtom(TNode node);
+ Node convertBvTerm(TNode node);
+ Node liftNode(TNode current);
+ void liftBvToBool(const std::vector<Node>& assertions,
+ std::vector<Node>& new_assertions);
+
+ Statistics d_statistics;
+ NodeNodeMap d_liftCache;
+ NodeNodeMap d_boolCache;
+ Node d_one;
+ Node d_zero;
+};
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback