Consolidate summarizer arguments

runtimeverification · May 4, 2023 · 401fd26 · 401fd26
1 parent e32b219
commit 401fd26
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 41 deletions.
diff --git a/kimp/src/kimp/__main__.py b/kimp/src/kimp/__main__.py
@@ -389,41 +389,12 @@ def create_argument_parser() -> ArgumentParser:
     command_parser.add_parser(
         'prove', help='Prove a K claim', parents=[shared_args, spec_file_shared_args, claim_shared_args, explore_args]
     )
-    prove_subparser.add_argument(
-        '--max-iterations',
-        type=int,
-        default=20,
-        help='Maximum number of iterations to run prover for.',
-    )
 
     # Summarize
-    summarize_subparser = command_parser.add_parser('summarize', help='Prove a K claim', parents=[shared_args])
-    summarize_subparser.add_argument(
-        '--definition-dir',
-        dest='definition_dir',
-        type=dir_path,
-        help='Path to Haskell definition to use.',
-    )
-    summarize_subparser.add_argument(
-        'spec_file',
-        type=file_path,
-        help='Path to .k file',
-    )
-    summarize_subparser.add_argument(
-        'spec_module',
-        type=str,
-        help='Spec main module',
-    )
-    summarize_subparser.add_argument(
-        'claim_id',
-        type=str,
-        help='Claim id',
-    )
-    summarize_subparser.add_argument(
-        '--max-iterations',
-        type=int,
-        default=20,
-        help='Maximum number of iterations to run summarizer for.',
+    _ = command_parser.add_parser(
+        'summarize',
+        help='Prove a K claim',
+        parents=[shared_args, spec_file_shared_args, claim_shared_args, explore_args],
     )
 
     # BMC Prove

diff --git a/kimp/src/kimp/kimp.py b/kimp/src/kimp/kimp.py
@@ -26,8 +26,8 @@
 from pyk.prelude.kbool import BOOL, notBool
 from pyk.prelude.ml import mlEqualsTrue
 from pyk.proof.equality import EqualityProof, EqualityProver
-from pyk.proof.reachability import APRBMCProof, APRBMCProver, APRProof, APRProver
 from pyk.proof.proof import Proof
+from pyk.proof.reachability import APRBMCProof, APRBMCProver, APRProof, APRProver
 from pyk.proof.utils import read_proof
 from pyk.utils import shorten_hashes
 
@@ -267,10 +267,6 @@ def summarize(
         spec_module: str,
         claim_id: str,
         max_iterations: int,
-        # max_depth: int,
-        # terminal_rules: Iterable[str],
-        # cut_rules: Iterable[str],
-        # proof_status: ProofStatus,
     ) -> None:
         claims = self.kprove.get_claims(
             Path(spec_file),
@@ -304,7 +300,7 @@ def summarize(
                     ]
                     if len(prior_loops_on_path) > 0:
                         _LOGGER.info(
-                            f'Loops found: {shorten_hashes(next_node.id)} -> {shorten_hashes(list(nd.id for nd in prior_loops_on_path))}'
+                            f'Loops found: {shorten_hashes(next_node.id)} -> {shorten_hashes([nd.id for nd in prior_loops_on_path])}'
                         )
                         generalized_term = next_node.cterm.kast
                         for node in prior_loops_on_path:
@@ -316,9 +312,7 @@ def summarize(
                     kcfg = prover.advance_proof(
                         kcfg_explore,
                         max_iterations=1,
-                        # execute_depth=1,
                         cut_point_rules=['IMP.while'],
-                        # terminal_rules='IMP.while',
                     )
 
         proof.write_proof()