diff --git a/.gitignore b/.gitignore index 6edb45a..0bc51c2 100644 --- a/.gitignore +++ b/.gitignore @@ -18,8 +18,9 @@ run.sh **/.pytest_cache run_nagini.py /tmp -results results/* +!results/tries_HumanEval-Dafny_1.json +!results/tries_HumanEval-RustBench_1.json /log_tries/ /log_tries/* .direnv diff --git a/results/tries_HumanEval-Dafny_1.json b/results/tries_HumanEval-Dafny_1.json new file mode 100644 index 0000000..21c5734 --- /dev/null +++ b/results/tries_HumanEval-Dafny_1.json @@ -0,0 +1,113 @@ +{ + "002-truncate.dfy": 0, + "000-has_close_elements.dfy": 1, + "003-below_zero.dfy": 1, + "005-intersperse.dfy": 4, + "004-mean_absolute_derivation.dfy": 4, + "006-parse_nested_parens.dfy": 4, + "009-rolling_max.dfy": 6, + "011-string_xor.dfy": 1, + "012-longest.dfy": 5, + "013-greatest_common_divisor.dfy": 3, + "014-all_prefixes.dfy": 1, + "016-count_distinct_characters.dfy": 6, + "021-rescale_to_unit.dfy": 3, + "023-strlen.dfy": 0, + "024-largest-divisor.dfy": 1, + "025-factorize.dfy": 3, + "026-remove_duplicates.dfy": 7, + "027-flip_case.dfy": 0, + "029-filter_by_prefix.dfy": 1, + "031-is-prime.dfy": 1, + "034-unique.dfy": 6, + "035-max-element.dfy": 2, + "036-fizz_buzz.dfy": 5, + "040-triples-sum-to-zero.dfy": 3, + "041-car_race_collision.dfy": 0, + "042-incr-list.dfy": 1, + "045-triangle_area.dfy": 0, + "046-fib4.dfy": 1, + "048-is-palindrome.dfy": 3, + "049-modp.dfy": 1, + "050-encode_shift.dfy": 1, + "051-remove-vowels.dfy": 1, + "052-below-threshold.dfy": 1, + "053-add.dfy": 0, + "054-same-chars.dfy": 0, + "055-fib.dfy": 1, + "057-monotonic.dfy": 1, + "059-largest-prime-factor.dfy": 1, + "060-sum_to_n.dfy": 0, + "062-derivative.dfy": 1, + "063-fibfib.dfy": 1, + "064-vowel_count.dfy": 2, + "065-circular_shift.dfy": 1, + "066-digitSum.dfy": 4, + "068-pluck.dfy": 3, + "069-search.dfy": 1, + "072-will_it_fly.dfy": 6, + "074-total_match.dfy": 2, + "075-is_multiply_prime.dfy": 5, + "077-is_cube.dfy": 1, + "078-hex_key.dfy": 2, + "079-decimal_to_binary.dfy": 0, + "080-is_happy.dfy": 1, + "081-numerical_letter_grade.dfy": 1, + "082-prime_length.dfy": 0, + "083-starts_one_ends.dfy": 0, + "084-solve.dfy": 2, + "085-add.dfy": 2, + "088-sort_array.dfy": 2, + "089-encrypt.dfy": 1, + "092-any_int.dfy": 0, + "093-encode.dfy": 2, + "094-skjkasdkd.dfy": 5, + "096-count_up_to.dfy": 2, + "097-multiply.dfy": 0, + "098-count_upper.dfy": 3, + "100-make_a_pile.dfy": 1, + "102-choose_num.dfy": 1, + "104-unique_digits.dfy": 5, + "106-f.dfy": 1, + "108-count_nums.dfy": 2, + "110-exchange.dfy": 0, + "115-max_fill.dfy": 6, + "116-sort_array.dfy": 6, + "121-solution.dfy": 10, + "122-add_elements.dfy": 2, + "123-get_odd_collatz.dfy": 10, + "127-intersection.dfy": 0, + "128-prod_signs.dfy": 2, + "130-tri.dfy": 1, + "133-sum_squares.dfy": 2, + "134-check_if_last_char_is_a_letter.dfy": 0, + "135_can_arrange.dfy": 1, + "138_is_equal_to_sum_even.dfy": 0, + "139-special_factorial.dfy": 2, + "142-sum_squares.dfy": 6, + "145-order_by_points.dfy": 2, + "146_specialFilter.dfy": 2, + "148-bf.dfy": 0, + "150-x_or_y.dfy": 0, + "151-double_the_difference.dfy": 3, + "152-compare.dfy": 1, + "153-Strongest_Extension.dfy": 1, + "154-cycpattern_check.dfy": 1, + "157-right_angle_triangle.dfy": 0, + "158-find_max.dfy": 1, + "159-eat.dfy": 0, + "161-solve.dfy": 1, + "010-is_palindrome.dfy": 3, + "033-sort_third.dfy": 6, + "043-pairs-sum-to-zero.dfy": 1, + "058-common.dfy": 1, + "007-filter_by_substring.dfy": 8, + "076-is_simple_power.dfy": 8, + "163-generate_integers.dfy": 9, + "008-sum_product.dfy": 1, + "070-strange_sort_list.dfy": 2, + "107-even_odd_palindrome.dfy": 3, + "112-reverse_delete.dfy": 2, + "136-largest_smallest_integers.dfy": 2, + "155_even_odd_count.dfy": 4 +} \ No newline at end of file diff --git a/results/tries_HumanEval-RustBench_1.json b/results/tries_HumanEval-RustBench_1.json new file mode 100644 index 0000000..0584721 --- /dev/null +++ b/results/tries_HumanEval-RustBench_1.json @@ -0,0 +1,34 @@ +{ + "014-all_prefixes.rs": 4, + "023-strlen.rs": 0, + "035-max-element.rs": 1, + "052-below-threshold.rs": 2, + "053-add.rs": 0, + "057-monotonic.rs": 1, + "062-derivative.rs": 2, + "abs.rs": 0, + "arithmetic_weird.rs": 1, + "array_concat.rs": 1, + "array_copy.rs": 2, + "array_product.rs": 1, + "barrier.rs": 6, + "binary_search_recursive.rs": 0, + "has_close_elements.rs": 2, + "has_only_one_distinct_element.rs": 6, + "integer_square_root.rs": 8, + "intersperse.rs": 1, + "is_non_prime.rs": 2, + "is_sorted.rs": 6, + "largest_prime_factor.rs": 6, + "last_position.rs": 5, + "max_array.rs": 1, + "max_dafny_lsp.rs": 4, + "remove_element.rs": 1, + "remove_elements.rs": 9, + "replace.rs": 1, + "reverse.rs": 2, + "smallest_list_length.rs": 2, + "two_way_sort.rs": 1, + "unique.rs": 3, + "unique_better.rs": 3 +} \ No newline at end of file