diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-25 08:41:13 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-25 08:41:13 -0500 |
| commit | 87a64143f02c919df14baeb3c1acdd1295df50e9 (patch) | |
| tree | 8a60d9db3d7b37f5436caf456719d4fbc340ef98 /src/expr/skolem_manager.cpp | |
| parent | 23c30f6961f9b19d656a3fb513134ce6c50b82ac (diff) | |
| parent | 8e1eac35d265eacfbeb5f16be61e5d4caf45d1af (diff) | |
Merge branch 'master' into issue6453issue6453
Diffstat (limited to 'src/expr/skolem_manager.cpp')
| -rw-r--r-- | src/expr/skolem_manager.cpp | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index 4004bf6fe..8e1c5e54c 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -53,6 +53,7 @@ const char* toString(SkolemFunId id) case SkolemFunId::SELECTOR_WRONG: return "SELECTOR_WRONG"; case SkolemFunId::SHARED_SELECTOR: return "SHARED_SELECTOR"; case SkolemFunId::SEQ_NTH_OOB: return "SEQ_NTH_OOB"; + case SkolemFunId::RE_UNFOLD_POS_COMPONENT: return "RE_UNFOLD_POS_COMPONENT"; default: return "?"; } } @@ -206,11 +207,37 @@ Node SkolemManager::mkSkolemFunction(SkolemFunId id, ss << "SKOLEM_FUN_" << id; Node k = nm->mkSkolem(ss.str(), tn, "an internal skolem function", flags); d_skolemFuns[key] = k; + d_skolemFunMap[k] = key; return k; } return it->second; } +Node SkolemManager::mkSkolemFunction(SkolemFunId id, + TypeNode tn, + const std::vector<Node>& cacheVals, + int flags) +{ + Assert(cacheVals.size() > 1); + Node cacheVal = NodeManager::currentNM()->mkNode(SEXPR, cacheVals); + return mkSkolemFunction(id, tn, cacheVal, flags); +} + +bool SkolemManager::isSkolemFunction(Node k, + SkolemFunId& id, + Node& cacheVal) const +{ + std::map<Node, std::tuple<SkolemFunId, TypeNode, Node>>::const_iterator it = + d_skolemFunMap.find(k); + if (it == d_skolemFunMap.end()) + { + return false; + } + id = std::get<0>(it->second); + cacheVal = std::get<2>(it->second); + return true; +} + Node SkolemManager::mkDummySkolem(const std::string& prefix, const TypeNode& type, const std::string& comment, |