diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-08 17:16:50 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-07-08 17:16:50 -0500 |
commit | 77db9e59b783667149c2a71b730e26fe74084073 (patch) | |
tree | 21b2f657b747004a27aa66165a555f72a128f40e /src/theory/sets/skolem_cache.h | |
parent | 1e71ddfb9ac9e368c9f99d351ae7954fb502663e (diff) |
Towards refactoring relations (#3078)
Diffstat (limited to 'src/theory/sets/skolem_cache.h')
-rw-r--r-- | src/theory/sets/skolem_cache.h | 73 |
1 files changed, 73 insertions, 0 deletions
diff --git a/src/theory/sets/skolem_cache.h b/src/theory/sets/skolem_cache.h new file mode 100644 index 000000000..74a8073d4 --- /dev/null +++ b/src/theory/sets/skolem_cache.h @@ -0,0 +1,73 @@ +/********************* */ +/*! \file skolem_cache.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A cache of skolems for theory of sets. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__SETS__SKOLEM_CACHE_H +#define CVC4__THEORY__SETS__SKOLEM_CACHE_H + +#include <map> +#include <unordered_set> + +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace sets { + +/** + * A cache of all set skolems generated by the TheorySets class. This + * cache is used to ensure that duplicate skolems are not generated when + * possible, and helps identify what skolems were allocated in the current run. + */ +class SkolemCache +{ + public: + SkolemCache(); + /** Identifiers for skolem types + * + * The comments below document the properties of each skolem introduced by + * inference in the sets solver, where by skolem we mean the fresh + * set variable that witnesses each of "exists k". + */ + enum SkolemId + { + // (a,b) in join(A,B) => exists k. (a,k) in A ^ (k,b) in B + // This is cached by the nodes corresponding to (a,b) and join(A,B). + SK_JOIN, + }; + + /** + * Makes a skolem of type tn that is cached based on the key (a,b,id). + * Argument c is the variable name of the skolem. + */ + Node mkTypedSkolemCached( + TypeNode tn, Node a, Node b, SkolemId id, const char* c); + /** Same as above, but without caching. */ + Node mkTypedSkolem(TypeNode tn, const char* c); + /** Returns true if n is a skolem allocated by this class */ + bool isSkolem(Node n) const; + + private: + /** map from node pairs and identifiers to skolems */ + std::map<Node, std::map<Node, std::map<SkolemId, Node> > > d_skolemCache; + /** the set of all skolems we have generated */ + std::unordered_set<Node, NodeHashFunction> d_allSkolems; +}; + +} // namespace sets +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__STRINGS__SKOLEM_CACHE_H */ |