INSTRUCTION

1.  to compile the executable, type "make" in src/ directory, 
    the default path of the executable is bin/slender
    (slender is an older name of slent)

2. add following lines in your ~/.bashrc 

    LD_LIBRARY_PATH="< the absolute path of the "bin" directory in your clone >/lib"
    LD_LIBRARY_PATH="< the absolute path of the "bin" directory in your clone >/z3-z3-4.4.1.0/build":$LD_LIBRARY_PATH
    export LD_LIBRARY_PATH
    PATH="< the absolute path of the "bin" directory in your clone >/z3-z3-4.4.1.0/build/":$PATH
    export PATH

3. Install ic3ia on your machine, and move the binary to the path "slent/bin/ic3ia/build/"
   Also, download and compile abc70930 under the path "slent/bin"

4. SLENT (and other solvers to compare with SLENT) can be executed with script.py
   type "python script.py -h" and you can see help information below
================================================================
    benchmark_option: -l=lan_rep -s=str_rep -k=kaluza 
    
    remove intermediate files: clear < benchmark_option >

    solve         : solve  < benchmark_option >
                           < -slent | -cvc4 | -z3 | -s3p | -ABC | -norn | -trau | -all >
                           [ time out (default=20.0s) ]

    single file   : single < folder_path > 
                           < -slent | -cvc4 | -z3 | -s3p | -ABC | -norn | -trau | -all >
                           [ time out (default=20.0s) ]
    
    for command "single", please enter a path of a folder containing only one laut file
              
================================================================

   To run SLENT on one specific instance, for example, use SLENT to solve the instance benchmark/laut/lan_rep/100 under 20 sec. timeout, one can use the following command.
   $ python script.py single benchmark/laut/lan_rep/100 -slent 20

   To run SLENT with the kaluza benchmark with 20 sec. timeout, one can use the following command.
   $ python script.py solve -k -slent 20

   Solvers to be compared with SLENT can be put under the path  "slent/bin" and set in script.py line 37, 46, 55
   One may also need to update script.py to parse the result of other solvers. Check line 373 and line 416-548 in script.py for reference.
   (Solvers listed in the help information are those compared in the experiment in the paper. To run the experiment with script.py, one should download and set the binaries by themself)

   If other solvers are setup, to run one of the solver with a set of benchmark or a single instance, one can simply modify the above commands.
   To run experiments with the kaluza benchmarks with "all the solvers" under 20 sec. timeout, one can apply the following command:
   $ python script.py solve -k -all 20 

   After solving a set of testcases with one or all the solvers, the experiment results of each solver can be found at ./exp/<name of the set of testcases>/<solver name>.csv
   For the result of solving single instance, the result can be found at <path to the instance>/<solver name>.csv

   To clear up all the intermediate files generated by SLENT in a set of instances, take kaluza benchmark for example, one can apply the following command
   $ python script.py clear -k

5. New set of benchmark can be added to the path "slent/benchmark/laut"
   Each instance should be a folder containing input files for different solvers
   Each set of testcases should be a folder containing instance(s)
   To set new benchmark, one should also add the corresponding path into script.py line 27

6. Search "concat", "Concat" and "CONCAT" through all the codes in src/ (aut.cpp, autMgr.cpp, ...) to see what is required to add an operation to SLENT.
   Operations are mainly implemented in src/aut.cpp, while it is necessary to register each operation in some other files like autMgr.cpp