Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/preprocessing/passes/real_to_int.cpp	Lines:	92	96	95.8 %
Date:	2021-11-07	Branches:	224	464	48.3 %


/******************************************************************************
 * 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"
#include "util/rational.h"

using namespace cvc5::theory;

namespace cvc5 {
namespace preprocessing {
namespace passes {

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

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 = 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]
                                 : 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 = 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		#include "util/rational.h"
29
30		using namespace cvc5::theory;
31
32		namespace cvc5 {
33		namespace preprocessing {
34		namespace passes {
35
36	15340	RealToInt::RealToInt(PreprocessingPassContext* preprocContext)
37	15340	: PreprocessingPass(preprocContext, "real-to-int"), d_cache(userContext())
38		{
39	15340	}
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 = 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	27	Node cc = coeffs.empty()
85		? Node::null()
86	22	: (coeffs.size() == 1
87	15	? coeffs[0]
88	34	: rewrite(NodeManager::currentNM()->mkNode(
89	98	kind::MULT, coeffs)));
90	54	std::vector<Node> sum;
91	79	for (std::map<Node, Node>::iterator itm = msum.begin();
92	79	itm != msum.end();
93		++itm)
94		{
95	104	Node v = itm->first;
96	104	Node c = itm->second;
97	104	Node s;
98	52	if (c.isNull())
99		{
100	19	c = cc.isNull() ? NodeManager::currentNM()->mkConst(Rational(1))
101		: cc;
102		}
103		else
104		{
105	33	if (!cc.isNull())
106		{
107	66	c = rewrite(
108	66	NodeManager::currentNM()->mkNode(kind::MULT, c, cc));
109		}
110		}
111	52	Assert(c.getType().isInteger());
112	52	if (v.isNull())
113		{
114	8	sum.push_back(c);
115		}
116		else
117		{
118	88	Node vv = realToIntInternal(v, cache, var_eq);
119	44	if (vv.getType().isInteger())
120		{
121	44	sum.push_back(
122	88	NodeManager::currentNM()->mkNode(kind::MULT, c, vv));
123		}
124		else
125		{
126		throw TypeCheckingExceptionPrivate(
127		v,
128		std::string("Cannot translate to Int: ") + v.toString());
129		}
130		}
131		}
132		Node sumt =
133	27	sum.empty()
134	27	? NodeManager::currentNM()->mkConst(Rational(0))
135	27	: (sum.size() == 1
136	11	? sum[0]
137	92	: NodeManager::currentNM()->mkNode(kind::PLUS, sum));
138	54	ret = NodeManager::currentNM()->mkNode(
139		ret_lit.getKind(),
140		sumt,
141	54	NodeManager::currentNM()->mkConst(Rational(0)));
142	27	if (!ret_pol)
143		{
144		ret = ret.negate();
145		}
146	27	Trace("real-as-int") << "Convert : " << std::endl;
147	27	Trace("real-as-int") << " " << n << std::endl;
148	27	Trace("real-as-int") << " " << ret << std::endl;
149		}
150		}
151		}
152		else
153		{
154	32	bool childChanged = false;
155	64	std::vector<Node> children;
156	84	for (unsigned i = 0; i < n.getNumChildren(); i++)
157		{
158	104	Node nc = realToIntInternal(n[i], cache, var_eq);
159	52	childChanged = childChanged \|\| nc != n[i];
160	52	children.push_back(nc);
161		}
162	32	if (childChanged)
163		{
164	32	if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
165		{
166	2	children.insert(children.begin(), n.getOperator());
167		}
168	32	ret = NodeManager::currentNM()->mkNode(n.getKind(), children);
169		}
170		}
171		}
172		else
173		{
174	70	TypeNode tn = n.getType();
175	35	if (tn.isReal() && !tn.isInteger())
176		{
177	22	if (n.getKind() == kind::BOUND_VARIABLE)
178		{
179		// cannot change the type of quantified variables, since this leads
180		// to incompleteness.
181		throw TypeCheckingExceptionPrivate(
182		n,
183		std::string("Cannot translate bound variable to Int: ")
184		+ n.toString());
185		}
186	22	else if (n.isVar())
187		{
188	44	Node toIntN = nm->mkNode(kind::TO_INTEGER, n);
189	22	ret = sm->mkPurifySkolem(toIntN, "__realToIntInternal_var");
190	22	var_eq.push_back(n.eqNode(ret));
191		// add the substitution to the preprocessing context, which ensures
192		// the model for n is correct, as well as substituting it in the input
193		// assertions when necessary.
194	22	d_preprocContext->addSubstitution(n, ret);
195		}
196		}
197		}
198	94	cache[n] = ret;
199	94	return ret;
200		}
201		}
202
203	13	PreprocessingPassResult RealToInt::applyInternal(
204		AssertionPipeline* assertionsToPreprocess)
205		{
206	26	std::vector<Node> var_eq;
207	51	for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
208		{
209	38	assertionsToPreprocess->replace(
210	76	i, realToIntInternal((*assertionsToPreprocess)[i], d_cache, var_eq));
211		}
212	26	return PreprocessingPassResult::NO_CONFLICT;
213		}
214
215
216		} // namespace passes
217		} // namespace preprocessing
218	31137	} // namespace cvc5