Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/fp/fp_expand_defs.cpp	Lines:	55	129	42.6 %
Date:	2021-05-24	Branches:	104	630	16.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds
 *
 * 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.
 * ****************************************************************************
 *
 * Expand definitions for floating-point arithmetic.
 */

#include "theory/fp/fp_expand_defs.h"

#include "expr/skolem_manager.h"

namespace cvc5 {
namespace theory {
namespace fp {

FpExpandDefs::FpExpandDefs(context::UserContext* u)
    :

      d_minMap(u),
      d_maxMap(u),
      d_toUBVMap(u),
      d_toSBVMap(u),
      d_toRealMap(u)
{
}

Node FpExpandDefs::minUF(Node node)
{
  Assert(node.getKind() == kind::FLOATINGPOINT_MIN);
  TypeNode t(node.getType());
  Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);

  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  ComparisonUFMap::const_iterator i(d_minMap.find(t));

  Node fun;
  if (i == d_minMap.end())
  {
    std::vector<TypeNode> args(2);
    args[0] = t;
    args[1] = t;
    fun = sm->mkDummySkolem("floatingpoint_min_zero_case",
                            nm->mkFunctionType(args,
#ifdef SYMFPUPROPISBOOL
                                               nm->booleanType()
#else
                                               nm->mkBitVectorType(1U)
#endif
                                                   ),
                            "floatingpoint_min_zero_case",
                            NodeManager::SKOLEM_EXACT_NAME);
    d_minMap.insert(t, fun);
  }
  else
  {
    fun = (*i).second;
  }
  return nm->mkNode(kind::APPLY_UF,
                    fun,
                    node[1],
                    node[0]);  // Application reverses the order or arguments
}

Node FpExpandDefs::maxUF(Node node)
{
  Assert(node.getKind() == kind::FLOATINGPOINT_MAX);
  TypeNode t(node.getType());
  Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);

  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  ComparisonUFMap::const_iterator i(d_maxMap.find(t));

  Node fun;
  if (i == d_maxMap.end())
  {
    std::vector<TypeNode> args(2);
    args[0] = t;
    args[1] = t;
    fun = sm->mkDummySkolem("floatingpoint_max_zero_case",
                            nm->mkFunctionType(args,
#ifdef SYMFPUPROPISBOOL
                                               nm->booleanType()
#else
                                               nm->mkBitVectorType(1U)
#endif
                                                   ),
                            "floatingpoint_max_zero_case",
                            NodeManager::SKOLEM_EXACT_NAME);
    d_maxMap.insert(t, fun);
  }
  else
  {
    fun = (*i).second;
  }
  return nm->mkNode(kind::APPLY_UF, fun, node[1], node[0]);
}

Node FpExpandDefs::toUBVUF(Node node)
{
  Assert(node.getKind() == kind::FLOATINGPOINT_TO_UBV);

  TypeNode target(node.getType());
  Assert(target.getKind() == kind::BITVECTOR_TYPE);

  TypeNode source(node[1].getType());
  Assert(source.getKind() == kind::FLOATINGPOINT_TYPE);

  std::pair<TypeNode, TypeNode> p(source, target);
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  ConversionUFMap::const_iterator i(d_toUBVMap.find(p));

  Node fun;
  if (i == d_toUBVMap.end())
  {
    std::vector<TypeNode> args(2);
    args[0] = nm->roundingModeType();
    args[1] = source;
    fun = sm->mkDummySkolem("floatingpoint_to_ubv_out_of_range_case",
                            nm->mkFunctionType(args, target),
                            "floatingpoint_to_ubv_out_of_range_case",
                            NodeManager::SKOLEM_EXACT_NAME);
    d_toUBVMap.insert(p, fun);
  }
  else
  {
    fun = (*i).second;
  }
  return nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
}

Node FpExpandDefs::toSBVUF(Node node)
{
  Assert(node.getKind() == kind::FLOATINGPOINT_TO_SBV);

  TypeNode target(node.getType());
  Assert(target.getKind() == kind::BITVECTOR_TYPE);

  TypeNode source(node[1].getType());
  Assert(source.getKind() == kind::FLOATINGPOINT_TYPE);

  std::pair<TypeNode, TypeNode> p(source, target);
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  ConversionUFMap::const_iterator i(d_toSBVMap.find(p));

  Node fun;
  if (i == d_toSBVMap.end())
  {
    std::vector<TypeNode> args(2);
    args[0] = nm->roundingModeType();
    args[1] = source;
    fun = sm->mkDummySkolem("floatingpoint_to_sbv_out_of_range_case",
                            nm->mkFunctionType(args, target),
                            "floatingpoint_to_sbv_out_of_range_case",
                            NodeManager::SKOLEM_EXACT_NAME);
    d_toSBVMap.insert(p, fun);
  }
  else
  {
    fun = (*i).second;
  }
  return nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
}

Node FpExpandDefs::toRealUF(Node node)
{
  Assert(node.getKind() == kind::FLOATINGPOINT_TO_REAL);
  TypeNode t(node[0].getType());
  Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);

  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  ComparisonUFMap::const_iterator i(d_toRealMap.find(t));

