Make ackermannization generally applicable rather than just BV (#3315)

The ackermannization process is currently already support general theories rather than specifically for BV. In this pull request, an option has been added to turn on ackermannization independently.

6 files changed, 84 insertions, 30 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 7289f650b..0a6dec216 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -38,6 +38,8 @@ libcvc4_add_sources(
   lib/strtok_r.h
   preprocessing/assertion_pipeline.cpp
   preprocessing/assertion_pipeline.h
+  preprocessing/passes/ackermann.cpp
+  preprocessing/passes/ackermann.h
   preprocessing/passes/apply_substs.cpp
   preprocessing/passes/apply_substs.h
   preprocessing/passes/apply_to_const.cpp
@@ -46,8 +48,6 @@ libcvc4_add_sources(
   preprocessing/passes/bool_to_bv.h
   preprocessing/passes/bv_abstraction.cpp
   preprocessing/passes/bv_abstraction.h
-  preprocessing/passes/bv_ackermann.cpp
-  preprocessing/passes/bv_ackermann.h
   preprocessing/passes/bv_eager_atoms.cpp
   preprocessing/passes/bv_eager_atoms.h
   preprocessing/passes/bv_gauss.cpp
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 394875fae..571094618 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -23,6 +23,14 @@ header = "options/smt_options.h"
   help       = "all dumping goes to FILE (instead of stdout)"
 
 [[option]]
+  name       = "ackermann"
+  category   = "regular"
+  long       = "ackermann"
+  type       = "bool"
+  default    = "false"
+  help       = "eliminate functions by ackermannization"
+
+[[option]]
   name       = "simplificationMode"
   smt_name   = "simplification-mode"
   category   = "regular"
diff --git a/src/preprocessing/passes/bv_ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index c8cefcb17..7ba689d0a 100644
--- a/src/preprocessing/passes/bv_ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -1,8 +1,8 @@
 /*********************                                                        */
-/*! \file bv_ackermann.cpp
+/*! \file ackermann.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Yoni Zohar, Aina Niemetz, Clark Barrett
+ **   Yoni Zohar, Aina Niemetz, Clark Barrett, Ying Sheng
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -21,10 +21,9 @@
 **   https://cs.nyu.edu/media/publications/hadarean_liana.pdf
  **/
 
-#include "preprocessing/passes/bv_ackermann.h"
+#include "preprocessing/passes/ackermann.h"
 
-#include "options/bv_options.h"
-#include "theory/bv/theory_bv_utils.h"
+#include "options/options.h"
 
 using namespace CVC4;
 using namespace CVC4::theory;
@@ -51,6 +50,7 @@ void addLemmaForPair(TNode args1,
     Assert(args1.getOperator() == func);
     Assert(args2.getKind() == kind::APPLY_UF && args2.getOperator() == func);
     Assert(args1.getNumChildren() == args2.getNumChildren());
+    Assert(args1.getNumChildren() >= 1);
 
     std::vector<Node> eqs(args1.getNumChildren());
 
@@ -58,7 +58,14 @@ void addLemmaForPair(TNode args1,
     {
       eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]);
     }
-    args_eq = bv::utils::mkAnd(eqs);
+    if (eqs.size() >= 2)
+    {
+      args_eq = nm->mkNode(kind::AND, eqs);
+    }
+    else
+    {
+      args_eq = eqs[0];
+    }
   }
   else
   {
@@ -89,10 +96,10 @@ void storeFunctionAndAddLemmas(TNode func,
   if (set.find(term) == set.end())
   {
     TypeNode tn = term.getType();
-    Node skolem = nm->mkSkolem("BVSKOLEM$$",
+    Node skolem = nm->mkSkolem("SKOLEM$$",
                                tn,
                                "is a variable created by the ackermannization "
-                               "preprocessing pass for theory BV");
+                               "preprocessing pass");
     for (const auto& t : set)
     {
       addLemmaForPair(t, term, func, assertions, nm);
@@ -164,7 +171,7 @@ void collectFunctionsAndLemmas(FunctionToArgsMap& fun_to_args,
       {
         AlwaysAssert(
             term.getKind() != kind::STORE,
-            "Cannot use eager bitblasting on QF_ABV formula with stores");
+            "Cannot use Ackermannization on formula with stores to arrays");
         /* add children to the vector, so that they are processed later */
         for (TNode n : term)
         {
@@ -180,16 +187,15 @@ void collectFunctionsAndLemmas(FunctionToArgsMap& fun_to_args,
 
 /* -------------------------------------------------------------------------- */
 
-BVAckermann::BVAckermann(PreprocessingPassContext* preprocContext)
-    : PreprocessingPass(preprocContext, "bv-ackermann"),
+Ackermann::Ackermann(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "ackermann"),
       d_funcToSkolem(preprocContext->getUserContext())
 {
 }
 
-PreprocessingPassResult BVAckermann::applyInternal(
+PreprocessingPassResult Ackermann::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
   AlwaysAssert(!options::incrementalSolving());
 
   /* collect all function applications and generate consistency lemmas
diff --git a/src/preprocessing/passes/bv_ackermann.h b/src/preprocessing/passes/ackermann.h
index 98d1080bd..8f27cab25 100644
--- a/src/preprocessing/passes/bv_ackermann.h
+++ b/src/preprocessing/passes/ackermann.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file bv_ackermann.h
+/*! \file ackermann.h
  ** \verbatim
  ** Top contributors (to current version):
  **   Aina Niemetz, Yoni Zohar
@@ -23,8 +23,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H
-#define CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H
+#ifndef CVC4__PREPROCESSING__PASSES__ACKERMANN_H
+#define CVC4__PREPROCESSING__PASSES__ACKERMANN_H
 
 #include <unordered_map>
 #include "expr/node.h"
@@ -39,10 +39,10 @@ using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>;
 using FunctionToArgsMap =
     std::unordered_map<TNode, TNodeSet, TNodeHashFunction>;
 
-class BVAckermann : public PreprocessingPass
+class Ackermann : public PreprocessingPass
 {
  public:
-   BVAckermann(PreprocessingPassContext* preprocContext);
+  Ackermann(PreprocessingPassContext* preprocContext);
 
  protected:
   /**
@@ -59,7 +59,10 @@ class BVAckermann : public PreprocessingPass
        AssertionPipeline* assertionsToPreprocess) override;
 
  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
+   * ackermannization */
   theory::SubstitutionMap d_funcToSkolem;
 };
 
@@ -67,4 +70,4 @@ class BVAckermann : public PreprocessingPass
 }  // namespace preprocessing
 }  // namespace CVC4
 
-#endif
+#endif /* CVC4__PREPROCESSING__PASSES__ACKERMANN_H */
diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp
index 36b3c6392..82132774b 100644
--- a/src/preprocessing/preprocessing_pass_registry.cpp
+++ b/src/preprocessing/preprocessing_pass_registry.cpp
@@ -23,11 +23,11 @@
 #include "base/cvc4_assert.h"
 #include "base/map_util.h"
 #include "base/output.h"
+#include "preprocessing/passes/ackermann.h"
 #include "preprocessing/passes/apply_substs.h"
 #include "preprocessing/passes/apply_to_const.h"
 #include "preprocessing/passes/bool_to_bv.h"
 #include "preprocessing/passes/bv_abstraction.h"
-#include "preprocessing/passes/bv_ackermann.h"
 #include "preprocessing/passes/bv_eager_atoms.h"
 #include "preprocessing/passes/bv_gauss.h"
 #include "preprocessing/passes/bv_intro_pow2.h"
@@ -142,7 +142,7 @@ PreprocessingPassRegistry::PreprocessingPassRegistry()
   registerPassInfo("ite-removal", callCtor<IteRemoval>);
   registerPassInfo("miplib-trick", callCtor<MipLibTrick>);
   registerPassInfo("non-clausal-simp", callCtor<NonClausalSimp>);
-  registerPassInfo("bv-ackermann", callCtor<BVAckermann>);
+  registerPassInfo("ackermann", callCtor<Ackermann>);
   registerPassInfo("sym-break", callCtor<SymBreakerPass>);
   registerPassInfo("ext-rew-pre", callCtor<ExtRewPre>);
   registerPassInfo("theory-preprocess", callCtor<TheoryPreprocess>);
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 918539f4f..8705bfb9b 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1185,6 +1185,10 @@ void SmtEngine::setDefaults() {
                << "generation" << endl;
       setOption("bitblastMode", SExpr("lazy"));
     }
+    else if (!options::incrementalSolving())
+    {
+      options::ackermann.set(true);
+    }
 
     if (options::incrementalSolving() && !d_logic.isPure(THEORY_BV))
     {
@@ -1208,11 +1212,45 @@ void SmtEngine::setDefaults() {
   {
     d_logic = LogicInfo("QF_NIA");
   }
-  else if ((d_logic.getLogicString() == "QF_UFBV"
-            || d_logic.getLogicString() == "QF_ABV")
-           && options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
+
+  // set options about ackermannization
+  if (options::produceModels())
   {
-    d_logic = LogicInfo("QF_BV");
+    if (options::ackermann()
+        && (d_logic.isTheoryEnabled(THEORY_ARRAYS)
+            || d_logic.isTheoryEnabled(THEORY_UF)))
+    {
+      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);
+    }
+  }
+
+  if (options::ackermann())
+  {
+    if (options::incrementalSolving())
+    {
+      throw OptionException(
+          "Incremental Ackermannization is currently not supported.");
+    }
+
+    if (d_logic.isTheoryEnabled(THEORY_UF))
+    {
+      d_logic = d_logic.getUnlockedCopy();
+      d_logic.disableTheory(THEORY_UF);
+      d_logic.lock();
+    }
+    if (d_logic.isTheoryEnabled(THEORY_ARRAYS))
+    {
+      d_logic = d_logic.getUnlockedCopy();
+      d_logic.disableTheory(THEORY_ARRAYS);
+      d_logic.lock();
+    }
   }
 
   // set default options associated with strings-exp
@@ -3241,10 +3279,9 @@ void SmtEnginePrivate::processAssertions() {
                          "Try --bv-div-zero-const to interpret division by zero as a constant.");
   }
 
-  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
-      && !options::incrementalSolving())
+  if (options::ackermann())
   {
-    d_passes["bv-ackermann"]->apply(&d_assertions);
+    d_passes["ackermann"]->apply(&d_assertions);
   }
 
   if (options::bvAbstraction() && !options::incrementalSolving())