## Operators
#### Autoformalize 
Translate a natural language problem into SMT-LIB language via GPT4.

Run the following command line:
```
python data_gen.py --api_id 1,2,3,4,5,6,7,8,9,10,11,12,13 --data train --num_retrive 8 \
    --index 0-7473 --type autoformalization --overwrite 1 --save_iter 1 --ref_iter 0
```

#### Informalize
Translate a SMT-LIB problem back to natural language via GPT4.

Run the following command line:
```
python data_gen.py --api_id 1,2,3,4,5,6,7,8,9,10,11,12,13 --data train --num_retrive 8 \
    --index 0-7473 --type mutation --overwrite 1 --save_iter 1 --informal_prompt 'math-word'
```
where `informal_prompt` refers to the prompt used in informalization.

#### Mutate 
Change the original calculations or add new calculations for given SMT-LIB problem.

Run the following command line:
```
python data_gen.py --api_id 1,2,3,4,5,6,7,8,9,10,11,12,13 --data train --num_retrive 8 \
    --index 0-1000 --type mutation --overwrite 1 --save_iter 15 --ref_iter 5 \
    --mutation_type 'mcmc' --remove_aux 1 --allow_real 0 --simplify 1 --comment 1 --rename 1
```
where 
- `mutation_type` indicates the method to mutate the formulations
- `remove_aux` indicates whether to remove auxillary variables after mutation
- `allow_real` indicates whether to use real type try again if the mutation failed; 
- `simplify` indicates whether to simplify the smt-lib formulation; 
- `comment` indicates whether to add comments between formulation; 
- `rename` indicates that whether change variable names to like `x_1, x_2, ...`;
#### Refresh 
Normalize the form of the given SMT-LIB problem.

Run the following command line: TBD

#### Solve 
Call LLM to solve the given natural language problem.

Run the following command line:
python data_gen.py --api_id 1,2,3,4,5,6,7,8,9,10,11,12,13 --data train --num_retrive 8 \
    --index 0-7473 --type solution --overwrite 1 --save_iter 0
    --ref_iter 1


#### General arguements
- `api_id` refers to the api number used in operations;
- `data` refers to the (train/test) dataset used;
- `index` refers to the sample index used in the dataset;
- `num_retrive` refers to the examples used in in-context learning;
- `overwrite` refers to whether covering the existing results;
- `ref_iter` refers to that the `generation_{ref_iter}` natural language problem will be used in autoformalization; 
- `save_iter` refers to that formalized results will be saved as the `generation_{save_iter}`;

Our features
- We support Sympy to solve some non-linear problem.


TODO