diff options
Diffstat (limited to 'src/theory/strings/arith_entail.h')
| -rw-r--r-- | src/theory/strings/arith_entail.h | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/theory/strings/arith_entail.h b/src/theory/strings/arith_entail.h index 2158b23b0..6529a81d1 100644 --- a/src/theory/strings/arith_entail.h +++ b/src/theory/strings/arith_entail.h @@ -96,6 +96,10 @@ class ArithEntail * checkWithAssumption(x + (str.len y) = 0, 0, x, false) = true * * Because: x = -(str.len y), so 0 >= x --> 0 >= -(str.len y) --> true + * + * Since this method rewrites on rewriting and may introduce new variables + * (slack variables for inequalities), it should *not* be called from the + * main rewriter of strings, or non-termination can occur. */ bool checkWithAssumption(Node assumption, Node a, @@ -114,6 +118,10 @@ class ArithEntail * checkWithAssumptions([x + (str.len y) = 0], 0, x, false) = true * * Because: x = -(str.len y), so 0 >= x --> 0 >= -(str.len y) --> true + * + * Since this method rewrites on rewriting and may introduce new variables + * (slack variables for inequalities), it should *not* be called from the + * main rewriter of strings, or non-termination can occur. */ bool checkWithAssumptions(std::vector<Node> assumptions, Node a, @@ -136,6 +144,10 @@ class ArithEntail Node getConstantBound(Node a, bool isLower = true); /** + * get constant bound on the length of s. + */ + Node getConstantBoundLength(Node s, 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 @@ -179,8 +191,14 @@ class ArithEntail void getArithApproximations(Node a, std::vector<Node>& approx, bool isOverApprox = false); + /** Set bound cache */ + void setConstantBoundCache(Node n, Node ret, bool isLower); + /** Get bound cache */ + Node getConstantBoundCache(Node n, bool isLower); /** The underlying rewriter */ Rewriter* d_rr; + /** Constant zero */ + Node d_zero; }; } // namespace strings |