Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/valuation.h	Lines:	3	3	100.0 %
Date:	2021-05-22	Branches:	0	0	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Morgan Deters, Dejan Jovanovic
 *
 * 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.
 * ****************************************************************************
 *
 * A "valuation" proxy for TheoryEngine
 *
 * A "valuation" proxy for TheoryEngine.  This class breaks the dependence
 * of theories' getValue() implementations on TheoryEngine.  getValue()
 * takes a Valuation, which delegates to TheoryEngine.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__VALUATION_H
#define CVC5__THEORY__VALUATION_H

#include "context/cdlist.h"
#include "expr/node.h"
#include "options/theory_options.h"

namespace cvc5 {

class TheoryEngine;

namespace theory {

struct Assertion;
class TheoryModel;
class SortInference;

/**
 * The status of an equality in the current context.
 */
enum EqualityStatus {
  /** The equality is known to be true and has been propagated */
  EQUALITY_TRUE_AND_PROPAGATED,
  /** The equality is known to be false and has been propagated */
  EQUALITY_FALSE_AND_PROPAGATED,
  /** The equality is known to be true */
  EQUALITY_TRUE,
  /** The equality is known to be false */
  EQUALITY_FALSE,
  /** The equality is not known, but is true in the current model */
  EQUALITY_TRUE_IN_MODEL,
  /** The equality is not known, but is false in the current model */
  EQUALITY_FALSE_IN_MODEL,
  /** The equality is completely unknown */
  EQUALITY_UNKNOWN
};/* enum EqualityStatus */

std::ostream& operator<<(std::ostream& os, EqualityStatus s);

/**
 * Returns true if the two statuses are compatible, i.e. both TRUE
 * or both FALSE (regardless of inmodel/propagation).
 */
bool equalityStatusCompatible(EqualityStatus s1, EqualityStatus s2);

class Valuation {
  TheoryEngine* d_engine;
public:
  Valuation(TheoryEngine* engine) :
    d_engine(engine) {
  }

  /**
   * Return true if n has an associated SAT literal
   */
  bool isSatLiteral(TNode n) const;

  /**
   * Get the current SAT assignment to the node n.
   *
   * This is only permitted if n is a theory atom that has an associated
   * SAT literal (or its negation).
   *
   * @return Node::null() if no current assignment; otherwise true or false.
   */
  Node getSatValue(TNode n) const;

  /**
   * Returns true if the node has a current SAT assignment. If yes, the
   * argument "value" is set to its value.
   *
   * This is only permitted if n is a theory atom that has an associated
   * SAT literal.
   *
   * @return true if the literal has a current assignment, and returns the
   * value in the "value" argument; otherwise false and the "value"
   * argument is unmodified.
   */
  bool hasSatValue(TNode n, bool& value) const;

  /**
   * Returns the equality status of the two terms, from the theory that owns the domain type.
   * The types of a and b must be the same.
   */
  EqualityStatus getEqualityStatus(TNode a, TNode b);

  /**
   * Returns the model value of the shared term (or null if not available).
   */
  Node getModelValue(TNode var);

  /**
   * Returns pointer to model. This model is only valid during last call effort
   * check.
   */
  TheoryModel* getModel();
  /**
   * Returns a pointer to the sort inference module, which lives in TheoryEngine
   * and is non-null when options::sortInference is true.
   */
  SortInference* getSortInference();

  //-------------------------------------- static configuration of the model
  /**
   * Set that k is an unevaluated kind in the TheoryModel, if it exists.
   * See TheoryModel::setUnevaluatedKind for details.
   */
  void setUnevaluatedKind(Kind k);
  /**
   * Set that k is an unevaluated kind in the TheoryModel, if it exists.
   * See TheoryModel::setSemiEvaluatedKind for details.
   */
  void setSemiEvaluatedKind(Kind k);
  /**
   * Set that k is an irrelevant kind in the TheoryModel, if it exists.
   * See TheoryModel::setIrrelevantKind for details.
   */
  void setIrrelevantKind(Kind k);
  //-------------------------------------- end static configuration of the model

