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) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel 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 Tvalid 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 toplevel 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 */ 