Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/term_context.h	Lines:	8	8	100.0 %
Date:	2021-05-22	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"

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);
};

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