Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/term_context.h	Lines:	10	10	100.0 %
Date:	2021-08-01	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.
 * ****************************************************************************
 *
 * Term context utilities.
 */

#include "cvc5_private.h"

#ifndef CVC5__EXPR__TERM_CONTEXT_H
#define CVC5__EXPR__TERM_CONTEXT_H

#include "expr/node.h"
#include "theory/theory_id.h"

namespace cvc5 {

/**
 * This is an abstract class for computing "term context identifiers". A term
 * context identifier is a hash value that identifies some property of the
 * context in which a term occurs. Common examples of the implementation of
 * such a mapping are implemented in the subclasses below.
 *
 * A term context identifier is intended to be information that can be locally
 * computed from the parent's hash, and hence does not rely on maintaining
 * paths.
 *
 * In the below documentation, we write t @ [p] to a term at a given position,
 * where p is a list of indices. For example, the atomic subterms of:
 *   (and P (not Q))
 * are P @ [0] and Q @ [1,0].
 */
class TermContext
{
 public:
  TermContext() {}
  virtual ~TermContext() {}
  /** The default initial value of root terms. */
  virtual uint32_t initialValue() const = 0;
  /**
   * Returns the term context identifier of the index^th child of t, where tval
   * is the term context identifier of t.
   */
  virtual uint32_t computeValue(TNode t, uint32_t tval, size_t index) const = 0;
  /**
   * Returns the term context identifier of the operator of t, where tval
   * is the term context identifier of t.
   */
  virtual uint32_t computeValueOp(TNode t, uint32_t tval) const;
};

/**
 * Remove term formulas (rtf) term context.
 *
 * Computes whether we are inside a term (as opposed to being part of Boolean
 * skeleton) and whether we are inside a quantifier. For example, for:
 *   (and (= a b) (forall ((x Int)) (P x)))
 * we have the following mappings (term -> inTerm,inQuant)
 *   (= a b) @ [0] -> false, false
 *   a @ [0,1] -> true, false
 *   (P x) @ [1,1] -> false, true
 *    x @ [1,1,0] -> true, true
 * Notice that the hash of a child can be computed from the parent's hash only,
 * and hence this can be implemented as an instance of the abstract class.
 */
class RtfTermContext : public TermContext
{
 public:
  RtfTermContext() {}
  /** The initial value: not in a term context or beneath a quantifier. */
  uint32_t initialValue() const override;
  /** Compute the value of the index^th child of t whose hash is tval */
  uint32_t computeValue(TNode t, uint32_t tval, size_t index) const override;
  /** get hash value from the flags */
  static uint32_t getValue(bool inQuant, bool inTerm);
  /** get flags from the hash value */
  static void getFlags(uint32_t val, bool& inQuant, bool& inTerm);

