diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-08-04 20:32:28 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-08-04 20:46:08 -0700 |
commit | 8bc706b090b030f43d1df795984b376c68b03616 (patch) | |
tree | 4d35b8d4901671e1245fbb9424f4ef84bfcddc74 /test/regress/regress2/pp-regfile.smt.expect | |
parent | 98e426dae609dcc94b0c5bde9d804332493e9175 (diff) |
[Strings] Add eager context-based evaluation
This commit adds eager evaluation of string terms based on the current
context. To do so, it declares the string kinds to be "interpreted" in
the equality engine. This allows us to avoid making a series of
decisions such as:
```
** (= "describe" (str.substr actionName 0 8)) :DE-DECISION:
*** (= actionName "deletecertificate") :DE-DECISION:
**** (= resource_partition "aws") :DE-DECISION:
***** (= resource_region "af-south-1") :DE-DECISION:
****** (= resource_account "") :DE-DECISION:
******* (= (str.len (str.substr actionName 0 3)) 0) :DE-DECISION:
******** (= (str.len (str.substr actionName 0 4)) 0) :DE-DECISION:
********* (= (str.len (str.substr actionName 0 6)) 0) :DE-DECISION:
********** (= (str.len (str.substr actionName 0 5)) 0) :DE-DECISION:
*********** (= (str.len (str.substr actionName 0 9)) 0) :DE-DECISION:
************ (= (str.len (str.substr actionName 0 7)) 0) :DE-DECISION:
************* (= (str.len (str.substr actionName 0 10)) 0) :DE-DECISION:
************** (= (str.len (str.substr actionName 0 2)) 0) :DE-DECISION:
*************** (= (str.len (str.substr actionName 0 13)) 0) :DE-DECISION:
**************** (= (str.len (str.substr actionName 0 12)) 0) :DE-DECISION:
***************** (= (str.len resource_service) 0) :DE-DECISION:
****************** (= (str.len resource_account) 0) :DE-DECISION:
```
In such a case, we can detect that there is a conflict after the first
two decisions because `(str.substr "deletecertificate" 0 8)` is
`deletece` which is different from `describe`. The equality engine uses
the rewriter to evaluate interpreted kinds with constant arguments.
This technique leads to a significant speedup on some of the newer
Amazon benchmarks.
Diffstat (limited to 'test/regress/regress2/pp-regfile.smt.expect')
0 files changed, 0 insertions, 0 deletions