blob: d3b59f895bdfb36cecaf9c3990dc155bc274f7de (
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
92
93
94
95
96
97
98
|
/******************************************************************************
* Top contributors (to current version):
* Andrew Reynolds
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 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.
* ****************************************************************************
*
* Skolem definition manager.
*/
#include "cvc5_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>;
using NodeSet = context::CDHashSet<Node>;
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.
*
* @param literal The literal that became asserted
* @param activatedSkolems The list to add skolems to
* @param useDefs If this flag is true, we add the skolem definition for
* skolems to activatedSkolems instead of the skolem itself.
*/
void notifyAsserted(TNode literal,
std::vector<TNode>& activatedSkolems,
bool useDefs = false);
/**
* 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>& 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 */
|
