1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
|
/********************* */
/*! \file theory_fp.cpp
** \verbatim
** Top contributors (to current version):
** Martin Brain, Tim King, Paul Meng
** This file is part of the CVC4 project.
** Copyright (c) 2009-2017 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.\endverbatim
**
** \brief [[ Add one-line brief description here ]]
**
** [[ Add lengthier description here ]]
** \todo document this file
**/
#include "theory/fp/theory_fp.h"
using namespace std;
namespace CVC4 {
namespace theory {
namespace fp {
namespace removeToFPGeneric {
Node removeToFPGeneric (TNode node) {
Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC);
FloatingPointToFPGeneric info =
node.getOperator().getConst<FloatingPointToFPGeneric>();
size_t children = node.getNumChildren();
Node op;
if (children == 1) {
op = NodeManager::currentNM()->mkConst(
FloatingPointToFPIEEEBitVector(info.t.exponent(),
info.t.significand()));
return NodeManager::currentNM()->mkNode(op, node[0]);
} else {
Assert(children == 2);
Assert(node[0].getType().isRoundingMode());
TypeNode t = node[1].getType();
if (t.isFloatingPoint()) {
op = NodeManager::currentNM()->mkConst(
FloatingPointToFPFloatingPoint(info.t.exponent(),
info.t.significand()));
} else if (t.isReal()) {
op = NodeManager::currentNM()->mkConst(
FloatingPointToFPReal(info.t.exponent(),
info.t.significand()));
} else if (t.isBitVector()) {
op = NodeManager::currentNM()->mkConst(
FloatingPointToFPSignedBitVector(info.t.exponent(),
info.t.significand()));
} else {
throw TypeCheckingExceptionPrivate(
node,
"cannot rewrite to_fp generic due to incorrect type of second "
"argument");
}
return NodeManager::currentNM()->mkNode(op, node[0], node[1]);
}
Unreachable("to_fp generic not rewritten");
}
}
/** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
TheoryFp::TheoryFp(context::Context* c, context::UserContext* u,
OutputChannel& out, Valuation valuation,
const LogicInfo& logicInfo)
: Theory(THEORY_FP, c, u, out, valuation, logicInfo)
{}/* TheoryFp::TheoryFp() */
Node TheoryFp::expandDefinition(LogicRequest &, Node node) {
Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node << std::endl;
if (node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC) {
Node res(removeToFPGeneric::removeToFPGeneric(node));
Trace("fp-expandDefinition") << "TO_FP_GENERIC rewritten to " << res << std::endl;
return res;
} else {
return node;
}
}
void TheoryFp::check(Effort level) {
if (done() && !fullEffort(level)) {
return;
}
while(!done()) {
// Get all the assertions
Assertion assertion = get();
TNode fact = assertion.assertion;
Debug("fp") << "TheoryFp::check(): processing " << fact << std::endl;
// Do the work
switch(fact.getKind()) {
/* cases for all the theory's kinds go here... */
default:
Unhandled(fact.getKind());
}
}
}/* TheoryFp::check() */
}/* CVC4::theory::fp namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
|
