GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/real_to_int.cpp Lines: 93 96 96.9 %
Date: 2021-03-23 Branches: 225 456 49.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file real_to_int.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Haniel Barbosa, Andrew Reynolds, Tim King
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief The RealToInt preprocessing pass
13
 **
14
 ** Converts real operations into integer operations
15
 **/
16
17
#include "preprocessing/passes/real_to_int.h"
18
19
#include <string>
20
21
#include "preprocessing/assertion_pipeline.h"
22
#include "preprocessing/preprocessing_pass_context.h"
23
#include "theory/arith/arith_msum.h"
24
#include "theory/rewriter.h"
25
#include "theory/theory_model.h"
26
27
namespace CVC4 {
28
namespace preprocessing {
29
namespace passes {
30
31
using namespace std;
32
using namespace CVC4::theory;
33
34
130
Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& var_eq)
35
{
36
130
  Trace("real-as-int-debug") << "Convert : " << n << std::endl;
37
130
  NodeMap::iterator find = cache.find(n);
38
130
  if (find != cache.end())
39
  {
40
36
    return (*find).second;
41
  }
42
  else
43
  {
44
94
    NodeManager* nm = NodeManager::currentNM();
45
188
    Node ret = n;
46
94
    if (n.getNumChildren() > 0)
47
    {
48
121
      if ((n.getKind() == kind::EQUAL && n[0].getType().isReal())
49
44
          || n.getKind() == kind::GEQ || n.getKind() == kind::LT
50
154
          || n.getKind() == kind::GT || n.getKind() == kind::LEQ)
51
      {
52
27
        ret = Rewriter::rewrite(n);
53
27
        Trace("real-as-int-debug") << "Now looking at : " << ret << std::endl;
54
27
        if (!ret.isConst())
55
        {
56
54
          Node ret_lit = ret.getKind() == kind::NOT ? ret[0] : ret;
57
27
          bool ret_pol = ret.getKind() != kind::NOT;
58
54
          std::map<Node, Node> msum;
59
27
          if (ArithMSum::getMonomialSumLit(ret_lit, msum))
60
          {
61
            // get common coefficient
62
54
            std::vector<Node> coeffs;
63
79
            for (std::map<Node, Node>::iterator itm = msum.begin();
64
79
                 itm != msum.end();
65
                 ++itm)
66
            {
67
104
              Node v = itm->first;
68
104
              Node c = itm->second;
69
52
              if (!c.isNull())
70
              {
71
33
                Assert(c.isConst());
72
66
                coeffs.push_back(NodeManager::currentNM()->mkConst(
73
66
                    Rational(c.getConst<Rational>().getDenominator())));
74
              }
75
            }
76
            Node cc =
77
27
                coeffs.empty()
78
                    ? Node::null()
79
22
                    : (coeffs.size() == 1
80
15
                           ? coeffs[0]
81
34
                           : Rewriter::rewrite(NodeManager::currentNM()->mkNode(
82
98
                                 kind::MULT, coeffs)));
83
54
            std::vector<Node> sum;
84
79
            for (std::map<Node, Node>::iterator itm = msum.begin();
85
79
                 itm != msum.end();
86
                 ++itm)
87
            {
88
104
              Node v = itm->first;
89
104
              Node c = itm->second;
90
104
              Node s;
91
52
              if (c.isNull())
92
              {
93
19
                c = cc.isNull() ? NodeManager::currentNM()->mkConst(Rational(1))
94
                                : cc;
95
              }
96
              else
97
              {
98
33
                if (!cc.isNull())
99
                {
100
33
                  c = Rewriter::rewrite(
101
66
                      NodeManager::currentNM()->mkNode(kind::MULT, c, cc));
102
                }
103
              }
104
52
              Assert(c.getType().isInteger());
105
52
              if (v.isNull())
106
              {
107
8
                sum.push_back(c);
108
              }
109
              else
110
              {
111
88
                Node vv = realToIntInternal(v, cache, var_eq);
112
44
                if (vv.getType().isInteger())
113
                {
114
44
                  sum.push_back(
115
88
                      NodeManager::currentNM()->mkNode(kind::MULT, c, vv));
116
                }
117
                else
118
                {
119
                  throw TypeCheckingExceptionPrivate(
120
                      v,
121
                      std::string("Cannot translate to Int: ") + v.toString());
122
                }
123
              }
124
            }
125
            Node sumt =
126
27
                sum.empty()
127
27
                    ? NodeManager::currentNM()->mkConst(Rational(0))
128
27
                    : (sum.size() == 1
129
11
                           ? sum[0]
130
92
                           : NodeManager::currentNM()->mkNode(kind::PLUS, sum));
131
54
            ret = NodeManager::currentNM()->mkNode(
132
                ret_lit.getKind(),
133
                sumt,
134
54
                NodeManager::currentNM()->mkConst(Rational(0)));
135
27
            if (!ret_pol)
136
            {
137
8
              ret = ret.negate();
138
            }
139
27
            Trace("real-as-int") << "Convert : " << std::endl;
140
27
            Trace("real-as-int") << "   " << n << std::endl;
141
27
            Trace("real-as-int") << "   " << ret << std::endl;
142
          }
143
        }
144
      }
145
      else
146
      {
147
28
        bool childChanged = false;
148
56
        std::vector<Node> children;
149
76
        for (unsigned i = 0; i < n.getNumChildren(); i++)
150
        {
151
96
          Node nc = realToIntInternal(n[i], cache, var_eq);
152
48
          childChanged = childChanged || nc != n[i];
153
48
          children.push_back(nc);
154
        }
155
28
        if (childChanged)
156
        {
157
28
          if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
158
          {
159
2
            children.insert(children.begin(), n.getOperator());
160
          }
161
28
          ret = NodeManager::currentNM()->mkNode(n.getKind(), children);
162
        }
163
      }
164
    }
165
    else
166
    {
167
78
      TypeNode tn = n.getType();
168
39
      if (tn.isReal() && !tn.isInteger())
169
      {
170
22
        if (n.getKind() == kind::BOUND_VARIABLE)
171
        {
172
          // cannot change the type of quantified variables, since this leads
173
          // to incompleteness.
174
          throw TypeCheckingExceptionPrivate(
175
              n,
176
              std::string("Cannot translate bound variable to Int: ")
177
                  + n.toString());
178
        }
179
22
        else if (n.isVar())
180
        {
181
66
          ret = nm->mkSkolem("__realToIntInternal_var",
182
44
                             nm->integerType(),
183
                             "Variable introduced in realToIntInternal pass");
184
22
          var_eq.push_back(n.eqNode(ret));
185
          // ensure that the original variable is defined to be the returned
186
          // one, which is important for models and for incremental solving.
187
44
          std::vector<Node> args;
188
22
          d_preprocContext->getSmt()->defineFunction(n, args, ret);
189
        }
190
      }
191
    }
192
94
    cache[n] = ret;
193
94
    return ret;
194
  }
195
}
196
197
8997
RealToInt::RealToInt(PreprocessingPassContext* preprocContext)
198
8997
    : PreprocessingPass(preprocContext, "real-to-int"){};
199
200
13
PreprocessingPassResult RealToInt::applyInternal(
201
    AssertionPipeline* assertionsToPreprocess)
202
{
203
26
  unordered_map<Node, Node, NodeHashFunction> cache;
204
26
  std::vector<Node> var_eq;
205
51
  for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
206
  {
207
38
    assertionsToPreprocess->replace(
208
76
        i, realToIntInternal((*assertionsToPreprocess)[i], cache, var_eq));
209
  }
210
26
  return PreprocessingPassResult::NO_CONFLICT;
211
}
212
213
214
}  // namespace passes
215
}  // namespace preprocessing
216
26685
}  // namespace CVC4