eg-cmds.txt

Please use the command to run eas trace example using `bit-vector SyGuS` encoding:

`./src/Driver.py -n 5 -r t.txt -a bv_sygus -dict -t eas-example/eas.trace`

Please use the command to run eas trace example using `ADT SyGuS` encoding:

`./src/Driver.py -n 5 -r t.txt -a adt_sygus -dict -t eas-example/eas.trace`

Please use the command to run eas trace example using `ADT SMT2` encoding:

`./src/Driver.py -n 5 -r t.txt -a fin_adt -dict -t eas-example/eas.trace`

Please use the command to run eas trace example using `SAT-encoding with enumeration` mode `on`:

`./src/Driver.py -n 5 -r t.txt -a sat_enum -dict -t eas-example/eas.trace`

Please use the command to run eas trace example using `SAT-encoding with enumeration` mode `off`:

`./src/Driver.py -s 7 -r t.txt -a sat -dict -t eas-example/eas.trace`

Please use the command to run eas trace example using `Guided SAT Enumerator enumeration` mode `on`:

`./src/Driver.py -n 5 -r t.txt -a guided_sat_enum -dict -t eas-example/eas.trace` 

Please use the command to run eas trace example using `Guided SAT Enumerator with enumeration` mode `off`:

`./src/Driver.py -s 3 -r t.txt -a guided_sat -t eas-example/eas.trace` 

The Default Solver is (Z3) but user can switch to any other solver supported by `py-smt`:

`./src/Driver.py -n 10 -r t.txt -a sat_enum -dict -t eas-example/eas.trace -solver msat`