diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-21 16:07:50 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-21 21:07:50 +0000 |
| commit | 08218e74b729bd7da4d95ecd77bdd696a22bb687 (patch) | |
| tree | 8e744877435654adcd499533a712dec0b36a9d19 /src/expr/skolem_manager.cpp | |
| parent | d99cc0f25aad013886a9648c93423c64fab9bdd4 (diff) | |
Formalize shared selectors as skolem functions (#6591)
This is work towards properly printing shared selectors in external proofs.
Diffstat (limited to 'src/expr/skolem_manager.cpp')
| -rw-r--r-- | src/expr/skolem_manager.cpp | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index bb29f84ee..4004bf6fe 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -51,6 +51,7 @@ const char* toString(SkolemFunId id) case SkolemFunId::MOD_BY_ZERO: return "MOD_BY_ZERO"; case SkolemFunId::SQRT: return "SQRT"; case SkolemFunId::SELECTOR_WRONG: return "SELECTOR_WRONG"; + case SkolemFunId::SHARED_SELECTOR: return "SHARED_SELECTOR"; case SkolemFunId::SEQ_NTH_OOB: return "SEQ_NTH_OOB"; default: return "?"; } @@ -190,7 +191,10 @@ Node SkolemManager::mkPurifySkolem(Node t, return k; } -Node SkolemManager::mkSkolemFunction(SkolemFunId id, TypeNode tn, Node cacheVal) +Node SkolemManager::mkSkolemFunction(SkolemFunId id, + TypeNode tn, + Node cacheVal, + int flags) { std::tuple<SkolemFunId, TypeNode, Node> key(id, tn, cacheVal); std::map<std::tuple<SkolemFunId, TypeNode, Node>, Node>::iterator it = @@ -200,7 +204,7 @@ Node SkolemManager::mkSkolemFunction(SkolemFunId id, TypeNode tn, Node cacheVal) NodeManager* nm = NodeManager::currentNM(); std::stringstream ss; ss << "SKOLEM_FUN_" << id; - Node k = nm->mkSkolem(ss.str(), tn, "an internal skolem function"); + Node k = nm->mkSkolem(ss.str(), tn, "an internal skolem function", flags); d_skolemFuns[key] = k; return k; } |