 private:
  /**
   * Returns true if the children of t should be considered in a "term" context,
   * which is any context beneath a symbol that does not belong to the Boolean
   * theory as well as other exceptions like equality, separation logic
   * connectives and bit-vector eager atoms.
   */
  static bool hasNestedTermChildren(TNode t);
};

/**
 * Simpler version of above that only computes whether we are inside a
 * quantifier.
 */
class InQuantTermContext : public TermContext
{
 public:
  InQuantTermContext() {}
  /** The initial value: not beneath a quantifier. */
  uint32_t initialValue() const override;
  /** Compute the value of the index^th child of t whose hash is tval */
  uint32_t computeValue(TNode t, uint32_t tval, size_t index) const override;
  /** get hash value from the flags */
  static uint32_t getValue(bool inQuant);
  /** get flags from the hash value */
  static bool inQuant(uint32_t val, bool& inQuant);
};

/**
 * Polarity term context.
 *
 * This class computes the polarity of a term-context-sensitive term, which is
 * one of {true, false, none}. This corresponds to the value that can be
 * assigned to that term while preservering satisfiability of the overall
 * formula, or none if such a value does not exist. If not "none", this
 * typically corresponds to whether the number of NOT the formula is beneath is
 * even, although special cases exist (e.g. the first child of IMPLIES).
 *
 * For example, given the formula:
 *   (and P (not (= (f x) 0)))
 * assuming the root of this formula has true polarity, we have that:
 *   P @ [0] -> true
 *   (not (= (f x) 0)) @ [1] -> true
 *   (= (f x) 0) @ [1,0] -> false
 *   (f x) @ [1,0,0]), x @ [1,0,0,0]), 0 @ [1,0,1] -> none
 *
 * Notice that a term-context-sensitive Node is not one-to-one with Node.
 * In particular, given the formula:
 *   (and P (not P))
 * We have that the P at path [0] has polarity true and the P at path [1,0] has
 * polarity false.
 *
 * Finally, notice that polarity does not correspond to a value that the
 * formula entails. Thus, for the formula:
 *   (or P Q)
 * we have that
 *   P @ [0] -> true
 *   Q @ [1] -> true
 * although neither is entailed.
 *
 * Notice that the hash of a child can be computed from the parent's hash only.
 */
class PolarityTermContext : public TermContext
{
 public:
  PolarityTermContext() {}
  /** The initial value: true polarity. */
  uint32_t initialValue() const override;
  /** Compute the value of the index^th child of t whose hash is tval */
  uint32_t computeValue(TNode t, uint32_t tval, size_t index) const override;
  /**
   * Get hash value from the flags, where hasPol false means no polarity.
   */
  static uint32_t getValue(bool hasPol, bool pol);
  /**
   * get flags from the hash value. If we have no polarity, both hasPol and pol
   * are set to false.
   */
  static void getFlags(uint32_t val, bool& hasPol, bool& pol);
};

/**
 * Similar to InQuantTermContext, but computes whether we are below a theory
 * leaf of given theory id.
 */
class TheoryLeafTermContext : public TermContext
{
 public:
  TheoryLeafTermContext(theory::TheoryId id) : d_theoryId(id) {}
  /** The initial value: not beneath a theory leaf. */
  uint32_t initialValue() const override;
  /** Compute the value of the index^th child of t whose hash is tval */
  uint32_t computeValue(TNode t, uint32_t tval, size_t index) const override;

 private:
  theory::TheoryId d_theoryId;
};

}  // namespace cvc5

