Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/relevance_manager.h	Lines:	1	1	100.0 %
Date:	2021-11-07	Branches:	0	0	0.0 %


/******************************************************************************
 * 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.
 * ****************************************************************************
 *
 * Relevance manager.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__RELEVANCE_MANAGER__H
#define CVC5__THEORY__RELEVANCE_MANAGER__H

#include <unordered_map>
#include <unordered_set>

#include "context/cdlist.h"
#include "expr/node.h"
#include "theory/difficulty_manager.h"
#include "theory/valuation.h"

namespace cvc5 {
namespace theory {

class TheoryModel;

/**
 * This class manages queries related to relevance of asserted literals.
 * In particular, note the following definition:
 *
 * Let F be a formula, and let L = { l_1, ..., l_n } be a set of
 * literals that propositionally entail it. A "relevant selection of L with
 * respect to F" is a subset of L that also propositionally entails F.
 *
 * This class computes a relevant selection of the current assertion stack
 * at FULL effort with respect to the input formula + theory lemmas that are
 * critical to justify (see LemmaProperty::NEEDS_JUSTIFY). By default, theory
 * lemmas are not critical to justify; in fact, all T-valid theory lemmas
 * are not critical to justify, since they are guaranteed to be satisfied in
 * all inputs. However, some theory lemmas that introduce skolems need
 * justification.
 *
 * As an example of such a lemma, take the example input formula:
 *   (and (exists ((x Int)) (P x)) (not (P 0)))
 * A skolemization lemma like the following needs justification:
 *   (=> (exists ((x Int)) (P x)) (P k))
 * Intuitively, this is because the satisfiability of the existential above is
 * being deferred to the satisfiability of (P k) where k is fresh. Thus,
 * a relevant selection must include both (exists ((x Int)) (P x)) and (P k)
 * in this example.
 *
 * Theories are responsible for marking such lemmas using the NEEDS_JUSTIFY
 * property when calling OutputChannel::lemma.
 *
 * Notice that this class has some relation to the justification decision
 * heuristic (--decision=justification), which constructs a relevant selection
 * of the input formula by construction. This class is orthogonal to this
 * method, since it computes relevant selection *after* a full assignment. Thus
 * its main advantage with respect to decision=justification is that it can be
 * used in combination with any SAT decision heuristic.
 *
 * Internally, this class stores the input assertions and can be asked if an
 * asserted literal is part of the current relevant selection. The relevant
 * selection is computed lazily, i.e. only when someone asks if a literal is
 * relevant, and only at most once per FULL effort check.
 */
class RelevanceManager
{
  typedef context::CDList<Node> NodeList;

 public:
  /**
   * @param lemContext The context which lemmas live at
   * @param val The valuation class, for computing what is relevant.
   */
  RelevanceManager(context::Context* lemContext, Valuation val);
  /**
   * Notify (preprocessed) assertions. This is called for input formulas or
   * lemmas that need justification that have been fully processed, just before
   * adding them to the PropEngine.
   */
  void notifyPreprocessedAssertions(const std::vector<Node>& assertions);
  /** Singleton version of above */
  void notifyPreprocessedAssertion(Node n);
  /**
   * Reset round, called at the beginning of a full effort check in
   * TheoryEngine.
   */
  void resetRound();
  /**
   * Is lit part of the current relevant selection? This computes the set of
   * relevant assertions if not already done so. This call is valid during a
   * full effort check in TheoryEngine, or after TheoryEngine has terminated
   * with "sat". This means that theories can query this during FULL or
   * LAST_CALL efforts, through the Valuation class.
   */
  bool isRelevant(Node lit);
  /**
   * Get the current relevant selection (see above). This computes this set
   * if not already done so. This call is valid during a full effort check in
   * TheoryEngine, or after TheoryEngine has terminated with "sat". This method
   * sets the flag success to false if we failed to compute relevant
   * assertions, which occurs if the values from the SAT solver do not satisfy
   * the assertions we are notified of. This should never happen.
   *
   * The value of this return is only valid if success was not updated to false.
   */
  const std::unordered_set<TNode>& getRelevantAssertions(bool& success);
  /** Notify lemma, for difficulty measurements */
  void notifyLemma(Node n);
  /** Notify that m is a (candidate) model, for difficulty measurements */
  void notifyCandidateModel(TheoryModel* m);
  /**
   * Get difficulty map
   */
  void getDifficultyMap(std::map<Node, Node>& dmap);

 private:
  /**
   * Add the set of assertions to the formulas known to this class. This
   * method handles optimizations such as breaking apart top-level applications
   * of and.
   */
  void addAssertionsInternal(std::vector<Node>& toProcess);
  /** compute the relevant selection */
  void computeRelevance();
  /**
   * Justify formula n. To "justify" means we have added literals to our
   * relevant selection set (d_rset) whose current values ensure that n
   * evaluates to true or false.
   *
   * This method returns 1 if we justified n to be true, -1 means
   * justified n to be false, 0 means n could not be justified.
   */
  int justify(TNode n, std::unordered_map<TNode, int>& cache);
  /** Is the top symbol of cur a Boolean connective? */
  bool isBooleanConnective(TNode cur);
  /**
   * Update justify last child. This method is a helper function for justify,
   * which is called at the moment that Boolean connective formula cur
   * has a new child that has been computed in the justify cache.
   *
   * @param cur The Boolean connective formula
   * @param childrenJustify The values of the previous children (not including
   * the current one)
   * @param cache The justify cache
   * @return True if we wish to visit the next child. If this is the case, then
   * the justify value of the current child is added to childrenJustify.
   */
  bool updateJustifyLastChild(TNode cur,
                              std::vector<int>& childrenJustify,
                              std::unordered_map<TNode, int>& cache);
  /** The valuation object, used to query current value of theory literals */
  Valuation d_val;
  /** The input assertions */
  NodeList d_input;
  /** The current relevant selection. */
  std::unordered_set<TNode> d_rset;
  /** Have we computed the relevant selection this round? */
  bool d_computed;
  /**
   * Did we succeed in computing the relevant selection? If this is false, there
   * was a syncronization issue between the input formula and the satisfying
   * assignment since this class found that the input formula was not satisfied
   * by the assignment. This should never happen, but if it does, this class
   * aborts and indicates that all literals are relevant.
   */
  bool d_success;
  /** Are we tracking the sources of why a literal is relevant */
  bool d_trackRSetExp;
  /**
   * Whether we have miniscoped top-level AND of assertions, which is done
   * as an optimization. This is disabled if e.g. we are computing difficulty,
   * which requires preserving the original form of the preprocessed
   * assertions.
   */
  bool d_miniscopeTopLevel;
  /**
   * Map from the domain of d_rset to the assertion in d_input that is the
   * reason why that literal is currently relevant.
   */
  std::map<TNode, TNode> d_rsetExp;
  /** Difficulty module */
  std::unique_ptr<DifficultyManager> d_dman;
};

}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY__RELEVANCE_MANAGER__H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds
4		*
5		* This file is part of the cvc5 project.
6		*
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.
11		* ****************************************************************************
12		*
13		* Relevance manager.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__RELEVANCE_MANAGER__H
19		#define CVC5__THEORY__RELEVANCE_MANAGER__H
20
21		#include <unordered_map>
22		#include <unordered_set>
23
24		#include "context/cdlist.h"
25		#include "expr/node.h"
26		#include "theory/difficulty_manager.h"
27		#include "theory/valuation.h"
28
29		namespace cvc5 {
30		namespace theory {
31
32		class TheoryModel;
33
34		/**
35		* This class manages queries related to relevance of asserted literals.
36		* In particular, note the following definition:
37		*
38		* Let F be a formula, and let L = { l_1, ..., l_n } be a set of
39		* literals that propositionally entail it. A "relevant selection of L with
40		* respect to F" is a subset of L that also propositionally entails F.
41		*
42		* This class computes a relevant selection of the current assertion stack
43		* at FULL effort with respect to the input formula + theory lemmas that are
44		* critical to justify (see LemmaProperty::NEEDS_JUSTIFY). By default, theory
45		* lemmas are not critical to justify; in fact, all T-valid theory lemmas
46		* are not critical to justify, since they are guaranteed to be satisfied in
47		* all inputs. However, some theory lemmas that introduce skolems need
48		* justification.
49		*
50		* As an example of such a lemma, take the example input formula:
51		* (and (exists ((x Int)) (P x)) (not (P 0)))
52		* A skolemization lemma like the following needs justification:
53		* (=> (exists ((x Int)) (P x)) (P k))
54		* Intuitively, this is because the satisfiability of the existential above is
55		* being deferred to the satisfiability of (P k) where k is fresh. Thus,
56		* a relevant selection must include both (exists ((x Int)) (P x)) and (P k)
57		* in this example.
58		*
59		* Theories are responsible for marking such lemmas using the NEEDS_JUSTIFY
60		* property when calling OutputChannel::lemma.
61		*
62		* Notice that this class has some relation to the justification decision
63		* heuristic (--decision=justification), which constructs a relevant selection
64		* of the input formula by construction. This class is orthogonal to this
65		* method, since it computes relevant selection after a full assignment. Thus
66		* its main advantage with respect to decision=justification is that it can be
67		* used in combination with any SAT decision heuristic.
68		*
69		* Internally, this class stores the input assertions and can be asked if an
70		* asserted literal is part of the current relevant selection. The relevant
71		* selection is computed lazily, i.e. only when someone asks if a literal is
72		* relevant, and only at most once per FULL effort check.
73		*/
74	23	class RelevanceManager
75		{
76		typedef context::CDList<Node> NodeList;
77
78		public:
79		/**
80		* @param lemContext The context which lemmas live at
81		* @param val The valuation class, for computing what is relevant.
82		*/
83		RelevanceManager(context::Context* lemContext, Valuation val);
84		/**
85		* Notify (preprocessed) assertions. This is called for input formulas or
86		* lemmas that need justification that have been fully processed, just before
87		* adding them to the PropEngine.
88		*/
89		void notifyPreprocessedAssertions(const std::vector<Node>& assertions);
90		/** Singleton version of above */
91		void notifyPreprocessedAssertion(Node n);
92		/**
93		* Reset round, called at the beginning of a full effort check in
94		* TheoryEngine.
95		*/
96		void resetRound();
97		/**
98		* Is lit part of the current relevant selection? This computes the set of
99		* relevant assertions if not already done so. This call is valid during a
100		* full effort check in TheoryEngine, or after TheoryEngine has terminated
101		* with "sat". This means that theories can query this during FULL or
102		* LAST_CALL efforts, through the Valuation class.
103		*/
104		bool isRelevant(Node lit);
105		/**
106		* Get the current relevant selection (see above). This computes this set
107		* if not already done so. This call is valid during a full effort check in
108		* TheoryEngine, or after TheoryEngine has terminated with "sat". This method
109		* sets the flag success to false if we failed to compute relevant
110		* assertions, which occurs if the values from the SAT solver do not satisfy
111		* the assertions we are notified of. This should never happen.
112		*
113		* The value of this return is only valid if success was not updated to false.
114		*/
115		const std::unordered_set<TNode>& getRelevantAssertions(bool& success);
116		/** Notify lemma, for difficulty measurements */
117		void notifyLemma(Node n);
118		/** Notify that m is a (candidate) model, for difficulty measurements */
119		void notifyCandidateModel(TheoryModel* m);
120		/**
121		* Get difficulty map
122		*/
123		void getDifficultyMap(std::map<Node, Node>& dmap);
124
125		private:
126		/**
127		* Add the set of assertions to the formulas known to this class. This
128		* method handles optimizations such as breaking apart top-level applications
129		* of and.
130		*/
131		void addAssertionsInternal(std::vector<Node>& toProcess);
132		/** compute the relevant selection */
133		void computeRelevance();
134		/**
135		* Justify formula n. To "justify" means we have added literals to our
136		* relevant selection set (d_rset) whose current values ensure that n
137		* evaluates to true or false.
138		*
139		* This method returns 1 if we justified n to be true, -1 means
140		* justified n to be false, 0 means n could not be justified.
141		*/
142		int justify(TNode n, std::unordered_map<TNode, int>& cache);
143		/** Is the top symbol of cur a Boolean connective? */
144		bool isBooleanConnective(TNode cur);
145		/**
146		* Update justify last child. This method is a helper function for justify,
147		* which is called at the moment that Boolean connective formula cur
148		* has a new child that has been computed in the justify cache.
149		*
150		* @param cur The Boolean connective formula
151		* @param childrenJustify The values of the previous children (not including
152		* the current one)
153		* @param cache The justify cache
154		* @return True if we wish to visit the next child. If this is the case, then
155		* the justify value of the current child is added to childrenJustify.
156		*/
157		bool updateJustifyLastChild(TNode cur,
158		std::vector<int>& childrenJustify,
159		std::unordered_map<TNode, int>& cache);
160		/** The valuation object, used to query current value of theory literals */
161		Valuation d_val;
162		/** The input assertions */
163		NodeList d_input;
164		/** The current relevant selection. */
165		std::unordered_set<TNode> d_rset;
166		/** Have we computed the relevant selection this round? */
167		bool d_computed;
168		/**
169		* Did we succeed in computing the relevant selection? If this is false, there
170		* was a syncronization issue between the input formula and the satisfying
171		* assignment since this class found that the input formula was not satisfied
172		* by the assignment. This should never happen, but if it does, this class
173		* aborts and indicates that all literals are relevant.
174		*/
175		bool d_success;
176		/** Are we tracking the sources of why a literal is relevant */
177		bool d_trackRSetExp;
178		/**
179		* Whether we have miniscoped top-level AND of assertions, which is done
180		* as an optimization. This is disabled if e.g. we are computing difficulty,
181		* which requires preserving the original form of the preprocessed
182		* assertions.
183		*/
184		bool d_miniscopeTopLevel;
185		/**
186		* Map from the domain of d_rset to the assertion in d_input that is the
187		* reason why that literal is currently relevant.
188		*/
189		std::map<TNode, TNode> d_rsetExp;
190		/** Difficulty module */
191		std::unique_ptr<DifficultyManager> d_dman;
192		};
193
194		} // namespace theory
195		} // namespace cvc5
196
197		#endif /* CVC5__THEORY__RELEVANCE_MANAGER__H */