summaryrefslogtreecommitdiff
path: root/src/theory/fp/theory_fp.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/fp/theory_fp.cpp')
-rw-r--r--src/theory/fp/theory_fp.cpp76
1 files changed, 42 insertions, 34 deletions
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 93b492b88..88d01ea20 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -23,6 +23,7 @@
#include <vector>
#include "base/configuration.h"
+#include "expr/skolem_manager.h"
#include "options/fp_options.h"
#include "smt/logic_exception.h"
#include "theory/fp/fp_converter.h"
@@ -205,6 +206,7 @@ Node TheoryFp::minUF(Node node) {
Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
NodeManager *nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
ComparisonUFMap::const_iterator i(d_minMap.find(t));
Node fun;
@@ -212,16 +214,16 @@ Node TheoryFp::minUF(Node node) {
std::vector<TypeNode> args(2);
args[0] = t;
args[1] = t;
- fun = nm->mkSkolem("floatingpoint_min_zero_case",
- nm->mkFunctionType(args,
+ fun = sm->mkDummySkolem("floatingpoint_min_zero_case",
+ nm->mkFunctionType(args,
#ifdef SYMFPUPROPISBOOL
- nm->booleanType()
+ nm->booleanType()
#else
- nm->mkBitVectorType(1U)
+ nm->mkBitVectorType(1U)
#endif
- ),
- "floatingpoint_min_zero_case",
- NodeManager::SKOLEM_EXACT_NAME);
+ ),
+ "floatingpoint_min_zero_case",
+ NodeManager::SKOLEM_EXACT_NAME);
d_minMap.insert(t, fun);
} else {
fun = (*i).second;
@@ -236,6 +238,7 @@ Node TheoryFp::maxUF(Node node) {
Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
NodeManager *nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
ComparisonUFMap::const_iterator i(d_maxMap.find(t));
Node fun;
@@ -243,16 +246,16 @@ Node TheoryFp::maxUF(Node node) {
std::vector<TypeNode> args(2);
args[0] = t;
args[1] = t;
- fun = nm->mkSkolem("floatingpoint_max_zero_case",
- nm->mkFunctionType(args,
+ fun = sm->mkDummySkolem("floatingpoint_max_zero_case",
+ nm->mkFunctionType(args,
#ifdef SYMFPUPROPISBOOL
- nm->booleanType()
+ nm->booleanType()
#else
- nm->mkBitVectorType(1U)
+ nm->mkBitVectorType(1U)
#endif
- ),
- "floatingpoint_max_zero_case",
- NodeManager::SKOLEM_EXACT_NAME);
+ ),
+ "floatingpoint_max_zero_case",
+ NodeManager::SKOLEM_EXACT_NAME);
d_maxMap.insert(t, fun);
} else {
fun = (*i).second;
@@ -271,6 +274,7 @@ Node TheoryFp::toUBVUF(Node node) {
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;
@@ -278,10 +282,10 @@ Node TheoryFp::toUBVUF(Node node) {
std::vector<TypeNode> args(2);
args[0] = nm->roundingModeType();
args[1] = source;
- fun = nm->mkSkolem("floatingpoint_to_ubv_out_of_range_case",
- nm->mkFunctionType(args, target),
- "floatingpoint_to_ubv_out_of_range_case",
- NodeManager::SKOLEM_EXACT_NAME);
+ 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;
@@ -300,6 +304,7 @@ Node TheoryFp::toSBVUF(Node node) {
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;
@@ -307,10 +312,10 @@ Node TheoryFp::toSBVUF(Node node) {
std::vector<TypeNode> args(2);
args[0] = nm->roundingModeType();
args[1] = source;
- fun = nm->mkSkolem("floatingpoint_to_sbv_out_of_range_case",
- nm->mkFunctionType(args, target),
- "floatingpoint_to_sbv_out_of_range_case",
- NodeManager::SKOLEM_EXACT_NAME);
+ 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;
@@ -324,16 +329,17 @@ Node TheoryFp::toRealUF(Node node) {
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 = nm->mkSkolem("floatingpoint_to_real_infinity_and_NaN_case",
- nm->mkFunctionType(args, nm->realType()),
- "floatingpoint_to_real_infinity_and_NaN_case",
- NodeManager::SKOLEM_EXACT_NAME);
+ 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;
@@ -348,6 +354,7 @@ Node TheoryFp::abstractRealToFloat(Node node)
Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
NodeManager *nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
ComparisonUFMap::const_iterator i(d_realToFloatMap.find(t));
Node fun;
@@ -356,10 +363,10 @@ Node TheoryFp::abstractRealToFloat(Node node)
std::vector<TypeNode> args(2);
args[0] = node[0].getType();
args[1] = node[1].getType();
- fun = nm->mkSkolem("floatingpoint_abstract_real_to_float",
- nm->mkFunctionType(args, node.getType()),
- "floatingpoint_abstract_real_to_float",
- NodeManager::SKOLEM_EXACT_NAME);
+ fun = sm->mkDummySkolem("floatingpoint_abstract_real_to_float",
+ nm->mkFunctionType(args, node.getType()),
+ "floatingpoint_abstract_real_to_float",
+ NodeManager::SKOLEM_EXACT_NAME);
d_realToFloatMap.insert(t, fun);
}
else
@@ -380,6 +387,7 @@ Node TheoryFp::abstractFloatToReal(Node node)
Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
NodeManager *nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
ComparisonUFMap::const_iterator i(d_floatToRealMap.find(t));
Node fun;
@@ -388,10 +396,10 @@ Node TheoryFp::abstractFloatToReal(Node node)
std::vector<TypeNode> args(2);
args[0] = t;
args[1] = nm->realType();
- fun = nm->mkSkolem("floatingpoint_abstract_float_to_real",
- nm->mkFunctionType(args, nm->realType()),
- "floatingpoint_abstract_float_to_real",
- NodeManager::SKOLEM_EXACT_NAME);
+ fun = sm->mkDummySkolem("floatingpoint_abstract_float_to_real",
+ nm->mkFunctionType(args, nm->realType()),
+ "floatingpoint_abstract_float_to_real",
+ NodeManager::SKOLEM_EXACT_NAME);
d_floatToRealMap.insert(t, fun);
}
else
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback