(proof-new) Add the strings proof checker (#4858)

It also adds enumeration for two new rules that have been recently added.

1 files changed, 16 insertions, 0 deletions

diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 364598cf4..a83e043bf 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -766,6 +766,22 @@ enum class PfRule : uint32_t
   //                (not (= (str.code t) (str.code s)))
   //                (not (= t s)))
   STRING_CODE_INJ,
+  //======================== Sequence unit
+  // Children: (P:(= (seq.unit x) (seq.unit y)))
+  // Arguments: none
+  // ---------------------
+  // Conclusion:(= x y)
+  // Also applies to the case where (seq.unit y) is a constant sequence
+  // of length one.
+  STRING_SEQ_UNIT_INJ,
+  // ======== String Trust
+  // Children: none
+  // Arguments: (Q)
+  // ---------------------
+  // Conclusion: (Q)
+  STRING_TRUST,
+
+  //================================================= Arithmetic rules
   // ======== Adding Inequalities
   // Note: an ArithLiteral is a term of the form (>< poly const)
   // where