Refactor bv-to-bool and bool-to-bv preprocessing passes (#1788)

2 files changed, 0 insertions, 473 deletions

diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
deleted file mode 100644
index 54c9cb08a..000000000
--- a/src/theory/bv/bv_to_bool.cpp
+++ /dev/null
@@ -1,387 +0,0 @@
-/*********************                                                        */
-/*! \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 "theory/bv/bv_to_bool.h"
-
-#include "smt_util/node_visitor.h"
-#include "smt/smt_statistics_registry.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv;
-
-BvToBoolPreprocessor::BvToBoolPreprocessor()
-  : d_liftCache()
-  , d_boolCache()
-  , d_one(utils::mkOne(1))
-  , d_zero(utils::mkZero(1))
-  , d_statistics()
-{}
-
-void BvToBoolPreprocessor::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 BvToBoolPreprocessor::getLiftCache(TNode term) const {
-  Assert(hasLiftCache(term)); 
-  return d_liftCache.find(term)->second; 
-}
-
-bool BvToBoolPreprocessor::hasLiftCache(TNode term) const {
-  return d_liftCache.find(term) != d_liftCache.end(); 
-}
-
-void BvToBoolPreprocessor::addToBoolCache(TNode term, Node new_term) {
-  Assert (new_term != Node()); 
-  Assert (!hasBoolCache(term));
-  Assert (utils::getSize(term) == 1);
-  Assert (new_term.getType().isBoolean());
-  d_boolCache[term] = new_term; 
-}
-
-Node BvToBoolPreprocessor::getBoolCache(TNode term) const {
-  Assert(hasBoolCache(term)); 
-  return d_boolCache.find(term)->second; 
-}
-
-bool BvToBoolPreprocessor::hasBoolCache(TNode term) const {
-  return d_boolCache.find(term) != d_boolCache.end(); 
-}
-bool BvToBoolPreprocessor::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 BvToBoolPreprocessor::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 BvToBoolPreprocessor::convertBvAtom(TNode node)
-{
-  Assert(node.getType().isBoolean() && node.getKind() == kind::EQUAL);
-  Assert(utils::getSize(node[0]) == 1);
-  Assert(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") << "BvToBoolPreprocessor::convertBvAtom " << node
-                      << " => " << result << "\n";
-
-  ++(d_statistics.d_numAtomsLifted);
-  return result;
-}
-
-Node BvToBoolPreprocessor::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") << "BvToBoolPreprocessor::convertBvTerm " << node
-                        << " => " << result << "\n";
-    return result;
-  }
-
-  if (node.getNumChildren() == 0)
-  {
-    Assert(node.getKind() == kind::CONST_BITVECTOR);
-    Node result = node == d_one ? utils::mkTrue() : utils::mkFalse();
-    // addToCache(node, result);
-    Debug("bv-to-bool") << "BvToBoolPreprocessor::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") << "BvToBoolPreprocessor::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") << "BvToBoolPreprocessor::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") << "BvToBoolPreprocessor::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") << "BvToBoolPreprocessor::convertBvTerm " << node
-                      << " => " << result << "\n";
-  return result;
-}
-
-Node BvToBoolPreprocessor::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") << "BvToBoolPreprocessor::liftNode " << current << " => \n" << result << "\n"; 
-  return result; 
-}
-
-void BvToBoolPreprocessor::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(new_assertion);
-    Trace("bv-to-bool") << "  " << assertions[i] <<" => " << new_assertions[i] <<"\n"; 
-  }
-}
-
-BvToBoolPreprocessor::Statistics::Statistics()
-  : d_numTermsLifted("theory::bv::BvToBool::NumTermsLifted", 0)
-  , d_numAtomsLifted("theory::bv::BvToBool::NumAtomsLifted", 0)
-  , d_numTermsForcedLifted("theory::bv::BvToBool::NumTermsForcedLifted", 0)
-  , d_numTermsLowered("theory::bv::BvToBool::NumTermsLowered", 0)
-  , d_numAtomsLowered("theory::bv::BvToBool::NumAtomsLowered", 0)
-  , d_numTermsForcedLowered("theory::bv::BvToBool::NumTermsForcedLowered", 0)
-{
-  smtStatisticsRegistry()->registerStat(&d_numTermsLifted);
-  smtStatisticsRegistry()->registerStat(&d_numAtomsLifted);
-  smtStatisticsRegistry()->registerStat(&d_numTermsForcedLifted);
-  smtStatisticsRegistry()->registerStat(&d_numTermsLowered);
-  smtStatisticsRegistry()->registerStat(&d_numAtomsLowered);
-  smtStatisticsRegistry()->registerStat(&d_numTermsForcedLowered);
-}
-
-BvToBoolPreprocessor::Statistics::~Statistics() {
-  smtStatisticsRegistry()->unregisterStat(&d_numTermsLifted);
-  smtStatisticsRegistry()->unregisterStat(&d_numAtomsLifted);
-  smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLifted);
-  smtStatisticsRegistry()->unregisterStat(&d_numTermsLowered);
-  smtStatisticsRegistry()->unregisterStat(&d_numAtomsLowered);
-  smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLowered);
-}
-
-void BvToBoolPreprocessor::addToLowerCache(TNode term, Node new_term) {
-  Assert (new_term != Node());
-  Assert (!hasLowerCache(term));
-  d_lowerCache[term] = new_term; 
-}
-
-Node BvToBoolPreprocessor::getLowerCache(TNode term) const {
-  Assert(hasLowerCache(term)); 
-  return d_lowerCache.find(term)->second; 
-}
-
-bool BvToBoolPreprocessor::hasLowerCache(TNode term) const {
-  return d_lowerCache.find(term) != d_lowerCache.end(); 
-}
-
-Node BvToBoolPreprocessor::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 == 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") << "BvToBoolPreprocessor::lowerNode " << current
-                      << " => \n"
-                      << result << "\n";
-  return result;
-}
-
-void BvToBoolPreprocessor::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"; 
-  }
-}
diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h
deleted file mode 100644
index 93a83626e..000000000
--- a/src/theory/bv/bv_to_bool.h
+++ /dev/null
@@ -1,86 +0,0 @@
-/*********************                                                        */
-/*! \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-2017 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__THEORY__BV__BV_TO_BOOL_H
-#define __CVC4__THEORY__BV__BV_TO_BOOL_H
-
-#include <unordered_map>
-
-#include "theory/bv/theory_bv_utils.h"
-#include "util/statistics_registry.h"
-
-namespace CVC4 {
-namespace theory {
-namespace bv {
-
-typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
-
-class BvToBoolPreprocessor {
-
-  struct Statistics {
-    IntStat d_numTermsLifted;
-    IntStat d_numAtomsLifted;
-    IntStat d_numTermsForcedLifted;
-    IntStat d_numTermsLowered;
-    IntStat d_numAtomsLowered;
-    IntStat d_numTermsForcedLowered;
-    Statistics();
-    ~Statistics();
-  };
-  
-  NodeNodeMap d_liftCache;
-  NodeNodeMap d_boolCache;
-  Node d_one;
-  Node d_zero;
-
-  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);
-  Statistics d_statistics;
-
-  NodeNodeMap d_lowerCache;
-  void addToLowerCache(TNode term, Node new_term);
-  Node getLowerCache(TNode term) const;
-  bool hasLowerCache(TNode term) const; 
-  Node lowerNode(TNode current, bool topLevel = false);
-
-public:
-  BvToBoolPreprocessor();
-  void liftBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
-  void lowerBoolToBv(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
-}; 
-
-
-
-}/* CVC4::theory::bv namespace */
-}/* CVC4::theory namespace */
-
-}/* CVC4 namespace */
-
-
-#endif /* __CVC4__THEORY__BV__BV_TO_BOOL_H */