-
Notifications
You must be signed in to change notification settings - Fork 4
/
eg-cmds.txt
31 lines (16 loc) · 1.32 KB
/
eg-cmds.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
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`