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) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel 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 bitvector 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 termcontextsensitive 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 termcontextsensitive Node is not onetoone 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 */ 