diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs b/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs index ef4af5328..5ba85e1d3 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs @@ -515,7 +515,9 @@ impl ConflictAnalysisContext<'_> { conflict.trigger_reason, ExplanationContext::without_working_nogood( self.assignments, - self.assignments.num_trail_entries() - 1, + self.assignments.num_trail_entries(), // Note that we do not do a + // `-1` here; the `Assignments` automatically undoes the last trail entry when an + // empty domain is created meaning that the `-1` has already been applied. self.notification_engine, ), self.propagators, diff --git a/pumpkin-solver/tests/mzn_infeasible/connected.fzn b/pumpkin-solver/tests/mzn_infeasible/connected.fzn new file mode 100644 index 000000000..dd379ca70 --- /dev/null +++ b/pumpkin-solver/tests/mzn_infeasible/connected.fzn @@ -0,0 +1,203 @@ +% Generated by MiniZinc 2.9.3 + +predicate int_lin_eq_imp(array [int] of int: as,array [int] of var int: bs,int: c,var bool: r); +predicate int_eq_imp(var int: a,var int: b,var bool: r); +array [1..16] of bool: X_INTRODUCED_4_ = [false,true,true,true,true,false,true,false,true,false,true,false,false,true,true,false]; +array [1..2] of int: X_INTRODUCED_140_ = [1,-1]; +var 1..16: X_INTRODUCED_7_ ::var_is_introduced ; +var 0..15: X_INTRODUCED_15_ ::var_is_introduced ; +var 0..15: X_INTRODUCED_16_ ::var_is_introduced ; +var 0..15: X_INTRODUCED_17_ ::var_is_introduced ; +var 0..15: X_INTRODUCED_18_ ::var_is_introduced ; +var 0..15: X_INTRODUCED_20_ ::var_is_introduced ; +var 0..15: X_INTRODUCED_22_ ::var_is_introduced ; +var 0..15: X_INTRODUCED_24_ ::var_is_introduced ; +var 0..15: X_INTRODUCED_27_ ::var_is_introduced ; +var 0..15: X_INTRODUCED_28_ ::var_is_introduced ; +var 1..16: X_INTRODUCED_32_ ::var_is_introduced ; +var 1..16: X_INTRODUCED_33_ ::var_is_introduced ; +var 1..16: X_INTRODUCED_34_ ::var_is_introduced ; +var 1..16: X_INTRODUCED_35_ ::var_is_introduced ; +var 1..16: X_INTRODUCED_37_ ::var_is_introduced ; +var 1..16: X_INTRODUCED_39_ ::var_is_introduced ; +var 1..16: X_INTRODUCED_41_ ::var_is_introduced ; +var 1..16: X_INTRODUCED_44_ ::var_is_introduced ; +var 1..16: X_INTRODUCED_45_ ::var_is_introduced ; +var bool: X_INTRODUCED_49_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_50_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_51_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_52_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_54_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_56_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_58_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_61_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_62_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_83_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_84_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_86_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_87_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_89_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_90_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_92_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_93_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_98_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_99_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_104_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_105_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_110_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_111_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_119_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_120_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_122_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_123_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_128_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_129_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_130_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_131_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_132_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_133_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_134_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_135_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_136_ ::var_is_introduced :: is_defined_var; +var 0..15: X_INTRODUCED_142_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_144_ ::var_is_introduced :: is_defined_var; +var 0..15: X_INTRODUCED_145_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_147_ ::var_is_introduced :: is_defined_var; +var 0..15: X_INTRODUCED_148_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_150_ ::var_is_introduced :: is_defined_var; +var 0..15: X_INTRODUCED_151_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_153_ ::var_is_introduced :: is_defined_var; +var 0..15: X_INTRODUCED_157_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_159_ ::var_is_introduced :: is_defined_var; +var 0..15: X_INTRODUCED_163_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_165_ ::var_is_introduced :: is_defined_var; +var 0..15: X_INTRODUCED_169_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_171_ ::var_is_introduced :: is_defined_var; +var 0..15: X_INTRODUCED_178_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_180_ ::var_is_introduced :: is_defined_var; +var 0..15: X_INTRODUCED_181_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_183_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_187_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_188_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_189_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_190_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_192_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_193_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_194_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_195_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_197_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_198_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_199_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_201_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_202_ ::var_is_introduced :: is_defined_var; +var bool: X_INTRODUCED_203_ ::var_is_introduced :: is_defined_var; +array [1..16] of var int: X_INTRODUCED_11_ ::var_is_introduced = [0,X_INTRODUCED_15_,X_INTRODUCED_16_,X_INTRODUCED_17_,X_INTRODUCED_18_,0,X_INTRODUCED_20_,0,X_INTRODUCED_22_,0,X_INTRODUCED_24_,0,0,X_INTRODUCED_27_,X_INTRODUCED_28_,0]; +array [1..16] of var int: X_INTRODUCED_12_ ::var_is_introduced = [1,X_INTRODUCED_32_,X_INTRODUCED_33_,X_INTRODUCED_34_,X_INTRODUCED_35_,6,X_INTRODUCED_37_,8,X_INTRODUCED_39_,10,X_INTRODUCED_41_,12,13,X_INTRODUCED_44_,X_INTRODUCED_45_,16]; +constraint array_bool_element(X_INTRODUCED_7_,X_INTRODUCED_4_,true); +constraint array_var_int_element(X_INTRODUCED_7_,X_INTRODUCED_11_,0); +constraint array_var_int_element(X_INTRODUCED_7_,X_INTRODUCED_12_,X_INTRODUCED_7_); +constraint array_bool_element(X_INTRODUCED_32_,X_INTRODUCED_4_,X_INTRODUCED_128_):: defines_var(X_INTRODUCED_128_); +constraint bool_clause([X_INTRODUCED_128_,X_INTRODUCED_49_],[]); +constraint array_bool_element(X_INTRODUCED_33_,X_INTRODUCED_4_,X_INTRODUCED_129_):: defines_var(X_INTRODUCED_129_); +constraint bool_clause([X_INTRODUCED_129_,X_INTRODUCED_50_],[]); +constraint array_bool_element(X_INTRODUCED_34_,X_INTRODUCED_4_,X_INTRODUCED_130_):: defines_var(X_INTRODUCED_130_); +constraint bool_clause([X_INTRODUCED_130_,X_INTRODUCED_51_],[]); +constraint array_bool_element(X_INTRODUCED_35_,X_INTRODUCED_4_,X_INTRODUCED_131_):: defines_var(X_INTRODUCED_131_); +constraint bool_clause([X_INTRODUCED_131_,X_INTRODUCED_52_],[]); +constraint array_bool_element(X_INTRODUCED_37_,X_INTRODUCED_4_,X_INTRODUCED_132_):: defines_var(X_INTRODUCED_132_); +constraint bool_clause([X_INTRODUCED_132_,X_INTRODUCED_54_],[]); +constraint array_bool_element(X_INTRODUCED_39_,X_INTRODUCED_4_,X_INTRODUCED_133_):: defines_var(X_INTRODUCED_133_); +constraint bool_clause([X_INTRODUCED_133_,X_INTRODUCED_56_],[]); +constraint array_bool_element(X_INTRODUCED_41_,X_INTRODUCED_4_,X_INTRODUCED_134_):: defines_var(X_INTRODUCED_134_); +constraint bool_clause([X_INTRODUCED_134_,X_INTRODUCED_58_],[]); +constraint array_bool_element(X_INTRODUCED_44_,X_INTRODUCED_4_,X_INTRODUCED_135_):: defines_var(X_INTRODUCED_135_); +constraint bool_clause([X_INTRODUCED_135_,X_INTRODUCED_61_],[]); +constraint array_bool_element(X_INTRODUCED_45_,X_INTRODUCED_4_,X_INTRODUCED_136_):: defines_var(X_INTRODUCED_136_); +constraint bool_clause([X_INTRODUCED_136_,X_INTRODUCED_62_],[]); +constraint array_var_int_element(X_INTRODUCED_32_,X_INTRODUCED_11_,X_INTRODUCED_142_):: defines_var(X_INTRODUCED_142_); +constraint bool_clause([X_INTRODUCED_144_,X_INTRODUCED_49_],[]); +constraint array_var_int_element(X_INTRODUCED_33_,X_INTRODUCED_11_,X_INTRODUCED_145_):: defines_var(X_INTRODUCED_145_); +constraint bool_clause([X_INTRODUCED_147_,X_INTRODUCED_50_],[]); +constraint array_var_int_element(X_INTRODUCED_34_,X_INTRODUCED_11_,X_INTRODUCED_148_):: defines_var(X_INTRODUCED_148_); +constraint bool_clause([X_INTRODUCED_150_,X_INTRODUCED_51_],[]); +constraint array_var_int_element(X_INTRODUCED_35_,X_INTRODUCED_11_,X_INTRODUCED_151_):: defines_var(X_INTRODUCED_151_); +constraint bool_clause([X_INTRODUCED_153_,X_INTRODUCED_52_],[]); +constraint array_var_int_element(X_INTRODUCED_37_,X_INTRODUCED_11_,X_INTRODUCED_157_):: defines_var(X_INTRODUCED_157_); +constraint bool_clause([X_INTRODUCED_159_,X_INTRODUCED_54_],[]); +constraint array_var_int_element(X_INTRODUCED_39_,X_INTRODUCED_11_,X_INTRODUCED_163_):: defines_var(X_INTRODUCED_163_); +constraint bool_clause([X_INTRODUCED_165_,X_INTRODUCED_56_],[]); +constraint array_var_int_element(X_INTRODUCED_41_,X_INTRODUCED_11_,X_INTRODUCED_169_):: defines_var(X_INTRODUCED_169_); +constraint bool_clause([X_INTRODUCED_171_,X_INTRODUCED_58_],[]); +constraint array_var_int_element(X_INTRODUCED_44_,X_INTRODUCED_11_,X_INTRODUCED_178_):: defines_var(X_INTRODUCED_178_); +constraint bool_clause([X_INTRODUCED_180_,X_INTRODUCED_61_],[]); +constraint array_var_int_element(X_INTRODUCED_45_,X_INTRODUCED_11_,X_INTRODUCED_181_):: defines_var(X_INTRODUCED_181_); +constraint bool_clause([X_INTRODUCED_183_,X_INTRODUCED_62_],[]); +constraint bool_clause([X_INTRODUCED_187_,X_INTRODUCED_49_],[]); +constraint bool_clause([X_INTRODUCED_190_,X_INTRODUCED_189_,X_INTRODUCED_188_,X_INTRODUCED_50_],[]); +constraint bool_clause([X_INTRODUCED_192_,X_INTRODUCED_51_],[]); +constraint bool_clause([X_INTRODUCED_193_,X_INTRODUCED_52_],[]); +constraint bool_clause([X_INTRODUCED_195_,X_INTRODUCED_194_,X_INTRODUCED_54_],[]); +constraint bool_clause([X_INTRODUCED_197_,X_INTRODUCED_56_],[]); +constraint bool_clause([X_INTRODUCED_199_,X_INTRODUCED_198_,X_INTRODUCED_58_],[]); +constraint bool_clause([X_INTRODUCED_201_,X_INTRODUCED_61_],[]); +constraint bool_clause([X_INTRODUCED_203_,X_INTRODUCED_202_,X_INTRODUCED_62_],[]); +constraint bool_clause([X_INTRODUCED_84_,X_INTRODUCED_83_],[]); +constraint bool_clause([X_INTRODUCED_87_,X_INTRODUCED_86_],[]); +constraint bool_clause([X_INTRODUCED_90_,X_INTRODUCED_89_],[]); +constraint bool_clause([X_INTRODUCED_93_,X_INTRODUCED_92_],[]); +constraint bool_clause([X_INTRODUCED_99_,X_INTRODUCED_98_],[]); +constraint bool_clause([X_INTRODUCED_105_,X_INTRODUCED_104_],[]); +constraint bool_clause([X_INTRODUCED_111_,X_INTRODUCED_110_],[]); +constraint bool_clause([X_INTRODUCED_120_,X_INTRODUCED_119_],[]); +constraint bool_clause([X_INTRODUCED_123_,X_INTRODUCED_122_],[]); +constraint int_eq_reif(X_INTRODUCED_32_,2,X_INTRODUCED_49_):: defines_var(X_INTRODUCED_49_); +constraint int_eq_reif(X_INTRODUCED_33_,3,X_INTRODUCED_50_):: defines_var(X_INTRODUCED_50_); +constraint int_eq_reif(X_INTRODUCED_34_,4,X_INTRODUCED_51_):: defines_var(X_INTRODUCED_51_); +constraint int_eq_reif(X_INTRODUCED_35_,5,X_INTRODUCED_52_):: defines_var(X_INTRODUCED_52_); +constraint int_eq_reif(X_INTRODUCED_37_,7,X_INTRODUCED_54_):: defines_var(X_INTRODUCED_54_); +constraint int_eq_reif(X_INTRODUCED_39_,9,X_INTRODUCED_56_):: defines_var(X_INTRODUCED_56_); +constraint int_eq_reif(X_INTRODUCED_41_,11,X_INTRODUCED_58_):: defines_var(X_INTRODUCED_58_); +constraint int_eq_reif(X_INTRODUCED_44_,14,X_INTRODUCED_61_):: defines_var(X_INTRODUCED_61_); +constraint int_eq_reif(X_INTRODUCED_45_,15,X_INTRODUCED_62_):: defines_var(X_INTRODUCED_62_); +constraint int_eq_reif(X_INTRODUCED_7_,2,X_INTRODUCED_83_):: defines_var(X_INTRODUCED_83_); +constraint int_ne_reif(X_INTRODUCED_32_,2,X_INTRODUCED_84_):: defines_var(X_INTRODUCED_84_); +constraint int_eq_reif(X_INTRODUCED_7_,3,X_INTRODUCED_86_):: defines_var(X_INTRODUCED_86_); +constraint int_ne_reif(X_INTRODUCED_33_,3,X_INTRODUCED_87_):: defines_var(X_INTRODUCED_87_); +constraint int_eq_reif(X_INTRODUCED_7_,4,X_INTRODUCED_89_):: defines_var(X_INTRODUCED_89_); +constraint int_ne_reif(X_INTRODUCED_34_,4,X_INTRODUCED_90_):: defines_var(X_INTRODUCED_90_); +constraint int_eq_reif(X_INTRODUCED_7_,5,X_INTRODUCED_92_):: defines_var(X_INTRODUCED_92_); +constraint int_ne_reif(X_INTRODUCED_35_,5,X_INTRODUCED_93_):: defines_var(X_INTRODUCED_93_); +constraint int_eq_reif(X_INTRODUCED_7_,7,X_INTRODUCED_98_):: defines_var(X_INTRODUCED_98_); +constraint int_ne_reif(X_INTRODUCED_37_,7,X_INTRODUCED_99_):: defines_var(X_INTRODUCED_99_); +constraint int_eq_reif(X_INTRODUCED_7_,9,X_INTRODUCED_104_):: defines_var(X_INTRODUCED_104_); +constraint int_ne_reif(X_INTRODUCED_39_,9,X_INTRODUCED_105_):: defines_var(X_INTRODUCED_105_); +constraint int_eq_reif(X_INTRODUCED_7_,11,X_INTRODUCED_110_):: defines_var(X_INTRODUCED_110_); +constraint int_ne_reif(X_INTRODUCED_41_,11,X_INTRODUCED_111_):: defines_var(X_INTRODUCED_111_); +constraint int_eq_reif(X_INTRODUCED_7_,14,X_INTRODUCED_119_):: defines_var(X_INTRODUCED_119_); +constraint int_ne_reif(X_INTRODUCED_44_,14,X_INTRODUCED_120_):: defines_var(X_INTRODUCED_120_); +constraint int_eq_reif(X_INTRODUCED_7_,15,X_INTRODUCED_122_):: defines_var(X_INTRODUCED_122_); +constraint int_ne_reif(X_INTRODUCED_45_,15,X_INTRODUCED_123_):: defines_var(X_INTRODUCED_123_); +constraint int_lin_eq_imp(X_INTRODUCED_140_,[X_INTRODUCED_15_,X_INTRODUCED_142_],1,X_INTRODUCED_144_):: defines_var(X_INTRODUCED_144_); +constraint int_lin_eq_imp(X_INTRODUCED_140_,[X_INTRODUCED_16_,X_INTRODUCED_145_],1,X_INTRODUCED_147_):: defines_var(X_INTRODUCED_147_); +constraint int_lin_eq_imp(X_INTRODUCED_140_,[X_INTRODUCED_17_,X_INTRODUCED_148_],1,X_INTRODUCED_150_):: defines_var(X_INTRODUCED_150_); +constraint int_lin_eq_imp(X_INTRODUCED_140_,[X_INTRODUCED_18_,X_INTRODUCED_151_],1,X_INTRODUCED_153_):: defines_var(X_INTRODUCED_153_); +constraint int_lin_eq_imp(X_INTRODUCED_140_,[X_INTRODUCED_20_,X_INTRODUCED_157_],1,X_INTRODUCED_159_):: defines_var(X_INTRODUCED_159_); +constraint int_lin_eq_imp(X_INTRODUCED_140_,[X_INTRODUCED_22_,X_INTRODUCED_163_],1,X_INTRODUCED_165_):: defines_var(X_INTRODUCED_165_); +constraint int_lin_eq_imp(X_INTRODUCED_140_,[X_INTRODUCED_24_,X_INTRODUCED_169_],1,X_INTRODUCED_171_):: defines_var(X_INTRODUCED_171_); +constraint int_lin_eq_imp(X_INTRODUCED_140_,[X_INTRODUCED_27_,X_INTRODUCED_178_],1,X_INTRODUCED_180_):: defines_var(X_INTRODUCED_180_); +constraint int_lin_eq_imp(X_INTRODUCED_140_,[X_INTRODUCED_28_,X_INTRODUCED_181_],1,X_INTRODUCED_183_):: defines_var(X_INTRODUCED_183_); +constraint int_eq_imp(X_INTRODUCED_32_,3,X_INTRODUCED_187_):: defines_var(X_INTRODUCED_187_); +constraint int_eq_imp(X_INTRODUCED_33_,2,X_INTRODUCED_188_):: defines_var(X_INTRODUCED_188_); +constraint int_eq_imp(X_INTRODUCED_33_,4,X_INTRODUCED_189_):: defines_var(X_INTRODUCED_189_); +constraint int_eq_imp(X_INTRODUCED_33_,7,X_INTRODUCED_190_):: defines_var(X_INTRODUCED_190_); +constraint int_eq_imp(X_INTRODUCED_34_,3,X_INTRODUCED_192_):: defines_var(X_INTRODUCED_192_); +constraint int_eq_imp(X_INTRODUCED_35_,9,X_INTRODUCED_193_):: defines_var(X_INTRODUCED_193_); +constraint int_eq_imp(X_INTRODUCED_37_,3,X_INTRODUCED_194_):: defines_var(X_INTRODUCED_194_); +constraint int_eq_imp(X_INTRODUCED_37_,11,X_INTRODUCED_195_):: defines_var(X_INTRODUCED_195_); +constraint int_eq_imp(X_INTRODUCED_39_,5,X_INTRODUCED_197_):: defines_var(X_INTRODUCED_197_); +constraint int_eq_imp(X_INTRODUCED_41_,7,X_INTRODUCED_198_):: defines_var(X_INTRODUCED_198_); +constraint int_eq_imp(X_INTRODUCED_41_,15,X_INTRODUCED_199_):: defines_var(X_INTRODUCED_199_); +constraint int_eq_imp(X_INTRODUCED_44_,15,X_INTRODUCED_201_):: defines_var(X_INTRODUCED_201_); +constraint int_eq_imp(X_INTRODUCED_45_,14,X_INTRODUCED_202_):: defines_var(X_INTRODUCED_202_); +constraint int_eq_imp(X_INTRODUCED_45_,11,X_INTRODUCED_203_):: defines_var(X_INTRODUCED_203_); +solve satisfy; diff --git a/pumpkin-solver/tests/mzn_infeasible/connected.template b/pumpkin-solver/tests/mzn_infeasible/connected.template new file mode 100644 index 000000000..214110184 --- /dev/null +++ b/pumpkin-solver/tests/mzn_infeasible/connected.template @@ -0,0 +1,21 @@ +% https://github.com/ConSol-Lab/Pumpkin/issues/321 +int: n = 4; + +array [1..n,1..n] of var bool: node_active = [| +false, true, true, false| +true, false, false, true| +true, true, true, true| +true, false, false, false |]; + +% check if you can reach every active node from active node +include "connected.mzn"; +constraint connected( + [x + (y-1)*n | x in 1..n-1, y in 1..n] ++ [x + (y-1)*n | x in 1..n, y in 1..n-1], + [x + (y-1)*n | x in 2..n, y in 1..n] ++ [x + (y-1)*n | x in 1..n, y in 2..n], + [node_active[x, y] | y in 1..n, x in 1..n], + % an edge is in the subgraph if from and to are active + [(node_active[x, y]) /\ (node_active[x + 1, y]) | x in 1..n-1, y in 1..n] + ++ [(node_active[x, y]) /\ (node_active[x, y + 1]) | x in 1..n, y in 1..n-1], +); + +solve satisfy; diff --git a/pumpkin-solver/tests/mzn_infeasible_test.rs b/pumpkin-solver/tests/mzn_infeasible_test.rs index fde11265a..231710b38 100644 --- a/pumpkin-solver/tests/mzn_infeasible_test.rs +++ b/pumpkin-solver/tests/mzn_infeasible_test.rs @@ -14,6 +14,7 @@ macro_rules! mzn_infeasible_test { }; } mzn_infeasible_test!(prop_stress); +mzn_infeasible_test!(connected); pub fn run_mzn_infeasible_test(instance_name: &str, folder_name: &str) { let _ = run_mzn_test::(instance_name, folder_name, TestType::Unsatisfiable);