Skip to content

Make log encoding domain threshold configurable by adding log_encoding_domain_threshold config option#85

Draft
Copilot wants to merge 4 commits intomainfrom
copilot/fix-7f1ac238-e797-4346-afc5-be1c0c68b1b3
Draft

Make log encoding domain threshold configurable by adding log_encoding_domain_threshold config option#85
Copilot wants to merge 4 commits intomainfrom
copilot/fix-7f1ac238-e797-4346-afc5-be1c0c68b1b3

Conversation

Copy link
Contributor

Copilot AI commented Aug 9, 2025

This PR resolves the TODO comment at line 600 in cspuz_core/src/encoder/mod.rs by making the hardcoded domain size threshold of 500 configurable for log encoding decisions.

Problem

The encoder used a hardcoded value of 500 to determine when to use log encoding for variables with large domains in complex constraints. This made it impossible for users to tune the log encoding behavior based on their specific use cases.

Solution

Added a new configuration field log_encoding_domain_threshold to the Config struct with the following changes:

  • Config struct: Added log_encoding_domain_threshold: usize field with default value 500
  • CLI support: Added --log-encoding-domain-threshold command-line option with help text
  • Encoder logic: Replaced hardcoded 500 value at line 600 with config.log_encoding_domain_threshold
  • Tests: Added unit test to verify the configuration field works correctly

Note: The threshold at line 690 for direct encoding decisions remains hardcoded at 500, as it serves a different purpose and should not be unified with the log encoding threshold.

Usage

Users can now configure the log encoding threshold via CLI:

# Use a higher threshold (prefer log encoding less often for complex constraints)
./cli --log-encoding-domain-threshold 1000 input.smt2

# Use a lower threshold (prefer log encoding more often for complex constraints)  
./cli --log-encoding-domain-threshold 100 input.smt2

Or programmatically:

let mut config = Config::default();
config.log_encoding_domain_threshold = 1000;

Backward Compatibility

The default value remains 500, so existing behavior is preserved. All existing tests continue to pass.


💡 You can make Copilot smarter by setting up custom instructions, customizing its development environment and configuring Model Context Protocol (MCP) servers. Learn more Copilot coding agent tips in the docs.

Copilot AI and others added 2 commits August 9, 2025 15:41
…d config option

Co-authored-by: semiexp <7336994+semiexp@users.noreply.github.com>
Co-authored-by: semiexp <7336994+semiexp@users.noreply.github.com>
Copilot AI changed the title [WIP] In cspuz_core/src/encoder/mod.rs, there is "TODO: make this configurable" comment. Resolve this TODO Make domain threshold configurable by adding encoding_domain_threshold config option Aug 9, 2025
Copilot AI requested a review from semiexp August 9, 2025 15:45
if let IntVarRepresentation::Domain(domain) = repr {
if domain.num_candidates() > 500 && complex_constraints_vars.contains(&var) {
// TODO: make this configurable
if domain.num_candidates() > config.encoding_domain_threshold && complex_constraints_vars.contains(&var) {
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

make it clear that this config is related to log encoding

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fixed in commit a661300. Renamed the config field to log_encoding_domain_threshold and updated CLI option to --log-encoding-domain-threshold to make it clear this config is specifically for log encoding decisions.

let repr = norm_vars.int_var(var);
let use_direct_encoding = match repr {
IntVarRepresentation::Domain(domain) => domain.num_candidates() <= 500,
IntVarRepresentation::Domain(domain) => domain.num_candidates() <= config.encoding_domain_threshold,
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this threshold 500 is not related

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fixed in commit a661300. Reverted this threshold back to the hardcoded value of 500, as you're correct - this threshold for direct encoding is conceptually different from the log encoding threshold and should not share the same configuration.

Copy link
Owner

@semiexp semiexp left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

check two comments

@semiexp
Copy link
Owner

semiexp commented Aug 10, 2025

@copilot check two comments

…ding threshold to hardcoded 500

Co-authored-by: semiexp <7336994+semiexp@users.noreply.github.com>
Copilot AI changed the title Make domain threshold configurable by adding encoding_domain_threshold config option Make log encoding domain threshold configurable by adding log_encoding_domain_threshold config option Aug 10, 2025
Copilot AI requested a review from semiexp August 10, 2025 03:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants