The main differences in the Cartesian CEGAR implementation in Scorpion compared to Fast Downward are the following:
- new functionality:
    - incremental search (for flaws and shortest abstract paths)
    - match tree (as an alternative to constructing an explicit abstract transition system)
    - split selector (more different options)
- code structure:
    - separate rewiring from TransitionSystem
    - flaw struct moved from Cegar into separate class
- efficiency:
    - Cartesian set
    - state ID order for updating refinement hierarchy
    - cost saturation

Dependencies
- The efficiency improvements are mostly independent of the other changes.
- The incremental search uses the new code structure. Thus it would be easier to address these changes first.
- The match tree requires the rewiring functionality to be independent of the transition system (it does not use an explicit transition system).


Short summary for each topic:
Incremental Search
Replaces the current search for an abstract solution (+ the maintaining of goal distances) in AbstractSearch and the consequent search for a flaw in Cegar.
New class shortest_paths: internally stores a shortest path tree over the abstract states that can be incrementally updated after each split and can be fully (re)computed using Dijkstra's algorithm. The class is used to keep track of the current goal distances for the abstract states and to extract abstract solutions in the main loop of the CEGAR algorithm. 
Note: The update_incrementally() function also uses the TransitionRewirer to update transitions when MatchTree is used. 
New class flaw_search: implements the search for flaws based on the abstract solution and uses the new flaw class instead of the old flaw struct inside the Cegar class. Directly returns a split to the main loop in Cegar and capsulates the entire "search for flaws" after the shortest abstract path was determined. 
The search incrementally constructs a graph representing the prefixes of each optimal abstract solution (in parallel) up to the point where a flaw occurs, using the information from ShortestPaths. All these flaws are collected. Depending on the setting of the PickFlawedAbstractState parameter, a flaw is chosen and passed to the split selector. The returned split is then passed back into the main loop of Cegar.  
- affected areas of code: abstract_search.cc/.h, cegar.cc/.h, new shortest_paths.cc/.h, new flaw_search.cc/.h, new flaw.cc/.h, new transition_rewirer.cc/.h
- useful commits:
    commit message includes [cegar-incremental-search], [remove-cegar-astar], and
    commits changing the flaw-search.cc 

Match Tree
The MatchTree class does not explicitly store the entire transition system. Instead transitions can be efficiently computed on demand, when they are needed.
Requires an interface to use this instead of the current transition system (like the use of TransitionRepresentation in Scorpion).
- affected areas of code: new class match_tree.cc/.h, new transition_rewirer.cc/.h, abstraction.cc/.h , refinement_hierarchy.cc (new functions to traverse the children).
- useful commits:
    commit message includes [cartesian-match-tree]

Split Selector
Some new options are added to the PickSplit Enum (strategies on how to select a split in case of multiple options).
Split struct is extended: now stores a count variable, the abstract state id, and the var value in addition to the var_id and the value vector.
New functions for the new PickSplit options: combine_splits and an implementation of the operator== and operator<<.    
SplitSelector class uses an additional PickSplit option (first pick + tiebreak pick)
and new functions for the new PickSplit Options are added. The pick_split function implementation is also changed.
Plugins for the new PickSplit options need to be registered.
- affected areas of code: split_selector.cc/.h, usage in new class flaw_search.cc

Cartesian Set
Uses BitsetMath:Block, ConstBitsetView and BitsetView (from per_state_bitset) instead of DynamicBitset for the internal representation of variable domains.
Also changes the BitsetMath:Block implementation (from int to char) and adds functions to ConstBitsetView and BitsetView.
Also adds some functions to the CartesianSet (get_num_variables, compute_size, set_static_members)
- affected areas of code: cartesian_set, search/per_state_bitset, possibly usages of new CartesianSet functions in Abstraction, new TransitionRewirer, AbstractState, new MatchTree, RefinementHierarchy, types.h

State ID order for updating refinement hierarchy
When inserting the new abstract states into the refinement hierarchy after splitting, the ids are assigned so that the state with the smaller value domain for the split variable is the right "node", because for each of these values a helper node is created in the refinement_hierarchy. 
affected areas of code: abstraction.cc call to refinement_hierarchy.split()
- useful commit hashes:
    5ceb1dae387841122fc3a5d055f0f17e8ec56112 ("[switch-neighbors-in-refinement-hierarchy] Use facts from smaller child state in refinement hierarchy.", 2021-11-14)

Cost Saturation:
In the function compute_saturated_costs() Scorpion no longer ignores unreachable states with infinite g-values to avoid computing these values. Only dead end states with infinite h-values get ignored.
- affected areas of code: one function in cost_saturation.cc
- useful commit hashes:
    8a481ed3e6868412026409c4441898eecbca6fa4 ("[cartesian-match-tree] Allow computing single-order SCPs.", 2020-06-23) - implementation
    67b12a2e92ab971ff95a06b1fb9f4acdc39f85b4 ("Remove use_fixed_time_limits option.", 2023-12-24) - added comment about the skipping of the g-values

Separate Rewiring from TransitionSystem
Move the logic for rewiring transitions in the refinement process into a separate class instead of keeping it inside the transition system class
- affected areas of code: parts where transitions are reconnected / computed 
  (abstraction, shortest_paths, transition_system) 

Separate Flaw class
Implement Flaw struct in a separate class not in cegar.cc. 
For the new flaw_search implementation (incremental search), the class was also restructured significantly. 
- affected areas of code : cegar, new flaw_search class

The current version of the Cartesian CEGAR implementation in Fast Downward has not been actively developed for some time and we want to start implementing some new features (like support for conditional effects, axioms, etc.) in the future. 
In the sprint in July 2026, we decided that it makes sense to first check which features have been added in Scorpion and which of those we can / want to port back into Fast Downward.