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/strings/proof_checker.cpp | |
| 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/strings/proof_checker.cpp')
| -rw-r--r-- | src/theory/strings/proof_checker.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp index 3f5edbb8e..b9038e3c8 100644 --- a/src/theory/strings/proof_checker.cpp +++ b/src/theory/strings/proof_checker.cpp @@ -325,7 +325,7 @@ Node StringProofRuleChecker::checkInternal(PfRule id, { Assert(args.size() == 1); SkolemCache skc(nullptr); - ret = TermRegistry::eagerReduce(t, &skc); + ret = TermRegistry::eagerReduce(t, &skc, d_alphaCard); } else if (id == PfRule::STRING_LENGTH_POS) { |