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/bv/abstraction.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/bv/abstraction.cpp')
| -rw-r--r-- | src/theory/bv/abstraction.cpp | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index acb67a373..348c8bebb 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -14,6 +14,7 @@ **/ #include "theory/bv/abstraction.h" +#include "expr/skolem_manager.h" #include "options/bv_options.h" #include "printer/printer.h" #include "smt/dump.h" @@ -282,6 +283,7 @@ Node AbstractionModule::getSignatureSkolem(TNode node) { Assert(node.getMetaKind() == kind::metakind::VARIABLE); NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); unsigned bitwidth = utils::getSize(node); if (d_signatureSkolems.find(bitwidth) == d_signatureSkolems.end()) { @@ -296,9 +298,9 @@ Node AbstractionModule::getSignatureSkolem(TNode node) { ostringstream os; os << "sig_" << bitwidth << "_" << index; - skolems.push_back(nm->mkSkolem(os.str(), - nm->mkBitVectorType(bitwidth), - "skolem for computing signatures")); + skolems.push_back(sm->mkDummySkolem(os.str(), + nm->mkBitVectorType(bitwidth), + "skolem for computing signatures")); } ++(d_signatureIndices[bitwidth]); return skolems[index]; @@ -435,6 +437,7 @@ void AbstractionModule::storeGeneralization(TNode s, TNode t) { void AbstractionModule::finalizeSignatures() { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); Debug("bv-abstraction") << "AbstractionModule::finalizeSignatures num signatures = " << d_signatures.size() << "\n"; @@ -519,8 +522,8 @@ void AbstractionModule::finalizeSignatures() TypeNode range = nm->mkBitVectorType(1); TypeNode abs_type = nm->mkFunctionType(arg_types, range); - Node abs_func = - nm->mkSkolem("abs_$$", abs_type, "abstraction function for bv theory"); + Node abs_func = sm->mkDummySkolem( + "abs_$$", abs_type, "abstraction function for bv theory"); Debug("bv-abstraction") << " abstracted by function " << abs_func << "\n"; // NOTE: signature expression type is BOOLEAN |