diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-07 13:36:15 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-07 18:36:15 +0000 |
commit | 04a494e251a8cc2c90bb429e2858f1c4eb8f88ff (patch) | |
tree | 03b1a5792f2f6ca5537353b86682f427090668da /src/theory/fp/theory_fp.cpp | |
parent | 5059658ee0d6fc65e4cb1652c605895d016cd274 (diff) |
Replace calls to NodeManager::mkSkolem with SkolemManager::mkDummySkolem (#6291)
This is in preparation for refactoring skolem creation throughout the code base to improve proofs and migrate Theory::expandDefinitions to Rewriter::expandDefinitions.
This PR also eliminates some unused code in TheoryArithPrivate.
Followup PRs will start formalizing/eliminating calls to mkDummySkolem.
Diffstat (limited to 'src/theory/fp/theory_fp.cpp')
-rw-r--r-- | src/theory/fp/theory_fp.cpp | 76 |
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 |