#endif /* CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_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		* Term context utilities.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__EXPR__TERM_CONTEXT_H
19		#define CVC5__EXPR__TERM_CONTEXT_H
20
21		#include "expr/node.h"
22		#include "theory/theory_id.h"
23
24		namespace cvc5 {
25
26		/**
27		* This is an abstract class for computing "term context identifiers". A term
28		* context identifier is a hash value that identifies some property of the
29		* context in which a term occurs. Common examples of the implementation of
30		* such a mapping are implemented in the subclasses below.
31		*
32		* A term context identifier is intended to be information that can be locally
33		* computed from the parent's hash, and hence does not rely on maintaining
34		* paths.
35		*
36		* In the below documentation, we write t @ [p] to a term at a given position,
37		* where p is a list of indices. For example, the atomic subterms of:
38		* (and P (not Q))
39		* are P @ [0] and Q @ [1,0].
40		*/
41		class TermContext
42		{
43		public:
44	26354	TermContext() {}
45	26354	virtual ~TermContext() {}
46		/** The default initial value of root terms. */
47		virtual uint32_t initialValue() const = 0;
48		/**
49		* Returns the term context identifier of the index^th child of t, where tval
50		* is the term context identifier of t.
51		*/
52		virtual uint32_t computeValue(TNode t, uint32_t tval, size_t index) const = 0;
53		/**
54		* Returns the term context identifier of the operator of t, where tval
55		* is the term context identifier of t.
56		*/
57		virtual uint32_t computeValueOp(TNode t, uint32_t tval) const;
58		};
59
60		/**
61		* Remove term formulas (rtf) term context.
62		*
63		* Computes whether we are inside a term (as opposed to being part of Boolean
64		* skeleton) and whether we are inside a quantifier. For example, for:
65		* (and (= a b) (forall ((x Int)) (P x)))
66		* we have the following mappings (term -> inTerm,inQuant)
67		* (= a b) @ [0] -> false, false
68		* a @ [0,1] -> true, false
69		* (P x) @ [1,1] -> false, true
70		* x @ [1,1,0] -> true, true
71		* Notice that the hash of a child can be computed from the parent's hash only,
72		* and hence this can be implemented as an instance of the abstract class.
73		*/
74	9905	class RtfTermContext : public TermContext
75		{
76		public:
77	9905	RtfTermContext() {}
78		/** The initial value: not in a term context or beneath a quantifier. */
79		uint32_t initialValue() const override;
80		/** Compute the value of the index^th child of t whose hash is tval */
81		uint32_t computeValue(TNode t, uint32_t tval, size_t index) const override;
82		/** get hash value from the flags */
83		static uint32_t getValue(bool inQuant, bool inTerm);
84		/** get flags from the hash value */
85		static void getFlags(uint32_t val, bool& inQuant, bool& inTerm);
86
87		private:
88		/**
89		* Returns true if the children of t should be considered in a "term" context,
90		* which is any context beneath a symbol that does not belong to the Boolean
91		* theory as well as other exceptions like equality, separation logic
92		* connectives and bit-vector eager atoms.
93		*/
94		static bool hasNestedTermChildren(TNode t);
95		};
96
97		/**
98		* Simpler version of above that only computes whether we are inside a
99		* quantifier.
100		*/
101	9905	class InQuantTermContext : public TermContext
102		{
103		public:
104	9905	InQuantTermContext() {}
105		/** The initial value: not beneath a quantifier. */
106		uint32_t initialValue() const override;
107		/** Compute the value of the index^th child of t whose hash is tval */
108		uint32_t computeValue(TNode t, uint32_t tval, size_t index) const override;
109		/** get hash value from the flags */
110		static uint32_t getValue(bool inQuant);
111		/** get flags from the hash value */
112		static bool inQuant(uint32_t val, bool& inQuant);
113		};
114
115		/**
116		* Polarity term context.
117		*
118		* This class computes the polarity of a term-context-sensitive term, which is
119		* one of {true, false, none}. This corresponds to the value that can be
120		* assigned to that term while preservering satisfiability of the overall
121		* formula, or none if such a value does not exist. If not "none", this
122		* typically corresponds to whether the number of NOT the formula is beneath is
123		* even, although special cases exist (e.g. the first child of IMPLIES).
124		*
125		* For example, given the formula:
126		* (and P (not (= (f x) 0)))
127		* assuming the root of this formula has true polarity, we have that:
128		* P @ [0] -> true
129		* (not (= (f x) 0)) @ [1] -> true
130		* (= (f x) 0) @ [1,0] -> false
131		* (f x) @ [1,0,0]), x @ [1,0,0,0]), 0 @ [1,0,1] -> none
132		*
133		* Notice that a term-context-sensitive Node is not one-to-one with Node.
134		* In particular, given the formula:
135		* (and P (not P))
136		* We have that the P at path [0] has polarity true and the P at path [1,0] has
137		* polarity false.
138		*
139		* Finally, notice that polarity does not correspond to a value that the
140		* formula entails. Thus, for the formula:
141		* (or P Q)
142		* we have that
143		* P @ [0] -> true
144		* Q @ [1] -> true
145		* although neither is entailed.
146		*
147		* Notice that the hash of a child can be computed from the parent's hash only.
148		*/
149	1074	class PolarityTermContext : public TermContext
150		{
151		public:
152	1074	PolarityTermContext() {}
153		/** The initial value: true polarity. */
154		uint32_t initialValue() const override;
155		/** Compute the value of the index^th child of t whose hash is tval */
156		uint32_t computeValue(TNode t, uint32_t tval, size_t index) const override;
157		/**
158		* Get hash value from the flags, where hasPol false means no polarity.
159		*/
160		static uint32_t getValue(bool hasPol, bool pol);
161		/**
162		* get flags from the hash value. If we have no polarity, both hasPol and pol
163		* are set to false.
164		*/
165		static void getFlags(uint32_t val, bool& hasPol, bool& pol);
166		};
167
168		/**
169		* Similar to InQuantTermContext, but computes whether we are below a theory
170		* leaf of given theory id.
171		*/
172	10940	class TheoryLeafTermContext : public TermContext
173		{
174		public:
175	5470	TheoryLeafTermContext(theory::TheoryId id) : d_theoryId(id) {}
176		/** The initial value: not beneath a theory leaf. */
177		uint32_t initialValue() const override;
178		/** Compute the value of the index^th child of t whose hash is tval */
179		uint32_t computeValue(TNode t, uint32_t tval, size_t index) const override;
180
181		private:
182		theory::TheoryId d_theoryId;
183		};
184
185		} // namespace cvc5
186
187		#endif /* CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */