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/skolem_manager.h | |
| 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/skolem_manager.h')
| -rw-r--r-- | src/expr/skolem_manager.h | 14 |
1 files changed, 9 insertions, 5 deletions
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. */ |