  /**
   * Ensure that the given node will have a designated SAT literal
   * that is definitionally equal to it.  The result of this function
   * is a Node that can be queried via getSatValue().
   *
   * Note that this call may add lemmas to the SAT solver corresponding to the
   * definition of subterms eliminated by preprocessing.
   *
   * @return the actual node that's been "literalized," which may
   * differ from the input due to theory-rewriting and preprocessing,
   * as well as CNF conversion
   */
  Node ensureLiteral(TNode n) CVC5_WARN_UNUSED_RESULT;

  /**
   * This returns the theory-preprocessed form of term n. The theory
   * preprocessed form of a term t is one returned by
   * TheoryPreprocess::preprocess (see theory/theory_preprocess.h). In
   * particular, the returned term has syntax sugar symbols eliminated
   * (e.g. div, mod, partial datatype selectors), has term formulas (e.g. ITE
   * terms eliminated) and has been rewritten.
   *
   * Note that this call may add lemmas to the SAT solver corresponding to the
   * definition of subterms eliminated by preprocessing.
   *
   * @param n The node to preprocess
   * @return The preprocessed form of n
   */
  Node getPreprocessedTerm(TNode n);
  /**
   * Same as above, but also tracks the skolems and their corresponding
   * definitions in sks and skAsserts respectively.
   */
  Node getPreprocessedTerm(TNode n,
                           std::vector<Node>& skAsserts,
                           std::vector<Node>& sks);

  /**
   * Returns whether the given lit (which must be a SAT literal) is a decision
   * literal or not.  Throws an exception if lit is not a SAT literal.  "lit" may
   * be in either phase; that is, if "lit" is a SAT literal, this function returns
   * true both for lit and the negation of lit.
   */
  bool isDecision(Node lit) const;

  /**
   * Return the current decision level of `lit`.
   *
   * @param lit: The node in question, must have an associated SAT literal.
   * @return Decision level of the SAT variable of `lit` (phase is disregarded),
   *         or -1 if `lit` has not been assigned yet.
   */
  int32_t getDecisionLevel(Node lit) const;

  /**
   * Return the user-context level when `lit` was introduced..
   *
   * @return User-context level or -1 if not yet introduced.
   */
  int32_t getIntroLevel(Node lit) const;

  /**
   * Get the assertion level of the SAT solver.
   */
  unsigned getAssertionLevel() const;

  /**
   * Request an entailment check according to the given theoryOfMode.
   * See theory.h for documentation on entailmentCheck().
   */
  std::pair<bool, Node> entailmentCheck(options::TheoryOfMode mode, TNode lit);

  /** need check ? */
  bool needCheck() const;

  /**
   * Is the literal lit (possibly) critical for satisfying the input formula in
   * the current context? This call is applicable only during collectModelInfo
   * or during LAST_CALL effort.
   */
  bool isRelevant(Node lit) const;

