[Strings] Add eager context-dependent evaluation (#4847)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 5 Aug 2020 14:18:10 +0000 (07:18 -0700)
committerGitHub <noreply@github.com>
Wed, 5 Aug 2020 14:18:10 +0000 (09:18 -0500)
commitce2fa6ad8858c70aebf253b910bea3726065e85d
tree308bf14063223c947a2a4e6ce8976d72d6e01383
parentc324bb21adb44374eb37a0254e31c0a0d0b3ebc7
[Strings] Add eager context-dependent evaluation (#4847)

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.
src/options/strings_options.toml
src/theory/strings/term_registry.cpp
src/theory/strings/term_registry.h
src/theory/strings/theory_strings.cpp