feat(pumpkin-proof-processor): Introduce the proof processor in the main branch

Cargo.toml

@@ -9,6 +9,7 @@ members = [
 
     "./pumpkin-crates/*", # Core libraries of the solver
     "./pumpkin-solver", # The solver binary
+    "./pumpkin-proof-processor", # The proof processor
     "./pumpkin-checker", # The uncertified proof checker
     "./pumpkin-solver-py", # The python interface
     "./pumpkin-macros", # Proc-macros used by the pumpkin source (unpublished)

clippy.toml

@@ -1,4 +1,6 @@
 allowed-duplicate-crates = [
     "hashbrown", 
     "windows-sys",
+    "regex-syntax",
+    "regex-automata",
 ]

minizinc/lib-for-proofs/README.md

@@ -0,0 +1,3 @@
+A MiniZinc library that converts all constraints to linear constraints, except `cumulative`.
+
+Based on the `linear` solver shipped with MiniZinc for MIP solvers.

minizinc/lib-for-proofs/domain_encodings.mzn

@@ -0,0 +1,109 @@
+/*%-----------------------------------------------------------------------------%
+% Domain encodings
+%-----------------------------------------------------------------------------%
+*/
+% Linear equality encoding
+
+% Single variable:  x = d  <->  x_eq_d[d]
+predicate equality_encoding(var int: x, array [int] of var int: x_eq_d) =
+  x in index_set(x_eq_d) /\
+    sum (d in dom(x)) (x_eq_d[d]) = 1 /\
+    sum (d in dom(x)) (d * x_eq_d[d]) = x /\
+    %    my_trace( "eq_enc: \(x), index_set(pp)=" ++ show(index_set( x_eq_d )) ++ "\n" ) /\
+    if fPostprocessDomains then equality_encoding__POST(x, x_eq_d) else true endif;
+
+% Two variables:  x = d /\ y = e  <->  x_eq_d[d] /\ y_eq_e[e] /\ xy_eq_de[d, e]
+predicate equality_encoding(
+  var int: x,
+  var int: y,
+  array [int] of var int: x_eq_d,
+  array [int] of var int: y_eq_e,
+  array [int, int] of var int: xy_eq_de,
+) =
+  x in index_set(x_eq_d) /\
+    y in index_set(y_eq_e) /\
+    index_set(x_eq_d) == index_set_1of2(xy_eq_de) /\
+    index_set(y_eq_e) == index_set_2of2(xy_eq_de) /\
+    sum (d in dom(x), e in dom(y)) (xy_eq_de[d, e]) = 1 /\
+    forall (d in dom(x)) (sum (e in dom(y)) (xy_eq_de[d, e]) = x_eq_d[d]) /\
+    forall (e in dom(y)) (sum (d in dom(x)) (xy_eq_de[d, e]) = y_eq_e[e]);
+
+% Array of variables:  x[i] = d  <->  x_eq_d[i,d]
+predicate equality_encoding(array [int] of var int: x, array [int, int] of var int: x_eq_d) =
+  forall (i in index_set(x)) (
+    x[i] in index_set_2of2(x_eq_d) /\
+      sum (d in index_set_2of2(x_eq_d)) (x_eq_d[i, d]) = 1 /\
+      sum (d in index_set_2of2(x_eq_d)) (d * x_eq_d[i, d]) = x[i]
+  );
+
+function var int: eq_new_var(var int: x, int: i) :: promise_total =
+  if i in dom(x) then let { var 0..1: xi } in xi else 0 endif;
+
+function array [int] of var int: eq_encode(var int: x) :: promise_total =
+  let {
+    array [int] of var int: y = array1d(lb(x)..ub(x), [eq_new_var(x, i) | i in lb(x)..ub(x)]);
+    constraint equality_encoding(x, y);
+  } in %    constraint
+  %      if card(dom(x))>0 then
+  %        my_trace("  eq_encode: dom(\(x)) = " ++ show(dom(x)) ++ ",  card( dom(\(x)) ) = " ++ show(card(dom(x))) ++ "\n")
+  %      else true endif;
+  %%   constraint assert(card(dom(x))>1, "  eq_encode: card(dom(\(x))) == " ++ show(card(dom(x))));
+  y;
+
+function array [int] of int: eq_encode(int: x) :: promise_total =
+  array1d(lb(x)..ub(x), [if i = x then 1 else 0 endif | i in lb(x)..ub(x)]);
+
+%%% The same for 2 variables:
+function var int: eq_new_var(var int: x, int: i, var int: y, int: j) :: promise_total =
+  if i in dom(x) /\ j in dom(y) then let { var 0..1: xi } in xi else 0 endif;
+
+function array [int, int] of var int: eq_encode(var int: x, var int: y) :: promise_total =
+  let {
+    array [int] of var int: pX = eq_encode(x);
+    array [int] of var int: pY = eq_encode(y);
+    array [int, int] of var int: pp =
+      array2d(
+        index_set(pX),
+        index_set(pY),
+        [eq_new_var(x, i, y, j) | i in index_set(pX), j in index_set(pY)],
+      );
+    constraint equality_encoding(x, y, pX, pY, pp);
+  } in pp;
+
+function array [int, int] of int: eq_encode(int: x, int: y) :: promise_total =
+  %  let {
+  %    constraint       if card(dom(x))*card(dom(y))>200 then
+  %      my_trace("  eq_encode: dom(\(x)) = " ++ show(dom(x)) ++ ", dom(\(y)) = " ++ show(dom(y)) ++ "\n")
+  %      else true endif;
+  %  } in
+  array2d(
+    lb(x)..ub(x),
+    lb(y)..ub(y),
+    [if i == x /\ j == y then 1 else 0 endif | i in lb(x)..ub(x), j in lb(y)..ub(y)],
+  );
+
+function array [int, int] of var int: eq_encode(array [int] of var int: x) :: promise_total =
+  let {
+    array [index_set(x), lb_array(x)..ub_array(x)] of var int: y =
+      array2d(
+        index_set(x),
+        lb_array(x)..ub_array(x),
+        [
+          let {
+            array [int] of var int: xi = eq_encode(x[i]);
+          } in if j in index_set(xi) then xi[j] else 0 endif |
+            i in index_set(x),
+            j in lb_array(x)..ub_array(x),
+        ],
+      );
+  } in y;
+
+function array [int, int] of int: eq_encode(array [int] of int: x) :: promise_total =
+  array2d(
+    index_set(x),
+    lb_array(x)..ub_array(x),
+    [if j = x[i] then 1 else 0 endif | i in index_set(x), j in lb_array(x)..ub_array(x)],
+  );
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%

minizinc/lib-for-proofs/fzn_all_different_int.mzn

@@ -0,0 +1,23 @@
+%-----------------------------------------------------------------------------%
+% 'all_different' constrains an array of objects to be all different.
+%
+% Linear version: equality encoding; see e.g. [Refalo, CP 2000]
+%
+% For a given d in dom(x), at most one i with x_i = d can exist.
+%-----------------------------------------------------------------------------%
+
+include "domain_encodings.mzn";
+
+predicate fzn_all_different_int(array [int] of var int: x) =
+  if length(x) <= 1 then
+    true
+  else
+    let {
+      array [int, int] of var 0..1: x_eq_d = eq_encode(x);
+    } in (
+      %        my_trace("  all_different_int: x[" ++ show(index_set(x)) ++ "]\n") /\
+      forall (d in index_set_2of2(x_eq_d)) (sum (i in index_set_1of2(x_eq_d)) (x_eq_d[i, d]) <= 1)
+    )
+  endif;
+
+%-----------------------------------------------------------------------------%

minizinc/lib-for-proofs/fzn_alldifferent_except_0.mzn

@@ -0,0 +1,20 @@
+/**  @group globals.alldifferent
+  Constrain the array of integers \a vs to be all different except those
+  elements that are assigned the value 0.
+*/
+predicate fzn_alldifferent_except_0(array [int] of var int: vs) =
+  %    forall(i, j in index_set(vs) where i < j) (
+  %       (vs[i] != 0 /\ vs[j] != 0) -> vs[i] != vs[j]
+  %    );
+  if length(vs) <= 1 then
+    true
+  else
+    let {
+      array [int, int] of var 0..1: x_eq_d = eq_encode(vs);
+    } in (
+      %        my_trace("  alldifferent_except_0: x[" ++ show(index_set(vs)) ++ "]\n") /\
+      forall (d in index_set_2of2(x_eq_d) diff {0}) (
+        sum (i in index_set_1of2(x_eq_d)) (x_eq_d[i, d]) <= 1
+      )
+    )
+  endif;

minizinc/lib-for-proofs/fzn_circuit.mzn

@@ -0,0 +1,47 @@
+include "alldifferent.mzn";
+
+% Linear version.
+predicate fzn_circuit(array [int] of var int: x) =
+  if length(x) = 0 then
+    true
+  else
+    let {
+      set of int: S = index_set(x);
+      int: l = min(S);
+      int: u = max(S);
+      int: n = card(S);
+      constraint forall (i in S) (x[i] in S diff {i}); %% Self-mapping and exclude i->i before alldifferent
+    } in alldifferent(x) /\
+      %    alldifferent(order) /\
+      if nMZN__fSECcuts > 0 then
+        let {
+          array [int, int] of var int: eq_x = eq_encode(x);
+          constraint assert(l == min(index_set_2of2(eq_x)), "circuit: index set mismatch"); %% self-mapping
+          constraint assert(u == max(index_set_2of2(eq_x)), "circuit: index set mismatch");
+        } in circuit__SECcuts(array1d(eq_x))
+      else
+        true
+      endif /\
+      if nMZN__fSECcuts < 2 then
+        %%% MTZ model. Note that INTEGER order vars seem better!:
+        let {
+          array [l + 1..l + n - 1] of var 2..n: order;
+        } in forall (i, j in l + 1..l + n - 1 where i != j /\ j in dom(x[i])) (
+          order[i] - order[j] + (n - 1) * bool2int(x[i] == j) + (n - 3) * bool2int(x[j] == i) <= %% the Desrochers & Laporte '91 term
+            %%%%  --- strangely enough it is much worse on vrp-s2-v2-c7_vrp-v2-c7_det_ADAPT_1_INVERSE.mzn!
+            n - 2
+        )
+      else
+        true
+      endif /\
+      %% ... but seems improved with this (leaving also for SEC)
+      if n > 2 then
+        forall (i, j in S where i < j) (x[i] != j \/ x[j] != i) %% Only this improves overall with DL'91
+      else
+        true
+      endif
+  endif;
+
+%-----------------------------------------------------------------------------%
+predicate circuit__SECcuts(array [int] of var int: x); %% passed on
+%-----------------------------------------------------------------------------%