<commit_before>﻿Z3Fs
===
### A simple DSL to solve SMT problems using Z3 API in F# ###

---
Details will be added later.

===
### TODO ###

- Check correctness of examples carefully.
- Examine difficult modules including uninterpreted functions and bit-vectors.
- Rearrange modules; many functions are in wrong places.
- Rewrite ToString() for pretty-printing.
- Standardize the use of %A and %O.<commit_msg>Add several rudimentary sections<commit_after>﻿Z3Fs
===
### A simple DSL to solve SMT problems using Z3 API in F# ###

---
### Purpose ###
`Z3Fs` aims at providing a simple API to express and solve SMT problems in F#.
Z3 has an official .NET API written in C# at [Codeplex](http://z3.codeplex.com/SourceControl/changeset/view/89c1785b7322#src/api/dotnet/Context.cs), but it is too verbose and not F#-friendly.
Hopefully, `Z3Fs` could give a look of a small EDSL for SMT solving in F#.

---
### Setup / Installation ###

---
### Implementation notes ###

---
### TODO ###

- Check correctness of examples carefully.
- Examine difficult modules including uninterpreted functions and bit-vectors.
- Rearrange modules; many functions are in wrong places.
- Rewrite ToString() for pretty-printing.
- Standardize the use of %A and %O.
{'fraction_non_alphanumeric': 0.11731391585760517, 'fraction_numerical': 0.014563106796116505, 'mean_word_length': 3.9087301587301586, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2667443', 'n_tokens_mistral': 386, 'n_tokens_neox': 372, 'n_words': 153}