updated code

README.md

@@ -123,8 +123,7 @@ python3 main.py --config-file <YAML_config_file> --max-benchmarks <max_benchmark
 If you are using a different endpoint, you will have to implement a wrapper class that inherits `Provider` in `llm_api_client.py`.
 See the `AzureOpenAI` class for an example.
 
-Currently we support running only the Llama-2 family of models locally.
-If you are using an LLM locally on your machine or your servers, you will have to download the model and set the path to the model checkpoints and tokenizer accordingly in `llama_2.py`.
+If you are hosting a model locally, you can use a local model inference/serving engine and make HTTP requests to it. You will have to set the `OPENAI_API_BASE` environment variable to the appropriate URL.
 
 ## Usage
 
@@ -141,7 +140,7 @@ The YAML configuration file contains the following fields:
 ```yaml
 checker: <checker_name> # only frama-c is supported for now
 checker_timeout: <checker_options> # timeout argument for the checker, in seconds
-model: <model_name> # the LLM to use (currently gpt-4, gpt-4-32k, gpt-3.5-turbo, codellama-34b-python are supported)
+model: <model_name> # the LLM to use (gpt-4, gpt-4-32k, gpt-3.5-turbo, etc.)
 benchmarks: <path_to_benchmarks_file> # this file must contain the list of benchmarks to run, one file path per line
 benchmark_features: <features_of_the_benchmarks> # this string should indicate the features of the benchmarks under consideration. 
                                            # For e.g., "one_loop_one_method" describes benchmarks with a single loop and a single method.
@@ -155,5 +154,12 @@ See [config/sample_config.yaml](config/sample_config.yaml) for an example of a c
 ## Dataset
 
 The dataset of pre-processed benchmarks used in our experiments is available [here](dataset.zip).
-This zip file contains benchmarks from all 4 experiments, after removing comments, and converting the assertions to ACSL assertions (for Frama-C).
+Pre-processing involves removing comments, and converting the assertions to ACSL assertions (for Frama-C).
+The ZIP file contains the following subdirectories with pre-processed benchmarks:
+
+- `loop_invariants`: Contains numerical benchmarks with one loop and one method. Loop invariants are to be inferred for these benchmarks to prove the assertion(s) in each benchmark.
+- `arrays`: Contains benchmarks with arrays, one method and at least one loop. Loop invariants are to be inferred for these benchmarks to prove the assertion(s) in each benchmark.
+- `termination`: Contains numerical benchmarks with one loop, one method. A ranking function (and supporting loop invariants if necessary) are to be inferred to prove termination of the loop.
+- `recursive_functions`: Contains benchmarks with recursive functions, for which pre-post conditions are to be inferred, to prove the assertion(s) in each benchmark.
+
 The loop invariants generated by Loopy can be found in the excel sheet [here](GeneratedInvariants.xlsx). This sheet includes the benchmarks that were successfully verified by Loopy.

src/boogie.py

@@ -58,6 +58,9 @@ def combine_llm_outputs(self, checker_input, llm_outputs, features=None):
     def extract_loop_invariants(self, code):
         raise NotImplementedError
 
+    def get_variant_expressions(self, completions):
+        raise NotImplementedError
+
 
 class BoogieChecker(Checker):
     def __init__(self, name="boogie"):