Integrate the APR and APRBMC proof/prover classes into one (#870)

Currently we have a completely separate class hierarchy for `APRProof`
and `APRBMCProof` classes, which requires duplicates in the `*Prover`
classes and in the `*NodePrinter` classes and in the `*Show` classes.
This unifies the classes by making the `bmc_depth` an optional parameter
of `APRProof` and tracking the `_bounded` nodes directly in `APRProof`.

- `bmc_depth: int | None` is added as a field to `APRProof`, as is the
`_bounded: set[int]` set. The various utilities for manipulating the
class are updated to account for this.
- The `APRProver` class is updated to check if the `bmc_depth` field is
present, and if alters its `advance_pending_node` logic to check for
loops and take that into account.
- The various display classes like `APRNodePrinter` and `APRSummary` are
updated.

---------

Co-authored-by: devops <[email protected]>

Author: ehildenb

docs/conf.py

@@ -9,8 +9,8 @@
 project = 'pyk'
 author = 'Runtime Verification, Inc'
 copyright = '2024, Runtime Verification, Inc'
-version = '0.1.621'
-release = '0.1.621'
+version = '0.1.622'
+release = '0.1.622'
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

package/version

@@ -1 +1 @@
-0.1.621
+0.1.622

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.621"
+version = "0.1.622"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/pyk/proof/__init__.py

@@ -1,3 +1,3 @@
 from .equality import EqualityProof, EqualityProver
 from .proof import ProofStatus
-from .reachability import APRBMCProof, APRBMCProver, APRProof, APRProver
+from .reachability import APRProof, APRProver

src/pyk/proof/proof.py

@@ -29,7 +29,7 @@ class ProofStatus(Enum):
 
 
 class Proof(ABC):
-    _PROOF_TYPES: Final = {'APRProof', 'APRBMCProof', 'EqualityProof', 'RefutationProof'}
+    _PROOF_TYPES: Final = {'APRProof', 'EqualityProof', 'RefutationProof'}
 
     id: str
     proof_dir: Path | None
@@ -199,7 +199,7 @@ def from_dict(cls: type[Proof], dct: Mapping[str, Any], proof_dir: Path | None =
     def read_proof(cls: type[Proof], id: str, proof_dir: Path) -> Proof:
         # these local imports allow us to call .to_dict() based on the proof type we read from JSON
         from .equality import EqualityProof, RefutationProof  # noqa
-        from .reachability import APRBMCProof, APRProof  # noqa
+        from .reachability import APRProof  # noqa
 
         proof_path = proof_dir / f'{hash_str(id)}.json'
         if Proof.proof_exists(id, proof_dir):
@@ -216,7 +216,7 @@ def read_proof(cls: type[Proof], id: str, proof_dir: Path) -> Proof:
     def read_proof_data(proof_dir: Path, id: str) -> Proof:
         # these local imports allow us to call .to_dict() based on the proof type we read from JSON
         from .equality import EqualityProof, RefutationProof  # noqa
-        from .reachability import APRBMCProof, APRProof  # noqa
+        from .reachability import APRProof  # noqa
 
         proof_path = proof_dir / id / 'proof.json'
         if Proof.proof_data_exists(id, proof_dir):