Refactor real2int (#1813)

This commit refactors the real2int preprocessing pass into the new style. This commit is essentially just a code move and adds a regression test for the preprocessing pass.

2 files changed, 254 insertions, 0 deletions

diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp
new file mode 100644
index 000000000..c92f4b962
--- /dev/null
+++ b/src/preprocessing/passes/real_to_int.cpp
@@ -0,0 +1,202 @@
+/*********************                                                        */
+/*! \file real_to_int.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** 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 The RealToInt preprocessing pass
+ **
+ ** Converts real operations into integer operations
+ **/
+
+#include "preprocessing/passes/real_to_int.h"
+
+#include <string>
+
+#include "theory/arith/arith_msum.h"
+#include "theory/rewriter.h"
+#include "theory/theory_model.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using namespace CVC4::theory;
+
+Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& var_eq)
+{
+  Trace("real-as-int-debug") << "Convert : " << n << std::endl;
+  NodeMap::iterator find = cache.find(n);
+  if (find != cache.end())
+  {
+    return (*find).second;
+  }
+  else
+  {
+    Node ret = n;
+    if (n.getNumChildren() > 0)
+    {
+      if (n.getKind() == kind::EQUAL || n.getKind() == kind::GEQ
+          || n.getKind() == kind::LT
+          || n.getKind() == kind::GT
+          || n.getKind() == kind::LEQ)
+      {
+        ret = Rewriter::rewrite(n);
+        Trace("real-as-int-debug") << "Now looking at : " << ret << std::endl;
+        if (!ret.isConst())
+        {
+          Node ret_lit = ret.getKind() == kind::NOT ? ret[0] : ret;
+          bool ret_pol = ret.getKind() != kind::NOT;
+          std::map<Node, Node> msum;
+          if (ArithMSum::getMonomialSumLit(ret_lit, msum))
+          {
+            // get common coefficient
+            std::vector<Node> coeffs;
+            for (std::map<Node, Node>::iterator itm = msum.begin();
+                 itm != msum.end();
+                 ++itm)
+            {
+              Node v = itm->first;
+              Node c = itm->second;
+              if (!c.isNull())
+              {
+                Assert(c.isConst());
+                coeffs.push_back(NodeManager::currentNM()->mkConst(
+                    Rational(c.getConst<Rational>().getDenominator())));
+              }
+            }
+            Node cc =
+                coeffs.empty()
+                    ? Node::null()
+                    : (coeffs.size() == 1
+                           ? coeffs[0]
+                           : Rewriter::rewrite(NodeManager::currentNM()->mkNode(
+                                 kind::MULT, coeffs)));
+            std::vector<Node> sum;
+            for (std::map<Node, Node>::iterator itm = msum.begin();
+                 itm != msum.end();
+                 ++itm)
+            {
+              Node v = itm->first;
+              Node c = itm->second;
+              Node s;
+              if (c.isNull())
+              {
+                c = cc.isNull() ? NodeManager::currentNM()->mkConst(Rational(1))
+                                : cc;
+              }
+              else
+              {
+                if (!cc.isNull())
+                {
+                  c = Rewriter::rewrite(
+                      NodeManager::currentNM()->mkNode(kind::MULT, c, cc));
+                }
+              }
+              Assert(c.getType().isInteger());
+              if (v.isNull())
+              {
+                sum.push_back(c);
+              }
+              else
+              {
+                Node vv = realToIntInternal(v, cache, var_eq);
+                if (vv.getType().isInteger())
+                {
+                  sum.push_back(
+                      NodeManager::currentNM()->mkNode(kind::MULT, c, vv));
+                }
+                else
+                {
+                  throw TypeCheckingException(
+                      v.toExpr(),
+                      string("Cannot translate to Int: ") + v.toString());
+                }
+              }
+            }
+            Node sumt =
+                sum.empty()
+                    ? NodeManager::currentNM()->mkConst(Rational(0))
+                    : (sum.size() == 1
+                           ? sum[0]
+                           : NodeManager::currentNM()->mkNode(kind::PLUS, sum));
+            ret = NodeManager::currentNM()->mkNode(
+                ret_lit.getKind(),
+                sumt,
+                NodeManager::currentNM()->mkConst(Rational(0)));
+            if (!ret_pol)
+            {
+              ret = ret.negate();
+            }
+            Trace("real-as-int") << "Convert : " << std::endl;
+            Trace("real-as-int") << "   " << n << std::endl;
+            Trace("real-as-int") << "   " << ret << std::endl;
+          }
+          else
+          {
+            throw TypeCheckingException(
+                n.toExpr(), string("Cannot translate to Int: ") + n.toString());
+          }
+        }
+      }
+      else
+      {
+        bool childChanged = false;
+        std::vector<Node> children;
+        for (unsigned i = 0; i < n.getNumChildren(); i++)
+        {
+          Node nc = realToIntInternal(n[i], cache, var_eq);
+          childChanged = childChanged || nc != n[i];
+          children.push_back(nc);
+        }
+        if (childChanged)
+        {
+          ret = NodeManager::currentNM()->mkNode(n.getKind(), children);
+        }
+      }
+    }
+    else
+    {
+      if (n.isVar())
+      {
+        if (!n.getType().isInteger())
+        {
+          ret = NodeManager::currentNM()->mkSkolem(
+              "__realToIntInternal_var",
+              NodeManager::currentNM()->integerType(),
+              "Variable introduced in realToIntInternal pass");
+          var_eq.push_back(n.eqNode(ret));
+          TheoryModel* m = d_preprocContext->getTheoryEngine()->getModel();
+          m->addSubstitution(n, ret);
+        }
+      }
+    }
+    cache[n] = ret;
+    return ret;
+  }
+}
+
+RealToInt::RealToInt(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "real-to-int"){};
+
+PreprocessingPassResult RealToInt::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  unordered_map<Node, Node, NodeHashFunction> cache;
+  std::vector<Node> var_eq;
+  for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
+  {
+    assertionsToPreprocess->replace(
+        i, realToIntInternal((*assertionsToPreprocess)[i], cache, var_eq));
+  }
+  return PreprocessingPassResult::NO_CONFLICT;
+}
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/passes/real_to_int.h b/src/preprocessing/passes/real_to_int.h
new file mode 100644
index 000000000..eb4ac6593
--- /dev/null
+++ b/src/preprocessing/passes/real_to_int.h
@@ -0,0 +1,52 @@
+/*********************                                                        */
+/*! \file real_to_int.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** 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 The RealToInt preprocessing pass
+ **
+ ** Converts real operations into integer operations
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H
+#define __CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H
+
+#include <unordered_map>
+#include <vector>
+
+#include "expr/node.h"
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
+
+class RealToInt : public PreprocessingPass
+{
+ public:
+  RealToInt(PreprocessingPassContext* preprocContext);
+
+ protected:
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+  Node realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& var_eq);
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H */