GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/term_context.h Lines: 6 7 85.7 %
Date: 2021-03-22 Branches: 0 0 0.0 %

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