Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/fp/fp_expand_defs.cpp	Lines:	80	129	62.0 %
Date:	2021-09-10	Branches:	152	628	24.2 %


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