diff options
| -rw-r--r-- | src/expr/dtype.cpp | 13 | ||||
| -rw-r--r-- | src/expr/skolem_manager.cpp | 8 | ||||
| -rw-r--r-- | src/expr/skolem_manager.h | 5 |
3 files changed, 18 insertions, 8 deletions
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index 9e09c06e6..52c15a08d 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -100,7 +100,8 @@ const DType& DType::datatypeOf(Node item) { case CONSTRUCTOR_TYPE: return t[t.getNumChildren() - 1].getDType(); case SELECTOR_TYPE: - case TESTER_TYPE: return t[0].getDType(); + case TESTER_TYPE: + case UPDATER_TYPE: return t[0].getDType(); default: Unhandled() << "arg must be a datatype constructor, selector, or tester"; } @@ -864,10 +865,12 @@ Node DType::getSharedSelector(TypeNode dtt, TypeNode t, size_t index) const std::stringstream ss; ss << "sel_" << index; SkolemManager* sm = nm->getSkolemManager(); - s = sm->mkDummySkolem(ss.str(), - nm->mkSelectorType(dtt, t), - "is a shared selector", - NodeManager::SKOLEM_NO_NOTIFY); + TypeNode stype = nm->mkSelectorType(dtt, t); + Node nindex = nm->mkConst(Rational(index)); + s = sm->mkSkolemFunction(SkolemFunId::SHARED_SELECTOR, + stype, + nindex, + NodeManager::SKOLEM_NO_NOTIFY); d_sharedSel[dtt][t][index] = s; Trace("dt-shared-sel") << "Made " << s << " of type " << dtt << " -> " << t << std::endl; 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; } diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index a6709373c..d62153941 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -39,6 +39,8 @@ enum class SkolemFunId SQRT, /** a wrongly applied selector */ SELECTOR_WRONG, + /** a shared selector */ + SHARED_SELECTOR, /** an application of seq.nth that is out of bounds */ SEQ_NTH_OOB, }; @@ -231,7 +233,8 @@ class SkolemManager */ Node mkSkolemFunction(SkolemFunId id, TypeNode tn, - Node cacheVal = Node::null()); + Node cacheVal = Node::null(), + int flags = NodeManager::SKOLEM_DEFAULT); /** * Create a skolem constant with the given name, type, and comment. This * should only be used if the definition of the skolem does not matter. |