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
170
171
172
173
174
175
176
177
178
179
180
181
|
/******************************************************************************
* Top contributors (to current version):
* Andrew Reynolds, Andres Noetzli
*
* 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.
* ****************************************************************************
*
* Arithmetic entailment computation for string terms.
*/
#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__ARITH_ENTAIL_H
#define CVC5__THEORY__STRINGS__ARITH_ENTAIL_H
#include <vector>
#include "expr/node.h"
namespace cvc5 {
namespace theory {
namespace strings {
/**
* Techniques for computing arithmetic entailment for string terms. This
* is an implementation of the techniques from Reynolds et al, "High Level
* Abstractions for Simplifying Extended String Constraints in SMT", CAV 2019.
*/
class ArithEntail
{
public:
/** check arithmetic entailment equal
* Returns true if it is always the case that a = b.
*/
static bool checkEq(Node a, Node b);
/** check arithmetic entailment
* Returns true if it is always the case that a >= b,
* and a>b if strict is true.
*/
static bool check(Node a, Node b, bool strict = false);
/** check arithmetic entailment
* Returns true if it is always the case that a >= 0.
*/
static bool check(Node a, bool strict = false);
/** check arithmetic entailment with approximations
*
* Returns true if it is always the case that a >= 0. We expect that a is in
* rewritten form.
*
* This function uses "approximation" techniques that under-approximate
* the value of a for the purposes of showing the entailment holds. For
* example, given:
* len( x ) - len( substr( y, 0, len( x ) ) )
* Since we know that len( substr( y, 0, len( x ) ) ) <= len( x ), the above
* term can be under-approximated as len( x ) - len( x ) = 0, which is >= 0,
* and thus the entailment len( x ) - len( substr( y, 0, len( x ) ) ) >= 0
* holds.
*/
static bool checkApprox(Node a);
/**
* Checks whether assumption |= a >= 0 (if strict is false) or
* assumption |= a > 0 (if strict is true), where assumption is an equality
* assumption. The assumption must be in rewritten form.
*
* Example:
*
* checkWithEqAssumption(x + (str.len y) = 0, -x, false) = true
*
* Because: x = -(str.len y), so -x >= 0 --> (str.len y) >= 0 --> true
*/
static bool checkWithEqAssumption(Node assumption,
Node a,
bool strict = false);
/**
* Checks whether assumption |= a >= b (if strict is false) or
* assumption |= a > b (if strict is true). The function returns true if it
* can be shown that the entailment holds and false otherwise. Assumption
* must be in rewritten form. Assumption may be an equality or an inequality.
*
* Example:
*
* checkWithAssumption(x + (str.len y) = 0, 0, x, false) = true
*
* Because: x = -(str.len y), so 0 >= x --> 0 >= -(str.len y) --> true
*/
static bool checkWithAssumption(Node assumption,
Node a,
Node b,
bool strict = false);
/**
* Checks whether assumptions |= a >= b (if strict is false) or
* assumptions |= a > b (if strict is true). The function returns true if it
* can be shown that the entailment holds and false otherwise. Assumptions
* must be in rewritten form. Assumptions may be an equalities or an
* inequalities.
*
* Example:
*
* checkWithAssumptions([x + (str.len y) = 0], 0, x, false) = true
*
* Because: x = -(str.len y), so 0 >= x --> 0 >= -(str.len y) --> true
*/
static bool checkWithAssumptions(std::vector<Node> assumptions,
Node a,
Node b,
bool strict = false);
/** get arithmetic lower bound
* If this function returns a non-null Node ret,
* then ret is a rational constant and
* we know that n >= ret always if isLower is true,
* or n <= ret if isLower is false.
*
* Notice the following invariant.
* If getConstantArithBound(a, true) = ret where ret is non-null, then for
* strict = { true, false } :
* ret >= strict ? 1 : 0
* if and only if
* check( a, strict ) = true.
*/
static Node getConstantBound(Node a, bool isLower = true);
/**
* Given an inequality y1 + ... + yn >= x, removes operands yi s.t. the
* original inequality still holds. Returns true if the original inequality
* holds and false otherwise. The list of ys is modified to contain a subset
* of the original ys.
*
* Example:
*
* inferZerosInSumGeq( (str.len x), [ (str.len x), (str.len y), 1 ], [] )
* --> returns true with ys = [ (str.len x) ] and zeroYs = [ (str.len y), 1 ]
* (can be used to rewrite the inequality to false)
*
* inferZerosInSumGeq( (str.len x), [ (str.len y) ], [] )
* --> returns false because it is not possible to show
* str.len(y) >= str.len(x)
*/
static bool inferZerosInSumGeq(Node x,
std::vector<Node>& ys,
std::vector<Node>& zeroYs);
private:
/** check entail arithmetic internal
* Returns true if we can show a >= 0 always.
* a is in rewritten form.
*/
static bool checkInternal(Node a);
/** Get arithmetic approximations
*
* This gets the (set of) arithmetic approximations for term a and stores
* them in approx. If isOverApprox is true, these are over-approximations
* for the value of a, otherwise, they are underapproximations. For example,
* an over-approximation for len( substr( y, n, m ) ) is m; an
* under-approximation for indexof( x, y, n ) is -1.
*
* Notice that this function is not generally recursive (although it may make
* a small bounded of recursive calls). Instead, it returns the shape
* of the approximations for a. For example, an under-approximation
* for the term len( replace( substr( x, 0, n ), y, z ) ) returned by this
* function might be len( substr( x, 0, n ) ) - len( y ), where we don't
* consider (recursively) the approximations for len( substr( x, 0, n ) ).
*/
static void getArithApproximations(Node a,
std::vector<Node>& approx,
bool isOverApprox = false);
};
} // namespace strings
} // namespace theory
} // namespace cvc5
#endif
|
