Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/preprocessing/passes/real_to_int.cpp	Lines:	92	96	95.8 %
Date:	2021-05-24	Branches:	224	466	48.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Haniel Barbosa, Andrew Reynolds, Aina Niemetz
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 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.
 * ****************************************************************************
 *
 * The RealToInt preprocessing pass.
 *
 * Converts real operations into integer operations.
 */

#include "preprocessing/passes/real_to_int.h"

#include <string>

#include "expr/skolem_manager.h"
#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "theory/arith/arith_msum.h"
#include "theory/rewriter.h"
#include "theory/theory_model.h"

using namespace cvc5::theory;

namespace cvc5 {
namespace preprocessing {
namespace passes {

RealToInt::RealToInt(PreprocessingPassContext* preprocContext)
    : PreprocessingPass(preprocContext, "real-to-int"),
      d_cache(preprocContext->getUserContext())
{
}

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
  {
    NodeManager* nm = NodeManager::currentNM();
    SkolemManager* sm = nm->getSkolemManager();
    Node ret = n;
    if (n.getNumChildren() > 0)
    {
      if ((n.getKind() == kind::EQUAL && n[0].getType().isReal())
          || 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 TypeCheckingExceptionPrivate(
                      v,
                      std::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
      {
        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)
        {
          if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
          {
            children.insert(children.begin(), n.getOperator());
          }
          ret = NodeManager::currentNM()->mkNode(n.getKind(), children);
        }
      }
    }
    else
    {
      TypeNode tn = n.getType();
      if (tn.isReal() && !tn.isInteger())
      {
        if (n.getKind() == kind::BOUND_VARIABLE)
        {
          // cannot change the type of quantified variables, since this leads
          // to incompleteness.
          throw TypeCheckingExceptionPrivate(
              n,
              std::string("Cannot translate bound variable to Int: ")
                  + n.toString());
        }
        else if (n.isVar())
        {
          Node toIntN = nm->mkNode(kind::TO_INTEGER, n);
          ret = sm->mkPurifySkolem(toIntN, "__realToIntInternal_var");
          var_eq.push_back(n.eqNode(ret));
          // add the substitution to the preprocessing context, which ensures
          // the model for n is correct, as well as substituting it in the input
          // assertions when necessary.
          d_preprocContext->addSubstitution(n, ret);
        }
      }
    }
    cache[n] = ret;
    return ret;
  }
}

PreprocessingPassResult RealToInt::applyInternal(
    AssertionPipeline* assertionsToPreprocess)
{
  std::vector<Node> var_eq;
  for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
  {
    assertionsToPreprocess->replace(
        i, realToIntInternal((*assertionsToPreprocess)[i], d_cache, var_eq));
  }
  return PreprocessingPassResult::NO_CONFLICT;
}


}  // namespace passes
}  // namespace preprocessing
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

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