From 15b67c0ed6b912cde6f7b23ef60d21691cabb296 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Thu, 22 Oct 2026 08:40:31 +0200 Subject: [PATCH 1/9] refactor: streamline the argument descriptions + MiniZinc flag descriptions --- minizinc/pumpkin-for-proofs.msc | 58 ++++----- minizinc/pumpkin.msc | 58 ++++----- pumpkin-solver/src/bin/pumpkin-solver/main.rs | 116 +++++++----------- pumpkin-solver/src/bin/pumpkin-solver/msc.rs | 31 ++++- 4 files changed, 129 insertions(+), 134 deletions(-) diff --git a/minizinc/pumpkin-for-proofs.msc b/minizinc/pumpkin-for-proofs.msc index eec3a7eca..64fa2a8e0 100644 --- a/minizinc/pumpkin-for-proofs.msc +++ b/minizinc/pumpkin-for-proofs.msc @@ -15,175 +15,175 @@ "extraFlags": [ [ "--proof-path", - "The output path for the proof file.\n\nWhen solving a DIMACS instance, a DRAT proof is logged. In case of a FlatZinc model, a DRCP\nproof is logged.\n\nIn case of a DRCP proof, if the file extension ends with `.gz`, a gzipped proof will be\nproduced.", + "The output path for the proof file.", "string", "" ], [ "--proof-type", - "What type of proof to log.\n\nIf the `proof_path` option is not provided, this is ignored.", + "What type of proof to log. (values: scaffold, full; default: scaffold)", "opt:scaffold:full", "scaffold" ], [ "--learning-max-num-high-lbd-nogoods", - "The number of high-lbd learned nogoods that are kept in the database.\n\nLearned nogoods are kept based on the tiered system introduced in \"Improving\nSAT Solvers by Exploiting Empirical Characteristics of CDCL - Chanseok Oh (2016)\".\n\nPossible values: usize", + "The number of high-lbd learned nogoods that are kept in the database. (default: 20000)", "int:0:18446744073709551615", "20000" ], [ "--learning-max-num-mid-lbd-nogoods", - "The number of mid-lbd learned nogoods that are kept in the database.\n\nThis is based on the variation of the three-tiered system proposed in\n\"Improving Implementation of SAT Competitions 2017–2019 Winners\".\n\nPossible values: usize", + "The number of mid-lbd learned nogoods that are kept in the database. (default: 7000)", "int:0:18446744073709551615", "7000" ], [ "--learning-max-num-low-lbd-nogoods", - "The number of low-lbd learned nogoods that are kept in the database.\n\nThis is based on the variation of the three-tiered system proposed in\n\"Improving Implementation of SAT Competitions 2017–2019 Winners\".\n\nPossible values: usize", + "The number of low-lbd learned nogoods that are kept in the database. (default: 100000)", "int:0:18446744073709551615", "100000" ], [ "--learning-low-lbd-threshold", - "The treshold determining whether a learned nogood is \"low\" LBD.\n\n\"Low\" LBD nogood are kept around for longer since they are of better \"quality\".\n\nLearned nogoods are kept based on the tiered system introduced \"Improving\nSAT Solvers by Exploiting Empirical Characteristics of CDCL - Chanseok Oh (2016)\"\nwith the variation from \"Improving Implementation of SAT Competitions 2017–2019 Winners\".\n\nPossible values: u32", + "The treshold determining whether a learned nogood is \"low\" LBD. (default: 3)", "int:0:4294967295", "3" ], [ "--learning-high-lbd-threshold", - "The treshold determining whether a learned nogood is \"low\" LBD.\n\n\"High\" LBD nogood are kept around for a shorter amount of time since they are of bad\n\"quality\".\n\nLearned nogoods are kept based on the tiered system introduced \"Improving\nSAT Solvers by Exploiting Empirical Characteristics of CDCL - Chanseok Oh (2016)\"\nwith the variation from \"Improving Implementation of SAT Competitions 2017–2019 Winners\".\n\nPossible values: u32", + "The treshold determining whether a learned nogood is \"high\" LBD. (default: 7)", "int:0:4294967295", "7" ], [ "--recursive-minimisation", - "Decides whether learned clauses are minimised as a post-processing step after computing the\n1-UIP Minimisation is done; according to the idea proposed in \"Generalized Conflict-Clause\nStrengthening for Satisfiability Solvers - Allen van Gelder (2011)\".\n\nPossible values: bool", + "Decides whether learned clauses are minimised as a post-processing step after computing the 1-UIP Minimisation is done; according to the idea proposed in \"Generalized Conflict-Clause Strengthening for Satisfiability Solvers - Allen van Gelder (2011)\".", "bool", "false" ], [ "--no-iterative-minimisation", - "Decides whether to apply semantic minimisation during conflict analysis; according to the\nidea proposed in \"Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)\".\n\nIf this flag is present then the minimisation is turned on.\n\nPossible values: bool", + "Decides whether to apply semantic minimisation during conflict analysis; according to the idea proposed in \"Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)\".", "bool", "false" ], [ "--restart-sequence-generator-type", - "Decides the sequence based on which the restarts are performed.\n\n- The \"constant\" approach uses a constant number of conflicts before another restart is triggered - The \"geometric\" approach uses a geometrically increasing sequence - The \"luby\" approach uses a recursive sequence of the form 1, 1, 2, 1, 1, 2, 4, 1, 1, 2, 1, 1, 2, 4, 8, 1, 1, 2.... (see \"Optimal speedup of Las Vegas algorithms - Luby et al. (1993)\")\n\nTo be used in combination with \"--restarts-base-interval\".", + "Decides the sequence based on which the restarts are performed. (values: constant, geometric, luby; default: constant)", "opt:constant:geometric:luby", "constant" ], [ "--restart-base-interval", - "The base interval length is used as a multiplier to the restart sequence.\n- In the case of the \"constant\" restart sequence this argument indicates the constant which\n is used to determine when a restart occurs\n- For the \"geometric\" approach this argument indicates the starting value of the sequence\n- For the \"luby\" approach, the sequence is multiplied by this value\n\nFor example, constant restarts with base interval 50 means a restart is triggered every 50\nconflicts.\n\nPossible values: u64", + "The base interval length is used as a multiplier to the restart sequence. (default: 50)", "int:0:18446744073709551615", "50" ], [ "--restart-min-initial-conflicts", - "Indicates the minimum number of initial conflicts before the first restart can occur. This\nallows the solver to learn some things about the problem before a restart is allowed to\noccur.\n\nPossible values: u64", + "Indicates the minimum number of initial conflicts before the first restart can occur. (default: 10000)", "int:0:18446744073709551615", "10000" ], [ "--restart-lbd-coef", - "Used to determine if a restart should be forced (see \"Refining Restarts Strategies for SAT\nand UNSAT - Audemard and Simon (2012)\").\n\nThe state is \"bad\" if the current LBD value is much greater than\nthe global LBD average. A greater (lower) value for lbd-coef means a less (more) frequent\nrestart policy. If the long-term average LBD multiplied by this coefficient is lower\nthan the short-term average LBD then a restart is performed.\n\nPossible values: f64", + "Used to determine if a restart should be forced (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). (default: 1.25)", "float", "1.25" ], [ "--restart-num-assigned-coef", - "Used to determine if a restart should be blocked (see \"Refining Restarts Strategies for SAT\nand UNSAT - Audemard and Simon (2012)\").\n\nTo be used in combination with \"--restarts-num-assigned-window\".\n\nA restart is blocked if the number of assigned propositional variables is much greater than\nthe average number of assigned variables in the recent past. A greater (lower) value for\n\"--restart-num-assigned-coef\" means fewer (more) blocked restarts.\n\nPossible values: f64", + "Used to determine if a restart should be blocked (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). (default: 1.4)", "float", "1.4" ], [ "--restart-num-assigned-window", - "Used to determine the length of the recent past that should be considered when deciding on\nblocking restarts (see \"Refining Restarts Strategies for SAT\nand UNSAT - Audemard and Simon (2012)\").\n\nThe solver considers the last \"--restart_num_assigned_window\" conflicts as the reference\npoint for the number of assigned variables.\n\nPossible values: u64", + "Used to determine the length of the recent past that should be considered when deciding on blocking restarts (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). (default: 5000)", "int:0:18446744073709551615", "5000" ], [ "--restart-geometric-coef", - "The coefficient in the geometric sequence `x_i = x_{i-1} * \"--restart-geometric-coef\"`\nwhere `x_1 = \"--restarts-base-interval\"`. Used only if \"--restarts-sequence-generator\"\nis assigned to \"geometric\".\n\nPossible values: f64 (Optional)", + "The coefficient in the geometric sequence `x_i = x_{i-1} * \"--restart-geometric-coef\"` where `x_1 = \"--restarts-base-interval\"`. Used only if \"--restarts-sequence-generator\" is assigned to \"geometric\".", "float", "" ], [ "--omit-timestamp", - "If `--verbose` is enabled then this option removes the timestamp information from the log\nmessages. Note that this option will only take affect in the case of a (W)CNF instance.\n\nPossible values: bool", + "If `--verbose` is enabled then this option removes the timestamp information from the log messages (only applicable for (W)CNF instances).", "bool", "false" ], [ "--omit-call-site", - "If `--verbose` is enabled then this option removes the call site information from the log\nmessages. The call site is the file and line from which the message\noriginated. Note that this option will only take affect in the case of a (W)CNF instance.\n\nPossible values: bool", + "If `--verbose` is enabled then this option removes the call site information from the log messages (only applicable for (W)CNF instances).", "bool", "false" ], [ "--upper-bound-encoding", - "The encoding to use for the upper bound constraint in a MaxSAT optimisation problem.\n\n- The \"generalised-totalizer\" value specifies that the solver should use the Generalized Totalizer Encoding (see \"Generalized totalizer encoding for pseudo-boolean constraints - Saurabh et al. (2015)\") - The \"cardinality-network\" value specifies that the solver should use the Cardinality Network Encoding (see \"Cardinality networks: a theoretical and empirical study - Asín et al. (2011)\").", + "The encoding to use for the upper bound constraint in a MaxSAT optimisation problem. (values: generalized-totalizer, cardinality-network; default: generalized-totalizer)", "opt:generalized-totalizer:cardinality-network", "generalized-totalizer" ], [ "--no-restarts", - "Determines that no restarts are allowed by the solver.\n\nPossible values: bool", + "Determines that no restarts are allowed by the solver.", "bool", "false" ], [ "--conflict-resolver", - "Determines the conflict resolver", + "Determines the conflict resolver (values: no-learning, one-uip, all-decision, extended-cpip, bounds-extended-cpip; default: one-uip)", "opt:no-learning:one-uip:all-decision:extended-cpip:bounds-extended-cpip", "one-uip" ], [ "--cumulative-allow-holes", - "Determines that the cumulative propagator(s) are allowed to create holes in the domain.\n\nPossible values: bool", + "Determines that the cumulative propagator(s) are allowed to create holes in the domain.", "bool", "false" ], [ "--cumulative-explanation-type", - "Determines the type of explanation used by the cumulative propagator(s) to explain propagations/conflicts", + "Determines the type of explanation used by the cumulative propagator(s) to explain propagations/conflicts (values: naive, big-step, pointwise; default: pointwise)", "opt:naive:big-step:pointwise", "pointwise" ], [ "--cumulative-propagation-method", - "Determines the type of propagator which is used by the cumulative propagator(s) to propagate the constraint.\n\nCurrently, the solver only supports variations on time-tabling methods.", + "Determines the type of propagator which is used by the cumulative propagator(s) to propagate the constraint. (values: time-table-per-point, time-table-per-point-incremental, time-table-per-point-incremental-synchronised, time-table-over-interval, time-table-over-interval-incremental, time-table-over-interval-incremental-synchronised; default: time-table-over-interval-incremental)", "opt:time-table-per-point:time-table-per-point-incremental:time-table-per-point-incremental-synchronised:time-table-over-interval:time-table-over-interval-incremental:time-table-over-interval-incremental-synchronised", "time-table-over-interval-incremental" ], [ "--cumulative-single-profiles", - "Determines whether a single profiles are used generated when explaining a propagation for the cumulative constraint.\n\nPossible values: bool", + "Determines whether a single profiles are used generated when explaining a propagation for the cumulative constraint", "bool", "false" ], [ "--cumulative-incremental-backtracking", - "Determines whether incremental backtracking is applied or whether the cumulative propagators compute the time-table from scratch upon backtracking\n\nPossible values: bool", + "Determines whether incremental backtracking is applied or whether the cumulative propagators compute the time-table from scratch upon backtracking", "bool", "false" ], [ "--optimisation-strategy", - "Determine what type of optimisation strategy is used by the solver", + "Determine what type of optimisation strategy is used by the solver (values: linear-sat-unsat, linear-unsat-sat; default: linear-sat-unsat)", "opt:linear-sat-unsat:linear-unsat-sat", "linear-sat-unsat" ], [ "--memory-preallocated", - "The amount of memory (in MB) that is preallocated for storing nogoods", + "The amount of memory (in MB) that is preallocated for storing nogoods (default: 50)", "int:0:18446744073709551615", "50" ], [ "--nogood-priority", - "The priority of the nogood propagator", + "The priority of the nogood propagator (values: high, medium, low, very-low, ultra-low, lowest; default: very-low)", "opt:high:medium:low:very-low:ultra-low:lowest", "very-low" ] diff --git a/minizinc/pumpkin.msc b/minizinc/pumpkin.msc index ec1de9bed..1bd5923e8 100644 --- a/minizinc/pumpkin.msc +++ b/minizinc/pumpkin.msc @@ -15,175 +15,175 @@ "extraFlags": [ [ "--proof-path", - "The output path for the proof file.\n\nWhen solving a DIMACS instance, a DRAT proof is logged. In case of a FlatZinc model, a DRCP\nproof is logged.\n\nIn case of a DRCP proof, if the file extension ends with `.gz`, a gzipped proof will be\nproduced.", + "The output path for the proof file.", "string", "" ], [ "--proof-type", - "What type of proof to log.\n\nIf the `proof_path` option is not provided, this is ignored.", + "What type of proof to log. (values: scaffold, full; default: scaffold)", "opt:scaffold:full", "scaffold" ], [ "--learning-max-num-high-lbd-nogoods", - "The number of high-lbd learned nogoods that are kept in the database.\n\nLearned nogoods are kept based on the tiered system introduced in \"Improving\nSAT Solvers by Exploiting Empirical Characteristics of CDCL - Chanseok Oh (2016)\".\n\nPossible values: usize", + "The number of high-lbd learned nogoods that are kept in the database. (default: 20000)", "int:0:18446744073709551615", "20000" ], [ "--learning-max-num-mid-lbd-nogoods", - "The number of mid-lbd learned nogoods that are kept in the database.\n\nThis is based on the variation of the three-tiered system proposed in\n\"Improving Implementation of SAT Competitions 2017–2019 Winners\".\n\nPossible values: usize", + "The number of mid-lbd learned nogoods that are kept in the database. (default: 7000)", "int:0:18446744073709551615", "7000" ], [ "--learning-max-num-low-lbd-nogoods", - "The number of low-lbd learned nogoods that are kept in the database.\n\nThis is based on the variation of the three-tiered system proposed in\n\"Improving Implementation of SAT Competitions 2017–2019 Winners\".\n\nPossible values: usize", + "The number of low-lbd learned nogoods that are kept in the database. (default: 100000)", "int:0:18446744073709551615", "100000" ], [ "--learning-low-lbd-threshold", - "The treshold determining whether a learned nogood is \"low\" LBD.\n\n\"Low\" LBD nogood are kept around for longer since they are of better \"quality\".\n\nLearned nogoods are kept based on the tiered system introduced \"Improving\nSAT Solvers by Exploiting Empirical Characteristics of CDCL - Chanseok Oh (2016)\"\nwith the variation from \"Improving Implementation of SAT Competitions 2017–2019 Winners\".\n\nPossible values: u32", + "The treshold determining whether a learned nogood is \"low\" LBD. (default: 3)", "int:0:4294967295", "3" ], [ "--learning-high-lbd-threshold", - "The treshold determining whether a learned nogood is \"low\" LBD.\n\n\"High\" LBD nogood are kept around for a shorter amount of time since they are of bad\n\"quality\".\n\nLearned nogoods are kept based on the tiered system introduced \"Improving\nSAT Solvers by Exploiting Empirical Characteristics of CDCL - Chanseok Oh (2016)\"\nwith the variation from \"Improving Implementation of SAT Competitions 2017–2019 Winners\".\n\nPossible values: u32", + "The treshold determining whether a learned nogood is \"high\" LBD. (default: 7)", "int:0:4294967295", "7" ], [ "--recursive-minimisation", - "Decides whether learned clauses are minimised as a post-processing step after computing the\n1-UIP Minimisation is done; according to the idea proposed in \"Generalized Conflict-Clause\nStrengthening for Satisfiability Solvers - Allen van Gelder (2011)\".\n\nPossible values: bool", + "Decides whether learned clauses are minimised as a post-processing step after computing the 1-UIP Minimisation is done; according to the idea proposed in \"Generalized Conflict-Clause Strengthening for Satisfiability Solvers - Allen van Gelder (2011)\".", "bool", "false" ], [ "--no-iterative-minimisation", - "Decides whether to apply semantic minimisation during conflict analysis; according to the\nidea proposed in \"Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)\".\n\nIf this flag is present then the minimisation is turned on.\n\nPossible values: bool", + "Decides whether to apply semantic minimisation during conflict analysis; according to the idea proposed in \"Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)\".", "bool", "false" ], [ "--restart-sequence-generator-type", - "Decides the sequence based on which the restarts are performed.\n\n- The \"constant\" approach uses a constant number of conflicts before another restart is triggered - The \"geometric\" approach uses a geometrically increasing sequence - The \"luby\" approach uses a recursive sequence of the form 1, 1, 2, 1, 1, 2, 4, 1, 1, 2, 1, 1, 2, 4, 8, 1, 1, 2.... (see \"Optimal speedup of Las Vegas algorithms - Luby et al. (1993)\")\n\nTo be used in combination with \"--restarts-base-interval\".", + "Decides the sequence based on which the restarts are performed. (values: constant, geometric, luby; default: constant)", "opt:constant:geometric:luby", "constant" ], [ "--restart-base-interval", - "The base interval length is used as a multiplier to the restart sequence.\n- In the case of the \"constant\" restart sequence this argument indicates the constant which\n is used to determine when a restart occurs\n- For the \"geometric\" approach this argument indicates the starting value of the sequence\n- For the \"luby\" approach, the sequence is multiplied by this value\n\nFor example, constant restarts with base interval 50 means a restart is triggered every 50\nconflicts.\n\nPossible values: u64", + "The base interval length is used as a multiplier to the restart sequence. (default: 50)", "int:0:18446744073709551615", "50" ], [ "--restart-min-initial-conflicts", - "Indicates the minimum number of initial conflicts before the first restart can occur. This\nallows the solver to learn some things about the problem before a restart is allowed to\noccur.\n\nPossible values: u64", + "Indicates the minimum number of initial conflicts before the first restart can occur. (default: 10000)", "int:0:18446744073709551615", "10000" ], [ "--restart-lbd-coef", - "Used to determine if a restart should be forced (see \"Refining Restarts Strategies for SAT\nand UNSAT - Audemard and Simon (2012)\").\n\nThe state is \"bad\" if the current LBD value is much greater than\nthe global LBD average. A greater (lower) value for lbd-coef means a less (more) frequent\nrestart policy. If the long-term average LBD multiplied by this coefficient is lower\nthan the short-term average LBD then a restart is performed.\n\nPossible values: f64", + "Used to determine if a restart should be forced (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). (default: 1.25)", "float", "1.25" ], [ "--restart-num-assigned-coef", - "Used to determine if a restart should be blocked (see \"Refining Restarts Strategies for SAT\nand UNSAT - Audemard and Simon (2012)\").\n\nTo be used in combination with \"--restarts-num-assigned-window\".\n\nA restart is blocked if the number of assigned propositional variables is much greater than\nthe average number of assigned variables in the recent past. A greater (lower) value for\n\"--restart-num-assigned-coef\" means fewer (more) blocked restarts.\n\nPossible values: f64", + "Used to determine if a restart should be blocked (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). (default: 1.4)", "float", "1.4" ], [ "--restart-num-assigned-window", - "Used to determine the length of the recent past that should be considered when deciding on\nblocking restarts (see \"Refining Restarts Strategies for SAT\nand UNSAT - Audemard and Simon (2012)\").\n\nThe solver considers the last \"--restart_num_assigned_window\" conflicts as the reference\npoint for the number of assigned variables.\n\nPossible values: u64", + "Used to determine the length of the recent past that should be considered when deciding on blocking restarts (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). (default: 5000)", "int:0:18446744073709551615", "5000" ], [ "--restart-geometric-coef", - "The coefficient in the geometric sequence `x_i = x_{i-1} * \"--restart-geometric-coef\"`\nwhere `x_1 = \"--restarts-base-interval\"`. Used only if \"--restarts-sequence-generator\"\nis assigned to \"geometric\".\n\nPossible values: f64 (Optional)", + "The coefficient in the geometric sequence `x_i = x_{i-1} * \"--restart-geometric-coef\"` where `x_1 = \"--restarts-base-interval\"`. Used only if \"--restarts-sequence-generator\" is assigned to \"geometric\".", "float", "" ], [ "--omit-timestamp", - "If `--verbose` is enabled then this option removes the timestamp information from the log\nmessages. Note that this option will only take affect in the case of a (W)CNF instance.\n\nPossible values: bool", + "If `--verbose` is enabled then this option removes the timestamp information from the log messages (only applicable for (W)CNF instances).", "bool", "false" ], [ "--omit-call-site", - "If `--verbose` is enabled then this option removes the call site information from the log\nmessages. The call site is the file and line from which the message\noriginated. Note that this option will only take affect in the case of a (W)CNF instance.\n\nPossible values: bool", + "If `--verbose` is enabled then this option removes the call site information from the log messages (only applicable for (W)CNF instances).", "bool", "false" ], [ "--upper-bound-encoding", - "The encoding to use for the upper bound constraint in a MaxSAT optimisation problem.\n\n- The \"generalised-totalizer\" value specifies that the solver should use the Generalized Totalizer Encoding (see \"Generalized totalizer encoding for pseudo-boolean constraints - Saurabh et al. (2015)\") - The \"cardinality-network\" value specifies that the solver should use the Cardinality Network Encoding (see \"Cardinality networks: a theoretical and empirical study - Asín et al. (2011)\").", + "The encoding to use for the upper bound constraint in a MaxSAT optimisation problem. (values: generalized-totalizer, cardinality-network; default: generalized-totalizer)", "opt:generalized-totalizer:cardinality-network", "generalized-totalizer" ], [ "--no-restarts", - "Determines that no restarts are allowed by the solver.\n\nPossible values: bool", + "Determines that no restarts are allowed by the solver.", "bool", "false" ], [ "--conflict-resolver", - "Determines the conflict resolver", + "Determines the conflict resolver (values: no-learning, one-uip, all-decision, extended-cpip, bounds-extended-cpip; default: one-uip)", "opt:no-learning:one-uip:all-decision:extended-cpip:bounds-extended-cpip", "one-uip" ], [ "--cumulative-allow-holes", - "Determines that the cumulative propagator(s) are allowed to create holes in the domain.\n\nPossible values: bool", + "Determines that the cumulative propagator(s) are allowed to create holes in the domain.", "bool", "false" ], [ "--cumulative-explanation-type", - "Determines the type of explanation used by the cumulative propagator(s) to explain propagations/conflicts", + "Determines the type of explanation used by the cumulative propagator(s) to explain propagations/conflicts (values: naive, big-step, pointwise; default: pointwise)", "opt:naive:big-step:pointwise", "pointwise" ], [ "--cumulative-propagation-method", - "Determines the type of propagator which is used by the cumulative propagator(s) to propagate the constraint.\n\nCurrently, the solver only supports variations on time-tabling methods.", + "Determines the type of propagator which is used by the cumulative propagator(s) to propagate the constraint. (values: time-table-per-point, time-table-per-point-incremental, time-table-per-point-incremental-synchronised, time-table-over-interval, time-table-over-interval-incremental, time-table-over-interval-incremental-synchronised; default: time-table-over-interval-incremental)", "opt:time-table-per-point:time-table-per-point-incremental:time-table-per-point-incremental-synchronised:time-table-over-interval:time-table-over-interval-incremental:time-table-over-interval-incremental-synchronised", "time-table-over-interval-incremental" ], [ "--cumulative-single-profiles", - "Determines whether a single profiles are used generated when explaining a propagation for the cumulative constraint.\n\nPossible values: bool", + "Determines whether a single profiles are used generated when explaining a propagation for the cumulative constraint", "bool", "false" ], [ "--cumulative-incremental-backtracking", - "Determines whether incremental backtracking is applied or whether the cumulative propagators compute the time-table from scratch upon backtracking\n\nPossible values: bool", + "Determines whether incremental backtracking is applied or whether the cumulative propagators compute the time-table from scratch upon backtracking", "bool", "false" ], [ "--optimisation-strategy", - "Determine what type of optimisation strategy is used by the solver", + "Determine what type of optimisation strategy is used by the solver (values: linear-sat-unsat, linear-unsat-sat; default: linear-sat-unsat)", "opt:linear-sat-unsat:linear-unsat-sat", "linear-sat-unsat" ], [ "--memory-preallocated", - "The amount of memory (in MB) that is preallocated for storing nogoods", + "The amount of memory (in MB) that is preallocated for storing nogoods (default: 50)", "int:0:18446744073709551615", "50" ], [ "--nogood-priority", - "The priority of the nogood propagator", + "The priority of the nogood propagator (values: high, medium, low, very-low, ultra-low, lowest; default: very-low)", "opt:high:medium:low:very-low:ultra-low:lowest", "very-low" ] diff --git a/pumpkin-solver/src/bin/pumpkin-solver/main.rs b/pumpkin-solver/src/bin/pumpkin-solver/main.rs index e5f9b53d7..656420c54 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/main.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/main.rs @@ -87,7 +87,7 @@ struct Args { /// /// In case of a DRCP proof, if the file extension ends with `.gz`, a gzipped proof will be /// produced. - #[arg(long, verbatim_doc_comment)] + #[arg(long, verbatim_doc_comment, value_name = "PATH")] proof_path: Option, /// What type of proof to log. @@ -100,12 +100,11 @@ struct Args { /// /// Learned nogoods are kept based on the tiered system introduced in "Improving /// SAT Solvers by Exploiting Empirical Characteristics of CDCL - Chanseok Oh (2016)". - /// - /// Possible values: usize #[arg( long = "learning-max-num-high-lbd-nogoods", default_value_t = 20_000, - verbatim_doc_comment + verbatim_doc_comment, + value_name = "usize" )] learning_max_num_high_lbd_nogoods: usize, @@ -113,12 +112,11 @@ struct Args { /// /// This is based on the variation of the three-tiered system proposed in /// "Improving Implementation of SAT Competitions 2017–2019 Winners". - /// - /// Possible values: usize #[arg( long = "learning-max-num-mid-lbd-nogoods", default_value_t = 7000, - verbatim_doc_comment + verbatim_doc_comment, + value_name = "usize" )] learning_max_num_mid_lbd_nogoods: usize, @@ -126,12 +124,11 @@ struct Args { /// /// This is based on the variation of the three-tiered system proposed in /// "Improving Implementation of SAT Competitions 2017–2019 Winners". - /// - /// Possible values: usize #[arg( long = "learning-max-num-low-lbd-nogoods", default_value_t = 100_000, - verbatim_doc_comment + verbatim_doc_comment, + value_name = "usize" )] learning_max_num_low_lbd_nogoods: usize, @@ -142,16 +139,15 @@ struct Args { /// Learned nogoods are kept based on the tiered system introduced "Improving /// SAT Solvers by Exploiting Empirical Characteristics of CDCL - Chanseok Oh (2016)" /// with the variation from "Improving Implementation of SAT Competitions 2017–2019 Winners". - /// - /// Possible values: u32 #[arg( long = "learning-low-lbd-threshold", default_value_t = 3, - verbatim_doc_comment + verbatim_doc_comment, + value_name = "u32" )] learning_low_lbd_threshold: u32, - /// The treshold determining whether a learned nogood is "low" LBD. + /// The treshold determining whether a learned nogood is "high" LBD. /// /// "High" LBD nogood are kept around for a shorter amount of time since they are of bad /// "quality". @@ -159,20 +155,17 @@ struct Args { /// Learned nogoods are kept based on the tiered system introduced "Improving /// SAT Solvers by Exploiting Empirical Characteristics of CDCL - Chanseok Oh (2016)" /// with the variation from "Improving Implementation of SAT Competitions 2017–2019 Winners". - /// - /// Possible values: u32 #[arg( long = "learning-high-lbd-threshold", default_value_t = 7, - verbatim_doc_comment + verbatim_doc_comment, + value_name = "u32" )] learning_high_lbd_threshold: u32, /// Decides whether learned clauses are minimised as a post-processing step after computing the /// 1-UIP Minimisation is done; according to the idea proposed in "Generalized Conflict-Clause /// Strengthening for Satisfiability Solvers - Allen van Gelder (2011)". - /// - /// Possible values: bool #[arg(long = "recursive-minimisation", verbatim_doc_comment)] recursive_minimisation: bool, @@ -180,8 +173,6 @@ struct Args { /// idea proposed in "Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)". /// /// If this flag is present then the minimisation is turned on. - /// - /// Possible values: bool #[arg(long = "no-iterative-minimisation", verbatim_doc_comment)] no_iterative_minimisation: bool, @@ -206,24 +197,23 @@ struct Args { /// /// For example, constant restarts with base interval 50 means a restart is triggered every 50 /// conflicts. - /// - /// Possible values: u64 #[arg( long = "restart-base-interval", default_value_t = 50, - verbatim_doc_comment + verbatim_doc_comment, + value_name = "u64" )] restart_base_interval: u64, - /// Indicates the minimum number of initial conflicts before the first restart can occur. This - /// allows the solver to learn some things about the problem before a restart is allowed to - /// occur. + /// Indicates the minimum number of initial conflicts before the first restart can occur. /// - /// Possible values: u64 + /// This allows the solver to learn some things about the problem before a restart is allowed + /// to occur. #[arg( long = "restart-min-initial-conflicts", default_value_t = 10000, - verbatim_doc_comment + verbatim_doc_comment, + value_name = "u64" )] restart_min_num_conflicts_before_first_restart: u64, @@ -234,12 +224,11 @@ struct Args { /// the global LBD average. A greater (lower) value for lbd-coef means a less (more) frequent /// restart policy. If the long-term average LBD multiplied by this coefficient is lower /// than the short-term average LBD then a restart is performed. - /// - /// Possible values: f64 #[arg( long = "restart-lbd-coef", default_value_t = 1.25, - verbatim_doc_comment + verbatim_doc_comment, + value_name = "f64" )] restart_lbd_coef: f64, @@ -251,12 +240,11 @@ struct Args { /// A restart is blocked if the number of assigned propositional variables is much greater than /// the average number of assigned variables in the recent past. A greater (lower) value for /// "--restart-num-assigned-coef" means fewer (more) blocked restarts. - /// - /// Possible values: f64 #[arg( long = "restart-num-assigned-coef", default_value_t = 1.4, - verbatim_doc_comment + verbatim_doc_comment, + value_name = "f64" )] restart_num_assigned_coef: f64, @@ -266,40 +254,43 @@ struct Args { /// /// The solver considers the last "--restart_num_assigned_window" conflicts as the reference /// point for the number of assigned variables. - /// - /// Possible values: u64 #[arg( long = "restart-num-assigned-window", default_value_t = 5000, - verbatim_doc_comment + verbatim_doc_comment, + value_name = "u64" )] restart_num_assigned_window: u64, /// The coefficient in the geometric sequence `x_i = x_{i-1} * "--restart-geometric-coef"` /// where `x_1 = "--restarts-base-interval"`. Used only if "--restarts-sequence-generator" /// is assigned to "geometric". - /// - /// Possible values: f64 (Optional) - #[arg(long = "restart-geometric-coef", verbatim_doc_comment)] + #[arg( + long = "restart-geometric-coef", + verbatim_doc_comment, + value_name = "f64" + )] restart_geometric_coef: Option, /// The time budget for the solver, given in milliseconds. - /// - /// Possible values: u64 (Optional) - #[arg(short = 't', long = "time-limit", verbatim_doc_comment)] + #[arg( + short = 't', + long = "time-limit", + verbatim_doc_comment, + value_name = "u64" + )] time_limit: Option, /// The random seed to use for the Pseudo Random Number Generator. /// /// Randomisation can be used for aspects such as the variable/value generator or initial /// ordering of variables. - /// - /// Possible values: u64 #[arg( short = 'r', long = "random-seed", default_value_t = 42, - verbatim_doc_comment + verbatim_doc_comment, + value_name = "u64" )] random_seed: u64, @@ -308,14 +299,10 @@ struct Args { /// For printing statistics see the option "--log-statistics", and for printing all solutions /// (in case of a satisfaction problem) or printing solutions of increasing quality (in case of /// an optimization problem) see the option "--all-solutions". - /// - /// Possible values: bool #[arg(short = 'v', long = "verbose", verbatim_doc_comment)] verbose: bool, /// Enables logging of statistics from the solver. - /// - /// Possible values: bool #[arg(short = 's', long = "log-statistics", verbatim_doc_comment)] log_statistics: bool, @@ -324,8 +311,6 @@ struct Args { /// /// See the MiniZinc specification () /// for more information. - /// - /// Possible values: bool #[arg(short = 'f', long = "free-search", verbatim_doc_comment)] free_search: bool, @@ -335,23 +320,18 @@ struct Args { /// /// See the MiniZinc specification () /// for more information. - /// - /// Possible values: bool #[arg(short = 'a', long = "all-solutions", verbatim_doc_comment)] all_solutions: bool, /// If `--verbose` is enabled then this option removes the timestamp information from the log - /// messages. Note that this option will only take affect in the case of a (W)CNF instance. - /// - /// Possible values: bool + /// messages (only applicable for (W)CNF instances). #[arg(long = "omit-timestamp", verbatim_doc_comment)] omit_timestamp: bool, /// If `--verbose` is enabled then this option removes the call site information from the log - /// messages. The call site is the file and line from which the message - /// originated. Note that this option will only take affect in the case of a (W)CNF instance. + /// messages (only applicable for (W)CNF instances). /// - /// Possible values: bool + /// The call site is the file and line from which the message originated. #[arg(long = "omit-call-site", default_value_t = false, verbatim_doc_comment)] omit_call_site: bool, @@ -367,8 +347,6 @@ struct Args { upper_bound_encoding: PseudoBooleanEncoding, /// Determines that no restarts are allowed by the solver. - /// - /// Possible values: bool #[arg(long = "no-restarts", verbatim_doc_comment)] no_restarts: bool, @@ -377,8 +355,6 @@ struct Args { conflict_resolver: ConflictResolverType, /// Determines that the cumulative propagator(s) are allowed to create holes in the domain. - /// - /// Possible values: bool #[arg(long = "cumulative-allow-holes", verbatim_doc_comment)] cumulative_allow_holes: bool, @@ -396,15 +372,11 @@ struct Args { /// Determines whether a single profiles are used generated when explaining a propagation for /// the cumulative constraint. - /// - /// Possible values: bool #[arg(long = "cumulative-single-profiles")] cumulative_single_profiles: bool, /// Determines whether incremental backtracking is applied or whether the cumulative /// propagators compute the time-table from scratch upon backtracking - /// - /// Possible values: bool #[arg(long = "cumulative-incremental-backtracking")] cumulative_incremental_backtracking: bool, @@ -413,7 +385,11 @@ struct Args { optimisation_strategy: OptimisationStrategy, /// The amount of memory (in MB) that is preallocated for storing nogoods. - #[arg(long = "memory-preallocated", default_value_t = 50)] + #[arg( + long = "memory-preallocated", + default_value_t = 50, + value_name = "usize" + )] memory_preallocated: usize, /// The priority of the nogood propagator. diff --git a/pumpkin-solver/src/bin/pumpkin-solver/msc.rs b/pumpkin-solver/src/bin/pumpkin-solver/msc.rs index 6f3b704ef..2a8c63088 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/msc.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/msc.rs @@ -82,10 +82,10 @@ fn extra_flag(arg: &Arg) -> Value { (None, Some(short)) => format!("-{short}"), (None, None) => unreachable!("non-positional arguments have a long or short flag"), }; - let description = arg + let summary = arg .get_long_help() .or(arg.get_help()) - .map(|help| help.to_string()) + .map(|help| summary(&help.to_string())) .unwrap_or_default(); let default = arg @@ -95,8 +95,8 @@ fn extra_flag(arg: &Arg) -> Value { .collect::>() .join(","); - let (flag_type, default) = if matches!(arg.get_action(), ArgAction::SetTrue) { - ("bool".to_owned(), "false".to_owned()) + let (flag_type, default, description) = if matches!(arg.get_action(), ArgAction::SetTrue) { + ("bool".to_owned(), "false".to_owned(), summary) } else if !arg.get_possible_values().is_empty() { let values = arg .get_possible_values() @@ -104,14 +104,33 @@ fn extra_flag(arg: &Arg) -> Value { .filter(|value| !value.is_hide_set()) .map(|value| value.get_name().to_owned()) .collect::>(); - (format!("opt:{}", values.join(":")), default) + let description = format!( + "{summary} (values: {}; default: {default})", + values.join(", ") + ); + (format!("opt:{}", values.join(":")), default, description) + } else if default.is_empty() { + (value_type(arg), default, summary) } else { - (value_type(arg), default) + let description = format!("{summary} (default: {default})"); + (value_type(arg), default, description) }; json!([flag, description, flag_type, default]) } +/// Condenses the help of an argument into a single line, such that it is displayed nicely by +/// `minizinc --help`, which does not indent the continuation lines of a description. +/// +/// The summary is the first paragraph of the help, up to the start of any list. +fn summary(help: &str) -> String { + help.lines() + .map(str::trim) + .take_while(|line| !line.is_empty() && !line.starts_with("- ")) + .collect::>() + .join(" ") +} + /// Returns the MiniZinc type corresponding to the type of value which is parsed for `arg`. fn value_type(arg: &Arg) -> String { let type_id = arg.get_value_parser().type_id(); From bbdc7252f7622a101e01c3543399fe1108687021 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Thu, 22 Oct 2026 09:00:54 +0200 Subject: [PATCH 2/9] refactor: clap-style defaults and possible values uses int --- minizinc/pumpkin-for-proofs.msc | 42 ++++++++++---------- minizinc/pumpkin.msc | 42 ++++++++++---------- pumpkin-solver/src/bin/pumpkin-solver/msc.rs | 18 ++++++--- 3 files changed, 55 insertions(+), 47 deletions(-) diff --git a/minizinc/pumpkin-for-proofs.msc b/minizinc/pumpkin-for-proofs.msc index 64fa2a8e0..1258eff66 100644 --- a/minizinc/pumpkin-for-proofs.msc +++ b/minizinc/pumpkin-for-proofs.msc @@ -15,43 +15,43 @@ "extraFlags": [ [ "--proof-path", - "The output path for the proof file.", + "The output path for the proof file. [possible values: string]", "string", "" ], [ "--proof-type", - "What type of proof to log. (values: scaffold, full; default: scaffold)", + "What type of proof to log. [default: scaffold] [possible values: scaffold, full]", "opt:scaffold:full", "scaffold" ], [ "--learning-max-num-high-lbd-nogoods", - "The number of high-lbd learned nogoods that are kept in the database. (default: 20000)", + "The number of high-lbd learned nogoods that are kept in the database. [default: 20000] [possible values: int]", "int:0:18446744073709551615", "20000" ], [ "--learning-max-num-mid-lbd-nogoods", - "The number of mid-lbd learned nogoods that are kept in the database. (default: 7000)", + "The number of mid-lbd learned nogoods that are kept in the database. [default: 7000] [possible values: int]", "int:0:18446744073709551615", "7000" ], [ "--learning-max-num-low-lbd-nogoods", - "The number of low-lbd learned nogoods that are kept in the database. (default: 100000)", + "The number of low-lbd learned nogoods that are kept in the database. [default: 100000] [possible values: int]", "int:0:18446744073709551615", "100000" ], [ "--learning-low-lbd-threshold", - "The treshold determining whether a learned nogood is \"low\" LBD. (default: 3)", + "The treshold determining whether a learned nogood is \"low\" LBD. [default: 3] [possible values: int]", "int:0:4294967295", "3" ], [ "--learning-high-lbd-threshold", - "The treshold determining whether a learned nogood is \"high\" LBD. (default: 7)", + "The treshold determining whether a learned nogood is \"high\" LBD. [default: 7] [possible values: int]", "int:0:4294967295", "7" ], @@ -69,43 +69,43 @@ ], [ "--restart-sequence-generator-type", - "Decides the sequence based on which the restarts are performed. (values: constant, geometric, luby; default: constant)", + "Decides the sequence based on which the restarts are performed. [default: constant] [possible values: constant, geometric, luby]", "opt:constant:geometric:luby", "constant" ], [ "--restart-base-interval", - "The base interval length is used as a multiplier to the restart sequence. (default: 50)", + "The base interval length is used as a multiplier to the restart sequence. [default: 50] [possible values: int]", "int:0:18446744073709551615", "50" ], [ "--restart-min-initial-conflicts", - "Indicates the minimum number of initial conflicts before the first restart can occur. (default: 10000)", + "Indicates the minimum number of initial conflicts before the first restart can occur. [default: 10000] [possible values: int]", "int:0:18446744073709551615", "10000" ], [ "--restart-lbd-coef", - "Used to determine if a restart should be forced (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). (default: 1.25)", + "Used to determine if a restart should be forced (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). [default: 1.25] [possible values: float]", "float", "1.25" ], [ "--restart-num-assigned-coef", - "Used to determine if a restart should be blocked (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). (default: 1.4)", + "Used to determine if a restart should be blocked (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). [default: 1.4] [possible values: float]", "float", "1.4" ], [ "--restart-num-assigned-window", - "Used to determine the length of the recent past that should be considered when deciding on blocking restarts (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). (default: 5000)", + "Used to determine the length of the recent past that should be considered when deciding on blocking restarts (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). [default: 5000] [possible values: int]", "int:0:18446744073709551615", "5000" ], [ "--restart-geometric-coef", - "The coefficient in the geometric sequence `x_i = x_{i-1} * \"--restart-geometric-coef\"` where `x_1 = \"--restarts-base-interval\"`. Used only if \"--restarts-sequence-generator\" is assigned to \"geometric\".", + "The coefficient in the geometric sequence `x_i = x_{i-1} * \"--restart-geometric-coef\"` where `x_1 = \"--restarts-base-interval\"`. Used only if \"--restarts-sequence-generator\" is assigned to \"geometric\". [possible values: float]", "float", "" ], @@ -123,7 +123,7 @@ ], [ "--upper-bound-encoding", - "The encoding to use for the upper bound constraint in a MaxSAT optimisation problem. (values: generalized-totalizer, cardinality-network; default: generalized-totalizer)", + "The encoding to use for the upper bound constraint in a MaxSAT optimisation problem. [default: generalized-totalizer] [possible values: generalized-totalizer, cardinality-network]", "opt:generalized-totalizer:cardinality-network", "generalized-totalizer" ], @@ -135,7 +135,7 @@ ], [ "--conflict-resolver", - "Determines the conflict resolver (values: no-learning, one-uip, all-decision, extended-cpip, bounds-extended-cpip; default: one-uip)", + "Determines the conflict resolver [default: one-uip] [possible values: no-learning, one-uip, all-decision, extended-cpip, bounds-extended-cpip]", "opt:no-learning:one-uip:all-decision:extended-cpip:bounds-extended-cpip", "one-uip" ], @@ -147,13 +147,13 @@ ], [ "--cumulative-explanation-type", - "Determines the type of explanation used by the cumulative propagator(s) to explain propagations/conflicts (values: naive, big-step, pointwise; default: pointwise)", + "Determines the type of explanation used by the cumulative propagator(s) to explain propagations/conflicts [default: pointwise] [possible values: naive, big-step, pointwise]", "opt:naive:big-step:pointwise", "pointwise" ], [ "--cumulative-propagation-method", - "Determines the type of propagator which is used by the cumulative propagator(s) to propagate the constraint. (values: time-table-per-point, time-table-per-point-incremental, time-table-per-point-incremental-synchronised, time-table-over-interval, time-table-over-interval-incremental, time-table-over-interval-incremental-synchronised; default: time-table-over-interval-incremental)", + "Determines the type of propagator which is used by the cumulative propagator(s) to propagate the constraint. [default: time-table-over-interval-incremental] [possible values: time-table-per-point, time-table-per-point-incremental, time-table-per-point-incremental-synchronised, time-table-over-interval, time-table-over-interval-incremental, time-table-over-interval-incremental-synchronised]", "opt:time-table-per-point:time-table-per-point-incremental:time-table-per-point-incremental-synchronised:time-table-over-interval:time-table-over-interval-incremental:time-table-over-interval-incremental-synchronised", "time-table-over-interval-incremental" ], @@ -171,19 +171,19 @@ ], [ "--optimisation-strategy", - "Determine what type of optimisation strategy is used by the solver (values: linear-sat-unsat, linear-unsat-sat; default: linear-sat-unsat)", + "Determine what type of optimisation strategy is used by the solver [default: linear-sat-unsat] [possible values: linear-sat-unsat, linear-unsat-sat]", "opt:linear-sat-unsat:linear-unsat-sat", "linear-sat-unsat" ], [ "--memory-preallocated", - "The amount of memory (in MB) that is preallocated for storing nogoods (default: 50)", + "The amount of memory (in MB) that is preallocated for storing nogoods [default: 50] [possible values: int]", "int:0:18446744073709551615", "50" ], [ "--nogood-priority", - "The priority of the nogood propagator (values: high, medium, low, very-low, ultra-low, lowest; default: very-low)", + "The priority of the nogood propagator [default: very-low] [possible values: high, medium, low, very-low, ultra-low, lowest]", "opt:high:medium:low:very-low:ultra-low:lowest", "very-low" ] diff --git a/minizinc/pumpkin.msc b/minizinc/pumpkin.msc index 1bd5923e8..2e9a55def 100644 --- a/minizinc/pumpkin.msc +++ b/minizinc/pumpkin.msc @@ -15,43 +15,43 @@ "extraFlags": [ [ "--proof-path", - "The output path for the proof file.", + "The output path for the proof file. [possible values: string]", "string", "" ], [ "--proof-type", - "What type of proof to log. (values: scaffold, full; default: scaffold)", + "What type of proof to log. [default: scaffold] [possible values: scaffold, full]", "opt:scaffold:full", "scaffold" ], [ "--learning-max-num-high-lbd-nogoods", - "The number of high-lbd learned nogoods that are kept in the database. (default: 20000)", + "The number of high-lbd learned nogoods that are kept in the database. [default: 20000] [possible values: int]", "int:0:18446744073709551615", "20000" ], [ "--learning-max-num-mid-lbd-nogoods", - "The number of mid-lbd learned nogoods that are kept in the database. (default: 7000)", + "The number of mid-lbd learned nogoods that are kept in the database. [default: 7000] [possible values: int]", "int:0:18446744073709551615", "7000" ], [ "--learning-max-num-low-lbd-nogoods", - "The number of low-lbd learned nogoods that are kept in the database. (default: 100000)", + "The number of low-lbd learned nogoods that are kept in the database. [default: 100000] [possible values: int]", "int:0:18446744073709551615", "100000" ], [ "--learning-low-lbd-threshold", - "The treshold determining whether a learned nogood is \"low\" LBD. (default: 3)", + "The treshold determining whether a learned nogood is \"low\" LBD. [default: 3] [possible values: int]", "int:0:4294967295", "3" ], [ "--learning-high-lbd-threshold", - "The treshold determining whether a learned nogood is \"high\" LBD. (default: 7)", + "The treshold determining whether a learned nogood is \"high\" LBD. [default: 7] [possible values: int]", "int:0:4294967295", "7" ], @@ -69,43 +69,43 @@ ], [ "--restart-sequence-generator-type", - "Decides the sequence based on which the restarts are performed. (values: constant, geometric, luby; default: constant)", + "Decides the sequence based on which the restarts are performed. [default: constant] [possible values: constant, geometric, luby]", "opt:constant:geometric:luby", "constant" ], [ "--restart-base-interval", - "The base interval length is used as a multiplier to the restart sequence. (default: 50)", + "The base interval length is used as a multiplier to the restart sequence. [default: 50] [possible values: int]", "int:0:18446744073709551615", "50" ], [ "--restart-min-initial-conflicts", - "Indicates the minimum number of initial conflicts before the first restart can occur. (default: 10000)", + "Indicates the minimum number of initial conflicts before the first restart can occur. [default: 10000] [possible values: int]", "int:0:18446744073709551615", "10000" ], [ "--restart-lbd-coef", - "Used to determine if a restart should be forced (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). (default: 1.25)", + "Used to determine if a restart should be forced (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). [default: 1.25] [possible values: float]", "float", "1.25" ], [ "--restart-num-assigned-coef", - "Used to determine if a restart should be blocked (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). (default: 1.4)", + "Used to determine if a restart should be blocked (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). [default: 1.4] [possible values: float]", "float", "1.4" ], [ "--restart-num-assigned-window", - "Used to determine the length of the recent past that should be considered when deciding on blocking restarts (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). (default: 5000)", + "Used to determine the length of the recent past that should be considered when deciding on blocking restarts (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). [default: 5000] [possible values: int]", "int:0:18446744073709551615", "5000" ], [ "--restart-geometric-coef", - "The coefficient in the geometric sequence `x_i = x_{i-1} * \"--restart-geometric-coef\"` where `x_1 = \"--restarts-base-interval\"`. Used only if \"--restarts-sequence-generator\" is assigned to \"geometric\".", + "The coefficient in the geometric sequence `x_i = x_{i-1} * \"--restart-geometric-coef\"` where `x_1 = \"--restarts-base-interval\"`. Used only if \"--restarts-sequence-generator\" is assigned to \"geometric\". [possible values: float]", "float", "" ], @@ -123,7 +123,7 @@ ], [ "--upper-bound-encoding", - "The encoding to use for the upper bound constraint in a MaxSAT optimisation problem. (values: generalized-totalizer, cardinality-network; default: generalized-totalizer)", + "The encoding to use for the upper bound constraint in a MaxSAT optimisation problem. [default: generalized-totalizer] [possible values: generalized-totalizer, cardinality-network]", "opt:generalized-totalizer:cardinality-network", "generalized-totalizer" ], @@ -135,7 +135,7 @@ ], [ "--conflict-resolver", - "Determines the conflict resolver (values: no-learning, one-uip, all-decision, extended-cpip, bounds-extended-cpip; default: one-uip)", + "Determines the conflict resolver [default: one-uip] [possible values: no-learning, one-uip, all-decision, extended-cpip, bounds-extended-cpip]", "opt:no-learning:one-uip:all-decision:extended-cpip:bounds-extended-cpip", "one-uip" ], @@ -147,13 +147,13 @@ ], [ "--cumulative-explanation-type", - "Determines the type of explanation used by the cumulative propagator(s) to explain propagations/conflicts (values: naive, big-step, pointwise; default: pointwise)", + "Determines the type of explanation used by the cumulative propagator(s) to explain propagations/conflicts [default: pointwise] [possible values: naive, big-step, pointwise]", "opt:naive:big-step:pointwise", "pointwise" ], [ "--cumulative-propagation-method", - "Determines the type of propagator which is used by the cumulative propagator(s) to propagate the constraint. (values: time-table-per-point, time-table-per-point-incremental, time-table-per-point-incremental-synchronised, time-table-over-interval, time-table-over-interval-incremental, time-table-over-interval-incremental-synchronised; default: time-table-over-interval-incremental)", + "Determines the type of propagator which is used by the cumulative propagator(s) to propagate the constraint. [default: time-table-over-interval-incremental] [possible values: time-table-per-point, time-table-per-point-incremental, time-table-per-point-incremental-synchronised, time-table-over-interval, time-table-over-interval-incremental, time-table-over-interval-incremental-synchronised]", "opt:time-table-per-point:time-table-per-point-incremental:time-table-per-point-incremental-synchronised:time-table-over-interval:time-table-over-interval-incremental:time-table-over-interval-incremental-synchronised", "time-table-over-interval-incremental" ], @@ -171,19 +171,19 @@ ], [ "--optimisation-strategy", - "Determine what type of optimisation strategy is used by the solver (values: linear-sat-unsat, linear-unsat-sat; default: linear-sat-unsat)", + "Determine what type of optimisation strategy is used by the solver [default: linear-sat-unsat] [possible values: linear-sat-unsat, linear-unsat-sat]", "opt:linear-sat-unsat:linear-unsat-sat", "linear-sat-unsat" ], [ "--memory-preallocated", - "The amount of memory (in MB) that is preallocated for storing nogoods (default: 50)", + "The amount of memory (in MB) that is preallocated for storing nogoods [default: 50] [possible values: int]", "int:0:18446744073709551615", "50" ], [ "--nogood-priority", - "The priority of the nogood propagator (values: high, medium, low, very-low, ultra-low, lowest; default: very-low)", + "The priority of the nogood propagator [default: very-low] [possible values: high, medium, low, very-low, ultra-low, lowest]", "opt:high:medium:low:very-low:ultra-low:lowest", "very-low" ] diff --git a/pumpkin-solver/src/bin/pumpkin-solver/msc.rs b/pumpkin-solver/src/bin/pumpkin-solver/msc.rs index 2a8c63088..03c078696 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/msc.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/msc.rs @@ -105,15 +105,23 @@ fn extra_flag(arg: &Arg) -> Value { .map(|value| value.get_name().to_owned()) .collect::>(); let description = format!( - "{summary} (values: {}; default: {default})", + "{summary} [default: {default}] [possible values: {}]", values.join(", ") ); (format!("opt:{}", values.join(":")), default, description) - } else if default.is_empty() { - (value_type(arg), default, summary) } else { - let description = format!("{summary} (default: {default})"); - (value_type(arg), default, description) + let flag_type = value_type(arg); + // Strip the bounds from the type, e.g. `int:0:4294967295` is shown as `int`. + let type_name = flag_type + .split(':') + .next() + .expect("split yields at least one item"); + let description = if default.is_empty() { + format!("{summary} [possible values: {type_name}]") + } else { + format!("{summary} [default: {default}] [possible values: {type_name}]") + }; + (flag_type, default, description) }; json!([flag, description, flag_type, default]) From 0b46544076914178b5b377dfe35bfe865ddeb04c Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Thu, 22 Oct 2026 11:16:43 +0200 Subject: [PATCH 3/9] refactor: give categories to the flags --- minizinc/pumpkin-for-proofs.msc | 136 ++++---- minizinc/pumpkin.msc | 136 ++++---- pumpkin-solver/src/bin/pumpkin-solver/main.rs | 329 +++++++++++------- 3 files changed, 334 insertions(+), 267 deletions(-) diff --git a/minizinc/pumpkin-for-proofs.msc b/minizinc/pumpkin-for-proofs.msc index 1258eff66..b3d2687e3 100644 --- a/minizinc/pumpkin-for-proofs.msc +++ b/minizinc/pumpkin-for-proofs.msc @@ -7,12 +7,24 @@ "stdFlags": [ "-t", "-r", + "-a", "-v", "-s", - "-f", - "-a" + "-f" ], "extraFlags": [ + [ + "--omit-timestamp", + "If `--verbose` is enabled then this option removes the timestamp information from the log messages (only applicable for (W)CNF instances).", + "bool", + "false" + ], + [ + "--omit-call-site", + "If `--verbose` is enabled then this option removes the call site information from the log messages (only applicable for (W)CNF instances).", + "bool", + "false" + ], [ "--proof-path", "The output path for the proof file. [possible values: string]", @@ -25,6 +37,30 @@ "opt:scaffold:full", "scaffold" ], + [ + "--optimisation-strategy", + "Determine what type of optimisation strategy is used by the solver [default: linear-sat-unsat] [possible values: linear-sat-unsat, linear-unsat-sat]", + "opt:linear-sat-unsat:linear-unsat-sat", + "linear-sat-unsat" + ], + [ + "--conflict-resolver", + "Determines the conflict resolver [default: one-uip] [possible values: no-learning, one-uip, all-decision, extended-cpip, bounds-extended-cpip]", + "opt:no-learning:one-uip:all-decision:extended-cpip:bounds-extended-cpip", + "one-uip" + ], + [ + "--recursive-minimisation", + "Decides whether learned clauses are minimised as a post-processing step after computing the 1-UIP Minimisation is done; according to the idea proposed in \"Generalized Conflict-Clause Strengthening for Satisfiability Solvers - Allen van Gelder (2011)\".", + "bool", + "false" + ], + [ + "--no-iterative-minimisation", + "Decides whether to apply semantic minimisation during conflict analysis; according to the idea proposed in \"Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)\".", + "bool", + "false" + ], [ "--learning-max-num-high-lbd-nogoods", "The number of high-lbd learned nogoods that are kept in the database. [default: 20000] [possible values: int]", @@ -56,14 +92,20 @@ "7" ], [ - "--recursive-minimisation", - "Decides whether learned clauses are minimised as a post-processing step after computing the 1-UIP Minimisation is done; according to the idea proposed in \"Generalized Conflict-Clause Strengthening for Satisfiability Solvers - Allen van Gelder (2011)\".", - "bool", - "false" + "--memory-preallocated", + "The amount of memory (in MB) that is preallocated for storing nogoods [default: 50] [possible values: int]", + "int:0:18446744073709551615", + "50" ], [ - "--no-iterative-minimisation", - "Decides whether to apply semantic minimisation during conflict analysis; according to the idea proposed in \"Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)\".", + "--nogood-priority", + "The priority of the nogood propagator [default: very-low] [possible values: high, medium, low, very-low, ultra-low, lowest]", + "opt:high:medium:low:very-low:ultra-low:lowest", + "very-low" + ], + [ + "--no-restarts", + "Determines that no restarts are allowed by the solver.", "bool", "false" ], @@ -79,6 +121,12 @@ "int:0:18446744073709551615", "50" ], + [ + "--restart-geometric-coef", + "The coefficient in the geometric sequence `x_i = x_{i-1} * \"--restart-geometric-coef\"` where `x_1 = \"--restarts-base-interval\"`. Used only if \"--restarts-sequence-generator\" is assigned to \"geometric\". [possible values: float]", + "float", + "" + ], [ "--restart-min-initial-conflicts", "Indicates the minimum number of initial conflicts before the first restart can occur. [default: 10000] [possible values: int]", @@ -104,46 +152,10 @@ "5000" ], [ - "--restart-geometric-coef", - "The coefficient in the geometric sequence `x_i = x_{i-1} * \"--restart-geometric-coef\"` where `x_1 = \"--restarts-base-interval\"`. Used only if \"--restarts-sequence-generator\" is assigned to \"geometric\". [possible values: float]", - "float", - "" - ], - [ - "--omit-timestamp", - "If `--verbose` is enabled then this option removes the timestamp information from the log messages (only applicable for (W)CNF instances).", - "bool", - "false" - ], - [ - "--omit-call-site", - "If `--verbose` is enabled then this option removes the call site information from the log messages (only applicable for (W)CNF instances).", - "bool", - "false" - ], - [ - "--upper-bound-encoding", - "The encoding to use for the upper bound constraint in a MaxSAT optimisation problem. [default: generalized-totalizer] [possible values: generalized-totalizer, cardinality-network]", - "opt:generalized-totalizer:cardinality-network", - "generalized-totalizer" - ], - [ - "--no-restarts", - "Determines that no restarts are allowed by the solver.", - "bool", - "false" - ], - [ - "--conflict-resolver", - "Determines the conflict resolver [default: one-uip] [possible values: no-learning, one-uip, all-decision, extended-cpip, bounds-extended-cpip]", - "opt:no-learning:one-uip:all-decision:extended-cpip:bounds-extended-cpip", - "one-uip" - ], - [ - "--cumulative-allow-holes", - "Determines that the cumulative propagator(s) are allowed to create holes in the domain.", - "bool", - "false" + "--cumulative-propagation-method", + "Determines the type of propagator which is used by the cumulative propagator(s) to propagate the constraint. [default: time-table-over-interval-incremental] [possible values: time-table-per-point, time-table-per-point-incremental, time-table-per-point-incremental-synchronised, time-table-over-interval, time-table-over-interval-incremental, time-table-over-interval-incremental-synchronised]", + "opt:time-table-per-point:time-table-per-point-incremental:time-table-per-point-incremental-synchronised:time-table-over-interval:time-table-over-interval-incremental:time-table-over-interval-incremental-synchronised", + "time-table-over-interval-incremental" ], [ "--cumulative-explanation-type", @@ -152,10 +164,10 @@ "pointwise" ], [ - "--cumulative-propagation-method", - "Determines the type of propagator which is used by the cumulative propagator(s) to propagate the constraint. [default: time-table-over-interval-incremental] [possible values: time-table-per-point, time-table-per-point-incremental, time-table-per-point-incremental-synchronised, time-table-over-interval, time-table-over-interval-incremental, time-table-over-interval-incremental-synchronised]", - "opt:time-table-per-point:time-table-per-point-incremental:time-table-per-point-incremental-synchronised:time-table-over-interval:time-table-over-interval-incremental:time-table-over-interval-incremental-synchronised", - "time-table-over-interval-incremental" + "--cumulative-allow-holes", + "Determines that the cumulative propagator(s) are allowed to create holes in the domain.", + "bool", + "false" ], [ "--cumulative-single-profiles", @@ -170,22 +182,10 @@ "false" ], [ - "--optimisation-strategy", - "Determine what type of optimisation strategy is used by the solver [default: linear-sat-unsat] [possible values: linear-sat-unsat, linear-unsat-sat]", - "opt:linear-sat-unsat:linear-unsat-sat", - "linear-sat-unsat" - ], - [ - "--memory-preallocated", - "The amount of memory (in MB) that is preallocated for storing nogoods [default: 50] [possible values: int]", - "int:0:18446744073709551615", - "50" - ], - [ - "--nogood-priority", - "The priority of the nogood propagator [default: very-low] [possible values: high, medium, low, very-low, ultra-low, lowest]", - "opt:high:medium:low:very-low:ultra-low:lowest", - "very-low" + "--upper-bound-encoding", + "The encoding to use for the upper bound constraint in a MaxSAT optimisation problem. [default: generalized-totalizer] [possible values: generalized-totalizer, cardinality-network]", + "opt:generalized-totalizer:cardinality-network", + "generalized-totalizer" ] ], "tags": [ diff --git a/minizinc/pumpkin.msc b/minizinc/pumpkin.msc index 2e9a55def..df122c43c 100644 --- a/minizinc/pumpkin.msc +++ b/minizinc/pumpkin.msc @@ -7,12 +7,24 @@ "stdFlags": [ "-t", "-r", + "-a", "-v", "-s", - "-f", - "-a" + "-f" ], "extraFlags": [ + [ + "--omit-timestamp", + "If `--verbose` is enabled then this option removes the timestamp information from the log messages (only applicable for (W)CNF instances).", + "bool", + "false" + ], + [ + "--omit-call-site", + "If `--verbose` is enabled then this option removes the call site information from the log messages (only applicable for (W)CNF instances).", + "bool", + "false" + ], [ "--proof-path", "The output path for the proof file. [possible values: string]", @@ -25,6 +37,30 @@ "opt:scaffold:full", "scaffold" ], + [ + "--optimisation-strategy", + "Determine what type of optimisation strategy is used by the solver [default: linear-sat-unsat] [possible values: linear-sat-unsat, linear-unsat-sat]", + "opt:linear-sat-unsat:linear-unsat-sat", + "linear-sat-unsat" + ], + [ + "--conflict-resolver", + "Determines the conflict resolver [default: one-uip] [possible values: no-learning, one-uip, all-decision, extended-cpip, bounds-extended-cpip]", + "opt:no-learning:one-uip:all-decision:extended-cpip:bounds-extended-cpip", + "one-uip" + ], + [ + "--recursive-minimisation", + "Decides whether learned clauses are minimised as a post-processing step after computing the 1-UIP Minimisation is done; according to the idea proposed in \"Generalized Conflict-Clause Strengthening for Satisfiability Solvers - Allen van Gelder (2011)\".", + "bool", + "false" + ], + [ + "--no-iterative-minimisation", + "Decides whether to apply semantic minimisation during conflict analysis; according to the idea proposed in \"Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)\".", + "bool", + "false" + ], [ "--learning-max-num-high-lbd-nogoods", "The number of high-lbd learned nogoods that are kept in the database. [default: 20000] [possible values: int]", @@ -56,14 +92,20 @@ "7" ], [ - "--recursive-minimisation", - "Decides whether learned clauses are minimised as a post-processing step after computing the 1-UIP Minimisation is done; according to the idea proposed in \"Generalized Conflict-Clause Strengthening for Satisfiability Solvers - Allen van Gelder (2011)\".", - "bool", - "false" + "--memory-preallocated", + "The amount of memory (in MB) that is preallocated for storing nogoods [default: 50] [possible values: int]", + "int:0:18446744073709551615", + "50" ], [ - "--no-iterative-minimisation", - "Decides whether to apply semantic minimisation during conflict analysis; according to the idea proposed in \"Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)\".", + "--nogood-priority", + "The priority of the nogood propagator [default: very-low] [possible values: high, medium, low, very-low, ultra-low, lowest]", + "opt:high:medium:low:very-low:ultra-low:lowest", + "very-low" + ], + [ + "--no-restarts", + "Determines that no restarts are allowed by the solver.", "bool", "false" ], @@ -79,6 +121,12 @@ "int:0:18446744073709551615", "50" ], + [ + "--restart-geometric-coef", + "The coefficient in the geometric sequence `x_i = x_{i-1} * \"--restart-geometric-coef\"` where `x_1 = \"--restarts-base-interval\"`. Used only if \"--restarts-sequence-generator\" is assigned to \"geometric\". [possible values: float]", + "float", + "" + ], [ "--restart-min-initial-conflicts", "Indicates the minimum number of initial conflicts before the first restart can occur. [default: 10000] [possible values: int]", @@ -104,46 +152,10 @@ "5000" ], [ - "--restart-geometric-coef", - "The coefficient in the geometric sequence `x_i = x_{i-1} * \"--restart-geometric-coef\"` where `x_1 = \"--restarts-base-interval\"`. Used only if \"--restarts-sequence-generator\" is assigned to \"geometric\". [possible values: float]", - "float", - "" - ], - [ - "--omit-timestamp", - "If `--verbose` is enabled then this option removes the timestamp information from the log messages (only applicable for (W)CNF instances).", - "bool", - "false" - ], - [ - "--omit-call-site", - "If `--verbose` is enabled then this option removes the call site information from the log messages (only applicable for (W)CNF instances).", - "bool", - "false" - ], - [ - "--upper-bound-encoding", - "The encoding to use for the upper bound constraint in a MaxSAT optimisation problem. [default: generalized-totalizer] [possible values: generalized-totalizer, cardinality-network]", - "opt:generalized-totalizer:cardinality-network", - "generalized-totalizer" - ], - [ - "--no-restarts", - "Determines that no restarts are allowed by the solver.", - "bool", - "false" - ], - [ - "--conflict-resolver", - "Determines the conflict resolver [default: one-uip] [possible values: no-learning, one-uip, all-decision, extended-cpip, bounds-extended-cpip]", - "opt:no-learning:one-uip:all-decision:extended-cpip:bounds-extended-cpip", - "one-uip" - ], - [ - "--cumulative-allow-holes", - "Determines that the cumulative propagator(s) are allowed to create holes in the domain.", - "bool", - "false" + "--cumulative-propagation-method", + "Determines the type of propagator which is used by the cumulative propagator(s) to propagate the constraint. [default: time-table-over-interval-incremental] [possible values: time-table-per-point, time-table-per-point-incremental, time-table-per-point-incremental-synchronised, time-table-over-interval, time-table-over-interval-incremental, time-table-over-interval-incremental-synchronised]", + "opt:time-table-per-point:time-table-per-point-incremental:time-table-per-point-incremental-synchronised:time-table-over-interval:time-table-over-interval-incremental:time-table-over-interval-incremental-synchronised", + "time-table-over-interval-incremental" ], [ "--cumulative-explanation-type", @@ -152,10 +164,10 @@ "pointwise" ], [ - "--cumulative-propagation-method", - "Determines the type of propagator which is used by the cumulative propagator(s) to propagate the constraint. [default: time-table-over-interval-incremental] [possible values: time-table-per-point, time-table-per-point-incremental, time-table-per-point-incremental-synchronised, time-table-over-interval, time-table-over-interval-incremental, time-table-over-interval-incremental-synchronised]", - "opt:time-table-per-point:time-table-per-point-incremental:time-table-per-point-incremental-synchronised:time-table-over-interval:time-table-over-interval-incremental:time-table-over-interval-incremental-synchronised", - "time-table-over-interval-incremental" + "--cumulative-allow-holes", + "Determines that the cumulative propagator(s) are allowed to create holes in the domain.", + "bool", + "false" ], [ "--cumulative-single-profiles", @@ -170,22 +182,10 @@ "false" ], [ - "--optimisation-strategy", - "Determine what type of optimisation strategy is used by the solver [default: linear-sat-unsat] [possible values: linear-sat-unsat, linear-unsat-sat]", - "opt:linear-sat-unsat:linear-unsat-sat", - "linear-sat-unsat" - ], - [ - "--memory-preallocated", - "The amount of memory (in MB) that is preallocated for storing nogoods [default: 50] [possible values: int]", - "int:0:18446744073709551615", - "50" - ], - [ - "--nogood-priority", - "The priority of the nogood propagator [default: very-low] [possible values: high, medium, low, very-low, ultra-low, lowest]", - "opt:high:medium:low:very-low:ultra-low:lowest", - "very-low" + "--upper-bound-encoding", + "The encoding to use for the upper bound constraint in a MaxSAT optimisation problem. [default: generalized-totalizer] [possible values: generalized-totalizer, cardinality-network]", + "opt:generalized-totalizer:cardinality-network", + "generalized-totalizer" ] ], "tags": [ diff --git a/pumpkin-solver/src/bin/pumpkin-solver/main.rs b/pumpkin-solver/src/bin/pumpkin-solver/main.rs index 656420c54..22a695f67 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/main.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/main.rs @@ -80,6 +80,81 @@ struct Args { #[arg(long, hide = true, exclusive = true)] generate_msc: Option, + /// The time budget for the solver, given in milliseconds. + #[arg( + short = 't', + long = "time-limit", + verbatim_doc_comment, + value_name = "u64" + )] + time_limit: Option, + + /// The random seed to use for the Pseudo Random Number Generator. + /// + /// Randomisation can be used for aspects such as the variable/value generator or initial + /// ordering of variables. + #[arg( + short = 'r', + long = "random-seed", + default_value_t = 42, + verbatim_doc_comment, + value_name = "u64" + )] + random_seed: u64, + + /// Instructs the solver to report all solutions in the case of satisfaction problems, + /// or print intermediate solutions of increasing quality in the case of optimisation + /// problems. + /// + /// See the MiniZinc specification () + /// for more information. + #[arg( + help_heading = "Output", + short = 'a', + long = "all-solutions", + verbatim_doc_comment + )] + all_solutions: bool, + + /// Enables log message output from the solver. + /// + /// For printing statistics see the option "--log-statistics", and for printing all solutions + /// (in case of a satisfaction problem) or printing solutions of increasing quality (in case of + /// an optimization problem) see the option "--all-solutions". + #[arg( + help_heading = "Output", + short = 'v', + long = "verbose", + verbatim_doc_comment + )] + verbose: bool, + + /// Enables logging of statistics from the solver. + #[arg( + help_heading = "Output", + short = 's', + long = "log-statistics", + verbatim_doc_comment + )] + log_statistics: bool, + + /// If `--verbose` is enabled then this option removes the timestamp information from the log + /// messages (only applicable for (W)CNF instances). + #[arg(help_heading = "Output", long = "omit-timestamp", verbatim_doc_comment)] + omit_timestamp: bool, + + /// If `--verbose` is enabled then this option removes the call site information from the log + /// messages (only applicable for (W)CNF instances). + /// + /// The call site is the file and line from which the message originated. + #[arg( + help_heading = "Output", + long = "omit-call-site", + default_value_t = false, + verbatim_doc_comment + )] + omit_call_site: bool, + /// The output path for the proof file. /// /// When solving a DIMACS instance, a DRAT proof is logged. In case of a FlatZinc model, a DRCP @@ -87,20 +162,73 @@ struct Args { /// /// In case of a DRCP proof, if the file extension ends with `.gz`, a gzipped proof will be /// produced. - #[arg(long, verbatim_doc_comment, value_name = "PATH")] + #[arg( + help_heading = "Proof Logging", + long, + verbatim_doc_comment, + value_name = "PATH" + )] proof_path: Option, /// What type of proof to log. /// /// If the `proof_path` option is not provided, this is ignored. - #[arg(long, value_enum, default_value_t)] + #[arg(help_heading = "Proof Logging", long, value_enum, default_value_t)] proof_type: ProofType, + /// Determine what type of optimisation strategy is used by the solver + #[arg( + help_heading = "Search", + long = "optimisation-strategy", + value_enum, + default_value_t + )] + optimisation_strategy: OptimisationStrategy, + + /// Instructs the solver to perform free search when solving a MiniZinc model; this flag + /// indicates that it is allowed to ignore the search annotations specified in the model. + /// + /// See the MiniZinc specification () + /// for more information. + #[arg( + help_heading = "Search", + short = 'f', + long = "free-search", + verbatim_doc_comment + )] + free_search: bool, + + /// Determines the conflict resolver. + #[arg(help_heading = "Conflict Analysis", long, value_enum, default_value_t)] + conflict_resolver: ConflictResolverType, + + /// Decides whether learned clauses are minimised as a post-processing step after computing the + /// 1-UIP Minimisation is done; according to the idea proposed in "Generalized Conflict-Clause + /// Strengthening for Satisfiability Solvers - Allen van Gelder (2011)". + #[arg( + help_heading = "Conflict Analysis", + long = "recursive-minimisation", + verbatim_doc_comment + )] + recursive_minimisation: bool, + + /// Decides whether to apply semantic minimisation during conflict analysis; according to the + /// idea proposed in "Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)". + /// + /// If this flag is present then the minimisation is turned on. + #[arg( + help_heading = "Conflict Analysis", + long = "no-iterative-minimisation", + verbatim_doc_comment + )] + no_iterative_minimisation: bool, + /// The number of high-lbd learned nogoods that are kept in the database. /// /// Learned nogoods are kept based on the tiered system introduced in "Improving /// SAT Solvers by Exploiting Empirical Characteristics of CDCL - Chanseok Oh (2016)". #[arg( + help_heading = "Nogood Database", long = "learning-max-num-high-lbd-nogoods", default_value_t = 20_000, verbatim_doc_comment, @@ -113,6 +241,7 @@ struct Args { /// This is based on the variation of the three-tiered system proposed in /// "Improving Implementation of SAT Competitions 2017–2019 Winners". #[arg( + help_heading = "Nogood Database", long = "learning-max-num-mid-lbd-nogoods", default_value_t = 7000, verbatim_doc_comment, @@ -125,6 +254,7 @@ struct Args { /// This is based on the variation of the three-tiered system proposed in /// "Improving Implementation of SAT Competitions 2017–2019 Winners". #[arg( + help_heading = "Nogood Database", long = "learning-max-num-low-lbd-nogoods", default_value_t = 100_000, verbatim_doc_comment, @@ -140,6 +270,7 @@ struct Args { /// SAT Solvers by Exploiting Empirical Characteristics of CDCL - Chanseok Oh (2016)" /// with the variation from "Improving Implementation of SAT Competitions 2017–2019 Winners". #[arg( + help_heading = "Nogood Database", long = "learning-low-lbd-threshold", default_value_t = 3, verbatim_doc_comment, @@ -156,6 +287,7 @@ struct Args { /// SAT Solvers by Exploiting Empirical Characteristics of CDCL - Chanseok Oh (2016)" /// with the variation from "Improving Implementation of SAT Competitions 2017–2019 Winners". #[arg( + help_heading = "Nogood Database", long = "learning-high-lbd-threshold", default_value_t = 7, verbatim_doc_comment, @@ -163,18 +295,27 @@ struct Args { )] learning_high_lbd_threshold: u32, - /// Decides whether learned clauses are minimised as a post-processing step after computing the - /// 1-UIP Minimisation is done; according to the idea proposed in "Generalized Conflict-Clause - /// Strengthening for Satisfiability Solvers - Allen van Gelder (2011)". - #[arg(long = "recursive-minimisation", verbatim_doc_comment)] - recursive_minimisation: bool, + /// The amount of memory (in MB) that is preallocated for storing nogoods. + #[arg( + help_heading = "Nogood Database", + long = "memory-preallocated", + default_value_t = 50, + value_name = "usize" + )] + memory_preallocated: usize, - /// Decides whether to apply semantic minimisation during conflict analysis; according to the - /// idea proposed in "Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)". - /// - /// If this flag is present then the minimisation is turned on. - #[arg(long = "no-iterative-minimisation", verbatim_doc_comment)] - no_iterative_minimisation: bool, + /// The priority of the nogood propagator. + #[arg( + help_heading = "Nogood Database", + long = "nogood-priority", + value_enum, + default_value_t + )] + nogood_propagator_priority: Priority, + + /// Determines that no restarts are allowed by the solver. + #[arg(help_heading = "Restarts", long = "no-restarts", verbatim_doc_comment)] + no_restarts: bool, /// Decides the sequence based on which the restarts are performed. /// @@ -186,7 +327,7 @@ struct Args { /// (1993)") /// /// To be used in combination with "--restarts-base-interval". - #[arg(long, value_enum, default_value_t)] + #[arg(help_heading = "Restarts", long, value_enum, default_value_t)] restart_sequence_generator_type: SequenceGeneratorType, /// The base interval length is used as a multiplier to the restart sequence. @@ -198,6 +339,7 @@ struct Args { /// For example, constant restarts with base interval 50 means a restart is triggered every 50 /// conflicts. #[arg( + help_heading = "Restarts", long = "restart-base-interval", default_value_t = 50, verbatim_doc_comment, @@ -205,11 +347,23 @@ struct Args { )] restart_base_interval: u64, + /// The coefficient in the geometric sequence `x_i = x_{i-1} * "--restart-geometric-coef"` + /// where `x_1 = "--restarts-base-interval"`. Used only if "--restarts-sequence-generator" + /// is assigned to "geometric". + #[arg( + help_heading = "Restarts", + long = "restart-geometric-coef", + verbatim_doc_comment, + value_name = "f64" + )] + restart_geometric_coef: Option, + /// Indicates the minimum number of initial conflicts before the first restart can occur. /// /// This allows the solver to learn some things about the problem before a restart is allowed /// to occur. #[arg( + help_heading = "Restarts", long = "restart-min-initial-conflicts", default_value_t = 10000, verbatim_doc_comment, @@ -225,6 +379,7 @@ struct Args { /// restart policy. If the long-term average LBD multiplied by this coefficient is lower /// than the short-term average LBD then a restart is performed. #[arg( + help_heading = "Restarts", long = "restart-lbd-coef", default_value_t = 1.25, verbatim_doc_comment, @@ -241,6 +396,7 @@ struct Args { /// the average number of assigned variables in the recent past. A greater (lower) value for /// "--restart-num-assigned-coef" means fewer (more) blocked restarts. #[arg( + help_heading = "Restarts", long = "restart-num-assigned-coef", default_value_t = 1.4, verbatim_doc_comment, @@ -255,6 +411,7 @@ struct Args { /// The solver considers the last "--restart_num_assigned_window" conflicts as the reference /// point for the number of assigned variables. #[arg( + help_heading = "Restarts", long = "restart-num-assigned-window", default_value_t = 5000, verbatim_doc_comment, @@ -262,139 +419,49 @@ struct Args { )] restart_num_assigned_window: u64, - /// The coefficient in the geometric sequence `x_i = x_{i-1} * "--restart-geometric-coef"` - /// where `x_1 = "--restarts-base-interval"`. Used only if "--restarts-sequence-generator" - /// is assigned to "geometric". - #[arg( - long = "restart-geometric-coef", - verbatim_doc_comment, - value_name = "f64" - )] - restart_geometric_coef: Option, - - /// The time budget for the solver, given in milliseconds. - #[arg( - short = 't', - long = "time-limit", - verbatim_doc_comment, - value_name = "u64" - )] - time_limit: Option, - - /// The random seed to use for the Pseudo Random Number Generator. - /// - /// Randomisation can be used for aspects such as the variable/value generator or initial - /// ordering of variables. - #[arg( - short = 'r', - long = "random-seed", - default_value_t = 42, - verbatim_doc_comment, - value_name = "u64" - )] - random_seed: u64, - - /// Enables log message output from the solver. - /// - /// For printing statistics see the option "--log-statistics", and for printing all solutions - /// (in case of a satisfaction problem) or printing solutions of increasing quality (in case of - /// an optimization problem) see the option "--all-solutions". - #[arg(short = 'v', long = "verbose", verbatim_doc_comment)] - verbose: bool, - - /// Enables logging of statistics from the solver. - #[arg(short = 's', long = "log-statistics", verbatim_doc_comment)] - log_statistics: bool, - - /// Instructs the solver to perform free search when solving a MiniZinc model; this flag - /// indicates that it is allowed to ignore the search annotations specified in the model. - /// - /// See the MiniZinc specification () - /// for more information. - #[arg(short = 'f', long = "free-search", verbatim_doc_comment)] - free_search: bool, - - /// Instructs the solver to report all solutions in the case of satisfaction problems, - /// or print intermediate solutions of increasing quality in the case of optimisation - /// problems. - /// - /// See the MiniZinc specification () - /// for more information. - #[arg(short = 'a', long = "all-solutions", verbatim_doc_comment)] - all_solutions: bool, - - /// If `--verbose` is enabled then this option removes the timestamp information from the log - /// messages (only applicable for (W)CNF instances). - #[arg(long = "omit-timestamp", verbatim_doc_comment)] - omit_timestamp: bool, - - /// If `--verbose` is enabled then this option removes the call site information from the log - /// messages (only applicable for (W)CNF instances). - /// - /// The call site is the file and line from which the message originated. - #[arg(long = "omit-call-site", default_value_t = false, verbatim_doc_comment)] - omit_call_site: bool, - - /// The encoding to use for the upper bound constraint in a MaxSAT optimisation problem. + /// Determines the type of propagator which is used by the cumulative propagator(s) to + /// propagate the constraint. /// - /// - The "generalised-totalizer" value specifies that the solver should use the Generalized - /// Totalizer Encoding (see "Generalized totalizer encoding for pseudo-boolean constraints - - /// Saurabh et al. (2015)") - /// - The "cardinality-network" value specifies that the solver should use the Cardinality - /// Network Encoding (see "Cardinality networks: a theoretical and empirical study - Asín et - /// al. (2011)"). - #[arg(long, value_enum, default_value_t)] - upper_bound_encoding: PseudoBooleanEncoding, - - /// Determines that no restarts are allowed by the solver. - #[arg(long = "no-restarts", verbatim_doc_comment)] - no_restarts: bool, - - /// Determines the conflict resolver. - #[arg(long, value_enum, default_value_t)] - conflict_resolver: ConflictResolverType, - - /// Determines that the cumulative propagator(s) are allowed to create holes in the domain. - #[arg(long = "cumulative-allow-holes", verbatim_doc_comment)] - cumulative_allow_holes: bool, + /// Currently, the solver only supports variations on time-tabling methods. + #[arg(help_heading = "Cumulative", long, value_enum, default_value_t)] + cumulative_propagation_method: CumulativePropagationMethod, /// Determines the type of explanation used by the cumulative propagator(s) to explain /// propagations/conflicts. - #[arg(long, value_enum, default_value_t)] + #[arg(help_heading = "Cumulative", long, value_enum, default_value_t)] cumulative_explanation_type: CumulativeExplanationType, - /// Determines the type of propagator which is used by the cumulative propagator(s) to - /// propagate the constraint. - /// - /// Currently, the solver only supports variations on time-tabling methods. - #[arg(long, value_enum, default_value_t)] - cumulative_propagation_method: CumulativePropagationMethod, + /// Determines that the cumulative propagator(s) are allowed to create holes in the domain. + #[arg( + help_heading = "Cumulative", + long = "cumulative-allow-holes", + verbatim_doc_comment + )] + cumulative_allow_holes: bool, /// Determines whether a single profiles are used generated when explaining a propagation for /// the cumulative constraint. - #[arg(long = "cumulative-single-profiles")] + #[arg(help_heading = "Cumulative", long = "cumulative-single-profiles")] cumulative_single_profiles: bool, /// Determines whether incremental backtracking is applied or whether the cumulative /// propagators compute the time-table from scratch upon backtracking - #[arg(long = "cumulative-incremental-backtracking")] - cumulative_incremental_backtracking: bool, - - /// Determine what type of optimisation strategy is used by the solver - #[arg(long = "optimisation-strategy", value_enum, default_value_t)] - optimisation_strategy: OptimisationStrategy, - - /// The amount of memory (in MB) that is preallocated for storing nogoods. #[arg( - long = "memory-preallocated", - default_value_t = 50, - value_name = "usize" + help_heading = "Cumulative", + long = "cumulative-incremental-backtracking" )] - memory_preallocated: usize, + cumulative_incremental_backtracking: bool, - /// The priority of the nogood propagator. - #[arg(long = "nogood-priority", value_enum, default_value_t)] - nogood_propagator_priority: Priority, + /// The encoding to use for the upper bound constraint in a MaxSAT optimisation problem. + /// + /// - The "generalised-totalizer" value specifies that the solver should use the Generalized + /// Totalizer Encoding (see "Generalized totalizer encoding for pseudo-boolean constraints - + /// Saurabh et al. (2015)") + /// - The "cardinality-network" value specifies that the solver should use the Cardinality + /// Network Encoding (see "Cardinality networks: a theoretical and empirical study - Asín et + /// al. (2011)"). + #[arg(help_heading = "MaxSAT", long, value_enum, default_value_t)] + upper_bound_encoding: PseudoBooleanEncoding, } fn configure_logging( From 51f5ae72ed65f721134af5108b9eab120add00db Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Thu, 22 Oct 2026 11:23:24 +0200 Subject: [PATCH 4/9] refactor: remove Max(SAT) flags from the .msc files --- minizinc/pumpkin-for-proofs.msc | 18 --------- minizinc/pumpkin.msc | 18 --------- pumpkin-solver/src/bin/pumpkin-solver/main.rs | 40 ++++++++++--------- pumpkin-solver/src/bin/pumpkin-solver/msc.rs | 10 ++++- 4 files changed, 31 insertions(+), 55 deletions(-) diff --git a/minizinc/pumpkin-for-proofs.msc b/minizinc/pumpkin-for-proofs.msc index b3d2687e3..2c24a2219 100644 --- a/minizinc/pumpkin-for-proofs.msc +++ b/minizinc/pumpkin-for-proofs.msc @@ -13,18 +13,6 @@ "-f" ], "extraFlags": [ - [ - "--omit-timestamp", - "If `--verbose` is enabled then this option removes the timestamp information from the log messages (only applicable for (W)CNF instances).", - "bool", - "false" - ], - [ - "--omit-call-site", - "If `--verbose` is enabled then this option removes the call site information from the log messages (only applicable for (W)CNF instances).", - "bool", - "false" - ], [ "--proof-path", "The output path for the proof file. [possible values: string]", @@ -180,12 +168,6 @@ "Determines whether incremental backtracking is applied or whether the cumulative propagators compute the time-table from scratch upon backtracking", "bool", "false" - ], - [ - "--upper-bound-encoding", - "The encoding to use for the upper bound constraint in a MaxSAT optimisation problem. [default: generalized-totalizer] [possible values: generalized-totalizer, cardinality-network]", - "opt:generalized-totalizer:cardinality-network", - "generalized-totalizer" ] ], "tags": [ diff --git a/minizinc/pumpkin.msc b/minizinc/pumpkin.msc index df122c43c..b1f5a5345 100644 --- a/minizinc/pumpkin.msc +++ b/minizinc/pumpkin.msc @@ -13,18 +13,6 @@ "-f" ], "extraFlags": [ - [ - "--omit-timestamp", - "If `--verbose` is enabled then this option removes the timestamp information from the log messages (only applicable for (W)CNF instances).", - "bool", - "false" - ], - [ - "--omit-call-site", - "If `--verbose` is enabled then this option removes the call site information from the log messages (only applicable for (W)CNF instances).", - "bool", - "false" - ], [ "--proof-path", "The output path for the proof file. [possible values: string]", @@ -180,12 +168,6 @@ "Determines whether incremental backtracking is applied or whether the cumulative propagators compute the time-table from scratch upon backtracking", "bool", "false" - ], - [ - "--upper-bound-encoding", - "The encoding to use for the upper bound constraint in a MaxSAT optimisation problem. [default: generalized-totalizer] [possible values: generalized-totalizer, cardinality-network]", - "opt:generalized-totalizer:cardinality-network", - "generalized-totalizer" ] ], "tags": [ diff --git a/pumpkin-solver/src/bin/pumpkin-solver/main.rs b/pumpkin-solver/src/bin/pumpkin-solver/main.rs index 22a695f67..af56e4aed 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/main.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/main.rs @@ -138,23 +138,6 @@ struct Args { )] log_statistics: bool, - /// If `--verbose` is enabled then this option removes the timestamp information from the log - /// messages (only applicable for (W)CNF instances). - #[arg(help_heading = "Output", long = "omit-timestamp", verbatim_doc_comment)] - omit_timestamp: bool, - - /// If `--verbose` is enabled then this option removes the call site information from the log - /// messages (only applicable for (W)CNF instances). - /// - /// The call site is the file and line from which the message originated. - #[arg( - help_heading = "Output", - long = "omit-call-site", - default_value_t = false, - verbatim_doc_comment - )] - omit_call_site: bool, - /// The output path for the proof file. /// /// When solving a DIMACS instance, a DRAT proof is logged. In case of a FlatZinc model, a DRCP @@ -460,8 +443,29 @@ struct Args { /// - The "cardinality-network" value specifies that the solver should use the Cardinality /// Network Encoding (see "Cardinality networks: a theoretical and empirical study - Asín et /// al. (2011)"). - #[arg(help_heading = "MaxSAT", long, value_enum, default_value_t)] + #[arg(help_heading = "Max(SAT)", long, value_enum, default_value_t)] upper_bound_encoding: PseudoBooleanEncoding, + + /// If `--verbose` is enabled then this option removes the timestamp information from the log + /// messages (only applicable for (W)CNF instances). + #[arg( + help_heading = "Max(SAT)", + long = "omit-timestamp", + verbatim_doc_comment + )] + omit_timestamp: bool, + + /// If `--verbose` is enabled then this option removes the call site information from the log + /// messages (only applicable for (W)CNF instances). + /// + /// The call site is the file and line from which the message originated. + #[arg( + help_heading = "Max(SAT)", + long = "omit-call-site", + default_value_t = false, + verbatim_doc_comment + )] + omit_call_site: bool, } fn configure_logging( diff --git a/pumpkin-solver/src/bin/pumpkin-solver/msc.rs b/pumpkin-solver/src/bin/pumpkin-solver/msc.rs index 03c078696..bb2cc4070 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/msc.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/msc.rs @@ -39,12 +39,20 @@ const CONFIGURATIONS: [(&str, &str, &str, &str); 2] = [ /// ). const MINIZINC_STD_FLAGS: [char; 9] = ['a', 'f', 'i', 'n', 'p', 'r', 's', 't', 'v']; +/// The help headings of arguments which are not applicable to MiniZinc models, and are therefore +/// not exposed. +const EXCLUDED_HEADINGS: [&str; 1] = ["Max(SAT)"]; + fn generate_msc(name: &str, id: &str, mznlib: &str) -> String { let command = Args::command(); let arguments = command .get_arguments() .filter(|arg| !arg.is_positional() && !arg.is_hide_set()) - .filter(|arg| !matches!(arg.get_action(), ArgAction::Help | ArgAction::Version)); + .filter(|arg| !matches!(arg.get_action(), ArgAction::Help | ArgAction::Version)) + .filter(|arg| { + arg.get_help_heading() + .is_none_or(|heading| !EXCLUDED_HEADINGS.contains(&heading)) + }); // Arguments whose short flag is a standard flag of MiniZinc (e.g. `-a`) are exposed as such; // all other arguments are exposed as extra flags. From 7f7745aaf1e54939804922b512751d45cd5a1d29 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Thu, 22 Oct 2026 11:30:06 +0200 Subject: [PATCH 5/9] chore: args doc cleanup --- minizinc/pumpkin-for-proofs.msc | 14 +++++++------- minizinc/pumpkin.msc | 14 +++++++------- .../sequence_generators/sequence_generator_type.rs | 4 ++-- 3 files changed, 16 insertions(+), 16 deletions(-) diff --git a/minizinc/pumpkin-for-proofs.msc b/minizinc/pumpkin-for-proofs.msc index 2c24a2219..2386e3b31 100644 --- a/minizinc/pumpkin-for-proofs.msc +++ b/minizinc/pumpkin-for-proofs.msc @@ -27,7 +27,7 @@ ], [ "--optimisation-strategy", - "Determine what type of optimisation strategy is used by the solver [default: linear-sat-unsat] [possible values: linear-sat-unsat, linear-unsat-sat]", + "Determines what type of optimisation strategy is used by the solver [default: linear-sat-unsat] [possible values: linear-sat-unsat, linear-unsat-sat]", "opt:linear-sat-unsat:linear-unsat-sat", "linear-sat-unsat" ], @@ -39,13 +39,13 @@ ], [ "--recursive-minimisation", - "Decides whether learned clauses are minimised as a post-processing step after computing the 1-UIP Minimisation is done; according to the idea proposed in \"Generalized Conflict-Clause Strengthening for Satisfiability Solvers - Allen van Gelder (2011)\".", + "Enables recursive minimisation of learned nogoods as a post-processing step after conflict analysis; according to the idea proposed in \"Generalized Conflict-Clause Strengthening for Satisfiability Solvers - Allen van Gelder (2011)\".", "bool", "false" ], [ "--no-iterative-minimisation", - "Decides whether to apply semantic minimisation during conflict analysis; according to the idea proposed in \"Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)\".", + "Disables semantic minimisation of learned nogoods during conflict analysis; according to the idea proposed in \"Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)\".", "bool", "false" ], @@ -69,13 +69,13 @@ ], [ "--learning-low-lbd-threshold", - "The treshold determining whether a learned nogood is \"low\" LBD. [default: 3] [possible values: int]", + "The threshold determining whether a learned nogood is \"low\" LBD. [default: 3] [possible values: int]", "int:0:4294967295", "3" ], [ "--learning-high-lbd-threshold", - "The treshold determining whether a learned nogood is \"high\" LBD. [default: 7] [possible values: int]", + "The threshold determining whether a learned nogood is \"high\" LBD. [default: 7] [possible values: int]", "int:0:4294967295", "7" ], @@ -111,7 +111,7 @@ ], [ "--restart-geometric-coef", - "The coefficient in the geometric sequence `x_i = x_{i-1} * \"--restart-geometric-coef\"` where `x_1 = \"--restarts-base-interval\"`. Used only if \"--restarts-sequence-generator\" is assigned to \"geometric\". [possible values: float]", + "The coefficient in the geometric sequence `x_i = x_{i-1} * \"--restart-geometric-coef\"` where `x_1 = \"--restart-base-interval\"`. Used only if \"--restart-sequence-generator-type\" is assigned to \"geometric\". [possible values: float]", "float", "" ], @@ -159,7 +159,7 @@ ], [ "--cumulative-single-profiles", - "Determines whether a single profiles are used generated when explaining a propagation for the cumulative constraint", + "Determines whether single profiles are used when explaining a propagation of the cumulative constraint", "bool", "false" ], diff --git a/minizinc/pumpkin.msc b/minizinc/pumpkin.msc index b1f5a5345..741ac0e6e 100644 --- a/minizinc/pumpkin.msc +++ b/minizinc/pumpkin.msc @@ -27,7 +27,7 @@ ], [ "--optimisation-strategy", - "Determine what type of optimisation strategy is used by the solver [default: linear-sat-unsat] [possible values: linear-sat-unsat, linear-unsat-sat]", + "Determines what type of optimisation strategy is used by the solver [default: linear-sat-unsat] [possible values: linear-sat-unsat, linear-unsat-sat]", "opt:linear-sat-unsat:linear-unsat-sat", "linear-sat-unsat" ], @@ -39,13 +39,13 @@ ], [ "--recursive-minimisation", - "Decides whether learned clauses are minimised as a post-processing step after computing the 1-UIP Minimisation is done; according to the idea proposed in \"Generalized Conflict-Clause Strengthening for Satisfiability Solvers - Allen van Gelder (2011)\".", + "Enables recursive minimisation of learned nogoods as a post-processing step after conflict analysis; according to the idea proposed in \"Generalized Conflict-Clause Strengthening for Satisfiability Solvers - Allen van Gelder (2011)\".", "bool", "false" ], [ "--no-iterative-minimisation", - "Decides whether to apply semantic minimisation during conflict analysis; according to the idea proposed in \"Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)\".", + "Disables semantic minimisation of learned nogoods during conflict analysis; according to the idea proposed in \"Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)\".", "bool", "false" ], @@ -69,13 +69,13 @@ ], [ "--learning-low-lbd-threshold", - "The treshold determining whether a learned nogood is \"low\" LBD. [default: 3] [possible values: int]", + "The threshold determining whether a learned nogood is \"low\" LBD. [default: 3] [possible values: int]", "int:0:4294967295", "3" ], [ "--learning-high-lbd-threshold", - "The treshold determining whether a learned nogood is \"high\" LBD. [default: 7] [possible values: int]", + "The threshold determining whether a learned nogood is \"high\" LBD. [default: 7] [possible values: int]", "int:0:4294967295", "7" ], @@ -111,7 +111,7 @@ ], [ "--restart-geometric-coef", - "The coefficient in the geometric sequence `x_i = x_{i-1} * \"--restart-geometric-coef\"` where `x_1 = \"--restarts-base-interval\"`. Used only if \"--restarts-sequence-generator\" is assigned to \"geometric\". [possible values: float]", + "The coefficient in the geometric sequence `x_i = x_{i-1} * \"--restart-geometric-coef\"` where `x_1 = \"--restart-base-interval\"`. Used only if \"--restart-sequence-generator-type\" is assigned to \"geometric\". [possible values: float]", "float", "" ], @@ -159,7 +159,7 @@ ], [ "--cumulative-single-profiles", - "Determines whether a single profiles are used generated when explaining a propagation for the cumulative constraint", + "Determines whether single profiles are used when explaining a propagation of the cumulative constraint", "bool", "false" ], diff --git a/pumpkin-crates/core/src/basic_types/sequence_generators/sequence_generator_type.rs b/pumpkin-crates/core/src/basic_types/sequence_generators/sequence_generator_type.rs index 1a60a4cd5..11127dc7f 100644 --- a/pumpkin-crates/core/src/basic_types/sequence_generators/sequence_generator_type.rs +++ b/pumpkin-crates/core/src/basic_types/sequence_generators/sequence_generator_type.rs @@ -16,9 +16,9 @@ pub enum SequenceGeneratorType { /// When `multiplicative_factor` is not an integer, then the above formula is **not** the same /// as the formula `f(i) = a * m^i` since intermediate values are founded down. Geometric, - /// Indicates that the restart strategy should use Luby restarts \[1\]. + /// Indicates that the restart strategy should use Luby restarts. /// - /// The Luby sequence is a recursive sequence of the form: + /// The Luby sequence \[1\] is a recursive sequence of the form: /// 1, 1, 2, 1, 1, 2, 4, 1, 1, 2, 1, 1, 2, 4, 8, 1, 1, 2.... /// /// # Bibliography From 51d3c4d07d001e9f3b6bf1d49ce80e6c5b0d14e7 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Thu, 22 Oct 2026 11:39:14 +0200 Subject: [PATCH 6/9] chore: update clearer value names --- pumpkin-solver/src/bin/pumpkin-solver/main.rs | 61 +++++++++++++++---- 1 file changed, 50 insertions(+), 11 deletions(-) diff --git a/pumpkin-solver/src/bin/pumpkin-solver/main.rs b/pumpkin-solver/src/bin/pumpkin-solver/main.rs index af56e4aed..19d15fad3 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/main.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/main.rs @@ -66,7 +66,8 @@ About: {about} author, version, about, - arg_required_else_help = true + arg_required_else_help = true, + next_line_help = true )] struct Args { /// The instance to solve. The file should have one of the following extensions: @@ -85,7 +86,7 @@ struct Args { short = 't', long = "time-limit", verbatim_doc_comment, - value_name = "u64" + value_name = "MS" )] time_limit: Option, @@ -156,7 +157,13 @@ struct Args { /// What type of proof to log. /// /// If the `proof_path` option is not provided, this is ignored. - #[arg(help_heading = "Proof Logging", long, value_enum, default_value_t)] + #[arg( + help_heading = "Proof Logging", + long, + value_enum, + default_value_t, + value_name = "TYPE" + )] proof_type: ProofType, /// Determine what type of optimisation strategy is used by the solver @@ -164,7 +171,8 @@ struct Args { help_heading = "Search", long = "optimisation-strategy", value_enum, - default_value_t + default_value_t, + value_name = "STRATEGY" )] optimisation_strategy: OptimisationStrategy, @@ -182,7 +190,13 @@ struct Args { free_search: bool, /// Determines the conflict resolver. - #[arg(help_heading = "Conflict Analysis", long, value_enum, default_value_t)] + #[arg( + help_heading = "Conflict Analysis", + long, + value_enum, + default_value_t, + value_name = "RESOLVER" + )] conflict_resolver: ConflictResolverType, /// Decides whether learned clauses are minimised as a post-processing step after computing the @@ -283,7 +297,7 @@ struct Args { help_heading = "Nogood Database", long = "memory-preallocated", default_value_t = 50, - value_name = "usize" + value_name = "MB" )] memory_preallocated: usize, @@ -292,7 +306,8 @@ struct Args { help_heading = "Nogood Database", long = "nogood-priority", value_enum, - default_value_t + default_value_t, + value_name = "PRIORITY" )] nogood_propagator_priority: Priority, @@ -310,7 +325,13 @@ struct Args { /// (1993)") /// /// To be used in combination with "--restarts-base-interval". - #[arg(help_heading = "Restarts", long, value_enum, default_value_t)] + #[arg( + help_heading = "Restarts", + long, + value_enum, + default_value_t, + value_name = "SEQUENCE_GENERATOR" + )] restart_sequence_generator_type: SequenceGeneratorType, /// The base interval length is used as a multiplier to the restart sequence. @@ -406,12 +427,24 @@ struct Args { /// propagate the constraint. /// /// Currently, the solver only supports variations on time-tabling methods. - #[arg(help_heading = "Cumulative", long, value_enum, default_value_t)] + #[arg( + help_heading = "Cumulative", + long, + value_enum, + default_value_t, + value_name = "PROPAGATION" + )] cumulative_propagation_method: CumulativePropagationMethod, /// Determines the type of explanation used by the cumulative propagator(s) to explain /// propagations/conflicts. - #[arg(help_heading = "Cumulative", long, value_enum, default_value_t)] + #[arg( + help_heading = "Cumulative", + long, + value_enum, + default_value_t, + value_name = "EXPLANATION" + )] cumulative_explanation_type: CumulativeExplanationType, /// Determines that the cumulative propagator(s) are allowed to create holes in the domain. @@ -443,7 +476,13 @@ struct Args { /// - The "cardinality-network" value specifies that the solver should use the Cardinality /// Network Encoding (see "Cardinality networks: a theoretical and empirical study - Asín et /// al. (2011)"). - #[arg(help_heading = "Max(SAT)", long, value_enum, default_value_t)] + #[arg( + help_heading = "Max(SAT)", + long, + value_enum, + default_value_t, + value_name = "ENCODING" + )] upper_bound_encoding: PseudoBooleanEncoding, /// If `--verbose` is enabled then this option removes the timestamp information from the log From f47f6d04145d106861881f22510c322f5eba95f1 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Thu, 22 Oct 2026 11:41:52 +0200 Subject: [PATCH 7/9] chore: clean up docs --- pumpkin-solver/src/bin/pumpkin-solver/main.rs | 37 ++++++++++--------- .../pseudo_boolean_constraint_encoder.rs | 13 ++++--- 2 files changed, 28 insertions(+), 22 deletions(-) diff --git a/pumpkin-solver/src/bin/pumpkin-solver/main.rs b/pumpkin-solver/src/bin/pumpkin-solver/main.rs index 19d15fad3..0d553070c 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/main.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/main.rs @@ -166,7 +166,7 @@ struct Args { )] proof_type: ProofType, - /// Determine what type of optimisation strategy is used by the solver + /// Determines what type of optimisation strategy is used by the solver. #[arg( help_heading = "Search", long = "optimisation-strategy", @@ -199,9 +199,9 @@ struct Args { )] conflict_resolver: ConflictResolverType, - /// Decides whether learned clauses are minimised as a post-processing step after computing the - /// 1-UIP Minimisation is done; according to the idea proposed in "Generalized Conflict-Clause - /// Strengthening for Satisfiability Solvers - Allen van Gelder (2011)". + /// Enables recursive minimisation of learned nogoods as a post-processing step after conflict + /// analysis; according to the idea proposed in "Generalized Conflict-Clause Strengthening for + /// Satisfiability Solvers - Allen van Gelder (2011)". #[arg( help_heading = "Conflict Analysis", long = "recursive-minimisation", @@ -209,10 +209,11 @@ struct Args { )] recursive_minimisation: bool, - /// Decides whether to apply semantic minimisation during conflict analysis; according to the - /// idea proposed in "Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)". + /// Disables semantic minimisation of learned nogoods during conflict analysis; according to + /// the idea proposed in "Semantic Learning for Lazy Clause Generation - Feydy et al. + /// (2013)". /// - /// If this flag is present then the minimisation is turned on. + /// By default, the minimisation is turned on. #[arg( help_heading = "Conflict Analysis", long = "no-iterative-minimisation", @@ -259,7 +260,7 @@ struct Args { )] learning_max_num_low_lbd_nogoods: usize, - /// The treshold determining whether a learned nogood is "low" LBD. + /// The threshold determining whether a learned nogood is "low" LBD. /// /// "Low" LBD nogood are kept around for longer since they are of better "quality". /// @@ -275,7 +276,7 @@ struct Args { )] learning_low_lbd_threshold: u32, - /// The treshold determining whether a learned nogood is "high" LBD. + /// The threshold determining whether a learned nogood is "high" LBD. /// /// "High" LBD nogood are kept around for a shorter amount of time since they are of bad /// "quality". @@ -324,12 +325,13 @@ struct Args { /// 1, 1, 2, 4, 8, 1, 1, 2.... (see "Optimal speedup of Las Vegas algorithms - Luby et al. /// (1993)") /// - /// To be used in combination with "--restarts-base-interval". + /// To be used in combination with "--restart-base-interval". #[arg( help_heading = "Restarts", long, value_enum, default_value_t, + verbatim_doc_comment, value_name = "SEQUENCE_GENERATOR" )] restart_sequence_generator_type: SequenceGeneratorType, @@ -352,7 +354,7 @@ struct Args { restart_base_interval: u64, /// The coefficient in the geometric sequence `x_i = x_{i-1} * "--restart-geometric-coef"` - /// where `x_1 = "--restarts-base-interval"`. Used only if "--restarts-sequence-generator" + /// where `x_1 = "--restart-base-interval"`. Used only if "--restart-sequence-generator-type" /// is assigned to "geometric". #[arg( help_heading = "Restarts", @@ -394,7 +396,7 @@ struct Args { /// Used to determine if a restart should be blocked (see "Refining Restarts Strategies for SAT /// and UNSAT - Audemard and Simon (2012)"). /// - /// To be used in combination with "--restarts-num-assigned-window". + /// To be used in combination with "--restart-num-assigned-window". /// /// A restart is blocked if the number of assigned propositional variables is much greater than /// the average number of assigned variables in the recent past. A greater (lower) value for @@ -412,7 +414,7 @@ struct Args { /// blocking restarts (see "Refining Restarts Strategies for SAT /// and UNSAT - Audemard and Simon (2012)"). /// - /// The solver considers the last "--restart_num_assigned_window" conflicts as the reference + /// The solver considers the last "--restart-num-assigned-window" conflicts as the reference /// point for the number of assigned variables. #[arg( help_heading = "Restarts", @@ -455,13 +457,13 @@ struct Args { )] cumulative_allow_holes: bool, - /// Determines whether a single profiles are used generated when explaining a propagation for - /// the cumulative constraint. + /// Determines whether single profiles are used when explaining a propagation of the cumulative + /// constraint. #[arg(help_heading = "Cumulative", long = "cumulative-single-profiles")] cumulative_single_profiles: bool, /// Determines whether incremental backtracking is applied or whether the cumulative - /// propagators compute the time-table from scratch upon backtracking + /// propagators compute the time-table from scratch upon backtracking. #[arg( help_heading = "Cumulative", long = "cumulative-incremental-backtracking" @@ -470,7 +472,7 @@ struct Args { /// The encoding to use for the upper bound constraint in a MaxSAT optimisation problem. /// - /// - The "generalised-totalizer" value specifies that the solver should use the Generalized + /// - The "generalized-totalizer" value specifies that the solver should use the Generalized /// Totalizer Encoding (see "Generalized totalizer encoding for pseudo-boolean constraints - /// Saurabh et al. (2015)") /// - The "cardinality-network" value specifies that the solver should use the Cardinality @@ -481,6 +483,7 @@ struct Args { long, value_enum, default_value_t, + verbatim_doc_comment, value_name = "ENCODING" )] upper_bound_encoding: PseudoBooleanEncoding, diff --git a/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/pseudo_boolean_constraint_encoder.rs b/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/pseudo_boolean_constraint_encoder.rs index 547aa0a2b..d6b1cf3dc 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/pseudo_boolean_constraint_encoder.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/pseudo_boolean_constraint_encoder.rs @@ -69,17 +69,20 @@ pub(crate) trait PseudoBooleanConstraintEncoderInterface { /// [`PseudoBooleanConstraintEncoder`]. #[derive(Default, Clone, Copy, Debug, ValueEnum)] pub(crate) enum PseudoBooleanEncoding { - /// Specifies the usage of the generalized totalizer encoding for pseudo-boolean constraints - /// \[1\]. + /// Specifies the usage of the generalized totalizer encoding for pseudo-boolean constraints. + /// + /// See \[1\] for more information. /// /// # Bibliography /// \[1] "Generalized totalizer encoding for pseudo-boolean constraints.", Joshi Saurabh, Ruben /// Martins, Vasco Manquinho; CP '15 #[default] GeneralizedTotalizer, - /// Specifies the usage of the cardinality network \[1\] encoding for unweighted cardinality - /// constraints in the form `x1 + ... + xn <= k`. The encoding is arc-consistent and - /// supports incremental strengthening of the upper bound. + /// Specifies the usage of the cardinality network encoding for unweighted cardinality + /// constraints in the form `x1 + ... + xn <= k`. + /// + /// The encoding \[1\] is arc-consistent and supports incremental strengthening of the upper + /// bound. /// /// # Bibliography /// \[1\] R. Asín, R. Nieuwenhuis, A. Oliveras, and E. Rodríguez-Carbonell, ‘Cardinality From a37c276babdae08a2e3885c24763d5c2aacba4c8 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Thu, 22 Oct 2026 11:47:56 +0200 Subject: [PATCH 8/9] chore: further cleanup for short help --- minizinc/pumpkin-for-proofs.msc | 30 +++--- minizinc/pumpkin.msc | 30 +++--- pumpkin-crates/core/src/optimisation/mod.rs | 8 +- pumpkin-solver/src/bin/pumpkin-solver/main.rs | 97 +++++++++++-------- 4 files changed, 95 insertions(+), 70 deletions(-) diff --git a/minizinc/pumpkin-for-proofs.msc b/minizinc/pumpkin-for-proofs.msc index 2386e3b31..ba9751cf9 100644 --- a/minizinc/pumpkin-for-proofs.msc +++ b/minizinc/pumpkin-for-proofs.msc @@ -27,25 +27,25 @@ ], [ "--optimisation-strategy", - "Determines what type of optimisation strategy is used by the solver [default: linear-sat-unsat] [possible values: linear-sat-unsat, linear-unsat-sat]", + "Determines what type of optimisation strategy is used by the solver. [default: linear-sat-unsat] [possible values: linear-sat-unsat, linear-unsat-sat]", "opt:linear-sat-unsat:linear-unsat-sat", "linear-sat-unsat" ], [ "--conflict-resolver", - "Determines the conflict resolver [default: one-uip] [possible values: no-learning, one-uip, all-decision, extended-cpip, bounds-extended-cpip]", + "Determines the conflict resolver. [default: one-uip] [possible values: no-learning, one-uip, all-decision, extended-cpip, bounds-extended-cpip]", "opt:no-learning:one-uip:all-decision:extended-cpip:bounds-extended-cpip", "one-uip" ], [ "--recursive-minimisation", - "Enables recursive minimisation of learned nogoods as a post-processing step after conflict analysis; according to the idea proposed in \"Generalized Conflict-Clause Strengthening for Satisfiability Solvers - Allen van Gelder (2011)\".", + "Enables recursive minimisation of learned nogoods.", "bool", "false" ], [ "--no-iterative-minimisation", - "Disables semantic minimisation of learned nogoods during conflict analysis; according to the idea proposed in \"Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)\".", + "Disables semantic minimisation of learned nogoods.", "bool", "false" ], @@ -81,13 +81,13 @@ ], [ "--memory-preallocated", - "The amount of memory (in MB) that is preallocated for storing nogoods [default: 50] [possible values: int]", + "The amount of memory (in MB) that is preallocated for storing nogoods. [default: 50] [possible values: int]", "int:0:18446744073709551615", "50" ], [ "--nogood-priority", - "The priority of the nogood propagator [default: very-low] [possible values: high, medium, low, very-low, ultra-low, lowest]", + "The priority of the nogood propagator. [default: very-low] [possible values: high, medium, low, very-low, ultra-low, lowest]", "opt:high:medium:low:very-low:ultra-low:lowest", "very-low" ], @@ -105,13 +105,13 @@ ], [ "--restart-base-interval", - "The base interval length is used as a multiplier to the restart sequence. [default: 50] [possible values: int]", + "The base interval length which is used as a multiplier to the restart sequence. [default: 50] [possible values: int]", "int:0:18446744073709551615", "50" ], [ "--restart-geometric-coef", - "The coefficient in the geometric sequence `x_i = x_{i-1} * \"--restart-geometric-coef\"` where `x_1 = \"--restart-base-interval\"`. Used only if \"--restart-sequence-generator-type\" is assigned to \"geometric\". [possible values: float]", + "The coefficient of the geometric restart sequence. [possible values: float]", "float", "" ], @@ -123,31 +123,31 @@ ], [ "--restart-lbd-coef", - "Used to determine if a restart should be forced (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). [default: 1.25] [possible values: float]", + "The coefficient used to determine whether a restart should be forced. [default: 1.25] [possible values: float]", "float", "1.25" ], [ "--restart-num-assigned-coef", - "Used to determine if a restart should be blocked (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). [default: 1.4] [possible values: float]", + "The coefficient used to determine whether a restart should be blocked. [default: 1.4] [possible values: float]", "float", "1.4" ], [ "--restart-num-assigned-window", - "Used to determine the length of the recent past that should be considered when deciding on blocking restarts (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). [default: 5000] [possible values: int]", + "The length of the recent past that is considered when deciding whether to block a restart. [default: 5000] [possible values: int]", "int:0:18446744073709551615", "5000" ], [ "--cumulative-propagation-method", - "Determines the type of propagator which is used by the cumulative propagator(s) to propagate the constraint. [default: time-table-over-interval-incremental] [possible values: time-table-per-point, time-table-per-point-incremental, time-table-per-point-incremental-synchronised, time-table-over-interval, time-table-over-interval-incremental, time-table-over-interval-incremental-synchronised]", + "Determines the type of propagator which is used for the cumulative constraint. [default: time-table-over-interval-incremental] [possible values: time-table-per-point, time-table-per-point-incremental, time-table-per-point-incremental-synchronised, time-table-over-interval, time-table-over-interval-incremental, time-table-over-interval-incremental-synchronised]", "opt:time-table-per-point:time-table-per-point-incremental:time-table-per-point-incremental-synchronised:time-table-over-interval:time-table-over-interval-incremental:time-table-over-interval-incremental-synchronised", "time-table-over-interval-incremental" ], [ "--cumulative-explanation-type", - "Determines the type of explanation used by the cumulative propagator(s) to explain propagations/conflicts [default: pointwise] [possible values: naive, big-step, pointwise]", + "Determines the type of explanation used by the cumulative propagator(s). [default: pointwise] [possible values: naive, big-step, pointwise]", "opt:naive:big-step:pointwise", "pointwise" ], @@ -159,13 +159,13 @@ ], [ "--cumulative-single-profiles", - "Determines whether single profiles are used when explaining a propagation of the cumulative constraint", + "Uses single profiles when explaining propagations of the cumulative constraint.", "bool", "false" ], [ "--cumulative-incremental-backtracking", - "Determines whether incremental backtracking is applied or whether the cumulative propagators compute the time-table from scratch upon backtracking", + "Enables incremental backtracking for the cumulative propagator(s).", "bool", "false" ] diff --git a/minizinc/pumpkin.msc b/minizinc/pumpkin.msc index 741ac0e6e..256cafa70 100644 --- a/minizinc/pumpkin.msc +++ b/minizinc/pumpkin.msc @@ -27,25 +27,25 @@ ], [ "--optimisation-strategy", - "Determines what type of optimisation strategy is used by the solver [default: linear-sat-unsat] [possible values: linear-sat-unsat, linear-unsat-sat]", + "Determines what type of optimisation strategy is used by the solver. [default: linear-sat-unsat] [possible values: linear-sat-unsat, linear-unsat-sat]", "opt:linear-sat-unsat:linear-unsat-sat", "linear-sat-unsat" ], [ "--conflict-resolver", - "Determines the conflict resolver [default: one-uip] [possible values: no-learning, one-uip, all-decision, extended-cpip, bounds-extended-cpip]", + "Determines the conflict resolver. [default: one-uip] [possible values: no-learning, one-uip, all-decision, extended-cpip, bounds-extended-cpip]", "opt:no-learning:one-uip:all-decision:extended-cpip:bounds-extended-cpip", "one-uip" ], [ "--recursive-minimisation", - "Enables recursive minimisation of learned nogoods as a post-processing step after conflict analysis; according to the idea proposed in \"Generalized Conflict-Clause Strengthening for Satisfiability Solvers - Allen van Gelder (2011)\".", + "Enables recursive minimisation of learned nogoods.", "bool", "false" ], [ "--no-iterative-minimisation", - "Disables semantic minimisation of learned nogoods during conflict analysis; according to the idea proposed in \"Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)\".", + "Disables semantic minimisation of learned nogoods.", "bool", "false" ], @@ -81,13 +81,13 @@ ], [ "--memory-preallocated", - "The amount of memory (in MB) that is preallocated for storing nogoods [default: 50] [possible values: int]", + "The amount of memory (in MB) that is preallocated for storing nogoods. [default: 50] [possible values: int]", "int:0:18446744073709551615", "50" ], [ "--nogood-priority", - "The priority of the nogood propagator [default: very-low] [possible values: high, medium, low, very-low, ultra-low, lowest]", + "The priority of the nogood propagator. [default: very-low] [possible values: high, medium, low, very-low, ultra-low, lowest]", "opt:high:medium:low:very-low:ultra-low:lowest", "very-low" ], @@ -105,13 +105,13 @@ ], [ "--restart-base-interval", - "The base interval length is used as a multiplier to the restart sequence. [default: 50] [possible values: int]", + "The base interval length which is used as a multiplier to the restart sequence. [default: 50] [possible values: int]", "int:0:18446744073709551615", "50" ], [ "--restart-geometric-coef", - "The coefficient in the geometric sequence `x_i = x_{i-1} * \"--restart-geometric-coef\"` where `x_1 = \"--restart-base-interval\"`. Used only if \"--restart-sequence-generator-type\" is assigned to \"geometric\". [possible values: float]", + "The coefficient of the geometric restart sequence. [possible values: float]", "float", "" ], @@ -123,31 +123,31 @@ ], [ "--restart-lbd-coef", - "Used to determine if a restart should be forced (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). [default: 1.25] [possible values: float]", + "The coefficient used to determine whether a restart should be forced. [default: 1.25] [possible values: float]", "float", "1.25" ], [ "--restart-num-assigned-coef", - "Used to determine if a restart should be blocked (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). [default: 1.4] [possible values: float]", + "The coefficient used to determine whether a restart should be blocked. [default: 1.4] [possible values: float]", "float", "1.4" ], [ "--restart-num-assigned-window", - "Used to determine the length of the recent past that should be considered when deciding on blocking restarts (see \"Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)\"). [default: 5000] [possible values: int]", + "The length of the recent past that is considered when deciding whether to block a restart. [default: 5000] [possible values: int]", "int:0:18446744073709551615", "5000" ], [ "--cumulative-propagation-method", - "Determines the type of propagator which is used by the cumulative propagator(s) to propagate the constraint. [default: time-table-over-interval-incremental] [possible values: time-table-per-point, time-table-per-point-incremental, time-table-per-point-incremental-synchronised, time-table-over-interval, time-table-over-interval-incremental, time-table-over-interval-incremental-synchronised]", + "Determines the type of propagator which is used for the cumulative constraint. [default: time-table-over-interval-incremental] [possible values: time-table-per-point, time-table-per-point-incremental, time-table-per-point-incremental-synchronised, time-table-over-interval, time-table-over-interval-incremental, time-table-over-interval-incremental-synchronised]", "opt:time-table-per-point:time-table-per-point-incremental:time-table-per-point-incremental-synchronised:time-table-over-interval:time-table-over-interval-incremental:time-table-over-interval-incremental-synchronised", "time-table-over-interval-incremental" ], [ "--cumulative-explanation-type", - "Determines the type of explanation used by the cumulative propagator(s) to explain propagations/conflicts [default: pointwise] [possible values: naive, big-step, pointwise]", + "Determines the type of explanation used by the cumulative propagator(s). [default: pointwise] [possible values: naive, big-step, pointwise]", "opt:naive:big-step:pointwise", "pointwise" ], @@ -159,13 +159,13 @@ ], [ "--cumulative-single-profiles", - "Determines whether single profiles are used when explaining a propagation of the cumulative constraint", + "Uses single profiles when explaining propagations of the cumulative constraint.", "bool", "false" ], [ "--cumulative-incremental-backtracking", - "Determines whether incremental backtracking is applied or whether the cumulative propagators compute the time-table from scratch upon backtracking", + "Enables incremental backtracking for the cumulative propagator(s).", "bool", "false" ] diff --git a/pumpkin-crates/core/src/optimisation/mod.rs b/pumpkin-crates/core/src/optimisation/mod.rs index 5b581e336..9fdb540f3 100644 --- a/pumpkin-crates/core/src/optimisation/mod.rs +++ b/pumpkin-crates/core/src/optimisation/mod.rs @@ -28,11 +28,15 @@ pub trait OptimisationProcedure). @@ -103,9 +105,10 @@ struct Args { )] random_seed: u64, - /// Instructs the solver to report all solutions in the case of satisfaction problems, - /// or print intermediate solutions of increasing quality in the case of optimisation - /// problems. + /// Reports all solutions (satisfaction) or all intermediate solutions (optimisation). + /// + /// For satisfaction problems, every solution is reported. For optimisation problems, solutions + /// of increasing quality are reported as they are found. /// /// See the MiniZinc specification () /// for more information. @@ -162,6 +165,7 @@ struct Args { long, value_enum, default_value_t, + verbatim_doc_comment, value_name = "TYPE" )] proof_type: ProofType, @@ -172,12 +176,12 @@ struct Args { long = "optimisation-strategy", value_enum, default_value_t, + verbatim_doc_comment, value_name = "STRATEGY" )] optimisation_strategy: OptimisationStrategy, - /// Instructs the solver to perform free search when solving a MiniZinc model; this flag - /// indicates that it is allowed to ignore the search annotations specified in the model. + /// Allows the solver to ignore the search annotations specified in a MiniZinc model. /// /// See the MiniZinc specification () /// for more information. @@ -195,13 +199,16 @@ struct Args { long, value_enum, default_value_t, + verbatim_doc_comment, value_name = "RESOLVER" )] conflict_resolver: ConflictResolverType, - /// Enables recursive minimisation of learned nogoods as a post-processing step after conflict - /// analysis; according to the idea proposed in "Generalized Conflict-Clause Strengthening for - /// Satisfiability Solvers - Allen van Gelder (2011)". + /// Enables recursive minimisation of learned nogoods. + /// + /// The minimisation is applied as a post-processing step after conflict analysis; according to + /// the idea proposed in "Generalized Conflict-Clause Strengthening for Satisfiability Solvers + /// - Allen van Gelder (2011)". #[arg( help_heading = "Conflict Analysis", long = "recursive-minimisation", @@ -209,11 +216,10 @@ struct Args { )] recursive_minimisation: bool, - /// Disables semantic minimisation of learned nogoods during conflict analysis; according to - /// the idea proposed in "Semantic Learning for Lazy Clause Generation - Feydy et al. - /// (2013)". + /// Disables semantic minimisation of learned nogoods during conflict analysis. /// - /// By default, the minimisation is turned on. + /// By default, semantic minimisation is applied during conflict analysis; according to the + /// idea proposed in "Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)". #[arg( help_heading = "Conflict Analysis", long = "no-iterative-minimisation", @@ -298,6 +304,7 @@ struct Args { help_heading = "Nogood Database", long = "memory-preallocated", default_value_t = 50, + verbatim_doc_comment, value_name = "MB" )] memory_preallocated: usize, @@ -308,6 +315,7 @@ struct Args { long = "nogood-priority", value_enum, default_value_t, + verbatim_doc_comment, value_name = "PRIORITY" )] nogood_propagator_priority: Priority, @@ -336,7 +344,8 @@ struct Args { )] restart_sequence_generator_type: SequenceGeneratorType, - /// The base interval length is used as a multiplier to the restart sequence. + /// The base interval length which is used as a multiplier to the restart sequence. + /// /// - In the case of the "constant" restart sequence this argument indicates the constant which /// is used to determine when a restart occurs /// - For the "geometric" approach this argument indicates the starting value of the sequence @@ -353,9 +362,11 @@ struct Args { )] restart_base_interval: u64, - /// The coefficient in the geometric sequence `x_i = x_{i-1} * "--restart-geometric-coef"` - /// where `x_1 = "--restart-base-interval"`. Used only if "--restart-sequence-generator-type" - /// is assigned to "geometric". + /// The coefficient of the geometric restart sequence. + /// + /// The sequence is defined as `x_i = x_{i-1} * "--restart-geometric-coef"` where + /// `x_1 = "--restart-base-interval"`. Used only if "--restart-sequence-generator-type" is + /// assigned to "geometric". #[arg( help_heading = "Restarts", long = "restart-geometric-coef", @@ -377,8 +388,9 @@ struct Args { )] restart_min_num_conflicts_before_first_restart: u64, - /// Used to determine if a restart should be forced (see "Refining Restarts Strategies for SAT - /// and UNSAT - Audemard and Simon (2012)"). + /// The coefficient used to determine whether a restart should be forced. + /// + /// See "Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)". /// /// The state is "bad" if the current LBD value is much greater than /// the global LBD average. A greater (lower) value for lbd-coef means a less (more) frequent @@ -393,8 +405,9 @@ struct Args { )] restart_lbd_coef: f64, - /// Used to determine if a restart should be blocked (see "Refining Restarts Strategies for SAT - /// and UNSAT - Audemard and Simon (2012)"). + /// The coefficient used to determine whether a restart should be blocked. + /// + /// See "Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)". /// /// To be used in combination with "--restart-num-assigned-window". /// @@ -410,9 +423,9 @@ struct Args { )] restart_num_assigned_coef: f64, - /// Used to determine the length of the recent past that should be considered when deciding on - /// blocking restarts (see "Refining Restarts Strategies for SAT - /// and UNSAT - Audemard and Simon (2012)"). + /// The length of the recent past that is considered when deciding whether to block a restart. + /// + /// See "Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)". /// /// The solver considers the last "--restart-num-assigned-window" conflicts as the reference /// point for the number of assigned variables. @@ -425,8 +438,7 @@ struct Args { )] restart_num_assigned_window: u64, - /// Determines the type of propagator which is used by the cumulative propagator(s) to - /// propagate the constraint. + /// Determines the type of propagator which is used for the cumulative constraint. /// /// Currently, the solver only supports variations on time-tabling methods. #[arg( @@ -434,17 +446,18 @@ struct Args { long, value_enum, default_value_t, + verbatim_doc_comment, value_name = "PROPAGATION" )] cumulative_propagation_method: CumulativePropagationMethod, - /// Determines the type of explanation used by the cumulative propagator(s) to explain - /// propagations/conflicts. + /// Determines the type of explanation used by the cumulative propagator(s). #[arg( help_heading = "Cumulative", long, value_enum, default_value_t, + verbatim_doc_comment, value_name = "EXPLANATION" )] cumulative_explanation_type: CumulativeExplanationType, @@ -457,16 +470,22 @@ struct Args { )] cumulative_allow_holes: bool, - /// Determines whether single profiles are used when explaining a propagation of the cumulative - /// constraint. - #[arg(help_heading = "Cumulative", long = "cumulative-single-profiles")] + /// Uses single profiles when explaining propagations of the cumulative constraint. + #[arg( + help_heading = "Cumulative", + long = "cumulative-single-profiles", + verbatim_doc_comment + )] cumulative_single_profiles: bool, - /// Determines whether incremental backtracking is applied or whether the cumulative - /// propagators compute the time-table from scratch upon backtracking. + /// Enables incremental backtracking for the cumulative propagator(s). + /// + /// Otherwise, the cumulative propagator(s) compute the time-table from scratch upon + /// backtracking. #[arg( help_heading = "Cumulative", - long = "cumulative-incremental-backtracking" + long = "cumulative-incremental-backtracking", + verbatim_doc_comment )] cumulative_incremental_backtracking: bool, @@ -488,8 +507,9 @@ struct Args { )] upper_bound_encoding: PseudoBooleanEncoding, - /// If `--verbose` is enabled then this option removes the timestamp information from the log - /// messages (only applicable for (W)CNF instances). + /// Removes the timestamp information from the log messages. + /// + /// Only applicable if `--verbose` is enabled, and only for (W)CNF instances. #[arg( help_heading = "Max(SAT)", long = "omit-timestamp", @@ -497,8 +517,9 @@ struct Args { )] omit_timestamp: bool, - /// If `--verbose` is enabled then this option removes the call site information from the log - /// messages (only applicable for (W)CNF instances). + /// Removes the call site information from the log messages. + /// + /// Only applicable if `--verbose` is enabled, and only for (W)CNF instances. /// /// The call site is the file and line from which the message originated. #[arg( From a2ca3e9df6dddb36835051b33e05c4a8a1e14875 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Thu, 22 Oct 2026 11:53:21 +0200 Subject: [PATCH 9/9] chore: make requirements between flags explicit --- minizinc/pumpkin-for-proofs.msc | 2 +- minizinc/pumpkin.msc | 2 +- pumpkin-solver/src/bin/pumpkin-solver/main.rs | 25 +++++++++++++++---- 3 files changed, 22 insertions(+), 7 deletions(-) diff --git a/minizinc/pumpkin-for-proofs.msc b/minizinc/pumpkin-for-proofs.msc index ba9751cf9..9128b513c 100644 --- a/minizinc/pumpkin-for-proofs.msc +++ b/minizinc/pumpkin-for-proofs.msc @@ -45,7 +45,7 @@ ], [ "--no-iterative-minimisation", - "Disables semantic minimisation of learned nogoods.", + "Disables semantic minimisation of learned nogoods during conflict analysis.", "bool", "false" ], diff --git a/minizinc/pumpkin.msc b/minizinc/pumpkin.msc index 256cafa70..b9d40a3c1 100644 --- a/minizinc/pumpkin.msc +++ b/minizinc/pumpkin.msc @@ -45,7 +45,7 @@ ], [ "--no-iterative-minimisation", - "Disables semantic minimisation of learned nogoods.", + "Disables semantic minimisation of learned nogoods during conflict analysis.", "bool", "false" ], diff --git a/pumpkin-solver/src/bin/pumpkin-solver/main.rs b/pumpkin-solver/src/bin/pumpkin-solver/main.rs index b0610ca57..2e148bc7b 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/main.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/main.rs @@ -159,14 +159,15 @@ struct Args { /// What type of proof to log. /// - /// If the `proof_path` option is not provided, this is ignored. + /// Requires "--proof-path" to be provided. #[arg( help_heading = "Proof Logging", long, value_enum, default_value_t, verbatim_doc_comment, - value_name = "TYPE" + value_name = "TYPE", + requires = "proof_path" )] proof_type: ProofType, @@ -321,7 +322,20 @@ struct Args { nogood_propagator_priority: Priority, /// Determines that no restarts are allowed by the solver. - #[arg(help_heading = "Restarts", long = "no-restarts", verbatim_doc_comment)] + #[arg( + help_heading = "Restarts", + long = "no-restarts", + verbatim_doc_comment, + conflicts_with_all = [ + "restart_sequence_generator_type", + "restart_base_interval", + "restart_geometric_coef", + "restart_min_num_conflicts_before_first_restart", + "restart_lbd_coef", + "restart_num_assigned_coef", + "restart_num_assigned_window", + ] + )] no_restarts: bool, /// Decides the sequence based on which the restarts are performed. @@ -365,13 +379,14 @@ struct Args { /// The coefficient of the geometric restart sequence. /// /// The sequence is defined as `x_i = x_{i-1} * "--restart-geometric-coef"` where - /// `x_1 = "--restart-base-interval"`. Used only if "--restart-sequence-generator-type" is + /// `x_1 = "--restart-base-interval"`. Required if "--restart-sequence-generator-type" is /// assigned to "geometric". #[arg( help_heading = "Restarts", long = "restart-geometric-coef", verbatim_doc_comment, - value_name = "f64" + value_name = "f64", + required_if_eq("restart_sequence_generator_type", "geometric") )] restart_geometric_coef: Option,