Merge remote-tracking branch 'origin/develop' into _update-deps/runti…

…meverification/haskell-backend

k-distribution/include/kframework/builtin/domains.md

@@ -1241,9 +1241,13 @@ You can:
                > left:
                  Int "*Int" Int                 [function, total, symbol(_*Int_), left, comm, smt-hook(*), hook(INT.mul)]
                /* FIXME: translate /Int and %Int into smtlib */
-               /* /Int and %Int implement t-division, which rounds towards 0 */
-               | Int "/Int" Int                 [function, symbol(_/Int_), left, smt-hook(div), hook(INT.tdiv)]
-               | Int "%Int" Int                 [function, symbol(_%Int_), left, smt-hook(mod), hook(INT.tmod)]
+               /* /Int and %Int implement t-division, which rounds towards 0. SMT hooks need to convert from Euclidian division operations */
+               | Int "/Int" Int                 [function, symbol(_/Int_), left,
+                                                 smt-hook((ite (or (= 0 (mod #1 #2)) (>= #1 0)) (div #1 #2) (ite (> #2 0) (+ (div #1 #2) 1) (- (div #1 #2) 1)))),
+                                                 hook(INT.tdiv)]
+               | Int "%Int" Int                 [function, symbol(_%Int_), left,
+                                                 smt-hook((ite (or (= 0 (mod #1 #2)) (>= #1 0)) (mod #1 #2) (ite (> #2 0) (- (mod #1 #2) #2) (+ (mod #1 #2) #2)))),
+                                                 hook(INT.tmod)]
                /* divInt and modInt implement e-division according to the Euclidean division theorem, therefore the remainder is always positive */
                | Int "divInt" Int               [function, symbol(_divInt_), left, smt-hook(div), hook(INT.ediv)]
                | Int "modInt" Int               [function, symbol(_modInt_), left, smt-hook(mod), hook(INT.emod)]

pyk/regression-new/kprove-haskell/sum-spec.k.out

@@ -31,7 +31,9 @@ Subproofs: 0
 │     #And { true #Equals N:Int >=Int 0 }
 ┃
 ┃ (branch)
-┣━━┓ constraint: N:Int >Int 0
+┣━━┓ subst: .Subst
+┃  ┃ constraint:
+┃  ┃     N:Int >Int 0
 ┃  │
 ┃  ├─ 3
 ┃  │     <generatedTop>
@@ -92,8 +94,11 @@ Subproofs: 0
 ┃  │     #And { true #Equals N:Int >=Int 0 }
 ┃  │     #And { true #Equals N:Int +Int -1 >=Int 0 }
 ┃  │
-┃  ┊  constraint: OMITTED CONSTRAINT
-┃  ┊  subst: OMITTED SUBST
+┃  ┊  constraint:
+┃  ┊      S:Int +Int C:Int +Int N:Int +Int -1 *Int C:Int +Int 1 +Int N:Int +Int -2 *Int N:Int +Int -1 /Int 2 ==K S:Int +Int N:Int *Int C:Int +Int N:Int +Int -1 *Int N:Int /Int 2
+┃  ┊  subst:
+┃  ┊      ?_COUNTER_CELL_af8c44a5 <- COUNTER_CELL_af8c44a5:Int
+┃  ┊      ?_GENERATEDCOUNTER_CELL_5e3e01ba <- GENERATEDCOUNTER_CELL_5e3e01ba:Int
 ┃  └─ 2 (leaf, target)
 ┃        <generatedTop>
 ┃          <k>
@@ -112,7 +117,9 @@ Subproofs: 0
 ┃        #And { true #Equals N:Int >=Int 0 }
 ┃        #And { true #Equals ?S:Int ==Int S:Int +Int N:Int *Int C:Int +Int N:Int -Int 1 *Int N:Int /Int 2 }
 ┃
-┗━━┓ constraint: N:Int ==Int 0
+┗━━┓ subst: .Subst
+   ┃ constraint:
+   ┃     N:Int ==Int 0
    │
    ├─ 4
    │     <generatedTop>
@@ -151,8 +158,11 @@ Subproofs: 0
    │     </generatedTop>
    │     #And { N:Int #Equals 0 }
    │
-   ┊  constraint: OMITTED CONSTRAINT
-   ┊  subst: OMITTED SUBST
+   ┊  constraint:
+   ┊      S:Int ==Int S:Int +Int N:Int *Int COUNTER_CELL_af8c44a5:Int +Int N:Int +Int -1 *Int N:Int /Int 2
+   ┊  subst:
+   ┊      C <- COUNTER_CELL_af8c44a5:Int
+   ┊      GENERATEDCOUNTER_CELL_5e3e01ba <- GENERATEDCOUNTER_CELL_949ec677:Int
    └─ 2 (leaf, target)
          <generatedTop>
            <k>

pyk/regression-new/kprove-haskell/test-spec.k.out

@@ -48,7 +48,8 @@ Subproofs: 0
 │     </generatedTop>
 │
 ┊  constraint: true
-┊  subst: GENERATEDCOUNTER_CELL_6de8d71b <- GENERATEDCOUNTER_CELL_c84b0b5f:Int
+┊  subst:
+┊      GENERATEDCOUNTER_CELL_6de8d71b <- GENERATEDCOUNTER_CELL_c84b0b5f:Int
 └─ 2 (leaf, target)
       <generatedTop>
         <k>

pyk/src/pyk/__main__.py

@@ -282,7 +282,7 @@ def explore_context() -> Iterator[KCFGExplore]:
         if options.show_kcfg and type(proof) is APRProof:
             node_printer = APRProofNodePrinter(proof, kprove, full_printer=True, minimize=False)
             show = APRProofShow(kprove, node_printer=node_printer)
-            print('\n'.join(show.show(proof)))
+            print('\n'.join(show.show(proof, minimize=False)))
     sys.exit(len([p.id for p in proofs if not p.passed]))
 
 

pyk/src/pyk/cterm/cterm.py

@@ -6,11 +6,12 @@
 from typing import TYPE_CHECKING
 
 from ..kast import KInner
-from ..kast.inner import KApply, KRewrite, KToken, Subst, bottom_up
+from ..kast.inner import KApply, KRewrite, KToken, KVariable, Subst, bottom_up
 from ..kast.manip import (
     abstract_term_safely,
     build_claim,
     build_rule,
+    extract_subst,
     flatten_label,
     free_vars,
     ml_pred_to_bool,
@@ -20,9 +21,9 @@
     split_config_and_constraints,
     split_config_from,
 )
-from ..prelude.k import GENERATED_TOP_CELL
+from ..prelude.k import GENERATED_TOP_CELL, K
 from ..prelude.kbool import andBool, orBool
-from ..prelude.ml import is_bottom, is_top, mlAnd, mlBottom, mlEqualsTrue, mlImplies, mlTop
+from ..prelude.ml import is_bottom, is_top, mlAnd, mlBottom, mlEquals, mlEqualsTrue, mlImplies, mlTop
 from ..utils import unique
 
 if TYPE_CHECKING:
@@ -38,7 +39,7 @@ class CTerm:
 
     Contains the data:
     - `config`: the _configuration_ (structural component of the state, potentially containing free variabls)
-    - `constraints`: conditiions which limit/constraint the free variables from the `config`
+    - `constraints`: conditions which limit/constraint the free variables from the `config`
     """
 
     config: KInner  # TODO Optional?
@@ -217,17 +218,7 @@ def anti_unify(
             if KToken('true', 'Bool') not in [disjunct_lhs, disjunct_rhs]:
                 new_cterm = new_cterm.add_constraint(mlEqualsTrue(orBool([disjunct_lhs, disjunct_rhs])))
 
-        new_constraints = []
-        fvs = new_cterm.free_vars
-        len_fvs = 0
-        while len_fvs < len(fvs):
-            len_fvs = len(fvs)
-            for constraint in common_constraints:
-                if constraint not in new_constraints:
-                    constraint_fvs = free_vars(constraint)
-                    if any(fv in fvs for fv in constraint_fvs):
-                        new_constraints.append(constraint)
-                        fvs = fvs | constraint_fvs
+        new_constraints = remove_useless_constraints(common_constraints, new_cterm.free_vars)
 
         for constraint in new_constraints:
             new_cterm = new_cterm.add_constraint(constraint)
@@ -253,6 +244,25 @@ def remove_useless_constraints(self, keep_vars: Iterable[str] = ()) -> CTerm:
         return CTerm(self.config, new_constraints)
 
 
+def cterm_match(cterm1: CTerm, cterm2: CTerm) -> CSubst | None:
+    """Find a substitution which can instantiate `cterm1` to `cterm2`.
+
+    Args:
+        cterm1: `CTerm` to instantiate to `cterm2`.
+        cterm2: `CTerm` to instantiate `cterm1` to.
+
+    Returns:
+        A `CSubst` which can instantiate `cterm1` to `cterm2`, or `None` if no such `CSubst` exists.
+    """
+    # todo: delete this function and use cterm1.match_with_constraint(cterm2) directly after closing #4496
+    subst = cterm1.config.match(cterm2.config)
+    if subst is None:
+        return None
+    source_constraints = [subst(c) for c in cterm1.constraints]
+    constraints = [c for c in cterm2.constraints if c not in source_constraints]
+    return CSubst(subst, constraints)
+
+
 def anti_unify(state1: KInner, state2: KInner, kdef: KDefinition | None = None) -> tuple[KInner, Subst, Subst]:
     """Return a generalized state over the two input states.
 
@@ -322,6 +332,26 @@ def from_dict(dct: dict[str, Any]) -> CSubst:
         constraints = (KInner.from_dict(c) for c in dct['constraints'])
         return CSubst(subst=subst, constraints=constraints)
 
+    @staticmethod
+    def from_pred(pred: KInner) -> CSubst:
+        """Extract from a boolean predicate a CSubst."""
+        subst, pred = extract_subst(pred)
+        return CSubst(subst=subst, constraints=flatten_label('#And', pred))
+
+    def pred(self, sort_with: KDefinition | None = None, subst: bool = True, constraints: bool = True) -> KInner:
+        """Return an ML predicate representing this substitution."""
+        _preds: list[KInner] = []
+        if subst:
+            for k, v in self.subst.minimize().items():
+                sort = K
+                if sort_with is not None:
+                    _sort = sort_with.sort(v)
+                    sort = _sort if _sort is not None else sort
+                _preds.append(mlEquals(KVariable(k, sort=sort), v, arg_sort=sort))
+        if constraints:
+            _preds.extend(self.constraints)
+        return mlAnd(_preds)
+
     @property
     def constraint(self) -> KInner:
         """Return the set of constraints as a single flattened constraint using `mlAnd`."""
@@ -333,8 +363,13 @@ def add_constraint(self, constraint: KInner) -> CSubst:
 
     def apply(self, cterm: CTerm) -> CTerm:
         """Apply this `CSubst` to the given `CTerm` (instantiating the free variables, and adding the constraints)."""
-        _kast = self.subst(cterm.kast)
-        return CTerm(_kast, [self.constraint])
+        config = self.subst(cterm.config)
+        constraints = [self.subst(constraint) for constraint in cterm.constraints] + list(self.constraints)
+        return CTerm(config, constraints)
+
+    def __call__(self, cterm: CTerm) -> CTerm:
+        """Overload for `CSubst.apply`."""
+        return self.apply(cterm)
 
 
 def cterm_build_claim(

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, mlEquals
+from ..prelude.ml import mlAnd
 
 if TYPE_CHECKING:
     from collections.abc import Iterable, Iterator
@@ -267,19 +267,8 @@ def implies(
             raise ValueError('Received empty predicate for valid implication.')
         ml_subst = self.kore_to_kast(result.substitution)
         ml_pred = self.kore_to_kast(result.predicate)
-        ml_preds = flatten_label('#And', ml_pred)
-        if is_top(ml_subst):
-            csubst = CSubst(subst=Subst({}), constraints=ml_preds)
-            return CTermImplies(csubst, (), None, result.logs)
-        subst_pattern = mlEquals(KVariable('###VAR'), KVariable('###TERM'))
-        _subst: dict[str, KInner] = {}
-        for subst_pred in flatten_label('#And', ml_subst):
-            m = subst_pattern.match(subst_pred)
-            if m is not None and type(m['###VAR']) is KVariable:
-                _subst[m['###VAR'].name] = m['###TERM']
-            else:
-                raise AssertionError(f'Received a non-substitution from implies endpoint: {subst_pred}')
-        csubst = CSubst(subst=Subst(_subst), constraints=ml_preds)
+        ml_subst_pred = mlAnd(flatten_label('#And', ml_subst) + flatten_label('#And', ml_pred))
+        csubst = CSubst.from_pred(ml_subst_pred)
         return CTermImplies(csubst, (), None, result.logs)
 
     def assume_defined(self, cterm: CTerm, module_name: str | None = None) -> CTerm:

pyk/src/pyk/kast/inner.py

@@ -749,20 +749,6 @@ def from_pred(pred: KInner) -> Subst:
                     raise ValueError(f'Invalid substitution predicate: {conjunct}')
         return Subst(subst)
 
-    @property
-    def ml_pred(self) -> KInner:
-        """Turn this `Subst` into a matching logic predicate using `{_#Equals_}` operator."""
-        items = []
-        for k in self:
-            if KVariable(k) != self[k]:
-                items.append(KApply('#Equals', [KVariable(k), self[k]]))
-        if len(items) == 0:
-            return KApply('#Top')
-        ml_term = items[0]
-        for _i in items[1:]:
-            ml_term = KApply('#And', [ml_term, _i])
-        return ml_term
-
     @property
     def pred(self) -> KInner:
         """Turn this `Subst` into a boolean predicate using `_==K_` operator."""

pyk/src/pyk/kast/manip.py

@@ -215,48 +215,39 @@ def extract_rhs(term: KInner) -> KInner:
 
 
 def extract_subst(term: KInner) -> tuple[Subst, KInner]:
-    def _subst_for_terms(term1: KInner, term2: KInner) -> Subst | None:
-        if type(term1) is KVariable and type(term2) not in {KToken, KVariable}:
-            return Subst({term1.name: term2})
-        if type(term2) is KVariable and type(term1) not in {KToken, KVariable}:
-            return Subst({term2.name: term1})
-        return None
-
-    def _extract_subst(conjunct: KInner) -> Subst | None:
-        if type(conjunct) is KApply:
-            if conjunct.label.name == '#Equals':
-                subst = _subst_for_terms(conjunct.args[0], conjunct.args[1])
-
-                if subst is not None:
-                    return subst
-
-                if (
-                    conjunct.args[0] == TRUE
-                    and type(conjunct.args[1]) is KApply
-                    and conjunct.args[1].label.name in {'_==K_', '_==Int_'}
-                ):
-                    subst = _subst_for_terms(conjunct.args[1].args[0], conjunct.args[1].args[1])
-
-                    if subst is not None:
-                        return subst
+    subst = {}
+    rem_conjuncts: list[KInner] = []
 
+    def _extract_subst(term: KInner, term2: KInner) -> tuple[str, KInner] | None:
+        if (
+            (isinstance(term, KVariable) and term.name not in subst)
+            and not (isinstance(term2, KVariable) and term2.name in subst)
+            and term.name not in free_vars(term2)
+        ):
+            return (term.name, term2)
+        if (
+            (isinstance(term2, KVariable) and term2.name not in subst)
+            and not (isinstance(term, KVariable) and term.name in subst)
+            and term2.name not in free_vars(term)
+        ):
+            return (term2.name, term)
+        if term == TRUE and isinstance(term2, KApply) and term2.label.name in {'_==K_', '_==Int_'}:
+            return _extract_subst(term2.args[0], term2.args[1])
+        if term2 == TRUE and isinstance(term, KApply) and term.label.name in {'_==K_', '_==Int_'}:
+            return _extract_subst(term.args[0], term.args[1])
         return None
 
-    conjuncts = flatten_label('#And', term)
-    subst = Subst()
-    rem_conjuncts: list[KInner] = []
-
-    for conjunct in conjuncts:
-        new_subst = _extract_subst(conjunct)
-        if new_subst is None:
-            rem_conjuncts.append(conjunct)
+    for conjunct in flatten_label('#And', term):
+        if isinstance(conjunct, KApply) and conjunct.label.name == '#Equals':
+            if _conjunct_subst := _extract_subst(conjunct.args[0], conjunct.args[1]):
+                name, value = _conjunct_subst
+                subst[name] = value
+            else:
+                rem_conjuncts.append(conjunct)
         else:
-            new_subst = subst.union(new_subst)
-            if new_subst is None:
-                raise ValueError('Conflicting substitutions')  # TODO handle this case
-            subst = new_subst
+            rem_conjuncts.append(conjunct)
 
-    return subst, mlAnd(rem_conjuncts)
+    return Subst(subst), mlAnd(rem_conjuncts)
 
 
 def count_vars(term: KInner) -> Counter[str]:

pyk/src/pyk/kcfg/kcfg.py

@@ -9,6 +9,8 @@
 from threading import RLock
 from typing import TYPE_CHECKING, Final, List, Union, cast, final
 
+from pyk.cterm.cterm import cterm_match
+
 from ..cterm import CSubst, CTerm, cterm_build_claim, cterm_build_rule
 from ..kast import EMPTY_ATT
 from ..kast.inner import KApply
@@ -1040,6 +1042,16 @@ def create_split(self, source_id: NodeIdLike, splits: Iterable[tuple[NodeIdLike,
         self.add_successor(split)
         return split
 
+    def create_split_by_nodes(self, source_id: NodeIdLike, target_ids: Iterable[NodeIdLike]) -> KCFG.Split | None:
+        """Create a split without crafting a CSubst."""
+        source = self.node(source_id)
+        targets = [self.node(nid) for nid in target_ids]
+        try:
+            csubsts = [not_none(cterm_match(source.cterm, target.cterm)) for target in targets]
+        except ValueError:
+            return None
+        return self.create_split(source.id, zip(target_ids, csubsts, strict=True))
+
     def ndbranches(self, *, source_id: NodeIdLike | None = None, target_id: NodeIdLike | None = None) -> list[NDBranch]:
         source_id = self._resolve(source_id) if source_id is not None else None
         target_id = self._resolve(target_id) if target_id is not None else None