diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-13 14:30:03 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-13 19:30:03 +0000 |
| commit | 10308c88ae5de234eb62c08380d53d4967112ccd (patch) | |
| tree | c60187541a2e5aabda5fd1141ab210900e690126 /src/expr | |
| parent | cdb5c6e7e03e4717f21c5726f02763962c23a7b2 (diff) | |
Formalize more skolems (#6307)
This formalizes more skolems in preparation for moving Theory::expandDefinitions to Rewriter::expandDefinitions.
It also adds proof support for datatypes purification.
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/skolem_manager.cpp | 6 | ||||
| -rw-r--r-- | src/expr/skolem_manager.h | 14 |
2 files changed, 13 insertions, 7 deletions
diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index 1d66cbee2..773159b09 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -50,6 +50,8 @@ const char* toString(SkolemFunId id) case SkolemFunId::INT_DIV_BY_ZERO: return "INT_DIV_BY_ZERO"; case SkolemFunId::MOD_BY_ZERO: return "MOD_BY_ZERO"; case SkolemFunId::SQRT: return "SQRT"; + case SkolemFunId::SELECTOR_WRONG: return "SELECTOR_WRONG"; + case SkolemFunId::SEQ_NTH_OOB: return "SEQ_NTH_OOB"; default: return "?"; } } @@ -190,8 +192,8 @@ Node SkolemManager::mkPurifySkolem(Node t, Node SkolemManager::mkSkolemFunction(SkolemFunId id, TypeNode tn, Node cacheVal) { - std::pair<SkolemFunId, Node> key(id, cacheVal); - std::map<std::pair<SkolemFunId, Node>, Node>::iterator it = + std::tuple<SkolemFunId, TypeNode, Node> key(id, tn, cacheVal); + std::map<std::tuple<SkolemFunId, TypeNode, Node>, Node>::iterator it = d_skolemFuns.find(key); if (it == d_skolemFuns.end()) { diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index 426202b7e..dd228e598 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -29,14 +29,18 @@ class ProofGenerator; /** Skolem function identifier */ enum class SkolemFunId { - /* an uninterpreted function f s.t. f(x) = x / 0.0 (real division) */ + /** an uninterpreted function f s.t. f(x) = x / 0.0 (real division) */ DIV_BY_ZERO, - /* an uninterpreted function f s.t. f(x) = x / 0 (integer division) */ + /** an uninterpreted function f s.t. f(x) = x / 0 (integer division) */ INT_DIV_BY_ZERO, - /* an uninterpreted function f s.t. f(x) = x mod 0 */ + /** an uninterpreted function f s.t. f(x) = x mod 0 */ MOD_BY_ZERO, - /* an uninterpreted function f s.t. f(x) = sqrt(x) */ + /** an uninterpreted function f s.t. f(x) = sqrt(x) */ SQRT, + /** a wrongly applied selector */ + SELECTOR_WRONG, + /** an application of seq.nth that is out of bounds */ + SEQ_NTH_OOB, }; /** Converts a skolem function name to a string. */ const char* toString(SkolemFunId id); @@ -283,7 +287,7 @@ class SkolemManager /** * Cached of skolem functions for mkSkolemFunction above. */ - std::map<std::pair<SkolemFunId, Node>, Node> d_skolemFuns; + std::map<std::tuple<SkolemFunId, TypeNode, Node>, Node> d_skolemFuns; /** * Mapping from witness terms to proof generators. */ |