Removing minimize_constraints and adding ability to use booster impli…

…es (#4577)

This PR improves on the handling and use of the `implies` endpoint in
the following two ways:
- it allows the use of the Booster implies endpoint
- it removes constraint minimization, which calls the implies endpoint
and was originally designed to streamline the path condition, but in
real-world cases only introduced an overhead.

pyk/src/pyk/cli/pyk.py

@@ -320,6 +320,7 @@ class ProveOptions(LoggingOptions, SpecOptions, SaveDirOptions):
     kore_rpc_command: str | Iterable[str] | None
     max_depth: int | None
     max_iterations: int | None
+    assume_defined: bool
     show_kcfg: bool
 
     @staticmethod
@@ -331,6 +332,7 @@ def default() -> dict[str, Any]:
             'kore_rpc_command': None,
             'max_depth': None,
             'max_iterations': None,
+            'assume_defined': False,
             'show_kcfg': False,
         }
 

pyk/src/pyk/cterm/symbolic.py

@@ -25,7 +25,7 @@
     kore_server,
 )
 from ..prelude.k import GENERATED_TOP_CELL, K_ITEM
-from ..prelude.ml import is_top, mlAnd, mlEquals
+from ..prelude.ml import is_top, mlEquals
 
 if TYPE_CHECKING:
     from collections.abc import Iterable, Iterator
@@ -92,28 +92,6 @@ def kast_to_kore(self, kinner: KInner) -> Pattern:
     def kore_to_kast(self, pattern: Pattern) -> KInner:
         return kore_to_kast(self._definition, pattern)
 
