GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/relevance_manager.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file relevance_manager.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Relevance manager.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__RELEVANCE_MANAGER__H
18
#define CVC4__THEORY__RELEVANCE_MANAGER__H
19
20
#include <unordered_map>
21
#include <unordered_set>
22
23
#include "context/cdlist.h"
24
#include "expr/node.h"
25
#include "theory/valuation.h"
26
27
namespace CVC4 {
28
namespace theory {
29
30
/**
31
 * This class manages queries related to relevance of asserted literals.
32
 * In particular, note the following definition:
33
 *
34
 * Let F be a formula, and let L = { l_1, ..., l_n } be a set of
35
 * literals that propositionally entail it. A "relevant selection of L with
36
 * respect to F" is a subset of L that also propositionally entails F.
37
 *
38
 * This class computes a relevant selection of the current assertion stack
39
 * at FULL effort with respect to the input formula + theory lemmas that are
40
 * critical to justify (see LemmaProperty::NEEDS_JUSTIFY). By default, theory
41
 * lemmas are not critical to justify; in fact, all T-valid theory lemmas
42
 * are not critical to justify, since they are guaranteed to be satisfied in
43
 * all inputs. However, some theory lemmas that introduce skolems need
44
 * justification.
45
 *
46
 * As an example of such a lemma, take the example input formula:
47
 *   (and (exists ((x Int)) (P x)) (not (P 0)))
48
 * A skolemization lemma like the following needs justification:
49
 *   (=> (exists ((x Int)) (P x)) (P k))
50
 * Intuitively, this is because the satisfiability of the existential above is
51
 * being deferred to the satisfiability of (P k) where k is fresh. Thus,
52
 * a relevant selection must include both (exists ((x Int)) (P x)) and (P k)
53
 * in this example.
54
 *
55
 * Theories are responsible for marking such lemmas using the NEEDS_JUSTIFY
56
 * property when calling OutputChannel::lemma.
57
 *
58
 * Notice that this class has some relation to the justification decision
59
 * heuristic (--decision=justification), which constructs a relevant selection
60
 * of the input formula by construction. This class is orthogonal to this
61
 * method, since it computes relevant selection *after* a full assignment. Thus
62
 * its main advantage with respect to decision=justification is that it can be
63
 * used in combination with any SAT decision heuristic.
64
 *
65
 * Internally, this class stores the input assertions and can be asked if an
66
 * asserted literal is part of the current relevant selection. The relevant
67
 * selection is computed lazily, i.e. only when someone asks if a literal is
68
 * relevant, and only at most once per FULL effort check.
69
 */
70
10
class RelevanceManager
71
{
72
  typedef context::CDList<Node> NodeList;
73
74
 public:
75
  RelevanceManager(context::UserContext* userContext, Valuation val);
76
  /**
77
   * Notify (preprocessed) assertions. This is called for input formulas or
78
   * lemmas that need justification that have been fully processed, just before
79
   * adding them to the PropEngine.
80
   */
81
  void notifyPreprocessedAssertions(const std::vector<Node>& assertions);
82
  /** Singleton version of above */
83
  void notifyPreprocessedAssertion(Node n);
84
  /**
85
   * Reset round, called at the beginning of a full effort check in
86
   * TheoryEngine.
87
   */
88
  void resetRound();
89
  /**
90
   * Is lit part of the current relevant selection? This call is valid during
91
   * full effort check in TheoryEngine. This means that theories can query this
92
   * during FULL or LAST_CALL efforts, through the Valuation class.
93
   */
94
  bool isRelevant(Node lit);
95
96
 private:
97
  /**
98
   * Add the set of assertions to the formulas known to this class. This
99
   * method handles optimizations such as breaking apart top-level applications
100
   * of and.
101
   */
102
  void addAssertionsInternal(std::vector<Node>& toProcess);
103
  /** compute the relevant selection */
104
  void computeRelevance();
105
  /**
106
   * Justify formula n. To "justify" means we have added literals to our
107
   * relevant selection set (d_rset) whose current values ensure that n
108
   * evaluates to true or false.
109
   *
110
   * This method returns 1 if we justified n to be true, -1 means
111
   * justified n to be false, 0 means n could not be justified.
112
   */
113
  int justify(TNode n,
114
              std::unordered_map<TNode, int, TNodeHashFunction>& cache);
115
  /** Is the top symbol of cur a Boolean connective? */
116
  bool isBooleanConnective(TNode cur);
117
  /**
118
   * Update justify last child. This method is a helper function for justify,
119
   * which is called at the moment that Boolean connective formula cur
120
   * has a new child that has been computed in the justify cache.
121
   *
122
   * @param cur The Boolean connective formula
123
   * @param childrenJustify The values of the previous children (not including
124
   * the current one)
125
   * @param cache The justify cache
126
   * @return True if we wish to visit the next child. If this is the case, then
127
   * the justify value of the current child is added to childrenJustify.
128
   */
129
  bool updateJustifyLastChild(
130
      TNode cur,
131
      std::vector<int>& childrenJustify,
132
      std::unordered_map<TNode, int, TNodeHashFunction>& cache);
133
  /** The valuation object, used to query current value of theory literals */
134
  Valuation d_val;
135
  /** The input assertions */
136
  NodeList d_input;
137
  /** The current relevant selection. */
138
  std::unordered_set<TNode, TNodeHashFunction> d_rset;
139
  /** Have we computed the relevant selection this round? */
140
  bool d_computed;
141
  /**
142
   * Did we succeed in computing the relevant selection? If this is false, there
143
   * was a syncronization issue between the input formula and the satisfying
144
   * assignment since this class found that the input formula was not satisfied
145
   * by the assignment. This should never happen, but if it does, this class
146
   * aborts and indicates that all literals are relevant.
147
   */
148
  bool d_success;
149
};
150
151
}  // namespace theory
152
}  // namespace CVC4
153
154
#endif /* CVC4__THEORY__RELEVANCE_MANAGER__H */