(proof-new) Updates to strings core solver (#4642)

This updates the core strings solver in preparation for proofs.

The main changes include:

The addition of the strings PfRule enum values.
The definition of a "getConclusion" static method, used by the core solver, and to be used in the future by the strings proof checker. This includes several optional forms of lemmas, which are added as options in this PR.
Major simplifications to our inference schemas for disequality handling (a STRING_DECOMPOSE inference rule). Note this is the only significant intended behavioral change in this PR.
Minor updates to the form of inferences send to inference manager, for instance to orient equalities in the expected way, and to reorder assumptions. These changes are done for uniformity and make the strings proof reconstruction from inference steps easier.

1 files changed, 17 insertions, 0 deletions

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 32c4c64c7..e69fa3317 100644
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -205,3 +205,20 @@ header = "options/strings_options.h"
 [[option.mode.NONE]]
   name = "none"
   help = "Do not compute intersections for regular expressions."
+
+[[option]]
+  name       = "stringUnifiedVSpt"
+  category   = "regular"
+  long       = "strings-unified-vspt"
+  type       = "bool"
+  default    = "true"
+  read_only  = true
+  help       = "use a single skolem for the variable splitting rule"
+
+[[option]]
+  name       = "stringLenConc"
+  category   = "regular"
+  long       = "strings-len-conc"
+  type       = "bool"
+  default    = "false"
+  help       = "add skolem length constraints in conclusions of inferences"