Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

MiniZinc::simplify_bool_constraint(): Assertion 'nonfixed >= 0' failed. #843

Open
LebedevRI opened this issue Sep 4, 2024 · 1 comment

Comments

@LebedevRI
Copy link

Probably not fully reduced:

int: NUM_GRAPH_NODES = 7; % par
int: NUM_GRAPH_EDGES = length(j,i in GRAPH_NODES where i > j)(1); % par

enum GRAPH_NODES = GN(1..NUM_GRAPH_NODES);
enum GRAPH_EDGES = GE(1..NUM_GRAPH_EDGES);
enum DISJOINT_SUBGRAPH_INDICES = DG(1..NUM_GRAPH_NODES);
enum DISJOINT_SUBGRAPH_NODES = DGn(GRAPH_NODES);
enum DISJOINT_SUBGRAPH_EDGE_INDICES = DGe(DISJOINT_SUBGRAPH_INDICES);

array[GRAPH_EDGES] of GRAPH_NODES: GRAPH_LEAVING_NODE  = [ j | j,i in GRAPH_NODES where i > j ];
array[GRAPH_EDGES] of GRAPH_NODES: GRAPH_ENTERING_NODE = [ i | j,i in GRAPH_NODES where i > j ];

array[GRAPH_NODES] of var bool: GraphNodes; % par
array[GRAPH_EDGES] of var bool: GraphEdges; % par
array[GRAPH_EDGES] of DISJOINT_SUBGRAPH_NODES: DISJOINT_SUBGRAPH_LEAVING_NODE = [DGn(GRAPH_LEAVING_NODE[e]) | e in GRAPH_EDGES];
array[GRAPH_EDGES] of DISJOINT_SUBGRAPH_NODES: DISJOINT_SUBGRAPH_ENTERING_NODE = [DGn(GRAPH_ENTERING_NODE[e]) | e in GRAPH_EDGES];
array[GRAPH_NODES] of var DISJOINT_SUBGRAPH_INDICES: NodeDisjointSubgraphIndex;
array[DISJOINT_SUBGRAPH_NODES] of var bool: NodeRootnessMask;
array[GRAPH_NODES] of var GRAPH_NODES: parent; 
array[GRAPH_NODES,GRAPH_NODES] of var bool: HardWires;

constraint forall (j,i in GRAPH_NODES)(
  let {
    GRAPH_NODES: m = min(i,j);
    GRAPH_NODES: M = max(i,j);
  } in
   HardWires[m,M] == ((m,M) == (1,2) \/ (m,M) == (2,3) \/ (m,M) == (2,7) \/ (m,M) == (4,5))
);

constraint forall (n in GRAPH_NODES)(
  GraphNodes[n] == exists(HardWires[n,..])
);
constraint forall (e in GRAPH_EDGES)(
  GraphEdges[e] == HardWires[GRAPH_LEAVING_NODE[e],GRAPH_ENTERING_NODE[e]]
);
constraint forall(n in GRAPH_NODES)(
  parent[n] != n -> exists(e in index_set(GRAPH_LEAVING_NODE) where GRAPH_ENTERING_NODE[e] = n)(GraphEdges[e] /\ GRAPH_LEAVING_NODE[e] = parent[n])
);

$ minizinc --version
MiniZinc to FlatZinc converter, version 2.8.5

@LebedevRI
Copy link
Author

(I think this is new in 2.8.5, never seen that with .4)

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

No branches or pull requests

1 participant