1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
|
/******************************************************************************
* 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 "cvc4_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 */
|