  Node fun;
  if (i == d_toRealMap.end())
  {
    std::vector<TypeNode> args(1);
    args[0] = t;
    fun = sm->mkDummySkolem("floatingpoint_to_real_infinity_and_NaN_case",
                            nm->mkFunctionType(args, nm->realType()),
                            "floatingpoint_to_real_infinity_and_NaN_case",
                            NodeManager::SKOLEM_EXACT_NAME);
    d_toRealMap.insert(t, fun);
  }
  else
  {
    fun = (*i).second;
  }
  return nm->mkNode(kind::APPLY_UF, fun, node[0]);
}

TrustNode FpExpandDefs::expandDefinition(Node node)
{
  Trace("fp-expandDefinition")
      << "FpExpandDefs::expandDefinition(): " << node << std::endl;

  Node res = node;
  Kind kind = node.getKind();

  if (kind == kind::FLOATINGPOINT_MIN)
  {
    res = NodeManager::currentNM()->mkNode(
        kind::FLOATINGPOINT_MIN_TOTAL, node[0], node[1], minUF(node));
  }
  else if (kind == kind::FLOATINGPOINT_MAX)
  {
    res = NodeManager::currentNM()->mkNode(
        kind::FLOATINGPOINT_MAX_TOTAL, node[0], node[1], maxUF(node));
  }
  else if (kind == kind::FLOATINGPOINT_TO_UBV)
  {
    FloatingPointToUBV info = node.getOperator().getConst<FloatingPointToUBV>();
    FloatingPointToUBVTotal newInfo(info);

    res =
        NodeManager::currentNM()->mkNode(  // kind::FLOATINGPOINT_TO_UBV_TOTAL,
            NodeManager::currentNM()->mkConst(newInfo),
            node[0],
            node[1],
            toUBVUF(node));
  }
  else if (kind == kind::FLOATINGPOINT_TO_SBV)
  {
    FloatingPointToSBV info = node.getOperator().getConst<FloatingPointToSBV>();
    FloatingPointToSBVTotal newInfo(info);

    res =
        NodeManager::currentNM()->mkNode(  // kind::FLOATINGPOINT_TO_SBV_TOTAL,
            NodeManager::currentNM()->mkConst(newInfo),
            node[0],
            node[1],
            toSBVUF(node));
  }
  else if (kind == kind::FLOATINGPOINT_TO_REAL)
  {
    res = NodeManager::currentNM()->mkNode(
        kind::FLOATINGPOINT_TO_REAL_TOTAL, node[0], toRealUF(node));
  }

  if (res != node)
  {
    Trace("fp-expandDefinition") << "FpExpandDefs::expandDefinition(): " << node
                                 << " rewritten to " << res << std::endl;
    return TrustNode::mkTrustRewrite(node, res, nullptr);
  }
  return TrustNode::null();
}

}  // namespace fp
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds
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		* Expand definitions for floating-point arithmetic.
14		*/
15
16		#include "theory/fp/fp_expand_defs.h"
17
18		#include "expr/skolem_manager.h"
19
20		namespace cvc5 {
21		namespace theory {
22		namespace fp {
23
24	9459	FpExpandDefs::FpExpandDefs(context::UserContext* u)
25		:
26
27		d_minMap(u),
28		d_maxMap(u),
29		d_toUBVMap(u),
30		d_toSBVMap(u),
31	9459	d_toRealMap(u)
32		{
33	9459	}
34
35		Node FpExpandDefs::minUF(Node node)
36		{
37		Assert(node.getKind() == kind::FLOATINGPOINT_MIN);
38		TypeNode t(node.getType());
39		Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
40
41		NodeManager* nm = NodeManager::currentNM();
42		SkolemManager* sm = nm->getSkolemManager();
43		ComparisonUFMap::const_iterator i(d_minMap.find(t));
44
45		Node fun;
46		if (i == d_minMap.end())
47		{
48		std::vector<TypeNode> args(2);
49		args[0] = t;
50		args[1] = t;
51		fun = sm->mkDummySkolem("floatingpoint_min_zero_case",
52		nm->mkFunctionType(args,
53		#ifdef SYMFPUPROPISBOOL
54		nm->booleanType()
55		#else
56		nm->mkBitVectorType(1U)
57		#endif
58		),
59		"floatingpoint_min_zero_case",
60		NodeManager::SKOLEM_EXACT_NAME);
61		d_minMap.insert(t, fun);
62		}
63		else
64		{
65		fun = (*i).second;
66		}
67		return nm->mkNode(kind::APPLY_UF,
68		fun,
69		node[1],
70		node[0]); // Application reverses the order or arguments
71		}
72
73	1	Node FpExpandDefs::maxUF(Node node)
74		{
75	1	Assert(node.getKind() == kind::FLOATINGPOINT_MAX);
76	2	TypeNode t(node.getType());
77	1	Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
78
79	1	NodeManager* nm = NodeManager::currentNM();
80	1	SkolemManager* sm = nm->getSkolemManager();
81	1	ComparisonUFMap::const_iterator i(d_maxMap.find(t));
82
83	2	Node fun;
84	1	if (i == d_maxMap.end())
85		{
86	2	std::vector<TypeNode> args(2);
87	1	args[0] = t;
88	1	args[1] = t;
89	3	fun = sm->mkDummySkolem("floatingpoint_max_zero_case",
90	2	nm->mkFunctionType(args,
91		#ifdef SYMFPUPROPISBOOL
92		nm->booleanType()
93		#else
94	2	nm->mkBitVectorType(1U)
95		#endif
96		),
97		"floatingpoint_max_zero_case",
98		NodeManager::SKOLEM_EXACT_NAME);
99	1	d_maxMap.insert(t, fun);
100		}
101		else
102		{
103		fun = (*i).second;
104		}
105	2	return nm->mkNode(kind::APPLY_UF, fun, node[1], node[0]);
106		}
107
108		Node FpExpandDefs::toUBVUF(Node node)
109		{
110		Assert(node.getKind() == kind::FLOATINGPOINT_TO_UBV);
111
112		TypeNode target(node.getType());
113		Assert(target.getKind() == kind::BITVECTOR_TYPE);
114
115		TypeNode source(node[1].getType());
116		Assert(source.getKind() == kind::FLOATINGPOINT_TYPE);
117
118		std::pair<TypeNode, TypeNode> p(source, target);
119		NodeManager* nm = NodeManager::currentNM();
120		SkolemManager* sm = nm->getSkolemManager();
121		ConversionUFMap::const_iterator i(d_toUBVMap.find(p));
122
123		Node fun;
124		if (i == d_toUBVMap.end())
125		{
126		std::vector<TypeNode> args(2);
127		args[0] = nm->roundingModeType();
128		args[1] = source;
129		fun = sm->mkDummySkolem("floatingpoint_to_ubv_out_of_range_case",
130		nm->mkFunctionType(args, target),
131		"floatingpoint_to_ubv_out_of_range_case",
132		NodeManager::SKOLEM_EXACT_NAME);
133		d_toUBVMap.insert(p, fun);
134		}
135		else
136		{
137		fun = (*i).second;
138		}
139		return nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
140		}
141
142		Node FpExpandDefs::toSBVUF(Node node)
143		{
144		Assert(node.getKind() == kind::FLOATINGPOINT_TO_SBV);
145
146		TypeNode target(node.getType());
147		Assert(target.getKind() == kind::BITVECTOR_TYPE);
148
149		TypeNode source(node[1].getType());
150		Assert(source.getKind() == kind::FLOATINGPOINT_TYPE);
151
152		std::pair<TypeNode, TypeNode> p(source, target);
153		NodeManager* nm = NodeManager::currentNM();
154		SkolemManager* sm = nm->getSkolemManager();
155		ConversionUFMap::const_iterator i(d_toSBVMap.find(p));
156
157		Node fun;
158		if (i == d_toSBVMap.end())
159		{
160		std::vector<TypeNode> args(2);
161		args[0] = nm->roundingModeType();
162		args[1] = source;
163		fun = sm->mkDummySkolem("floatingpoint_to_sbv_out_of_range_case",
164		nm->mkFunctionType(args, target),
165		"floatingpoint_to_sbv_out_of_range_case",
166		NodeManager::SKOLEM_EXACT_NAME);
167		d_toSBVMap.insert(p, fun);
168		}
169		else
170		{
171		fun = (*i).second;
172		}
173		return nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
174		}
175
176	4	Node FpExpandDefs::toRealUF(Node node)
177		{
178	4	Assert(node.getKind() == kind::FLOATINGPOINT_TO_REAL);
179	8	TypeNode t(node[0].getType());
180	4	Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
181
182	4	NodeManager* nm = NodeManager::currentNM();
183	4	SkolemManager* sm = nm->getSkolemManager();
184	4	ComparisonUFMap::const_iterator i(d_toRealMap.find(t));
185
186	8	Node fun;
187	4	if (i == d_toRealMap.end())
188		{
189	8	std::vector<TypeNode> args(1);
190	4	args[0] = t;
191	12	fun = sm->mkDummySkolem("floatingpoint_to_real_infinity_and_NaN_case",
192	8	nm->mkFunctionType(args, nm->realType()),
193		"floatingpoint_to_real_infinity_and_NaN_case",
194		NodeManager::SKOLEM_EXACT_NAME);
195	4	d_toRealMap.insert(t, fun);
196		}
197		else
198		{
199		fun = (*i).second;
200		}
201	8	return nm->mkNode(kind::APPLY_UF, fun, node[0]);
202		}
203
204	2593	TrustNode FpExpandDefs::expandDefinition(Node node)
205		{
206	5186	Trace("fp-expandDefinition")
207	2593	<< "FpExpandDefs::expandDefinition(): " << node << std::endl;
208
209	5186	Node res = node;
210	2593	Kind kind = node.getKind();
211
212	2593	if (kind == kind::FLOATINGPOINT_MIN)
213		{
214		res = NodeManager::currentNM()->mkNode(
215		kind::FLOATINGPOINT_MIN_TOTAL, node[0], node[1], minUF(node));
216		}
217	2593	else if (kind == kind::FLOATINGPOINT_MAX)
218		{
219	2	res = NodeManager::currentNM()->mkNode(
220	2	kind::FLOATINGPOINT_MAX_TOTAL, node[0], node[1], maxUF(node));
221		}
222	2592	else if (kind == kind::FLOATINGPOINT_TO_UBV)
223		{
224		FloatingPointToUBV info = node.getOperator().getConst<FloatingPointToUBV>();
225		FloatingPointToUBVTotal newInfo(info);
226
227		res =
228		NodeManager::currentNM()->mkNode( // kind::FLOATINGPOINT_TO_UBV_TOTAL,
229		NodeManager::currentNM()->mkConst(newInfo),
230		node[0],
231		node[1],
232		toUBVUF(node));
233		}
234	2592	else if (kind == kind::FLOATINGPOINT_TO_SBV)
235		{
236		FloatingPointToSBV info = node.getOperator().getConst<FloatingPointToSBV>();
237		FloatingPointToSBVTotal newInfo(info);
238
239		res =
240		NodeManager::currentNM()->mkNode( // kind::FLOATINGPOINT_TO_SBV_TOTAL,
241		NodeManager::currentNM()->mkConst(newInfo),
242		node[0],
243		node[1],
244		toSBVUF(node));
245		}
246	2592	else if (kind == kind::FLOATINGPOINT_TO_REAL)
247		{
248	8	res = NodeManager::currentNM()->mkNode(
249	8	kind::FLOATINGPOINT_TO_REAL_TOTAL, node[0], toRealUF(node));
250		}
251
252	2593	if (res != node)
253		{
254	10	Trace("fp-expandDefinition") << "FpExpandDefs::expandDefinition(): " << node
255	5	<< " rewritten to " << res << std::endl;
256	5	return TrustNode::mkTrustRewrite(node, res, nullptr);
257		}
258	2588	return TrustNode::null();
259		}
260
261		} // namespace fp
262		} // namespace theory
263	28191	} // namespace cvc5