Refactored BVAckermann preprocessing pass. (#1889)

2 files changed, 241 insertions, 0 deletions

diff --git a/src/preprocessing/passes/bv_ackermann.cpp b/src/preprocessing/passes/bv_ackermann.cpp
new file mode 100644
index 000000000..850136f9d
--- /dev/null
+++ b/src/preprocessing/passes/bv_ackermann.cpp
@@ -0,0 +1,173 @@
+/*********************                                                        */
+/*! \file bv_ackermann.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz
+ ** 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 Ackermannization preprocessing pass.
+ **
+ ** This implements the Ackermannization preprocessing pass, which enables
+ ** very limited theory combination support for eager bit-blasting via
+ ** Ackermannization. It reduces constraints over the combination of the
+ ** theories of fixed-size bit-vectors and uninterpreted functions as
+ ** described in
+ **   Liana Hadarean, An Efficient and Trustworthy Theory Solver for
+ **   Bit-vectors in Satisfiability Modulo Theories.
+**   https://cs.nyu.edu/media/publications/hadarean_liana.pdf
+ **/
+
+#include "preprocessing/passes/bv_ackermann.h"
+
+#include "expr/node.h"
+#include "options/bv_options.h"
+#include "theory/bv/theory_bv_utils.h"
+
+#include <unordered_set>
+
+using namespace CVC4;
+using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+/* -------------------------------------------------------------------------- */
+
+namespace
+{
+
+void storeFunction(
+    TNode func,
+    TNode term,
+    FunctionToArgsMap& fun_to_args,
+    SubstitutionMap& fun_to_skolem)
+{
+  if (fun_to_args.find(func) == fun_to_args.end())
+  {
+    fun_to_args.insert(make_pair(func, NodeSet()));
+  }
+  NodeSet& set = fun_to_args[func];
+  if (set.find(term) == set.end())
+  {
+    set.insert(term);
+    Node skolem = bv::utils::mkVar(bv::utils::getSize(term));
+    fun_to_skolem.addSubstitution(term, skolem);
+  }
+}
+
+void collectFunctionSymbols(
+    TNode term,
+    FunctionToArgsMap& fun_to_args,
+    SubstitutionMap& fun_to_skolem,
+    std::unordered_set<TNode, TNodeHashFunction>& seen)
+{
+  if (seen.find(term) != seen.end()) return;
+  if (term.getKind() == kind::APPLY_UF)
+  {
+    storeFunction(term.getOperator(), term, fun_to_args, fun_to_skolem);
+  }
+  else if (term.getKind() == kind::SELECT)
+  {
+    storeFunction(term[0], term, fun_to_args, fun_to_skolem);
+  }
+  else
+  {
+    AlwaysAssert(term.getKind() != kind::STORE,
+                 "Cannot use eager bitblasting on QF_ABV formula with stores");
+  }
+  for (const TNode& n : term)
+  {
+    collectFunctionSymbols(n, fun_to_args, fun_to_skolem, seen);
+  }
+  seen.insert(term);
+}
+
+}  // namespace
+
+/* -------------------------------------------------------------------------- */
+
+BVAckermann::BVAckermann(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "bv-ackermann"),
+      d_funcToSkolem(preprocContext->getUserContext())
+{
+}
+
+PreprocessingPassResult BVAckermann::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
+  AlwaysAssert(!options::incrementalSolving());
+
+  std::unordered_set<TNode, TNodeHashFunction> seen;
+
+  for (const Node& a : assertionsToPreprocess->ref())
+  {
+    collectFunctionSymbols(a, d_funcToArgs, d_funcToSkolem, seen);
+  }
+
+  NodeManager* nm = NodeManager::currentNM();
+  for (const auto& p : d_funcToArgs)
+  {
+    TNode func = p.first;
+    const NodeSet& args = p.second;
+    NodeSet::const_iterator it1 = args.begin();
+    for (; it1 != args.end(); ++it1)
+    {
+      for (NodeSet::const_iterator it2 = it1; it2 != args.end(); ++it2)
+      {
+        TNode args1 = *it1;
+        TNode args2 = *it2;
+        Node args_eq;
+
+        if (args1.getKind() == kind::APPLY_UF)
+        {
+          AlwaysAssert(args1.getKind() == kind::APPLY_UF
+                       && args1.getOperator() == func);
+          AlwaysAssert(args2.getKind() == kind::APPLY_UF
+                       && args2.getOperator() == func);
+          AlwaysAssert(args1.getNumChildren() == args2.getNumChildren());
+
+          std::vector<Node> eqs(args1.getNumChildren());
+
+          for (unsigned i = 0, n = args1.getNumChildren(); i < n; ++i)
+          {
+            eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]);
+          }
+          args_eq = bv::utils::mkAnd(eqs);
+        }
+        else
+        {
+          AlwaysAssert(args1.getKind() == kind::SELECT && args1[0] == func);
+          AlwaysAssert(args2.getKind() == kind::SELECT && args2[0] == func);
+          AlwaysAssert(args1.getNumChildren() == 2);
+          AlwaysAssert(args2.getNumChildren() == 2);
+          args_eq = nm->mkNode(kind::EQUAL, args1[1], args2[1]);
+        }
+        Node func_eq = nm->mkNode(kind::EQUAL, args1, args2);
+        Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq);
+        assertionsToPreprocess->push_back(lemma);
+      }
+    }
+  }
+
+  /* replace applications of UF by skolems */
+  // FIXME for model building, github issue #1118)
+  for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
+  {
+    assertionsToPreprocess->replace(
+        i, d_funcToSkolem.apply((*assertionsToPreprocess)[i]));
+  }
+
+  return PreprocessingPassResult::NO_CONFLICT;
+}
+
+/* -------------------------------------------------------------------------- */
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/passes/bv_ackermann.h b/src/preprocessing/passes/bv_ackermann.h
new file mode 100644
index 000000000..dbac79d21
--- /dev/null
+++ b/src/preprocessing/passes/bv_ackermann.h
@@ -0,0 +1,68 @@
+/*********************                                                        */
+/*! \file bv_ackermann.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz
+ ** 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 Ackermannization preprocessing pass.
+ **
+ ** This implements the Ackermannization preprocessing pass, which enables
+ ** very limited theory combination support for eager bit-blasting via
+ ** Ackermannization. It reduces constraints over the combination of the
+ ** theories of fixed-size bit-vectors and uninterpreted functions as
+ ** described in
+ **   Liana Hadarean, An Efficient and Trustworthy Theory Solver for
+ **   Bit-vectors in Satisfiability Modulo Theories.
+**   https://cs.nyu.edu/media/publications/hadarean_liana.pdf
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H
+#define __CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+#include <unordered_map>
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+typedef std::unordered_map<Node, NodeSet, NodeHashFunction> FunctionToArgsMap;
+
+class BVAckermann : public PreprocessingPass
+{
+ public:
+   BVAckermann(PreprocessingPassContext* preprocContext);
+
+ protected:
+  /**
+   * Apply Ackermannization as follows:
+   *
+   * - For each application f(X) where X = (x1, . . . , xn), introduce a fresh
+   *   variable f_X and use it to replace all occurrences of f(X).
+   *
+   * - For each f(X) and f(Y) with X = (x1, . . . , xn) and Y = (y1, . . . , yn)
+   *   occurring in the input formula, add the following lemma:
+   *     (x_1 = y_1 /\ ... /\ x_n = y_n) => f_X = f_Y
+   */
+   PreprocessingPassResult applyInternal(
+       AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+  FunctionToArgsMap d_funcToArgs;
+  theory::SubstitutionMap d_funcToSkolem;
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif