Repository: testsmt/yinyang (language: python)

Issue:
Pypi packaging



Discussion / hints:

Fix patch:
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 2f6c06d..dda843d 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -16,9 +16,13 @@ jobs:
         python-version: ${{ matrix.python-version }}
     - name: Install dependencies
       run: |
+        pip install codespell
         python -m pip install flake8
         python -m pip install --upgrade pip 
         python -m pip install antlr4-python3-runtime==4.9.2  
+    - name: Spell check 
+      run: |
+        codespell --skip="Solver.py,SMTLIBv2*,*.g4,*.tokens,*.interp,*.smt2"
     - name: Run Unittests
       run: |
         python -m unittest tests/RunUnitTests.py
@@ -45,3 +49,6 @@ jobs:
     - name: code style and static analysis with flake 
       run: |
         bin/checkstyle.sh
+    - name: pypi check  
+      run: |
+        tests/integration/misc/pypi.sh
diff --git a/.gitignore b/.gitignore
index e0e8c99..c601f9c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,6 @@
 __pycache__
 .DS_Store
+build
+dist
+logs
+yinyang.egg-info
\ No newline at end of file
diff --git a/MANIFEST.in b/MANIFEST.in
new file mode 100644
index 0000000..45a7391
--- /dev/null
+++ b/MANIFEST.in
@@ -0,0 +1,1 @@
+include yinyang/config/*
\ No newline at end of file
diff --git a/README.md b/README.md
index b218f10..f1cc156 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,4 @@
-<p align="center"><a><img width="130" alt="portfolio_view" align="center" src="media/logo.png"></a></p>
+<p align="center"><a><img width="160" alt="portfolio_view" align="center" src="https://testsmt.github.io/img/tool_logo_with_name.png"></a></p>
 
 <br>
 <p align="center">
@@ -16,20 +16,26 @@
 
 yinyang
 ------------
-A fuzzer for SMT solvers. Given a set of seed SMT formulas, yinyang generates mutant formulas to stress-test SMT solvers. yinyang can be used to robustify SMT solvers. It already found **1,500+** bugs in the two state-of-the-art SMT solvers Z3 and CVC4.
+A fuzzing framework for SMT solvers. Given a set of seed SMT formulas, yinyang generates mutant formulas to stress-test SMT solvers. yinyang can be used to robustify SMT solvers. It already found **1,500+** bugs in the two state-of-the-art SMT solvers Z3 and CVC4.
 
 
 
 Installation
 ------------
-Requirements: 
-- python 3.6+ 
-- antlr4 python runtime  
-``` bash
-git clone https://github.com/testsmt/yinyang.git 
-pip3 install antlr4-python3-runtime==4.9.2  
+To install a stable version of yinyang use:    
+
+```
+pip3 install yinyang
 ```
 
+To install the most recent version, check out the repository:            
+
+``` bash                                                                           
+git clone https://github.com/testsmt/yinyang.git                        
+pip3 install antlr4-python3-runtime==4.9.2                                   
+``` 
+
+Note that you may want to add `yinyang/bin` to your PATH, for running yinyang conveniently without prefix.  
 
 Usage
 -------------
@@ -40,20 +46,20 @@ to download the corresponding SMT-LIB 2 benchmarks. Alternatively, you can downl
 
 3. **Run yinyang** on the benchmarks e.g. with Z3 and CVC4.  
 ```bash
-bin/opfuzz "z3 model_validate=true;cvc4 --check-models -m -i -q" benchmarks 
+typefuzz "z3 model_validate=true;cvc4 --check-models -m -i -q" benchmarks 
 ```
 
 yinyang will by default randomly select formulas from the folder `./benchmarks` and generate 300 mutants per seed formula. If a bug has been found, the bug trigger is stored in `./bugs`. yinyang will run in an infinite loop. You can use the shortcut CTRL+C to terminate yinyang manually.
 
-:blue_book: [Documentation](https://yinyang.readthedocs.io/en/latest/)
+📘 [Documentation](https://yinyang.readthedocs.io/en/latest/)
 
 Feedback
 ---------
 For bugs/issues/questions/feature requests please file an issue. We are always happy to receive your feedback or help you adjust yinyang to the needs of your custom solver, help you build on yinyang, etc.
  
- :memo: [Contact us](https://yinyang.readthedocs.io/en/latest/building_on.html#contact)
+📬 [Contact us](https://yinyang.readthedocs.io/en/latest/building_on.html#contact)
 
-Additional Ressources
+Additional Resources
 ----------
 - [Citing yinyang](https://yinyang.readthedocs.io/en/latest/building_on.html#citing-yinyang)
 - [Project website](https://testsmt.github.io/) with bug statistics, talk videos, etc.
diff --git a/bin/checkstyle.sh b/bin/checkstyle.sh
index c125333..8283446 100755
--- a/bin/checkstyle.sh
+++ b/bin/checkstyle.sh
@@ -1,2 +1,2 @@
 #! /bin/bash
-flake8  --exclude "*SMTLIBv2*,*runtests.py*,__init__.py" src tests config bin/opfuzz bin/yinyang bin/typefuzz --select=E --ignore=E402 --statistics 
+flake8  --exclude "*SMTLIBv2*,*runtests.py*,__init__.py" yinyang/src tests yinyang/config bin/opfuzz bin/yinyang bin/typefuzz --select=E --ignore=E402 --statistics 
diff --git a/bin/opfuzz b/bin/opfuzz
index 6584095..c691d90 100755
--- a/bin/opfuzz
+++ b/bin/opfuzz
@@ -22,6 +22,7 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 
+import os
 import sys
 import signal
 import inspect
@@ -31,14 +32,17 @@ path = Path(__file__)
 rootpath = str(path.parent.absolute().parent)
 sys.path.append(rootpath)
 
-from src.base.Driver import run_checks
-from src.base.Error import raise_runtime_error
-from src.base.ArgumentParser import build_opfuzz_parser
-from src.base.Exitcodes import OK_BUGS, OK_NOBUGS, ERR_USAGE, ERR_INTERNAL
+current_dir = os.getcwd()
 
-from src.core.Fuzzer import Fuzzer
+from yinyang.src.base.Driver import run_checks
+from yinyang.src.base.Error import raise_runtime_error
+from yinyang.src.base.ArgumentParser import build_opfuzz_parser
+from yinyang.src.base.Exitcodes import OK_BUGS, OK_NOBUGS
+from yinyang.src.base.Exitcodes import ERR_USAGE, ERR_INTERNAL
 
-from config.OpfuzzHelptext import (
+from yinyang.src.core.Fuzzer import Fuzzer
+
+from yinyang.config.OpfuzzHelptext import (
     usage,
     header,
     short_description,
@@ -48,7 +52,7 @@ from config.OpfuzzHelptext import (
 
 
 def main():
-    parser = build_opfuzz_parser(rootpath, usage)
+    parser = build_opfuzz_parser(current_dir, usage)
 
     if len(sys.argv) == 1:
 
diff --git a/bin/typefuzz b/bin/typefuzz
index 2f26208..3945148 100755
--- a/bin/typefuzz
+++ b/bin/typefuzz
@@ -21,7 +21,7 @@
 # LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
-
+import os
 import sys
 import signal
 import inspect
@@ -31,14 +31,17 @@ path = Path(__file__)
 rootpath = str(path.parent.absolute().parent)
 sys.path.append(rootpath)
 
-from src.base.Driver import run_checks
-from src.base.Error import raise_runtime_error
-from src.base.ArgumentParser import build_typefuzz_parser
-from src.base.Exitcodes import OK_BUGS, OK_NOBUGS, ERR_USAGE, ERR_INTERNAL
+current_dir = os.getcwd()
+
+from yinyang.src.base.Driver import run_checks
+from yinyang.src.base.Error import raise_runtime_error
+from yinyang.src.base.ArgumentParser import build_typefuzz_parser
+from yinyang.src.base.Exitcodes import OK_BUGS, OK_NOBUGS
+from yinyang.src.base.Exitcodes import ERR_USAGE, ERR_INTERNAL
 
-from src.core.Fuzzer import Fuzzer
+from yinyang.src.core.Fuzzer import Fuzzer
 
-from config.TypefuzzHelptext import (
+from yinyang.config.TypefuzzHelptext import (
     usage,
     header,
     short_description,
@@ -48,7 +51,7 @@ from config.TypefuzzHelptext import (
 
 
 def main():
-    parser = build_typefuzz_parser(rootpath, usage)
+    parser = build_typefuzz_parser(current_dir, usage)
 
     if len(sys.argv) == 1:
 
diff --git a/bin/yinyang b/bin/yinyang
index 17aad83..57b1173 100755
--- a/bin/yinyang
+++ b/bin/yinyang
@@ -22,6 +22,7 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 
+import os
 import sys
 import signal
 import inspect
@@ -31,14 +32,17 @@ path = Path(__file__)
 rootpath = str(path.parent.absolute().parent)
 sys.path.append(rootpath)
 
-from src.base.Driver import run_checks
-from src.base.Error import raise_runtime_error
-from src.base.ArgumentParser import build_yinyang_parser
-from src.base.Exitcodes import OK_BUGS, OK_NOBUGS, ERR_USAGE, ERR_INTERNAL
+current_dir = os.getcwd()
 
-from src.core.Fuzzer import Fuzzer
+from yinyang.src.base.Driver import run_checks
+from yinyang.src.base.Error import raise_runtime_error
+from yinyang.src.base.ArgumentParser import build_yinyang_parser
+from yinyang.src.base.Exitcodes import OK_BUGS, OK_NOBUGS
+from yinyang.src.base.Exitcodes import ERR_USAGE, ERR_INTERNAL
 
-from config.YinyangHelptext import (
+from yinyang.src.core.Fuzzer import Fuzzer
+
+from yinyang.config.YinyangHelptext import (
     usage,
     header,
     short_description,
@@ -48,7 +52,7 @@ from config.YinyangHelptext import (
 
 
 def main():
-    parser = build_yinyang_parser(rootpath, usage)
+    parser = build_yinyang_parser(current_dir, usage)
 
     if len(sys.argv) == 1:
 
diff --git a/config/generalization.txt b/config/generalization.txt
deleted file mode 100644
index c502ad0..0000000
--- a/config/generalization.txt
+++ /dev/null
@@ -1,111 +0,0 @@
-;
-(par (A) (id A A))
-;
-; ### funs from core theory 
-;(true Bool)  
-;(false Bool)
-(not Bool Bool)
-(=> Bool Bool Bool :right-assoc)
-(and Bool Bool Bool :left-assoc)
-(or Bool Bool Bool :left-assoc)
-(xor Bool Bool Bool :left-assoc)
-;(par (A) (= A A Bool :chainable))
-;(par (A) (distinct A A Bool :pairwise))
-;(par (A) (ite Bool A A A))
-
-; ### funs from ints 
-;(NUMERAL Int) 
-(- Int Int)                 ; negation
-(- Int Int Int :left-assoc) ; subtraction
-(+ Int Int Int :left-assoc) 
-(* Int Int Int :left-assoc)
-(div Int Int Int :left-assoc)
-(mod Int Int Int)
-(abs Int Int)
-(<= Int Int Bool :chainable)
-(<  Int Int Bool :chainable)
-(>= Int Int Bool :chainable)
-(>  Int Int Bool :chainable)
-
-; ### funs from reals
-;(NUMERAL Real) 
-;(DECIMAL Real) 
-(- Real Real)                  ; negation
-(- Real Real Real :left-assoc) ; subtraction
-(+ Real Real Real :left-assoc) 
-(* Real Real Real :left-assoc)
-(/ Real Real Real :left-assoc)
-(<= Real Real Bool :chainable)
-(<  Real Real Bool :chainable)
-(>= Real Real Bool :chainable)
-(>  Real Real Bool :chainable)
-
-; ### funs from real-ints 
-;(NUMERAL Int) 
-;(- Int Int)                 ; negation
-(- Int Int Int :left-assoc) ; subtraction
-(+ Int Int Int :left-assoc) 
-(* Int Int Int :left-assoc)
-(div Int Int Int :left-assoc)
-(mod Int Int Int)
-(abs Int Int)
-(<= Int Int Bool :chainable)
-(<  Int Int Bool :chainable)
-(>= Int Int Bool :chainable)
-(>  Int Int Bool :chainable)
-;(DECIMAL Real) 
-(- Real Real)                  ; negation
-(- Real Real Real :left-assoc) ; subtraction
-(+ Real Real Real :left-assoc) 
-(* Real Real Real :left-assoc)
-(/ Real Real Real :left-assoc)
-(<= Real Real Bool :chainable)
-(<  Real Real Bool :chainable)
-(>= Real Real Bool :chainable)
-(>  Real Real Bool :chainable)
-(to_real Int Real)
-(to_int Real Int)
-(is_int Real Bool)
-
-; ### funs from strings
-;
-; ## Core functions 
-(str.++ String String String :left-assoc)
-(str.len String Int)
-(str.< String String Bool :chainable)
-;
-; ## Regular expression functions
-(str.to_re String RegLan) 
-(str.in_re String RegLan Bool) 
-(re.none RegLan)
-(re.all RegLan)
-(re.allchar RegLan)
-(re.++ RegLan RegLan RegLan :left-assoc)
-(re.union RegLan RegLan RegLan :left-assoc)
-(re.inter RegLan RegLan RegLan :left-assoc)
-(re.* RegLan RegLan) 
-;
-; ## Regular expression functions
-(str.<= String String Bool :chainable)   
-(str.at String Int String)
-(str.substr String Int Int String)
-(str.prefixof String String Bool)
-(str.suffixof String String Bool)
-(str.contains String String Bool)
-(str.indexof String String Int Int)
-(str.replace String String String String)
-(str.replace_all String String String String)
-(str.replace_re String RegLan String String) 
-(str.replace_re_all String RegLan String String) 
-(re.comp RegLan RegLan)
-(re.diff RegLan RegLan RegLan :left-assoc)
-(re.+ RegLan RegLan)
-(re.opt RegLan RegLan)
-(re.range String String RegLan)
-; 
-; ## Maps to and from integers
-(str.is_digit String Bool)
-(str.to_code String Int) 
-(str.from_code Int String) 
-(str.to_int String Int)
-(str.from_int Int String)
diff --git a/docs/basic_usage.rst b/docs/basic_usage.rst
index 290d2fe..340463a 100644
--- a/docs/basic_usage.rst
+++ b/docs/basic_usage.rst
@@ -1,13 +1,11 @@
 Basic usage
 ==============
 
-yinyang is a mutation-based fuzzer, i.e. it mutates a set of seed formulas using a mutation strategy and then uses the mutated formulas as the test seeds for SMT solvers. yinyang can so detect soundness bugs, invalid model bugs, crashes, segfaults, etc. Its default mutation strategy is ``opfuzz`` which generates mutants by  interchanging operators, e.g, ``=,distinct,+,-, *,/``.  
-
-You can run yinyang with the ``opfuzz`` strategy using the following command:   
+yinyang is a mutation-based fuzzer, i.e. it mutates a set of seed formulas using a mutation strategy and then uses the mutated formulas as the test seeds for SMT solvers. yinyang can so detect soundness bugs, invalid model bugs, crashes, segfaults, etc. With ``typefuzz`` we generate mutants by generating fresh expressions from the ones from the seed and root them by operators such as ``=,distinct,+,-, *,/`` by one another. You can run yinyang with the ``typefuzz`` strategy using the following command:   
 
 .. code-block:: bash
    
-   $ python3 yinyang.py "<solver_clis>" <seed_path>
+   $ typefuzz "<solver_clis>" <seed_path>
 
 - ``<solver_clis>``: a sequence of SMT solvers command lines separated by semicolons. At least two SMT solvers command lines are necessary.  
 
@@ -19,7 +17,7 @@ You can run yinyang with the ``opfuzz`` strategy using the following command:
 
 .. code-block:: bash
     
-    $ python3 yinyang.py "z3 model_validate=true;cvc4 --check-models -m -i -q" benchmarks 
+    $ typefuzz "z3 model_validate=true;cvc4 --check-models -m -i -q" benchmarks 
 
 
 yinyang will by default randomly select formulas from the folder ``./benchmarks``. By default SMT-LIB files larger than 20k will be ignored.  yinyang will generate 300 mutants per seed formula and will run in an infinite loop. You can use the shortcut ``CTRL+C`` to terminate yinyang manually. If a bug has been found, the bug trigger is stored in ``./bugs``.
@@ -28,4 +26,4 @@ yinyang will by default randomly select formulas from the folder ``./benchmarks`
    To catch invalid model bugs, you have to supply options to enable model validation in ``<solver_clis>``. Also consider that you may need to supply options to enable model production and incremental mode to command lines in ``<solver_clis>``.
 
 **Reducing a bug**.
-After finding a bug, it is useful to produce a minimal test case before reporting the bug to save the SMT solver developers' time and effort. For many test cases, the C code reducer `creduce <https://embed.cs.utah.edu/creduce/>`_ does a great job. Besides, SMT-LIB specific reducer `pyDelta <https://github.com/nafur/pydelta>`_ can be used.   
+After finding a bug, it is useful to produce a minimal test case before reporting the bug to save the SMT solver developers' time and effort. For many test cases, the C code reducer `creduce <https://embed.cs.utah.edu/creduce/>`_ does a great job. Besides, SMT-LIB specific reducer `pydelta <https://github.com/nafur/pydelta>`_ can be used.
diff --git a/docs/building_on.rst b/docs/building_on.rst
index 00daddc..d8bb506 100644
--- a/docs/building_on.rst
+++ b/docs/building_on.rst
@@ -1,85 +1,77 @@
 Building on yinyang
 ===================
+This section  gives a brief overview of TypeFuzz's implementation and describes how researchers and practitioners can customize and extend TypeFuzz and yinyang.
 
-Project structure
-....................
+Understanding TypeFuzz's implementation
+...................................................
+The following file tree shows the most important files of typefuzz and includes a brief description. 
 
-The following tree shows the most important files of the project and includes a description thereof.
+.. code-block:: text
 
+    yinyang
+    ├── bin
+    │   └── typefuzz                        - main executable of typefuzz, cli interface
+    ├── config
+    │   ├── Config.py                       - solver configurations, crash, duplicate, ignore lists
+    │   └── typefuzz_config.txt             - typefuzz configuration file 
+    ├── src
+    │   ├── base                            - contains driver, argument parser, exitcodes, etc.
+    │   ├── core
+    │   │   └──  Fuzzer.py                  - implements the fuzzing loop and the bug checking oracle
+    │   ├── mutators
+    |   |   └── GenTypeAwareMutation
+    │   │       └── GenTypeAwareMutation.py - mutator integrating generative type-aware mutations
+    │   └── parsing
+    │       ├── Ast.py                      - classes for scripts, commands, expressions, etc.
+    │       ├── Parse.py                    - SMT-LIB v2.6 parser
+    │       ├── SMTLIBv2.g4                 - SMT-LIB v2.6 antlr4 grammar
+    │       └── Typechecker.py              - SMT-LIB v2.6 type checker
+    └── tests                               - contains unit, integration, and regression tests
+
+When TypeFuzz is called from the command line, it executes `bin/typefuzz` containing the main function. After parsing the command line and reading in the seeds, the method `Fuzzer.py:run` is called. It randomly pops an SMT-LIB file from the seed list (`Fuzzer.py:142`), then parses (`Fuzzer.py:98`) and type-checks (`Fuzzer.py:146`) the SMT-LIB file. Next, we compute the set of unique expressions (`Fuzzer.py:148`) from the seed and pass it to a newly created mutator GenTypeAwareMutation (`Fuzzer.py:149`). The mutator is then called in a for-loop realizing n consecutive mutations (`Fuzzer.py:171`). Each mutated formula is then passed to the SMT solvers under test which checks for soundness bugs, invalid model bugs, assertion violations, segfaults (`Fuzzer.py:185`) and dumps the bug triggers to the disk. For details on these checks, read the comments in the method `Fuzzer.py:test`.            
+
+Generative type-aware mutation's mutator class is realized in `GenTypeAwareMutation.py`. It takes a type-checked SMT-LIB script and the set of its unique expressions as arguments to the constructor. Then, we parse the configuration file (`yinyang/config/typefuzz_config.txt`) containing the operator signatures. The method `mutate` implements a mutation step. First, we call the method `get_all_subterms` to return a list of all expressions (`av_expr`) and another list with their types (`expr_type`). Next, we repeatedly choose a term t1 from the formula to be substituted by a term t2 (returned by `get_replacee`). If we could successfully construct such a term, then we substitute and return the mutated formula.
+
+The `get_replacee(term)` method randomly chooses an operator from the list of candidate operators. The list of candidate operators contains all operators with a return type matching term's type and includes the identity operator `id`. Next, we pick a type-conforming expression from the set of unique expressions for every argument for the operator at hand and return the expression. The `get_replacee`method may fail, e.g., if we would have picked an operator of a conforming type but no term with conforming types to its arguments exist. To avoid this, we repeat the `get_replacee` method several times.
+
+Customizing and extending yinyang
+...............................................
+The yinyang framework has many tests to ensure the reliability of its mutators and the bug detection logic. All tests are integrated into a CI making sure that the bug-finding ability is preserved on every commit. yinyang adheres to the PEP 8 code quality standard. We briefly describe how researchers and practitioners can customize and extend the framework. For an in-depth overview of the yinyang framework, see the [documentation](https://yinyang.readthedocs.io/en/latest/).                 
+
+Run TypeFuzz with other SMT Solvers
+....................................
+Besides Z3 and CVC4, TypeFuzz can be run with any other SMT solver such as [MathSAT](http://mathsat.fbk.eu), [Boolector](http://verify.inf.usi.ch/content/opensmt2), [Yices](http://yices.csl.sri.com/), and [SMT-Interpol](http://ultimate.informatik.uni-freiburg.de/smtinterpol/), etc. Since TypeFuzz is based on differential testing, it needs at least two solver configurations, ideally with a large overlap in the supported SMT logics. Furthermore, yinyang's type checker currently has stable support for string and arithmetic logics. Support for other logics is currently experimental but will be finalized shortly.
+
+Solver configurations could either be specified in the command line or in the configuration file `yinyang/config/Config.py` such as:  
 .. code-block:: text
-    
-    .
-    ├── config                                  
-    │   ├── config.py                   - solver configurations, crash, duplicate, ignore lists 
-    │   ├── fusion_functions.txt        - fusion functions 
-    │   ├── operator_mutations.txt      - operators used by the opfuzz
-    │   └── option_setting.txt          - options used for option fuzzing   
-    ├── docs                            - documentation
-    ├── examples                        - small SMT-LIB example formulas
-    ├── scripts                         - third-party scripts 
-    ├── src                                     
-    │   ├── args.py                     - commandline parser 
-    │   ├── generators                      
-    │   │   ├── Generator.py            - generic generator class 
-    │   │   ├── SemanticFusion
-    │   │   │   ├── SemanticFusion.py   - generator for fusion
-    │   │   │   ├── VariableFusion.py   - variable fusion, template filling         
-    │   │   │   └── util.py             - conjunction and disjunction of formulas,etc.
-    │   │   └── TypeAwareOpMutation.py  - generator for opfuzz 
-    │   ├── modules
-    │   │   ├── Fuzzer.py               - implements fuzzing loop    
-    │   │   ├── OptionGenerator.py      - implements option fuzzing
-    │   │   ├── Solver.py               - calls SMT solvers  
-    │   │   ├── Statistic.py            - fuzzing statistics 
-    │   ├── parsing
-    │   │   ├── SMTLIBv2.g4             - antlr SMT-LIB grammar
-    │   │   ├── ast.py                  - AST implementation 
-    │   │   ├── ast_visitor.py          - generates AST from parse tree    
-    │   │   ├── parse.py                - parse SMT-LIB from file/string
-    │   │   ├── regenerate_grammar.sh   - script to regenerate SMT-LIB grammar   
-    │   │   └── util.py
-    │   └── utils.py
-    ├── tests                                   
-    │   ├── integration_tests           - opfuzz sanity checks, bug detection etc.          
-    │   └── unittests                   - regular unittests   
-    └── yinyang.py
-
-Devise a custom mutation strategy 
-..................................
-
-1. Add a new generator class to ``src/generators``, e.g., ``CustomGenerator.py``. A generator takes a path to a single SMT-LIB in its constructor, parses the corresponding SMT-LIB file into a Script object, and returns the mutated Script class. The mutation should usually be implemented in a separate generate method, e.g. ``CustomGenerator.py::generate()``. For an example, consider ``src/generators/TypeAwareOpMutation.py``.                
-
-2. Add strategy to commandline option argument ``--strategy`` in ``src/args.py``.    
-
-3. Integrate the generator in the fuzzing loop in ``src/modules/Fuzzer.py::run()``.     
-
-
-Extend the input language 
-................................
-1. Extend grammar ``src/parsing/SMTLIBv2.g4``.   
-2. Regenerate the grammar using ``regenerate_grammar.sh``.
-3. Extend parse tree visitor ``src/parsing/ast_visitor.py`` and AST implementation ``src/parsing/ast.py``.  
-
-
-Use yinyang as an SMT-LIB parser 
-..................................
-The following example shows how you can use yinyang as an SMT-LIB parser.  
-
-.. code-block:: python3 
-
-    from src.parsing.ast import *
-    from src.parsing.parse import *
-    formula=\
-    """
-    (declare-fun x () Int)
-    (declare-fun y () Int)
-    (declare-fun z () Int)
-    (assert (> (* (+ 3 x) (- y 2)) (/ 5 z)))
-    (check-sat)
-    """
-
-    formula, glob = parse_str(formula)
 
+    solvers = [
+        "yices-smt2 --incremental" 
+        "z3 model_validate=true",
+        "z3 model_validate=true smt.arith.solver=6",
+        "cvc4 --check-models --produce-models --incremental --strings-exp -q",
+    ]
+
+To run TypeFuzz with these four solver configurations in the config file, you would need to run `typefuzz "" <benchmark-dir>`. Note, the `crash_list` in yinyang/config/config.py, which may need to be updated ensuring that crashes by the new solver(s) are caught.
+
+Devise a custom mutator 
+.........................
+
+Fuzzing frameworks such as AFL and others have greatly benefited from the SE/PL community efforts to extend their mutation strategies. In the same spirit, we describe steps on how users can extend yinyang with custom mutators.                
+
+1. Add a new mutator class to `src/mutators`, e.g., `CustomGenerator.py`. A mutator takes a parsed SMT-LIB script as its input and returns the mutated script. The mutation should usually be implemented in a separate mutate method `CustomGenerator.py::mutate()`. For example, consider, `src/mutators/GenTypeAwareMutation/GenTypeAwareMutation.py` or `src/mutators/TypeAwareOpMutation.py`.
+2. Provide an executable in the `bin` directory and add parser code to `base/ArgumentParser.py`. 
+3. Integrate the mutator in the fuzzing loop in `src/core/Fuzzer.py::run()`.
+
+Extend the input language
+..........................
+
+Similar to many PLs, the [SMT-LIB language](https://smtlib.cs.uiowa.edu/language.shtml) is steadily augmented by new features, theories, etc. Furthermore, researchers use SMT-LIB dialects for their solver inputs (e.g. for sygus rewrite rules). To support such use cases, we have based yinyang's parser on an [ANTLR](https://www.antlr.org/) grammar that is simple to customize.
+
+1. Extend grammar `src/parsing/SMTLIBv2.g4`.
+2. Regenerate the grammar using `src/parsing/regenerate_grammar.sh`.
+3. Extend parse tree visitor `src/parsing/AstVisitor.py` and AST implementation `src/parsing/Ast.py`.
+4. If type checking is needed, augment the type checker in `src/parsing/Typechecker.py`.    
 
 
 Citing yinyang 
@@ -127,4 +119,6 @@ We are always happy to receive your feedback or help you adjust yinyang to the n
 
 * `Chengyu Zhang <http://chengyuzhang.com/>`_ - dale.chengyu.zhang@gmail.com
 
+* `Jiwon Park <https://www.linkedin.com/in/jiwon-park-473998170/?originalSubdomain=fr>`_ - jiwon.park@polytechnique.edu  
+
 * `Zhendong Su <https://people.inf.ethz.ch/suz/>`_ - zhendong.su@inf.ethz.ch 
diff --git a/docs/customization.rst b/docs/customization.rst
index f389d78..afc71d6 100644
--- a/docs/customization.rst
+++ b/docs/customization.rst
@@ -4,7 +4,7 @@ Customization
 Options 
 .........
 
-yinyang provides the following options. Please consult ``python3 yinyang.py --help`` for a full list.
+yinyang provides the following options. Please consult ``typefuzz --help`` for a full list.
 
 * ``-i --iterations ITERATIONS`` the number of iterations on each seed. (default: 300)  
 * ``-m --modulo MODULO`` specifies how often the mutants will be forwarded to the SMT solvers. For example, with 300 iterations and 2 as a modulo, 150 mutants per seed file will be passed to the SMT solvers. High modulo and iteration counts prioritize deeper mutations. (default: 2) 
@@ -12,17 +12,16 @@ yinyang provides the following options. Please consult ``python3 yinyang.py --he
 * ``-d, --diagnose`` forwards solver outputs to stdout e.g. for solver command line diagnosis. 
 * ``-bugs BUGSFOLDER`` (default: ./bugs) 
 * ``-scratch SCRATCHFOLDER`` specifies where the mutant formulas are temporarily stored. Note, if you run yinyang with several processes in parallel, each instance should have its own scratch folder. (default: ./scratch)      
-* ``-s --strategy {opfuzz,fusion}`` sets the mutation strategy. For more details on fusion, see :doc:`fusion`.  (default: opfuzz)
 * ``-km --keep-mutants`` do not delete the mutants from the scratch folder. Warning: beware that this can quickly exhaust your entire disk space.
 * ``-q --quiet`` do not output statistics and other output.
 * ``-fl", "--file-size-limit`` file size limit on seed formula in bytes. (default: 20000)
 
 
-                        
 
 Customize solvers configurations  
 .................................
-If you want to test several SMT solver configurations at once the putting them  as a commandline argument like ``python3 yinyang.py "<solver_clis>" <seed_path>`` may be inconvenient to you. Instead, you can modify the solver list in ``config/config.py``.  
+If you want to test several SMT solver configurations at once the putting them  as a commandline argument like ``typefuzz "<solver_clis>" <seed_path>`` may be inconvenient to you. Instead, you can modify the solver list in ``.yinyang/Config.py``. The directory file need to be created by the user.   
+
 As an example consider:
 
 .. code-block:: python3
@@ -35,74 +34,46 @@ As an example consider:
         "cvc4 --check-models --produce-models --incremental --strings-exp -q",         
     ] 
 
-You can then use ``python3 yinyang.py "" <seed_path>`` to run the above five solver configurations.    
-
-Option fuzzing
-.......................
-If you want to test many options of an SMT solver with yinyang, you can turn on option fuzzing via ``-optfuzz <file>`` with configuration file ``config/option_setting.txt`` specifying the options. This will randomly add ``set-option`` commands to the mutants.    
-
-**Format:**
-
-.. code-block:: text 
-
-    <solver keywords>
-    <option name> [type|value]*
-    <option name> [type|value]*
-    ###
-    <solver keywords>
-    <option name> [type|value]*
-    <option name> [type|value]*
-    ###
-    <solver keywords>
-    <option name> [type|value]*
-    <option name> [type|value]*
-
-- ``<solver keywords>``  Keywords for matching the solver command lines. If the keywords can be matched.
-
-- ``<option name>``: Name of the option item. 
-
-- ``[type|value]*``: Type or value of the option. The type can be either `bool` or `int` and the value can be either `true`, `false`, or an integer. By default, i.e., by leaving this position empty, the option is assigned to be `bool`. 
-
-- ``###``: Splits option blocks. The options in different blocks are independent.
+You can then use ``typefuzz "" <seed_path>`` to run the above five solver configurations.
 
 
 Customize bug detection  
 .........................
-yinyang's bug detection logic is based on three lists: ``crash_list, duplicate_list, ignore_list`` of ``config/config.py`` which you can customize. yinyang detects crash bugs by matching the stdout and stderr of the solvers in with the strings in the list``crash_list``. If yinyang detects a bug this way, it subsequently matches the crash message against all strings in ``duplicate_list``. The ``duplicate_list`` is useful to filter out repeatedly occurring bugs from getting copied to ``./bugs``.  The ``ignore_list`` can be used to filter out errors occurring in a solver call.  By default yinyang detects mutants returning non-zero exit codes as crashes except those that match with the ``ignore_list``.        
+yinyang's bug detection logic is based on three lists: ``crash_list, duplicate_list, ignore_list`` of ``.yinyang/Config.py`` which you can customize. yinyang detects crash bugs by matching the stdout and stderr of the solvers in with the strings in the list``crash_list``. If yinyang detects a bug this way, it subsequently matches the crash message against all strings in ``duplicate_list``. The ``duplicate_list`` is useful to filter out repeatedly occurring bugs from getting copied to ``./bugs``.  The ``ignore_list`` can be used to filter out errors occurring in a solver call.  By default yinyang detects mutants returning non-zero exit codes as crashes except those that match with the ``ignore_list``.        
 
 
-The below setup shows the three lists in ``config/config.py`` that worked well in practice with Z3 and CVC4. 
+The below setup shows the three lists in ``.yinyang/Config.py`` that worked well in practice with Z3 and CVC4. 
 
 .. code-block:: python3
 
-    crash_list = [                                                                  
-        "Exception",                                                                
-        "lang.AssertionError",                                                      
-        "lang.Error",                                                               
-        "runtime error",                                                            
-        "LEAKED",                                                                      
-        "Leaked",                                                                      
-        "Segmentation fault",                                                          
-        "segmentation fault",                                                          
-        "segfault",                                                                    
-        "ASSERTION",                                                                   
-        "Assertion",                                                                   
-        "Fatal failure",                                                               
-        "Internal error detected",                                                     
-        "an invalid model was generated",                                              
-        "Failed to verify",                                                            
-        "failed to verify",                                                            
-        "ERROR: AddressSanitizer:",                                                    
-        "invalid expression",                                                          
-        "Aborted"                                                                      
-    ]                                                                                  
-                                                                                   
-    duplicate_list = [                                                                 
-                                                                                       
-    ]                                                                                  
-                                                                                   
-    ignore_list = [                                                                    
-       "(error ",          
+    crash_list = [
+        "Exception",
+        "lang.AssertionError",
+        "lang.Error",
+        "runtime error",
+        "LEAKED",
+        "Leaked",
+        "Segmentation fault",
+        "segmentation fault",
+        "segfault",
+        "ASSERTION",
+        "Assertion",
+        "Fatal failure",
+        "Internal error detected",
+        "an invalid model was generated",
+        "Failed to verify",
+        "failed to verify",
+        "ERROR: AddressSanitizer:",
+        "invalid expression",
+        "Aborted"
+    ]
+
+    duplicate_list = [
+
+    ]
+
+    ignore_list = [
+       "(error ",
         "unexpected char",
         "failed to open file",
         "Expected result sat but got unsat",
@@ -113,38 +84,3 @@ The below setup shows the three lists in ``config/config.py`` that worked well i
         "Symbol 'str.to.re' not declared as a variable",
         "Unimplemented code encountered",
     ]
-
-
-
-Customizing mutations 
-...............................
-
-To customize ``opfuzz``'s mutations, you can edit ``config/operator_mutations.txt``. An operator mutation can be bidirectional or unidirectional and may be conditioned on the arity of the operator.
-
-**Format:**
-
-.. code-block:: text 
-
- [<op_name>, ..., <op_name> [arity: k[+,-]]]*
- [<op_name> -> <op_name> [arity: k[+,-]]]*
-
-    
-where ``k`` is a positive integer, ``+`` indicates at least one and ``-`` indicates at most one.   
-
-**Example:**
-
-
-.. code-block:: text 
-    
-    +, -, * 
-    =,distinct: arity: 2+ 
-    -,abs: arity: 1- 
-    abs -> - 
-
-
-Line 1: Operators ``+, -, *`` in the same line form an equivalence class and can bidirectionally replace each other. 
-
-Line 2+3: Operator mutations conditioned on arity. This requires operators ``=`` and ``distinct`` to have at least two arguments to trigger the  mutation, and ``-``, ``abs`` to have at most one argument.
-
-Line 4:  Unidirectional from operator ``abs`` to operator ``-``.
-
diff --git a/docs/fusion.rst b/docs/fusion.rst
index bcd720e..1238e4e 100644
--- a/docs/fusion.rst
+++ b/docs/fusion.rst
@@ -54,14 +54,14 @@ Fusion requires the seeds that are pre-categorized to be either sat or unsat. Pr
 
 Fusion functions
 ................................
-The configuration file ``config/fusion_functions.txt`` specifies fusion and inversion functions.  The format is the following:  
+The configuration file ``yinyang/config/fusion_functions.txt`` specifies fusion and inversion functions.  The format is the following:  
 
 .. code-block:: text 
 
     #begin  
-    <declartation of x>
-    <declartation of y>
-    <declartation of z>
+    <declaration of x>
+    <declaration of y>
+    <declaration of z>
     [<declaration of c>]
     <assert fusion function>
     <assert inversion function> 
@@ -70,7 +70,7 @@ The configuration file ``config/fusion_functions.txt`` specifies fusion and inve
 
 **Example:**
 
-The following code shows schematically fusion and inversion are described in ``config/fusion_functions.txt``.
+The following code shows schematically fusion and inversion are described in ``yinyang/config/fusion_functions.txt``.
 
 .. code-block:: text 
 
diff --git a/docs/index.rst b/docs/index.rst
index 87fd39a..b5f5a13 100644
--- a/docs/index.rst
+++ b/docs/index.rst
@@ -6,16 +6,16 @@ yinyang: a fuzzer for SMT solvers
   :align: center 
 
 
-yinyang is a `fuzzer <https://en.wikipedia.org/wiki/Fuzzing>`_ for SMT solvers. Given a set of `SMT-LIB <http://smtlib.cs.uiowa.edu/language.shtml>`_ seed formulas, it generates mutant formulas to stress-test SMT solvers. yinyang roughly operates in the following stages: 
+yinyang is a `fuzzing framework <https://en.wikipedia.org/wiki/Fuzzing>`_ for SMT solvers. It realizes three tools `typefuzz`, `opfuzz` and `yinyang`.  Given a set of `SMT-LIB <http://smtlib.cs.uiowa.edu/language.shtml>`_ seed formulas, each of the tools generates mutant formulas to stress-test SMT solvers. yinyang roughly operates in the following stages: 
 
 
 1. *Parsing:* First, yinyang parses a single or a set of SMT-LIB formulas to be used for fuzzing. yinyang's parser supports the SMT-LIB v2.6 standard and is customizable. 
 
-2. *Mutation:* Next, yinyang will mutate the parsed formula(s) using a mutation strategy. By default, yinyang performs type-aware substitutions of operators and will by default generate 300 mutant formulas per parsed formula. Another mutation strategy is fusion, which fuses two formulas of known satisfiability.     
+2. *Mutation:* Next, yinyang will mutate the parsed formula(s) using a mutation strategy. yinyang ships three mutation stragies. The most powerful one is generative type-aware operator mutation which mutates expressions within seed formulas and will by default generate 300 mutant formulas per parsed formula.
 
-3. *Oracle Check:* Finally, yinyang will query the SMT solvers under test with the mutant formulas and compare the result against a test oracle. By default, such a test oracle would be a second SMT solver but it can also be fixed to be sat or unsat.  
+3. *Oracle Check:* Finally, yinyang will query the SMT solvers under test with the mutant formulas and compare the result against a test oracle. By default, such a test oracle would be a second SMT solver but it can also be fixed to be sat or unsat.
 
-yinyang is intended for use by (1) SMT solver developers testing existing solvers, (2) researchers inventing new decision procedures to asses the robustness of their implementations, and (3) practitioners developing applications based on SMT solvers.    
+yinyang is intended for use by (1) SMT solver developers testing existing solvers, (2) researchers inventing new decision procedures to asses the robustness of their implementations, and (3) practitioners developing applications based on SMT solvers.
 
 .. toctree::
    :maxdepth: 2
diff --git a/docs/installation.rst b/docs/installation.rst
index f2895ad..1f05907 100644
--- a/docs/installation.rst
+++ b/docs/installation.rst
@@ -1,17 +1,15 @@
 Installation
 ==============
 
-*Requirements:* 
+To install a stable version of yinyang use:
 
-- python 3.6+
-- antlr4 python runtime
+```
+pip3 install yinyang
+```
 
-
-The following commands clone yinyang and install the antlr4 python runtime.  
+The following commands clone yinyang and install the antlr4 python runtime.
 
 .. code-block:: bash
 
-    $ git clone https://github.com/testsmt/yinyang.git 
-    $ pip3 install antlr4-python3-runtime==4.9.2  
-
-
+    $ git clone https://github.com/testsmt/yinyang.git
+    $ pip3 install antlr4-python3-runtime==4.9.2
diff --git a/docs/setup.rst b/docs/setup.rst
index 63a5b6d..237b836 100644
--- a/docs/setup.rst
+++ b/docs/setup.rst
@@ -17,7 +17,7 @@ or use your own benchmarks.
 SMT solvers
 ..............
 
-To run yinyang in default mode, you need to install two or more SMT solvers.   
+To run typefuzz or opfuzz, you need to install two or more SMT solvers.   
 The SMT-LIB initiative provides a comprehensive `list of SMT solvers <http://smtlib.cs.uiowa.edu/solvers.shtml>`_.
 Make sure that all SMT solver you consider for testing supports the chosen seeds. 
 
diff --git a/pyproject.toml b/pyproject.toml
new file mode 100644
index 0000000..374b58c
--- /dev/null
+++ b/pyproject.toml
@@ -0,0 +1,6 @@
+[build-system]
+requires = [
+    "setuptools>=42",
+    "wheel"
+]
+build-backend = "setuptools.build_meta"
diff --git a/setup.cfg b/setup.cfg
new file mode 100644
index 0000000..78efab4
--- /dev/null
+++ b/setup.cfg
@@ -0,0 +1,28 @@
+[metadata]
+name = yinyang
+version = 0.3.0
+author = Dominik Winterer, Chengyu Zhang, Jiwon Park, Zhendong Su
+author_email = dominik.winterer@inf.ethz.ch, dale.chengyu.zhang@gmail.com, jiwon.park@polytechnique.edu, ‎zhendong.su@inf.ethz.ch
+description = A fuzzing framework for SMT solvers
+long_description = file: README.md
+long_description_content_type = text/markdown
+url = https://testsmt.github.io/
+project_urls =
+    Bug Tracker = https://github.com/testsmt/yinyang/issues
+    Documentation = https://yinyang.readthedocs.io/en/latest/
+    Source Code = https://github.com/testsmt/yinyang
+classifiers =
+    Programming Language :: Python :: 3
+    License :: OSI Approved :: MIT License
+    Operating System :: OS Independent
+
+[options]
+include_package_data = True
+packages = find:
+install_requires =
+    antlr4-python3-runtime==4.9.2
+python_requires = >=3.6
+scripts =
+    bin/yinyang
+    bin/opfuzz
+    bin/typefuzz
diff --git a/yinyang/__init__.py b/yinyang/__init__.py
new file mode 100644
index 0000000..e69de29
diff --git a/config/Config.py b/yinyang/config/Config.py
similarity index 99%
rename from config/Config.py
rename to yinyang/config/Config.py
index c463ccc..6a00b7b 100644
--- a/config/Config.py
+++ b/yinyang/config/Config.py
@@ -50,7 +50,7 @@
 
 ignore_list = [
     "(error ",
-    "unsupport",
+    "unsupported",
     "unexpected char",
     "failed to open file",
     "Expected result sat but got unsat",
diff --git a/config/OpfuzzHelptext.py b/yinyang/config/OpfuzzHelptext.py
similarity index 98%
rename from config/OpfuzzHelptext.py
rename to yinyang/config/OpfuzzHelptext.py
index a37f382..34a6247 100644
--- a/config/OpfuzzHelptext.py
+++ b/yinyang/config/OpfuzzHelptext.py
@@ -20,15 +20,13 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 
-from src.base.Version import VERSION, COMMIT
+from yinyang.src.base.Version import VERSION
 
 
 header = (
     "opfuzz -- a differential fuzzer for SMT solvers [version: "
     + VERSION
-    + " ("
-    + COMMIT
-    + ")]"
+    + "]"
 )
 
 usage = """ opfuzz [options] solver_clis seed_file   [optionally, more seed files]
diff --git a/config/TypefuzzHelptext.py b/yinyang/config/TypefuzzHelptext.py
similarity index 97%
rename from config/TypefuzzHelptext.py
rename to yinyang/config/TypefuzzHelptext.py
index fc7c54b..7ee4123 100644
--- a/config/TypefuzzHelptext.py
+++ b/yinyang/config/TypefuzzHelptext.py
@@ -20,7 +20,7 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 
-from src.base.Version import VERSION
+from yinyang.src.base.Version import VERSION
 
 
 header = (
@@ -99,7 +99,6 @@
 SMT solvers need options to support a particular set of seeds. E.g, cvc5 needs
 the option "--strings-exp" to support string logic. Otherwise it will often
 throw an error message.
-
 """  # noqa: E501
 
 
@@ -120,7 +119,8 @@
     -s <path>, --scratchfolder <path>
             temp folder to dump mutants (default: ./scratch)
     -c <file>, --config <file>
-            set custom config file. (default: config/typefuzz_config.txt)
+            set custom config file. 
+            (default: yinyang/config/typefuzz_config.txt)
     -L <bytes>, --limit <bytes>
             file size limit on seed formula in bytes (default: 100000)
     -n, --no-log    disable logging
diff --git a/config/YinyangHelptext.py b/yinyang/config/YinyangHelptext.py
similarity index 97%
rename from config/YinyangHelptext.py
rename to yinyang/config/YinyangHelptext.py
index fd10192..b354d09 100644
--- a/config/YinyangHelptext.py
+++ b/yinyang/config/YinyangHelptext.py
@@ -20,15 +20,13 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 
-from src.base.Version import VERSION, COMMIT
+from yinyang.src.base.Version import VERSION
 
 
 header = (
     "yinyang -- a differential fuzzer for SMT solvers [version: "
     + VERSION
-    + " ("
-    + COMMIT
-    + ")]"
+    + "]"
 )
 
 usage = """ yinyang [options] -o oracle solver_clis seed_file1 seed_file2 [optionally, more seed files]
@@ -71,7 +69,7 @@
 yinyang is a tool for finding bugs in SMT solver by generating mutant SMT-LIB
 scripts from a set of seed SMT-LIB scripts (.smt2 files) with known
 satisfiability (i.e. either sat or unsat) and generates mutant formulas of the
-same satisfiability. yinyang realizes semantic fusion whihc can work with a
+same satisfiability. yinyang realizes semantic fusion which can work with a
 single SMT solver. The idea behind semantic fusion is to fuse formula pairs of
 the same satisfiability (both either sat or unsat) and so produce mutant
 formulas of known satisfiability.
diff --git a/yinyang/config/__init__.py b/yinyang/config/__init__.py
new file mode 100644
index 0000000..e69de29
diff --git a/config/fusion_functions.txt b/yinyang/config/fusion_functions.txt
similarity index 100%
rename from config/fusion_functions.txt
rename to yinyang/config/fusion_functions.txt
diff --git a/config/operator_mutations.txt b/yinyang/config/operator_mutations.txt
similarity index 100%
rename from config/operator_mutations.txt
rename to yinyang/config/operator_mutations.txt
diff --git a/config/option_setting.txt b/yinyang/config/option_setting.txt
similarity index 99%
rename from config/option_setting.txt
rename to yinyang/config/option_setting.txt
index 94e48c0..78580ea 100644
--- a/config/option_setting.txt
+++ b/yinyang/config/option_setting.txt
@@ -320,7 +320,7 @@ rewriter.push_ite_arith
 rewriter.push_ite_bv
 rewriter.push_to_real
 rewriter.rewrite_patterns
-rewriter.som
+rewriter.some
 rewriter.sort_store
 rewriter.sort_sums
 rewriter.split_concat_eq
diff --git a/config/typefuzz_config.txt b/yinyang/config/typefuzz_config.txt
similarity index 100%
rename from config/typefuzz_config.txt
rename to yinyang/config/typefuzz_config.txt
diff --git a/yinyang/src/__init__.py b/yinyang/src/__init__.py
new file mode 100644
index 0000000..e69de29
diff --git a/src/base/ArgumentParser.py b/yinyang/src/base/ArgumentParser.py
similarity index 78%
rename from src/base/ArgumentParser.py
rename to yinyang/src/base/ArgumentParser.py
index 2e0ceb1..cb0b520 100644
--- a/src/base/ArgumentParser.py
+++ b/yinyang/src/base/ArgumentParser.py
@@ -20,10 +20,17 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 
+import sys
 import argparse
 
-from src.base.Exitcodes import ERR_USAGE
-from src.base.Version import VERSION, COMMIT
+from yinyang.src.base.Exitcodes import ERR_USAGE
+from yinyang.src.base.Version import VERSION, COMMIT
+
+from pathlib import Path
+
+path = Path(__file__)
+ROOTPATH = str(path.parent.absolute().parent.parent.parent)
+sys.path.append(ROOTPATH)
 
 
 class ArgumentParser(argparse.ArgumentParser):
@@ -36,7 +43,7 @@ def error(self, message):
         )
 
 
-def add_common_args(parser, rootpath):
+def add_common_args(parser, rootpath, current_dir):
     parser.add_argument(
         "SOLVER_CLIS",
         metavar="solver_clis",
@@ -50,7 +57,7 @@ def add_common_args(parser, rootpath):
         "-l",
         "--logfolder",
         metavar="path_path_to_folder",
-        default=rootpath + "/logs",
+        default=current_dir + "/logs",
     )
     parser.add_argument(
         "-h",
@@ -69,13 +76,13 @@ def add_common_args(parser, rootpath):
         "-b",
         "--bugsfolder",
         metavar="path_to_folder",
-        default=rootpath + "/bugs",
+        default=current_dir + "/bugs",
     )
     parser.add_argument(
         "-s",
         "--scratchfolder",
         metavar="path_to_folder",
-        default=rootpath + "/scratch",
+        default=current_dir + "/scratch",
     )
     parser.add_argument(
         "-q",
@@ -96,7 +103,7 @@ def add_common_args(parser, rootpath):
     )
 
 
-def add_opfuzz_args(parser, rootpath):
+def add_opfuzz_args(parser, rootpath, current_dir):
     parser.add_argument(
         "-i",
         "--iterations",
@@ -121,11 +128,11 @@ def add_opfuzz_args(parser, rootpath):
         "-c",
         "--config",
         metavar="path_to_file",
-        default=rootpath + "/config/operator_mutations.txt",
+        default=rootpath + "/yinyang/config/operator_mutations.txt",
     )
 
 
-def add_typefuzz_args(parser, rootpath):
+def add_typefuzz_args(parser, rootpath, current_dir):
     parser.add_argument(
         "-i",
         "--iterations",
@@ -150,11 +157,11 @@ def add_typefuzz_args(parser, rootpath):
         "-c",
         "--config",
         metavar="path_to_file",
-        default=rootpath + "/config/typefuzz_config.txt",
+        default=rootpath + "/yinyang/config/typefuzz_config.txt",
     )
 
 
-def add_yinyang_args(parser, rootpath):
+def add_yinyang_args(parser, rootpath, current_dir):
     parser.add_argument(
         "-o",
         "--oracle",
@@ -179,44 +186,44 @@ def add_yinyang_args(parser, rootpath):
         "-c",
         "--config",
         metavar="path_to_file",
-        default=rootpath + "/config/fusion_functions.txt",
+        default=rootpath + "/yinyang/config/fusion_functions.txt",
     )
 
 
-def build_opfuzz_parser(rootpath, usage):
+def build_opfuzz_parser(current_dir, usage):
     parser = ArgumentParser(
         description="",
         usage=usage,
         formatter_class=argparse.RawDescriptionHelpFormatter,
         add_help=False,
     )
-    add_common_args(parser, rootpath)
-    add_opfuzz_args(parser, rootpath)
+    add_common_args(parser, ROOTPATH, current_dir)
+    add_opfuzz_args(parser, ROOTPATH, current_dir)
 
     return parser
 
 
-def build_typefuzz_parser(rootpath, usage):
+def build_typefuzz_parser(current_dir, usage):
     parser = ArgumentParser(
         description="",
         usage=usage,
         formatter_class=argparse.RawDescriptionHelpFormatter,
         add_help=False,
     )
-    add_common_args(parser, rootpath)
-    add_typefuzz_args(parser, rootpath)
+    add_common_args(parser, ROOTPATH, current_dir)
+    add_typefuzz_args(parser, ROOTPATH, current_dir)
 
     return parser
 
 
-def build_yinyang_parser(rootpath, usage):
+def build_yinyang_parser(current_dir, usage):
     parser = ArgumentParser(
         description="",
         usage=usage,
         formatter_class=argparse.RawDescriptionHelpFormatter,
         add_help=False,
     )
-    add_common_args(parser, rootpath)
-    add_yinyang_args(parser, rootpath)
+    add_common_args(parser, ROOTPATH, current_dir)
+    add_yinyang_args(parser, ROOTPATH, current_dir)
 
     return parser
diff --git a/src/base/Driver.py b/yinyang/src/base/Driver.py
similarity index 96%
rename from src/base/Driver.py
rename to yinyang/src/base/Driver.py
index 45a393f..6296811 100644
--- a/src/base/Driver.py
+++ b/yinyang/src/base/Driver.py
@@ -23,16 +23,16 @@
 import os
 import sys
 from pathlib import Path
-from src.base.Exitcodes import ERR_USAGE, ERR_EXHAUSTED_DISK
+from yinyang.src.base.Exitcodes import ERR_USAGE, ERR_EXHAUSTED_DISK
 
 path = Path(__file__)
 rootpath = str(path.parent.absolute().parent)
 
 try:
     sys.path.insert(1, os.getcwd() + "/.yinyang")
-    from Config import solvers
+    from yinyang.config import solvers
 except Exception as e:
-    from config.Config import solvers
+    from yinyang.config.Config import solvers
 
 
 def check_solver_clis():
diff --git a/src/base/Error.py b/yinyang/src/base/Error.py
similarity index 96%
rename from src/base/Error.py
rename to yinyang/src/base/Error.py
index 8106180..df37729 100644
--- a/src/base/Error.py
+++ b/yinyang/src/base/Error.py
@@ -20,7 +20,7 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 
-from src.base.Version import VERSION, COMMIT
+from yinyang.src.base.Version import VERSION, COMMIT
 
 
 def raise_runtime_error(trace, argv, e):
diff --git a/src/base/Exitcodes.py b/yinyang/src/base/Exitcodes.py
similarity index 81%
rename from src/base/Exitcodes.py
rename to yinyang/src/base/Exitcodes.py
index 4d2b346..250c734 100644
--- a/src/base/Exitcodes.py
+++ b/yinyang/src/base/Exitcodes.py
@@ -20,9 +20,9 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 
-OK_NOBUGS = 0  # no error and no bugs
-OK_BUGS = 1  # no error and bugs
-ERR_USAGE = 2  # commandline usage error
-ERR_INTERNAL = 3  # internal error within the tool
-ERR_SOLVER_CFG = 4  # usage error of one or more solver configurations
+OK_NOBUGS = 0           # no error and no bugs
+OK_BUGS = 10            # no error and bugs
+ERR_USAGE = 2           # commandline usage error
+ERR_INTERNAL = 3        # internal error within the tool
+ERR_SOLVER_CFG = 4      # usage error of one or more solver configurations
 ERR_EXHAUSTED_DISK = 5  # disk space exhaustion error
diff --git a/src/base/Utils.py b/yinyang/src/base/Utils.py
similarity index 100%
rename from src/base/Utils.py
rename to yinyang/src/base/Utils.py
diff --git a/src/base/Version.py b/yinyang/src/base/Version.py
similarity index 98%
rename from src/base/Version.py
rename to yinyang/src/base/Version.py
index 404f215..c15c52b 100644
--- a/src/base/Version.py
+++ b/yinyang/src/base/Version.py
@@ -20,5 +20,5 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 
-VERSION = "0.2.0"
+VERSION = "0.3.0"
 COMMIT = "unknown"
diff --git a/yinyang/src/base/__init__.py b/yinyang/src/base/__init__.py
new file mode 100644
index 0000000..e69de29
diff --git a/src/core/Fuzzer.py b/yinyang/src/core/Fuzzer.py
similarity index 93%
rename from src/core/Fuzzer.py
rename to yinyang/src/core/Fuzzer.py
index ce32315..3a58899 100644
--- a/src/core/Fuzzer.py
+++ b/yinyang/src/core/Fuzzer.py
@@ -30,24 +30,24 @@
 import logging
 import pathlib
 
-from src.core.Statistic import Statistic
-from src.core.Solver import Solver, SolverQueryResult, SolverResult
+from yinyang.src.core.Statistic import Statistic
+from yinyang.src.core.Solver import Solver, SolverQueryResult, SolverResult
 
-from src.parsing.Parse import parse_file
-from src.parsing.Typechecker import typecheck
+from yinyang.src.parsing.Parse import parse_file
+from yinyang.src.parsing.Typechecker import typecheck
 
-from src.mutators.TypeAwareOpMutation import TypeAwareOpMutation
-from src.mutators.SemanticFusion.SemanticFusion import SemanticFusion
-from src.mutators.GenTypeAwareMutation.Util import get_unique_subterms
-from src.mutators.GenTypeAwareMutation.GenTypeAwareMutation import (
+from yinyang.src.mutators.TypeAwareOpMutation import TypeAwareOpMutation
+from yinyang.src.mutators.SemanticFusion.SemanticFusion import SemanticFusion
+from yinyang.src.mutators.GenTypeAwareMutation.Util import get_unique_subterms
+from yinyang.src.mutators.GenTypeAwareMutation.GenTypeAwareMutation import (
     GenTypeAwareMutation
 )
 
 
-from src.base.Utils import random_string, plain, escape
-from src.base.Exitcodes import OK_BUGS, OK_NOBUGS, ERR_EXHAUSTED_DISK
+from yinyang.src.base.Utils import random_string, plain, escape
+from yinyang.src.base.Exitcodes import OK_BUGS, OK_NOBUGS, ERR_EXHAUSTED_DISK
 
-from src.core.Logger import (
+from yinyang.src.core.Logger import (
     init_logging,
     log_strategy_num_seeds,
     log_generation_attempt,
@@ -60,7 +60,7 @@
     log_soundness_trigger,
     log_invalid_mutant,
 )
-from src.core.FuzzerUtil import (
+from yinyang.src.core.FuzzerUtil import (
     get_seeds,
     grep_result,
     admissible_seed_size,
@@ -249,13 +249,14 @@ def test(self, script, iteration):
                 return False
 
             # Match stdout and stderr against the crash list
-            # (see config/Config.py:27) which contains various crash messages
-            # such as assertion errors, check failure, invalid models, etc.
+            # (see yinyang/config/Config.py:27) which contains various
+            # crash messages such as assertion errors, check failure, 
+            # invalid models, etc.
             if in_crash_list(stdout, stderr):
 
                 # Match stdout and stderr against the duplicate list
-                # (see config/Config.py:51) to prevent catching duplicate bug
-                # triggers.
+                # (see yinyang/config/Config.py:51) to prevent catching 
+                # duplicate bug triggers.
                 if not in_duplicate_list(stdout, stderr):
                     self.statistic.effective_calls += 1
                     self.statistic.crashes += 1
@@ -271,7 +272,8 @@ def test(self, script, iteration):
 
                 # Check whether the solver call produced errors, e.g, related
                 # to its parser, options, type-checker etc., by matching stdout
-                # and stderr against the ignore list (see config/Config.py:54).
+                # and stderr against the ignore list 
+                # (see yinyang/config/Config.py:54).
                 if in_ignore_list(stdout, stderr):
                     log_ignore_list_mutant(solver_cli)
                     self.statistic.invalid_mutants += 1
diff --git a/src/core/FuzzerUtil.py b/yinyang/src/core/FuzzerUtil.py
similarity index 92%
rename from src/core/FuzzerUtil.py
rename to yinyang/src/core/FuzzerUtil.py
index 6237ae7..c1121e3 100644
--- a/src/core/FuzzerUtil.py
+++ b/yinyang/src/core/FuzzerUtil.py
@@ -23,15 +23,15 @@
 import re
 import pathlib
 
-from src.base.Utils import in_list
+from yinyang.src.base.Utils import in_list
 
 try:
     sys.path.insert(1, os.getcwd() + "/.yinyang")
-    from Config import crash_list, duplicate_list, ignore_list
+    from yinyang.config import crash_list, duplicate_list, ignore_list
 except Exception as e:
-    from config.Config import crash_list, duplicate_list, ignore_list
+    from yinyang.config.Config import crash_list, duplicate_list, ignore_list
 
-from src.core.Solver import SolverResult, SolverQueryResult
+from yinyang.src.core.Solver import SolverResult, SolverQueryResult
 
 
 def in_crash_list(stdout, stderr):
diff --git a/src/core/Logger.py b/yinyang/src/core/Logger.py
similarity index 98%
rename from src/core/Logger.py
rename to yinyang/src/core/Logger.py
index 06d8e25..f28d5ec 100644
--- a/src/core/Logger.py
+++ b/yinyang/src/core/Logger.py
@@ -116,7 +116,7 @@ def log_solver_timeout(args, solver_cli, i):
         str(i)
         + "/"
         + str(args.iterations)
-        + " Solver timeout occured. sol="
+        + " Solver timeout occurred. sol="
         + str(solver_cli)
     )
 
diff --git a/src/core/OptionGenerator.py b/yinyang/src/core/OptionGenerator.py
similarity index 100%
rename from src/core/OptionGenerator.py
rename to yinyang/src/core/OptionGenerator.py
diff --git a/src/core/Solver.py b/yinyang/src/core/Solver.py
similarity index 98%
rename from src/core/Solver.py
rename to yinyang/src/core/Solver.py
index 1ecf8fd..86f627a 100644
--- a/src/core/Solver.py
+++ b/yinyang/src/core/Solver.py
@@ -23,7 +23,7 @@
 import subprocess
 from enum import Enum
 
-from src.base.Exitcodes import ERR_USAGE
+from yinyang.src.base.Exitcodes import ERR_USAGE
 
 
 class SolverQueryResult(Enum):
diff --git a/src/core/Statistic.py b/yinyang/src/core/Statistic.py
similarity index 100%
rename from src/core/Statistic.py
rename to yinyang/src/core/Statistic.py
diff --git a/yinyang/src/core/__init__.py b/yinyang/src/core/__init__.py
new file mode 100644
index 0000000..e69de29
diff --git a/src/mutators/GenTypeAwareMutation/GenTypeAwareMutation.py b/yinyang/src/mutators/GenTypeAwareMutation/GenTypeAwareMutation.py
similarity index 94%
rename from src/mutators/GenTypeAwareMutation/GenTypeAwareMutation.py
rename to yinyang/src/mutators/GenTypeAwareMutation/GenTypeAwareMutation.py
index 15b5f8e..4a985eb 100644
--- a/src/mutators/GenTypeAwareMutation/GenTypeAwareMutation.py
+++ b/yinyang/src/mutators/GenTypeAwareMutation/GenTypeAwareMutation.py
@@ -22,15 +22,15 @@
 
 import random
 
-from src.mutators.Mutator import Mutator
-from src.mutators.GenTypeAwareMutation.Operator import (
+from yinyang.src.mutators.Mutator import Mutator
+from yinyang.src.mutators.GenTypeAwareMutation.Operator import (
     Operator, handle_parametric_op, handle_non_parametric_op
 )
-from src.mutators.GenTypeAwareMutation.Util import (
+from yinyang.src.mutators.GenTypeAwareMutation.Util import (
     type2num, get_all_subterms, local_compatible
 )
-from src.parsing.Ast import Expr
-from src.parsing.Types import ALL
+from yinyang.src.parsing.Ast import Expr
+from yinyang.src.parsing.Types import ALL
 
 
 class GenTypeAwareMutation(Mutator):
@@ -44,7 +44,7 @@ def __init__(self, formula, args, unique_expr):
     def parse_config_file(self):
         """
         Read the customizable configuration file.
-        Customize the configuration file at config/generalization.txt.
+        Customize the configuration file at yinyang/config/generalization.txt.
         Configuration file contains all the signatures of SMT-LIB operators
         and the signatures are used for operator choice during the mutation.
         """
diff --git a/src/mutators/GenTypeAwareMutation/Operator.py b/yinyang/src/mutators/GenTypeAwareMutation/Operator.py
similarity index 98%
rename from src/mutators/GenTypeAwareMutation/Operator.py
rename to yinyang/src/mutators/GenTypeAwareMutation/Operator.py
index 99a8019..c62a654 100644
--- a/src/mutators/GenTypeAwareMutation/Operator.py
+++ b/yinyang/src/mutators/GenTypeAwareMutation/Operator.py
@@ -20,7 +20,7 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 
-from src.parsing.Types import sort2type
+from yinyang.src.parsing.Types import sort2type
 
 
 class Operator:
diff --git a/src/mutators/GenTypeAwareMutation/Util.py b/yinyang/src/mutators/GenTypeAwareMutation/Util.py
similarity index 98%
rename from src/mutators/GenTypeAwareMutation/Util.py
rename to yinyang/src/mutators/GenTypeAwareMutation/Util.py
index 7c56306..3720e84 100644
--- a/src/mutators/GenTypeAwareMutation/Util.py
+++ b/yinyang/src/mutators/GenTypeAwareMutation/Util.py
@@ -22,8 +22,8 @@
 
 import copy
 
-from src.parsing.Ast import Term
-from src.parsing.Types import (
+from yinyang.src.parsing.Ast import Term
+from yinyang.src.parsing.Types import (
     BOOLEAN_TYPE, REAL_TYPE, INTEGER_TYPE, ROUNDINGMODE_TYPE,
     STRING_TYPE, REGEXP_TYPE
 )
diff --git a/yinyang/src/mutators/GenTypeAwareMutation/__init__.py b/yinyang/src/mutators/GenTypeAwareMutation/__init__.py
new file mode 100644
index 0000000..e69de29
diff --git a/src/mutators/Mutator.py b/yinyang/src/mutators/Mutator.py
similarity index 100%
rename from src/mutators/Mutator.py
rename to yinyang/src/mutators/Mutator.py
diff --git a/src/mutators/SemanticFusion/SemanticFusion.py b/yinyang/src/mutators/SemanticFusion/SemanticFusion.py
old mode 100755
new mode 100644
similarity index 93%
rename from src/mutators/SemanticFusion/SemanticFusion.py
rename to yinyang/src/mutators/SemanticFusion/SemanticFusion.py
index f7c0b4c..7a9ece9
--- a/src/mutators/SemanticFusion/SemanticFusion.py
+++ b/yinyang/src/mutators/SemanticFusion/SemanticFusion.py
@@ -23,8 +23,8 @@
 import random
 import copy
 
-from src.mutators.Mutator import Mutator
-from src.mutators.SemanticFusion.VariableFusion import (
+from yinyang.src.mutators.Mutator import Mutator
+from yinyang.src.mutators.SemanticFusion.VariableFusion import (
     fill_template,
     inv_x,
     inv_y,
@@ -32,14 +32,14 @@
     add_fusion_constraints,
     add_var_decls,
 )
-from src.mutators.SemanticFusion.Util import (
+from yinyang.src.mutators.SemanticFusion.Util import (
     random_var_triplets,
     disjunction,
     conjunction,
 )
-from src.base.Exitcodes import ERR_USAGE
-from src.parsing.Parse import parse_str
-from src.parsing.Ast import DeclareFun
+from yinyang.src.base.Exitcodes import ERR_USAGE
+from yinyang.src.parsing.Parse import parse_str
+from yinyang.src.parsing.Ast import DeclareFun
 
 
 class SemanticFusion(Mutator):
diff --git a/src/mutators/SemanticFusion/Util.py b/yinyang/src/mutators/SemanticFusion/Util.py
old mode 100755
new mode 100644
similarity index 99%
rename from src/mutators/SemanticFusion/Util.py
rename to yinyang/src/mutators/SemanticFusion/Util.py
index 6066e74..aaad004
--- a/src/mutators/SemanticFusion/Util.py
+++ b/yinyang/src/mutators/SemanticFusion/Util.py
@@ -23,7 +23,7 @@
 import random
 import itertools
 
-from src.parsing.Ast import (
+from yinyang.src.parsing.Ast import (
     Term,
     Script,
     Assert,
diff --git a/src/mutators/SemanticFusion/VariableFusion.py b/yinyang/src/mutators/SemanticFusion/VariableFusion.py
old mode 100755
new mode 100644
similarity index 97%
rename from src/mutators/SemanticFusion/VariableFusion.py
rename to yinyang/src/mutators/SemanticFusion/VariableFusion.py
index fc02687..15da885
--- a/src/mutators/SemanticFusion/VariableFusion.py
+++ b/yinyang/src/mutators/SemanticFusion/VariableFusion.py
@@ -24,7 +24,7 @@
 import copy
 import string
 
-from src.parsing.Ast import Const, Var, Expr, Assert, DeclareConst
+from yinyang.src.parsing.Ast import Const, Var, Expr, Assert, DeclareConst
 
 
 def gen_random_string(length):
@@ -73,7 +73,7 @@ def get_constant_idx(template):
 
 def get_constant_value(declare_const):
     """
-    :declare_const: DeclareConst statement specifiying the random constant
+    :declare_const: DeclareConst statement specifying the random constant
     :returns: expression for random constant
     """
     const_type = declare_const.sort
diff --git a/yinyang/src/mutators/SemanticFusion/__init__.py b/yinyang/src/mutators/SemanticFusion/__init__.py
new file mode 100644
index 0000000..e69de29
diff --git a/src/mutators/TypeAwareOpMutation.py b/yinyang/src/mutators/TypeAwareOpMutation.py
similarity index 98%
rename from src/mutators/TypeAwareOpMutation.py
rename to yinyang/src/mutators/TypeAwareOpMutation.py
index 8669b12..5787d02 100644
--- a/src/mutators/TypeAwareOpMutation.py
+++ b/yinyang/src/mutators/TypeAwareOpMutation.py
@@ -22,7 +22,7 @@
 
 import random
 
-from src.mutators.Mutator import Mutator
+from yinyang.src.mutators.Mutator import Mutator
 
 
 class TypeAwareOpMutation(Mutator):
diff --git a/yinyang/src/mutators/__init__.py b/yinyang/src/mutators/__init__.py
new file mode 100644
index 0000000..e69de29
diff --git a/src/parsing/Ast.py b/yinyang/src/parsing/Ast.py
similarity index 100%
rename from src/parsing/Ast.py
rename to yinyang/src/parsing/Ast.py
diff --git a/src/parsing/AstVisitor.py b/yinyang/src/parsing/AstVisitor.py
similarity index 98%
rename from src/parsing/AstVisitor.py
rename to yinyang/src/parsing/AstVisitor.py
index 21349e4..1db66b0 100644
--- a/src/parsing/AstVisitor.py
+++ b/yinyang/src/parsing/AstVisitor.py
@@ -20,9 +20,9 @@
 # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 # SOFTWARE.
 
-from src.parsing.SMTLIBv2Parser import SMTLIBv2Parser
-from src.parsing.SMTLIBv2Visitor import SMTLIBv2Visitor
-from src.parsing.Ast import (
+from yinyang.src.parsing.SMTLIBv2Parser import SMTLIBv2Parser
+from yinyang.src.parsing.SMTLIBv2Visitor import SMTLIBv2Visitor
+from yinyang.src.parsing.Ast import (
     Var,
     Const,
     Expr,
@@ -52,7 +52,7 @@
     FunDecl,
     SMTLIBCommand,
 )
-from src.parsing.Types import (
+from yinyang.src.parsing.Types import (
     BITVECTOR_TYPE,
     INTEGER_TYPE,
     REAL_TYPE,
diff --git a/src/parsing/Parse.py b/yinyang/src/parsing/Parse.py
similarity index 95%
rename from src/parsing/Parse.py
rename to yinyang/src/parsing/Parse.py
index 8145065..d0318ec 100644
--- a/src/parsing/Parse.py
+++ b/yinyang/src/parsing/Parse.py
@@ -26,10 +26,10 @@
 
 from antlr4.error.ErrorListener import ErrorListener
 
-from src.parsing.SMTLIBv2Lexer import SMTLIBv2Lexer
-from src.parsing.SMTLIBv2Parser import SMTLIBv2Parser
-from src.parsing.TimeoutDecorator import exit_after
-from src.parsing.AstVisitor import AstVisitor
+from yinyang.src.parsing.SMTLIBv2Lexer import SMTLIBv2Lexer
+from yinyang.src.parsing.SMTLIBv2Parser import SMTLIBv2Parser
+from yinyang.src.parsing.TimeoutDecorator import exit_after
+from yinyang.src.parsing.AstVisitor import AstVisitor
 
 from antlr4.CommonTokenStream import CommonTokenStream
 from antlr4.FileStream import FileStream
@@ -103,7 +103,7 @@ def generate_ast(stream, prep_seed=True):
     vis = AstVisitor()
     formula = vis.visitStart(tree)
 
-    # empty file or parser preceding parser errror
+    # empty file or parser preceding parser error
     if len(formula.commands) == 0:
         return None
 
diff --git a/src/parsing/SMTLIBv2.g4 b/yinyang/src/parsing/SMTLIBv2.g4
similarity index 100%
rename from src/parsing/SMTLIBv2.g4
rename to yinyang/src/parsing/SMTLIBv2.g4
diff --git a/src/parsing/SMTLIBv2.interp b/yinyang/src/parsing/SMTLIBv2.interp
similarity index 100%
rename from src/parsing/SMTLIBv2.interp
rename to yinyang/src/parsing/SMTLIBv2.interp
diff --git a/src/parsing/SMTLIBv2.tokens b/yinyang/src/parsing/SMTLIBv2.tokens
similarity index 100%
rename from src/parsing/SMTLIBv2.tokens
rename to yinyang/src/parsing/SMTLIBv2.tokens
diff --git a/src/parsing/SMTLIBv2Lexer.interp b/yinyang/src/parsing/SMTLIBv2Lexer.interp
similarity index 100%
rename from src/parsing/SMTLIBv2Lexer.interp
rename to yinyang/src/parsing/SMTLIBv2Lexer.interp
diff --git a/src/parsing/SMTLIBv2Lexer.py b/yinyang/src/parsing/SMTLIBv2Lexer.py
similarity index 100%
rename from src/parsing/SMTLIBv2Lexer.py
rename to yinyang/src/parsing/SMTLIBv2Lexer.py
diff --git a/src/parsing/SMTLIBv2Lexer.tokens b/yinyang/src/parsing/SMTLIBv2Lexer.tokens
similarity index 100%
rename from src/parsing/SMTLIBv2Lexer.tokens
rename to yinyang/src/parsing/SMTLIBv2Lexer.tokens
diff --git a/src/parsing/SMTLIBv2Listener.py b/yinyang/src/parsing/SMTLIBv2Listener.py
similarity index 100%
rename from src/parsing/SMTLIBv2Listener.py
rename to yinyang/src/parsing/SMTLIBv2Listener.py
diff --git a/src/parsing/SMTLIBv2Parser.py b/yinyang/src/parsing/SMTLIBv2Parser.py
similarity index 100%
rename from src/parsing/SMTLIBv2Parser.py
rename to yinyang/src/parsing/SMTLIBv2Parser.py
diff --git a/src/parsing/SMTLIBv2Visitor.py b/yinyang/src/parsing/SMTLIBv2Visitor.py
similarity index 99%
rename from src/parsing/SMTLIBv2Visitor.py
rename to yinyang/src/parsing/SMTLIBv2Visitor.py
index c8df08c..4c82c3c 100644
--- a/src/parsing/SMTLIBv2Visitor.py
+++ b/yinyang/src/parsing/SMTLIBv2Visitor.py
@@ -22,8 +22,8 @@
 
 # Generated from SMTLIBv2.g4 by ANTLR 4.8
 from antlr4 import *
-from src.parsing.Ast import *
-from src.parsing.SMTLIBv2Parser import SMTLIBv2Parser
+from yinyang.src.parsing.Ast import *
+from yinyang.src.parsing.SMTLIBv2Parser import SMTLIBv2Parser
 
 # This class defines a complete generic visitor for a parse tree produced by SMTLIBv2Parser.
 class SMTLIBv2Visitor(ParseTreeVisitor):
diff --git a/src/parsing/TimeoutDecorator.py b/yinyang/src/parsing/TimeoutDecorator.py
similarity index 100%
rename from src/parsing/TimeoutDecorator.py
rename to yinyang/src/parsing/TimeoutDecorator.py
diff --git a/src/parsing/Typechecker.py b/yinyang/src/parsing/Typechecker.py
similarity index 99%
rename from src/parsing/Typechecker.py
rename to yinyang/src/parsing/Typechecker.py
index 8c28be4..2710c5b 100644
--- a/src/parsing/Typechecker.py
+++ b/yinyang/src/parsing/Typechecker.py
@@ -24,7 +24,7 @@
 
 sys.setrecursionlimit(100000)
 
-from src.parsing.Types import (
+from yinyang.src.parsing.Types import (
     sort2type,
     # Types
     BOOLEAN_TYPE, REAL_TYPE, INTEGER_TYPE, ROUNDINGMODE_TYPE, STRING_TYPE,
@@ -49,7 +49,7 @@
     FP_LT, FP_GEQ, FP_GT, FP_EQ, FP_MIN, FP_MAX, FP_FMA, TO_FP_UNSIGNED, TO_FP
 )
 
-from src.parsing.Ast import Assert
+from yinyang.src.parsing.Ast import Assert
 
 
 class Context:
diff --git a/src/parsing/Types.py b/yinyang/src/parsing/Types.py
similarity index 100%
rename from src/parsing/Types.py
rename to yinyang/src/parsing/Types.py
diff --git a/src/parsing/__init__.py b/yinyang/src/parsing/__init__.py
similarity index 100%
rename from src/parsing/__init__.py
rename to yinyang/src/parsing/__init__.py
diff --git a/src/parsing/antlr-4.9.2-complete.jar b/yinyang/src/parsing/antlr-4.9.2-complete.jar
old mode 100755
new mode 100644
similarity index 100%
rename from src/parsing/antlr-4.9.2-complete.jar
rename to yinyang/src/parsing/antlr-4.9.2-complete.jar
diff --git a/src/parsing/regenerate_grammar.sh b/yinyang/src/parsing/regenerate_grammar.sh
old mode 100755
new mode 100644
similarity index 100%
rename from src/parsing/regenerate_grammar.sh
rename to yinyang/src/parsing/regenerate_grammar.sh


Test patch:
diff --git a/tests/integration/detection/TestDetection.py b/tests/integration/detection/TestDetection.py
index ffaaec6..a6257c4 100644
--- a/tests/integration/detection/TestDetection.py
+++ b/tests/integration/detection/TestDetection.py
@@ -205,7 +205,7 @@ def test_timeout():
     )
     log = open(newest_log("logs")).read()
 
-    if log.count("Solver timeout occured.") != 1:
+    if log.count("Solver timeout occurred.") != 1:
         print("[ERROR] Timeout undetected.")
         print(cmd)
         exit(1)
@@ -336,7 +336,7 @@ def test_duplicate_list():
 
 ignore_list = [
     "(error ",
-    "unsupport",
+    "unsupported",
     "unexpected char",
     "failed to open file",
     "Expected result sat but got unsat",
@@ -349,8 +349,8 @@ def test_duplicate_list():
 ]
 
 """
-    os.system("mv config/config.py config/config.py.orig")
-    with open("config/Config.py", "w") as f:
+    os.system("mv yinyang/config/config.py yinyang/config/config.py.orig")
+    with open("yinyang/config/Config.py", "w") as f:
         f.write(config_py)
     create_mocksolver_msg(msg, solver)
     first_config = os.path.abspath(solver)
@@ -364,7 +364,7 @@ def test_duplicate_list():
         exit(1)
     else:
         os.system("rm -rf " + solver)
-    os.system("mv config/config.py.orig config/config.py")
+    os.system("mv yinyang/config/config.py.orig yinyang/config/config.py")
 
 
 if __name__ == "__main__":
diff --git a/tests/integration/misc/pypi.sh b/tests/integration/misc/pypi.sh
new file mode 100755
index 0000000..f38a0e6
--- /dev/null
+++ b/tests/integration/misc/pypi.sh
@@ -0,0 +1,48 @@
+#! /bin/bash
+
+if ! pip uninstall -y antlr4-python3-runtime; then
+    exit 1
+fi
+
+if ! pip install yinyang; then 
+    exit 1
+fi
+
+yinyang
+
+if [ $? -ne 2 ]; then
+    exit 1
+fi
+
+opfuzz 
+
+if [ $? -ne 2 ]; then
+    exit 1
+fi
+
+typefuzz 
+
+if [ $? -ne 2 ]; then
+    exit 1
+fi
+
+sudo apt-get install -y cvc4 z3
+
+cd ..
+yinyang -o sat "z3 model_validate=true;cvc4 --check-models -m -i -q" yinyang/examples/phi1.smt2 yinyang/examples/phi2.smt2
+
+if [ $? -eq 3 ]; then
+    exit 1
+fi
+
+opfuzz "z3 model_validate=true;cvc4 --check-models -m -i -q" yinyang/examples/phi1.smt2
+
+if [ $? -eq 3 ]; then
+    exit 1
+fi
+
+typefuzz "z3 model_validate=true;cvc4 --check-models -m -i -q" yinyang/examples/phi1.smt2
+
+if [ $? -eq 3 ]; then
+    exit 1
+fi
diff --git a/tests/integration/parsing/ast/Ast.py b/tests/integration/parsing/ast/Ast.py
index 61771bc..38ad757 100755
--- a/tests/integration/parsing/ast/Ast.py
+++ b/tests/integration/parsing/ast/Ast.py
@@ -24,10 +24,10 @@
 
 from antlr4.CommonTokenStream import FileStream, CommonTokenStream
 
-from src.parsing.SMTLIBv2Lexer import SMTLIBv2Lexer
-from src.parsing.SMTLIBv2Parser import SMTLIBv2Parser
-from src.parsing.AstVisitor import AstVisitor
-from src.parsing.Parse import parse_file
+from yinyang.src.parsing.SMTLIBv2Lexer import SMTLIBv2Lexer
+from yinyang.src.parsing.SMTLIBv2Parser import SMTLIBv2Parser
+from yinyang.src.parsing.AstVisitor import AstVisitor
+from yinyang.src.parsing.Parse import parse_file
 
 sys.setrecursionlimit(100000)
 sys.path.append("../../../../")
diff --git a/tests/integration/parsing/ast/CheckOutput.py b/tests/integration/parsing/ast/CheckOutput.py
index 73f742b..ca6b1d0 100755
--- a/tests/integration/parsing/ast/CheckOutput.py
+++ b/tests/integration/parsing/ast/CheckOutput.py
@@ -30,9 +30,9 @@
 
 from antlr4.CommonTokenStream import FileStream, CommonTokenStream
 
-from src.parsing.SMTLIBv2Lexer import SMTLIBv2Lexer
-from src.parsing.SMTLIBv2Parser import SMTLIBv2Parser
-from src.parsing.AstVisitor import AstVisitor
+from yinyang.src.parsing.SMTLIBv2Lexer import SMTLIBv2Lexer
+from yinyang.src.parsing.SMTLIBv2Parser import SMTLIBv2Parser
+from yinyang.src.parsing.AstVisitor import AstVisitor
 
 
 sys.setrecursionlimit(100000)
diff --git a/tests/integration/parsing/parser/Parse.py b/tests/integration/parsing/parser/Parse.py
index c4448fe..8c8a827 100755
--- a/tests/integration/parsing/parser/Parse.py
+++ b/tests/integration/parsing/parser/Parse.py
@@ -23,8 +23,8 @@
 import sys
 
 from antlr4.CommonTokenStream import CommonTokenStream, FileStream
-from src.parsing.SMTLIBv2Lexer import SMTLIBv2Lexer
-from src.parsing.SMTLIBv2Parser import SMTLIBv2Parser
+from yinyang.src.parsing.SMTLIBv2Lexer import SMTLIBv2Lexer
+from yinyang.src.parsing.SMTLIBv2Parser import SMTLIBv2Parser
 
 sys.setrecursionlimit(100000)
 sys.path.append("../../")
diff --git a/tests/integration/parsing/parser/Run.py b/tests/integration/parsing/parser/Run.py
index b0ad258..c4af77b 100755
--- a/tests/integration/parsing/parser/Run.py
+++ b/tests/integration/parsing/parser/Run.py
@@ -38,7 +38,7 @@ def do_parsing(fn):
     cmd = "timeout -s 9 1 python3.7 parse.py " + fn + ";echo $?"
     out = sp.getoutput(cmd)
 
-    # To supress debug related issues
+    # To suppress debug related issues
     if "dbg" in out:
         return 0
 
diff --git a/tests/unit/TestGenTypeAwareMutation.py b/tests/unit/TestGenTypeAwareMutation.py
index bbeecb1..2175ada 100644
--- a/tests/unit/TestGenTypeAwareMutation.py
+++ b/tests/unit/TestGenTypeAwareMutation.py
@@ -26,15 +26,15 @@
 sys.path.append("../../")
 import os
 
-from src.parsing.Parse import *
-from src.parsing.Typechecker import Context, typecheck
-from src.mutators.GenTypeAwareMutation.GenTypeAwareMutation import *
-from src.mutators.GenTypeAwareMutation.Util import *
+from yinyang.src.parsing.Parse import *
+from yinyang.src.parsing.Typechecker import Context, typecheck
+from yinyang.src.mutators.GenTypeAwareMutation.GenTypeAwareMutation import *
+from yinyang.src.mutators.GenTypeAwareMutation.Util import *
 
 
 class Mockargs:
     modulo = 3
-    config = "config/generalization.txt"
+    config = "yinyang/config/typefuzz_config.txt"
 
 
 class GenTypeAwareMutationTestCase(unittest.TestCase):
diff --git a/tests/unit/TestLocalVariables.py b/tests/unit/TestLocalVariables.py
index 1cb70e4..dedfd90 100644
--- a/tests/unit/TestLocalVariables.py
+++ b/tests/unit/TestLocalVariables.py
@@ -26,16 +26,16 @@
 
 sys.path.append("../../")
 
-from src.parsing.parse import *
-from src.parsing.typechecker import Context, typecheck
-from src.generators.TypeAwareOpMutation import TypeAwareOpMutation
-from src.generators.GenTypeAwareMutation.GenTypeAwareMutation import *
-from src.generators.GenTypeAwareMutation.Util import *
+from yinyang.src.parsing.parse import *
+from yinyang.src.parsing.typechecker import Context, typecheck
+from yinyang.src.generators.TypeAwareOpMutation import TypeAwareOpMutation
+from yinyang.src.generators.GenTypeAwareMutation.GenTypeAwareMutation import *
+from yinyang.src.generators.GenTypeAwareMutation.Util import *
 
 
 class Mockargs:
     modulo = 3
-    config_file = "config/generalization.txt"
+    config_file = "yinyang/config/generalization.txt"
 
 
 class LocalVariableMutationTestCase(unittest.TestCase):
diff --git a/tests/unit/TestParsing.py b/tests/unit/TestParsing.py
index 3f46ce6..c9f8736 100644
--- a/tests/unit/TestParsing.py
+++ b/tests/unit/TestParsing.py
@@ -23,7 +23,7 @@
 import unittest
 import sys
 
-from src.parsing.Parse import parse_str, parse_file
+from yinyang.src.parsing.Parse import parse_str, parse_file
 
 sys.path.append("../../")
 
diff --git a/tests/unit/TestSemanticFusion.py b/tests/unit/TestSemanticFusion.py
index 6347a54..17fe102 100644
--- a/tests/unit/TestSemanticFusion.py
+++ b/tests/unit/TestSemanticFusion.py
@@ -23,8 +23,8 @@
 import sys
 import unittest
 
-from src.parsing.Parse import parse_file
-from src.mutators.SemanticFusion.SemanticFusion import SemanticFusion
+from yinyang.src.parsing.Parse import parse_file
+from yinyang.src.mutators.SemanticFusion.SemanticFusion import SemanticFusion
 
 sys.path.append("../../")
 
diff --git a/tests/unit/TestTerm.py b/tests/unit/TestTerm.py
index 3d3b64f..fb35c0d 100644
--- a/tests/unit/TestTerm.py
+++ b/tests/unit/TestTerm.py
@@ -23,8 +23,8 @@
 import sys
 import unittest
 
-from src.parsing.Parse import parse_str
-from src.parsing.Ast import Const, Var, Expr
+from yinyang.src.parsing.Parse import parse_str
+from yinyang.src.parsing.Ast import Const, Var, Expr
 
 sys.path.append("../../")
 
diff --git a/tests/unit/TestTypeAwareOpMutation.py b/tests/unit/TestTypeAwareOpMutation.py
index b919206..3b0d626 100644
--- a/tests/unit/TestTypeAwareOpMutation.py
+++ b/tests/unit/TestTypeAwareOpMutation.py
@@ -23,8 +23,8 @@
 import sys
 import unittest
 
-from src.parsing.Parse import parse_str, parse_file
-from src.mutators.TypeAwareOpMutation import TypeAwareOpMutation
+from yinyang.src.parsing.Parse import parse_str, parse_file
+from yinyang.src.mutators.TypeAwareOpMutation import TypeAwareOpMutation
 
 sys.path.append("../../")
 
diff --git a/tests/unit/TestTypechecker.py b/tests/unit/TestTypechecker.py
index b0cba0f..41ae015 100644
--- a/tests/unit/TestTypechecker.py
+++ b/tests/unit/TestTypechecker.py
@@ -26,21 +26,21 @@
 
 sys.path.append("../../")
 
-from src.parsing.Ast import (
+from yinyang.src.parsing.Ast import (
     Assert,
 )
-from src.parsing.Parse import (
+from yinyang.src.parsing.Parse import (
     parse_str, parse_file
 )
 
-from src.parsing.Types import (
+from yinyang.src.parsing.Types import (
     UNKNOWN,
     BOOLEAN_TYPE,
     INTEGER_TYPE,
     STRING_TYPE,
 )
 
-from src.parsing.Typechecker import Context, typecheck_expr, typecheck
+from yinyang.src.parsing.Typechecker import Context, typecheck_expr, typecheck
 
 
 def check_type(expr):