-    def minimize_constraints(self, constraints: tuple[KInner, ...], path_condition: KInner) -> tuple[KInner, ...]:
-        """Minimize given branching constraints with respect to a given path condition."""
-        # By construction, this function is to be called with at least two sets of constraints
-        assert len(constraints) >= 2
-        # Determine intersection between all returned sets of branching constraints
-        flattened_default = [flatten_label('#And', c) for c in constraints]
-        intersection = set.intersection(*(set(cs) for cs in flattened_default))
-        # If intersection is empty, there is nothing to be done
-        if not intersection:
-            return constraints
-        # Check if non-empty intersection is entailed by the path condition
-        dummy_config = self._definition.empty_config(sort=GENERATED_TOP_CELL)
-        path_condition_cterm = CTerm(dummy_config, constraints=[path_condition])
-        intersection_cterm = CTerm(dummy_config, constraints=intersection)
-        implication_check = self.implies(path_condition_cterm, intersection_cterm, bind_universally=True)
-        # The intersection is not entailed, there is nothing to be done
-        if implication_check.csubst is None:
-            return constraints
-        # The intersection is entailed and can be filtered out of the branching constraints
-        else:
-            return tuple(mlAnd(c for c in cs if c not in intersection) for cs in flattened_default)
-
     def execute(
         self,
         cterm: CTerm,
@@ -148,11 +126,6 @@ def execute(
             self.kore_to_kast(not_none(s.rule_predicate)) if s.rule_predicate is not None else None
             for s in resp_next_states
         )
-        # Branch constraint minimization makes sense only if there is a proper branching
-        if len(branching_constraints) >= 2 and all(bc is not None for bc in branching_constraints):
-            branching_constraints = self.minimize_constraints(
-                tuple(not_none(bc) for bc in branching_constraints), path_condition=mlAnd(cterm.constraints)
-            )
         next_states = tuple(
             NextState(CTerm.from_kast(self.kore_to_kast(ns.kore)), c)
             for ns, c in zip(resp_next_states, branching_constraints, strict=True)
@@ -219,6 +192,7 @@ def implies(
         bind_universally: bool = False,
         failure_reason: bool = False,
         module_name: str | None = None,
+        assume_defined: bool = False,
     ) -> CTermImplies:
         _LOGGER.debug(f'Checking implication: {antecedent} #Implies {consequent}')
         _consequent = consequent.kast
@@ -235,7 +209,9 @@ def implies(
         antecedent_kore = self.kast_to_kore(antecedent.kast)
         consequent_kore = self.kast_to_kore(_consequent)
         try:
-            result = self._kore_client.implies(antecedent_kore, consequent_kore, module_name=module_name)
+            result = self._kore_client.implies(
+                antecedent_kore, consequent_kore, module_name=module_name, assume_defined=assume_defined
+            )
         except SmtSolverError as err:
             raise self._smt_solver_error(err) from err
 
@@ -253,6 +229,7 @@ def implies(
                     bind_universally=bind_universally,
                     failure_reason=False,
                     module_name=module_name,
+                    assume_defined=assume_defined,
                 )
                 config_match = _config_match.csubst
                 if config_match is None:

pyk/src/pyk/kcfg/explore.py

@@ -72,7 +72,9 @@ def _extract_rule_labels(self, _logs: tuple[LogEntry, ...]) -> list[str]:
                     _rule_lines.append(f'{node_log.result.rule_id}:UNKNOWN')
         return _rule_lines
 
-    def implication_failure_reason(self, antecedent: CTerm, consequent: CTerm) -> tuple[bool, str]:
+    def implication_failure_reason(
+        self, antecedent: CTerm, consequent: CTerm, assume_defined: bool = False
+    ) -> tuple[bool, str]:
         def _is_cell_subst(csubst: KInner) -> bool:
             if type(csubst) is KApply and csubst.label.name == '_==K_':
                 csubst_arg = csubst.args[0]
@@ -91,7 +93,9 @@ def _is_negative_cell_subst(constraint: KInner) -> bool:
                         return True
             return False
 
-        cterm_implies = self.cterm_symbolic.implies(antecedent, consequent, failure_reason=True)
+        cterm_implies = self.cterm_symbolic.implies(
+            antecedent, consequent, failure_reason=True, assume_defined=assume_defined
+        )
         if cterm_implies.csubst is not None:
             return (True, '')
 

pyk/src/pyk/kore/rpc.py

@@ -1027,12 +1027,14 @@ def implies(
         consequent: Pattern,
         *,
         module_name: str | None = None,
+        assume_defined: bool = False,
     ) -> ImpliesResult:
         params = filter_none(
             {
                 'antecedent': self._state(antecedent),
                 'consequent': self._state(consequent),
                 'module': module_name,
+                'assume-defined': assume_defined,
             }
         )
 

pyk/src/pyk/ktool/prove_rpc.py

@@ -48,6 +48,7 @@ def prove_rpc(self, options: ProveOptions) -> list[Proof]:
         return [
             self._prove_claim_rpc(
                 claim,
+                assume_defined=options.assume_defined,
                 max_depth=options.max_depth,
                 save_directory=options.save_directory,
                 max_iterations=options.max_iterations,
@@ -58,6 +59,7 @@ def prove_rpc(self, options: ProveOptions) -> list[Proof]:
     def _prove_claim_rpc(
         self,
         claim: KClaim,
+        assume_defined: bool,
         max_depth: int | None = None,
         save_directory: Path | None = None,
         max_iterations: int | None = None,
@@ -85,10 +87,10 @@ def _prove_claim_rpc(
             with self._explore_context() as kcfg_explore:
                 if is_functional_claim:
                     assert type(proof) is EqualityProof
-                    prover = ImpliesProver(proof, kcfg_explore)
+                    prover = ImpliesProver(proof, kcfg_explore, assume_defined=assume_defined)
                 else:
                     assert type(proof) is APRProof
-                    prover = APRProver(kcfg_explore, execute_depth=max_depth)
+                    prover = APRProver(kcfg_explore, execute_depth=max_depth, assume_defined=assume_defined)
                 prover.advance_proof(proof, max_iterations=max_iterations)
 
         if proof.passed:

pyk/src/pyk/proof/implies.py

@@ -410,13 +410,15 @@ def lines(self) -> list[str]:
 class ImpliesProver(Prover[ImpliesProof, ImpliesProofStep, ImpliesProofResult]):
     proof: ImpliesProof
     kcfg_explore: KCFGExplore
+    assume_defined: bool
 
     def close(self) -> None:
         self.kcfg_explore.cterm_symbolic._kore_client.close()
 
-    def __init__(self, proof: ImpliesProof, kcfg_explore: KCFGExplore):
+    def __init__(self, proof: ImpliesProof, kcfg_explore: KCFGExplore, assume_defined: bool = False):
         self.kcfg_explore = kcfg_explore
         self.proof = proof
+        self.assume_defined = assume_defined
 
     def step_proof(self, step: ImpliesProofStep) -> list[ImpliesProofResult]:
         proof_type = type(step.proof).__name__
@@ -450,6 +452,7 @@ def step_proof(self, step: ImpliesProofStep) -> list[ImpliesProofResult]:
                 antecedent=CTerm(config=dummy_config, constraints=[simplified_antecedent]),
                 consequent=CTerm(config=dummy_config, constraints=[simplified_consequent]),
                 bind_universally=step.proof.bind_universally,
+                assume_defined=self.assume_defined,
             )
             result = _result.csubst
             if result is not None:

pyk/src/pyk/proof/reachability.py

@@ -671,6 +671,7 @@ class APRProver(Prover[APRProof, APRProofStep, APRProofResult]):
     always_check_subsumption: bool
     fast_check_subsumption: bool
     direct_subproof_rules: bool
+    assume_defined: bool
     kcfg_explore: KCFGExplore
 
     def __init__(
@@ -683,6 +684,7 @@ def __init__(
         always_check_subsumption: bool = True,
         fast_check_subsumption: bool = False,
         direct_subproof_rules: bool = False,
+        assume_defined: bool = False,
     ) -> None:
 
         self.kcfg_explore = kcfg_explore
@@ -694,6 +696,7 @@ def __init__(
         self.always_check_subsumption = always_check_subsumption
         self.fast_check_subsumption = fast_check_subsumption
         self.direct_subproof_rules = direct_subproof_rules
+        self.assume_defined = assume_defined
 
     def close(self) -> None:
         self.kcfg_explore.cterm_symbolic._kore_client.close()
@@ -737,7 +740,7 @@ def _check_subsume(self, node: KCFG.Node, target_node: KCFG.Node, proof_id: str)
         if self.fast_check_subsumption and not self._may_subsume(node, target_node):
             _LOGGER.info(f'Skipping full subsumption check because of fast may subsume check {proof_id}: {node.id}')
             return None
-        _csubst = self.kcfg_explore.cterm_symbolic.implies(node.cterm, target_cterm)
+        _csubst = self.kcfg_explore.cterm_symbolic.implies(node.cterm, target_cterm, assume_defined=self.assume_defined)
         csubst = _csubst.csubst
         if csubst is not None:
             _LOGGER.info(f'Subsumed into target node {proof_id}: {shorten_hashes((node.id, target_node.id))}')
@@ -804,7 +807,9 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]:
         ]
 
     def failure_info(self, proof: APRProof) -> FailureInfo:
-        return APRFailureInfo.from_proof(proof, self.kcfg_explore, counterexample_info=self.counterexample_info)
+        return APRFailureInfo.from_proof(
+            proof, self.kcfg_explore, counterexample_info=self.counterexample_info, assume_defined=self.assume_defined
+        )
 
 
 @dataclass(frozen=True)
@@ -871,7 +876,9 @@ def __init__(
         )
 
     @staticmethod
-    def from_proof(proof: APRProof, kcfg_explore: KCFGExplore, counterexample_info: bool = False) -> APRFailureInfo:
+    def from_proof(
+        proof: APRProof, kcfg_explore: KCFGExplore, counterexample_info: bool = False, assume_defined: bool = False
+    ) -> APRFailureInfo:
         target = proof.kcfg.node(proof.target)
         pending_nodes = {node.id for node in proof.pending}
         failing_nodes = {node.id for node in proof.failing}
@@ -881,7 +888,7 @@ def from_proof(proof: APRProof, kcfg_explore: KCFGExplore, counterexample_info:
         for node in proof.failing:
             node_cterm, _ = kcfg_explore.cterm_symbolic.simplify(node.cterm)
             target_cterm, _ = kcfg_explore.cterm_symbolic.simplify(target.cterm)
-            _, reason = kcfg_explore.implication_failure_reason(node_cterm, target_cterm)
+            _, reason = kcfg_explore.implication_failure_reason(node_cterm, target_cterm, assume_defined=assume_defined)
             path_condition = kcfg_explore.pretty_print(proof.path_constraints(node.id))
             failure_reasons[node.id] = reason
             path_conditions[node.id] = path_condition

pyk/src/tests/integration/cterm/test_simple.py

@@ -7,7 +7,7 @@
 from pyk.cterm import CTerm
 from pyk.kast.inner import KApply, KSequence, KToken, KVariable
 from pyk.prelude.kint import leInt
-from pyk.prelude.ml import mlAnd, mlEqualsTrue, mlTop
+from pyk.prelude.ml import mlEqualsTrue, mlTop
 from pyk.prelude.utils import token
 from pyk.testing import CTermSymbolicTest, KPrintTest
 
@@ -43,37 +43,6 @@ def le_int(n: int, var: str) -> KInner:
     return mlEqualsTrue(leInt(token(n), KVariable(var)))
 
 
-MINIMIZE_CONSTRAINTS_TEST_DATA: Final = (
-    (
-        'no-intersection',
-        [[le_int(0, 'X')], [le_int(0, 'Y')]],
-        mlTop(),
-        [[le_int(0, 'X')], [le_int(0, 'Y')]],
-    ),
-    (
-        'intersection-not-entailed',
-        [
-            [le_int(0, 'X'), le_int(0, 'Y')],
-            [le_int(0, 'X'), le_int(0, 'Z')],
-        ],
-        mlTop(),
-        [[le_int(0, 'X'), le_int(0, 'Y')], [le_int(0, 'X'), le_int(0, 'Z')]],
-    ),
-    (
-        'intersection-entailed',
-        [
-            [le_int(0, 'X'), le_int(0, 'Y')],
-            [le_int(0, 'X'), le_int(0, 'Z')],
-        ],
-        le_int(10, 'X'),
-        [
-            [le_int(0, 'Y')],
-            [le_int(0, 'Z')],
-        ],
-    ),
-)
-
-
 class TestSimpleProof(CTermSymbolicTest, KPrintTest):
     KOMPILE_MAIN_FILE = K_FILES / 'simple-proofs.k'
     KOMPILE_ARGS = {'syntax_module': 'SIMPLE-PROOFS'}
@@ -161,26 +130,3 @@ def test_simplify(
         # Then
         assert actual_k == expected_k
         assert actual_state == expected_state
-
-    @pytest.mark.parametrize(
-        'test_id,constraints,pc,expected_minimized_constraints',
-        MINIMIZE_CONSTRAINTS_TEST_DATA,
-        ids=[test_id for test_id, *_ in MINIMIZE_CONSTRAINTS_TEST_DATA],
-    )
-    def test_minimize_constraints(
-        self,
-        cterm_symbolic: CTermSymbolic,
-        test_id: str,
-        constraints: Iterable[Iterable[KInner]],
-        pc: KInner,
-        expected_minimized_constraints: Iterable[Iterable[KInner]],
-    ) -> None:
-        # Given
-        _constraints = tuple(mlAnd(cs) for cs in constraints)
-        _expected_minimized_constraints = tuple(mlAnd(cs) for cs in expected_minimized_constraints)
-
-        # When
-        _minimized_constraints = cterm_symbolic.minimize_constraints(_constraints, pc)
-
-        # Then
-        assert _minimized_constraints == _expected_minimized_constraints

pyk/src/tests/unit/kore/test_client.py

@@ -177,7 +177,7 @@ def test_execute(
     (
         int_bottom,
         int_top,
-        {'antecedent': kore(int_bottom), 'consequent': kore(int_top)},
+        {'antecedent': kore(int_bottom), 'consequent': kore(int_top), 'assume-defined': False},
         {'valid': True, 'implication': kore(int_top)},
         ImpliesResult(True, int_top, None, None, ()),
     ),