diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-07 07:18:08 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-07 12:18:08 +0000 |
| commit | 22ab38c4a3bad18129c740968b36af8c378c4294 (patch) | |
| tree | 250b6a9c2417df52984327b301c0a3aa8ffa15a1 /src/theory/evaluator.h | |
| parent | 991bef531131336549eccd2446243204f4733c20 (diff) | |
Make the cardinality of the alphabet of strings configurable (#7298)
This adds an option to change the cardinality of the alphabet of strings. The alphabet of strings is always a prefix of the interval of unicode code points in the string standard.
Diffstat (limited to 'src/theory/evaluator.h')
| -rw-r--r-- | src/theory/evaluator.h | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h index 2e96952b8..e13dcfbca 100644 --- a/src/theory/evaluator.h +++ b/src/theory/evaluator.h @@ -90,7 +90,11 @@ class Rewriter; class Evaluator { public: - Evaluator(Rewriter* rr); + /** + * @param rr (optional) the rewriter to use when a node cannot be evaluated. + * @param strAlphaCard The assumed cardinality of the alphabet for strings. + */ + Evaluator(Rewriter* rr, uint32_t strAlphaCard = 196608); /** * Evaluates node `n` under the substitution described by the variable names * `args` and the corresponding values `vals`. This method uses evaluation |