blob: 1b7b9b4dc2d4ebc888c571e98c38d0ae868db91c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
|
/********************* */
/*! \file skolem_def_manager.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 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 Skolem definition manager
**/
#include "cvc4_private.h"
#ifndef CVC5__PROP__SKOLEM_DEF_MANAGER_H
#define CVC5__PROP__SKOLEM_DEF_MANAGER_H
#include <iosfwd>
#include <unordered_set>
#include <vector>
#include "context/cdhashset.h"
#include "context/cdinsert_hashmap.h"
#include "context/context.h"
#include "expr/node.h"
namespace cvc5 {
namespace prop {
/**
* This class manages the mapping between introduced skolems and the lemmas
* that define their behavior. It can be used to manage which lemmas are
* relevant in the current context, e.g. a lemma corresponding to a skolem
* definition for k is relevant when k appears in an asserted literal.
*
* It also has utilities for tracking (in a SAT-context-dependent manner) which
* skolems are "active", e.g. appear in any asserted literal.
*/
class SkolemDefManager
{
using NodeNodeMap = context::CDInsertHashMap<Node, Node, NodeHashFunction>;
using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
public:
SkolemDefManager(context::Context* context,
context::UserContext* userContext);
~SkolemDefManager();
/**
* Notify skolem definition. This is called when a lemma def is added to the
* SAT solver that corresponds to the skolem definition for skolem k.
*/
void notifySkolemDefinition(TNode k, Node def);
/**
* Get skolem definition for k, where k must be a skolem having a definition
* managed by this class.
*/
TNode getDefinitionForSkolem(TNode k) const;
/**
* Notify that the given literal has been asserted. This method adds skolems
* that become "active" as a result of asserting this literal. A skolem
* is active in the SAT context if it appears in an asserted literal.
*/
void notifyAsserted(TNode literal, std::vector<TNode>& activatedSkolems);
/**
* Get the set of skolems maintained by this class that occur in node n,
* add them to skolems.
*
* @param n The node to traverse
* @param skolems The set where the skolems are added
*/
void getSkolems(TNode n,
std::unordered_set<Node, NodeHashFunction>& skolems) const;
/** Does n have skolems having definitions managed by this class? */
bool hasSkolems(TNode n) const;
private:
/** skolems to definitions (user-context dependent) */
NodeNodeMap d_skDefs;
/** set of active skolems (SAT-context dependent) */
NodeSet d_skActive;
};
} // namespace prop
} // namespace cvc5
#endif /* CVC5__PROP__SKOLEM_DEF_MANAGER_H */
|