  //------------------------------------------- access methods for assertions
  /**
   * The following methods are intended only to be used in limited use cases,
   * for cases where a theory (e.g. quantifiers) requires knowing about the
   * assertions from other theories.
   */
  /** The beginning iterator of facts for theory tid.*/
  context::CDList<Assertion>::const_iterator factsBegin(TheoryId tid);
  /** The beginning iterator of facts for theory tid.*/
  context::CDList<Assertion>::const_iterator factsEnd(TheoryId tid);
  /**
   * Is the cardinality of type tn finite? This method depends on whether
   * finite model finding is enabled. For details, see theory_engine.h.
   */
  bool isFiniteType(TypeNode tn) const;
};/* class Valuation */

}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY__VALUATION_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Morgan Deters, Dejan Jovanovic
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		* A "valuation" proxy for TheoryEngine
14		*
15		* A "valuation" proxy for TheoryEngine. This class breaks the dependence
16		* of theories' getValue() implementations on TheoryEngine. getValue()
17		* takes a Valuation, which delegates to TheoryEngine.
18		*/
19
20		#include "cvc5_private.h"
21
22		#ifndef CVC5__THEORY__VALUATION_H
23		#define CVC5__THEORY__VALUATION_H
24
25		#include "context/cdlist.h"
26		#include "expr/node.h"
27		#include "options/theory_options.h"
28
29		namespace cvc5 {
30
31		class TheoryEngine;
32
33		namespace theory {
34
35		struct Assertion;
36		class TheoryModel;
37		class SortInference;
38
39		/**
40		* The status of an equality in the current context.
41		*/
42		enum EqualityStatus {
43		/** The equality is known to be true and has been propagated */
44		EQUALITY_TRUE_AND_PROPAGATED,
45		/** The equality is known to be false and has been propagated */
46		EQUALITY_FALSE_AND_PROPAGATED,
47		/** The equality is known to be true */
48		EQUALITY_TRUE,
49		/** The equality is known to be false */
50		EQUALITY_FALSE,
51		/** The equality is not known, but is true in the current model */
52		EQUALITY_TRUE_IN_MODEL,
53		/** The equality is not known, but is false in the current model */
54		EQUALITY_FALSE_IN_MODEL,
55		/** The equality is completely unknown */
56		EQUALITY_UNKNOWN
57		};/* enum EqualityStatus */
58
59		std::ostream& operator<<(std::ostream& os, EqualityStatus s);
60
61		/**
62		* Returns true if the two statuses are compatible, i.e. both TRUE
63		* or both FALSE (regardless of inmodel/propagation).
64		*/
65		bool equalityStatusCompatible(EqualityStatus s1, EqualityStatus s2);
66
67		class Valuation {
68		TheoryEngine* d_engine;
69		public:
70	132493	Valuation(TheoryEngine* engine) :
71	132493	d_engine(engine) {
72	132493	}
73
74		/**
75		* Return true if n has an associated SAT literal
76		*/
77		bool isSatLiteral(TNode n) const;
78
79		/**
80		* Get the current SAT assignment to the node n.
81		*
82		* This is only permitted if n is a theory atom that has an associated
83		* SAT literal (or its negation).
84		*
85		* @return Node::null() if no current assignment; otherwise true or false.
86		*/
87		Node getSatValue(TNode n) const;
88
89		/**
90		* Returns true if the node has a current SAT assignment. If yes, the
91		* argument "value" is set to its value.
92		*
93		* This is only permitted if n is a theory atom that has an associated
94		* SAT literal.
95		*
96		* @return true if the literal has a current assignment, and returns the
97		* value in the "value" argument; otherwise false and the "value"
98		* argument is unmodified.
99		*/
100		bool hasSatValue(TNode n, bool& value) const;
101
102		/**
103		* Returns the equality status of the two terms, from the theory that owns the domain type.
104		* The types of a and b must be the same.
105		*/
106		EqualityStatus getEqualityStatus(TNode a, TNode b);
107
108		/**
109		* Returns the model value of the shared term (or null if not available).
110		*/
111		Node getModelValue(TNode var);
112
113		/**
114		* Returns pointer to model. This model is only valid during last call effort
115		* check.
116		*/
117		TheoryModel* getModel();
118		/**
119		* Returns a pointer to the sort inference module, which lives in TheoryEngine
120		* and is non-null when options::sortInference is true.
121		*/
122		SortInference* getSortInference();
123
124		//-------------------------------------- static configuration of the model
125		/**
126		* Set that k is an unevaluated kind in the TheoryModel, if it exists.
127		* See TheoryModel::setUnevaluatedKind for details.
128		*/
129		void setUnevaluatedKind(Kind k);
130		/**
131		* Set that k is an unevaluated kind in the TheoryModel, if it exists.
132		* See TheoryModel::setSemiEvaluatedKind for details.
133		*/
134		void setSemiEvaluatedKind(Kind k);
135		/**
136		* Set that k is an irrelevant kind in the TheoryModel, if it exists.
137		* See TheoryModel::setIrrelevantKind for details.
138		*/
139		void setIrrelevantKind(Kind k);
140		//-------------------------------------- end static configuration of the model
141
142		/**
143		* Ensure that the given node will have a designated SAT literal
144		* that is definitionally equal to it. The result of this function
145		* is a Node that can be queried via getSatValue().
146		*
147		* Note that this call may add lemmas to the SAT solver corresponding to the
148		* definition of subterms eliminated by preprocessing.
149		*
150		* @return the actual node that's been "literalized," which may
151		* differ from the input due to theory-rewriting and preprocessing,
152		* as well as CNF conversion
153		*/
154		Node ensureLiteral(TNode n) CVC5_WARN_UNUSED_RESULT;
155
156		/**
157		* This returns the theory-preprocessed form of term n. The theory
158		* preprocessed form of a term t is one returned by
159		* TheoryPreprocess::preprocess (see theory/theory_preprocess.h). In
160		* particular, the returned term has syntax sugar symbols eliminated
161		* (e.g. div, mod, partial datatype selectors), has term formulas (e.g. ITE
162		* terms eliminated) and has been rewritten.
163		*
164		* Note that this call may add lemmas to the SAT solver corresponding to the
165		* definition of subterms eliminated by preprocessing.
166		*
167		* @param n The node to preprocess
168		* @return The preprocessed form of n
169		*/
170		Node getPreprocessedTerm(TNode n);
171		/**
172		* Same as above, but also tracks the skolems and their corresponding
173		* definitions in sks and skAsserts respectively.
174		*/
175		Node getPreprocessedTerm(TNode n,
176		std::vector<Node>& skAsserts,
177		std::vector<Node>& sks);
178
179		/**
180		* Returns whether the given lit (which must be a SAT literal) is a decision
181		* literal or not. Throws an exception if lit is not a SAT literal. "lit" may
182		* be in either phase; that is, if "lit" is a SAT literal, this function returns
183		* true both for lit and the negation of lit.
184		*/
185		bool isDecision(Node lit) const;
186
187		/**
188		* Return the current decision level of `lit`.
189		*
190		* @param lit: The node in question, must have an associated SAT literal.
191		* @return Decision level of the SAT variable of `lit` (phase is disregarded),
192		* or -1 if `lit` has not been assigned yet.
193		*/
194		int32_t getDecisionLevel(Node lit) const;
195
196		/**
197		* Return the user-context level when `lit` was introduced..
198		*
199		* @return User-context level or -1 if not yet introduced.
200		*/
201		int32_t getIntroLevel(Node lit) const;
202
203		/**
204		* Get the assertion level of the SAT solver.
205		*/
206		unsigned getAssertionLevel() const;
207
208		/**
209		* Request an entailment check according to the given theoryOfMode.
210		* See theory.h for documentation on entailmentCheck().
211		*/
212		std::pair<bool, Node> entailmentCheck(options::TheoryOfMode mode, TNode lit);
213
214		/** need check ? */
215		bool needCheck() const;
216
217		/**
218		* Is the literal lit (possibly) critical for satisfying the input formula in
219		* the current context? This call is applicable only during collectModelInfo
220		* or during LAST_CALL effort.
221		*/
222		bool isRelevant(Node lit) const;
223
224		//------------------------------------------- access methods for assertions
225		/**
226		* The following methods are intended only to be used in limited use cases,
227		* for cases where a theory (e.g. quantifiers) requires knowing about the
228		* assertions from other theories.
229		*/
230		/** The beginning iterator of facts for theory tid.*/
231		context::CDList<Assertion>::const_iterator factsBegin(TheoryId tid);
232		/** The beginning iterator of facts for theory tid.*/
233		context::CDList<Assertion>::const_iterator factsEnd(TheoryId tid);
234		/**
235		* Is the cardinality of type tn finite? This method depends on whether
236		* finite model finding is enabled. For details, see theory_engine.h.
237		*/
238		bool isFiniteType(TypeNode tn) const;
239		};/* class Valuation */
240
241		} // namespace theory
242		} // namespace cvc5
243
244		#endif /* CVC5__THEORY__VALUATION_H */