summaryrefslogtreecommitdiff
path: root/test/regress/regress2/pp-regfile.smt.expect
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2020-08-04 20:32:28 -0700
committerAndres Noetzli <andres.noetzli@gmail.com>2020-08-04 20:46:08 -0700
commit8bc706b090b030f43d1df795984b376c68b03616 (patch)
tree4d35b8d4901671e1245fbb9424f4ef84bfcddc74 /test/regress/regress2/pp-regfile.smt.expect
parent98e426dae609dcc94b0c5bde9d804332493e9175 (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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback