Merge branch 'main' of https://github.com/JetBrains-Research/verified…

…-cogen

.github/workflows/test-pytest.yml

@@ -0,0 +1,38 @@
+name: Run pytest
+
+on: [push]
+
+env:
+  PYTHON_VERSION: "3.11"
+  POETRY_VERSION: "1.8.3"
+  POETRY_URL: https://install.python-poetry.org
+
+jobs:
+  run-pytest:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+      - name: Set up Python ${{ env.PYTHON_VERSION }}
+        uses: actions/setup-python@v5
+        with:
+          python-version: ${{ env.PYTHON_VERSION }}
+        id: setup_python
+      - name: Cache Poetry cache
+        uses: actions/cache@v4
+        with:
+          path: ~/.cache/pypoetry
+          key: poetry-cache-${{ runner.os }}-${{ steps.setup_python.outputs.python-version }}-${{ env.POETRY_VERSION }}
+      - name: Cache Packages
+        uses: actions/cache@v4
+        with:
+          path: ~/.local
+          key: poetry-local-${{ runner.os }}-${{ steps.setup_python.outputs.python-version }}-${{ hashFiles('**/poetry.lock') }}-${{ hashFiles('.github/workflows/*.yml') }}
+      - name: Install Poetry ${{ env.POETRY_VERSION }}
+        run: |
+          curl -sSL ${{ env.POETRY_URL }} | python - --version ${{ env.POETRY_VERSION }}
+          echo "$HOME/.local/bin" >> $GITHUB_PATH
+      - name: Install Dependencies
+        run: poetry install
+      - name: Run pytest
+        run: poetry run pytest

.gitignore

@@ -5,7 +5,7 @@ llm-generated
 .envrc
 **/.DS_Store
 pyrightconfig.json
-**/DafnyBench/
+benches/DafnyBench/
 break_assert.rs
 .venv
 **/target

benches/HumanEvalPrompts/Strongest_Extension.prompt

@@ -0,0 +1,16 @@
+You will be given the name of a class (a string) and a list of extensions.
+The extensions are to be used to load additional classes to the class. The
+strength of the extension is as follows: Let CAP be the number of the uppercase
+letters in the extension's name, and let SM be the number of lowercase letters 
+in the extension's name, the strength is given by the fraction CAP - SM. 
+You should find the strongest extension and return a string in this 
+format: ClassName.StrongestExtensionName.
+If there are two or more extensions with the same strength, you should
+choose the one that comes first in the list.
+For example, if you are given "Slices" as the class and a list of the
+extensions: ['SErviNGSliCes', 'Cheese', 'StuFfed'] then you should
+return 'Slices.SErviNGSliCes' since 'SErviNGSliCes' is the strongest extension 
+(its strength is -1).
+Example:
+for Strongest_Extension('my_class', ['AA', 'Be', 'CC']) == 'my_class.AA'
+

benches/HumanEvalPrompts/add.prompt

@@ -0,0 +1,6 @@
+Given a non-empty list of integers lst. add the even elements that are at odd indices..
+
+
+Examples:
+    add([4, 2, 6, 7]) ==> 2 
+

benches/HumanEvalPrompts/add_elements.prompt

@@ -0,0 +1,13 @@
+
+Given a non-empty array of integers arr and an integer k, return
+the sum of the elements with at most two digits from the first k elements of arr.
+
+Example:
+
+    Input: arr = [111,21,3,4000,5,6,7,8,9], k = 4
+    Output: 24 # sum of 21 + 3
+
+Constraints:
+    1. 1 <= len(arr) <= 100
+    2. 1 <= k <= len(arr)
+

benches/HumanEvalPrompts/all_prefixes.prompt

@@ -0,0 +1,4 @@
+ Return list of all prefixes from shortest to longest of the input string
+>>> all_prefixes('abc')
+['a', 'ab', 'abc']
+

benches/HumanEvalPrompts/anti_shuffle.prompt

@@ -0,0 +1,12 @@
+
+Write a function that takes a string and returns an ordered version of it.
+Ordered version of string, is a string where all words (separated by space)
+are replaced by a new word where all the characters arranged in
+ascending order based on ascii value.
+Note: You should keep the order of words and blank spaces in the sentence.
+
+For example:
+anti_shuffle('Hi') returns 'Hi'
+anti_shuffle('hello') returns 'ehllo'
+anti_shuffle('Hello World!!!') returns 'Hello !!!Wdlor'
+

benches/HumanEvalPrompts/any_int.prompt

@@ -0,0 +1,17 @@
+
+Create a function that takes 3 numbers.
+Returns true if one of the numbers is equal to the sum of the other two, and all numbers are integers.
+Returns false in any other cases.
+
+Examples
+any_int(5, 2, 7) ➞ True
+
+any_int(3, 2, 2) ➞ False
+
+any_int(3, -2, 1) ➞ True
+
+any_int(3.6, -2.2, 2) ➞ False
+
+
+
+

benches/HumanEvalPrompts/below_threshold.prompt

@@ -0,0 +1,6 @@
+Return True if all numbers in the list l are below threshold t.
+>>> below_threshold([1, 2, 4, 10], 100)
+True
+>>> below_threshold([1, 20, 4, 10], 5)
+False
+

benches/HumanEvalPrompts/below_zero.prompt

@@ -0,0 +1,8 @@
+ You're given a list of deposit and withdrawal operations on a bank account that starts with
+zero balance. Your task is to detect if at any point the balance of account fallls below zero, and
+at that point function should return True. Otherwise it should return False.
+>>> below_zero([1, 2, 3])
+False
+>>> below_zero([1, 2, -4, 5])
+True
+

benches/HumanEvalPrompts/bf.prompt

@@ -0,0 +1,15 @@
+
+There are eight planets in our solar system: the closerst to the Sun 
+is Mercury, the next one is Venus, then Earth, Mars, Jupiter, Saturn, 
+Uranus, Neptune.
+Write a function that takes two planet names as strings planet1 and planet2. 
+The function should return a tuple containing all planets whose orbits are 
+located between the orbit of planet1 and the orbit of planet2, sorted by 
+the proximity to the sun. 
+The function should return an empty tuple if planet1 or planet2
+are not correct planet names. 
+Examples
+bf("Jupiter", "Neptune") ==> ("Saturn", "Uranus")
+bf("Earth", "Mercury") ==> ("Venus")
+bf("Mercury", "Uranus") ==> ("Venus", "Earth", "Mars", "Jupiter", "Saturn")
+

benches/HumanEvalPrompts/by_length.prompt

@@ -0,0 +1,21 @@
+
+Given an array of integers, sort the integers that are between 1 and 9 inclusive,
+reverse the resulting array, and then replace each digit by its corresponding name from
+"One", "Two", "Three", "Four", "Five", "Six", "Seven", "Eight", "Nine".
+
+For example:
+  arr = [2, 1, 1, 4, 5, 8, 2, 3]   
+        -> sort arr -> [1, 1, 2, 2, 3, 4, 5, 8] 
+        -> reverse arr -> [8, 5, 4, 3, 2, 2, 1, 1]
+  return ["Eight", "Five", "Four", "Three", "Two", "Two", "One", "One"]
+
+  If the array is empty, return an empty array:
+  arr = []
+  return []
+
+  If the array has any strange number ignore it:
+  arr = [1, -1 , 55] 
+        -> sort arr -> [-1, 1, 55]
+        -> reverse arr -> [55, 1, -1]
+  return = ['One']
+

benches/HumanEvalPrompts/can_arrange.prompt

@@ -0,0 +1,9 @@
+Create a function which returns the largest index of an element which
+is not greater than or equal to the element immediately preceding it. If
+no such element exists then return -1. The given array will not contain
+duplicate values.
+
+Examples:
+can_arrange([1,2,4,3,5]) = 3
+can_arrange([1,2,3]) = -1
+

benches/HumanEvalPrompts/car_race_collision.prompt

@@ -0,0 +1,11 @@
+
+Imagine a road that's a perfectly straight infinitely long line.
+n cars are driving left to right;  simultaneously, a different set of n cars
+are driving right to left.   The two sets of cars start out being very far from
+each other.  All cars move in the same speed.  Two cars are said to collide
+when a car that's moving left to right hits a car that's moving right to left.
+However, the cars are infinitely sturdy and strong; as a result, they continue moving
+in their trajectory as if they did not collide.
+
+This function outputs the number of such collisions.
+

benches/HumanEvalPrompts/change_base.prompt

@@ -0,0 +1,10 @@
+Change numerical base of input number x to base.
+return string representation after the conversion.
+base numbers are less than 10.
+>>> change_base(8, 3)
+'22'
+>>> change_base(8, 2)
+'1000'
+>>> change_base(7, 2)
+'111'
+

benches/HumanEvalPrompts/check_dict_case.prompt

@@ -0,0 +1,11 @@
+
+Given a dictionary, return True if all keys are strings in lower 
+case or all keys are strings in upper case, else return False.
+The function should return False is the given dictionary is empty.
+Examples:
+check_dict_case({"a":"apple", "b":"banana"}) should return True.
+check_dict_case({"a":"apple", "A":"banana", "B":"banana"}) should return False.
+check_dict_case({"a":"apple", 8:"banana", "a":"apple"}) should return False.
+check_dict_case({"Name":"John", "Age":"36", "City":"Houston"}) should return False.
+check_dict_case({"STATE":"NC", "ZIP":"12345" }) should return True.
+

benches/HumanEvalPrompts/check_if_last_char_is_a_letter.prompt

@@ -0,0 +1,12 @@
+
+Create a function that returns True if the last character
+of a given string is an alphabetical character and is not
+a part of a word, and False otherwise.
+Note: "word" is a group of characters separated by space.
+
+Examples:
+check_if_last_char_is_a_letter("apple pie") ➞ False
+check_if_last_char_is_a_letter("apple pi e") ➞ True
+check_if_last_char_is_a_letter("apple pi e ") ➞ False
+check_if_last_char_is_a_letter("") ➞ False 
+

benches/HumanEvalPrompts/choose_num.prompt

@@ -0,0 +1,8 @@
+This function takes two positive numbers x and y and returns the
+biggest even integer number that is in the range [x, y] inclusive. If 
+there's no such number, then the function should return -1.
+
+For example:
+choose_num(12, 15) = 14
+choose_num(13, 12) = -1
+

benches/HumanEvalPrompts/circular_shift.prompt

@@ -0,0 +1,8 @@
+Circular shift the digits of the integer x, shift the digits right by shift
+and return the result as a string.
+If shift > number of digits, return digits reversed.
+>>> circular_shift(12, 1)
+"21"
+>>> circular_shift(12, 2)
+"12"
+

benches/HumanEvalPrompts/closest_integer.prompt

@@ -0,0 +1,17 @@
+
+Create a function that takes a value (string) representing a number
+and returns the closest integer to it. If the number is equidistant
+from two integers, round it away from zero.
+
+Examples
+>>> closest_integer("10")
+10
+>>> closest_integer("15.3")
+15
+
+Note:
+Rounding away from zero means that if the given number is equidistant
+from two integers, the one you should return is the one that is the
+farthest from zero. For example closest_integer("14.5") should
+return 15 and closest_integer("-14.5") should return -15.
+

benches/HumanEvalPrompts/common.prompt

@@ -0,0 +1,7 @@
+Return sorted unique common elements for two lists.
+>>> common([1, 4, 3, 34, 653, 2, 5], [5, 7, 1, 5, 9, 653, 121])
+[1, 5, 653]
+>>> common([5, 3, 2, 8], [3, 2])
+[2, 3]
+
+

benches/HumanEvalPrompts/compare.prompt

@@ -0,0 +1,14 @@
+I think we all remember that feeling when the result of some long-awaited
+event is finally known. The feelings and thoughts you have at that moment are
+definitely worth noting down and comparing.
+Your task is to determine if a person correctly guessed the results of a number of matches.
+You are given two arrays of scores and guesses of equal length, where each index shows a match. 
+Return an array of the same length denoting how far off each guess was. If they have guessed correctly,
+the value is 0, and if not, the value is the absolute difference between the guess and the score.
+
+
+example:
+
+compare([1,2,3,4,5,1],[1,2,3,4,2,-2]) -> [0,0,0,0,3,3]
+compare([0,5,0,0,0,4],[4,1,1,0,0,-2]) -> [4,4,1,0,0,6]
+

