FStar
FStar copied to clipboard
FStarLang
Encode String literals in SMT
Based on #1380 by @A-Manning
I added a switch to enable encoding (smtencoding.encode_string), and the example in #1380 is able to typecheck.
Hi @fangyi-zhou, Thanks for this contribution! @aseemr and I were discussing it this morning.
This looks like a great basis for comprehensive encoding of FStar.String to Z3's string theory.
Would you be interested to enhance this PR by providing interpretations for more of the functions in FStar.String. It should follow the same pattern as you have established already in the code.
In particular, Z3's string theory supports many more functions than just strlen and strcat. See here, for an interactive example: https://www.philipzucker.com/z3-rise4fun/sequences.html
It would be great to map the functions in FStar.String to the operations listed here:
(str.++ a b c) | String concatenation of one or more strings
(str.len s) | String length. Returns an integer.
(str.substr s offset length) | Retrieves substring of s at offset
(str.indexof s sub) | Retrieves first position of sub in s, -1 if there are no occurrences
(str.indexof s sub offset) | Retrieves first position of sub at or after offset in s, -1 if there are no occurrences
(str.at s offset) | Substring of length 1 at offset in s.
(str.contains s sub) | Does s contain the substring sub?
(str.prefixof pre s) | Is pre a prefix of s?
(str.suffixof suf s) | Is suf a suffix of s?
(str.replace s src dst) | Replace the first occurrence of src by dst in s.
(str.to.int s) | Retrieve integer encoded by string s (ground rewriting only).
(int.to.str i) | Retrieve string encoding of integer i (ground rewriting only).
A few of the FStar.String functions do not have natural analogs: e.g., lowercase and uppercase. For these we can write F* axioms to interpret them in terms of the other operations.
Thanks for the comments @nikswamy, I'm happy to add the proposed extensions, I'll try to finish them within upcoming weeks :)