Differences between revisions 1 and 2
Revision 1 as of 2016-08-19 11:57:46
Size: 1879
Editor: XmlRpcBot
Comment:
Revision 2 as of 2016-08-23 13:07:33
Size: 1880
Editor: XmlRpcBot
Comment:
Deletions are marked like this. Additions are marked like this.
Line 19: Line 19:
 * ''update_option'' ({use_first, use_second, use_random}): When the merge tree is used within another merge strategy, howshould it be updated when a merge different to a merge from the tree is performed: choose among use_first, use_second, and use_random to choose which node of the tree should survive and represent the new merged index. Specify use_first (use_second) to let the node represententing the index that would have been merged earlier (later) survive. use_random chooses a random node.  * ''update_option'' ({use_first, use_second, use_random}): When the merge tree is used within another merge strategy, how should it be updated when a merge different to a merge from the tree is performed: choose among use_first, use_second, and use_random to choose which node of the tree should survive and represent the new merged index. Specify use_first (use_second) to let the node represententing the index that would have been merged earlier (later) survive. use_random chooses a random node.

This page describes the available merge trees that can be used to precompute a merge strategy, either for the entire task or a given subset of transition systems of a given factored transition system. Merge trees are typically used in the merge strategy of type 'precomputed', but they can also be used as fallback merge strategies in 'combined' merge strategies.

Linear merge trees

These merge trees implement several linear merge orders, which are described in the paper:

linear(random_seed=-1, update_option=use_random, variable_order=CG_GOAL_LEVEL)
  • random_seed (int [-1, infinity]): Set to -1 (default) to use the global random number generator. Set to any other value to use a local random number generator with the given seed.

  • update_option ({use_first, use_second, use_random}): When the merge tree is used within another merge strategy, how should it be updated when a merge different to a merge from the tree is performed: choose among use_first, use_second, and use_random to choose which node of the tree should survive and represent the new merged index. Specify use_first (use_second) to let the node represententing the index that would have been merged earlier (later) survive. use_random chooses a random node.

  • variable_order ({CG_GOAL_LEVEL, CG_GOAL_RANDOM, GOAL_CG_LEVEL, RANDOM, LEVEL, REVERSE_LEVEL}): the order in which atomic transition systems are merged

FastDownward: Doc/MergeTree (last edited 2021-08-06 16:41:03 by XmlRpcBot)