diff options
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. */ |