1    	/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
2    	/*                                                                           */
3    	/*                  This file is part of the program and library             */
4    	/*         SCIP --- Solving Constraint Integer Programs                      */
5    	/*                                                                           */
6    	/*  Copyright (c) 2002-2023 Zuse Institute Berlin (ZIB)                      */
7    	/*                                                                           */
8    	/*  Licensed under the Apache License, Version 2.0 (the "License");          */
9    	/*  you may not use this file except in compliance with the License.         */
10   	/*  You may obtain a copy of the License at                                  */
11   	/*                                                                           */
12   	/*      http://www.apache.org/licenses/LICENSE-2.0                           */
13   	/*                                                                           */
14   	/*  Unless required by applicable law or agreed to in writing, software      */
15   	/*  distributed under the License is distributed on an "AS IS" BASIS,        */
16   	/*  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. */
17   	/*  See the License for the specific language governing permissions and      */
18   	/*  limitations under the License.                                           */
19   	/*                                                                           */
20   	/*  You should have received a copy of the Apache-2.0 license                */
21   	/*  along with SCIP; see the file LICENSE. If not visit scipopt.org.         */
22   	/*                                                                           */
23   	/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
24   	
25   	/**@file   symmetry_lexred.c
26   	 * @ingroup OTHER_CFILES
27   	 * @brief  methods for handling symmetries by dynamic lexicographic ordering reduction
28   	 * @author Jasper van Doornmalen
29   	 *
30   	 * This implements lexicographic reduction, which generalizes symresack propagation to work for non-binary variable
31   	 * domains, and is dynamified. Whereas static lexicographic reduction propagates that a vector \f$x\f$ is
32   	 * lexicographically larger than its permuted counterpart (i.e., \f$x \succeq \gamma(x)\f$ with \f$\succeq\f$ being
33   	 * standard elementwise lexicographic comparison), the dynamic variant determines the variable vector ordering
34   	 * dynamically. Just as in orbital reduction (cf. symmetry_orbital.c), the variable order is chosen as the variables
35   	 * branched on from the root node to the focus node.
36   	 * Thus, in node \f$\beta\f$, we propagate \f$\sigma_\beta(x) \succeq \sigma_\beta(\gamma(x))\f$,
37   	 * where \f$\sigma_\beta(\cdot)\f$ permutes and restricts the variable vector such that it corresponds to the branched
38   	 * variables in the order from the rooted path to \f$\beta\f$.
39   	 *
40   	 * See Section 4.1 and Example 11 in [vD,H]:@n
41   	 * J. van Doornmalen, C. Hojny, "A Unified Framework for Symmetry Handling", preprint, 2023,
42   	 * https://doi.org/10.48550/arXiv.2211.01295.
43   	 *
44   	 * For dynamic lexicographic reduction, it is crucial that the vectors \f$\sigma_\beta(x)\f$ are the branching
45   	 * variables up to node \f$\beta\f$ in the given order. Since SCIP can change the tree structure during solving
46   	 * (re-writing history), we store the original branching decisions at the moment they are made. See event_shadowtree.c .
47   	 */
48   	
49   	/*---+----1----+----2----+----3----+----4----+----5----+----6----+----7----+----8----+----9----+----0----+----1----+----2*/
50   	
51   	#include "blockmemshell/memory.h"
52   	#include "scip/symmetry_lexred.h"
53   	#include "scip/pub_cons.h"
54   	#include "scip/pub_message.h"
55   	#include "scip/pub_var.h"
56   	#include "scip/struct_var.h"
57   	#include "scip/type_var.h"
58   	#include "scip/scip.h"
59   	#include "scip/scip_branch.h"
60   	#include "scip/scip_conflict.h"
61   	#include "scip/scip_cons.h"
62   	#include "scip/scip_copy.h"
63   	#include "scip/scip_cut.h"
64   	#include "scip/scip_general.h"
65   	#include "scip/scip_lp.h"
66   	#include "scip/scip_mem.h"
67   	#include "scip/scip_message.h"
68   	#include "scip/scip_numerics.h"
69   	#include "scip/scip_param.h"
70   	#include "scip/scip_prob.h"
71   	#include "scip/scip_probing.h"
72   	#include "scip/scip_sol.h"
73   	#include "scip/scip_var.h"
74   	#include "scip/debug.h"
75   	#include "scip/struct_scip.h"
76   	#include "scip/struct_mem.h"
77   	#include "scip/struct_tree.h"
78   	#include "scip/symmetry.h"
79   	#include "scip/event_shadowtree.h"
80   	#include <string.h>
81   	
82   	
83   	/*
84   	 * Data structures
85   	 */
86   	
87   	
88   	/** data per permutation for lexicographic reduction propagator */
89   	struct LexRedPermData
90   	{
91   	   SCIP_Bool             isdynamic;          /**< whether permutation shall be propagated with dynamic variable order */
92   	   SCIP_VAR**            vars;               /**< variables affected by permutation */
93   	   int                   nvars;              /**< number of variables */
94   	   int*                  perm;               /**< permutation for lexicographic reduction */
95   	   int*                  invperm;            /**< inverse permutation */
96   	   SCIP_HASHMAP*         varmap;             /**< map of variables to indices in vars array */
97   	   SYM_SYMTYPE           symtype;            /**< type of symmetries in perm */
98   	   SCIP_Real*            vardomaincenter;    /**< array of centers of variable domains */
99   	};
100  	typedef struct LexRedPermData LEXDATA;
101  	
102  	
103  	/** data for dynamic lexicographic reduction propagator */
104  	struct SCIP_LexRedData
105  	{
106  	   SCIP_EVENTHDLR*       shadowtreeeventhdlr;/**< eventhandler for the shadow tree data structure */
107  	   SCIP_HASHMAP*         symvarmap;          /**< map of variables affected by some permutation handled by a LEXDATA */
108  	   int                   nsymvars;           /**< number of variables in symvarmap */
109  	   LEXDATA**             lexdatas;           /**< array of pointers to individual LEXDATA's */
110  	   int                   nlexdatas;          /**< number of datas in array */
111  	   int                   maxnlexdatas;       /**< allocated datas array size */
112  	   int                   nred;               /**< total number of reductions */
113  	   int                   ncutoff;            /**< total number of cutoffs */
114  	   SCIP_Bool             hasdynamicperm;     /**< whether there exists a permutation that is treated dynamically */
115  	   SCIP_Bool             treewarninggiven;   /**< whether a warning is given for missing nodes in shadowtree */
116  	};
117  	
118  	
119  	/** to store branch-and-bound tree paths, (depth, index)-information per variable in rooted path */
120  	struct NodeDepthBranchIndex
121  	{
122  	   int                   nodedepth;          /**< depth of var domain change */
123  	   int                   index;              /**< index of var domain change on node at depth */
124  	};
125  	typedef struct NodeDepthBranchIndex NODEDEPTHBRANCHINDEX;
126  	
127  	
128  	/** auxiliary struct to pass branch-and-bound tree information to sort function */
129  	struct VarArrayNodeDepthBranchIndex
130  	{
131  	   NODEDEPTHBRANCHINDEX* nodedepthbranchindices; /**< pointer to branch-and-bound tree information */
132  	   SCIP_LEXREDDATA*      masterdata;             /**< pointer to global data for lexicographic reduction propagator */
133  	   SCIP_VAR**            vars;                   /**< pointer to variable array */
134  	};
135  	typedef struct VarArrayNodeDepthBranchIndex VARARRAYNODEDEPTHBRANCHINDEX;
136  	
137  	
138  	/*
139  	 * Local methods
140  	 */
141  	
142  	/** frees dynamic lexicographic reduction propagator data */
143  	static
144  	SCIP_RETCODE lexdataFree(
145  	   SCIP*                 scip,               /**< SCIP data structure */
146  	   LEXDATA**             lexdata             /**< pointer to individual lexicographic reduction propagator datas */
147  	   )
148  	{
149  	   SCIP_Bool issigned;
150  	   int permlen;
151  	   int i;
152  	
153  	   assert( scip != NULL );
154  	   assert( lexdata != NULL );
155  	   assert( (*lexdata) != NULL );
156  	
157  	   if ( (*lexdata)->symtype == SYM_SYMTYPE_SIGNPERM )
158  	   {
159  	      issigned = TRUE;
160  	      permlen = 2 * (*lexdata)->nvars;
161  	   }
162  	   else
163  	   {
164  	      issigned = FALSE;
165  	      permlen = (*lexdata)->nvars;
166  	   }
167  	
168  	   if ( (*lexdata)->nvars > 0 )
169  	   {
170  	      assert( (*lexdata)->invperm != NULL );
171  	      assert( (*lexdata)->perm != NULL );
172  	      assert( (*lexdata)->vars != NULL );
173  	
174  	      /* free hashmap */
175  	      if ( (*lexdata)->isdynamic )
176  	      {
177  	         assert( (*lexdata)->varmap != NULL );
178  	         SCIPhashmapFree(&((*lexdata)->varmap));
179  	      }
180  	
181  	      /* release variables */
182  	      for (i = 0; i < (*lexdata)->nvars; ++i)
183  	      {
184  	         SCIP_CALL( SCIPreleaseVar(scip, &(*lexdata)->vars[i]) );
185  	      }
186  	
187  	      SCIPfreeBlockMemoryArray(scip, &(*lexdata)->invperm, permlen);
188  	      SCIPfreeBlockMemoryArray(scip, &(*lexdata)->perm, permlen);
189  	      SCIPfreeBlockMemoryArray(scip, &(*lexdata)->vars, (*lexdata)->nvars);
190  	
191  	      if ( issigned )
192  	      {
193  	         SCIPfreeBlockMemoryArray(scip, &(*lexdata)->vardomaincenter, (*lexdata)->nvars);
194  	      }
195  	      else
196  	      {
197  	         assert( (*lexdata)->vardomaincenter == NULL );
198  	      }
199  	   }
200  	#ifndef NDEBUG
201  	   else
202  	   {
203  	      assert( (*lexdata)->nvars == 0 );
204  	      assert( (*lexdata)->invperm == NULL );
205  	      assert( (*lexdata)->vardomaincenter == NULL );
206  	      assert( (*lexdata)->perm == NULL );
207  	      assert( (*lexdata)->vars == NULL );
208  	      assert( (*lexdata)->varmap == NULL );
209  	   }
210  	#endif
211  	   SCIPfreeBlockMemory(scip, lexdata);
212  	
213  	   return SCIP_OKAY;
214  	}
215  	
216  	
217  	/** creates dynamic lexicographic reduction propagator data
218  	 *
219  	 *  Fixed points are removed.
220  	 */
221  	static
222  	SCIP_RETCODE lexdataCreate(
223  	   SCIP*                 scip,               /**< SCIP data structure */
224  	   SCIP_LEXREDDATA*      masterdata,         /**< pointer to global data for lexicographic reduction propagator */
225  	   LEXDATA**             lexdata,            /**< pointer to store data for permutation to be added */
226  	   SCIP_VAR*const*       vars,               /**< input variables of the lexicographic reduction propagator */
227  	   int                   nvars,              /**< input number of variables of the lexicographic reduction propagator */
228  	   int*                  perm,               /**< input permutation of the lexicographic reduction propagator */
229  	   SYM_SYMTYPE           symtype,            /**< type of symmetries in perm */
230  	   SCIP_Real*            permvardomaincenter, /**< array containing center point for each variable domain */
231  	   SCIP_Bool             usedynamicorder,    /**< whether a dynamic variable order shall be used */
232  	   SCIP_Bool*            success             /**< to store whether the component is successfully added */
233  	   )
234  	{
235  	   SCIP_VAR* var;
236  	   SCIP_Bool issignedperm;
237  	   int* indexcorrection;
238  	   int naffectedvariables;
239  	   int permlen;
240  	   int i;
241  	   int j;
242  	
243  	   assert( scip != NULL );
244  	   assert( masterdata != NULL );
245  	   assert( lexdata != NULL );
246  	   assert( vars != NULL );
247  	   assert( nvars >= 0 );
248  	   assert( perm != NULL );
249  	   assert( symtype == SYM_SYMTYPE_PERM || permvardomaincenter != NULL );
250  	   assert( success != NULL );
251  	   assert( SCIPisTransformed(scip) );
252  	   assert( masterdata->shadowtreeeventhdlr != NULL );
253  	
254  	   *success = TRUE;
255  	   issignedperm = symtype == SYM_SYMTYPE_PERM ? FALSE : TRUE;
256  	
257  	   /* initialize the data structures */
258  	   SCIP_CALL( SCIPallocBlockMemory(scip, lexdata) );
259  	   (*lexdata)->symtype = symtype;
260  	
261  	   (*lexdata)->isdynamic = usedynamicorder;
262  	
263  	   /* remove fixed points */
264  	   naffectedvariables = 0;
265  	   SCIP_CALL( SCIPallocBufferArray(scip, &indexcorrection, nvars) );
266  	   for (i = 0; i < nvars; ++i)
267  	   {
268  	      if ( perm[i] == i )
269  	         indexcorrection[i] = -1; /* fixed points get an entry < 0 in the indexcorrection array */
270  	      else
271  	         indexcorrection[i] = naffectedvariables++;
272  	   }
273  	
274  	   /* do nothing if reductions would be trivial */
275  	   if ( naffectedvariables <= 0 )
276  	   {
277  	      assert( naffectedvariables == 0 );
278  	      SCIPfreeBufferArray(scip, &indexcorrection);
279  	
280  	      *success = FALSE;
281  	      SCIPfreeBlockMemory(scip, lexdata);
282  	      return SCIP_OKAY;
283  	   }
284  	
285  	   /* require that the shadowtree is active if dynamic propagation is used */
286  	   if ( usedynamicorder )
287  	   {
288  	      masterdata->hasdynamicperm = TRUE;
289  	
290  	      SCIP_CALL( SCIPactivateShadowTree(scip, masterdata->shadowtreeeventhdlr) );
291  	   }
292  	
293  	   /* initialize variable arrays */
294  	   (*lexdata)->nvars = naffectedvariables;
295  	   permlen = issignedperm ? 2 * (*lexdata)->nvars : (*lexdata)->nvars;
296  	
297  	   SCIP_CALL( SCIPallocBlockMemoryArray(scip, &(*lexdata)->vars, (*lexdata)->nvars) );
298  	   SCIP_CALL( SCIPallocBlockMemoryArray(scip, &(*lexdata)->perm, permlen) );
299  	   SCIP_CALL( SCIPallocBlockMemoryArray(scip, &(*lexdata)->invperm, permlen) );
300  	   if ( issignedperm )
301  	   {
302  	      SCIP_CALL( SCIPallocBlockMemoryArray(scip, &(*lexdata)->vardomaincenter, (*lexdata)->nvars) );
303  	   }
304  	   else
305  	      (*lexdata)->vardomaincenter = NULL;
306  	
307  	   /* determine the vars, perm, and centers */
308  	   for (j = 0; j < nvars; ++j)
309  	   {
310  	      i = indexcorrection[j];
311  	      if ( i < 0 )
312  	         continue;
313  	
314  	      /* j is the original index, i is the relabeled index */
315  	      (*lexdata)->vars[i] = vars[j];
316  	
317  	      if ( issignedperm )
318  	      {
319  	         if ( perm[j] >= nvars )
320  	         {
321  	            (*lexdata)->perm[i] = indexcorrection[perm[j] - nvars] + (*lexdata)->nvars;
322  	            (*lexdata)->perm[i + (*lexdata)->nvars] = indexcorrection[perm[j] - nvars];
323  	            assert( (*lexdata)->nvars <= (*lexdata)->perm[i] && (*lexdata)->perm[i] < 2 * (*lexdata)->nvars );
324  	         }
325  	         else
326  	         {
327  	            (*lexdata)->perm[i] = indexcorrection[perm[j]];
328  	            (*lexdata)->perm[i + (*lexdata)->nvars] = indexcorrection[perm[j]] + (*lexdata)->nvars;
329  	         }
330  	      }
331  	      else
332  	         (*lexdata)->perm[i] = indexcorrection[perm[j]];
333  	
334  	      if ( issignedperm )
335  	         (*lexdata)->vardomaincenter[i] = permvardomaincenter[j];
336  	
337  	      assert( perm[j] != j );
338  	      assert( (*lexdata)->perm[i] != i );
339  	      assert( (*lexdata)->perm[i] >= 0 );
340  	      assert( (*lexdata)->perm[i] < permlen );
341  	   }
342  	
343  	   /* determine invperm */
344  	   for (i = 0; i < (*lexdata)->nvars; ++i)
345  	   {
346  	      if ( (*lexdata)->perm[i] >= (*lexdata)->nvars )
347  	      {
348  	         assert( issignedperm );
349  	
350  	         (*lexdata)->invperm[(*lexdata)->perm[i]] = i;
351  	         (*lexdata)->invperm[(*lexdata)->perm[i] - (*lexdata)->nvars] = i + (*lexdata)->nvars;
352  	      }
353  	      else
354  	      {
355  	         (*lexdata)->invperm[(*lexdata)->perm[i]] = i;
356  	
357  	         if ( issignedperm )
358  	            (*lexdata)->invperm[(*lexdata)->perm[i] + (*lexdata)->nvars] = i + (*lexdata)->nvars;
359  	      }
360  	   }
361  	   SCIPfreeBufferArray(scip, &indexcorrection);
362  	
363  	   /* make sure that we deal with transformed variables and that variables cannot be multi-aggregated, and capture */
364  	   for (i = 0; i < (*lexdata)->nvars; ++i)
365  	   {
366  	      assert( SCIPvarIsTransformed((*lexdata)->vars[i]) );
367  	      SCIP_CALL( SCIPmarkDoNotMultaggrVar(scip, (*lexdata)->vars[i]) );
368  	      SCIP_CALL( SCIPcaptureVar(scip, (*lexdata)->vars[i]) );
369  	   }
370  	
371  	   /* create hashmap for all variables, both globally and just for this lexdata */
372  	   assert( (masterdata->symvarmap == NULL) == (masterdata->nsymvars == 0) );
373  	   if ( usedynamicorder )
374  	   {
375  	      if ( masterdata->symvarmap == NULL )
376  	      {
377  	         SCIP_CALL( SCIPhashmapCreate(&masterdata->symvarmap, SCIPblkmem(scip), (*lexdata)->nvars) );
378  	      }
379  	      assert( masterdata->symvarmap != NULL );
380  	
381  	      SCIP_CALL( SCIPhashmapCreate(&(*lexdata)->varmap, SCIPblkmem(scip), (*lexdata)->nvars) );
382  	      assert( (*lexdata)->varmap != NULL );
383  	
384  	      for (i = 0; i < (*lexdata)->nvars; ++i)
385  	      {
386  	         var = (*lexdata)->vars[i];
387  	         assert( var != NULL );
388  	         assert( SCIPvarIsTransformed(var) );
389  	
390  	         /* the hashmap in lexdata maps to the index in the vars array */
391  	         SCIP_CALL( SCIPhashmapInsertInt((*lexdata)->varmap, (void*) var, i) );
392  	
393  	         /* var already added to hashmap */
394  	         if ( SCIPhashmapExists(masterdata->symvarmap, (void*) var) )
395  	            continue;
396  	
397  	         /* the hashmap in symvarmap maps to a unique index */
398  	         SCIP_CALL( SCIPhashmapInsertInt(masterdata->symvarmap, (void*) var, masterdata->nsymvars++) );
399  	      }
400  	   }
401  	   else
402  	      (*lexdata)->varmap = NULL;
403  	
404  	   return SCIP_OKAY;
405  	}
406  	
407  	
408  	/** comparator used in the getVarOrder() function, for sorting an array of NODEDEPTHBRANCHINDEX by depth, then by index
409  	 *
410  	 *  @warning this function is only meant to be used in the getVarOrder() function
411  	 *
412  	 *  @pre datapointer is populated with a VARARRAYNODEDEPTHBRANCHINDEX pointer
413  	 *  @pre the comparator is only called on entries with set (depth, index)-information
414  	 *  @pre the (depth, index)-informations are all different
415  	 *
416  	 *  result:
417  	 *    0: the same index is compared, so the (depth, index)-informations are the same
418  	 *   -1: the depth of ind1 is smaller than the depth of ind2, or it's equal and the index is smaller
419  	 *    1: the depth of ind2 is smaller than the depth of ind1, or it's equal and the index is smaller
420  	 */
421  	static
422  	SCIP_DECL_SORTINDCOMP(sortbynodedepthbranchindices)
423  	{
424  	   /* unpack the dataptr */
425  	   VARARRAYNODEDEPTHBRANCHINDEX* vararraynodedepthbranchindices;
426  	   NODEDEPTHBRANCHINDEX* nodedepthbranchindices;
427  	   SCIP_LEXREDDATA* masterdata;
428  	   SCIP_VAR** vars;
429  	   NODEDEPTHBRANCHINDEX* index1;
430  	   NODEDEPTHBRANCHINDEX* index2;
431  	
432  	   vararraynodedepthbranchindices = (VARARRAYNODEDEPTHBRANCHINDEX*) dataptr;
433  	   nodedepthbranchindices = vararraynodedepthbranchindices->nodedepthbranchindices;
434  	   masterdata = vararraynodedepthbranchindices->masterdata;
435  	   vars = vararraynodedepthbranchindices->vars;
436  	
437  	   /* comparing the same element is an identity operation */
438  	   if ( ind1 == ind2 )
439  	      return 0;
440  	
441  	   /* sort by depth, then by index, in increasing order */
442  	   index1 = &(nodedepthbranchindices[SCIPhashmapGetImageInt(masterdata->symvarmap, vars[ind1])]);
443  	   index2 = &(nodedepthbranchindices[SCIPhashmapGetImageInt(masterdata->symvarmap, vars[ind2])]);
444  	
445  	   if ( index1->nodedepth < index2->nodedepth )
446  	      return -1;
447  	   if ( index1->nodedepth > index2->nodedepth )
448  	      return 1;
449  	   assert( index1->index != index2->index );
450  	
451  	   /* depth is the same, sort by index */
452  	   if ( index1->index < index2->index )
453  	      return -1;
454  	   if ( index1->index > index2->index )
455  	      return 1;
456  	
457  	   /* this may not happen, since all elements must be different */
458  	   assert( index1->index == index2->index );
459  	
460  	   return 0;
461  	}
462  	
463  	
464  	/** return the index of a variable at a specific position of a variable order */
465  	static
466  	int varOrderGetIndex(
467  	   int*                  varorder,           /**< variable order (or NULL) */
468  	   int                   pos                 /**< position for which index is returned */
469  	   )
470  	{
471  	   assert( pos >= 0 );
472  	
473  	   if ( varorder == NULL )
474  	      return pos;
475  	   return varorder[pos];
476  	}
477  	
478  	
479  	/** gets the variable ordering based on the branching decisions at the node */
480  	static
481  	SCIP_RETCODE getVarOrder(
482  	   SCIP*                 scip,               /**< SCIP data structure */
483  	   SCIP_LEXREDDATA*      masterdata,         /**< pointer to global data for lexicographic reduction propagator */
484  	   LEXDATA*              lexdata,            /**< pointer to data for this permutation */
485  	   NODEDEPTHBRANCHINDEX* nodedepthbranchindices, /**< array with (depth, index)-information per variable in
486  	                                                  *   rooted path to focus node */
487  	   int                   nvarstotal,         /**< length of that array */
488  	   SCIP_VAR**            branchvars,         /**< array populated with variables branched on in the symvarmap hashset */
489  	   int                   nbranchvars,        /**< number of elements in branchvars array */
490  	   int*                  varorder,           /**< array to populate with variable order */
491  	   int*                  nselvars,           /**< pointer to number of variables in the ordering */
492  	   int                   maxnselvars         /**< maximal size of the number of selected variables */
493  	)
494  	{
495  	   SCIP_VAR** vars;
496  	   int nvars;
497  	   SCIP_VAR* var;
498  	   int varindex;
499  	   int i;
500  	
501  	   assert( scip != NULL );
502  	   assert( masterdata != NULL );
503  	   assert( lexdata != NULL );
504  	   assert( nodedepthbranchindices != NULL );
505  	   assert( nvarstotal >= 0 );
506  	   assert( branchvars != NULL );
507  	   assert( nbranchvars >= 0 );
508  	   assert( varorder != NULL );
509  	   assert( nselvars != NULL );
510  	
511  	   vars = lexdata->vars;
512  	   assert( vars != NULL );
513  	   nvars = lexdata->nvars;
514  	   assert( nvars >= 0 );
515  	
516  	   /* first collect every variable that was branched on */
517  	   *nselvars = 0;
518  	
519  	   if ( nvars < nbranchvars )
520  	   {
521  	      /* for permutations with small support, just check all support entries */
522  	      for (i = 0; i < nvars; ++i)
523  	      {
524  	         var = vars[i];
525  	         assert( var != NULL );
526  	
527  	         assert( SCIPhashmapExists(masterdata->symvarmap, (void*) var) );
528  	         varindex = SCIPhashmapGetImageInt(masterdata->symvarmap, var);
529  	         assert( varindex >= 0 );
530  	         assert( varindex < masterdata->nsymvars );
531  	
532  	         assert( nodedepthbranchindices[varindex].nodedepth >= 0 );
533  	
534  	         /* skip variables that have not been used for branching */
535  	         if ( nodedepthbranchindices[varindex].nodedepth <= 0 )
536  	            continue;
537  	
538  	         /* add index i of branching variable */
539  	         assert( i >= 0 );
540  	         assert( i < nvars );
541  	         assert( (*nselvars) < maxnselvars );
542  	         varorder[(*nselvars)++] = i;
543  	      }
544  	   }
545  	   else
546  	   {
547  	      /* for permutations where the support is larger than the number of branched vars, check for the branched vars */
548  	      for (i = 0; i < nbranchvars; ++i)
549  	      {
550  	         var = branchvars[i];
551  	         assert( var != NULL );
552  	
553  	#ifndef NDEBUG
554  	         /* debugging: test if it is indeed a branched variable! */
555  	         varindex = SCIPhashmapGetImageInt(masterdata->symvarmap, var);
556  	         assert( varindex >= 0 );
557  	         assert( varindex < masterdata->nsymvars );
558  	         assert( nodedepthbranchindices[varindex].nodedepth > 0 );
559  	#endif
560  	
561  	         /* get the variable index in the lexdata->vars array */
562  	         varindex = SCIPhashmapGetImageInt(lexdata->varmap, (void*) var);
563  	         assert( varindex == INT_MAX || (varindex >= 0 && varindex < lexdata->nvars) );
564  	
565  	         /* skip variables that are not permuted by the permutation */
566  	         if ( varindex == INT_MAX )
567  	            continue;
568  	         assert( lexdata->vars[varindex] == var );
569  	
570  	         /* add index varindex of the branching variable */
571  	         varorder[(*nselvars)++] = varindex;
572  	      }
573  	   }
574  	
575  	   if ( *nselvars > 1 )
576  	   {
577  	      /* sort the first n elements of varorder by depth, then by index, as indicated by nodedepthbranchindices. */
578  	      VARARRAYNODEDEPTHBRANCHINDEX vararraynodedepthbranchindices;
579  	      vararraynodedepthbranchindices.nodedepthbranchindices = nodedepthbranchindices;
580  	      vararraynodedepthbranchindices.masterdata = masterdata;
581  	      vararraynodedepthbranchindices.vars = vars;
582  	      SCIPsortInd(varorder, sortbynodedepthbranchindices, (void*) &vararraynodedepthbranchindices, *nselvars);
583  	   }
584  	
585  	   return SCIP_OKAY;
586  	}
587  	
588  	
589  	/** gerts local variable bounds or reads bound from peek data */
590  	static
591  	SCIP_RETCODE getVarBounds(
592  	   SCIP_VAR*             var1,               /**< first variable in comparison */
593  	   SCIP_VAR*             var2,               /**< second variable in comparison */
594  	   SCIP_Bool             peekmode,           /**< whether function is called in peek mode */
595  	   int                   varidx1,            /**< index of var1 (or NULL) */
596  	   int                   varidx2,            /**< index of var2 (or NULL) */
597  	   SCIP_Real*            peeklbs,            /**< lower bounds of variables in peek mode (or NULL) */
598  	   SCIP_Real*            peekubs,            /**< upper bounds of variables in peek mode (or NULL) */
599  	   SCIP_Bool*            peekbdset,          /**< whether peek bounds have been set (or NULL) */
600  	   SCIP_Real*            lb1,                /**< pointer to store lower bound of var1 */
601  	   SCIP_Real*            ub1,                /**< pointer to store upper bound of var1 */
602  	   SCIP_Real*            lb2,                /**< pointer to store lower bound of var2 */
603  	   SCIP_Real*            ub2                 /**< pointer to store upper bound of var2 */
604  	   )
605  	{
606  	   assert( var1 != NULL );
607  	   assert( var2 != NULL );
608  	   assert( (!peekmode) || peeklbs != NULL );
609  	   assert( (!peekmode) || peekubs != NULL );
610  	   assert( (!peekmode) || peekbdset != NULL );
611  	   assert( lb1 != NULL );
612  	   assert( ub1 != NULL );
613  	   assert( lb2 != NULL );
614  	   assert( ub2 != NULL );
615  	
616  	   if ( peekmode && peekbdset[varidx1] )
617  	   {
618  	      *ub1 = peekubs[varidx1];
619  	      *lb1 = peeklbs[varidx1];
620  	   }
621  	   else
622  	   {
623  	      *ub1 = SCIPvarGetUbLocal(var1);
624  	      *lb1 = SCIPvarGetLbLocal(var1);
625  	   }
626  	   if ( peekmode && peekbdset[varidx2] )
627  	   {
628  	      *ub2 = peekubs[varidx2];
629  	      *lb2 = peeklbs[varidx2];
630  	   }
631  	   else
632  	   {
633  	      *ub2 = SCIPvarGetUbLocal(var2);
634  	      *lb2 = SCIPvarGetLbLocal(var2);
635  	   }
636  	
637  	   return SCIP_OKAY;
638  	}
639  	
640  	/** returns whether a shifted variable is always smaller than another shifted variable
641  	 *
642  	 *  Shifts are always (var - shift).
643  	 */
644  	static
645  	SCIP_Bool alwaysLTshiftedVars(
646  	   SCIP*                 scip,               /**< SCIP data structure */
647  	   SCIP_VAR*             var1,               /**< first variable in comparison */
648  	   SCIP_VAR*             var2,               /**< second variable in comparison */
649  	   SCIP_Real             shift1,             /**< shift of var1 */
650  	   SCIP_Real             shift2,             /**< shift of var2 */
651  	   SCIP_Bool             isnegated,          /**< whether shift of var2 is negated */
652  	   SCIP_Bool             peekmode,           /**< whether function is called in peek mode */
653  	   int                   varidx1,            /**< index of var1 (or NULL) */
654  	   int                   varidx2,            /**< index of var2 (or NULL) */
655  	   SCIP_Real*            peeklbs,            /**< lower bounds of variables in peek mode (or NULL) */
656  	   SCIP_Real*            peekubs,            /**< upper bounds of variables in peek mode (or NULL) */
657  	   SCIP_Bool*            peekbdset           /**< whether peek bounds have been set (or NULL) */
658  	   )
659  	{
660  	   SCIP_Real ub1;
661  	   SCIP_Real ub2;
662  	   SCIP_Real lb1;
663  	   SCIP_Real lb2;
664  	
665  	   assert( scip != NULL );
666  	   assert( var1 != NULL );
667  	   assert( var2 != NULL );
668  	   assert( (!peekmode) || peeklbs != NULL );
669  	   assert( (!peekmode) || peekubs != NULL );
670  	   assert( (!peekmode) || peekbdset != NULL );
671  	
672  	   SCIP_CALL_ABORT( getVarBounds(var1, var2, peekmode, varidx1, varidx2, peeklbs, peekubs, peekbdset,
673  	         &lb1, &ub1, &lb2, &ub2) );
674  	
675  	   /* for negated variables, check: var1 - shift1 < shift2 - var2 */
676  	   if ( isnegated && SCIPisLT(scip, ub1, shift1 + shift2 - ub2) )
677  	      return TRUE;
678  	
679  	   /* for non-negated variables, check: var1 - center1 < var2 - center2 */
680  	   if ( (!isnegated) && SCIPisLT(scip, ub1, shift1 - shift2 + lb2) )
681  	      return TRUE;
682  	
683  	   return FALSE;
684  	}
685  	
686  	
687  	/** returns whether a shifted variable can be greater than another shifted variable
688  	 *
689  	 *  Shifts are always (var - shift).
690  	 */
691  	static
692  	SCIP_Bool canGTshiftedVars(
693  	   SCIP*                 scip,               /**< SCIP data structure */
694  	   SCIP_VAR*             var1,               /**< first variable in comparison */
695  	   SCIP_VAR*             var2,               /**< second variable in comparison */
696  	   SCIP_Real             shift1,             /**< shift of var1 */
697  	   SCIP_Real             shift2,             /**< shift of var2 */
698  	   SCIP_Bool             isnegated,          /**< whether shift of var2 is negated */
699  	   SCIP_Bool             peekmode,           /**< whether function is called in peek mode */
700  	   int                   varidx1,            /**< index of var1 (or NULL) */
701  	   int                   varidx2,            /**< index of var2 (or NULL) */
702  	   SCIP_Real*            peeklbs,            /**< lower bounds of variables in peek mode (or NULL) */
703  	   SCIP_Real*            peekubs,            /**< upper bounds of variables in peek mode (or NULL) */
704  	   SCIP_Bool*            peekbdset           /**< whether peek bounds have been set (or NULL) */
705  	   )
706  	{
707  	   SCIP_Real ub1;
708  	   SCIP_Real ub2;
709  	   SCIP_Real lb1;
710  	   SCIP_Real lb2;
711  	
712  	   assert( scip != NULL );
713  	   assert( var1 != NULL );
714  	   assert( var2 != NULL );
715  	   assert( (!peekmode) || peeklbs != NULL );
716  	   assert( (!peekmode) || peekubs != NULL );
717  	   assert( (!peekmode) || peekbdset != NULL );
718  	
719  	   SCIP_CALL_ABORT( getVarBounds(var1, var2, peekmode, varidx1, varidx2, peeklbs, peekubs, peekbdset,
720  	         &lb1, &ub1, &lb2, &ub2) );
721  	
722  	   /* for negated variables, check: var1 - shift1 > shift2 - var2 */
723  	   if ( isnegated && SCIPisGT(scip, ub1, shift1 + shift2 - ub2) )
724  	      return TRUE;
725  	
726  	   /* for non-negated variables, check: var1 - center1 > var2 - center2 */
727  	   if ( (!isnegated) && SCIPisGT(scip, ub1, shift1 - shift2 + lb2) )
728  	      return TRUE;
729  	
730  	   return FALSE;
731  	}
732  	
733  	
734  	/** propagates lower bound of first variable in relation x >= y for shifted variables */
735  	static
736  	SCIP_RETCODE propagateLowerBoundVar(
737  	   SCIP*                 scip,               /**< SCIP data structure */
738  	   SCIP_VAR*             var1,               /**< first variable in pair */
739  	   SCIP_VAR*             var2,               /**< second variable in pair */
740  	   SCIP_Real             center1,            /**< center of var1 (original var domain) */
741  	   SCIP_Real             center2,            /**< center of var2 (original var domain) */
742  	   SCIP_Bool             isnegated,          /**< whether var2 is negated by symmetry */
743  	   SCIP_Bool*            infeasible,         /**< pointer to store whether infeasibility is found */
744  	   int*                  nreductions,        /**< pointer to store number of reductions */
745  	   SCIP_Bool             peekmode,           /**< whether function is called in peek mode */
746  	   int                   varidx1,            /**< index of var1 (or NULL) */
747  	   int                   varidx2,            /**< index of var2 (or NULL) */
748  	   SCIP_Real*            peeklbs,            /**< lower bounds of variables in peek mode (or NULL) */
749  	   SCIP_Real*            peekubs,            /**< upper bounds of variables in peek mode (or NULL) */
750  	   SCIP_Bool*            peekbdset           /**< whether peek bounds have been set (or NULL) */
751  	   )
752  	{
753  	   SCIP_Real ub1;
754  	   SCIP_Real ub2;
755  	   SCIP_Real lb1;
756  	   SCIP_Real lb2;
757  	
758  	   SCIP_Bool tighten = FALSE;
759  	   SCIP_Real newbd;
760  	
761  	   assert( (!peekmode) || peeklbs != NULL );
762  	   assert( (!peekmode) || peekubs != NULL );
763  	   assert( (!peekmode) || peekbdset != NULL );
764  	
765  	   SCIP_CALL( getVarBounds(var1, var2, peekmode, varidx1, varidx2, peeklbs, peekubs, peekbdset,
766  	         &lb1, &ub1, &lb2, &ub2) );
767  	
768  	   /* tighten domain of var1 to ensure that var1 - center1 >= isnegated * (var2 - center2 ) */
769  	   if ( isnegated )
770  	   {
771  	      if ( SCIPisLT(scip, lb1 - center1, center2 - ub2) )
772  	      {
773  	         tighten = TRUE;
774  	         newbd = center1 + center2 - ub2;
775  	      }
776  	   }
777  	   else
778  	   {
779  	      if ( SCIPisLT(scip, lb1 - center1, lb2 - center2) )
780  	      {
781  	         tighten = TRUE;
782  	         newbd = center1 + lb2 - center2;
783  	      }
784  	   }
785  	
786  	   if ( tighten )
787  	   {
788  	      /* in peek mode, only store updated bounds */
789  	      if ( peekmode )
790  	      {
791  	         peeklbs[varidx1] = newbd; /*lint !e644*/
792  	         peekubs[varidx1] = ub1;
793  	         peekbdset[varidx1] = TRUE;
794  	      }
795  	      else
796  	      {
797  	         SCIP_CALL( SCIPtightenVarLb(scip, var1, newbd, TRUE, infeasible, &tighten) );
798  	         if ( tighten )
799  	         {
800  	            SCIPdebugMessage("Restricting variable LB %12s to %5.2f\n", SCIPvarGetName(var1), newbd);
801  	            *nreductions += 1;
802  	         }
803  	         else
804  	         {
805  	            SCIPdebugMessage("Restricting variable LB %12s to %5.2f (no success)\n",
806  	               SCIPvarGetName(var1), newbd);
807  	         }
808  	         if ( *infeasible )
809  	         {
810  	            SCIPdebugMessage("Detected infeasibility restricting variable LB %12s to %5.2f\n",
811  	               SCIPvarGetName(var1), newbd);
812  	            return SCIP_OKAY;
813  	         }
814  	      }
815  	   }
816  	
817  	   return SCIP_OKAY;
818  	}
819  	
820  	
821  	/** propagates upper bound of second variable in relation x >= y for shifted variables */
822  	static
823  	SCIP_RETCODE propagateUpperBoundSymVar(
824  	   SCIP*                 scip,               /**< SCIP data structure */
825  	   SCIP_VAR*             var1,               /**< first variable in pair */
826  	   SCIP_VAR*             var2,               /**< second variable in pair */
827  	   SCIP_Real             center1,            /**< center of var1 (original var domain) */
828  	   SCIP_Real             center2,            /**< center of var2 (original var domain) */
829  	   SCIP_Bool             isnegated,          /**< whether var2 is negated by symmetry */
830  	   SCIP_Bool*            infeasible,         /**< pointer to store whether infeasibility is found */
831  	   int*                  nreductions,        /**< pointer to store number of reductions */
832  	   SCIP_Bool             peekmode,           /**< whether function is called in peek mode */
833  	   int                   varidx1,            /**< index of var1 (or NULL) */
834  	   int                   varidx2,            /**< index of var2 (or NULL) */
835  	   SCIP_Real*            peeklbs,            /**< lower bounds of variables in peek mode (or NULL) */
836  	   SCIP_Real*            peekubs,            /**< upper bounds of variables in peek mode (or NULL) */
837  	   SCIP_Bool*            peekbdset           /**< whether peek bounds have been set (or NULL) */
838  	   )
839  	{
840  	   SCIP_Real ub1;
841  	   SCIP_Real ub2;
842  	   SCIP_Real lb1;
843  	   SCIP_Real lb2;
844  	
845  	   SCIP_Bool tighten = FALSE;
846  	   SCIP_Real newbd;
847  	
848  	   assert( scip != NULL );
849  	   assert( var1 != NULL );
850  	   assert( var2 != NULL );
851  	   assert( infeasible != NULL );
852  	   assert( nreductions != NULL );
853  	   assert( (!peekmode) || peeklbs != NULL );
854  	   assert( (!peekmode) || peekubs != NULL );
855  	   assert( (!peekmode) || peekbdset != NULL );
856  	
857  	   SCIP_CALL( getVarBounds(var1, var2, peekmode, varidx1, varidx2, peeklbs, peekubs, peekbdset,
858  	         &lb1, &ub1, &lb2, &ub2) );
859  	
860  	   /* tighten domain of var2 to ensure that var1 - center1 >= isnegated * (var2 - center2 ) */
861  	   if ( isnegated )
862  	   {
863  	      if ( SCIPisLT(scip, ub1 - center1, center2 - lb2) )
864  	      {
865  	         tighten = TRUE;
866  	         newbd = center1 + center2 - ub1;
867  	      }
868  	   }
869  	   else
870  	   {
871  	      if ( SCIPisLT(scip, ub1 - center1, ub2 - center2) )
872  	      {
873  	         tighten = TRUE;
874  	         newbd = center2 - center1 + ub1;
875  	      }
876  	   }
877  	
878  	   if ( tighten )
879  	   {
880  	      /* in peek mode, only store updated bounds */
881  	      if ( peekmode )
882  	      {
883  	         if ( isnegated )
884  	         {
885  	            peeklbs[varidx2] = newbd; /*lint !e644*/
886  	            peekubs[varidx2] = ub2;
887  	            peekbdset[varidx2] = TRUE;
888  	         }
889  	         else
890  	         {
891  	            peeklbs[varidx2] = lb2;
892  	            peekubs[varidx2] = newbd;
893  	            peekbdset[varidx2] = TRUE;
894  	         }
895  	      }
896  	      else
897  	      {
898  	         if ( isnegated )
899  	         {
900  	            SCIP_CALL( SCIPtightenVarLb(scip, var2, newbd, TRUE, infeasible, &tighten) );
901  	         }
902  	         else
903  	         {
904  	            SCIP_CALL( SCIPtightenVarUb(scip, var2, newbd, TRUE, infeasible, &tighten) );
905  	         }
906  	
907  	         if ( tighten )
908  	         {
909  	            SCIPdebugMessage("Restricting variable %sB %12s to %5.2f\n",
910  	               isnegated ? "L" : "U", SCIPvarGetName(var2), newbd);
911  	            *nreductions += 1;
912  	         }
913  	         else
914  	         {
915  	            SCIPdebugMessage("Restricting variable %sB %12s to %5.2f (no success)\n",
916  	               isnegated ? "L" : "U", SCIPvarGetName(var2), newbd);
917  	         }
918  	         if ( *infeasible )
919  	         {
920  	            SCIPdebugMessage("Detected infeasibility restricting variable %sB %12s to %5.2f\n",
921  	               isnegated ? "L" : "U", SCIPvarGetName(var2), newbd);
922  	            return SCIP_OKAY;
923  	         }
924  	      }
925  	   }
926  	
927  	   return SCIP_OKAY;
928  	}
929  	
930  	
931  	/** propagates x - c >=  c - x */
932  	static
933  	SCIP_RETCODE propagateSelfReflectionVar(
934  	   SCIP*                 scip,               /**< SCIP data structure */
935  	   SCIP_VAR*             var,                /**< variable */
936  	   SCIP_Real             center,             /**< center of var (original var domain) */
937  	   SCIP_Bool*            infeasible,         /**< pointer to store whether infeasibility is found */
938  	   int*                  nreductions,        /**< pointer to store number of reductions */
939  	   SCIP_Bool             peekmode,           /**< whether function is called in peek mode */
940  	   int                   varidx,             /**< index of var (or NULL) */
941  	   SCIP_Real*            peeklbs,            /**< lower bounds of variables in peek mode (or NULL) */
942  	   SCIP_Real*            peekubs,            /**< upper bounds of variables in peek mode (or NULL) */
943  	   SCIP_Bool*            peekbdset           /**< whether peek bounds have been set (or NULL) */
944  	   )
945  	{
946  	   SCIP_Real ub1;
947  	   SCIP_Real ub2;
948  	   SCIP_Real lb1;
949  	   SCIP_Real lb2;
950  	   SCIP_Bool tighten = FALSE;
951  	
952  	   assert( scip != NULL );
953  	   assert( var != NULL );
954  	   assert( infeasible != NULL );
955  	   assert( nreductions != NULL );
956  	   assert( (!peekmode) || peeklbs != NULL );
957  	   assert( (!peekmode) || peekubs != NULL );
958  	   assert( (!peekmode) || peekbdset != NULL );
959  	
960  	   SCIP_CALL( getVarBounds(var, var, peekmode, varidx, varidx, peeklbs, peekubs, peekbdset,
961  	         &lb1, &ub1, &lb2, &ub2) );
962  	
963  	   if ( SCIPisLT(scip, ub1, center) )
964  	   {
965  	      *infeasible = TRUE;
966  	      return SCIP_OKAY;
967  	   }
968  	   else if ( SCIPisLT(scip, lb1, center) )
969  	   {
970  	      if ( peekmode )
971  	      {
972  	         peeklbs[varidx] = center;
973  	         peekubs[varidx] = ub1;
974  	         peekbdset[varidx] = TRUE;
975  	      }
976  	      else
977  	      {
978  	         SCIP_CALL( SCIPtightenVarLb(scip, var, center, TRUE, infeasible, &tighten) );
979  	         if ( tighten )
980  	         {
981  	            SCIPdebugMessage("Restricting variable LB %12s to %5.2f\n", SCIPvarGetName(var), center);
982  	            *nreductions += 1;
983  	         }
984  	         else
985  	         {
986  	            SCIPdebugMessage("Restricting variable LB %12s to %5.2f (no success)\n",
987  	               SCIPvarGetName(var), center);
988  	         }
989  	         if ( *infeasible )
990  	         {
991  	            SCIPdebugMessage("Detected infeasibility restricting variable LB %12s to %5.2f\n",
992  	               SCIPvarGetName(var), center);
993  	            return SCIP_OKAY;
994  	         }
995  	      }
996  	   }
997  	
998  	   return SCIP_OKAY;
999  	}
1000 	
1001 	
1002 	/** propagates lexicographic order for one pair of symmetric variables */
1003 	static
1004 	SCIP_RETCODE propagateVariablePair(
1005 	   SCIP*                 scip,               /**< SCIP data structure */
1006 	   SCIP_VAR*             var1,               /**< first variable in pair */
1007 	   SCIP_VAR*             var2,               /**< second variable in pair */
1008 	   SCIP_Real             center1,            /**< center of var1 (original var domain) */
1009 	   SCIP_Real             center2,            /**< center of var2 (original var domain) */
1010 	   SCIP_Bool             isnegated,          /**< whether var2 is negated by symmetry */
1011 	   SCIP_Bool*            infeasible,         /**< pointer to store whether infeasibility is found */
1012 	   int*                  nreductions,        /**< pointer to store number of reductions */
1013 	   SCIP_Bool             peekmode,           /**< whether function is called in peek mode */
1014 	   int                   varidx1,            /**< index of var1 (or NULL) */
1015 	   int                   varidx2,            /**< index of var2 (or NULL) */
1016 	   SCIP_Real*            peeklbs,            /**< lower bounds of variables in peek mode (or NULL) */
1017 	   SCIP_Real*            peekubs,            /**< upper bounds of variables in peek mode (or NULL) */
1018 	   SCIP_Bool*            peekbdset           /**< whether peek bounds have been set (or NULL) */
1019 	   )
1020 	{
1021 	   assert( scip != NULL );
1022 	   assert( var1 != NULL );
1023 	   assert( var2 != NULL );
1024 	   assert( infeasible != NULL );
1025 	   assert( nreductions != NULL );
1026 	
1027 	   /* perform lexicographic comparison: var1 - center1 >= +/- (var2 - center2)  */
1028 	   if ( alwaysLTshiftedVars(scip, var1, var2, center1, center2, isnegated, peekmode,
1029 	         varidx1, varidx2, peeklbs, peekubs, peekbdset) )
1030 	   {
1031 	#ifdef SCIP_DEBUG
1032 	      SCIP_Real ub1;
1033 	      SCIP_Real ub2;
1034 	      SCIP_Real lb1;
1035 	      SCIP_Real lb2;
1036 	
1037 	      /* get bounds of shifted (and possibly negated) variables */
1038 	      ub1 = SCIPvarGetUbLocal(var1);
1039 	      lb1 = SCIPvarGetLbLocal(var1);
1040 	      ub2 = SCIPvarGetUbLocal(var2);
1041 	      lb2 = SCIPvarGetLbLocal(var2);
1042 	
1043 	      SCIPdebugMessage("Detected infeasibility: x < y for "
1044 	         "x: lb=%5.2f, ub=%5.2f, shift=%5.2f "
1045 	         "y: lb=%5.2f, ub=%5.2f, shift=%5.2f negated=%u\n",
1046 	         lb1, ub1, center1, lb2, ub2, center2, isnegated);
1047 	#endif
1048 	
1049 	      *infeasible = TRUE;
1050 	      return SCIP_OKAY;
1051 	   }
1052 	
1053 	   /* for signed permutations, a variable might be mapped to itself */
1054 	   if ( var1 == var2 )
1055 	   {
1056 	      SCIP_CALL( propagateSelfReflectionVar(scip, var1, center1, infeasible, nreductions, peekmode, varidx1,
1057 	            peeklbs, peekubs, peekbdset) );
1058 	   }
1059 	   else
1060 	   {
1061 	      SCIP_CALL( propagateLowerBoundVar(scip, var1, var2, center1, center2, isnegated, infeasible, nreductions, peekmode,
1062 	            varidx1, varidx2, peeklbs, peekubs, peekbdset) );
1063 	      if ( *infeasible )
1064 	         return SCIP_OKAY;
1065 	
1066 	      SCIP_CALL( propagateUpperBoundSymVar(scip, var1, var2, center1, center2, isnegated, infeasible, nreductions, peekmode,
1067 	            varidx1, varidx2, peeklbs, peekubs, peekbdset) );
1068 	   }
1069 	
1070 	   return SCIP_OKAY;
1071 	}
1072 	
1073 	/** checks if the static lexred with a certain variable ordering is feasible in the hypothetical scenario where
1074 	 *  variables with indices i and j are fixed to fixvalue (i.e., peeking)
1075 	 */
1076 	static
1077 	SCIP_RETCODE peekStaticLexredIsFeasible(
1078 	   SCIP*                 scip,               /**< SCIP data structure */
1079 	   LEXDATA*              lexdata,            /**< pointer to data for this permutation */
1080 	   int*                  varorder,           /**< array populated with variable order (or NULL for static propagation) */
1081 	   int                   nselvars,           /**< number of variables in the ordering */
1082 	   int                   fixi,               /**< variable index of left fixed column */
1083 	   int                   fixj,               /**< variable index of right fixed column */
1084 	   int                   fixrow,             /**< row index in var ordering, from which to start peeking */
1085 	   SCIP_Real             fixvaluei,          /**< value on which variables i is fixed */
1086 	   SCIP_Real             fixvaluej,          /**< value on which variables j is fixed */
1087 	   SCIP_Bool*            peekfeasible,       /**< pointer to store whether this is feasible or not */
1088 	   SCIP_Real*            peeklbs,            /**< lower bounds of variables in peek mode (or NULL) */
1089 	   SCIP_Real*            peekubs,            /**< upper bounds of variables in peek mode (or NULL) */
1090 	   SCIP_Bool*            peekbdset           /**< whether peek bounds have been set (or NULL) */
1091 	   )
1092 	{
1093 	   int row;
1094 	   int i;
1095 	   int j;
1096 	   SCIP_VAR* vari;
1097 	   SCIP_VAR* varj;
1098 	   SCIP_Real centeri;
1099 	   SCIP_Real centerj;
1100 	   SCIP_Bool issigned;
1101 	   SCIP_Bool isnegated;
1102 	   SCIP_Bool infeasible = FALSE;
1103 	   int nreductions;
1104 	
1105 	   assert( scip != NULL );
1106 	   assert( lexdata != NULL );
1107 	   assert( lexdata->vars != NULL );
1108 	   assert( lexdata->nvars >= 0 );
1109 	   assert( nselvars <= lexdata->nvars );
1110 	   assert( nselvars > 0 );
1111 	   assert( fixi >= 0 );
1112 	   assert( fixi < lexdata->nvars );
1113 	   assert( fixj < lexdata->nvars );
1114 	   assert( fixi != fixj || lexdata->symtype == SYM_SYMTYPE_SIGNPERM );
1115 	   assert( fixi != fixj || fixvaluei == fixvaluej ); /*lint !e777*/
1116 	   assert( fixrow >= 0 );
1117 	   assert( fixrow < nselvars );
1118 	   assert( peekfeasible != NULL );
1119 	   assert( fixi == varOrderGetIndex(varorder, fixrow) );
1120 	   assert( fixj == (lexdata->invperm[varOrderGetIndex(varorder, fixrow)] % lexdata->nvars) );
1121 	   assert( fixi == (lexdata->perm[fixj] % lexdata->nvars) );
1122 	
1123 	   *peekfeasible = TRUE;
1124 	   issigned = lexdata->symtype == SYM_SYMTYPE_SIGNPERM ? TRUE : FALSE;
1125 	   assert( (!issigned) || lexdata->vardomaincenter != NULL );
1126 	
1127 	   /* intialize peekbdset */
1128 	   for (i = 0; i < lexdata->nvars; ++i)
1129 	      peekbdset[i] = FALSE;
1130 	
1131 	   peeklbs[fixi] = fixvaluei;
1132 	   peeklbs[fixj] = fixvaluej;
1133 	   peekubs[fixi] = fixvaluei;
1134 	   peekubs[fixj] = fixvaluej;
1135 	   peekbdset[fixi] = TRUE;
1136 	   peekbdset[fixj] = TRUE;
1137 	
1138 	   for (row = fixrow + 1; row < nselvars; ++row)
1139 	   {
1140 	      /* get left and right column indices */
1141 	      i = varOrderGetIndex(varorder, row);
1142 	      j = lexdata->invperm[i];
1143 	      assert( i == lexdata->perm[j] );
1144 	
1145 	      /* no fixed points */
1146 	      assert( i != j );
1147 	
1148 	      assert( 0 <= i && i < lexdata->nvars );
1149 	      assert( 0 <= j && j < 2 * lexdata->nvars );
1150 	      assert( issigned || j < lexdata->nvars );
1151 	
1152 	      vari = lexdata->vars[i];
1153 	      if ( j >= lexdata->nvars )
1154 	      {
1155 	         assert( lexdata->symtype == SYM_SYMTYPE_SIGNPERM );
1156 	         j = j - lexdata->nvars;
1157 	         varj = lexdata->vars[j];
1158 	         isnegated = TRUE;
1159 	      }
1160 	      else
1161 	      {
1162 	         varj = lexdata->vars[j];
1163 	         isnegated = FALSE;
1164 	      }
1165 	
1166 	      if ( issigned )
1167 	      {
1168 	         assert( lexdata->vardomaincenter != NULL );
1169 	         centeri = lexdata->vardomaincenter[i];
1170 	         centerj = lexdata->vardomaincenter[j];
1171 	      }
1172 	      else
1173 	      {
1174 	         centeri = 0.0;
1175 	         centerj = 0.0;
1176 	      }
1177 	
1178 	      /* propagate that vari >= varj */
1179 	
1180 	      /* vari >= varj can never hold if the maximal value of vari is smaller than the minimal value of varj */
1181 	      if ( alwaysLTshiftedVars(scip, vari, varj, centeri, centerj, isnegated, TRUE, i, j, peeklbs, peekubs, peekbdset) )
1182 	      {
1183 	         *peekfeasible = FALSE;
1184 	         SCIPdebugMessage("PEEK: Detected infeasibility at row %3d.\n", row);
1185 	         break;
1186 	      }
1187 	
1188 	      SCIP_CALL( propagateLowerBoundVar(scip, vari, varj, centeri, centerj, isnegated, &infeasible, &nreductions, TRUE,
1189 	            i, j, peeklbs, peekubs, peekbdset) );
1190 	
1191 	      SCIP_CALL( propagateUpperBoundSymVar(scip, vari, varj, centeri, centerj, isnegated, &infeasible, &nreductions, TRUE,
1192 	            i, j, peeklbs, peekubs, peekbdset) );
1193 	
1194 	      /* if there exists a solution with vari > varj, reductions are feasible w.r.t. lexred */
1195 	      if ( canGTshiftedVars(scip, vari, varj, centeri, centerj, isnegated, TRUE,
1196 	            i, j, peeklbs, peekubs, peekbdset) )
1197 	         break;
1198 	   }
1199 	
1200 	   return SCIP_OKAY;
1201 	}
1202 	
1203 	/** propagates static lexicographic reduction with specified variable ordering */
1204 	static
1205 	SCIP_RETCODE propagateStaticLexred(
1206 	   SCIP*                 scip,               /**< SCIP data structure */
1207 	   LEXDATA*              lexdata,            /**< pointer to data for this permutation */
1208 	   int*                  varorder,           /**< array populated with variable order (or NULL if static propagation) */
1209 	   int                   nselvars,           /**< number of variables in the ordering */
1210 	   SCIP_Bool*            infeasible,         /**< pointer to store whether the problem is infeasible */
1211 	   int*                  nreductions         /**< pointer to store the number of found domain reductions */
1212 	   )
1213 	{ /*lint --e{771}*/
1214 	   int row;
1215 	   int i = -1;
1216 	   int j = -1;
1217 	   SCIP_VAR* vari = NULL;
1218 	   SCIP_VAR* varj = NULL;
1219 	   SCIP_Real centeri;
1220 	   SCIP_Real centerj;
1221 	   SCIP_Bool success;
1222 	   SCIP_Bool issigned;
1223 	   SCIP_Bool isnegated;
1224 	
1225 	   assert( scip != NULL );
1226 	   assert( lexdata != NULL );
1227 	   assert( nselvars >= 0 );
1228 	   assert( infeasible != NULL );
1229 	   assert( !*infeasible );
1230 	   assert( nreductions != NULL );
1231 	   assert( *nreductions >= 0 );
1232 	
1233 	   /* avoid trivial cases */
1234 	   if ( nselvars <= 0 )
1235 	      return SCIP_OKAY;
1236 	
1237 	   issigned = lexdata->symtype == SYM_SYMTYPE_SIGNPERM ? TRUE : FALSE;
1238 	   assert( (!issigned) || lexdata->vardomaincenter != NULL );
1239 	
1240 	   /* iterate over the variable array entrywise
1241 	    *
1242 	    * We see this as two columns, with the left vector being the variable ordering,
1243 	    * and the right column the permuted variables of this var ordering.
1244 	    */
1245 	   for (row = 0; row < nselvars; ++row)
1246 	   {
1247 	      /* left and right column indices */
1248 	      i = varOrderGetIndex(varorder, row);
1249 	      j = lexdata->invperm[i];
1250 	      assert( i == lexdata->perm[j] );
1251 	
1252 	      /* no fixed points */
1253 	      assert( i != j );
1254 	
1255 	      assert( 0 <= i && i < lexdata->nvars );
1256 	      assert( 0 <= j && j < 2 * lexdata->nvars );
1257 	      assert( issigned || j < lexdata->nvars );
1258 	
1259 	      vari = lexdata->vars[i];
1260 	      if ( j >= lexdata->nvars )
1261 	      {
1262 	         assert( issigned );
1263 	         j = j - lexdata->nvars;
1264 	         varj = lexdata->vars[j];
1265 	         isnegated = TRUE;
1266 	      }
1267 	      else
1268 	      {
1269 	         varj = lexdata->vars[j];
1270 	         isnegated = FALSE;
1271 	      }
1272 	
1273 	      if ( issigned )
1274 	      {
1275 	         assert( lexdata->vardomaincenter != NULL );
1276 	         centeri = lexdata->vardomaincenter[i];
1277 	         centerj = lexdata->vardomaincenter[j];
1278 	      }
1279 	      else
1280 	      {
1281 	         centeri = 0.0;
1282 	         centerj = 0.0;
1283 	      }
1284 	
1285 	      SCIP_CALL( propagateVariablePair(scip, vari, varj, centeri, centerj, isnegated, infeasible, nreductions, FALSE,
1286 	         0, 0, NULL, NULL, NULL) );
1287 	
1288 	      if ( *infeasible )
1289 	         return SCIP_OKAY;
1290 	
1291 	      /* terminate if there exists a solution being lexicographically strictly larger than its image */
1292 	      if ( canGTshiftedVars(scip, vari, varj, centeri, centerj, isnegated, FALSE,
1293 	            0, 0, NULL, NULL, NULL) )
1294 	         break;
1295 	   }
1296 	   assert( vari != NULL );
1297 	   assert( varj != NULL );
1298 	   assert( 0 <= i && i < lexdata->nvars );
1299 	   assert( 0 <= j && j < lexdata->nvars );
1300 	
1301 	   /* if the variables in "row" are fixed to the same value, we might find further propagations */
1302 	   if ( row < nselvars )
1303 	   {
1304 	      SCIP_Real* peeklbs;
1305 	      SCIP_Real* peekubs;
1306 	      SCIP_Bool* peekbdset;
1307 	      SCIP_Real ub1;
1308 	      SCIP_Real ub2;
1309 	      SCIP_Real lb1;
1310 	      SCIP_Real lb2;
1311 	      SCIP_Real lbi;
1312 	      SCIP_Real ubi;
1313 	      SCIP_Real lbj;
1314 	      SCIP_Real ubj;
1315 	      SCIP_Bool peekfeasible;
1316 	
1317 	      SCIP_CALL( getVarBounds(vari, varj, FALSE, 0, 0, NULL, NULL, NULL, &lb1, &ub1, &lb2, &ub2) );
1318 	
1319 	      /* special treatment if i-th and j-th variable are the same in a signed permutation */
1320 	      if ( vari == varj )
1321 	      {
1322 	         assert( lexdata->symtype == SYM_SYMTYPE_SIGNPERM );
1323 	         assert( SCIPGE(scip, lb1, lexdata->vardomaincenter[i]) ); /* propagation enforces xi - center >= center - xi */
1324 	
1325 	         /* both variables can only be the same if they are fixed to the domain center */
1326 	         if ( SCIPGT(scip, lb1, lexdata->vardomaincenter[i]) )
1327 	            return SCIP_OKAY;
1328 	
1329 	         SCIP_CALL( SCIPallocBufferArray(scip, &peeklbs, lexdata->nvars) );
1330 	         SCIP_CALL( SCIPallocBufferArray(scip, &peekubs, lexdata->nvars) );
1331 	         SCIP_CALL( SCIPallocBufferArray(scip, &peekbdset, lexdata->nvars) );
1332 	
1333 	         SCIP_CALL( peekStaticLexredIsFeasible(scip, lexdata, varorder, nselvars, i, j,
1334 	               row, lexdata->vardomaincenter[i], lexdata->vardomaincenter[i],
1335 	               &peekfeasible, peeklbs, peekubs, peekbdset) );
1336 	         if ( !peekfeasible )
1337 	         {
1338 	            /* both variables cannot be the same, so the non-negated variable must be greater than the domain center */
1339 	            switch ( SCIPvarGetType(vari) )
1340 	            {
1341 	            case SCIP_VARTYPE_BINARY:
1342 	            case SCIP_VARTYPE_IMPLINT:
1343 	            case SCIP_VARTYPE_INTEGER:
1344 	               assert( SCIPisIntegral(scip, lb1) );
1345 	               SCIP_CALL( SCIPtightenVarLb(scip, vari, lexdata->vardomaincenter[i] + 1.0, TRUE, infeasible, &success) );
1346 	               if ( success )
1347 	                  *nreductions += 1;
1348 	               if ( *infeasible )
1349 	                  goto FREEMEMORY;
1350 	               lb1 = lexdata->vardomaincenter[i] + 1.0;
1351 	               assert( SCIPLE(scip, lb1, ub1) );
1352 	               break;
1353 	            case SCIP_VARTYPE_CONTINUOUS:
1354 	               /* continuous variable type: act as if we increase the variable by a very little bit.
1355 	                * This is only possible if we're able to increase the variable bound by a bit.
1356 	                */
1357 	               if ( SCIPEQ(scip, lb1, ub1) )
1358 	               {
1359 	                  *infeasible = TRUE;
1360 	                  goto FREEMEMORY;
1361 	               }
1362 	               break;
1363 	            default:
1364 	               SCIPerrorMessage("unsupported variable type encountered at the lexicographic reduction propagator\n");
1365 	               return SCIP_ERROR;
1366 	            }
1367 	         }
1368 	      }
1369 	      else
1370 	      {
1371 	         /* The previous loop is broken at row "row", which allows for choosing vari > varj.
1372 	          *
1373 	          * Now check if vari == varj is permitted, and if not, tighten the domain further.
1374 	          *
1375 	          * @todo We peek twice if vari and varj are unfixed
1376 	          * But, if the subcycle only contains var1 and var2, a single peek suffices.
1377 	          * This is similar to orbisack and symresack propagation.
1378 	          *
1379 	          * Case 1: vari is minimal (lbi).
1380 	          * Then, propagation of lbi = vari >= varj can yield two situations:
1381 	          *   Option 1: varj can take a value < lbi. Then no further reductions can be detected.
1382 	          *   Option 2: varj gets fixed to lbi. Then, we must check if feasibility is found, still.
1383 	          *     If it turns out infeasible, then we know vari cannot take value lbi, so we can increase the lower bound.
1384 	          */
1385 	         centeri = 0.0;
1386 	         centerj = 0.0;
1387 	
1388 	         if ( lexdata->vardomaincenter != NULL )
1389 	         {
1390 	            centeri = lexdata->vardomaincenter[i];
1391 	            centerj = lexdata->vardomaincenter[j];
1392 	         }
1393 	
1394 	         /* translate variable bounds to shifted variable domain and take negation into account */
1395 	         lbi = lb1 - centeri;
1396 	         ubi = ub1 - centeri;
1397 	         if ( isnegated )
1398 	         {
1399 	            lbj = centerj - ub2;
1400 	            ubj = centerj - lb2;
1401 	         }
1402 	         else
1403 	         {
1404 	            lbj = lb2 - centerj;
1405 	            ubj = ub2 - centerj;
1406 	         }
1407 	
1408 	         /* check whether peek is called */
1409 	         if ( (!SCIPEQ(scip, lbi, lbj)) && (!SCIPEQ(scip, ubi, ubj)) )
1410 	            return SCIP_OKAY;
1411 	
1412 	         SCIP_CALL( SCIPallocBufferArray(scip, &peeklbs, lexdata->nvars) );
1413 	         SCIP_CALL( SCIPallocBufferArray(scip, &peekubs, lexdata->nvars) );
1414 	         SCIP_CALL( SCIPallocBufferArray(scip, &peekbdset, lexdata->nvars) );
1415 	
1416 	         if ( SCIPEQ(scip, lbj, lbi) )
1417 	         {
1418 	            SCIP_Real fixvalj;
1419 	
1420 	            /* translate lbj back to original variable domain of variable j */
1421 	            if ( isnegated )
1422 	               fixvalj = centerj - lbj;
1423 	            else
1424 	               fixvalj = lbj + centerj;
1425 	
1426 	            /* this is Option 2: varj gets fixed to lbi by propagation. */
1427 	            SCIP_CALL( peekStaticLexredIsFeasible(scip, lexdata, varorder, nselvars, i, j,
1428 	                  row, lbi + centeri, fixvalj, &peekfeasible, peeklbs, peekubs, peekbdset) );
1429 	            if ( !peekfeasible )
1430 	            {
1431 	               /* vari cannot take value lb1, so we increase the lower bound. (do not use lbi as this is a shifted domain bound) */
1432 	               switch ( SCIPvarGetType(vari) )
1433 	               {
1434 	               case SCIP_VARTYPE_BINARY:
1435 	               case SCIP_VARTYPE_IMPLINT:
1436 	               case SCIP_VARTYPE_INTEGER:
1437 	                  /* discrete variable type: increase lower bound by 1. */
1438 	                  assert( SCIPisIntegral(scip, lb1) );
1439 	                  SCIP_CALL( SCIPtightenVarLb(scip, vari, lb1 + 1.0, TRUE, infeasible, &success) );
1440 	                  if ( success )
1441 	                     *nreductions += 1;
1442 	                  if ( *infeasible )
1443 	                     goto FREEMEMORY;
1444 	                  lb1 = lb1 + 1.0;
1445 	                  assert( SCIPLE(scip, lb1, ub1) );
1446 	                  break;
1447 	               case SCIP_VARTYPE_CONTINUOUS:
1448 	                  /* continuous variable type: act as if we increase the variable by a very little bit.
1449 	                   * That is only possible if we're able to increase the variable bound by a bit.
1450 	                   */
1451 	                  if ( SCIPEQ(scip, lbi, ubi) )
1452 	                  {
1453 	                     *infeasible = TRUE;
1454 	                     goto FREEMEMORY;
1455 	                  }
1456 	                  break;
1457 	               default:
1458 	                  SCIPerrorMessage("unsupported variable type encountered at the lexicographic reduction propagator\n");
1459 	                  return SCIP_ERROR;
1460 	               }
1461 	            }
1462 	         }
1463 	
1464 	         /* Case 2: varj is maximal (ubj).
1465 	          * Then, propagation of vari >= varj = ubj can yield two situatiosn:
1466 	          *   Option 1: vari can take a value > ubj. Then, no further reductions can be detected.
1467 	          *   Option 2: vari gets fixed to ubj. Then, we must check if feasibility is found, still.
1468 	          *     If it turns out infeasible, then we know varj cannot take value ubj, so we can decrease the upper bound.
1469 	          */
1470 	         assert( SCIPGE(scip, ubi, ubj) );  /* this must be the case after reductions in the for-loop */
1471 	         if ( SCIPEQ(scip, ubi, ubj) )
1472 	         {
1473 	            SCIP_Real fixvalj;
1474 	
1475 	            /* translate ubj back to original variable domain of variable j */
1476 	            if ( isnegated )
1477 	               fixvalj = centerj - ubj;
1478 	            else
1479 	               fixvalj = ubj + centerj;
1480 	
1481 	            /* this is Option 2: vari gets fixed to ubj by propagation. */
1482 	            SCIP_CALL( peekStaticLexredIsFeasible(scip, lexdata, varorder, nselvars, i, j,
1483 	                  row, ubi + centeri, fixvalj, &peekfeasible, peeklbs, peekubs, peekbdset) );
1484 	            if ( !peekfeasible )
1485 	            {
1486 	               /* varj cannot take value ub2, so we decrease the upper or lower bound. (do not use ubj as this is a shifted domain bound)*/
1487 	               switch ( SCIPvarGetType(varj) )
1488 	               {
1489 	               case SCIP_VARTYPE_BINARY:
1490 	               case SCIP_VARTYPE_IMPLINT:
1491 	               case SCIP_VARTYPE_INTEGER:
1492 	                  /* discrete variable type: decrease upper bound by 1. */
1493 	                  if ( isnegated )
1494 	                  {
1495 	                     assert( SCIPisIntegral(scip, lb2) );
1496 	                     SCIP_CALL( SCIPtightenVarUb(scip, varj, lb2 + 1.0, TRUE, infeasible, &success) );
1497 	                  }
1498 	                  else
1499 	                  {
1500 	                     assert( SCIPisIntegral(scip, ub2) );
1501 	                     SCIP_CALL( SCIPtightenVarUb(scip, varj, ub2 - 1.0, TRUE, infeasible, &success) );
1502 	                  }
1503 	                  if ( success )
1504 	                     *nreductions += 1;
1505 	                  if ( *infeasible )
1506 	                     goto FREEMEMORY;
1507 	                  ubj = ubj - 1.0;
1508 	                  assert( SCIPLE(scip, lbj, ubj) );
1509 	                  break;
1510 	               case SCIP_VARTYPE_CONTINUOUS:
1511 	                  /* continuous variable type: act as if we decrease the variable by a very little bit.
1512 	                   * that is only possible if we're able to decrease the variable bound by a bit. */
1513 	                  if ( SCIPEQ(scip, lbj, ubj) )
1514 	                  {
1515 	                     *infeasible = TRUE;
1516 	                     goto FREEMEMORY;
1517 	                  }
1518 	                  break;
1519 	               default:
1520 	                  return SCIP_ERROR;
1521 	               }
1522 	            }
1523 	         }
1524 	      }
1525 	   FREEMEMORY:
1526 	      SCIPfreeBufferArray(scip, &peekbdset);
1527 	      SCIPfreeBufferArray(scip, &peekubs);
1528 	      SCIPfreeBufferArray(scip, &peeklbs);
1529 	   }
1530 	
1531 	   return SCIP_OKAY;
1532 	}
1533 	
1534 	
1535 	/** propagation method for a dynamic lexicographic reduction */
1536 	static
1537 	SCIP_RETCODE propagateLexredDynamic(
1538 	   SCIP*                 scip,               /**< SCIP data structure */
1539 	   SCIP_LEXREDDATA*      masterdata,         /**< pointer to global data for lexicographic reduction propagator */
1540 	   LEXDATA*              lexdata,            /**< pointer to data for this permutation */
1541 	   NODEDEPTHBRANCHINDEX* nodedepthbranchindices, /**< array with (depth, index)-information per variable in
1542 	                                                  *   rooted path to focus node */
1543 	   int                   nvarstotal,         /**< length of nodedepthbranchindices array */
1544 	   SCIP_VAR**            branchvars,         /**< array populated with variables branched on */
1545 	   int                   nbranchvars,        /**< number of elements in branchvars array */
1546 	   SCIP_Bool*            infeasible,         /**< pointer to store whether the problem is infeasible */
1547 	   int*                  nreductions         /**< pointer to store the number of found domain reductions */
1548 	   )
1549 	{
1550 	   int* varorder;
1551 	   int nvarorder;
1552 	   int nvars;
1553 	
1554 	   assert( scip != NULL );
1555 	   assert( masterdata != NULL );
1556 	   assert( lexdata != NULL );
1557 	   assert( lexdata->isdynamic );
1558 	   assert( nodedepthbranchindices != NULL );
1559 	   assert( nvarstotal >= 0 );
1560 	   assert( branchvars != NULL );
1561 	   assert( nbranchvars >= 0 );
1562 	   assert( infeasible != NULL );
1563 	   assert( nreductions != NULL );
1564 	
1565 	   nvars = lexdata->nvars;
1566 	
1567 	   /* get variable order */
1568 	   SCIP_CALL( SCIPallocBufferArray(scip, &varorder, nvars) );
1569 	
1570 	   SCIP_CALL( getVarOrder(scip, masterdata, lexdata, nodedepthbranchindices, nvarstotal, branchvars, nbranchvars,
1571 	         varorder, &nvarorder, nvars) );
1572 	   assert( nvarorder >= 0 );
1573 	   assert( nvarorder <= nvars );
1574 	
1575 	   /* possibly propagate the constraint with this variable order */
1576 	   if ( nvarorder > 0 )
1577 	   {
1578 	      SCIP_CALL( propagateStaticLexred(scip, lexdata, varorder, nvarorder, infeasible, nreductions) );
1579 	   }
1580 	   SCIPfreeBufferArray(scip, &varorder);
1581 	
1582 	   return SCIP_OKAY;
1583 	}
1584 	
1585 	
1586 	/** propagation method for a dynamic lexicographic reduction */
1587 	static
1588 	SCIP_RETCODE propagateLexredStatic(
1589 	   SCIP*                 scip,               /**< SCIP data structure */
1590 	   SCIP_LEXREDDATA*      masterdata,         /**< pointer to global data for lexicographic reduction propagator */
1591 	   LEXDATA*              lexdata,            /**< pointer to data for this permutation */
1592 	   SCIP_Bool*            infeasible,         /**< pointer to store whether the problem is infeasible */
1593 	   int*                  nreductions         /**< pointer to store the number of found domain reductions */
1594 	   )
1595 	{
1596 	   assert( scip != NULL );
1597 	   assert( masterdata != NULL );
1598 	   assert( lexdata != NULL );
1599 	   assert( ! lexdata->isdynamic );
1600 	   assert( infeasible != NULL );
1601 	   assert( nreductions != NULL );
1602 	
1603 	   /* skip trivial cases */
1604 	   if ( lexdata->nvars == 0 )
1605 	      return SCIP_OKAY;
1606 	
1607 	   /* propagate the constraint with this variable order */
1608 	   SCIP_CALL( propagateStaticLexred(scip, lexdata, NULL, lexdata->nvars, infeasible, nreductions) );
1609 	
1610 	   return SCIP_OKAY;
1611 	}
1612 	
1613 	
1614 	/** propagation method for applying dynamic lexicographic reduction for a single permutation */
1615 	static
1616 	SCIP_RETCODE propagateLexicographicReductionPerm(
1617 	   SCIP*                 scip,               /**< SCIP data structure */
1618 	   SCIP_LEXREDDATA*      masterdata,         /**< pointer to global data for lexicographic reduction propagator */
1619 	   LEXDATA*              lexdata,            /**< pointer to data for this permutation */
1620 	   NODEDEPTHBRANCHINDEX* nodedepthbranchindices, /**< array with (depth, index)-information per variable in
1621 	                                                  *   rooted path to focus node */
1622 	   int                   nvarstotal,         /**< length of that array */
1623 	   SCIP_VAR**            branchvars,         /**< array populated with variables branched on */
1624 	   int                   nbranchvars,        /**< number of elements in branchvars array */
1625 	   SCIP_Bool*            infeasible,         /**< pointer to store whether the problem is infeasible */
1626 	   int*                  nreductions         /**< pointer to store the number of found domain reductions */
1627 	   )
1628 	{
1629 	   assert( scip != NULL );
1630 	   assert( masterdata != NULL );
1631 	   assert( lexdata != NULL );
1632 	   assert( nodedepthbranchindices != NULL || ! lexdata->isdynamic );
1633 	   assert( nvarstotal >= 0 || ! lexdata->isdynamic );
1634 	   assert( branchvars != NULL || ! lexdata->isdynamic );
1635 	   assert( nbranchvars >= 0 || ! lexdata->isdynamic );
1636 	   assert( infeasible != NULL );
1637 	   assert( nreductions != NULL );
1638 	
1639 	   *nreductions = 0;
1640 	   *infeasible = FALSE;
1641 	
1642 	   if ( lexdata->isdynamic )
1643 	   {
1644 	      SCIP_CALL( propagateLexredDynamic(scip, masterdata, lexdata,
1645 	            nodedepthbranchindices, nvarstotal, branchvars, nbranchvars, infeasible, nreductions) );
1646 	   }
1647 	   else
1648 	   {
1649 	      SCIP_CALL( propagateLexredStatic(scip, masterdata, lexdata, infeasible, nreductions) );
1650 	   }
1651 	
1652 	   return SCIP_OKAY;
1653 	}
1654 	
1655 	
1656 	/** populates array with information of first variable change
1657 	 *  @pre assuming nodedepthbranchindices is initially clean
1658 	 */
1659 	static
1660 	SCIP_RETCODE shadowtreeFillNodeDepthBranchIndices(
1661 	   SCIP*                 scip,               /**< SCIP data structure */
1662 	   SCIP_LEXREDDATA*      masterdata,         /**< pointer to global data for lexicographic reduction propagator */
1663 	   NODEDEPTHBRANCHINDEX* nodedepthbranchindices, /**< array to populate */
1664 	   SCIP_VAR**            branchvars,         /**< array to populate with variables branched on */
1665 	   int*                  nbranchvars,        /**< number of elements in branchvars array */
1666 	   SCIP_SHADOWTREE*      shadowtree,         /**< pointer to shadow tree structure */
1667 	   SCIP_NODE*            focusnode,          /**< focusnode to which the rooted path is evaluated */
1668 	   SCIP_Bool*            inforesolved        /**< pointer to store whether information is successfully resolved */
1669 	   )
1670 	{
1671 	   SCIP_SHADOWNODE* shadownode;
1672 	   SCIP_SHADOWNODE* shadowchild;
1673 	   int shadowdepth;
1674 	   SCIP_VAR* var;
1675 	   int varindex;
1676 	   int nlevelvars;
1677 	   int c;
1678 	   int i;
1679 	
1680 	   assert( scip != NULL );
1681 	   assert( masterdata != NULL );
1682 	   assert( masterdata->symvarmap != NULL );
1683 	   assert( masterdata->nsymvars >= 0 );
1684 	   assert( nodedepthbranchindices != NULL );
1685 	   assert( branchvars != NULL );
1686 	   assert( nbranchvars != NULL );
1687 	   assert( shadowtree != NULL );
1688 	   assert( focusnode != NULL );
1689 	   assert( inforesolved != NULL );
1690 	
1691 	   shadownode = SCIPshadowTreeGetShadowNode(shadowtree, focusnode);
1692 	
1693 	   if ( shadownode == NULL )
1694 	   {
1695 	      /* the arrays to fill are unchanged, so they remain clean */
1696 	      *inforesolved = FALSE;
1697 	      if ( !masterdata->treewarninggiven )
1698 	      {
1699 	         SCIPwarningMessage(scip, "Attempting lexicographic reduction on nodes not existing in the symmetry shadowtree"
1700 	            " (and suppressing future warnings)\n");
1701 	         masterdata->treewarninggiven = TRUE;
1702 	      }
1703 	      return SCIP_OKAY;
1704 	   }
1705 	   shadowdepth = SCIPnodeGetDepth(focusnode);
1706 	
1707 	   /* branchvars array is initially empty */
1708 	   *nbranchvars = 0;
1709 	
1710 	   /* We start looking one level lower, because we consider the branching decisions each time. */
1711 	   shadownode = shadownode->parent;
1712 	
1713 	   /* Now, walk from the leaf to the root. Each time look at all the children of the node considered,
1714 	    * and save the variable depth and index in the branching array. It is important to consider all children each time,
1715 	    * because we need to comply with the instance where in different branches it is branched on different variables.
1716 	    * This has to be consistent.
1717 	    */
1718 	   while (shadownode != NULL)
1719 	   {
1720 	      assert( shadowdepth > 0 );
1721 	      nlevelvars = 0;
1722 	      for (c = 0; c < shadownode->nchildren; ++c)
1723 	      {
1724 	         shadowchild = shadownode->children[c];
1725 	
1726 	         /* get the variables branched on, for each of the children (that's likely 1 variable each time) */
1727 	         for (i = 0; i < shadowchild->nbranchingdecisions; ++i)
1728 	         {
1729 	            var = shadowchild->branchingdecisions[i].var;
1730 	            assert( SCIPvarIsTransformed(var) );
1731 	
1732 	            varindex = SCIPhashmapGetImageInt(masterdata->symvarmap, var);
1733 	
1734 	            /* ignore variables that are irrelevant for lexicographic reduction */
1735 	            if ( varindex == INT_MAX )
1736 	               continue;
1737 	
1738 	            assert( varindex >= 0 );
1739 	            assert( varindex < masterdata->nsymvars );
1740 	
1741 	            /* var already in other child at this level? Continue */
1742 	            if ( nodedepthbranchindices[varindex].nodedepth == shadowdepth )
1743 	               continue;
1744 	
1745 	            /* the variable is either not seen (nodedepth == 0), or it is at a higher level (nodedepth > shadowdepth) */
1746 	            assert( nodedepthbranchindices[varindex].nodedepth == 0 ||
1747 	               nodedepthbranchindices[varindex].nodedepth > shadowdepth);
1748 	
1749 	            if ( nodedepthbranchindices[varindex].nodedepth == 0 )
1750 	            {
1751 	               /* variable is not featured in branchvars, yet */
1752 	               assert( *nbranchvars < masterdata->nsymvars );
1753 	               branchvars[(*nbranchvars)++] = var;
1754 	            }
1755 	
1756 	            /* var is not seen on this level yet. Update */
1757 	            nodedepthbranchindices[varindex].nodedepth = shadowdepth;
1758 	            nodedepthbranchindices[varindex].index = nlevelvars++;
1759 	         }
1760 	      }
1761 	
1762 	      /* prepare for the next iteration */
1763 	      shadownode = shadownode->parent;
1764 	      --shadowdepth;
1765 	   }
1766 	   /* In the last iteration, we handled the branching decisions at the root node, so shadowdepth must have value 0. */
1767 	   assert( shadowdepth == 0 );
1768 	
1769 	   *inforesolved = TRUE;
1770 	   return SCIP_OKAY;
1771 	}
1772 	
1773 	
1774 	/** cleans nodedepthbranchindices array */
1775 	static
1776 	SCIP_RETCODE shadowtreeUndoNodeDepthBranchIndices(
1777 	   SCIP*                 scip,               /**< SCIP data structure */
1778 	   SCIP_LEXREDDATA*      masterdata,         /**< pointer to global data for lexicographic reduction propagator */
1779 	   NODEDEPTHBRANCHINDEX* nodedepthbranchindices, /**< array populated by nodedepthbranchindices to clean */
1780 	   SCIP_VAR**            branchvars,         /**< array populated with variables branched on */
1781 	   int*                  nbranchvars,        /**< number of elements in branchvars array */
1782 	   SCIP_SHADOWTREE*      shadowtree,         /**< pointer to shadow tree structure */
1783 	   SCIP_NODE*            focusnode           /**< focusnode to which the rooted path is evaluated */
1784 	   )
1785 	{
1786 	   /* undo the operations from shadowtreeFillNodeDepthBranchIndices, which makes nodedepthbranchindices clean */
1787 	   SCIP_SHADOWNODE* shadownode;
1788 	   SCIP_SHADOWNODE* shadowchild;
1789 	#ifndef NDEBUG
1790 	   int shadowdepth;
1791 	#endif
1792 	   SCIP_VAR* var;
1793 	   int varindex;
1794 	   int c;
1795 	   int i;
1796 	
1797 	   assert( scip != NULL );
1798 	   assert( masterdata != NULL );
1799 	   assert( masterdata->symvarmap != NULL );
1800 	   assert( masterdata->nsymvars >= 0 );
1801 	   assert( nodedepthbranchindices != NULL );
1802 	   assert( branchvars != NULL );
1803 	   assert( nbranchvars != NULL );
1804 	   assert( *nbranchvars >= 0 );
1805 	   assert( *nbranchvars <= masterdata->nsymvars );
1806 	   assert( shadowtree != NULL );
1807 	   assert( focusnode != NULL );
1808 	
1809 	   shadownode = SCIPshadowTreeGetShadowNode(shadowtree, focusnode);
1810 	#ifndef NDEBUG
1811 	   shadowdepth = SCIPnodeGetDepth(focusnode);
1812 	#endif
1813 	
1814 	   /* clean nbranchvars array */
1815 	   while ( *nbranchvars > 0 )
1816 	      branchvars[--(*nbranchvars)] = NULL;
1817 	   assert( *nbranchvars == 0 );
1818 	
1819 	   /* we start looking one level lower, because we consider the branching decisions each time */
1820 	   shadownode = shadownode->parent;
1821 	
1822 	   /* now, walk from the leaf to the root. Each time look at all the children of the node considered,
1823 	    * and save the variable depth and index in the branching array. It is important to consider all children each time,
1824 	    * because we need to comply with the instance where in different branches it is branched on different variables.
1825 	    * This has to be consistent.
1826 	    */
1827 	   while (shadownode != NULL)
1828 	   {
1829 	#ifndef NDEBUG
1830 	      assert( shadowdepth > 0 );
1831 	#endif
1832 	      for (c = 0; c < shadownode->nchildren; ++c)
1833 	      {
1834 	         shadowchild = shadownode->children[c];
1835 	         /* get the variables branched on, for each of the children (that's likely 1 variable each time) */
1836 	         for (i = 0; i < shadowchild->nbranchingdecisions; ++i)
1837 	         {
1838 	            var = shadowchild->branchingdecisions[i].var;
1839 	            /* ignore variables not relevant for lexicographic reduction */
1840 	            if ( !SCIPhashmapExists(masterdata->symvarmap, (void*) var) )
1841 	               continue;
1842 	            assert( SCIPhashmapExists(masterdata->symvarmap, (void*) var) );
1843 	
1844 	            varindex = SCIPhashmapGetImageInt(masterdata->symvarmap, var);
1845 	            assert( varindex >= 0 );
1846 	            assert( varindex < masterdata->nsymvars );
1847 	
1848 	            /* reset */
1849 	            nodedepthbranchindices[varindex].index = 0;
1850 	            nodedepthbranchindices[varindex].nodedepth = 0;
1851 	         }
1852 	      }
1853 	
1854 	      /* prepare for the next iteration */
1855 	      shadownode = shadownode->parent;
1856 	#ifndef NDEBUG
1857 	      --shadowdepth;
1858 	#endif
1859 	   }
1860 	   /* In the last iteration, we handled the branching decisions at the root node, so shadowdepth must have value 0. */
1861 	   assert( shadowdepth == 0 );
1862 	
1863 	   return SCIP_OKAY;
1864 	}
1865 	
1866 	
1867 	/*
1868 	 * Interface methods
1869 	 */
1870 	
1871 	
1872 	/** prints lexicographic reduction propagation data */
1873 	SCIP_RETCODE SCIPlexicographicReductionGetStatistics(
1874 	   SCIP*                 scip,               /**< SCIP data structure */
1875 	   SCIP_LEXREDDATA*      masterdata,         /**< pointer to global data for lexicographic reduction propagator */
1876 	   int*                  nred,               /**< total number of reductions applied */
1877 	   int*                  ncutoff             /**< total number of cutoffs applied */
1878 	   )
1879 	{
1880 	   assert( scip != NULL );
1881 	   assert( masterdata != NULL );
1882 	   assert( nred != NULL );
1883 	
1884 	   *nred = masterdata->nred;
1885 	   *ncutoff = masterdata->ncutoff;
1886 	
1887 	   return SCIP_OKAY;
1888 	}
1889 	
1890 	/** prints lexicographic reduction propagation data */
1891 	SCIP_RETCODE SCIPlexicographicReductionPrintStatistics(
1892 	   SCIP*                 scip,               /**< SCIP data structure */
1893 	   SCIP_LEXREDDATA*      masterdata          /**< pointer to global data for lexicographic reduction propagator */
1894 	   )
1895 	{
1896 	   int i;
1897 	
1898 	   assert( scip != NULL );
1899 	   assert( masterdata != NULL );
1900 	
1901 	   if ( masterdata->nlexdatas == 0 )
1902 	   {
1903 	      SCIPverbMessage(scip, SCIP_VERBLEVEL_HIGH, NULL, "   lexicographic reduction:   no permutations\n");
1904 	      return SCIP_OKAY;
1905 	   }
1906 	
1907 	   SCIPverbMessage(scip, SCIP_VERBLEVEL_HIGH, NULL, "   lexicographic reduction: %4d permutations with support sizes ",
1908 	      masterdata->nlexdatas);
1909 	
1910 	   for (i = 0; i < masterdata->nlexdatas; ++i)
1911 	   {
1912 	      if ( i > 0 )
1913 	         SCIPverbMessage(scip, SCIP_VERBLEVEL_HIGH, NULL, ", ");
1914 	      SCIPverbMessage(scip, SCIP_VERBLEVEL_HIGH, NULL, "%d", masterdata->lexdatas[i]->nvars);
1915 	   }
1916 	
1917 	   SCIPverbMessage(scip, SCIP_VERBLEVEL_HIGH, NULL, "\n");
1918 	
1919 	   return SCIP_OKAY;
1920 	}
1921 	
1922 	
1923 	/** applies lexicographic reduction propagation */
1924 	SCIP_RETCODE SCIPlexicographicReductionPropagate(
1925 	   SCIP*                 scip,               /**< SCIP data structure */
1926 	   SCIP_LEXREDDATA*      masterdata,         /**< pointer to global data for lexicographic reduction propagator */
1927 	   SCIP_Bool*            infeasible,         /**< pointer to store whether infeasibility is found */
1928 	   int*                  nred,               /**< pointer to store the number of domain reductions */
1929 	   SCIP_Bool*            didrun              /**< a global pointer maintaining if any symmetry propagator has run
1930 	                                              *   only set this to TRUE when a reduction is found, never set to FALSE */
1931 	   )
1932 	{
1933 	   int nlocalred;
1934 	   int p;
1935 	   SCIP_SHADOWTREE* shadowtree = NULL;
1936 	   SCIP_NODE* focusnode = NULL;
1937 	   NODEDEPTHBRANCHINDEX* nodedepthbranchindices = NULL;
1938 	   SCIP_VAR** branchvars = NULL;
1939 	   int nbranchvars = 0;
1940 	   SCIP_Bool inforesolved;
1941 	
1942 	   assert( scip != NULL );
1943 	   assert( masterdata != NULL );
1944 	   assert( (masterdata->lexdatas == NULL) == (masterdata->nlexdatas == 0) );
1945 	   assert( masterdata->nlexdatas >= 0 );
1946 	   assert( masterdata->nlexdatas <= masterdata->maxnlexdatas );
1947 	   assert( infeasible != NULL );
1948 	   assert( nred != NULL );
1949 	   assert( didrun != NULL );
1950 	
1951 	   *infeasible = FALSE;
1952 	   *nred = 0;
1953 	
1954 	   /* early termination */
1955 	   if ( masterdata->nlexdatas == 0 )
1956 	      return SCIP_OKAY;
1957 	
1958 	   /* compute the variable ordering based on the branching decisions
1959 	    * of the shadowtree if there exist dynamic permutations
1960 	    */
1961 	   if ( masterdata->hasdynamicperm )
1962 	   {
1963 	      assert( masterdata->shadowtreeeventhdlr != NULL );
1964 	      shadowtree = SCIPgetShadowTree(masterdata->shadowtreeeventhdlr);
1965 	      focusnode = SCIPgetFocusNode(scip);
1966 	
1967 	      /* fill the node-depth-branch-indices structure
1968 	       *
1969 	       * this is an array that maps every variable index to (depth, index) = (0, 0) if the variable is not branched on,
1970 	       * or (depth, index) is the depth (branching at root node: depth 1) and variable index when it was branched thereon.
1971 	       * For individual dynamic lexicographic reductions, we use this ordering the following way:
1972 	       *  1. Choose those variables that have (depth, index) with depth > 0 (these)
1973 	       *  2. Sort by depth, then by index, in increasing order.
1974 	       */
1975 	      SCIP_CALL( SCIPallocCleanBufferArray(scip, &nodedepthbranchindices, masterdata->nsymvars) );
1976 	      SCIP_CALL( SCIPallocCleanBufferArray(scip, &branchvars, masterdata->nsymvars) );
1977 	      SCIP_CALL( shadowtreeFillNodeDepthBranchIndices(scip, masterdata, nodedepthbranchindices,
1978 	            branchvars, &nbranchvars, shadowtree, focusnode, &inforesolved) );
1979 	
1980 	      /* if the information cannot be resolved because a node is missing from the shadowtree, do not propagate */
1981 	      if ( !inforesolved )
1982 	      {
1983 	         /* shadowtreeFillNodeDepthBranchIndices keeps the input arrays clean if it terminates early */
1984 	         SCIPfreeCleanBufferArray(scip, &branchvars);
1985 	         SCIPfreeCleanBufferArray(scip, &nodedepthbranchindices);
1986 	         return SCIP_OKAY;
1987 	      }
1988 	      /* ... Do everything using this nodedepthbranchindices structure */
1989 	   }
1990 	
1991 	   if ( nbranchvars > 0 || ! masterdata->hasdynamicperm )
1992 	   {
1993 	      /* apply lexicographic reduction propagator to all lexdata objects */
1994 	      for (p = 0; p < masterdata->nlexdatas; ++p)
1995 	      {
1996 	         assert( masterdata->lexdatas[p] != NULL );
1997 	
1998 	         SCIP_CALL( propagateLexicographicReductionPerm(scip, masterdata, masterdata->lexdatas[p],
1999 	            nodedepthbranchindices, masterdata->nsymvars, branchvars, nbranchvars, infeasible, &nlocalred) );
2000 	
2001 	         /* keep track of the total number of fixed vars */
2002 	         *nred += nlocalred;
2003 	
2004 	         /* a symmetry propagator has ran, so set didrun to TRUE */
2005 	         *didrun = TRUE;
2006 	
2007 	         /* stop if we find infeasibility */
2008 	         if ( *infeasible )
2009 	            break;
2010 	      }
2011 	
2012 	      /* maintain total number of reductions made */
2013 	      masterdata->nred += *nred;
2014 	      if ( *infeasible )
2015 	         ++masterdata->ncutoff;
2016 	   }
2017 	
2018 	   /* possibly clean the node-depth-branch-indices structure */
2019 	   if ( masterdata->hasdynamicperm )
2020 	   {
2021 	      assert( shadowtree != NULL );
2022 	      assert( focusnode != NULL );
2023 	      SCIP_CALL( shadowtreeUndoNodeDepthBranchIndices(scip, masterdata, nodedepthbranchindices,
2024 	            branchvars, &nbranchvars, shadowtree, focusnode) );
2025 	      assert( nbranchvars == 0 );
2026 	      SCIPfreeCleanBufferArray(scip, &branchvars);
2027 	      SCIPfreeCleanBufferArray(scip, &nodedepthbranchindices);
2028 	   }
2029 	
2030 	   return SCIP_OKAY;
2031 	}
2032 	
2033 	
2034 	/** adds permutation for lexicographic reduction propagation */
2035 	SCIP_RETCODE SCIPlexicographicReductionAddPermutation(
2036 	   SCIP*                 scip,               /**< SCIP data structure */
2037 	   SCIP_LEXREDDATA*      masterdata,         /**< pointer to global data for lexicographic reduction propagator */
2038 	   SCIP_VAR**            permvars,           /**< variable array of the permutation */
2039 	   int                   npermvars,          /**< number of variables in that array */
2040 	   int*                  perm,               /**< permutation */
2041 	   SYM_SYMTYPE           symtype,            /**< type of symmetries in perm */
2042 	   SCIP_Real*            permvardomaincenter, /**< array containing center point for each variable domain */
2043 	   SCIP_Bool             usedynamicorder,    /**< whether a dynamic variable order shall be used */
2044 	   SCIP_Bool*            success             /**< to store whether the component is successfully added */
2045 	   )
2046 	{
2047 	   assert( scip != NULL );
2048 	   assert( masterdata != NULL );
2049 	   assert( (masterdata->lexdatas == NULL) == (masterdata->nlexdatas == 0) );
2050 	   assert( masterdata->nlexdatas >= 0 );
2051 	   assert( masterdata->nlexdatas <= masterdata->maxnlexdatas );
2052 	   assert( masterdata->shadowtreeeventhdlr != NULL );
2053 	   assert( permvars != NULL );
2054 	   assert( npermvars > 0 );
2055 	   assert( perm != NULL );
2056 	
2057 	   if ( symtype != SYM_SYMTYPE_PERM && symtype != SYM_SYMTYPE_SIGNPERM )
2058 	   {
2059 	      *success = FALSE;
2060 	      return SCIP_OKAY;
2061 	   }
2062 	   assert( symtype == SYM_SYMTYPE_PERM || permvardomaincenter != NULL );
2063 	   assert( SCIPisTransformed(scip) );
2064 	
2065 	   /* resize component array if needed */
2066 	   if ( masterdata->nlexdatas == masterdata->maxnlexdatas )
2067 	   {
2068 	      int newsize;
2069 	
2070 	      newsize = SCIPcalcMemGrowSize(scip, masterdata->nlexdatas + 1);
2071 	      assert( newsize >= 0 );
2072 	
2073 	      if ( masterdata->nlexdatas == 0 )
2074 	      {
2075 	         SCIP_CALL( SCIPallocBlockMemoryArray(scip, &masterdata->lexdatas, newsize) );
2076 	      }
2077 	      else
2078 	      {
2079 	         SCIP_CALL( SCIPreallocBlockMemoryArray(scip, &masterdata->lexdatas,
2080 	            masterdata->maxnlexdatas, newsize) );
2081 	      }
2082 	
2083 	      masterdata->maxnlexdatas = newsize;
2084 	   }
2085 	
2086 	   /* prepare lexdatas */
2087 	   SCIP_CALL( lexdataCreate(scip, masterdata, &masterdata->lexdatas[masterdata->nlexdatas],
2088 	         permvars, npermvars, perm, symtype, permvardomaincenter, usedynamicorder, success) );
2089 	
2090 	   /* if not successfully added, undo increasing the counter */
2091 	   if ( *success )
2092 	      ++masterdata->nlexdatas;
2093 	
2094 	   return SCIP_OKAY;
2095 	}
2096 	
2097 	
2098 	/** resets lexicographic reduction propagation (removes all permutations) */
2099 	SCIP_RETCODE SCIPlexicographicReductionReset(
2100 	   SCIP*                 scip,               /**< SCIP data structure */
2101 	   SCIP_LEXREDDATA*      masterdata          /**< pointer to global data for lexicographic reduction propagator */
2102 	   )
2103 	{
2104 	   assert( scip != NULL );
2105 	   assert( masterdata != NULL );
2106 	   assert( (masterdata->lexdatas == NULL) == (masterdata->nlexdatas == 0) );
2107 	   assert( masterdata->nlexdatas >= 0 );
2108 	   assert( masterdata->nlexdatas <= masterdata->maxnlexdatas );
2109 	   assert( masterdata->shadowtreeeventhdlr != NULL );
2110 	
2111 	   while ( masterdata->nlexdatas > 0 )
2112 	   {
2113 	      SCIP_CALL( lexdataFree(scip, &(masterdata->lexdatas[--masterdata->nlexdatas])) );
2114 	   }
2115 	   assert( masterdata->nlexdatas == 0 );
2116 	
2117 	   SCIPfreeBlockMemoryArrayNull(scip, &masterdata->lexdatas, masterdata->maxnlexdatas);
2118 	   masterdata->lexdatas = NULL;
2119 	   masterdata->maxnlexdatas = 0;
2120 	
2121 	   assert( masterdata->nsymvars >= 0 );
2122 	   assert( (masterdata->symvarmap == NULL) == (masterdata->nsymvars == 0) );
2123 	   if ( masterdata->symvarmap != NULL )
2124 	   {
2125 	      SCIPhashmapFree(&masterdata->symvarmap);
2126 	      masterdata->symvarmap = NULL;
2127 	      masterdata->nsymvars = 0;
2128 	   }
2129 	
2130 	   masterdata->hasdynamicperm = FALSE;
2131 	
2132 	   return SCIP_OKAY;
2133 	}
2134 	
2135 	
2136 	/** frees lexicographic reduction data */
2137 	SCIP_RETCODE SCIPlexicographicReductionFree(
2138 	   SCIP*                 scip,               /**< SCIP data structure */
2139 	   SCIP_LEXREDDATA**     masterdata          /**< pointer to global data for lexicographic reduction propagator */
2140 	   )
2141 	{
2142 	   assert( scip != NULL );
2143 	   assert( masterdata != NULL );
2144 	   assert( *masterdata != NULL );
2145 	
2146 	   SCIP_CALL( SCIPlexicographicReductionReset(scip, *masterdata) );
2147 	   assert( (*masterdata)->lexdatas == NULL );
2148 	   assert( (*masterdata)->symvarmap == NULL );
2149 	
2150 	   SCIPfreeBlockMemory(scip, masterdata);
2151 	   return SCIP_OKAY;
2152 	}
2153 	
2154 	
2155 	/** initializes structures needed for lexicographic reduction propagation
2156 	 *
2157 	 *
2158 	 *  This is only done exactly once.
2159 	 */
2160 	SCIP_RETCODE SCIPincludeLexicographicReduction(
2161 	   SCIP*                 scip,               /**< SCIP data structure */
2162 	   SCIP_LEXREDDATA**     masterdata,         /**< pointer to global data for lexicographic reduction propagator */
2163 	   SCIP_EVENTHDLR*       shadowtreeeventhdlr /**< pointer to the shadow tree eventhdlr */
2164 	   )
2165 	{
2166 	   assert( scip != NULL );
2167 	   assert( masterdata != NULL );
2168 	   assert( shadowtreeeventhdlr != NULL );
2169 	
2170 	   SCIP_CALL( SCIPcheckStage(scip, "SCIPincludeLexicographicReduction", TRUE, TRUE, FALSE, FALSE, FALSE, FALSE, FALSE,
2171 	      FALSE, FALSE, FALSE, FALSE, FALSE, FALSE, FALSE) );
2172 	
2173 	   SCIP_CALL( SCIPallocBlockMemory(scip, masterdata) );
2174 	
2175 	   (*masterdata)->shadowtreeeventhdlr = shadowtreeeventhdlr;
2176 	   (*masterdata)->symvarmap = NULL;
2177 	   (*masterdata)->nsymvars = 0;
2178 	   (*masterdata)->lexdatas = NULL;
2179 	   (*masterdata)->nlexdatas = 0;
2180 	   (*masterdata)->maxnlexdatas = 0;
2181 	   (*masterdata)->nred = 0;
2182 	   (*masterdata)->ncutoff = 0;
2183 	   (*masterdata)->hasdynamicperm = FALSE;
2184 	   (*masterdata)->treewarninggiven = FALSE;
2185 	
2186 	   return SCIP_OKAY;
2187 	}
2188