Make sort inference a preprocessing pass (#2309)

2 files changed, 143 insertions, 0 deletions

diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp
new file mode 100644
index 000000000..e2b0bfb59
--- /dev/null
+++ b/src/preprocessing/passes/sort_infer.cpp
@@ -0,0 +1,85 @@
+/*********************                                                        */
+/*! \file sort_infer.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** 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 Sort inference preprocessing pass
+ **/
+
+#include "preprocessing/passes/sort_infer.h"
+
+#include "options/smt_options.h"
+#include "options/uf_options.h"
+#include "theory/rewriter.h"
+
+using namespace std;
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+SortInferencePass::SortInferencePass(PreprocessingPassContext* preprocContext,
+                                     SortInference* si)
+    : PreprocessingPass(preprocContext, "sort-inference"), d_si(si)
+{
+}
+
+PreprocessingPassResult SortInferencePass::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  if (options::sortInference())
+  {
+    d_si->initialize(assertionsToPreprocess->ref());
+    std::map<Node, Node> model_replace_f;
+    std::map<Node, std::map<TypeNode, Node> > visited;
+    for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; i++)
+    {
+      Node prev = (*assertionsToPreprocess)[i];
+      Node next = d_si->simplify(prev, model_replace_f, visited);
+      if (next != prev)
+      {
+        next = theory::Rewriter::rewrite(next);
+        assertionsToPreprocess->replace(i, next);
+        Trace("sort-infer-preprocess")
+            << "*** Preprocess SortInferencePass " << prev << endl;
+        Trace("sort-infer-preprocess")
+            << "   ...got " << (*assertionsToPreprocess)[i] << endl;
+      }
+    }
+    std::vector<Node> newAsserts;
+    d_si->getNewAssertions(newAsserts);
+    for (const Node& na : newAsserts)
+    {
+      Node nar = theory::Rewriter::rewrite(na);
+      Trace("sort-infer-preprocess")
+          << "*** Preprocess SortInferencePass : new constraint " << nar
+          << endl;
+      assertionsToPreprocess->push_back(nar);
+    }
+    // indicate correspondence between the functions
+    // TODO (#2308): move this to a better place
+    SmtEngine* smt = smt::currentSmtEngine();
+    for (const std::pair<const Node, Node>& mrf : model_replace_f)
+    {
+      smt->setPrintFuncInModel(mrf.first.toExpr(), false);
+      smt->setPrintFuncInModel(mrf.second.toExpr(), true);
+    }
+  }
+  // only need to compute monotonicity on the resulting formula if we are
+  // using this option
+  if (options::ufssFairnessMonotone())
+  {
+    d_si->computeMonotonicity(assertionsToPreprocess->ref());
+  }
+  return PreprocessingPassResult::NO_CONFLICT;
+}
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/passes/sort_infer.h b/src/preprocessing/passes/sort_infer.h
new file mode 100644
index 000000000..e56d7ab60
--- /dev/null
+++ b/src/preprocessing/passes/sort_infer.h
@@ -0,0 +1,58 @@
+/*********************                                                        */
+/*! \file sort_infer.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** 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 Sort inference preprocessing pass
+ **/
+
+#ifndef __CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_
+#define __CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_
+
+#include <map>
+#include <string>
+#include <vector>
+#include "expr/node.h"
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "theory/sort_inference.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+/** SortInferencePass
+ *
+ * This preprocessing pass runs sort inference techniques on the input formula.
+ * For details on these techniques, see theory/sort_inference.h.
+ */
+class SortInferencePass : public PreprocessingPass
+{
+ public:
+  SortInferencePass(PreprocessingPassContext* preprocContext,
+                    SortInference* si);
+
+ protected:
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+  /**
+   * Pointer to the sort inference module. This should be the sort inference
+   * belonging to the theory engine of the current SMT engine.
+   */
+  SortInference* d_si;
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ */