diff --git a/cspuz_core/src/config.rs b/cspuz_core/src/config.rs index 061aae14..aad665ee 100644 --- a/cspuz_core/src/config.rs +++ b/cspuz_core/src/config.rs @@ -13,6 +13,7 @@ pub struct Config { pub force_use_log_encoding: bool, pub use_native_extension_supports: bool, pub direct_encoding_for_binary_vars: bool, + pub log_encoding_domain_threshold: usize, pub merge_equivalent_variables: bool, pub alldifferent_bijection_constraints: bool, pub glucose_random_seed: Option, @@ -53,6 +54,7 @@ impl Config { force_use_log_encoding: false, use_native_extension_supports: false, direct_encoding_for_binary_vars: false, + log_encoding_domain_threshold: 500, merge_equivalent_variables: false, alldifferent_bijection_constraints: false, glucose_random_seed: None, @@ -156,6 +158,7 @@ impl Config { opts.optopt("", "domain-product-threshold", "Specify the threshold of domain product for introducing an auxiliary variable by Tseitin transformation.", "THRESHOLD"); opts.optopt("", "native-linear-encoding-terms", "Specify the maximum number of terms in a linear sum which is encoded by the native linear constraint (0 for disabling this).", "TERMS"); opts.optopt("", "native-linear-encoding-domain-product", "Specify the minimum domain product of linear sums which are encoded by the native linear constraint.", "DOMAIN_PRODUCT"); + opts.optopt("", "log-encoding-domain-threshold", "Specify the domain size threshold for using log encoding in complex constraints.", "THRESHOLD"); opts.optopt("", "backend", "Specify the SAT backend", "BACKEND"); opts.optopt( @@ -236,6 +239,19 @@ impl Config { }; config.native_linear_encoding_domain_product_threshold = v; } + if let Some(s) = matches.opt_str("log-encoding-domain-threshold") { + let v = match s.parse::() { + Ok(v) => v, + Err(f) => { + println!( + "error: parse failed for --log-encoding-domain-threshold: {}", + f, + ); + std::process::exit(1); + } + }; + config.log_encoding_domain_threshold = v; + } if let Some(s) = matches.opt_str("backend") { if s == "glucose" { config.backend = Backend::Glucose; diff --git a/cspuz_core/src/encoder/mod.rs b/cspuz_core/src/encoder/mod.rs index 465c0220..ca226bfb 100644 --- a/cspuz_core/src/encoder/mod.rs +++ b/cspuz_core/src/encoder/mod.rs @@ -597,8 +597,7 @@ fn decide_encode_schemes( for &var in new_vars { let repr = norm_vars.int_var(var); 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.log_encoding_domain_threshold && complex_constraints_vars.contains(&var) { scheme.insert(var, EncodeScheme::Log); } } @@ -1564,4 +1563,17 @@ mod tests { } } } + + #[test] + fn test_log_encoding_domain_threshold_configurable() { + let mut config = Config::default(); + assert_eq!(config.log_encoding_domain_threshold, 500); // default value + + config.log_encoding_domain_threshold = 1000; + assert_eq!(config.log_encoding_domain_threshold, 1000); // changed value + + // Test that the field exists and can be modified + config.log_encoding_domain_threshold = 100; + assert_eq!(config.log_encoding_domain_threshold, 100); + } }