Head

GCC Code Coverage Report

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