Use multiprocessing in several modes

scripts/run_several_modes.sh

@@ -0,0 +1,19 @@
+#!/bin/bash
+
+vcmd=${1:-"dafny verify --allow-warnings --verification-time-limit 10"}
+prompts_dir=${2:-"prompts/humaneval-dafny"}
+dir=${3:-"benches/HumanEval-Dafny"}
+ext=${4:-"dfy"}
+
+PYLOG_LEVEL=INFO NOFILE=1 poetry run several_modes \
+    --insert-conditions-mode=llm-single-step \
+    --llm-profile=anthropic-claude-3.5-sonnet \
+    --bench-type validating \
+    --tries 10 \
+    --runs 5 \
+    --verifier-command="dafny verify --verification-time-limit 20" \
+    --filter-by-ext dfy \
+    --output-logging \
+    --dir benches/HumanEval-Dafny \
+    --modes mode1 mode2 mode3 mode4 mode5 mode6 \
+    --prompts-directory prompts/dafny_eval prompts/dafny_eval prompts/dafny_eval_without_impls prompts/dafny_eval_without_impls_textd prompts/dafny_eval_without_impls_textd prompts/dafny_eval_without_impls_textd

verified_cogen/args.py

@@ -1,6 +1,6 @@
 import argparse
 import os
-from typing import Optional, no_type_check, List
+from typing import List, Optional, no_type_check
 
 from verified_cogen.tools.modes import VALID_MODES
 

verified_cogen/experiments/incremental_run.py

@@ -5,7 +5,7 @@
 
 from verified_cogen.args import ProgramArgs, get_default_parser
 from verified_cogen.llm.llm import LLM
-from verified_cogen.main import make_runner_cls, construct_rewriter
+from verified_cogen.main import construct_rewriter, make_runner_cls
 from verified_cogen.runners import RunnerConfig
 from verified_cogen.runners.languages import AnnotationType, register_basic_languages
 from verified_cogen.tools import (

verified_cogen/runners/languages/language.py

@@ -1,6 +1,6 @@
 from abc import abstractmethod
 from enum import Enum
-from typing import Any, Pattern, List, Tuple
+from typing import Any, List, Pattern, Tuple
 
 
 class AnnotationType(Enum):

verified_cogen/runners/languages/nagini.py

@@ -1,5 +1,5 @@
 import re
-from typing import Pattern, List, Tuple
+from typing import List, Pattern, Tuple
 
 from verified_cogen.runners.languages.language import AnnotationType, GenericLanguage
 from verified_cogen.tools.pureCallsDetectors import detect_and_replace_pure_calls_nagini

verified_cogen/runners/rewriters/nagini_rewriter.py

@@ -1,4 +1,4 @@
-from typing import Tuple, List
+from typing import List, Tuple
 
 from verified_cogen.runners.rewriters import Rewriter
 

verified_cogen/runners/rewriters/nagini_rewriter_fixing.py

@@ -1,4 +1,4 @@
-from typing import Tuple, Optional, Dict, List
+from typing import Dict, List, Optional, Tuple
 
 from verified_cogen.runners.rewriters.__init__ import Rewriter
 

verified_cogen/runners/rewriters/nagini_rewriter_fixing_ast.py

@@ -1,9 +1,9 @@
-from typing import Tuple, Optional
+from typing import Optional, Tuple
 
 from verified_cogen.runners.rewriters.__init__ import Rewriter
 from verified_cogen.tools.inequality_replacer import (
-    replace_inequalities,
     contains_double_inequality,
+    replace_inequalities,
 )
 
 

verified_cogen/runners/validating.py

@@ -1,4 +1,4 @@
-from typing import Optional, List
+from typing import List, Optional
 
 from verified_cogen.llm import prompts
 from verified_cogen.llm.llm import LLM

verified_cogen/several_modes/__init__.py

@@ -0,0 +1,4 @@
+from verified_cogen.several_modes.several_modes import main
+
+if __name__ == "__main__":
+    main()

verified_cogen/several_modes/args.py

@@ -1,6 +1,6 @@
 import argparse
 import os
-from typing import Optional, no_type_check, List
+from typing import List, Optional, no_type_check
 
 from verified_cogen.tools.modes import VALID_MODES
 

verified_cogen/several_modes/constants.py

@@ -0,0 +1,54 @@
+from verified_cogen.runners.languages import AnnotationType
+
+MODE_MAPPING = {
+    "mode1": [AnnotationType.INVARIANTS, AnnotationType.ASSERTS],
+    "mode2": [
+        AnnotationType.INVARIANTS,
+        AnnotationType.ASSERTS,
+        AnnotationType.PRE_CONDITIONS,
+        AnnotationType.POST_CONDITIONS,
+    ],
+    "mode3": [
+        AnnotationType.INVARIANTS,
+        AnnotationType.ASSERTS,
+        AnnotationType.IMPLS,
+    ],
+    "mode4": [
+        AnnotationType.INVARIANTS,
+        AnnotationType.ASSERTS,
+        AnnotationType.IMPLS,
+    ],
+    "mode5": [
+        AnnotationType.INVARIANTS,
+        AnnotationType.ASSERTS,
+        AnnotationType.PRE_CONDITIONS,
+        AnnotationType.POST_CONDITIONS,
+        AnnotationType.IMPLS,
+    ],
+    "mode6": [
+        AnnotationType.INVARIANTS,
+        AnnotationType.ASSERTS,
+        AnnotationType.PRE_CONDITIONS,
+        AnnotationType.POST_CONDITIONS,
+        AnnotationType.IMPLS,
+        AnnotationType.PURE,
+    ],
+}
+
+REMOVE_IMPLS_MAPPING = {
+    "mode1": False,
+    "mode2": False,
+    "mode3": True,
+    "mode4": True,
+    "mode5": True,
+    "mode6": True,
+}
+
+TEXT_DESCRIPTIONS = {
+    "mode1": False,
+    "mode2": False,
+    "mode3": False,
+    "mode4": True,
+    "mode5": True,
+    "mode6": True,
+}