Support ackermannization on uninterpreted sorts in BV (#3372)

Support ackermannization on uninterpreted sorts in BV. For uninterpreted sorts, we create a bit-vector sort to replace it. For an uninterpreted sort `S`, if the number of variables within sort `S` is `n`, the replacing bit-vector will have size (log n)+1.

3 files changed, 136 insertions, 15 deletions

diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index 87c7fa2ce..888456174 100644
--- a/src/preprocessing/passes/ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -22,8 +22,9 @@
  **/
 
 #include "preprocessing/passes/ackermann.h"
-
+#include <cmath>
 #include "base/check.h"
+#include "expr/node_algorithm.h"
 #include "options/options.h"
 
 using namespace CVC4;
@@ -186,9 +187,111 @@ void collectFunctionsAndLemmas(FunctionToArgsMap& fun_to_args,
 
 /* -------------------------------------------------------------------------- */
 
+/* Given a minimum capacity for an uninterpreted sort, return the size of the
+ * new BV type */
+size_t getBVSkolemSize(size_t capacity)
+{
+  return static_cast<size_t>(log2(capacity)) + 1;
+}
+
+/* Given the lowest capacity requirements for each uninterpreted sort, assign
+ * a sufficient bit-vector size.
+ * Populate usVarsToBVVars so that it maps variables with uninterpreted sort to
+ * the fresh skolem BV variables. variables */
+void collectUSortsToBV(const unordered_set<TNode, TNodeHashFunction>& vars,
+                       const USortToBVSizeMap& usortCardinality,
+                       SubstitutionMap& usVarsToBVVars)
+{
+  NodeManager* nm = NodeManager::currentNM();
+
+  for (TNode var : vars)
+  {
+    TypeNode type = var.getType();
+    size_t size = getBVSkolemSize(usortCardinality.at(type));
+    Node skolem = nm->mkSkolem(
+        "BVSKOLEM$$",
+        nm->mkBitVectorType(size),
+        "a variable created by the ackermannization "
+        "preprocessing pass, representing a variable with uninterpreted sort "
+            + type.toString() + ".");
+    usVarsToBVVars.addSubstitution(var, skolem);
+  }
+}
+
+/* This function returns the list of terms with uninterpreted sort in the
+ * formula represented by assertions. */
+std::unordered_set<TNode, TNodeHashFunction> getVarsWithUSorts(
+    AssertionPipeline* assertions)
+{
+  std::unordered_set<TNode, TNodeHashFunction> res;
+
+  for (const Node& assertion : assertions->ref())
+  {
+    std::unordered_set<TNode, TNodeHashFunction> vars;
+    expr::getVariables(assertion, vars);
+
+    for (const TNode& var : vars)
+    {
+      if (var.getType().isSort())
+      {
+        res.insert(var);
+      }
+    }
+  }
+
+  return res;
+}
+
+/* This is the top level of converting uninterpreted sorts to bit-vectors.
+ * We count the number of different variables for each uninterpreted sort.
+ * Then for each sort, we will assign a new bit-vector type with a sufficient
+ * size. The size is calculated to have enough capacity, that can accommodate
+ * the variables occured in the original formula. At the end, all variables of
+ * uninterpreted sorts will be converted into Skolem variables of BV */
+void usortsToBitVectors(const LogicInfo& d_logic,
+                        AssertionPipeline* assertions,
+                        USortToBVSizeMap& usortCardinality,
+                        SubstitutionMap& usVarsToBVVars)
+{
+  std::unordered_set<TNode, TNodeHashFunction> toProcess =
+      getVarsWithUSorts(assertions);
+
+  if (toProcess.size() > 0)
+  {
+    /* the current version only supports BV for removing uninterpreted sorts */
+    if (not d_logic.isTheoryEnabled(theory::THEORY_BV))
+    {
+      return;
+    }
+
+    for (TNode term : toProcess)
+    {
+      TypeNode type = term.getType();
+      /* Update the counts for each uninterpreted sort.
+       * For non-existing keys, C++ will create a new element for it, which has
+       * a default 0 value, before incrementing by 1. */
+      usortCardinality[type] = usortCardinality[type] + 1;
+    }
+
+    collectUSortsToBV(toProcess, usortCardinality, usVarsToBVVars);
+
+    for (size_t i = 0, size = assertions->size(); i < size; ++i)
+    {
+      Node old = (*assertions)[i];
+      assertions->replace(i, usVarsToBVVars.apply((*assertions)[i]));
+      Trace("uninterpretedSorts-to-bv")
+          << "  " << old << " => " << (*assertions)[i] << "\n";
+    }
+  }
+}
+
+/* -------------------------------------------------------------------------- */
+
 Ackermann::Ackermann(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "ackermann"),
-      d_funcToSkolem(preprocContext->getUserContext())
+      d_funcToSkolem(preprocContext->getUserContext()),
+      d_usVarsToBVVars(preprocContext->getUserContext()),
+      d_logic(preprocContext->getLogicInfo())
 {
 }
 
@@ -215,6 +318,10 @@ PreprocessingPassResult Ackermann::applyInternal(
         i, d_funcToSkolem.apply((*assertionsToPreprocess)[i]));
   }
 
+  /* replace uninterpreted sorts with bit-vectors */
+  usortsToBitVectors(
+      d_logic, assertionsToPreprocess, d_usortCardinality, d_usVarsToBVVars);
+
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
diff --git a/src/preprocessing/passes/ackermann.h b/src/preprocessing/passes/ackermann.h
index 410dde8b9..4aa26da85 100644
--- a/src/preprocessing/passes/ackermann.h
+++ b/src/preprocessing/passes/ackermann.h
@@ -38,6 +38,8 @@ namespace passes {
 using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>;
 using FunctionToArgsMap =
     std::unordered_map<TNode, TNodeSet, TNodeHashFunction>;
+using USortToBVSizeMap =
+    std::unordered_map<TypeNode, size_t, TypeNode::HashFunction>;
 
 class Ackermann : public PreprocessingPass
 {
@@ -54,6 +56,10 @@ class Ackermann : public PreprocessingPass
    * - 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
+   *
+   * - For each uninterpreted sort S, suppose k is the number of variables with
+   *   sort S, then for each such variable X, introduce a fresh variable BV_X
+   *   with BV with size log_2(k)+1 and use it to replace all occurrences of X.
    */
   PreprocessingPassResult applyInternal(
       AssertionPipeline* assertionsToPreprocess) override;
@@ -61,9 +67,15 @@ class Ackermann : public PreprocessingPass
  private:
   /* Map each function to a set of terms associated with it */
   FunctionToArgsMap d_funcToArgs;
-  /* Map each function term to the new Skolem variable created by
+  /* Map each function-application term to the new Skolem variable created by
    * ackermannization */
   theory::SubstitutionMap d_funcToSkolem;
+  /* Map each variable with uninterpreted sort to the new Skolem BV variable
+   * created by ackermannization */
+  theory::SubstitutionMap d_usVarsToBVVars;
+  /* Map each uninterpreted sort to the number of variables in this sort. */
+  USortToBVSizeMap d_usortCardinality;
+  LogicInfo d_logic;
 };
 
 }  // namespace passes
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0276684d6..cb1445b93 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1212,21 +1212,18 @@ void SmtEngine::setDefaults() {
   }
 
   // set options about ackermannization
-  if (options::produceModels())
+  if (options::ackermann() && options::produceModels()
+      && (d_logic.isTheoryEnabled(THEORY_ARRAYS)
+          || d_logic.isTheoryEnabled(THEORY_UF)))
   {
-    if (options::ackermann()
-        && (d_logic.isTheoryEnabled(THEORY_ARRAYS)
-            || d_logic.isTheoryEnabled(THEORY_UF)))
+    if (options::produceModels.wasSetByUser())
     {
-      if (options::produceModels.wasSetByUser())
-      {
-        throw OptionException(std::string(
-            "Ackermannization currently does not support model generation."));
-      }
-      Notice() << "SmtEngine: turn off ackermannization to support model"
-               << "generation" << endl;
-      options::ackermann.set(false);
+      throw OptionException(std::string(
+          "Ackermannization currently does not support model generation."));
     }
+    Notice() << "SmtEngine: turn off ackermannization to support model"
+             << "generation" << endl;
+    options::ackermann.set(false);
   }
 
   if (options::ackermann())
@@ -1237,6 +1234,11 @@ void SmtEngine::setDefaults() {
           "Incremental Ackermannization is currently not supported.");
     }
 
+    if (d_logic.isQuantified())
+    {
+      throw LogicException("Cannot use Ackermannization on quantified formula");
+    }
+
     if (d_logic.isTheoryEnabled(THEORY_UF))
     {
       d_logic = d_logic.getUnlockedCopy();