benches/HumanEvalPrompts/compare_one.prompt

@@ -0,0 +1,11 @@
+
+Create a function that takes integers, floats, or strings representing
+real numbers, and returns the larger variable in its given variable type.
+Return None if the values are equal.
+Note: If a real number is represented as a string, the floating point might be . or ,
+
+compare_one(1, 2.5) ➞ 2.5
+compare_one(1, "2,3") ➞ "2,3"
+compare_one("5,1", "6") ➞ "6"
+compare_one("1", 1) ➞ None
+

benches/HumanEvalPrompts/concatenate.prompt

@@ -0,0 +1,6 @@
+ Concatenate list of strings into a single string
+>>> concatenate([])
+''
+>>> concatenate(['a', 'b', 'c'])
+'abc'
+

benches/HumanEvalPrompts/correct_bracketing.prompt

@@ -0,0 +1,12 @@
+ brackets is a string of "(" and ")".
+return True if every opening bracket has a corresponding closing bracket.
+
+>>> correct_bracketing("(")
+False
+>>> correct_bracketing("()")
+True
+>>> correct_bracketing("(()())")
+True
+>>> correct_bracketing(")(()")
+False
+

benches/HumanEvalPrompts/count_distinct_characters.prompt

@@ -0,0 +1,6 @@
+ Given a string, find out how many distinct characters (regardless of case) does it consist of
+>>> count_distinct_characters('xyzXYZ')
+3
+>>> count_distinct_characters('Jerry')
+4
+

benches/HumanEvalPrompts/count_nums.prompt

@@ -0,0 +1,9 @@
+
+Write a function count_nums which takes an array of integers and returns
+the number of elements which has a sum of digits > 0.
+If a number is negative, then its first signed digit will be negative:
+e.g. -123 has signed digits -1, 2, and 3.
+>>> count_nums([]) == 0
+>>> count_nums([-1, 11, -11]) == 1
+>>> count_nums([1, 1, 2]) == 3
+

benches/HumanEvalPrompts/count_up_to.prompt

@@ -0,0 +1,10 @@
+Implement a function that takes an non-negative integer and returns an array of the first n
+integers that are prime numbers and less than n.
+for example:
+count_up_to(5) => [2,3]
+count_up_to(11) => [2,3,5,7]
+count_up_to(0) => []
+count_up_to(20) => [2,3,5,7,11,13,17,19]
+count_up_to(1) => []
+count_up_to(18) => [2,3,5,7,11,13,17]
+

benches/HumanEvalPrompts/count_upper.prompt

@@ -0,0 +1,8 @@
+
+Given a string s, count the number of uppercase vowels in even indices.
+
+For example:
+count_upper('aBCdEf') returns 1
+count_upper('abcdefg') returns 0
+count_upper('dBBE') returns 0
+

benches/HumanEvalPrompts/cycpattern_check.prompt

@@ -0,0 +1,9 @@
+You are given 2 words. You need to return True if the second word or any of its rotations is a substring in the first word
+cycpattern_check("abcd","abd") => False
+cycpattern_check("hello","ell") => True
+cycpattern_check("whassup","psus") => False
+cycpattern_check("abab","baa") => True
+cycpattern_check("efef","eeff") => False
+cycpattern_check("himenss","simen") => True
+
+

benches/HumanEvalPrompts/decimal_to_binary.prompt

@@ -0,0 +1,11 @@
+You will be given a number in decimal form and your task is to convert it to
+binary format. The function should return a string, with each character representing a binary
+number. Each character in the string will be '0' or '1'.
+
+There will be an extra couple of characters 'db' at the beginning and at the end of the string.
+The extra characters are there to help with the format.
+
+Examples:
+decimal_to_binary(15)   # returns "db1111db"
+decimal_to_binary(32)   # returns "db100000db"
+

benches/HumanEvalPrompts/derivative.prompt

@@ -0,0 +1,8 @@
+ xs represent coefficients of a polynomial.
+xs[0] + xs[1] * x + xs[2] * x^2 + ....
+ Return derivative of this polynomial in the same form.
+>>> derivative([3, 1, 2, 4, 5])
+[1, 4, 12, 20]
+>>> derivative([1, 2, 3])
+[2, 6]
+