diff options
Diffstat (limited to 'src/expr/skolem_manager.h')
| -rw-r--r-- | src/expr/skolem_manager.h | 24 |
1 files changed, 21 insertions, 3 deletions
diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index d62153941..a7d35d155 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -29,6 +29,7 @@ class ProofGenerator; /** Skolem function identifier */ enum class SkolemFunId { + NONE, /** 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) */ @@ -43,6 +44,13 @@ enum class SkolemFunId SHARED_SELECTOR, /** an application of seq.nth that is out of bounds */ SEQ_NTH_OOB, + /** + * Regular expression unfold component: if (str.in_re t R), where R is + * (re.++ r0 ... rn), then the RE_UNFOLD_POS_COMPONENT{t,R,i} is a string + * skolem ki such that t = (str.++ k0 ... kn) and (str.in_re k0 r0) for + * i = 0, ..., n. + */ + RE_UNFOLD_POS_COMPONENT, }; /** Converts a skolem function name to a string. */ const char* toString(SkolemFunId id); @@ -235,6 +243,16 @@ class SkolemManager TypeNode tn, Node cacheVal = Node::null(), int flags = NodeManager::SKOLEM_DEFAULT); + /** Same as above, with multiple cache values */ + Node mkSkolemFunction(SkolemFunId id, + TypeNode tn, + const std::vector<Node>& cacheVals, + int flags = NodeManager::SKOLEM_DEFAULT); + /** + * Is k a skolem function? Returns true if k was generated by the above call. + * Updates the arguments to the values used when constructing it. + */ + bool isSkolemFunction(Node k, SkolemFunId& id, Node& cacheVal) const; /** * 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. @@ -281,10 +299,10 @@ class SkolemManager static Node getOriginalForm(Node n); private: - /** - * Cached of skolem functions for mkSkolemFunction above. - */ + /** Cache of skolem functions for mkSkolemFunction above. */ std::map<std::tuple<SkolemFunId, TypeNode, Node>, Node> d_skolemFuns; + /** Backwards mapping of above */ + std::map<Node, std::tuple<SkolemFunId, TypeNode, Node>> d_skolemFunMap; /** * Mapping from witness terms to proof generators. */ |