<commit_before>Smtlink
====================

*Smtlink* is a framework for integrating external *SMT* solvers into *ACL2* based on
*clause processors* and *computed hints*.

It supports both ACL2 and *ACL2(r)*. The current default SMT solver integrated is
*Z3*. *SMT-LIB* is expected to be integrated in near future.

### Requirements

* Python 2 is properly installed
* Z3 is properly installed
One can check it by running below program:
```
  from z3 import *
  x = Real('x')
  y = Real('y')
  s = Solver()
  s.add(x + y > 5, x > 1, y > 1)
  print(s.check())
  print(s.model())
```
One should expect some results like:
```
>>> print(s.check())
sat
>>> print(s.model())
[y = 4, x = 2]
```

* ACL2 and its book directory is properly installed
* Smtlink uses Unix commands

### Build Smtlink

* Setup Smtlink configuration in file *smtlink-config* in directory $HOME. The
  configuration takes below format
  ```
  interface-dir=...
  smt-module=...
  smt-class=...
  smt-cmd=...
  pythonpath=...
  ```
  
*  Below table explains what they stands for:
  
  Option        | Explanation                                         | Example
  ------------- | --------------------------------------------------- | -------------
  interface-dir | The directory to SMT solver interface module files  | /Users/.../smtlink/z3_interface
  smt-module    | The module name (i.e. the file name)                | ACL2_to_Z3
  smt-class     | The class name                                      | ACL22SMT<commit_msg>Updated to remove spaces, because it's Python!!!!!!!!!!!!!<commit_after>Smtlink
====================

*Smtlink* is a framework for integrating external *SMT* solvers into *ACL2* based on
*clause processors* and *computed hints*.

It supports both ACL2 and *ACL2(r)*. The current default SMT solver integrated is
*Z3*. *SMT-LIB* is expected to be integrated in near future.

### Requirements

* Python 2 is properly installed
* Z3 is properly installed
One can check it by running below program:
```
from z3 import *
x = Real('x')
y = Real('y')
s = Solver()
s.add(x + y > 5, x > 1, y > 1)
print(s.check())
print(s.model())
```
One should expect some results like:
```
>>> print(s.check())
sat
>>> print(s.model())
[y = 4, x = 2]
```

* ACL2 and its book directory is properly installed
* Smtlink uses Unix commands

### Build Smtlink

* Setup Smtlink configuration in file *smtlink-config* in directory $HOME. The
  configuration takes below format
  ```
  interface-dir=...
  smt-module=...
  smt-class=...
  smt-cmd=...
  pythonpath=...
  ```
  
*  Below table explains what they stands for:
  
  Option        | Explanation                                         | Example
  ------------- | --------------------------------------------------- | -------------
  interface-dir | The directory to SMT solver interface module files  | /Users/.../smtlink/z3_interface
  smt-module    | The module name (i.e. the file name)                | ACL2_to_Z3
  smt-class     | The class name                                      | ACL22SMT
{'fraction_non_alphanumeric': 0.17872481004294682, 'fraction_numerical': 0.011892963330029732, 'mean_word_length': 2.19072708113804, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 21, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 8, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3447892', 'n_tokens_mistral': 945, 'n_tokens_neox': 890, 'n_words': 321}