search

ufmg-smite / lean-smt

Tactics for discharging Lean goals into SMT solvers.
Apache License 2.0
89 stars 18 forks source link

Add initial support for strings. #8

Closed abdoo8080 closed 2 years ago

abdoo8080 commented 2 years ago

This PR adds initial support for strings functions. We face 3 problems when we generate queries for string theorems:

  1. String theory in SMT-LIB does not support a character type. Those are converted into codepoints using str.to_code instead.
  2. Not all string functions in Lean have an obvious corresponding function in SMT-LIB, and vice versa. For those, we need to be careful not introduce any soundness bug in the translation.
  3. Many string functions in Lean are partial, so we cannot prove theorems that make use of them in Lean anyways.