cons_pseudoboolean.c

Go to the documentation of this file.

/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
/*                                                                           */
/*                  This file is part of the program and library             */
/*         SCIP --- Solving Constraint Integer Programs                      */
/*                                                                           */
/*  Copyright (c) 2002-2024 Zuse Institute Berlin (ZIB)                      */
/*                                                                           */
/*  Licensed under the Apache License, Version 2.0 (the "License");          */
/*  you may not use this file except in compliance with the License.         */
/*  You may obtain a copy of the License at                                  */
/*                                                                           */
/*      http://www.apache.org/licenses/LICENSE-2.0                           */
/*                                                                           */
/*  Unless required by applicable law or agreed to in writing, software      */
/*  distributed under the License is distributed on an "AS IS" BASIS,        */
/*  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. */
/*  See the License for the specific language governing permissions and      */
/*  limitations under the License.                                           */
/*                                                                           */
/*  You should have received a copy of the Apache-2.0 license                */
/*  along with SCIP; see the file LICENSE. If not visit scipopt.org.         */
/*                                                                           */
/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
 
/**@file   cons_pseudoboolean.c
 * @ingroup DEFPLUGINS_CONS
 * @brief  constraint handler for pseudo Boolean constraints
 * @author Gerald Gamrath
 * @author Stefan Heinz
 * @author Michael Winkler
 * @author Dominik Kamp
 *
 * The constraint handler deals with pseudo Boolean constraints. These are constraints of the form
 * \f[
 * \mbox{lhs} \leq \sum_{k=0}^m c_k \cdot x_k  +  \sum_{i=0}^n c_i \cdot \prod_{j \in I_i} x_j \leq \mbox{rhs}
 * \f]
 * where all x are binary and all c are integer
 *
 * @todo Add eventhandling.
 */
 
/*---+----1----+----2----+----3----+----4----+----5----+----6----+----7----+----8----+----9----+----0----+----1----+----2*/
 
#include "blockmemshell/memory.h"
#include "scip/cons_and.h"
#include "scip/cons_indicator.h"
#include "scip/cons_knapsack.h"
#include "scip/cons_linear.h"
#include "scip/cons_logicor.h"
#include "scip/cons_pseudoboolean.h"
#include "scip/cons_setppc.h"
#include "scip/cons_xor.h"
#include "scip/debug.h"
#include "scip/pub_cons.h"
#include "scip/pub_message.h"
#include "scip/pub_misc.h"
#include "scip/pub_misc_sort.h"
#include "scip/pub_var.h"
#include "scip/scip_cons.h"
#include "scip/scip_copy.h"
#include "scip/scip_general.h"
#include "scip/scip_mem.h"
#include "scip/scip_message.h"
#include "scip/scip_numerics.h"
#include "scip/scip_param.h"
#include "scip/scip_prob.h"
#include "scip/scip_sol.h"
#include "scip/scip_var.h"
#include "scip/symmetry_graph.h"
#include <string.h>
 
#ifdef WITHEQKNAPSACK
#include "scip/cons_eqknapsack.h"
#endif
 
/* constraint handler properties */
#define CONSHDLR_NAME          "pseudoboolean"
#define CONSHDLR_DESC          "constraint handler dealing with pseudo Boolean constraints"
#define CONSHDLR_ENFOPRIORITY  -1000000 /**< priority of the constraint handler for constraint enforcing */
#define CONSHDLR_CHECKPRIORITY -5000000 /**< priority of the constraint handler for checking feasibility */
#define CONSHDLR_EAGERFREQ          100 /**< frequency for using all instead of only the useful constraints in separation,
                                              *   propagation and enforcement, -1 for no eager evaluations, 0 for first only */
#define CONSHDLR_MAXPREROUNDS        -1 /**< maximal number of presolving rounds the constraint handler participates in (-1: no limit) */
#define CONSHDLR_NEEDSCONS         TRUE /**< should the constraint handler be skipped, if no constraints are available? */
 
#define CONSHDLR_PRESOLTIMING            SCIP_PRESOLTIMING_MEDIUM /**< presolving timing of the constraint handler (fast, medium, or exhaustive) */
 
#define DEFAULT_DECOMPOSENORMALPBCONS FALSE /**< decompose every normal pseudo boolean constraint into a "linear" constraint and "and" constraints */
#define DEFAULT_DECOMPOSEINDICATORPBCONS TRUE /**< decompose every soft pseudo boolean constraint into "indicator" constraints and "and" constraints */
 
#define DEFAULT_SEPARATENONLINEAR  TRUE /**< if decomposed, should the nonlinear constraints be separated during LP processing */
#define DEFAULT_PROPAGATENONLINEAR TRUE /**< if decomposed, should the nonlinear constraints be propagated during node processing */
#define DEFAULT_REMOVABLENONLINEAR TRUE /**< if decomposed, should the nonlinear constraints be removable */
#define NONLINCONSUPGD_PRIORITY   60000 /**< priority of upgrading nonlinear constraints */
 
/* remove this line to compile the upgrade from nonlinear to pseudoboolean constraints */
#undef NONLINCONSUPGD_PRIORITY  /*lint !e750*/
 
/*
 * Data structures
 */
#define HASHSIZE_PSEUDOBOOLEANNONLINEARTERMS 500 /**< minimal size of hash table in and constraint tables */
 
 
/* - create special linear(knapsack, setppc, logicor, (eqknapsack)) and and-constraints with check flags FALSE, to
 *   get smaller amount of locks on the term variables, do all presolving ...?! in these constraint handlers
 *
 * - do the checking here, lock and-resultants in both directions and all and-variables according to their
 *   coefficients and sides of the constraint,
 *   @note this only works if the and-resultant has no objective cofficient, otherwise we need to lock variables also in both directions
 *
 * - need to keep and constraint pointer for special propagations like if two ands are due to their variables in
 *   one clique, add this cliques of and-resultants
 *
 * - do special presolving like on instance :
 * check/IP/PseudoBoolean/normalized-PB07/OPT-SMALLINT-NLC/submittedPB07/manquinho/bsg/normalized-bsg_1000_25_1.opb.gz
 *
 *  there exist constraint like:        1 x1 x2 + 1 x1 x3 + 1 x1 x4 + 1 x1 x5 <= 1 ;
 *  which "equals" a linear constraint: 3 x1 + x2 + x3 + x4 + x5 <= 4 ;
 *
 *  in more general terms:                     1 x1 x2 x3 x4 + 1 x1 x2 x5 x6 x7 + 1 x1 x2 x8 x9 <= 1 ;
 *  which "equals" a pseudoboolean constraint: 2 x1 + 2 x2 + 1 x3 x4 + 1 x5 x6 x7 + 1 x8 x9 <= 5 ;
 *
 *  in an even more general terms:             5 x1 x2 x3 x4 + 1 x1 x2 x5 x6 x7 + 1 x1 x2 x8 x9 <= 6 ;
 *            equals(should the knapsack do)   1 x1 x2 x3 x4 + 1 x1 x2 x5 x6 x7 + 1 x1 x2 x8 x9 <= 2 ;
 *  which "equals" a pseudoboolean constraint: 2 x1 + 2 x2 + 1 x3 x4 + 1 x5 x6 x7 + 1 x8 x9 <= 6 ;
 *  (         without knapsack                 7 x1 + 7 x2 + 5 x3 x4 + 1 x5 x6 x7 + 1 x8 x9 <= 20 ; )
 *
 *  another special case :                     1 x1 x2 x3 + 1 x1 x2 x4 + 1 x5 x6 <= 1 ;
 *  which "equals" a pseudoboolean constraint: 2 x1 + 2 x2 + 1 x3 + 1 x4 + 1 x5 x6 <= 5 ;
 *  which "equals" a pseudoboolean constraint: 4 x1 + 4 x2 + 2 x3 + 2 x4 + 1 x5 + 1 x6 <= 10 ;
 *
 *  another special case :                     1 x1 x2 + 1 x1 x3 + 2 x4 x5 <= 3 ;
 *  which "equals" a pseudoboolean constraint: 2 x1 + 1 x2 + 1 x3 + 2 x4 x5 <= 5 ;
 *  which "equals" a pseudoboolean constraint: 2 x1 + 1 x2 + 1 x3 + 1 x4 + 1 x5 <= 5 ;
 */
/* @todo - in and-constraint better count nfixed zeros in both directions and maybe nfixedones for better propagation
 *
 *       - do better conflict analysis by choosing the earliest fixed variable which led to a conflict instead of maybe
 *         best coefficient or create more conflicts by using all to zero fixed variables one by one
 *
 *       - how to make sure that we aggregate in a right way, when aggregating a resultant and a "normal" variable,
 *         maybe add in SCIPaggregateVars a check for original variables, to prefer them if the variable type is the
 *         same; probably it would be better too if we would aggregate two resultants that the one with less variables
 *         inside the and-constraint will stay active
 *
 * @note since product resultants are artificial, we do not care for their solution value, but this can lead to fixation
 *       of the resultant not representing the product, in 'optimization mode' we do not care, but this might make
 *       solution debugging complicated
 */
 
/** and-constraint data object */
struct ConsAndData
{
   SCIP_CONS*            cons;                /**< pointer to the and-constraint of this 'term' of variables */
   SCIP_CONS*            origcons;            /**< pointer to the original and-constraint of this 'term' of variables
                                               *   only after problem was transformed, NULL otherwise */
   SCIP_VAR**            vars;                /**< all and-constraint variables */
   int                   nvars;               /**< number of all and-constraint variables */
   int                   svars;               /**< size for all and-constraint variables */
   SCIP_VAR**            newvars;             /**< new variables in this presolving round */
   int                   nnewvars;            /**< number of new variables in this presolving round */
   int                   snewvars;            /**< size of new variables in this presolving round */
   int                   noriguses;           /**< how often is this data in used by original constraints */
   int                   nuses;               /**< how often is this data in used by transformed constraints */
   unsigned int          istransformed:1;     /**< is transformed data active */
   unsigned int          isoriginal:1;        /**< is original data active */
};
typedef struct ConsAndData CONSANDDATA;
 
/** constraint data for pseudoboolean constraints */
struct SCIP_ConsData
{
   SCIP_Real             lhs;                /**< left hand side of constraint */
   SCIP_Real             rhs;                /**< right hand side of constraint */
 
   SCIP_CONS*            lincons;            /**< linear constraint which represents this pseudoboolean constraint */
   SCIP_LINEARCONSTYPE   linconstype;        /**< type of linear constraint which represents this pseudoboolean constraint */
   int                   nlinvars;           /**< number of linear variables (without and-resultants) */
 
   CONSANDDATA**         consanddatas;       /**< array of and-constraints-data-objects sorted after problem index of
                                              *   and-resultant of corresponding and-constraint */
   SCIP_Real*            andcoefs;           /**< array of coefficients for and-constraints of
                                              *   and-constraints-data-objects
                                              *   (changes during presolving, needs to be updated in every presolving
                                              *   round) */
   SCIP_Bool*            andnegs;            /**< array of negation status for and-constraints of
                                              *   and-constraints-data-objects
                                              *   (changes during presolving, needs to be updated in every presolving
                                              *   round) */
   int                   nconsanddatas;      /**< number of and-constraints-data-objects */
   int                   sconsanddatas;      /**< size of and-constraints-data-objects array */
 
   SCIP_VAR*             intvar;             /**< a artificial variable which was added only for the objective function,
                                              *   if this variable is not NULL this constraint (without this integer
                                              *   variable) describes the objective function */
 
   SCIP_VAR*             indvar;             /**< indicator variable if it's a soft constraint, or NULL */
   SCIP_Real             weight;             /**< weight of the soft constraint, if it is one */
 
   unsigned int          issoftcons:1;       /**< is this a soft constraint */
   unsigned int          changed:1;          /**< was constraint changed? */
   unsigned int          propagated:1;       /**< is constraint already propagated? */
   unsigned int          presolved:1;        /**< is constraint already presolved? */
   unsigned int          cliquesadded:1;     /**< were the cliques of the constraint already extracted? */
   unsigned int          upgradetried:1;     /**< was constraint upgrading already tried */
};
 
/** constraint handler data */
struct SCIP_ConshdlrData
{
   CONSANDDATA**         allconsanddatas;    /**< array of all and-constraint data objects inside the whole problem,
                                              *   created via this constraint handler */
   int                   nallconsanddatas;   /**< number of all and-constraint data objects inside the whole problem,
                                              *   created via this constraint handler */
   int                   sallconsanddatas;   /**< size of all and-constraint data objects inside the whole problem,
                                              *   created via this constraint handler */
   SCIP_HASHTABLE*       hashtable;          /**< hash table for all and-constraint data objects */
   int                   hashtablesize;      /**< size for hash table for all and-constraint data objects */
 
   SCIP_HASHMAP*         hashmap;            /**< hash map for mapping all resultant to and-constraint */
   int                   hashmapsize;        /**< size for hash map for mapping all resultant to and-constraint */
 
   SCIP_Bool             decomposenormalpbcons; /**< decompose every normal pseudo boolean constraint into a "linear" constraint and "and" constraints */
   SCIP_Bool             decomposeindicatorpbcons; /**< decompose every soft pseudo boolean constraint into "indicator" constraints and "and" constraints */
   SCIP_Bool             inithashmapandtable;/**< flag to store if the hashmap and -table is initialized */
   int                   nlinconss;          /**< for counting number of created linear constraints */
   int                   noriguses;          /**< how many consanddata objects are used by original constraints */
};
 
 
/*
 * Local methods
 */
 
/** comparison method for sorting and-resultants according to their problem index, which is used instead of the
 *  original index because the implicit resultants are shuffled when creating the constraints that otherwise results in
 *  shuffled problem copies,
 *  if an and-resultant is fixed, it will be put in front with respect to its original index
 *  if an and-resultant is negated, it will be put in front of its negation counterpart
 */
static
SCIP_DECL_SORTPTRCOMP(resvarComp)
{
   SCIP_VAR* var1 = elem1;
   SCIP_VAR* var2 = elem2;
   SCIP_Bool varneg1 = SCIPvarIsNegated(var1);
   SCIP_Bool varneg2 = SCIPvarIsNegated(var2);
 
   if( varneg1 )
      var1 = SCIPvarGetNegatedVar(var1);
 
   if( varneg2 )
      var2 = SCIPvarGetNegatedVar(var2);
 
   int varind1 = SCIPvarGetProbindex(var1);
   int varind2 = SCIPvarGetProbindex(var2);
 
   if( varind1 == -1 && varind2 == -1 )
   {
      varind1 = SCIPvarGetIndex(var1);
      varind2 = SCIPvarGetIndex(var2);
   }
 
   if( varind1 < varind2 )
      return -1;
   if( varind1 > varind2 )
      return +1;
 
   if( varneg1 && !varneg2 )
      return -1;
   if( !varneg1 && varneg2 )
      return +1;
 
   assert(elem1 == elem2);
   return 0;
}
 
/** comparison method for sorting consanddatas according to the problem index of their corresponding and-resultants,
 *  if a consanddata object is deleted, it is handled like it has an inactive resultant, so this will be put
 *  in front while sorting
 */
static
SCIP_DECL_SORTPTRCOMP(resvarCompWithInactive)
{
   CONSANDDATA* consanddata1 = (CONSANDDATA*)elem1;
   CONSANDDATA* consanddata2 = (CONSANDDATA*)elem2;
 
   assert(consanddata1 != NULL);
   assert(consanddata2 != NULL);
 
   /* consider that constraint data object can be only original */
   if( consanddata1->istransformed != consanddata2->istransformed )
      return consanddata1->istransformed ? +1 : -1;
 
   SCIP_CONS* consand1;
   SCIP_CONS* consand2;
 
   if( consanddata1->istransformed )
   {
      consand1 = consanddata1->cons;
      consand2 = consanddata2->cons;
   }
   else
   {
      consand1 = consanddata1->origcons;
      consand2 = consanddata2->origcons;
   }
 
   /* check if and-constraint is still active */
   if( SCIPconsIsDeleted(consand1) )
   {
      if( SCIPconsIsDeleted(consand2) )
         return 0;
      else
         return -1;
   }
   else if( SCIPconsIsDeleted(consand2) )
      return +1;
 
   /* hack with setting the scip pointer to NULL */
   return resvarComp((void*)SCIPgetResultantAnd(NULL, consand1), (void*)SCIPgetResultantAnd(NULL, consand2));
}
 
/** gets the key of the given element */
static
SCIP_DECL_HASHGETKEY(hashGetKeyAndConsDatas)
{  /*lint --e{715}*/
   /* the key is the element itself */
   return elem;
}
 
/** returns TRUE iff both keys are equal; two non-linear terms are equal if they have the same variables */
static
SCIP_DECL_HASHKEYEQ(hashKeyEqAndConsDatas)
{
#ifndef NDEBUG
   SCIP* scip;
#endif
   CONSANDDATA* cdata1;
   CONSANDDATA* cdata2;
   int v;
 
   cdata1 = (CONSANDDATA*)key1;
   cdata2 = (CONSANDDATA*)key2;
 
#ifndef NDEBUG
   scip = (SCIP*)userptr;
#endif
   assert(scip != NULL);
   assert(cdata1 != NULL);
   assert(cdata2 != NULL);
   assert(cdata1->vars != NULL);
   assert(cdata1->nvars > 1);
   assert(cdata2->vars != NULL);
   assert(cdata2->nvars > 1);
 
#ifndef NDEBUG
   /* check that cdata1 variables are sorted */
   for( v = cdata1->nvars - 1; v > 0; --v )
      assert(SCIPvarGetIndex(cdata1->vars[v]) >= SCIPvarGetIndex(cdata1->vars[v - 1]));
   /* check that cdata2 variables are sorted */
   for( v = cdata2->nvars - 1; v > 0; --v )
      assert(SCIPvarGetIndex(cdata2->vars[v]) >= SCIPvarGetIndex(cdata2->vars[v - 1]));
#endif
 
   /* checks trivial case */
   if( cdata1->nvars != cdata2->nvars )
      return FALSE;
 
   /* checks trivial case */
   if( cdata1->cons != NULL && cdata2->cons != NULL && cdata1->cons != cdata2->cons )
      return FALSE;
 
   /* check each variable in both cdatas for equality */
   for( v = cdata1->nvars - 1; v >= 0; --v )
   {
      assert(cdata1->vars[v] != NULL);
      assert(cdata2->vars[v] != NULL);
 
      /* tests if variables are equal */
      if( cdata1->vars[v] != cdata2->vars[v] )
      {
         assert(SCIPvarCompare(cdata1->vars[v], cdata2->vars[v]) == 1 ||
            SCIPvarCompare(cdata1->vars[v], cdata2->vars[v]) == -1);
         return FALSE;
      }
      assert(SCIPvarCompare(cdata1->vars[v], cdata2->vars[v]) == 0);
   }
 
   return TRUE;
}
 
/** returns the hash value of the key */
static
SCIP_DECL_HASHKEYVAL(hashKeyValAndConsDatas)
{  /*lint --e{715}*/
   CONSANDDATA* cdata;
   int minidx;
   int mididx;
   int maxidx;
 
   cdata = (CONSANDDATA*)key;
 
   assert(cdata != NULL);
   assert(cdata->vars != NULL);
   assert(cdata->nvars > 1);
#ifndef NDEBUG
   {
      /* check that these variables are sorted */
      int v;
      for( v = cdata->nvars - 1; v > 0; --v )
         assert(SCIPvarGetIndex(cdata->vars[v]) >= SCIPvarGetIndex(cdata->vars[v - 1]));
   }
#endif
 
   minidx = SCIPvarGetIndex(cdata->vars[0]);
   mididx = SCIPvarGetIndex(cdata->vars[cdata->nvars / 2]);
   maxidx = SCIPvarGetIndex(cdata->vars[cdata->nvars - 1]);
   assert(minidx >= 0 && minidx <= maxidx);
 
   return SCIPhashFour(cdata->nvars, minidx, mididx, maxidx);
}
 
/** initializes the hashmap and -table used in this constraint handler data for artificial variables and specific
 *  and-constraint data objects
 */
static
SCIP_RETCODE inithashmapandtable(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONSHDLRDATA**   conshdlrdata        /**< pointer to store the constraint handler data */
   )
{
   if( ((*conshdlrdata)->inithashmapandtable) )
   {
      assert((*conshdlrdata)->hashtable != NULL);
      assert((*conshdlrdata)->hashmap != NULL);
 
      return SCIP_OKAY;
   }
 
   assert((*conshdlrdata)->hashtable == NULL);
   assert((*conshdlrdata)->hashmap == NULL);
 
   /* create a hash table for and-constraint data objects */
   (*conshdlrdata)->hashtablesize = HASHSIZE_PSEUDOBOOLEANNONLINEARTERMS;
   SCIP_CALL( SCIPhashtableCreate(&((*conshdlrdata)->hashtable), SCIPblkmem(scip), (*conshdlrdata)->hashtablesize,
         hashGetKeyAndConsDatas, hashKeyEqAndConsDatas, hashKeyValAndConsDatas, (void*) scip) );
 
   /* create a hash table for and-resultant to and-constraint data objects */
   (*conshdlrdata)->hashmapsize = HASHSIZE_PSEUDOBOOLEANNONLINEARTERMS;
   SCIP_CALL( SCIPhashmapCreate(&((*conshdlrdata)->hashmap), SCIPblkmem(scip), (*conshdlrdata)->hashmapsize) );
 
   (*conshdlrdata)->inithashmapandtable = TRUE;
 
   return SCIP_OKAY;
}
 
/** creates constraint handler data for pseudo boolean constraint handler */
static
SCIP_RETCODE conshdlrdataCreate(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONSHDLRDATA**   conshdlrdata        /**< pointer to store the constraint handler data */
   )
{
   assert(scip != NULL);
   assert(conshdlrdata != NULL);
 
   SCIP_CALL( SCIPallocBlockMemory(scip, conshdlrdata) );
 
   (*conshdlrdata)->allconsanddatas = NULL;
   (*conshdlrdata)->nallconsanddatas = 0;
   (*conshdlrdata)->sallconsanddatas = 10;
 
   SCIP_CALL( SCIPallocBlockMemoryArray(scip, &((*conshdlrdata)->allconsanddatas), (*conshdlrdata)->sallconsanddatas ) );
 
   /* set hashmap and -table to NULL, mark them as uninitialized */
   (*conshdlrdata)->inithashmapandtable = FALSE;
   (*conshdlrdata)->hashtable = NULL;
   (*conshdlrdata)->hashtablesize = 0;
   (*conshdlrdata)->hashmap = NULL;
   (*conshdlrdata)->hashmapsize = 0;
 
   /* for constraint names count number of created constraints */
   (*conshdlrdata)->nlinconss = 0;
 
   /* initializes how many consanddata objects are used by original constraints */
   (*conshdlrdata)->noriguses = 0;
 
   return SCIP_OKAY;
}
 
 
/** frees constraint handler data for pseudo boolean constraint handler */
static
SCIP_RETCODE conshdlrdataFree(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONSHDLRDATA**   conshdlrdata        /**< pointer to the constraint handler data */
   )
{
   assert(scip != NULL);
   assert(conshdlrdata != NULL);
   assert(*conshdlrdata != NULL);
   assert((*conshdlrdata)->nallconsanddatas == 0);
 
   /* free hash table if necessary */
   if( (*conshdlrdata)->inithashmapandtable )
   {
      SCIPhashmapFree(&((*conshdlrdata)->hashmap));
      (*conshdlrdata)->hashmapsize = 0;
      SCIPhashtableFree(&((*conshdlrdata)->hashtable));
      (*conshdlrdata)->hashtablesize = 0;
   }
   else
   {
      assert((*conshdlrdata)->hashmap == NULL);
      assert((*conshdlrdata)->hashtable == NULL);
   }
   (*conshdlrdata)->inithashmapandtable = FALSE;
 
   /* clear array for all consanddata objects */
   SCIPfreeBlockMemoryArray(scip, &((*conshdlrdata)->allconsanddatas), (*conshdlrdata)->sallconsanddatas );
 
   (*conshdlrdata)->allconsanddatas = NULL;
   (*conshdlrdata)->nallconsanddatas = 0;
   (*conshdlrdata)->sallconsanddatas = 0;
 
   SCIPfreeBlockMemory(scip, conshdlrdata);
 
   return SCIP_OKAY;
}
 
/** gets number of variables in linear constraint */
static
SCIP_RETCODE getLinearConsNVars(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< linear constraint */
   SCIP_LINEARCONSTYPE const constype,       /**< linear constraint type */
   int*const             nvars               /**< pointer to store number variables of linear constraint */
   )
{
   assert(scip != NULL);
   assert(cons != NULL);
   assert(nvars != NULL);
 
   /* determine for each special linear constranit all variables and coefficients */
   switch( constype )
   {
   case SCIP_LINEARCONSTYPE_LINEAR:
      *nvars = SCIPgetNVarsLinear(scip, cons);
      break;
   case SCIP_LINEARCONSTYPE_LOGICOR:
      *nvars = SCIPgetNVarsLogicor(scip, cons);
      break;
   case SCIP_LINEARCONSTYPE_KNAPSACK:
      *nvars = SCIPgetNVarsKnapsack(scip, cons);
      break;
   case SCIP_LINEARCONSTYPE_SETPPC:
      *nvars = SCIPgetNVarsSetppc(scip, cons);
      break;
#ifdef WITHEQKNAPSACK
   case SCIP_LINEARCONSTYPE_EQKNAPSACK:
      *nvars = SCIPgetNVarsEQKnapsack(scip, cons);
      break;
#endif
   case SCIP_LINEARCONSTYPE_INVALIDCONS:
   default:
      SCIPerrorMessage("unknown linear constraint type\n");
      return SCIP_INVALIDDATA;
   }
 
   return SCIP_OKAY;
}
 
 
/** gets sides of linear constraint */
static
SCIP_RETCODE getLinearConsSides(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< linear constraint */
   SCIP_LINEARCONSTYPE const constype,       /**< linear constraint type */
   SCIP_Real*const       lhs,                /**< pointer to store left hand side of linear constraint */
   SCIP_Real*const       rhs                 /**< pointer to store right hand side of linear constraint */
   )
{
   SCIP_SETPPCTYPE type;
 
   switch( constype )
   {
   case SCIP_LINEARCONSTYPE_LINEAR:
      *lhs = SCIPgetLhsLinear(scip, cons);
      *rhs = SCIPgetRhsLinear(scip, cons);
      break;
   case SCIP_LINEARCONSTYPE_LOGICOR:
      *lhs = 1.0;
      *rhs = SCIPinfinity(scip);
      break;
   case SCIP_LINEARCONSTYPE_KNAPSACK:
      *lhs = -SCIPinfinity(scip);
      *rhs = SCIPgetCapacityKnapsack(scip, cons);
      break;
   case SCIP_LINEARCONSTYPE_SETPPC:
      type = SCIPgetTypeSetppc(scip, cons);
 
      switch( type )
      {
      case SCIP_SETPPCTYPE_PARTITIONING:
         *lhs = 1.0;
         *rhs = 1.0;
         break;
      case SCIP_SETPPCTYPE_PACKING:
         *lhs = -SCIPinfinity(scip);
         *rhs = 1.0;
         break;
      case SCIP_SETPPCTYPE_COVERING:
         *lhs = 1.0;
         *rhs = SCIPinfinity(scip);
         break;
      default:
         SCIPerrorMessage("unknown setppc type\n");
         return SCIP_INVALIDDATA;
      }
      break;
#ifdef WITHEQKNAPSACK
   case SCIP_LINEARCONSTYPE_EQKNAPSACK:
      *lhs = SCIPgetCapacityEQKnapsack(scip, cons);
      *rhs = *lhs;
      break;
#endif
   case SCIP_LINEARCONSTYPE_INVALIDCONS:
   default:
      SCIPerrorMessage("unknown linear constraint type\n");
      return SCIP_INVALIDDATA;
   }
 
   return SCIP_OKAY;
}
 
/** gets variables and coefficients of linear constraint */
static
SCIP_RETCODE getLinearConsVarsData(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< linear constraint */
   SCIP_LINEARCONSTYPE const constype,       /**< linear constraint type */
   SCIP_VAR**const       vars,               /**< array to store variables of linear constraint */
   SCIP_Real*const       coefs,              /**< array to store coefficient of linear constraint, or NULL */
   int*const             nvars               /**< pointer to store number variables of linear constraint */
   )
{
   SCIP_VAR** linvars;
   int v;
 
   assert(scip != NULL);
   assert(cons != NULL);
   assert(vars != NULL);
   assert(nvars != NULL);
 
   /* determine for each special linear constrait all variables and coefficients */
   switch( constype )
   {
   case SCIP_LINEARCONSTYPE_LINEAR:
   {
      SCIP_Real* lincoefs;
 
      *nvars = SCIPgetNVarsLinear(scip, cons);
      linvars = SCIPgetVarsLinear(scip, cons);
 
      if( coefs != NULL )
      {
         lincoefs = SCIPgetValsLinear(scip, cons);
 
         for( v = 0; v < *nvars; ++v )
         {
            vars[v] = linvars[v];
            coefs[v] = lincoefs[v];
         }
      }
      else
      {
         for( v = 0; v < *nvars; ++v )
            vars[v] = linvars[v];
      }
 
      break;
   }
   case SCIP_LINEARCONSTYPE_LOGICOR:
      *nvars = SCIPgetNVarsLogicor(scip, cons);
      linvars = SCIPgetVarsLogicor(scip, cons);
      assert( linvars != NULL );
 
      if( coefs != NULL )
      {
         for( v = 0; v < *nvars; ++v )
         {
            vars[v] = linvars[v];
            coefs[v] = 1.0;
         }
      }
      else
      {
         for( v = 0; v < *nvars; ++v )
            vars[v] = linvars[v];
      }
 
      break;
   case SCIP_LINEARCONSTYPE_KNAPSACK:
   {
      SCIP_Longint* weights;
 
      *nvars = SCIPgetNVarsKnapsack(scip, cons);
      linvars = SCIPgetVarsKnapsack(scip, cons);
      assert( linvars != NULL );
 
      if( coefs != NULL )
      {
         weights = SCIPgetWeightsKnapsack(scip, cons);
 
         for( v = 0; v < *nvars; ++v )
         {
            vars[v] = linvars[v];
            coefs[v] = (SCIP_Real) weights[v];
         }
      }
      else
      {
         for( v = 0; v < *nvars; ++v )
            vars[v] = linvars[v];
      }
 
      break;
   }
   case SCIP_LINEARCONSTYPE_SETPPC:
      *nvars = SCIPgetNVarsSetppc(scip, cons);
      linvars = SCIPgetVarsSetppc(scip, cons);
      assert( linvars != NULL );
 
      if( coefs != NULL )
      {
         for( v = 0; v < *nvars; ++v )
         {
            vars[v] = linvars[v];
            coefs[v] = 1.0;
         }
      }
      else
      {
         for( v = 0; v < *nvars; ++v )
            vars[v] = linvars[v];
      }
 
      break;
#ifdef WITHEQKNAPSACK
   case SCIP_LINEARCONSTYPE_EQKNAPSACK:
   {
      SCIP_Longint* weights;
 
      *nvars = SCIPgetNVarsEQKnapsack(scip, cons);
      linvars = SCIPgetVarsEQKnapsack(scip, cons);
      assert( linvars != NULL );
 
      if( coefs != NULL )
      {
         weights = SCIPgetWeightsEQKnapsack(scip, cons);
 
         for( v = 0; v < *nvars; ++v )
         {
            vars[v] = linvars[v];
            coefs[v] = (SCIP_Real) weights[v];
         }
      }
      else
      {
         for( v = 0; v < *nvars; ++v )
            vars[v] = linvars[v];
      }
 
      break;
   }
#endif
   case SCIP_LINEARCONSTYPE_INVALIDCONS:
   default:
      SCIPerrorMessage("unknown linear constraint type\n");
      return SCIP_INVALIDDATA;
   }
 
   return SCIP_OKAY;
}
 
/** splits up into original linear variables and artificial and-resultants */
static
SCIP_RETCODE getLinVarsAndAndRess(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< pseudoboolean constraint */
   SCIP_VAR**const       vars,               /**< all variables of linear constraint */
   SCIP_Real*const       coefs,              /**< all coefficients of linear constraint, or NULL */
   int const             nvars,              /**< number of all variables of linear constraint */
   SCIP_VAR**const       linvars,            /**< array to store not and-resultant variables of linear constraint, or NULL */
   SCIP_Real*const       lincoefs,           /**< array to store coefficients of not and-resultant variables of linear
                                              *   constraint, or NULL */
   int*const             nlinvars,           /**< pointer to store number of not and-resultant variables, or NULL */
   SCIP_VAR**const       andress,            /**< array to store and-resultant variables of linear constraint, or NULL */
   SCIP_Real*const       andcoefs,           /**< array to store coefficients of and-resultant variables of linear
                                              *   constraint, or NULL */
   SCIP_Bool*const       andnegs,            /**< array to store negation status of and-resultant variables of linear
                                              *   constraint, or NULL */
   int*const             nandress            /**< pointer to store number of and-resultant variables, or NULL */
   )
{
   SCIP_CONSHDLR* conshdlr;
   SCIP_CONSHDLRDATA* conshdlrdata;
   int v;
 
   assert(scip != NULL);
   assert(cons != NULL);
   assert(vars != NULL);
   assert((linvars != NULL) == (nlinvars != NULL));
   assert((andress == NULL) || (nandress != NULL));
   assert((andcoefs != NULL) == (andnegs != NULL));
   assert((coefs != NULL) == ((lincoefs != NULL) || (andcoefs != NULL)));
   assert(linvars != NULL || andress != NULL);
 
   if( nlinvars != NULL )
      *nlinvars = 0;
   if( nandress != NULL )
      *nandress = 0;
 
   conshdlr = SCIPconsGetHdlr(cons);
   assert(conshdlr != NULL);
   conshdlrdata = SCIPconshdlrGetData(conshdlr);
   assert(conshdlrdata != NULL);
   assert(conshdlrdata->hashmap != NULL);
 
   /* split variables into original and artificial variables */
   for( v = 0; v < nvars; ++v )
   {
      SCIP_Bool hashmapentryexists;
      SCIP_VAR* hashmapvar;
 
      assert(vars[v] != NULL);
 
      hashmapentryexists = SCIPhashmapExists(conshdlrdata->hashmap, (void*)(vars[v]));
 
      if( !hashmapentryexists && SCIPvarIsNegated(vars[v]) )
      {
         hashmapvar = SCIPvarGetNegationVar(vars[v]);
         hashmapentryexists = SCIPhashmapExists(conshdlrdata->hashmap, (void*)(hashmapvar));
      }
      else
         hashmapvar = vars[v];
 
      /* if and resultant is not a resultant anymore (meaning the corresponding and-constraint was deleted/upgraded),
       * correct the flag and count this variable as normal linear variable
       */
      if( hashmapentryexists )
      {
         if( !SCIPconsIsOriginal(cons) )
         {
            CONSANDDATA* consanddata = (CONSANDDATA*) SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)(hashmapvar));
            assert(consanddata != NULL);
 
            hashmapentryexists = (consanddata->istransformed);
 
            if( hashmapentryexists )
            {
               assert(consanddata->cons != NULL);
               hashmapentryexists = !SCIPconsIsDeleted(consanddata->cons);
            }
         }
      }
 
      if( !hashmapentryexists && linvars != NULL && nlinvars != NULL )
      {
         linvars[*nlinvars] = vars[v];
         if( lincoefs != NULL )
         {
            assert(coefs != NULL);
            lincoefs[*nlinvars] = coefs[v];
         }
         ++(*nlinvars);
      }
      else if( hashmapentryexists && nandress != NULL )
      {
         if( andress != NULL )
         {
            andress[*nandress] = hashmapvar;
 
            if( andcoefs != NULL )
            {
               assert(andnegs != NULL);
               assert(coefs != NULL);
               andcoefs[*nandress] = coefs[v];
               andnegs[*nandress] = (vars[v] != hashmapvar);
            }
         }
         ++(*nandress);
      }
   }
 
   return SCIP_OKAY;
}
 
 
#ifdef CHECK_CONSISTENCY
/** check constraint consistency */
static
void checkConsConsistency(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons                /**< pseudoboolean constraint */
   )
{
   SCIP_CONSDATA* consdata;
   SCIP_VAR** vars;
   SCIP_Real* coefs;
   int nvars;
   SCIP_VAR** linvars;
   SCIP_Real* lincoefs;
   int nlinvars;
   SCIP_VAR** andress;
   SCIP_Real* andcoefs;
   SCIP_Bool* andnegs;
   int nandress;
   SCIP_Bool* alreadyfound;
   SCIP_VAR* res;
   int c;
   int v;
   SCIP_Real newlhs;
   SCIP_Real newrhs;
 
   assert(scip != NULL);
   assert(cons != NULL);
 
   if( SCIPgetStage(scip) == SCIP_STAGE_FREETRANS )
      return;
 
   consdata = SCIPconsGetData(cons);
   assert(consdata != NULL);
 
   /* check standard pointers and sizes */
   assert(consdata->lincons != NULL);
   assert(!SCIPconsIsDeleted(consdata->lincons));
   assert(consdata->linconstype > SCIP_LINEARCONSTYPE_INVALIDCONS);
   assert(consdata->consanddatas != NULL);
   assert(consdata->nconsanddatas > 0);
   assert(consdata->nconsanddatas <= consdata->sconsanddatas);
 
   /* get sides of linear constraint */
   SCIP_CALL_ABORT( getLinearConsSides(scip, consdata->lincons, consdata->linconstype, &newlhs, &newrhs) );
   assert(!SCIPisInfinity(scip, newlhs));
   assert(!SCIPisInfinity(scip, -newrhs));
   assert(SCIPisLE(scip, newlhs, newrhs));
   assert(SCIPisEQ(scip, newrhs, consdata->rhs) || SCIPisEQ(scip, newrhs, -consdata->lhs));
   assert(SCIPisEQ(scip, newlhs, consdata->lhs) || SCIPisEQ(scip, newlhs, -consdata->rhs));
 
   /* check number of linear variables */
   SCIP_CALL_ABORT( getLinearConsNVars(scip, consdata->lincons, consdata->linconstype, &nvars) );
   assert(nvars == consdata->nlinvars + consdata->nconsanddatas);
 
   /* get temporary memory */
   SCIP_CALL_ABORT( SCIPallocBufferArray(scip, &vars, nvars) );
   SCIP_CALL_ABORT( SCIPallocBufferArray(scip, &coefs, nvars) );
   SCIP_CALL_ABORT( SCIPallocBufferArray(scip, &linvars, nvars) );
   SCIP_CALL_ABORT( SCIPallocBufferArray(scip, &lincoefs, nvars) );
   SCIP_CALL_ABORT( SCIPallocBufferArray(scip, &andress, nvars) );
   SCIP_CALL_ABORT( SCIPallocBufferArray(scip, &andcoefs, nvars) );
   SCIP_CALL_ABORT( SCIPallocBufferArray(scip, &andnegs, nvars) );
   SCIP_CALL_ABORT( SCIPallocClearBufferArray(scip, &alreadyfound, nvars) );
 
   /* get variables and coefficients */
   SCIP_CALL_ABORT( getLinearConsVarsData(scip, consdata->lincons, consdata->linconstype, vars, coefs, &nvars) );
   assert(nvars == 0 || (coefs != NULL));
 
   /* calculate all not artificial linear variables and all artificial and-resultants */
   SCIP_CALL_ABORT( getLinVarsAndAndRess(scip, cons, vars, coefs, nvars, linvars, lincoefs, &nlinvars,
         andress, andcoefs, andnegs, &nandress) );
   assert(nlinvars == consdata->nlinvars);
   assert(nandress == consdata->nconsanddatas);
 
   for( v = nandress - 1; v >= 0; --v )
   {
      SCIP_VAR* andresultant = andress[v];
      int nfound = 0;
 
      for( c = consdata->nconsanddatas - 1; c >= 0; --c )
      {
         assert(consdata->consanddatas[c] != NULL);
         if( consdata->consanddatas[c]->cons != NULL )
         {
            res = SCIPgetResultantAnd(scip, consdata->consanddatas[c]->cons);
            assert(res != NULL);
 
            if( res == andresultant && consdata->andnegs[c] == andnegs[v] && consdata->andcoefs[c] == andcoefs[v] )
            {
               /* resultant should be either active or a negated variable of an active one */
               assert(SCIPvarIsActive(res) || (SCIPvarIsNegated(res) && SCIPvarIsActive(SCIPvarGetNegationVar(res))));
               assert(!alreadyfound[c]);
 
               /* all and-resultants should be merged, so it is only allowed that each variable exists one time */
               alreadyfound[c] = TRUE;
               ++nfound;
               break;
            }
         }
      }
      assert(nfound == 1);
   }
 
   for( c = consdata->nconsanddatas - 1; c >= 0; --c )
   {
      assert(alreadyfound[c]);
   }
 
   /* free temporary memory */
   SCIPfreeBufferArray(scip, &alreadyfound);
   SCIPfreeBufferArray(scip, &andnegs);
   SCIPfreeBufferArray(scip, &andcoefs);
   SCIPfreeBufferArray(scip, &andress);
   SCIPfreeBufferArray(scip, &lincoefs);
   SCIPfreeBufferArray(scip, &linvars);
   SCIPfreeBufferArray(scip, &coefs);
   SCIPfreeBufferArray(scip, &vars);
}
#else
#define checkConsConsistency(scip, cons) /**/
#endif
 
 
/** transforming transformed consanddata object back to original space, if an corresponding original constraint exists,
 *  also clearing all transformed data, i.e. releasing transformed variables
 */
static
SCIP_RETCODE transformToOrig(
   SCIP*const            scip,               /**< SCIP data structure */
   CONSANDDATA*          consanddata,        /**< consanddata object */
   SCIP_CONSHDLRDATA*    conshdlrdata        /**< constraint handler data */
   )
{
   SCIP_VAR** tmpvars;
   SCIP_Bool origdata;
   int ntmpvars;
   int v;
 
   assert(scip != NULL);
   assert(consanddata != NULL);
   assert(conshdlrdata != NULL);
 
   origdata = TRUE;
 
   tmpvars = consanddata->vars;
   ntmpvars = consanddata->nvars;
 
   /* release all transformed variables */
   for( v = ntmpvars - 1; v >= 0; --v )
   {
      assert(tmpvars[v] != NULL);
      if( SCIPvarIsTransformed(tmpvars[v]) )
      {
         SCIP_CALL( SCIPreleaseVar(scip, &tmpvars[v]) );
         origdata = FALSE;
      }
   }
 
   tmpvars = consanddata->newvars;
   ntmpvars = consanddata->nnewvars;
 
   /* release all variables */
   for( v = ntmpvars - 1; v >= 0; --v )
   {
      assert(tmpvars[v] != NULL);
      if( SCIPvarIsTransformed(tmpvars[v]) )
      {
         SCIP_CALL( SCIPreleaseVar(scip, &tmpvars[v]) );
         origdata = FALSE;
      }
   }
 
   /* reinstall original data */
   if( !origdata || consanddata->nvars == 0 )
   {
      SCIPfreeBlockMemoryArrayNull(scip, &(consanddata->vars), consanddata->svars);
      SCIPfreeBlockMemoryArrayNull(scip, &(consanddata->newvars), consanddata->snewvars);
 
      consanddata->nuses = 0;
      consanddata->nvars = 0;
      consanddata->svars = 0;
      consanddata->nnewvars = 0;
      consanddata->snewvars = 0;
      consanddata->istransformed = FALSE;
 
      if( consanddata->noriguses > 0 )
      {
         assert(consanddata->origcons != NULL);
         assert(consanddata->isoriginal);
 
         assert(SCIPgetNVarsAnd(scip, consanddata->origcons) > 0);
         assert(SCIPgetVarsAnd(scip, consanddata->origcons) != NULL);
         consanddata->nvars = SCIPgetNVarsAnd(scip, consanddata->origcons);
         consanddata->svars = consanddata->nvars;
 
         if( consanddata->nvars > 0 )
         {
            SCIP_VAR** andvars = SCIPgetVarsAnd(scip, consanddata->origcons);
 
            SCIP_CALL( SCIPduplicateBlockMemoryArray(scip, &(consanddata->vars), andvars, consanddata->nvars) );
 
            /* sort variables */
            SCIPsortPtr((void**)(consanddata->vars), SCIPvarComp, consanddata->nvars);
         }
 
         /* check that the hash map and tabkle are still having all information */
         if( conshdlrdata->inithashmapandtable )
         {
            assert(conshdlrdata->hashmap != NULL);
            assert(conshdlrdata->hashtable != NULL);
            assert(SCIPgetResultantAnd(scip, consanddata->origcons) != NULL);
            assert(SCIPhashtableExists(conshdlrdata->hashtable, (void*)consanddata));
            assert(consanddata == (CONSANDDATA*)(SCIPhashtableRetrieve(conshdlrdata->hashtable, (void*)consanddata)));
            assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddata->origcons)));
            assert(consanddata == (CONSANDDATA*)(SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddata->origcons))));
         }
      }
      else
         assert(consanddata->origcons == NULL);
   }
   else
   {
      assert(consanddata->nuses == 0);
      assert(consanddata->nnewvars == 0);
      assert(consanddata->snewvars == 0);
      assert(consanddata->newvars == NULL);
 
      consanddata->istransformed = FALSE;
 
      if( consanddata->noriguses > 0 )
      {
         assert(consanddata->origcons != NULL);
         assert(consanddata->nvars > 0);
         assert(consanddata->svars > 0);
         assert(consanddata->vars != NULL);
         assert(consanddata->isoriginal);
 
         /* check that the hash map and tabkle are still having all information */
         if( conshdlrdata->inithashmapandtable )
         {
            assert(conshdlrdata->hashmap != NULL);
            assert(conshdlrdata->hashtable != NULL);
            assert(SCIPgetResultantAnd(scip, consanddata->origcons) != NULL);
            assert(SCIPhashtableExists(conshdlrdata->hashtable, (void*)consanddata));
            assert(consanddata == (CONSANDDATA*)(SCIPhashtableRetrieve(conshdlrdata->hashtable, (void*)consanddata)));
            assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddata->origcons)));
            assert(consanddata == (CONSANDDATA*)(SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddata->origcons))));
         }
      }
   }
 
   return SCIP_OKAY;
}
 
 
 
/** creates a pseudo boolean constraint data */
static
SCIP_RETCODE consdataCreate(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONSHDLR*const   conshdlr,           /**< pseudoboolean constraint handler */
   SCIP_CONSDATA**       consdata,           /**< pointer to linear constraint data */
   SCIP_CONS*const       lincons,            /**< linear constraint with artificial and-resultants representing this pseudoboolean constraint */
   SCIP_LINEARCONSTYPE const linconstype,    /**< type of linear constraint */
   SCIP_CONS**const      andconss,           /**< array of and-constraints which occur in this pseudoboolean constraint */
   SCIP_Real*const       andcoefs,           /**< coefficients of and-constraints */
   SCIP_Bool*const       andnegs,            /**< negation status of and-constraints (or NULL, if no negated resultants) */
   int const             nandconss,          /**< number of and-constraints */
   SCIP_VAR*const        indvar,             /**< indicator variable if it's a soft constraint, or NULL */
   SCIP_Real const       weight,             /**< weight of the soft constraint, if it is one */
   SCIP_Bool const       issoftcons,         /**< is this a soft constraint */
   SCIP_VAR* const       intvar,             /**< a artificial variable which was added only for the objective function,
                                              *   if this variable is not NULL this constraint (without this integer
                                              *   variable) describes the objective function */
   SCIP_Real             lhs,                /**< left hand side of row */
   SCIP_Real             rhs,                /**< right hand side of row */
   SCIP_Bool             check,              /**< is the new constraint a check constraint? */
   SCIP_Bool             transforming        /**< are we called by CONSTRANS */
   )
{
   SCIP_Bool transformed;
   int nvars;
 
   assert(scip != NULL);
   assert(conshdlr != NULL);
   assert(consdata != NULL);
   assert(lincons != NULL && linconstype > SCIP_LINEARCONSTYPE_INVALIDCONS);
   assert(nandconss == 0 || (andconss != NULL && andcoefs != NULL));
   assert(!issoftcons || (!SCIPisZero(scip, weight) && indvar != NULL));
 
   /* adjust right hand side */
   if( SCIPisInfinity(scip, rhs) )
      rhs = SCIPinfinity(scip);
   else if( SCIPisInfinity(scip, -rhs) )
      rhs = -SCIPinfinity(scip);
 
   /* adjust left hand side */
   if( SCIPisInfinity(scip, -lhs) )
      lhs = -SCIPinfinity(scip);
   else if( SCIPisInfinity(scip, lhs) )
      lhs = SCIPinfinity(scip);
 
   /* check left and right side */
   if( SCIPisGT(scip, lhs, rhs) )
   {
      SCIPerrorMessage("left hand side of pseudo boolean constraint greater than right hand side\n");
      SCIPerrorMessage(" -> lhs=%g, rhs=%g\n", lhs, rhs);
      return SCIP_INVALIDDATA;
   }
 
   transformed = SCIPisTransformed(scip);
 
   /* allocate memory for the constraint data */
   SCIP_CALL( SCIPallocBlockMemory(scip, consdata) );
 
   /* initialize the weights for soft constraints */
   (*consdata)->issoftcons = issoftcons;
   if( issoftcons )
   {
      (*consdata)->weight = weight;
      if( transformed )
      {
         SCIP_CALL( SCIPgetTransformedVar(scip, indvar, &((*consdata)->indvar)) );
      }
      else
         (*consdata)->indvar = indvar;
   }
   else
      (*consdata)->indvar = NULL;
 
   /* copy artificial integer variable if it exist */
   if( intvar != NULL )
   {
      if( transformed )
      {
         SCIP_CALL( SCIPgetTransformedVar(scip, intvar, &((*consdata)->intvar)) );
      }
      else
         (*consdata)->intvar = intvar;
   }
   else
      (*consdata)->intvar = NULL;
 
   /* copy linear constraint */
   (*consdata)->lincons = lincons;
   (*consdata)->linconstype = linconstype;
 
   /* get transformed linear constraint and capture it if necessary */
   if( transforming )
   {
      /* do not capture the and constraint when scip is in transformed mode; this automatically happens in
       * SCIPtransformCons()
       */
      SCIP_CALL( SCIPtransformCons(scip, (*consdata)->lincons, &((*consdata)->lincons)) );
      assert((*consdata)->lincons != NULL);
   }
 
   if( transforming || transformed )
   {
      assert(SCIPconsIsTransformed((*consdata)->lincons));
 
      /* we want to check all necessary transformed linear constraints */
      SCIP_CALL( SCIPsetConsChecked(scip, (*consdata)->lincons, check) );
   }
 
   /* get number of non-linear terms in pseudoboolean constraint */
   SCIP_CALL( getLinearConsNVars(scip, (*consdata)->lincons, (*consdata)->linconstype, &nvars) );
   (*consdata)->nlinvars = nvars - nandconss;
 
   /* copy and-constraints */
   if( nandconss > 0 )
   {
      SCIP_CONSHDLRDATA* conshdlrdata;
      SCIP_VAR** andress;
      int c;
 
      SCIP_CALL( SCIPallocBlockMemoryArray(scip, &((*consdata)->consanddatas), nandconss) );
      SCIP_CALL( SCIPduplicateBlockMemoryArray(scip, &((*consdata)->andcoefs), andcoefs, nandconss) );
      if( andnegs != NULL )
      {
         SCIP_CALL( SCIPduplicateBlockMemoryArray(scip, &((*consdata)->andnegs), andnegs, nandconss) );
      }
      else
      {
         SCIP_CALL( SCIPallocClearBlockMemoryArray(scip, &((*consdata)->andnegs), nandconss) );
      }
      (*consdata)->nconsanddatas = nandconss;
      (*consdata)->sconsanddatas = nandconss;
 
      /* allocate temporary memory */
      SCIP_CALL( SCIPallocBufferArray(scip, &andress, nandconss) );
 
      conshdlrdata = SCIPconshdlrGetData(conshdlr);
      assert(conshdlrdata != NULL);
      assert(conshdlrdata->hashmap != NULL);
 
      /* get all and-resultants for sorting */
      for( c = nandconss - 1; c >= 0; --c )
      {
         assert(andconss[c] != NULL);
 
         andress[c] = SCIPgetResultantAnd(scip, andconss[c]);
         assert(andress[c] != NULL);
 
         (*consdata)->consanddatas[c] = (CONSANDDATA*) SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)andress[c]);
         assert((*consdata)->consanddatas[c] != NULL);
         assert((*consdata)->consanddatas[c]->origcons == andconss[c] || (*consdata)->consanddatas[c]->cons == andconss[c]);
 
         if( transforming )
         {
            /* if we perform a new transformation, we need to capture the transformed constraint */
            if( (*consdata)->consanddatas[c]->origcons != NULL && (*consdata)->consanddatas[c]->cons == NULL )
            {
               SCIP_VAR** vars;
               int ncvars;
               int v;
 
               /* do not capture the and constraint when scip is in transformed mode; this automatically happens in
                * SCIPtransformCons()
                */
               SCIP_CALL( SCIPtransformCons(scip, (*consdata)->consanddatas[c]->origcons, &((*consdata)->consanddatas[c]->cons)) );
               assert((*consdata)->consanddatas[c]->cons != NULL);
               assert((*consdata)->consanddatas[c]->newvars == NULL);
               assert((*consdata)->consanddatas[c]->isoriginal);
 
               (*consdata)->consanddatas[c]->istransformed = TRUE;
 
               vars = (*consdata)->consanddatas[c]->vars;
               ncvars = (*consdata)->consanddatas[c]->nvars;
               assert(vars != NULL || ncvars == 0);
 
               /* get transformed variables */
               SCIP_CALL( SCIPgetTransformedVars(scip, ncvars, vars, vars) );
 
               /* resort variables in transformed problem, because the order might change while tranforming */
               SCIPsortPtr((void**)vars, SCIPvarComp, ncvars);
 
               /* capture all transformed variables */
               for( v = ncvars - 1; v >= 0; --v )
               {
                  SCIP_CALL( SCIPcaptureVar(scip, vars[v]) ); /*lint !e613*/
               }
            }
            else if( (*consdata)->consanddatas[c]->cons != NULL )
               assert((*consdata)->consanddatas[c]->istransformed);
 
            ++((*consdata)->consanddatas[c]->nuses);
         }
         else if( transformed )
         {
            assert((*consdata)->consanddatas[c]->cons == andconss[c]);
            assert(SCIPconsIsTransformed(andconss[c]));
            assert((*consdata)->consanddatas[c]->istransformed);
         }
      }
 
      /* sort and-constraints after problem indices of corresponding and-resultants */
      SCIPsortPtrPtrRealBool((void**)andress, (void**)((*consdata)->consanddatas), (*consdata)->andcoefs, (*consdata)->andnegs, resvarComp, nandconss);
 
      /* free temporary memory */
      SCIPfreeBufferArray(scip, &andress);
   }
   else
   {
      (*consdata)->consanddatas = NULL;
      (*consdata)->andcoefs = NULL;
      (*consdata)->andnegs = NULL;
      (*consdata)->nconsanddatas = 0;
      (*consdata)->sconsanddatas = 0;
   }
 
   /* copy left and right hand side */
   (*consdata)->lhs = lhs;
   (*consdata)->rhs = rhs;
 
   (*consdata)->changed = TRUE;
   (*consdata)->propagated = FALSE;
   (*consdata)->presolved = FALSE;
   (*consdata)->cliquesadded = FALSE;
   (*consdata)->upgradetried = TRUE;
 
   /* count number of used consanddata objects in original problem */
   if( SCIPgetStage(scip) == SCIP_STAGE_PROBLEM )
   {
      SCIP_CONSHDLRDATA* conshdlrdata;
      conshdlrdata = SCIPconshdlrGetData(conshdlr);
      assert(conshdlrdata != NULL);
 
      conshdlrdata->noriguses += (*consdata)->nconsanddatas;
   }
 
   return SCIP_OKAY;
}
 
/** free a pseudo boolean constraint data */
static
SCIP_RETCODE consdataFree(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONSDATA**       consdata,           /**< pointer to linear constraint data */
   SCIP_Bool             isorig,             /**< are we freeing an original constraint? */
   SCIP_CONSHDLRDATA*    conshdlrdata        /**< constraint handler data */
   )
{
   CONSANDDATA** consanddatas;
   int nconsanddatas;
   int c;
 
   assert(scip != NULL);
   assert(consdata != NULL);
   assert(*consdata != NULL);
   assert((*consdata)->nconsanddatas == 0 || (*consdata)->consanddatas != NULL);
   assert(conshdlrdata != NULL);
 
   /* release linear constraint */
   if( (*consdata)->lincons != NULL )
   {
      SCIP_CALL( SCIPreleaseCons(scip, &((*consdata)->lincons)) );
   }
 
   nconsanddatas = (*consdata)->nconsanddatas;
   consanddatas = (*consdata)->consanddatas;
 
   /* count down uses and if necessary release constraints and delete data from hashtable and -map */
   for( c = nconsanddatas - 1; c >= 0; --c )
   {
      assert((consanddatas[c]->origcons == NULL) == (consanddatas[c]->noriguses == 0));
      assert((consanddatas[c]->cons == NULL) == (consanddatas[c]->nuses == 0));
      assert(consanddatas[c]->nuses >= 0);
      assert(consanddatas[c]->noriguses >= 0);
      assert(isorig ? consanddatas[c]->cons == NULL : TRUE);
 
      /* are we deleteing a transformed constraint */
      if( !isorig && consanddatas[c]->cons != NULL )
      {
         assert(!SCIPconsIsOriginal(consanddatas[c]->cons));
 
         --(consanddatas[c]->nuses);
 
         /* if the consanddata is not used anymore, release the constraint and clear the hashmap- and table */
         if( consanddatas[c]->nuses == 0 )
         {
            if( conshdlrdata->inithashmapandtable )
            {
               assert(conshdlrdata->hashmap != NULL);
               assert(conshdlrdata->hashtable != NULL);
 
               /* remove consanddata from hashtable, if it existed only in transformed space */
               if( consanddatas[c]->origcons == NULL )
               {
                  assert(SCIPhashtableExists(conshdlrdata->hashtable, (void*)consanddatas[c]));
                  SCIP_CALL( SCIPhashtableRemove(conshdlrdata->hashtable, (void*)consanddatas[c]) );
               }
               assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddatas[c]->cons)));
               SCIP_CALL( SCIPhashmapRemove(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddatas[c]->cons)) );
            }
 
            SCIP_CALL( SCIPreleaseCons(scip, &(consanddatas[c]->cons)) );
 
            /* if the consanddata object was only used in transformed space, delete the memory block */
            if( consanddatas[c]->origcons == NULL )
            {
               int d;
 
               assert(conshdlrdata->nallconsanddatas > 0);
 
               for( d = conshdlrdata->nallconsanddatas - 1; d >= 0; --d )
               {
                  if( conshdlrdata->allconsanddatas[d] == consanddatas[c] )
                  {
                     --conshdlrdata->nallconsanddatas;
 
                     SCIPfreeBlockMemory(scip, &(conshdlrdata->allconsanddatas[d])); /*lint !e866*/
 
                     conshdlrdata->allconsanddatas[d] = conshdlrdata->allconsanddatas[conshdlrdata->nallconsanddatas];
                     break;
                  }
               }
               assert(d >= 0);
               continue;
            }
         }
      }
      /* are we deleteing an original constraint */
      else if( isorig && consanddatas[c]->origcons != NULL )
      {
         assert(SCIPconsIsOriginal(consanddatas[c]->origcons));
         assert(consanddatas[c]->nuses == 0);
         assert(consanddatas[c]->nnewvars == 0);
         assert(consanddatas[c]->snewvars == 0);
         assert(consanddatas[c]->newvars == NULL);
 
         --(consanddatas[c]->noriguses);
 
         /* if the consanddata is not used anymore, release the constraint and clear the hashmap- and table */
         if( consanddatas[c]->noriguses == 0 )
         {
            int d;
 
            if( conshdlrdata->inithashmapandtable )
            {
               assert(conshdlrdata->hashmap != NULL);
               assert(conshdlrdata->hashtable != NULL);
 
               assert(SCIPhashtableExists(conshdlrdata->hashtable, (void*)consanddatas[c]));
               SCIP_CALL( SCIPhashtableRemove(conshdlrdata->hashtable, (void*)consanddatas[c]) );
 
               assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddatas[c]->origcons)));
               SCIP_CALL( SCIPhashmapRemove(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddatas[c]->origcons)) );
            }
 
            if( consanddatas[c]->vars != NULL )
            {
               assert(consanddatas[c]->nvars > 0);
               assert(consanddatas[c]->svars > 0);
               assert(consanddatas[c]->svars >= consanddatas[c]->nvars);
 
               SCIPfreeBlockMemoryArrayNull(scip, &(consanddatas[c]->vars), consanddatas[c]->svars);
               consanddatas[c]->nvars = 0;
               consanddatas[c]->svars = 0;
            }
            else
            {
               assert(consanddatas[c]->nvars == 0);
               assert(consanddatas[c]->svars == 0);
            }
 
            SCIP_CALL( SCIPreleaseCons(scip, &(consanddatas[c]->origcons)) );
            assert(consanddatas[c]->origcons == NULL);
 
            /* delete consanddata object */
            assert(conshdlrdata->nallconsanddatas > 0);
            for( d = conshdlrdata->nallconsanddatas - 1; d >= 0; --d )
            {
               if( conshdlrdata->allconsanddatas[d] == consanddatas[c] )
               {
                  --conshdlrdata->nallconsanddatas;
 
                  SCIPfreeBlockMemory(scip, &(conshdlrdata->allconsanddatas[d])); /*lint !e866*/
 
                  conshdlrdata->allconsanddatas[d] = conshdlrdata->allconsanddatas[conshdlrdata->nallconsanddatas];
                  break;
               }
            }
            assert(d >= 0);
 
            continue;
         }
      }
      else
      {
         assert(!consanddatas[c]->istransformed);
         assert(consanddatas[c]->cons == NULL);
      }
 
      /* clear and remove capture of transformed consanddata */
      if( consanddatas[c]->nuses == 0 && consanddatas[c]->istransformed )
      {
         SCIP_CALL( transformToOrig(scip, consanddatas[c], conshdlrdata) );
      }
#ifndef NDEBUG
      else if( consanddatas[c]->nuses == 0 )
      {
         SCIP_VAR** tmpvars;
         int ntmpvars;
         int v;
 
         assert(consanddatas[c]->nnewvars == 0);
         assert(consanddatas[c]->snewvars == 0);
         assert(consanddatas[c]->newvars == NULL);
 
         tmpvars = consanddatas[c]->vars;
         ntmpvars = consanddatas[c]->nvars;
 
         /* release all variables */
         for( v = ntmpvars - 1; v >= 0; --v )
         {
            assert(tmpvars[v] != NULL);
            assert(SCIPvarIsOriginal(tmpvars[v]));
         }
      }
#endif
 
      /* restore original data */
      if( !consanddatas[c]->istransformed && consanddatas[c]->noriguses > 0 )
      {
         assert(consanddatas[c]->origcons != NULL);
         assert(consanddatas[c]->nuses == 0);
         assert(consanddatas[c]->nnewvars == 0);
         assert(consanddatas[c]->snewvars == 0);
         assert(consanddatas[c]->newvars == NULL);
         assert(consanddatas[c]->nvars > 0);
         assert(consanddatas[c]->svars > 0);
         assert(consanddatas[c]->svars >= consanddatas[c]->nvars);
         assert(consanddatas[c]->vars != NULL);
         assert(consanddatas[c]->isoriginal);
 
         assert(consanddatas[c]->nvars == SCIPgetNVarsAnd(scip, consanddatas[c]->origcons));
         assert(SCIPgetVarsAnd(scip, consanddatas[c]->origcons) != NULL);
 
         /* check that the hash map and tabkle are still having all information */
         if( conshdlrdata->inithashmapandtable )
         {
            assert(conshdlrdata->hashmap != NULL);
            assert(conshdlrdata->hashtable != NULL);
            assert(SCIPgetResultantAnd(scip, consanddatas[c]->origcons) != NULL);
            assert(SCIPhashtableExists(conshdlrdata->hashtable, (void*)consanddatas[c]));
            assert(consanddatas[c] == (CONSANDDATA*)(SCIPhashtableRetrieve(conshdlrdata->hashtable, (void*)consanddatas[c])));
            assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddatas[c]->origcons)));
            assert(consanddatas[c] == (CONSANDDATA*)(SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddatas[c]->origcons))));
         }
      }
   }
 
   /* free array of and-constraints */
   SCIPfreeBlockMemoryArrayNull(scip, &((*consdata)->andnegs), (*consdata)->sconsanddatas);
   SCIPfreeBlockMemoryArrayNull(scip, &((*consdata)->andcoefs), (*consdata)->sconsanddatas);
   SCIPfreeBlockMemoryArrayNull(scip, &((*consdata)->consanddatas), (*consdata)->sconsanddatas);
 
   SCIPfreeBlockMemory(scip, consdata);
 
   return SCIP_OKAY;
}
 
/** check the locks of an AND resultant and removes it from all global structures if the resultant is not locked anymore */
static
SCIP_RETCODE checkLocksAndRes(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_VAR*             res                 /**< resultant of AND constraint */
   )
{
   assert(scip != NULL);
   assert(res != NULL);
 
   /* the resultant has no locks left and might be dual fixed now, we need to delete all its cliques */
   if( SCIPvarIsActive(res) && SCIPvarGetNLocksDownType(res, SCIP_LOCKTYPE_MODEL) == 0
      && SCIPvarGetNLocksUpType(res, SCIP_LOCKTYPE_MODEL) == 0 && SCIPgetStage(scip) < SCIP_STAGE_FREETRANS )
   {
      SCIP_CALL( SCIPremoveVarFromGlobalStructures(scip, res) );
   }
 
   return SCIP_OKAY;
}
 
/** installs rounding locks for the given and-constraint associated with given coefficient */
static
SCIP_RETCODE lockRoundingAndCons(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< pseudoboolean constraint */
   CONSANDDATA*const     consanddata,        /**< CONSANDDATA object for which we want to add the locks */
   SCIP_Real const       coef,               /**< coefficient which led to old locks */
   SCIP_Real const       lhs,                /**< left hand side */
   SCIP_Real const       rhs                 /**< right hand side */
   )
{
   SCIP_VAR** vars;
   int nvars;
   SCIP_VAR* res;
   SCIP_Bool haslhs;
   SCIP_Bool hasrhs;
   int v;
 
   assert(scip != NULL);
   assert(cons != NULL);
   assert(!SCIPconsIsLockedType(cons, SCIP_LOCKTYPE_CONFLICT));
   assert(consanddata != NULL);
   assert(!SCIPisInfinity(scip, coef) && !SCIPisInfinity(scip, -coef));
   assert(!SCIPisInfinity(scip, lhs));
   assert(!SCIPisInfinity(scip, -rhs));
   assert(SCIPisLE(scip, lhs, rhs));
 
   /* choose correct variable array to add locks for, we only add locks for now valid variables */
   if( consanddata->nnewvars > 0 )
   {
      vars = consanddata->newvars;
      nvars = consanddata->nnewvars;
   }
   else
   {
      vars = consanddata->vars;
      nvars = consanddata->nvars;
   }
 
   res = SCIPgetResultantAnd(scip, consanddata->cons);
   assert(nvars == 0 || (vars != NULL && res != NULL));
 
   /* check which sites are infinity */
   haslhs = !SCIPisInfinity(scip, -lhs);
   hasrhs = !SCIPisInfinity(scip, rhs);
 
   if( SCIPconsIsLocked(cons) )
   {
      /* locking variables */
      if( SCIPisPositive(scip, coef) )
      {
         for( v = nvars - 1; v >= 0; --v )
         {
            SCIP_CALL( SCIPlockVarCons(scip, vars[v], cons, haslhs, hasrhs) );
         }
      }
      else
      {
         for( v = nvars - 1; v >= 0; --v )
         {
            SCIP_CALL( SCIPlockVarCons(scip, vars[v], cons, hasrhs, haslhs) );
         }
      }
      SCIP_CALL( SCIPlockVarCons(scip, res, cons, TRUE, TRUE) );
   }
 
   return SCIP_OKAY;
}
 
/** removes rounding locks for the given and-constraint associated with given coefficient */
static
SCIP_RETCODE unlockRoundingAndCons(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< pseudoboolean constraint */
   CONSANDDATA*const     consanddata,        /**< CONSANDDATA object for which we want to delete the locks */
   SCIP_Real const       coef,               /**< coefficient which led to old locks */
   SCIP_Real const       lhs,                /**< left hand side which led to old locks */
   SCIP_Real const       rhs                 /**< right hand side which led to old locks */
   )
{
   SCIP_VAR** vars;
   int nvars;
   SCIP_VAR* res;
   SCIP_Bool haslhs;
   SCIP_Bool hasrhs;
   int v;
 
   assert(scip != NULL);
   assert(cons != NULL);
   assert(!SCIPconsIsLockedType(cons, SCIP_LOCKTYPE_CONFLICT));
   assert(consanddata != NULL);
   assert(!SCIPisInfinity(scip, coef) && !SCIPisInfinity(scip, -coef));
   assert(!SCIPisInfinity(scip, lhs));
   assert(!SCIPisInfinity(scip, -rhs));
   assert(SCIPisLE(scip, lhs, rhs));
 
   vars = consanddata->vars;
   nvars = consanddata->nvars;
 
   if( consanddata->cons != NULL )
      res = SCIPgetResultantAnd(scip, consanddata->cons);
   else
      res = NULL;
   assert(nvars == 0 || vars != NULL);
 
   /* check which sites are infinity */
   haslhs = !SCIPisInfinity(scip, -lhs);
   hasrhs = !SCIPisInfinity(scip, rhs);
 
   if( SCIPconsIsLocked(cons) )
   {
      /* unlock variables */
      if( SCIPisPositive(scip, coef) )
      {
         for( v = nvars - 1; v >= 0; --v )
         {
            SCIP_CALL( SCIPunlockVarCons(scip, vars[v], cons, haslhs, hasrhs) );
         }
      }
      else
      {
         for( v = nvars - 1; v >= 0; --v )
         {
            SCIP_CALL( SCIPunlockVarCons(scip, vars[v], cons, hasrhs, haslhs) );
         }
      }
 
      if( res != NULL )
      {
         SCIP_CALL( SCIPunlockVarCons(scip, res, cons, TRUE, TRUE) );
 
         SCIP_CALL( checkLocksAndRes(scip, res) );
      }
   }
 
   return SCIP_OKAY;
}
 
/** prints pseudoboolean constraint in CIP format to file stream */
static
SCIP_RETCODE consdataPrint(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< pseudoboolean constraint */
   FILE*const            file                /**< output file (or NULL for standard output) */
   )
{
   SCIP_CONSHDLR* conshdlr;
   SCIP_CONSHDLRDATA* conshdlrdata;
   SCIP_CONSDATA* consdata;
   SCIP_VAR*** monomialvars;
   SCIP_VAR** vars;
   SCIP_Real* coefs;
   SCIP_Real* monomialcoefs;
   SCIP_Real lhs;
   SCIP_Real rhs;
   int* monomialnvars;
   int nvars;
   int nmonomials;
   int v;
 
   assert(scip != NULL);
   assert(cons != NULL);
 
   consdata = SCIPconsGetData(cons);
   assert(consdata != NULL);
   assert(consdata->intvar == NULL);
   assert(consdata->lincons != NULL);
 
   /* gets number of variables in linear constraint */
   SCIP_CALL( getLinearConsNVars(scip, consdata->lincons, consdata->linconstype, &nvars) );
 
   /* every variable in the linear constraint is either a linear variable or a term variable
    * but there can be additional fixed or negation-paired and-resultants with relevant and-constraints
    * whose values are already resolved in the linear constraint
    */
   assert(consdata->nlinvars + consdata->nconsanddatas >= nvars);
 
   /* initialize buffers for storing the terms and coefficients */
   SCIP_CALL( SCIPallocBufferArray(scip, &vars, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &coefs, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &monomialvars, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &monomialcoefs, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &monomialnvars, nvars) );
 
   /* get sides of linear constraint */
   SCIP_CALL( getLinearConsSides(scip, consdata->lincons, consdata->linconstype, &lhs, &rhs) );
   assert(!SCIPisInfinity(scip, lhs));
   assert(!SCIPisInfinity(scip, -rhs));
   assert(SCIPisLE(scip, lhs, rhs));
 
   /* get variables and coefficient of linear constraint */
   SCIP_CALL( getLinearConsVarsData(scip, consdata->lincons, consdata->linconstype, vars, coefs, &nvars) );
   assert(nvars == 0 || (coefs != NULL));
 
   /* get and-data hashmap */
   conshdlr = SCIPconsGetHdlr(cons);
   assert(conshdlr != NULL);
   conshdlrdata = SCIPconshdlrGetData(conshdlr);
   assert(conshdlrdata != NULL);
   assert(conshdlrdata->hashmap != NULL);
   nmonomials = 0;
 
   /* collect all terms */
   for( v = 0; v < nvars; ++v )
   {
      CONSANDDATA* consanddata = NULL;
      SCIP_VAR** andvars = NULL;
      SCIP_VAR* var = vars[v];
      int nandvars = 0;
 
      assert(SCIPvarIsBinary(var));
 
      /* find and-constraint to standard or negated and-resultant */
      do
      {
         /* @todo: drop indicator variable */
         assert(!consdata->issoftcons || var != consdata->indvar);
         consanddata = (CONSANDDATA*)SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)var);
 
         if( consanddata != NULL )
         {
            SCIP_CONS* andcons = SCIPconsIsOriginal(cons) ? consanddata->origcons : consanddata->cons;
 
            andvars = SCIPgetVarsAnd(scip, andcons);
            nandvars = SCIPgetNVarsAnd(scip, andcons);
 
            break;
         }
 
         var = var == vars[v] ? SCIPvarGetNegatedVar(var) : vars[v];
      }
      while( var != vars[v] );
 
      if( consanddata == NULL )
      {
         assert(var != NULL);
         assert(var == vars[v]);
         monomialvars[nmonomials] = vars + v;
         monomialnvars[nmonomials] = 1;
      }
      else
      {
         SCIP_Bool fixed = nandvars == 0;
         SCIP_Bool negated = var != vars[v];
 
         if( fixed != negated )
         {
            if( !SCIPisInfinity(scip, -lhs) )
               lhs -= coefs[v];
 
            if( !SCIPisInfinity(scip, rhs) )
               rhs -= coefs[v];
         }
 
         if( fixed )
            continue;
 
         if( negated )
            coefs[v] *= -1.0;
 
         assert(andvars != NULL);
         monomialvars[nmonomials] = andvars;
         assert(nandvars >= 1);
         monomialnvars[nmonomials] = nandvars;
      }
 
      assert(!SCIPisZero(scip, coefs[v]));
      monomialcoefs[nmonomials] = coefs[v];
      ++nmonomials;
   }
 
   /* print left side */
   if( !SCIPisInfinity(scip, -lhs) && !SCIPisInfinity(scip, rhs) && lhs != rhs ) /*lint !e777*/
      SCIPinfoMessage(scip, file, "%.15g <= ", lhs);
 
   /* print pseudoboolean polynomial */
   SCIP_CALL( SCIPwriteVarsPolynomial(scip, file, monomialvars, NULL, monomialcoefs, monomialnvars, nmonomials, TRUE) );
 
   /* print right side */
   if( lhs == rhs ) /*lint !e777*/
      SCIPinfoMessage(scip, file, " == %.15g", rhs);
   else if( !SCIPisInfinity(scip, rhs) )
      SCIPinfoMessage(scip, file, " <= %.15g", rhs);
   else if( !SCIPisInfinity(scip, -lhs) )
      SCIPinfoMessage(scip, file, " >= %.15g", lhs);
   else
      SCIPinfoMessage(scip, file, " [free]");
 
   /* free buffers for storing the terms and coefficients */
   SCIPfreeBufferArray(scip, &monomialnvars);
   SCIPfreeBufferArray(scip, &monomialcoefs);
   SCIPfreeBufferArray(scip, &monomialvars);
   SCIPfreeBufferArray(scip, &coefs);
   SCIPfreeBufferArray(scip, &vars);
 
   /* print indicator variable if soft constraint */
   if( consdata->issoftcons )
   {
      SCIPinfoMessage(scip, file, " (indvar = ");
      SCIP_CALL( SCIPwriteVarName(scip, file, consdata->indvar, TRUE) );
      SCIPinfoMessage(scip, file, ")");
      assert(consdata->weight == SCIPvarGetObj(consdata->indvar)); /*lint !e777*/
   }
 
   return SCIP_OKAY;
}
 
/** creates and/or adds the resultant for a given term */
static
SCIP_RETCODE createAndAddAndCons(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONSHDLR*const   conshdlr,           /**< pseudoboolean constraint handler */
   SCIP_VAR**const       vars,               /**< array of variables to get and-constraints for */
   int const             nvars,              /**< number of variables to get and-constraints for */
   SCIP_Bool const       initial,            /**< should the LP relaxation of constraint be in the initial LP?
                                              *   Usually set to TRUE. Set to FALSE for 'lazy constraints'. */
   SCIP_Bool const       enforce,            /**< should the constraint be enforced during node processing?
                                              *   TRUE for model constraints, FALSE for additional, redundant
                                              *   constraints. */
   SCIP_Bool const       check,              /**< should the constraint be checked for feasibility?
                                              *   TRUE for model constraints, FALSE for additional, redundant
                                              *   constraints. */
   SCIP_Bool const       local,              /**< is constraint only valid locally?
                                              *   Usually set to FALSE. Has to be set to TRUE, e.g., for branching
                                              *   constraints. */
   SCIP_Bool const       modifiable,         /**< is constraint modifiable (subject to column generation)?
                                              *   Usually set to FALSE. In column generation applications, set to TRUE
                                              *   if pricing adds coefficients to this constraint. */
   SCIP_Bool const       dynamic,            /**< is constraint subject to aging?
                                              *   Usually set to FALSE. Set to TRUE for own cuts which
                                              *   are seperated as constraints. */
   SCIP_Bool const       stickingatnode,     /**< should the constraint always be kept at the node where it was added, even
                                              *   if it may be moved to a more global node?
                                              *   Usually set to FALSE. Set to TRUE to for constraints that represent
                                              *   node data. */
   SCIP_CONS**const      andcons             /**< pointer to store and-constraint */
   )
{
   CONSANDDATA* newdata;
   CONSANDDATA* tmpdata;
   SCIP_CONSHDLRDATA* conshdlrdata;
   char name[SCIP_MAXSTRLEN];
   SCIP_Bool separate;
   SCIP_Bool propagate;
   SCIP_Bool removable;
   SCIP_Bool transformed;
 
   assert(scip != NULL);
   assert(conshdlr != NULL);
   assert(vars != NULL);
   assert(nvars > 0);
   assert(andcons != NULL);
 
   conshdlrdata = SCIPconshdlrGetData(conshdlr);
   assert(conshdlrdata != NULL);
   assert(conshdlrdata->hashtable != NULL);
 
   transformed = SCIPisTransformed(scip);
 
   /* allocate memory for a possible new consanddata object */
   SCIP_CALL( SCIPallocBlockMemory(scip, &newdata) );
   SCIP_CALL( SCIPduplicateBlockMemoryArray(scip, &(newdata->vars), vars, nvars) );
   newdata->nvars = nvars;
   newdata->svars = nvars;
   newdata->newvars = NULL;
   newdata->nnewvars = 0;
   newdata->snewvars = 0;
   newdata->noriguses = 0;
   newdata->nuses = 0;
   newdata->istransformed = transformed;
   newdata->isoriginal = !transformed;
   newdata->cons = NULL;
   newdata->origcons = NULL;
 
   /* sort variables */
   SCIPsortPtr((void**)(newdata->vars), SCIPvarComp, nvars);
 
   /* get constraint from current hash table with same variables as cons0 */
   tmpdata = (CONSANDDATA*)(SCIPhashtableRetrieve(conshdlrdata->hashtable, (void*)newdata));
 
   /* if there is already the same and constraint created use this resultant */
   if( tmpdata != NULL )
   {
#ifndef NDEBUG
      SCIP_VAR* res;
#endif
      if( transformed )
      {
         assert(tmpdata->cons != NULL);
         *andcons = tmpdata->cons;
 
         assert(tmpdata->nuses > 0);
         /* increase usage of data object */
         ++(tmpdata->nuses);
      }
      else
      {
         assert(tmpdata->origcons != NULL);
         *andcons = tmpdata->origcons;
 
         assert(tmpdata->noriguses > 0);
         /* increase usage of data object */
         ++(tmpdata->noriguses);
      }
      assert(*andcons != NULL);
 
#ifndef NDEBUG
      res = SCIPgetResultantAnd(scip, *andcons);
      assert(res != NULL);
 
      /* check that we already have added this resultant to and-constraint entry */
      assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)res));
#endif
   }
   else
   {
      /* create new and-constraint */
      SCIP_CONS* newcons;
      SCIP_VAR* resultant;
 
      /* create auxiliary variable */
      (void)SCIPsnprintf(name, SCIP_MAXSTRLEN, ARTIFICIALVARNAMEPREFIX"%d", conshdlrdata->nallconsanddatas);
      SCIP_CALL( SCIPcreateVar(scip, &resultant, name, 0.0, 1.0, 0.0, SCIP_VARTYPE_BINARY,
            TRUE, TRUE, NULL, NULL, NULL, NULL, NULL) );
 
      /* @todo: branch on artificial variables, the test results show that it is of advantage */
      /* change branching priority of artificial variable to -1 */
      SCIP_CALL( SCIPchgVarBranchPriority(scip, resultant, -1) );
 
      /* add auxiliary variable to the problem */
      SCIP_CALL( SCIPaddVar(scip, resultant) );
 
      /* @todo: keep and-resultants defined to check debug solution */
#ifdef SCIP_DISABLED_CODE
#ifdef WITH_DEBUG_SOLUTION
      if( SCIPdebugIsMainscip(scip) )
      {
         SCIP_Real val;
         SCIP_Real debugsolval;
         int v;
 
         for( v = nvars - 1; v >= 0; --v )
         {
            SCIP_CALL( SCIPdebugGetSolVal(scip, vars[v], &val) );
            assert(SCIPisFeasZero(scip, val) || SCIPisFeasEQ(scip, val, 1.0));
 
            if( val < 0.5 )
               break;
         }
         val = ((val < 0.5) ? 0.0 : 1.0);
 
         SCIP_CALL( SCIPdebugGetSolVal(scip, resultant, &debugsolval) );
         if( (SCIPvarIsOriginal(resultant) || SCIPvarIsTransformedOrigvar(resultant)) && !SCIPisFeasEQ(scip, debugsolval, val) )
         {
            SCIPerrorMessage("computed solution value %g for resultant <%s> violates debug solution value %g\n", val, SCIPvarGetName(resultant), debugsolval);
            SCIPABORT();
            return SCIP_ERROR; /*lint !e527*/
         }
         else if( !SCIPvarIsOriginal(resultant) && !SCIPvarIsTransformedOrigvar(resultant) )
         {
            SCIP_CALL( SCIPdebugAddSolVal(scip, resultant, val) );
         }
      }
#endif
#endif
 
      SCIP_CALL( SCIPgetBoolParam(scip, "constraints/" CONSHDLR_NAME "/nlcseparate", &separate) );
      SCIP_CALL( SCIPgetBoolParam(scip, "constraints/" CONSHDLR_NAME "/nlcpropagate", &propagate) );
      SCIP_CALL( SCIPgetBoolParam(scip, "constraints/" CONSHDLR_NAME "/nlcremovable", &removable) );
 
      /* we do not want to check the and constraints, so the check flag will be FALSE */
 
      /* create and add "and" constraint for the multiplication of the binary variables */
      (void)SCIPsnprintf(name, SCIP_MAXSTRLEN, "andcons_%d", conshdlrdata->nallconsanddatas);
      SCIP_CALL( SCIPcreateConsAnd(scip, &newcons, name, resultant, newdata->nvars, newdata->vars,
            initial, separate, enforce, check && FALSE, propagate,
            local, modifiable, dynamic, removable, stickingatnode) ); /*lint !e506*/
      SCIP_CALL( SCIPaddCons(scip, newcons) );
      SCIPdebugPrintCons(scip, newcons, NULL);
 
      /* force all deriving constraint from this and constraint to be checked and not removable */
      SCIP_CALL( SCIPchgAndConsCheckFlagWhenUpgr(scip, newcons, TRUE) );
      SCIP_CALL( SCIPchgAndConsRemovableFlagWhenUpgr(scip, newcons, TRUE) );
 
      *andcons = newcons;
      assert(*andcons != NULL);
 
      /* resize data for all and-constraints if necessary */
      if( conshdlrdata->nallconsanddatas == conshdlrdata->sallconsanddatas )
      {
         SCIP_CALL( SCIPensureBlockMemoryArray(scip, &(conshdlrdata->allconsanddatas), &(conshdlrdata->sallconsanddatas), SCIPcalcMemGrowSize(scip, conshdlrdata->sallconsanddatas + 1)) );
      }
 
      /* add new data object to global hash table */
      conshdlrdata->allconsanddatas[conshdlrdata->nallconsanddatas] = newdata;
      ++(conshdlrdata->nallconsanddatas);
 
      if( transformed )
      {
         int v;
 
         newdata->cons = newcons;
         SCIP_CALL( SCIPcaptureCons(scip, newdata->cons) );
 
         /* initialize usage of data object */
         newdata->nuses = 1;
 
         /* capture all variables */
         for( v = newdata->nvars - 1; v >= 0; --v )
         {
            SCIP_CALL( SCIPcaptureVar(scip, newdata->vars[v]) ); /*lint !e613*/
         }
      }
      else
      {
         newdata->origcons = newcons;
         SCIP_CALL( SCIPcaptureCons(scip, newdata->origcons) );
 
         /* initialize usage of data object */
         newdata->noriguses = 1;
      }
 
      /* no such and-constraint in current hash table: insert the new object into hash table */
      SCIP_CALL( SCIPhashtableInsert(conshdlrdata->hashtable, (void*)newdata) );
 
      /* insert new mapping */
      assert(!SCIPhashmapExists(conshdlrdata->hashmap, (void*)resultant));
      SCIP_CALL( SCIPhashmapInsert(conshdlrdata->hashmap, (void*)resultant, (void*)newdata) );
 
      /* release and-resultant and -constraint */
      SCIP_CALL( SCIPreleaseVar(scip, &resultant) );
      SCIP_CALL( SCIPreleaseCons(scip, &newcons) );
 
      return SCIP_OKAY;
   }
 
   /* free memory */
   SCIPfreeBlockMemoryArray(scip, &(newdata->vars), newdata->svars);
   SCIPfreeBlockMemory(scip, &newdata);
 
   return SCIP_OKAY;
}
 
/** adds a term to the given pseudoboolean constraint */
static
SCIP_RETCODE addCoefTerm(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< pseudoboolean constraint */
   SCIP_VAR**const       vars,               /**< variables of the nonlinear term */
   int const             nvars,              /**< number of variables of the nonlinear term */
   SCIP_Real const       val                 /**< coefficient of constraint entry */
   )
{
   SCIP_CONSHDLR* conshdlr;
   SCIP_CONSHDLRDATA* conshdlrdata;
   SCIP_CONS* andcons;
   SCIP_CONSDATA* consdata;
   SCIP_VAR* res;
 
   assert(scip != NULL);
   assert(cons != NULL);
   assert(nvars == 0 || vars != NULL);
 
   if( nvars == 0 || SCIPisZero(scip, val) )
      return SCIP_OKAY;
 
   consdata = SCIPconsGetData(cons);
   assert(consdata != NULL);
 
   conshdlr = SCIPconsGetHdlr(cons);
   assert(conshdlr != NULL);
 
   conshdlrdata =  SCIPconshdlrGetData(conshdlr);
   assert(conshdlrdata != NULL);
 
   /* create (and add) and-constraint */
   SCIP_CALL( createAndAddAndCons(scip, conshdlr, vars, nvars,
         SCIPconsIsInitial(cons), SCIPconsIsEnforced(cons), SCIPconsIsChecked(cons), SCIPconsIsLocal(cons),
         SCIPconsIsModifiable(cons), SCIPconsIsDynamic(cons), SCIPconsIsStickingAtNode(cons),
         &andcons) );
   assert(andcons != NULL);
 
   /* ensure memory size */
   if( consdata->nconsanddatas == consdata->sconsanddatas )
   {
      SCIP_CALL( SCIPensureBlockMemoryArray(scip, &(consdata->consanddatas), &(consdata->sconsanddatas), consdata->sconsanddatas + 1) );
   }
 
   res = SCIPgetResultantAnd(scip, andcons);
   assert(res != NULL);
   assert(SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)res) != NULL);
 
   consdata->consanddatas[consdata->nconsanddatas] = (CONSANDDATA*) SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)res);
   ++(consdata->nconsanddatas);
 
   /* add auxiliary variables to linear constraint */
   switch( consdata->linconstype )
   {
   case SCIP_LINEARCONSTYPE_LINEAR:
      SCIP_CALL( SCIPaddCoefLinear(scip, consdata->lincons, res, val) );
      break;
   case SCIP_LINEARCONSTYPE_LOGICOR:
      if( !SCIPisEQ(scip, val, 1.0) )
         return SCIP_INVALIDDATA;
 
      SCIP_CALL( SCIPaddCoefLogicor(scip, consdata->lincons, res) );
      break;
   case SCIP_LINEARCONSTYPE_KNAPSACK:
      if( !SCIPisIntegral(scip, val) || !SCIPisPositive(scip, val) )
         return SCIP_INVALIDDATA;
 
      SCIP_CALL( SCIPaddCoefKnapsack(scip, consdata->lincons, res, (SCIP_Longint) val) );
      break;
   case SCIP_LINEARCONSTYPE_SETPPC:
      if( !SCIPisEQ(scip, val, 1.0) )
         return SCIP_INVALIDDATA;
 
      SCIP_CALL( SCIPaddCoefSetppc(scip, consdata->lincons, res) );
      break;
#ifdef WITHEQKNAPSACK
   case SCIP_LINEARCONSTYPE_EQKNAPSACK:
      if( !SCIPisIntegral(scip, val) || !SCIPisPositive(scip, val) )
         return SCIP_INVALIDDATA;
 
      SCIP_CALL( SCIPaddCoefEQKnapsack(scip, consdata->lincons, res, (SCIP_Longint) val) );
      break;
#endif
   case SCIP_LINEARCONSTYPE_INVALIDCONS:
   default:
      SCIPerrorMessage("unknown linear constraint type\n");
      return SCIP_INVALIDDATA;
   }
 
   /* install rounding locks for all new variable */
   SCIP_CALL( lockRoundingAndCons(scip, cons, consdata->consanddatas[consdata->nconsanddatas - 1], val, consdata->lhs, consdata->rhs) );
 
   /* change flags */
   consdata->changed = TRUE;
   consdata->propagated = FALSE;
   consdata->presolved = FALSE;
   consdata->cliquesadded = FALSE;
   consdata->upgradetried = FALSE;
 
   return SCIP_OKAY;
}
 
/** changes left hand side of linear constraint */
static
SCIP_RETCODE chgLhsLinearCons(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< linear constraint */
   SCIP_LINEARCONSTYPE const constype,       /**< linear constraint type */
   SCIP_Real const       lhs                 /**< new left hand side of linear constraint */
   )
{
   switch( constype )
   {
   case SCIP_LINEARCONSTYPE_LINEAR:
      SCIP_CALL( SCIPchgLhsLinear(scip, cons, lhs) );
      break;
   case SCIP_LINEARCONSTYPE_LOGICOR:
   case SCIP_LINEARCONSTYPE_KNAPSACK:
   case SCIP_LINEARCONSTYPE_SETPPC:
      SCIPerrorMessage("changing left hand side only allowed on standard lienar constraint \n");
      return SCIP_INVALIDDATA;
#ifdef WITHEQKNAPSACK
   case SCIP_LINEARCONSTYPE_EQKNAPSACK:
#endif
   case SCIP_LINEARCONSTYPE_INVALIDCONS:
   default:
      SCIPerrorMessage("unknown linear constraint type\n");
      return SCIP_INVALIDDATA;
   }
 
   return SCIP_OKAY;
}
 
/** changes right hand side of linear constraint */
static
SCIP_RETCODE chgRhsLinearCons(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< linear constraint */
   SCIP_LINEARCONSTYPE const constype,       /**< linear constraint type */
   SCIP_Real const       rhs                 /**< new right hand side of linear constraint */
   )
{
   switch( constype )
   {
   case SCIP_LINEARCONSTYPE_LINEAR:
      SCIP_CALL( SCIPchgRhsLinear(scip, cons, rhs) );
      break;
   case SCIP_LINEARCONSTYPE_LOGICOR:
   case SCIP_LINEARCONSTYPE_KNAPSACK:
   case SCIP_LINEARCONSTYPE_SETPPC:
      SCIPerrorMessage("changing left hand side only allowed on standard lienar constraint \n");
      return SCIP_INVALIDDATA;
#ifdef WITHEQKNAPSACK
   case SCIP_LINEARCONSTYPE_EQKNAPSACK:
#endif
   case SCIP_LINEARCONSTYPE_INVALIDCONS:
   default:
      SCIPerrorMessage("unknown linear constraint type\n");
      return SCIP_INVALIDDATA;
   }
 
   return SCIP_OKAY;
}
 
/** sets left hand side of linear constraint */
static
SCIP_RETCODE chgLhs(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< linear constraint */
   SCIP_Real             lhs                 /**< new left hand side */
   )
{
   SCIP_CONSDATA* consdata;
   SCIP_VAR** vars;
   SCIP_Real* coefs;
   int nvars;
   SCIP_VAR** linvars;
   SCIP_Real* lincoefs;
   int nlinvars;
   SCIP_VAR** andress;
   SCIP_Real* andcoefs;
   SCIP_Bool* andnegs;
   int nandress;
   SCIP_Real oldlhs;
   SCIP_Real oldrhs;
 
   assert(scip != NULL);
   assert(cons != NULL);
   assert(!SCIPconsIsLockedType(cons, SCIP_LOCKTYPE_CONFLICT));
   assert(!SCIPisInfinity(scip, lhs));
 
   /* adjust value to not be smaller than -inf */
   if ( SCIPisInfinity(scip, -lhs) )
      lhs = -SCIPinfinity(scip);
 
   consdata = SCIPconsGetData(cons);
   assert(consdata != NULL);
 
   /* get sides of linear constraint */
   SCIP_CALL( getLinearConsSides(scip, consdata->lincons, consdata->linconstype, &oldlhs, &oldrhs) );
   assert(!SCIPisInfinity(scip, oldlhs));
   assert(!SCIPisInfinity(scip, -oldrhs));
   assert(SCIPisLE(scip, oldlhs, oldrhs));
 
   /* check whether the side is not changed */
   if( SCIPisEQ(scip, oldlhs, lhs) )
      return SCIP_OKAY;
 
   /* gets number of variables in linear constraint */
   SCIP_CALL( getLinearConsNVars(scip, consdata->lincons, consdata->linconstype, &nvars) );
 
   /* allocate temporary memory */
   SCIP_CALL( SCIPallocBufferArray(scip, &vars, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &coefs, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &linvars, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &lincoefs, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &andress, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &andcoefs, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &andnegs, nvars) );
 
   /* get variables and coefficient of linear constraint */
   SCIP_CALL( getLinearConsVarsData(scip, consdata->lincons, consdata->linconstype, vars, coefs, &nvars) );
   assert(nvars == 0 || (coefs != NULL));
 
   /* calculate all not artificial linear variables and all artificial and-resultants */
   SCIP_CALL( getLinVarsAndAndRess(scip, cons, vars, coefs, nvars, linvars, lincoefs, &nlinvars, andress, andcoefs, andnegs, &nandress) );
   assert(consdata->nconsanddatas == nandress);
 
   /* if necessary, update the rounding locks of variables */
   if( SCIPconsIsLocked(cons) )
   {
      SCIP_VAR** andvars;
      int nandvars;
      SCIP_Real val;
      int v;
      int c;
 
      assert(SCIPconsIsTransformed(cons));
 
      if( SCIPisInfinity(scip, -oldlhs) && !SCIPisInfinity(scip, -lhs) )
      {
         /* non-linear part */
         for( c = consdata->nconsanddatas - 1; c >= 0; --c )
         {
            CONSANDDATA* consanddata;
            SCIP_CONS* andcons;
 
            consanddata = consdata->consanddatas[c];
            assert(consanddata != NULL);
 
            andcons = consanddata->cons;
            assert(andcons != NULL);
 
            andvars = SCIPgetVarsAnd(scip, andcons);
            nandvars = SCIPgetNVarsAnd(scip, andcons);
            val = andnegs[c] ? -andcoefs[c] : andcoefs[c];
 
            /* lock variables */
            if( SCIPisPositive(scip, val) )
            {
               for( v = nandvars - 1; v >= 0; --v )
               {
                  SCIP_CALL( SCIPlockVarCons(scip, andvars[v], cons, TRUE, FALSE) );
               }
            }
            else
            {
               for( v = nandvars - 1; v >= 0; --v )
               {
                  SCIP_CALL( SCIPlockVarCons(scip, andvars[v], cons, FALSE, TRUE) );
               }
            }
         }
      }
      else if( !SCIPisInfinity(scip, -oldlhs) && SCIPisInfinity(scip, -lhs) )
      {
         /* non-linear part */
         for( c = consdata->nconsanddatas - 1; c >= 0; --c )
         {
            CONSANDDATA* consanddata;
            SCIP_CONS* andcons;
 
            consanddata = consdata->consanddatas[c];
            assert(consanddata != NULL);
 
            andcons = consanddata->cons;
            assert(andcons != NULL);
 
            andvars = SCIPgetVarsAnd(scip, andcons);
            nandvars = SCIPgetNVarsAnd(scip, andcons);
            val = andnegs[c] ? -andcoefs[c] : andcoefs[c];
 
            /* lock variables */
            if( SCIPisPositive(scip, val) )
            {
               for( v = nandvars - 1; v >= 0; --v )
               {
                  SCIP_CALL( SCIPunlockVarCons(scip, andvars[v], cons, TRUE, FALSE) );
               }
            }
            else
            {
               for( v = nandvars - 1; v >= 0; --v )
               {
                  SCIP_CALL( SCIPunlockVarCons(scip, andvars[v], cons, FALSE, TRUE) );
               }
            }
         }
      }
   }
 
   /* check whether the left hand side is increased, if and only if that's the case we maybe can propagate, tighten and add more cliques */
   if( SCIPisLT(scip, oldlhs, lhs) )
   {
      consdata->propagated = FALSE;
   }
 
   /* set new left hand side and update constraint data */
   SCIP_CALL( chgLhsLinearCons(scip, consdata->lincons, consdata->linconstype, lhs) );
   consdata->lhs = lhs;
   consdata->presolved = FALSE;
   consdata->changed = TRUE;
 
   /* free temporary memory */
   SCIPfreeBufferArray(scip, &andnegs);
   SCIPfreeBufferArray(scip, &andcoefs);
   SCIPfreeBufferArray(scip, &andress);
   SCIPfreeBufferArray(scip, &lincoefs);
   SCIPfreeBufferArray(scip, &linvars);
   SCIPfreeBufferArray(scip, &coefs);
   SCIPfreeBufferArray(scip, &vars);
 
   return SCIP_OKAY;
}
 
/** sets right hand side of pseudoboolean constraint */
static
SCIP_RETCODE chgRhs(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< linear constraint */
   SCIP_Real             rhs                 /**< new right hand side */
   )
{
   SCIP_CONSDATA* consdata;
   SCIP_VAR** vars;
   SCIP_Real* coefs;
   int nvars;
   SCIP_VAR** linvars;
   SCIP_Real* lincoefs;
   int nlinvars;
   SCIP_VAR** andress;
   SCIP_Real* andcoefs;
   SCIP_Bool* andnegs;
   int nandress;
   SCIP_Real oldlhs;
   SCIP_Real oldrhs;
 
   assert(scip != NULL);
   assert(cons != NULL);
   assert(!SCIPconsIsLockedType(cons, SCIP_LOCKTYPE_CONFLICT));
   assert(!SCIPisInfinity(scip, -rhs));
 
   /* adjust value to not be larger than inf */
   if( SCIPisInfinity(scip, rhs) )
      rhs = SCIPinfinity(scip);
 
   consdata = SCIPconsGetData(cons);
   assert(consdata != NULL);
 
   /* get sides of linear constraint */
   SCIP_CALL( getLinearConsSides(scip, consdata->lincons, consdata->linconstype, &oldlhs, &oldrhs) );
   assert(!SCIPisInfinity(scip, oldlhs));
   assert(!SCIPisInfinity(scip, -oldrhs));
   assert(SCIPisLE(scip, oldlhs, oldrhs));
 
   /* check whether the side is not changed */
   if( SCIPisEQ(scip, oldrhs, rhs) )
      return SCIP_OKAY;
 
   /* gets number of variables in linear constraint */
   SCIP_CALL( getLinearConsNVars(scip, consdata->lincons, consdata->linconstype, &nvars) );
 
   /* allocate temporary memory */
   SCIP_CALL( SCIPallocBufferArray(scip, &vars, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &coefs, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &linvars, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &lincoefs, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &andress, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &andcoefs, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &andnegs, nvars) );
 
   /* get variables and coefficient of linear constraint */
   SCIP_CALL( getLinearConsVarsData(scip, consdata->lincons, consdata->linconstype, vars, coefs, &nvars) );
   assert(nvars == 0 || (coefs != NULL));
 
   /* calculate all not artificial linear variables and all artificial and-resultants */
   SCIP_CALL( getLinVarsAndAndRess(scip, cons, vars, coefs, nvars, linvars, lincoefs, &nlinvars, andress, andcoefs, andnegs, &nandress) );
   assert(consdata->nconsanddatas == nandress);
 
   /* if necessary, update the rounding locks of variables */
   if( SCIPconsIsLocked(cons) )
   {
      SCIP_VAR** andvars;
      int nandvars;
      SCIP_Real val;
      int v;
      int c;
 
      assert(SCIPconsIsTransformed(cons));
 
      if( SCIPisInfinity(scip, oldrhs) && !SCIPisInfinity(scip, rhs) )
      {
         /* non-linear part */
         for( c = consdata->nconsanddatas - 1; c >= 0; --c )
         {
            CONSANDDATA* consanddata;
            SCIP_CONS* andcons;
 
            consanddata = consdata->consanddatas[c];
            assert(consanddata != NULL);
 
            andcons = consanddata->cons;
            assert(andcons != NULL);
 
            andvars = SCIPgetVarsAnd(scip, andcons);
            nandvars = SCIPgetNVarsAnd(scip, andcons);
            val = andnegs[c] ? -andcoefs[c] : andcoefs[c];
 
            /* lock variables */
            if( SCIPisPositive(scip, val) )
            {
               for( v = nandvars - 1; v >= 0; --v )
               {
                  SCIP_CALL( SCIPlockVarCons(scip, andvars[v], cons, FALSE, TRUE) );
               }
            }
            else
            {
               for( v = nandvars - 1; v >= 0; --v )
               {
                  SCIP_CALL( SCIPlockVarCons(scip, andvars[v], cons, TRUE, FALSE) );
               }
            }
         }
      }
      else if( !SCIPisInfinity(scip, oldrhs) && SCIPisInfinity(scip, rhs) )
      {
         /* non-linear part */
         for( c = consdata->nconsanddatas - 1; c >= 0; --c )
         {
            CONSANDDATA* consanddata;
            SCIP_CONS* andcons;
 
            consanddata = consdata->consanddatas[c];
            assert(consanddata != NULL);
 
            andcons = consanddata->cons;
            assert(andcons != NULL);
 
            andvars = SCIPgetVarsAnd(scip, andcons);
            nandvars = SCIPgetNVarsAnd(scip, andcons);
            val = andnegs[c] ? -andcoefs[c] : andcoefs[c];
 
            /* lock variables */
            if( SCIPisPositive(scip, val) )
            {
               for( v = nandvars - 1; v >= 0; --v )
               {
                  SCIP_CALL( SCIPunlockVarCons(scip, andvars[v], cons, FALSE, TRUE) );
               }
            }
            else
            {
               for( v = nandvars - 1; v >= 0; --v )
               {
                  SCIP_CALL( SCIPunlockVarCons(scip, andvars[v], cons, TRUE, FALSE) );
               }
            }
         }
      }
   }
 
   /* check whether the right hand side is decreased, if and only if that's the case we maybe can propagate, tighten and add more cliques */
   if( SCIPisGT(scip, oldrhs, rhs) )
   {
      consdata->propagated = FALSE;
   }
 
   /* set new right hand side and update constraint data */
   SCIP_CALL( chgRhsLinearCons(scip, consdata->lincons, consdata->linconstype, rhs) );
   consdata->rhs = rhs;
   consdata->presolved = FALSE;
   consdata->changed = TRUE;
 
   /* free temporary memory */
   SCIPfreeBufferArray(scip, &andnegs);
   SCIPfreeBufferArray(scip, &andcoefs);
   SCIPfreeBufferArray(scip, &andress);
   SCIPfreeBufferArray(scip, &lincoefs);
   SCIPfreeBufferArray(scip, &linvars);
   SCIPfreeBufferArray(scip, &coefs);
   SCIPfreeBufferArray(scip, &vars);
 
   return SCIP_OKAY;
}
 
/** create and-constraints and get all and-resultants */
static
SCIP_RETCODE createAndAddAnds(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONSHDLR*const   conshdlr,           /**< pseudoboolean constraint handler */
   SCIP_VAR**const*const terms,              /**< array of term variables to get and-constraints for */
   SCIP_Real*const       termcoefs,          /**< array of coefficients for and-constraints */
   int const             nterms,             /**< number of terms to get and-constraints for */
   int const*const       ntermvars,          /**< array of number of variable in each term */
   SCIP_Bool const       initial,            /**< should the LP relaxation of constraint be in the initial LP?
                                              *   Usually set to TRUE. Set to FALSE for 'lazy constraints'. */
   SCIP_Bool const       enforce,            /**< should the constraint be enforced during node processing?
                                              *   TRUE for model constraints, FALSE for additional, redundant
                                              *   constraints. */
   SCIP_Bool const       check,              /**< should the constraint be checked for feasibility?
                                              *   TRUE for model constraints, FALSE for additional, redundant
                                              *   constraints. */
   SCIP_Bool const       local,              /**< is constraint only valid locally?
                                              *   Usually set to FALSE. Has to be set to TRUE, e.g., for branching
                                              *   constraints. */
   SCIP_Bool const       modifiable,         /**< is constraint modifiable (subject to column generation)?
                                              *   Usually set to FALSE. In column generation applications, set to TRUE
                                              *   if pricing adds coefficients to this constraint. */
   SCIP_Bool const       dynamic,            /**< is constraint subject to aging?
                                              *   Usually set to FALSE. Set to TRUE for own cuts which
                                              *   are seperated as constraints. */
   SCIP_Bool const       stickingatnode,     /**< should the constraint always be kept at the node where it was added, even
                                              *   if it may be moved to a more global node?
                                              *   Usually set to FALSE. Set to TRUE to for constraints that represent
                                              *   node data. */
   SCIP_CONS**const      andconss,           /**< array to store all created and-constraints for given terms */
   SCIP_Real*const       andvals,            /**< array to store all coefficients of and-constraints */
   SCIP_Bool*const       andnegs,            /**< array to store negation status of and-constraints */
   int*const             nandconss           /**< number of created and constraints */
   )
{
   int t;
 
   assert(scip != NULL);
   assert(conshdlr != NULL);
   assert(nterms == 0 || (terms != NULL && ntermvars != NULL));
   assert(andconss != NULL);
   assert(andvals != NULL);
   assert(nandconss != NULL);
 
   (*nandconss) = 0;
 
   if( nterms == 0 )
      return SCIP_OKAY;
 
   /* loop over all terms and create/get all and constraints */
   for( t = 0; t < nterms; ++t )
   {
      if( !SCIPisZero(scip, termcoefs[t]) && ntermvars[t] > 0 )
      {
         SCIP_CALL( createAndAddAndCons(scip, conshdlr, terms[t], ntermvars[t],
               initial, enforce, check, local, modifiable, dynamic, stickingatnode,
               &(andconss[*nandconss])) );
         assert(andconss[*nandconss] != NULL);
         andvals[*nandconss] = termcoefs[t];
         andnegs[*nandconss] = FALSE;
         ++(*nandconss);
      }
   }
 
   return SCIP_OKAY;
}
 
/** created linear constraint of pseudo boolean constraint */
static
SCIP_RETCODE createAndAddLinearCons(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONSHDLR*const   conshdlr,           /**< pseudoboolean constraint handler */
   SCIP_VAR**const       linvars,            /**< linear variables */
   int const             nlinvars,           /**< number of linear variables */
   SCIP_Real*const       linvals,            /**< linear coefficients */
   SCIP_VAR**const       andress,            /**< and-resultant variables */
   int const             nandress,           /**< number of and-resultant variables */
   SCIP_Real const*const andvals,            /**< and-resultant coefficients */
   SCIP_Bool*const       andnegs,            /**< and-resultant negation status */
   SCIP_Real*const       lhs,                /**< pointer to left hand side of linear constraint */
   SCIP_Real*const       rhs,                /**< pointer to right hand side of linear constraint */
   SCIP_Bool const       issoftcons,         /**< is this a soft constraint */
   SCIP_Bool const       initial,            /**< should the LP relaxation of constraint be in the initial LP?
                                              *   Usually set to TRUE. Set to FALSE for 'lazy constraints'. */
   SCIP_Bool const       separate,           /**< should the constraint be separated during LP processing?
                                              *   Usually set to TRUE. */
   SCIP_Bool const       enforce,            /**< should the constraint be enforced during node processing?
                                              *   TRUE for model constraints, FALSE for additional, redundant
                                              *   constraints. */
   SCIP_Bool const       check,              /**< should the constraint be checked for feasibility?
                                              *   TRUE for model constraints, FALSE for additional, redundant
                                              *   constraints. */
   SCIP_Bool const       propagate,          /**< should the constraint be propagated during node processing?
                                              *   Usually set to TRUE. */
   SCIP_Bool const       local,              /**< is constraint only valid locally?
                                              *   Usually set to FALSE. Has to be set to TRUE, e.g., for branching
                                              *   constraints. */
   SCIP_Bool const       modifiable,         /**< is constraint modifiable (subject to column generation)?
                                              *   Usually set to FALSE. In column generation applications, set to TRUE
                                              *   if pricing adds coefficients to this constraint. */
   SCIP_Bool const       dynamic,            /**< is constraint subject to aging?
                                              *   Usually set to FALSE. Set to TRUE for own cuts which
                                              *   are seperated as constraints. */
   SCIP_Bool const       removable,          /**< should the relaxation be removed from the LP due to aging or cleanup?
                                              *   Usually set to FALSE. Set to TRUE for 'lazy constraints' and 'user
                                              *   cuts'. */
   SCIP_Bool const       stickingatnode,     /**< should the constraint always be kept at the node where it was added, even
                                              *   if it may be moved to a more global node?
                                              *   Usually set to FALSE. Set to TRUE to for constraints that represent
                                              *   node data. */
   SCIP_CONS**const      lincons,            /**< pointer to store created linear constraint */
   SCIP_LINEARCONSTYPE*const linconstype     /**< pointer to store the type of the linear constraint */
   )
{
   SCIP_CONSHDLRDATA* conshdlrdata;
   SCIP_CONSHDLR* upgrconshdlr;
   SCIP_CONS* cons;
   char name[SCIP_MAXSTRLEN];
   int v;
   SCIP_Bool created;
   SCIP_Bool integral;
   int nzero;
   int ncoeffspone;
   int ncoeffsnone;
   int ncoeffspint;
   int ncoeffsnint;
 
   assert(scip != NULL);
   assert(conshdlr != NULL);
   assert(nlinvars == 0 || (linvars != NULL && linvals != NULL));
   assert(nandress == 0 || (andress != NULL && andvals != NULL));
   assert(lhs != NULL);
   assert(rhs != NULL);
   assert(lincons != NULL);
   assert(linconstype != NULL);
   assert(nlinvars > 0 || nandress > 0);
 
   conshdlrdata = SCIPconshdlrGetData(conshdlr);
   assert(conshdlrdata != NULL);
 
   (*linconstype) = SCIP_LINEARCONSTYPE_INVALIDCONS;
   (*lincons) = NULL;
   cons = NULL;
 
   (void)SCIPsnprintf(name, SCIP_MAXSTRLEN, "pseudoboolean_linear%d", conshdlrdata->nlinconss);
   ++(conshdlrdata->nlinconss);
 
   created = FALSE;
 
   if( !modifiable )
   {
      SCIP_Real val;
      int nvars;
 
      /* calculate some statistics for upgrading on linear constraint */
      nzero = 0;
      ncoeffspone = 0;
      ncoeffsnone = 0;
      ncoeffspint = 0;
      ncoeffsnint = 0;
      integral = TRUE;
      nvars = nlinvars + nandress;
 
      /* calculate information over linear part */
      for( v = nlinvars - 1; v >= 0; --v )
      {
         val = linvals[v];
 
         if( SCIPisZero(scip, val) )
         {
            ++nzero;
            continue;
         }
         if( SCIPisEQ(scip, val, 1.0) )
            ++ncoeffspone;
         else if( SCIPisEQ(scip, val, -1.0) )
            ++ncoeffsnone;
         else if( SCIPisIntegral(scip, val) )
         {
            if( SCIPisPositive(scip, val) )
               ++ncoeffspint;
            else
               ++ncoeffsnint;
         }
         else
         {
            integral = FALSE;
            break;
         }
      }
 
      if( integral )
      {
         /* calculate information over and-resultants */
         for( v = nandress - 1; v >= 0; --v )
         {
            val = andvals[v];
 
            if( SCIPisZero(scip, val) )
            {
               ++nzero;
               continue;
            }
            if( SCIPisEQ(scip, val, 1.0) )
               ++ncoeffspone;
            else if( SCIPisEQ(scip, val, -1.0) )
               ++ncoeffsnone;
            else if( SCIPisIntegral(scip, val) )
            {
               if( SCIPisPositive(scip, val) )
                  ++ncoeffspint;
               else
                  ++ncoeffsnint;
            }
            else
            {
               integral = FALSE;
               break;
            }
         }
      }
 
      SCIPdebugMsg(scip, "While creating the linear constraint of the pseudoboolean constraint we found %d zero coefficients that were removed\n", nzero);
 
      /* try to upgrade to a special linear constraint */
      if( integral )
      {
         upgrconshdlr = SCIPfindConshdlr(scip, "logicor");
 
         /* check, if linear constraint can be upgraded to logic or constraint
          * - logic or constraints consist only of binary variables with a
          *   coefficient of +1.0 or -1.0 (variables with -1.0 coefficients can be negated):
          *        lhs     <= x1 + ... + xp - y1 - ... - yn <= rhs
          * - negating all variables y = (1-Y) with negative coefficients gives:
          *        lhs + n <= x1 + ... + xp + Y1 + ... + Yn <= rhs + n
          * - negating all variables x = (1-X) with positive coefficients and multiplying with -1 gives:
          *        p - rhs <= X1 + ... + Xp + y1 + ... + yn <= p - lhs
          * - logic or constraints have left hand side of +1.0, and right hand side of +infinity: x(S) >= 1.0
          *    -> without negations:  (lhs == 1 - n  and  rhs == +inf)  or  (lhs == -inf  and  rhs = p - 1)
          */
         if( upgrconshdlr != NULL && nvars > 2 && ncoeffspone + ncoeffsnone == nvars
            && ((SCIPisEQ(scip, *lhs, 1.0 - ncoeffsnone) && SCIPisInfinity(scip, *rhs))
               || (SCIPisInfinity(scip, -*lhs) && SCIPisEQ(scip, *rhs, ncoeffspone - 1.0))) )
         {
            SCIP_VAR** transvars;
            int mult;
 
            SCIPdebugMsg(scip, "linear constraint will be logic-or constraint\n");
 
            /* check, if we have to multiply with -1 (negate the positive vars) or with +1 (negate the negative vars) */
            mult = SCIPisInfinity(scip, *rhs) ? +1 : -1;
 
            /* get temporary memory */
            SCIP_CALL( SCIPallocBufferArray(scip, &transvars, nvars) );
 
            /* negate positive or negative variables */
            for( v = 0; v < nlinvars; ++v )
            {
               if( mult * linvals[v] > 0.0 )
                  transvars[v] = linvars[v];
               else
               {
                  SCIP_CALL( SCIPgetNegatedVar(scip, linvars[v], &transvars[v]) );
               }
               assert(transvars[v] != NULL);
            }
 
            /* negate positive or negative variables */
            for( v = 0; v < nandress; ++v )
            {
               if( mult * andvals[v] > 0.0 )
                  transvars[nlinvars + v] = andress[v];
               else
               {
                  SCIP_CALL( SCIPgetNegatedVar(scip, andress[v], &transvars[nlinvars + v]) );
                  andnegs[v] = TRUE;
               }
               assert(transvars[nlinvars + v] != NULL);
            }
 
            assert(!modifiable);
            /* create the constraint */
            SCIP_CALL( SCIPcreateConsLogicor(scip, &cons, name, nvars, transvars,
                  initial, separate, enforce, check, propagate, local, modifiable, dynamic, removable, stickingatnode) );
 
            created = TRUE;
            (*linconstype) = SCIP_LINEARCONSTYPE_LOGICOR;
 
            /* free temporary memory */
            SCIPfreeBufferArray(scip, &transvars);
 
            *lhs = 1.0;
            *rhs = SCIPinfinity(scip);
         }
 
         upgrconshdlr = SCIPfindConshdlr(scip, "setppc");
 
         /* check, if linear constraint can be upgraded to set partitioning, packing, or covering constraint
          * - all set partitioning / packing / covering constraints consist only of binary variables with a
          *   coefficient of +1.0 or -1.0 (variables with -1.0 coefficients can be negated):
          *        lhs     <= x1 + ... + xp - y1 - ... - yn <= rhs
          * - negating all variables y = (1-Y) with negative coefficients gives:
          *        lhs + n <= x1 + ... + xp + Y1 + ... + Yn <= rhs + n
          * - negating all variables x = (1-X) with positive coefficients and multiplying with -1 gives:
          *        p - rhs <= X1 + ... + Xp + y1 + ... + yn <= p - lhs
          * - a set partitioning constraint has left hand side of +1.0, and right hand side of +1.0 : x(S) == 1.0
          *    -> without negations:  lhs == rhs == 1 - n  or  lhs == rhs == p - 1
          * - a set packing constraint has left hand side of -infinity, and right hand side of +1.0 : x(S) <= 1.0
          *    -> without negations:  (lhs == -inf  and  rhs == 1 - n)  or  (lhs == p - 1  and  rhs = +inf)
          * - a set covering constraint has left hand side of +1.0, and right hand side of +infinity: x(S) >= 1.0
          *    -> without negations:  (lhs == 1 - n  and  rhs == +inf)  or  (lhs == -inf  and  rhs = p - 1)
          */
         if( upgrconshdlr != NULL && !created && ncoeffspone + ncoeffsnone == nvars )
         {
            SCIP_VAR** transvars;
            int mult;
 
            if( SCIPisEQ(scip, *lhs, *rhs) && (SCIPisEQ(scip, *lhs, 1.0 - ncoeffsnone) || SCIPisEQ(scip, *lhs, ncoeffspone - 1.0)) )
            {
               SCIPdebugMsg(scip, "linear pseudoboolean constraint will be a set partitioning constraint\n");
 
               /* check, if we have to multiply with -1 (negate the positive vars) or with +1 (negate the negative vars) */
               mult = SCIPisEQ(scip, *lhs, 1.0 - ncoeffsnone) ? +1 : -1;
 
               /* get temporary memory */
               SCIP_CALL( SCIPallocBufferArray(scip, &transvars, nvars) );
 
               /* negate positive or negative variables for linear variables */
               for( v = 0; v < nlinvars; ++v )
               {
                  if( mult * linvals[v] > 0.0 )
                     transvars[v] = linvars[v];
                  else
                  {
                     SCIP_CALL( SCIPgetNegatedVar(scip, linvars[v], &transvars[v]) );
                  }
                  assert(transvars[v] != NULL);
               }
 
               /* negate positive or negative variables for and-resultants */
               for( v = 0; v < nandress; ++v )
               {
                  if( mult * andvals[v] > 0.0 )
                     transvars[nlinvars + v] = andress[v];
                  else
                  {
                     SCIP_CALL( SCIPgetNegatedVar(scip, andress[v], &transvars[nlinvars + v]) );
                     andnegs[v] = TRUE;
                  }
                  assert(transvars[nlinvars + v] != NULL);
               }
 
               /* create the constraint */
               assert(!modifiable);
               SCIP_CALL( SCIPcreateConsSetpart(scip, &cons, name, nvars, transvars,
                     initial, separate, enforce, check, propagate, local, modifiable, dynamic, removable, stickingatnode) );
 
               created = TRUE;
               (*linconstype) = SCIP_LINEARCONSTYPE_SETPPC;
 
               /* release temporary memory */
               SCIPfreeBufferArray(scip, &transvars);
 
               *lhs = 1.0;
               *rhs = 1.0;
            }
            else if( (SCIPisInfinity(scip, -*lhs) && SCIPisEQ(scip, *rhs, 1.0 - ncoeffsnone))
               || (SCIPisEQ(scip, *lhs, ncoeffspone - 1.0) && SCIPisInfinity(scip, *rhs)) )
            {
               SCIPdebugMsg(scip, "linear pseudoboolean constraint will be a set packing constraint\n");
 
               /* check, if we have to multiply with -1 (negate the positive vars) or with +1 (negate the negative vars) */
               mult = SCIPisInfinity(scip, -*lhs) ? +1 : -1;
 
               /* get temporary memory */
               SCIP_CALL( SCIPallocBufferArray(scip, &transvars, nvars) );
 
               /* negate positive or negative variables for linear variables */
               for( v = 0; v < nlinvars; ++v )
               {
                  if( mult * linvals[v] > 0.0 )
                     transvars[v] = linvars[v];
                  else
                  {
                     SCIP_CALL( SCIPgetNegatedVar(scip, linvars[v], &transvars[v]) );
                  }
                  assert(transvars[v] != NULL);
               }
 
               /* negate positive or negative variables for and-resultants*/
               for( v = 0; v < nandress; ++v )
               {
                  if( mult * andvals[v] > 0.0 )
                     transvars[nlinvars + v] = andress[v];
                  else
                  {
                     SCIP_CALL( SCIPgetNegatedVar(scip, andress[v], &transvars[nlinvars + v]) );
                     andnegs[v] = TRUE;
                  }
                  assert(transvars[nlinvars + v] != NULL);
               }
 
               /* create the constraint */
               assert(!modifiable);
               SCIP_CALL( SCIPcreateConsSetpack(scip, &cons, name, nvars, transvars,
                     initial, separate, enforce, check, propagate, local, modifiable, dynamic, removable, stickingatnode) );
 
               created = TRUE;
               (*linconstype) = SCIP_LINEARCONSTYPE_SETPPC;
 
               /* release temporary memory */
               SCIPfreeBufferArray(scip, &transvars);
 
               *lhs = -SCIPinfinity(scip);
               *rhs = 1.0;
            }
            else if( (SCIPisEQ(scip, *lhs, 1.0 - ncoeffsnone) && SCIPisInfinity(scip, *rhs))
               || (SCIPisInfinity(scip, -*lhs) && SCIPisEQ(scip, *rhs, ncoeffspone - 1.0)) )
            {
               if( nvars != 1 )
               {
                  if( nvars == 2 )
                  {
                     SCIPwarningMessage(scip, "Does not expect this, because this constraint should be a set packing constraint.\n");
                  }
                  else
                  {
                     SCIPwarningMessage(scip, "Does not expect this, because this constraint should be a logicor constraint.\n");
                  }
               }
               SCIPdebugMsg(scip, "linear pseudoboolean constraint will be a set covering constraint\n");
 
               /* check, if we have to multiply with -1 (negate the positive vars) or with +1 (negate the negative vars) */
               mult = SCIPisInfinity(scip, *rhs) ? +1 : -1;
 
               /* get temporary memory */
               SCIP_CALL( SCIPallocBufferArray(scip, &transvars, nvars) );
 
               /* negate positive or negative variables for linear variables */
               for( v = 0; v < nlinvars; ++v )
               {
                  if( mult * linvals[v] > 0.0 )
                     transvars[v] = linvars[v];
                  else
                  {
                     SCIP_CALL( SCIPgetNegatedVar(scip, linvars[v], &transvars[v]) );
                  }
                  assert(transvars[v] != NULL);
               }
 
               /* negate positive or negative variables for and-resultants*/
               for( v = 0; v < nandress; ++v )
               {
                  if( mult * andvals[v] > 0.0 )
                     transvars[nlinvars + v] = andress[v];
                  else
                  {
                     SCIP_CALL( SCIPgetNegatedVar(scip, andress[v], &transvars[nlinvars + v]) );
                     andnegs[v] = TRUE;
                  }
                  assert(transvars[nlinvars + v] != NULL);
               }
 
               /* create the constraint */
               assert(!modifiable);
               SCIP_CALL( SCIPcreateConsSetcover(scip, &cons, name, nvars, transvars,
                     initial, separate, enforce, check, propagate, local, modifiable, dynamic, removable, stickingatnode) );
 
               created = TRUE;
               (*linconstype) = SCIP_LINEARCONSTYPE_SETPPC;
 
               /* release temporary memory */
               SCIPfreeBufferArray(scip, &transvars);
 
               *lhs = 1.0;
               *rhs = SCIPinfinity(scip);
            }
         }
 
         upgrconshdlr = SCIPfindConshdlr(scip, "knapsack");
 
         /* check, if linear constraint can be upgraded to a knapsack constraint
          * - all variables must be binary
          * - all coefficients must be integral
          * - exactly one of the sides must be infinite
          */
         if( upgrconshdlr != NULL && !created && (ncoeffspone + ncoeffsnone + ncoeffspint + ncoeffsnint == nvars) && (SCIPisInfinity(scip, -*lhs) != SCIPisInfinity(scip, *rhs)) )
         {
            SCIP_VAR** transvars;
            SCIP_Longint* weights;
            SCIP_Longint capacity;
            SCIP_Longint weight;
            int mult;
 
            SCIPdebugMsg(scip, "linear pseudoboolean constraint will be a knapsack constraint\n");
 
            /* get temporary memory */
            SCIP_CALL( SCIPallocBufferArray(scip, &transvars, nvars) );
            SCIP_CALL( SCIPallocBufferArray(scip, &weights, nvars) );
 
            /* if the right hand side is non-infinite, we have to negate all variables with negative coefficient;
             * otherwise, we have to negate all variables with positive coefficient and multiply the row with -1
             */
            if( SCIPisInfinity(scip, *rhs) )
            {
               mult = -1;
               capacity = (SCIP_Longint)SCIPfeasFloor(scip, -*lhs);
            }
            else
            {
               mult = +1;
               capacity = (SCIP_Longint)SCIPfeasFloor(scip, *rhs);
            }
 
            /* negate positive or negative variables for linear variables */
            for( v = 0; v < nlinvars; ++v )
            {
               assert(SCIPisFeasIntegral(scip, linvals[v]));
               weight = mult * (SCIP_Longint)SCIPfeasFloor(scip, linvals[v]);
               if( weight > 0 )
               {
                  transvars[v] = linvars[v];
                  weights[v] = weight;
               }
               else
               {
                  SCIP_CALL( SCIPgetNegatedVar(scip, linvars[v], &transvars[v]) );
                  weights[v] = -weight;
                  capacity -= weight;
               }
               assert(transvars[v] != NULL);
            }
            /* negate positive or negative variables for and-resultants */
            for( v = 0; v < nandress; ++v )
            {
               assert(SCIPisFeasIntegral(scip, andvals[v]));
               weight = mult * (SCIP_Longint)SCIPfeasFloor(scip, andvals[v]);
               if( weight > 0 )
               {
                  transvars[nlinvars + v] = andress[v];
                  weights[nlinvars + v] = weight;
               }
               else
               {
                  SCIP_CALL( SCIPgetNegatedVar(scip, andress[v], &transvars[nlinvars + v]) );
                  andnegs[v] = TRUE;
                  weights[nlinvars + v] = -weight;
                  capacity -= weight;
               }
               assert(transvars[nlinvars + v] != NULL);
            }
 
            /* create the constraint */
            SCIP_CALL( SCIPcreateConsKnapsack(scip, &cons, name, nvars, transvars, weights, capacity,
                  initial, separate, enforce, check, propagate, local, modifiable, dynamic, removable, stickingatnode) );
 
            created = TRUE;
            (*linconstype) = SCIP_LINEARCONSTYPE_KNAPSACK;
 
            /* free temporary memory */
            SCIPfreeBufferArray(scip, &weights);
            SCIPfreeBufferArray(scip, &transvars);
 
            *lhs = -SCIPinfinity(scip);
            *rhs = capacity;
         }
#ifdef WITHEQKNAPSACK
 
         upgrconshdlr = SCIPfindConshdlr(scip, "eqknapsack");
 
         /* check, if linear constraint can be upgraded to a knapsack constraint
          * - all variables must be binary
          * - all coefficients must be integral
          * - both sides must be infinite
          */
         if( upgrconshdlr != NULL && !created && (ncoeffspone + ncoeffsnone + ncoeffspint + ncoeffsnint == nvars) && SCIPisEQ(scip, *lhs, *rhs) )
         {
            SCIP_VAR** transvars;
            SCIP_Longint* weights;
            SCIP_Longint capacity;
            SCIP_Longint weight;
            int mult;
 
            assert(!SCIPisInfinity(scip, *rhs));
 
            SCIPdebugMsg(scip, "linear pseudoboolean constraint will be a equality-knapsack constraint\n");
 
            /* get temporary memory */
            SCIP_CALL( SCIPallocBufferArray(scip, &transvars, nvars) );
            SCIP_CALL( SCIPallocBufferArray(scip, &weights, nvars) );
 
            if( SCIPisPositive(scip, *rhs) )
            {
               mult = +1;
               capacity = (SCIP_Longint)SCIPfeasFloor(scip, *rhs);
            }
            else
            {
               mult = -1;
               capacity = (SCIP_Longint)SCIPfeasFloor(scip, -*rhs);
            }
 
            /* negate positive or negative variables for linear variables */
            for( v = 0; v < nlinvars; ++v )
            {
               assert(SCIPisFeasIntegral(scip, linvals[v]));
               weight = mult * (SCIP_Longint)SCIPfeasFloor(scip, linvals[v]);
               if( weight > 0 )
               {
                  transvars[v] = linvars[v];
                  weights[v] = weight;
               }
               else
               {
                  SCIP_CALL( SCIPgetNegatedVar(scip, linvars[v], &transvars[v]) );
                  weights[v] = -weight;
                  capacity -= weight;
               }
               assert(transvars[v] != NULL);
            }
            /* negate positive or negative variables for and-resultants */
            for( v = 0; v < nandress; ++v )
            {
               assert(SCIPisFeasIntegral(scip, andvals[v]));
               weight = mult * (SCIP_Longint)SCIPfeasFloor(scip, andvals[v]);
               if( weight > 0 )
               {
                  transvars[nlinvars + v] = andress[v];
                  weights[nlinvars + v] = weight;
               }
               else
               {
                  SCIP_CALL( SCIPgetNegatedVar(scip, andress[v], &transvars[nlinvars + v]) );
                  andnegs[v] = TRUE;
                  weights[nlinvars + v] = -weight;
                  capacity -= weight;
               }
               assert(transvars[nlinvars + v] != NULL);
            }
 
            /* create the constraint */
            SCIP_CALL( SCIPcreateConsEqKnapsack(scip, &cons, name, nvars, transvars, weights, capacity,
                  initial, separate, enforce, check, propagate, local, modifiable, dynamic, removable, stickingatnode) );
 
            created = TRUE;
            (*linconstype) = SCIP_LINEARCONSTYPE_EQKNAPSACK;
 
            /* free temporary memory */
            SCIPfreeBufferArray(scip, &weights);
            SCIPfreeBufferArray(scip, &transvars);
 
            *lhs = capacity;
            *rhs = capacity;
         }
#endif
      }
   }
 
   upgrconshdlr = SCIPfindConshdlr(scip, "linear");
   assert(created || upgrconshdlr != NULL);
 
   if( !created )
   {
      SCIP_CALL( SCIPcreateConsLinear(scip, &cons, name, nlinvars, linvars, linvals, *lhs, *rhs,
            initial, separate, enforce, check, propagate, local, modifiable, dynamic, removable, stickingatnode) );
 
      (*linconstype) = SCIP_LINEARCONSTYPE_LINEAR;
 
      /* add all and-resultants */
      for( v = 0; v < nandress; ++v )
      {
         assert(andress[v] != NULL);
 
         /* add auxiliary variables to linear constraint */
         SCIP_CALL( SCIPaddCoefLinear(scip, cons, andress[v], andvals[v]) );
      }
   }
 
   assert(cons != NULL && *linconstype > SCIP_LINEARCONSTYPE_INVALIDCONS);
   SCIPdebugPrintCons(scip, cons, NULL);
   *lincons = cons;
 
   /* @todo: add indicator variable */
   /* add hard constraint */
   if( !issoftcons )
   {
      SCIP_CALL( SCIPaddCons(scip, cons) );
 
      /* mark linear constraint not to be upgraded - otherwise we loose control over it */
      SCIP_CALL( SCIPcaptureCons(scip, cons) );
      SCIPconsAddUpgradeLocks(cons, 1);
      SCIP_CALL( SCIPreleaseCons(scip, &cons) );
   }
 
   return SCIP_OKAY;
}
 
/** checks one original pseudoboolean constraint for feasibility of given solution */
static
SCIP_RETCODE checkOrigPbCons(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< pseudo boolean constraint */
   SCIP_SOL*const        sol,                /**< solution to be checked, or NULL for current solution */
   SCIP_Bool*const       violated,           /**< pointer to store whether the constraint is violated */
   SCIP_Bool const       printreason         /**< should violation of constraint be printed */
   )
{
   SCIP_CONSDATA* consdata;
   SCIP_CONSHDLR* conshdlr;
   SCIP_CONSHDLRDATA* conshdlrdata;
 
   SCIP_VAR** vars;
   SCIP_Real* coefs;
   SCIP_Real lhs;
   SCIP_Real rhs;
   SCIP_Real activity;
   int nvars;
   int v;
 
   SCIP_Real lhsviol;
   SCIP_Real rhsviol;
   SCIP_Real absviol;
   SCIP_Real relviol;
 
   assert(scip != NULL);
   assert(cons != NULL);
   assert(SCIPconsIsOriginal(cons));
   assert(violated != NULL);
 
   *violated = FALSE;
 
   SCIPdebugMsg(scip, "checking original pseudo boolean constraint <%s>\n", SCIPconsGetName(cons));
   SCIPdebugPrintCons(scip, cons, NULL);
 
   consdata = SCIPconsGetData(cons);
   assert(consdata != NULL);
   assert(consdata->lincons != NULL);
   assert(consdata->linconstype > SCIP_LINEARCONSTYPE_INVALIDCONS);
   assert(SCIPconsIsOriginal(consdata->lincons));
 
   /* gets number of variables in linear constraint */
   SCIP_CALL( getLinearConsNVars(scip, consdata->lincons, consdata->linconstype, &nvars) );
 
   /* allocate temporary memory */
   SCIP_CALL( SCIPallocBufferArray(scip, &vars, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &coefs, nvars) );
 
   /* get sides of linear constraint */
   SCIP_CALL( getLinearConsSides(scip, consdata->lincons, consdata->linconstype, &lhs, &rhs) );
   assert(!SCIPisInfinity(scip, lhs));
   assert(!SCIPisInfinity(scip, -rhs));
   assert(SCIPisLE(scip, lhs, rhs));
 
   /* get variables and coefficient of linear constraint */
   SCIP_CALL( getLinearConsVarsData(scip, consdata->lincons, consdata->linconstype, vars, coefs, &nvars) );
   assert(nvars == 0 || (coefs != NULL));
 
   /* every variable in the linear constraint is either a linear variable or a term variable
    * but there can be additional fixed or negation-paired and-resultants with relevant and-constraints
    * whose values are already resolved in the linear constraint
    */
   assert(consdata->nlinvars + consdata->nconsanddatas >= nvars);
 
   conshdlr = SCIPconsGetHdlr(cons);
   assert(conshdlr != NULL);
 
   conshdlrdata = SCIPconshdlrGetData(conshdlr);
   assert(conshdlrdata != NULL);
   assert(conshdlrdata->hashmap != NULL);
 
   activity = 0.0;
 
   /* compute pseudoboolean activity */
   for( v = 0; v < nvars; ++v )
   {
      CONSANDDATA* consanddata = NULL;
      SCIP_VAR* var = vars[v];
      SCIP_Real solval;
 
      /* find and-constraint to standard or negated and-resultant */
      do
      {
         consanddata = (CONSANDDATA*)SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)var);
 
         if( consanddata != NULL )
            break;
 
         var = var == vars[v] ? SCIPvarGetNegatedVar(var) : vars[v];
      }
      while( var != vars[v] );
 
      /* get linear solution */
      if( consanddata == NULL )
         solval = SCIPgetSolVal(scip, sol, vars[v]);
      /* get term solution */
      else
      {
         SCIP_CONS* andcons = consanddata->origcons;
         SCIP_VAR** andvars;
         int nandvars;
         int i;
 
         /* use transformed constraint if no original constraint exists */
         if( andcons == NULL )
            andcons = consanddata->cons;
 
         assert(SCIPgetResultantAnd(scip, andcons) == var);
 
         andvars = SCIPgetVarsAnd(scip, andcons);
         nandvars = SCIPgetNVarsAnd(scip, andcons);
         assert(nandvars == 0 || andvars != NULL);
 
         solval = 1.0;
 
         for( i = 0; i < nandvars; ++i )
            solval *= SCIPgetSolVal(scip, sol, andvars[i]);
 
         if( var != vars[v] )
            solval = 1.0 - solval;
      }
 
      /* add activity contribution */
      activity += coefs[v] * solval;
   }
 
   SCIPdebugMsg(scip, "lhs = %g, activity = %g, rhs = %g\n", lhs, activity, rhs);
 
   /* calculate absolute and relative violation */
   lhsviol = lhs - activity;
   rhsviol = activity - rhs;
 
   if(lhsviol > rhsviol)
   {
      absviol = lhsviol;
      relviol = SCIPrelDiff(lhs, activity);
   }
   else
   {
      absviol = rhsviol;
      relviol = SCIPrelDiff(activity, rhs);
   }
 
   /* update absolute and relative violation of the solution */
   if( sol != NULL )
      SCIPupdateSolConsViolation(scip, sol, absviol, relviol);
 
   /* check left hand side for violation */
   if( SCIPisFeasLT(scip, activity, lhs) )
   {
      if( printreason )
      {
         SCIP_CALL( SCIPprintCons(scip, cons, NULL ) );
         SCIPinfoMessage(scip, NULL, ";\n");
         SCIPinfoMessage(scip, NULL, "violation: left hand side is violated by %.15g\n", lhs - activity);
 
         /* print linear constraint in SCIP_DEBUG mode too */
         SCIPdebugPrintCons(scip, SCIPconsGetData(cons)->lincons, NULL);
      }
 
      *violated = TRUE;
   }
 
   /* check right hand side for violation */
   if( SCIPisFeasGT(scip, activity, rhs) )
   {
      if( printreason )
      {
         SCIP_CALL( SCIPprintCons(scip, cons, NULL ) );
         SCIPinfoMessage(scip, NULL, ";\n");
         SCIPinfoMessage(scip, NULL, "violation: right hand side is violated by %.15g\n", activity - rhs);
      }
 
      *violated = TRUE;
   }
 
   /* free temporary memory */
   SCIPfreeBufferArray(scip, &coefs);
   SCIPfreeBufferArray(scip, &vars);
 
   return SCIP_OKAY;
}
 
/** checks all and-constraints inside the pseudoboolean constraint handler for feasibility of given solution or current
 *  solution
 */
static
SCIP_RETCODE checkAndConss(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONSHDLR*const   conshdlr,           /**< pseudo boolean constraint handler */
   SCIP_SOL*const        sol,                /**< solution to be checked, or NULL for current solution */
   SCIP_Bool*const       violated            /**< pointer to store whether the constraint is violated */
   )
{
   SCIP_CONSHDLRDATA* conshdlrdata;
   SCIP_CONS* andcons;
   SCIP_VAR** vars;
   SCIP_VAR* res;
   int nvars;
   int c;
   int v;
 
   assert(scip != NULL);
   assert(conshdlr != NULL);
   assert(violated != NULL);
 
   conshdlrdata = SCIPconshdlrGetData(conshdlr);
   assert(conshdlrdata != NULL);
 
   *violated = FALSE;
 
   for( c = conshdlrdata->nallconsanddatas - 1; c >= 0; --c )
   {
      SCIP_Real solval;
      SCIP_Real minsolval;
      SCIP_Real sumsolval;
      SCIP_Real viol;
 
      if( !conshdlrdata->allconsanddatas[c]->istransformed )
         continue;
 
      andcons = conshdlrdata->allconsanddatas[c]->cons;
 
      /* need to check even locally deleted constraints */
      if( andcons == NULL ) /*|| !SCIPconsIsActive(andcons) )*/
         continue;
 
      vars = SCIPgetVarsAnd(scip, andcons);
      nvars = SCIPgetNVarsAnd(scip, andcons);
      res = SCIPgetResultantAnd(scip, andcons);
      assert(nvars == 0 || (vars != NULL && res != NULL));
 
      /* check if the and-constraint is violated */
      minsolval = 1.0;
      sumsolval = 0.0;
      for( v = nvars - 1; v >= 0; --v )
      {
         solval = SCIPgetSolVal(scip, sol, vars[v]);
 
         if( solval < minsolval )
            minsolval = solval;
 
         sumsolval += solval;
      }
 
      /* the resultant must be at most as large as every operator
       * and at least as large as one minus the sum of negated operators
       */
      solval = SCIPgetSolVal(scip, sol, res);
      viol = MAX3(0.0, solval - minsolval, sumsolval - (nvars - 1.0 + solval));
 
      if( SCIPisFeasPositive(scip, viol) )
      {
         /* only reset constraint age if we are in enforcement */
         if( sol == NULL )
         {
            SCIP_CALL( SCIPresetConsAge(scip, andcons) );
         }
 
         *violated = TRUE;
         break;
      }
      else if( sol == NULL )
      {
         SCIP_CALL( SCIPincConsAge(scip, andcons) );
      }
   }
 
   return SCIP_OKAY;
}
 
/** creates by copying and captures a linear constraint */
static
SCIP_RETCODE copyConsPseudoboolean(
   SCIP*const            targetscip,         /**< target SCIP data structure */
   SCIP_CONS**           targetcons,         /**< pointer to store the created target constraint */
   SCIP*const            sourcescip,         /**< source SCIP data structure */
   SCIP_CONS*const       sourcecons,         /**< source constraint which will be copied */
   const char*           name,               /**< name of constraint */
   SCIP_HASHMAP*const    varmap,             /**< a SCIP_HASHMAP mapping variables of the source SCIP to corresponding
                                              *   variables of the target SCIP */
   SCIP_HASHMAP*const    consmap,            /**< a hashmap to store the mapping of source constraints to the corresponding
                                              *   target constraints */
   SCIP_Bool const       initial,            /**< should the LP relaxation of constraint be in the initial LP? */
   SCIP_Bool const       separate,           /**< should the constraint be separated during LP processing? */
   SCIP_Bool const       enforce,            /**< should the constraint be enforced during node processing? */
   SCIP_Bool const       check,              /**< should the constraint be checked for feasibility? */
   SCIP_Bool const       propagate,          /**< should the constraint be propagated during node processing? */
   SCIP_Bool const       local,              /**< is constraint only valid locally? */
   SCIP_Bool const       modifiable,         /**< is constraint modifiable (subject to column generation)? */
   SCIP_Bool const       dynamic,            /**< is constraint subject to aging? */
   SCIP_Bool const       removable,          /**< should the relaxation be removed from the LP due to aging or cleanup? */
   SCIP_Bool const       stickingatnode,     /**< should the constraint always be kept at the node where it was added, even
                                              *   if it may be moved to a more global node? */
   SCIP_Bool const       global,             /**< create a global or a local copy? */
   SCIP_Bool*const       valid               /**< pointer to store if the copying was valid */
   )
{
   SCIP_CONSDATA* sourceconsdata;
   SCIP_CONS* sourcelincons;
 
   assert(targetscip != NULL);
   assert(targetcons != NULL);
   assert(sourcescip != NULL);
   assert(sourcecons != NULL);
   assert(strcmp(SCIPconshdlrGetName(SCIPconsGetHdlr(sourcecons)), CONSHDLR_NAME) == 0);
   assert(valid != NULL);
 
   *valid = TRUE;
 
   sourceconsdata = SCIPconsGetData(sourcecons);
   assert(sourceconsdata != NULL);
 
   /* get linear constraint */
   sourcelincons = sourceconsdata->lincons;
   assert(sourcelincons != NULL);
 
   /* get copied version of linear constraint */
   if( !SCIPconsIsDeleted(sourcelincons) )
   {
      SCIP_CONSHDLR* conshdlrlinear;
      SCIP_CONS* targetlincons;
      SCIP_CONS** targetandconss;
      SCIP_Real* targetandcoefs;
      int ntargetandconss;
      SCIP_LINEARCONSTYPE targetlinconstype;
 
      targetlinconstype = sourceconsdata->linconstype;
 
      switch( targetlinconstype )
      {
      case SCIP_LINEARCONSTYPE_LINEAR:
         conshdlrlinear = SCIPfindConshdlr(sourcescip, "linear");
         assert(conshdlrlinear != NULL);
         break;
      case SCIP_LINEARCONSTYPE_LOGICOR:
         conshdlrlinear = SCIPfindConshdlr(sourcescip, "logicor");
         assert(conshdlrlinear != NULL);
         break;
      case SCIP_LINEARCONSTYPE_KNAPSACK:
         conshdlrlinear = SCIPfindConshdlr(sourcescip, "knapsack");
         assert(conshdlrlinear != NULL);
         break;
      case SCIP_LINEARCONSTYPE_SETPPC:
         conshdlrlinear = SCIPfindConshdlr(sourcescip, "setppc");
         assert(conshdlrlinear != NULL);
         break;
#ifdef WITHEQKNAPSACK
      case SCIP_LINEARCONSTYPE_EQKNAPSACK:
         conshdlrlinear = SCIPfindConshdlr(sourcescip, "eqknapsack");
         assert(conshdlrlinear != NULL);
         break;
#endif
      case SCIP_LINEARCONSTYPE_INVALIDCONS:
      default:
         SCIPerrorMessage("unknown linear constraint type\n");
         return SCIP_INVALIDDATA;
      }
 
      if( conshdlrlinear == NULL ) /*lint !e774*/
      {
         SCIPerrorMessage("linear constraint handler not found\n");
         return SCIP_INVALIDDATA;
      }
 
      targetlincons = NULL;
 
      /* copy linear constraint */
      SCIP_CALL( SCIPgetConsCopy(sourcescip, targetscip, sourcelincons, &targetlincons, conshdlrlinear, varmap, consmap, SCIPconsGetName(sourcelincons),
            SCIPconsIsInitial(sourcelincons), SCIPconsIsSeparated(sourcelincons), SCIPconsIsEnforced(sourcelincons), SCIPconsIsChecked(sourcelincons),
            SCIPconsIsPropagated(sourcelincons), SCIPconsIsLocal(sourcelincons), SCIPconsIsModifiable(sourcelincons), SCIPconsIsDynamic(sourcelincons),
            SCIPconsIsRemovable(sourcelincons), SCIPconsIsStickingAtNode(sourcelincons), global, valid) );
 
      if( *valid )
      {
         assert(targetlincons != NULL);
         assert(SCIPconsGetHdlr(targetlincons) != NULL);
         /* @note due to copying special linear constraints, now leads only to simple linear constraints, we check that
          *       our target constraint handler is the same as our source constraint handler of the linear constraint,
          *       if copying was not valid
          */
         if( strcmp(SCIPconshdlrGetName(SCIPconsGetHdlr(targetlincons)), "linear") == 0 )
            targetlinconstype = SCIP_LINEARCONSTYPE_LINEAR;
      }
 
      targetandconss = NULL;
      targetandcoefs = NULL;
      ntargetandconss = 0;
 
      if( *valid )
      {
         SCIP_CONSHDLR* conshdlrand;
         int c;
         int nsourceandconss;
         SCIP_HASHTABLE* linconsvarsmap;
         SCIP_VAR** targetlinvars;
         SCIP_Real* targetlincoefs;
         int ntargetlinvars;
 
         conshdlrand = SCIPfindConshdlr(sourcescip, "and");
         assert(conshdlrand != NULL);
 
         nsourceandconss = sourceconsdata->nconsanddatas;
 
         /* allocate temporary memory */
         SCIP_CALL( SCIPallocBufferArray(sourcescip, &targetandconss, nsourceandconss) );
         SCIP_CALL( SCIPallocBufferArray(sourcescip, &targetandcoefs, nsourceandconss) );
 
         /* get the number of vars in the copied linear constraint and allocate buffers
          * for the variables and the coefficients
          */
         SCIP_CALL( getLinearConsNVars(targetscip, targetlincons, targetlinconstype, &ntargetlinvars) );
         SCIP_CALL( SCIPallocBufferArray(sourcescip, &targetlinvars, ntargetlinvars) );
         SCIP_CALL( SCIPallocBufferArray(sourcescip, &targetlincoefs, ntargetlinvars) );
 
         /* retrieve the variables of the copied linear constraint */
         SCIP_CALL( getLinearConsVarsData(targetscip, targetlincons, targetlinconstype,
                                          targetlinvars, targetlincoefs, &ntargetlinvars) );
 
         /* now create a hashtable and insert the variables into it, so that it
          * can be checked in constant time if a variable was removed due to
          * compressed copying when looping over the and resultants
          */
         SCIP_CALL( SCIPhashtableCreate(&linconsvarsmap, SCIPblkmem(targetscip), ntargetlinvars, SCIPvarGetHashkey,
                                        SCIPvarIsHashkeyEq, SCIPvarGetHashkeyVal, NULL) );
 
         for( c = 0 ; c < ntargetlinvars; ++c )
         {
            SCIP_CALL( SCIPhashtableInsert(linconsvarsmap, targetlinvars[c]) );
         }
 
         /* free the buffer arrays that were only required for building the hastable */
         SCIPfreeBufferArray(sourcescip, &targetlincoefs);
         SCIPfreeBufferArray(sourcescip, &targetlinvars);
 
         for( c = 0 ; c < nsourceandconss; ++c )
         {
            CONSANDDATA* consanddata;
            SCIP_CONS* oldcons;
            SCIP_VAR* targetandresultant;
            SCIP_Bool validand;
 
            consanddata = sourceconsdata->consanddatas[c];
            assert(consanddata != NULL);
            oldcons = SCIPconsIsOriginal(sourcecons) ? consanddata->origcons : consanddata->cons;
            targetandresultant = (SCIP_VAR*) SCIPhashmapGetImage(varmap, SCIPgetResultantAnd(sourcescip, oldcons));
            assert(targetandresultant != NULL);
 
            /* if compressed copying is active, the resultant might not have been copied by the linear
             * constraint and we don't need to add it to the pseudo boolean constraint in this case
             */
            if( !SCIPhashtableExists(linconsvarsmap, targetandresultant) )
               continue;
 
            validand = TRUE;
 
            targetandconss[ntargetandconss] = NULL;
 
            /* copy and-constraints */
            SCIP_CALL( SCIPgetConsCopy(sourcescip, targetscip, oldcons, &targetandconss[ntargetandconss], conshdlrand, varmap, consmap, SCIPconsGetName(oldcons),
                  SCIPconsIsInitial(oldcons), SCIPconsIsSeparated(oldcons), SCIPconsIsEnforced(oldcons), SCIPconsIsChecked(oldcons),
                  SCIPconsIsPropagated(oldcons), SCIPconsIsLocal(oldcons), SCIPconsIsModifiable(oldcons), SCIPconsIsDynamic(oldcons),
                  SCIPconsIsRemovable(oldcons), SCIPconsIsStickingAtNode(oldcons), global, &validand) );
 
            *valid &= validand;
 
            if( validand )
            {
               targetandcoefs[ntargetandconss] = sourceconsdata->andcoefs[c];
               ++ntargetandconss;
            }
         }
 
         SCIPhashtableFree(&linconsvarsmap);
         assert(ntargetandconss <= ntargetlinvars);
      }
 
      if( *valid )
      {
         SCIP_Real targetrhs;
         SCIP_Real targetlhs;
 
         SCIP_VAR* intvar;
         SCIP_VAR* indvar;
         const char* consname;
 
         /* third the indicator and artificial integer variable part */
         assert(sourceconsdata->issoftcons == (sourceconsdata->indvar != NULL));
         indvar = sourceconsdata->indvar;
         intvar = sourceconsdata->intvar;
 
         /* copy indicator variable */
         if( indvar != NULL )
         {
            assert(*valid);
            SCIP_CALL( SCIPgetVarCopy(sourcescip, targetscip, indvar, &indvar, varmap, consmap, global, valid) );
            assert(!(*valid) || indvar != NULL);
         }
         /* copy artificial integer variable */
         if( intvar != NULL && *valid )
         {
            SCIP_CALL( SCIPgetVarCopy(sourcescip, targetscip, intvar, &intvar, varmap, consmap, global, valid) );
            assert(!(*valid) || intvar != NULL);
         }
 
         if( *valid )
         {
            if( name != NULL )
               consname = name;
            else
               consname = SCIPconsGetName(sourcecons);
 
            /* get new left and right hand sides of copied linear constraint since
             * they might have changed if compressed copying is used
             */
            SCIP_CALL( getLinearConsSides(targetscip, targetlincons, targetlinconstype, &targetlhs, &targetrhs) );
 
            /* create new pseudoboolean constraint */
            /* coverity[var_deref_op] */
            /* coverity[var_deref_model] */
            /* Note that due to compression the and constraints might have disappeared in which case ntargetandconss == 0. */
            SCIP_CALL( SCIPcreateConsPseudobooleanWithConss(targetscip, targetcons, consname,
                  targetlincons, targetlinconstype, targetandconss, targetandcoefs, ntargetandconss,
                  indvar, sourceconsdata->weight, sourceconsdata->issoftcons, intvar, targetlhs, targetrhs,
                  initial, separate, enforce, check, propagate, local, modifiable, dynamic, removable, stickingatnode) );
         }
      }
 
      if( !(*valid) && !SCIPisConsCompressionEnabled(sourcescip) )
      {
         SCIPverbMessage(sourcescip, SCIP_VERBLEVEL_MINIMAL, NULL, "could not copy constraint <%s>\n", SCIPconsGetName(sourcecons));
      }
 
      /* release copied linear constraint */
      if( targetlincons != NULL )
      {
         SCIP_CALL( SCIPreleaseCons(targetscip, &targetlincons) );
      }
 
      /* release copied and constraint */
      if( targetandconss != NULL )
      {
         int c;
 
         assert(ntargetandconss <= sourceconsdata->nconsanddatas);
 
         for( c = 0 ; c < ntargetandconss; ++c )
         {
            if( targetandconss[c] != NULL )
            {
               SCIP_CALL( SCIPreleaseCons(targetscip, &targetandconss[c]) );
            }
         }
      }
 
      /* free temporary memory */
      SCIPfreeBufferArrayNull(sourcescip, &targetandcoefs);
      SCIPfreeBufferArrayNull(sourcescip, &targetandconss);
   }
   else
      *valid = FALSE;
 
   return SCIP_OKAY;
}
 
/** compute all changes in consanddatas array */
static
SCIP_RETCODE computeConsAndDataChanges(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONSHDLRDATA*const conshdlrdata      /**< pseudoboolean constraint handler data */
   )
{
   CONSANDDATA** allconsanddatas;
   CONSANDDATA* consanddata;
   int c;
 
   assert(scip != NULL);
   assert(conshdlrdata != NULL);
 
   allconsanddatas = conshdlrdata->allconsanddatas;
   assert(allconsanddatas != NULL);
   assert(conshdlrdata->nallconsanddatas >= 0);
   assert(conshdlrdata->nallconsanddatas <= conshdlrdata->sallconsanddatas);
 
   for( c = conshdlrdata->nallconsanddatas - 1; c >= 0; --c )
   {
      SCIP_CONS* cons;
      SCIP_VAR** vars;
      int nvars;
      SCIP_VAR** newvars;
      int nnewvars;
      int v;
 
      consanddata = allconsanddatas[c];
 
      if( !consanddata->istransformed )
         continue;
 
      if( consanddata->nuses == 0 )
         continue;
 
      vars = consanddata->vars;
      nvars = consanddata->nvars;
      assert(nvars == 0 || vars != NULL);
      assert(consanddata->nnewvars == 0 && ((consanddata->snewvars > 0) == (consanddata->newvars != NULL)));
 
      if( nvars == 0 )
      {
#ifndef NDEBUG
         /* if an old consanddata-object has no variables left there should be no new variables */
         if( consanddata->cons != NULL )
            assert(SCIPgetNVarsAnd(scip, consanddata->cons) == 0);
#endif
         continue;
      }
 
      cons = consanddata->cons;
      assert(cons != NULL);
 
      if( SCIPconsIsDeleted(cons) )
         continue;
 
      /* sort and-variables */
      if( !SCIPisAndConsSorted(scip, consanddata->cons) )
      {
         SCIP_CALL( SCIPsortAndCons(scip, consanddata->cons) );
         assert(SCIPisAndConsSorted(scip, consanddata->cons));
      }
 
      /* get new and-variables */
      nnewvars = SCIPgetNVarsAnd(scip, consanddata->cons);
      newvars = SCIPgetVarsAnd(scip, consanddata->cons);
 
      /* stop if the constraint has no variables or there was an error (coverity issue) */
      if( nnewvars <= 0 )
         continue;
 
#ifndef NDEBUG
      /* check that old variables are sorted */
      for( v = nvars - 1; v > 0; --v )
         assert(SCIPvarGetIndex(vars[v]) >= SCIPvarGetIndex(vars[v - 1]));
      /* check that new variables are sorted */
      for( v = nnewvars - 1; v > 0; --v )
         assert(SCIPvarGetIndex(newvars[v]) >= SCIPvarGetIndex(newvars[v - 1]));
#endif
 
      /* check for changings, if and-constraint did not change we do not need to copy all variables */
      if( nvars == nnewvars )
      {
         SCIP_Bool changed;
 
         changed = FALSE;
 
         /* check each variable */
         for( v = nvars - 1; v >= 0; --v )
         {
            if( vars[v] != newvars[v] )
            {
               changed = TRUE;
               break;
            }
         }
 
         if( !changed )
            continue;
      }
 
      /* resize newvars array if necessary */
      if( nnewvars > consanddata->snewvars )
      {
         SCIP_CALL( SCIPensureBlockMemoryArray(scip, &(consanddata->newvars), &(consanddata->snewvars), nnewvars) );
      }
 
      /* copy all variables */
      BMScopyMemoryArray(consanddata->newvars, newvars, nnewvars);
      consanddata->nnewvars = nnewvars;
 
      /* capture all variables */
      for( v = consanddata->nnewvars - 1; v >= 0; --v )
      {
         /* in original problem the variables was already deleted */
         assert(consanddata->newvars[v] != NULL);
         SCIP_CALL( SCIPcaptureVar(scip, consanddata->newvars[v]) );
      }
   }
 
   return SCIP_OKAY;
}
 
/** remove old locks */
static
SCIP_RETCODE removeOldLocks(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< pseudoboolean constraint */
   CONSANDDATA*const     consanddata,        /**< CONSANDDATA object for which we want to delete the locks and the
                                              *   capture of the corresponding and-constraint */
   SCIP_Real const       coef,               /**< coefficient which led to old locks */
   SCIP_Real const       lhs,                /**< left hand side which led to old locks */
   SCIP_Real const       rhs                 /**< right hand side which led to old locks */
   )
{
   assert(scip != NULL);
   assert(cons != NULL);
   assert(consanddata != NULL);
   assert(!SCIPisInfinity(scip, coef) && !SCIPisInfinity(scip, -coef));
   assert(!SCIPisInfinity(scip, lhs));
   assert(!SCIPisInfinity(scip, -rhs));
   assert(SCIPisLE(scip, lhs, rhs));
 
   /* remove rounding locks */
   SCIP_CALL( unlockRoundingAndCons(scip, cons, consanddata, coef, lhs, rhs) );
 
   assert(consanddata->cons != NULL);
 
   return SCIP_OKAY;
}
 
/** add new locks */
static
SCIP_RETCODE addNewLocks(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< pseudoboolean constraint */
   CONSANDDATA*const     consanddata,        /**< CONSANDDATA object for which we want to delete the locks and the
                                              *   capture of the corresponding and-constraint */
   SCIP_Real const       coef,               /**< coefficient which lead to new locks */
   SCIP_Real const       lhs,                /**< left hand side which lead to new locks */
   SCIP_Real const       rhs                 /**< right hand side which lead to new locks */
   )
{
   assert(scip != NULL);
   assert(cons != NULL);
   assert(consanddata != NULL);
   assert(!SCIPisInfinity(scip, coef) && !SCIPisInfinity(scip, -coef));
   assert(!SCIPisInfinity(scip, lhs));
   assert(!SCIPisInfinity(scip, -rhs));
   assert(SCIPisLE(scip, lhs, rhs));
 
   /* add rounding locks due to old variables in consanddata object */
   SCIP_CALL( lockRoundingAndCons(scip, cons, consanddata, coef, lhs, rhs) );
 
   assert(consanddata->cons != NULL);
 
   return SCIP_OKAY;
}
 
/** update all locks inside this constraint and all captures on all and-constraints */
static
SCIP_RETCODE correctLocksAndCaptures(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< pseudoboolean constraint */
   SCIP_CONSHDLRDATA*const conshdlrdata,     /**< pseudoboolean constraint handler data */
   SCIP_Real const       newlhs,             /**< new left hand side of pseudoboolean constraint */
   SCIP_Real const       newrhs,             /**< new right hand side of pseudoboolean constraint */
   SCIP_VAR**const       andress,            /**< new and-resultants in pseudoboolean constraint */
   SCIP_Real*const       andcoefs,           /**< new and-resultants-coeffcients in pseudoboolean constraint */
   SCIP_Bool*const       andnegs,            /**< new negation status of and-resultants in pseudoboolean constraint */
   int const             nandress            /**< number of current and-resultants in pseudoboolean constraint */
   )
{
   CONSANDDATA** newconsanddatas;
   int nnewconsanddatas;
   int snewconsanddatas;
   SCIP_Real* newandcoefs;
   SCIP_Real* oldandcoefs;
   SCIP_Bool* newandnegs;
   SCIP_Bool* oldandnegs;
   CONSANDDATA** consanddatas;
   int nconsanddatas;
   SCIP_CONSDATA* consdata;
   int oldnvars;
   int c;
   int c1;
 
   assert(scip != NULL);
   assert(cons != NULL);
   assert(conshdlrdata != NULL);
   assert(conshdlrdata->hashmap != NULL);
   assert(nandress == 0 || (andress != NULL && andcoefs != NULL));
   assert(!SCIPisInfinity(scip, newlhs));
   assert(!SCIPisInfinity(scip, -newrhs));
   assert(SCIPisLE(scip, newlhs, newrhs));
 
   consdata = SCIPconsGetData(cons);
   assert(consdata != NULL);
 
   /* sort and-constraints by the problem indices of corresponding and-resultants */
   SCIPsortPtrRealBool((void**)(consdata->consanddatas), consdata->andcoefs, consdata->andnegs, resvarCompWithInactive, consdata->nconsanddatas);
 
   /* sort and-resultants by their problem indices */
   SCIPsortPtrRealBool((void**)andress, andcoefs, andnegs, resvarComp, nandress);
 
   consanddatas = consdata->consanddatas;
   oldandcoefs = consdata->andcoefs;
   oldandnegs = consdata->andnegs;
   nconsanddatas = consdata->nconsanddatas;
   assert(nconsanddatas == 0 || (consanddatas != NULL && oldandcoefs != NULL));
 
   snewconsanddatas = nconsanddatas + nandress;
 
   /* allocate new block memory arrays */
   SCIP_CALL( SCIPallocBlockMemoryArray(scip, &newconsanddatas, snewconsanddatas) );
   SCIP_CALL( SCIPallocBlockMemoryArray(scip, &newandcoefs, snewconsanddatas) );
   SCIP_CALL( SCIPallocBlockMemoryArray(scip, &newandnegs, snewconsanddatas) );
 
   nnewconsanddatas = 0;
 
   /* collect new consanddata objects and update locks and captures */
   for( c = 0, c1 = 0; c < nconsanddatas && c1 < nandress; )
   {
      SCIP_CONS* andcons;
      SCIP_VAR* res1;
      SCIP_VAR* res2;
      int compval;
 
      assert(consanddatas[c] != NULL);
 
      /* consanddata object could have been deleted in the last presolving round */
      if( !consanddatas[c]->istransformed )
      {
         ++c;
         consdata->changed = TRUE;
         consdata->upgradetried = FALSE;
         continue;
      }
 
      andcons = consanddatas[c]->cons;
      assert(andcons != NULL);
 
      if( andcons == NULL ) /*lint !e774*/
      {
         ++c;
         consdata->changed = TRUE;
         consdata->upgradetried = FALSE;
         continue;
      }
      else if( SCIPconsIsDeleted(andcons) )
      {
         /* remove rounding locks, because the and constraint was deleted  */
         SCIP_CALL( unlockRoundingAndCons(scip, cons, consanddatas[c],
               oldandnegs[c] ? -oldandcoefs[c] : oldandcoefs[c], consdata->lhs, consdata->rhs) );
         ++c;
         consdata->changed = TRUE;
         consdata->upgradetried = FALSE;
         continue;
      }
      assert(andcons != NULL);
 
      /* get and-resultants of consanddata object in constraint data */
      res1 = SCIPgetResultantAnd(scip, andcons);
      assert(res1 != NULL);
      assert(SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)res1) == consanddatas[c]);
 
      /* get and-resultants in new corresponding linear constraint */
      res2 = andress[c1];
      assert(res2 != NULL);
      assert(SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)res2) != NULL);
 
      /* get comparison value */
      compval = resvarComp((void*)res1, (void*)res2);
 
      /* collect new consanddata objects sorted with respect to the problem index of corresponding and-resultants */
      if( compval == -1 )
      {
         assert(!SCIPisZero(scip, oldandcoefs[c]));
         assert(consanddatas[c]->nuses > 0);
         --(consanddatas[c]->nuses);
 
         /* remove old locks */
         SCIP_CALL( removeOldLocks(scip, cons, consanddatas[c], oldandnegs[c] ? -oldandcoefs[c] : oldandcoefs[c],
               consdata->lhs, consdata->rhs) );
         ++c;
         consdata->changed = TRUE;
         consdata->upgradetried = FALSE;
         consdata->propagated = FALSE;
         consdata->presolved = FALSE;
      }
      else if( compval == +1 )
      {
         assert(!SCIPisZero(scip, andcoefs[c1]));
         assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)res2));
         newconsanddatas[nnewconsanddatas] = (CONSANDDATA*) SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)res2);
         newandcoefs[nnewconsanddatas] = andcoefs[c1];
         newandnegs[nnewconsanddatas] = andnegs[c1];
         ++(newconsanddatas[nnewconsanddatas]->nuses);
 
         /* add new locks */
         SCIP_CALL( addNewLocks(scip, cons, newconsanddatas[nnewconsanddatas], newandnegs[nnewconsanddatas] ?
               -newandcoefs[nnewconsanddatas] : newandcoefs[nnewconsanddatas], newlhs, newrhs) );
         ++c1;
         consdata->changed = TRUE;
         consdata->upgradetried = FALSE;
         consdata->cliquesadded = FALSE;
         consdata->propagated = FALSE;
         consdata->presolved = FALSE;
 
         ++nnewconsanddatas;
      }
      else
      {
         SCIP_Bool coefsignchanged;
         SCIP_Bool lhschanged;
         SCIP_Bool rhschanged;
 
         assert(!SCIPisZero(scip, oldandcoefs[c]));
         assert(!SCIPisZero(scip, andcoefs[c1]));
         assert(SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)res2) == consanddatas[c]);
 
         /* copy old consanddata object and new coefficent */
         newconsanddatas[nnewconsanddatas] = consanddatas[c];
 
         newandcoefs[nnewconsanddatas] = andcoefs[c1];
         newandnegs[nnewconsanddatas] = andnegs[c1];
 
         if( ((oldandnegs[c] == andnegs[c1]) && !SCIPisEQ(scip, oldandcoefs[c], newandcoefs[c1]))
            || ((oldandnegs[c] != newandnegs[c1]) && !SCIPisEQ(scip, oldandcoefs[c], -newandcoefs[c1])) )
            consdata->upgradetried = FALSE;
 
         coefsignchanged = (oldandnegs[c] == andnegs[c1]) &&
            ((oldandcoefs[c] < 0 && andcoefs[c1] > 0) || (oldandcoefs[c] > 0 && andcoefs[c1] < 0));
         coefsignchanged = coefsignchanged || ((oldandnegs[c] != andnegs[c1]) &&
            ((oldandcoefs[c] < 0 && andcoefs[c1] < 0) || (oldandcoefs[c] > 0 && andcoefs[c1] > 0)));
         lhschanged = (SCIPisInfinity(scip, -consdata->lhs) && !SCIPisInfinity(scip, -newlhs)) || (!SCIPisInfinity(scip, -consdata->lhs) && SCIPisInfinity(scip, -newlhs))
            || (consdata->lhs < 0 && newlhs > 0) || (consdata->lhs > 0 && newlhs < 0);
         rhschanged = (SCIPisInfinity(scip, consdata->rhs) && !SCIPisInfinity(scip, newrhs)) || (!SCIPisInfinity(scip, consdata->rhs) && SCIPisInfinity(scip, newrhs))
            || (consdata->rhs < 0 && newrhs > 0) || (consdata->rhs > 0 && newrhs < 0);
 
         /* update or renew locks */
         if( coefsignchanged || lhschanged || rhschanged || newconsanddatas[nnewconsanddatas]->nnewvars > 0)
         {
            /* renew locks */
            SCIP_CALL( removeOldLocks(scip, cons, newconsanddatas[nnewconsanddatas], oldandnegs[c] ?
                  -oldandcoefs[c] : oldandcoefs[c], consdata->lhs, consdata->rhs) );
            SCIP_CALL( addNewLocks(scip, cons, newconsanddatas[nnewconsanddatas], newandnegs[nnewconsanddatas] ?
                  -newandcoefs[nnewconsanddatas] : newandcoefs[nnewconsanddatas], newlhs, newrhs) );
 
            consdata->changed = TRUE;
            consdata->upgradetried = FALSE;
            consdata->cliquesadded = FALSE;
            consdata->propagated = FALSE;
            consdata->presolved = FALSE;
         }
 
         ++c;
         ++c1;
         ++nnewconsanddatas;
      }
   }
 
   /* add all remaining consanddatas and update locks and captures */
   if( c < nconsanddatas )
   {
      assert(c1 == nandress);
 
      for( ; c < nconsanddatas; ++c )
      {
         SCIP_CONS* andcons;
#ifndef NDEBUG
         SCIP_VAR* res1;
 
         assert(consanddatas[c] != NULL);
#endif
         andcons = consanddatas[c]->cons;
#ifndef NDEBUG
         if( andcons != NULL )
         {
            res1 = SCIPgetResultantAnd(scip, andcons);
            assert(res1 != NULL);
            assert(SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)res1) == consanddatas[c]);
         }
#endif
         if( andcons == NULL )
         {
            consdata->changed = TRUE;
            consdata->upgradetried = FALSE;
            continue;
         }
 
         assert(consanddatas[c]->nuses > 0);
         --(consanddatas[c]->nuses);
 
         /* remove old locks */
         SCIP_CALL( removeOldLocks(scip, cons, consanddatas[c], oldandnegs[c] ? -oldandcoefs[c] : oldandcoefs[c],
               consdata->lhs, consdata->rhs) );
         consdata->changed = TRUE;
         consdata->upgradetried = FALSE;
         consdata->propagated = FALSE;
         consdata->presolved = FALSE;
      }
   }
   else if( c1 < nandress )
   {
      for( ; c1 < nandress; ++c1 )
      {
         SCIP_VAR* res2;
 
         res2 = andress[c1];
         assert(res2 != NULL);
         assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)res2));
         newconsanddatas[nnewconsanddatas] = (CONSANDDATA*) SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)res2);
         newandcoefs[nnewconsanddatas] = andcoefs[c1];
         newandnegs[nnewconsanddatas] = andnegs[c1];
         ++(newconsanddatas[nnewconsanddatas]->nuses);
 
         /* add new locks */
         SCIP_CALL( addNewLocks(scip, cons, newconsanddatas[nnewconsanddatas], newandnegs[nnewconsanddatas] ?
               -newandcoefs[nnewconsanddatas] : newandcoefs[nnewconsanddatas], newlhs, newrhs) );
 
         ++nnewconsanddatas;
         consdata->changed = TRUE;
         consdata->upgradetried = FALSE;
         consdata->cliquesadded = FALSE;
         consdata->propagated = FALSE;
         consdata->presolved = FALSE;
      }
   }
   assert(c == nconsanddatas && c1 == nandress);
 
   /* delete old and-coefficients and consanddata objects */
   SCIPfreeBlockMemoryArray(scip, &(consdata->andcoefs), consdata->sconsanddatas);
   SCIPfreeBlockMemoryArray(scip, &(consdata->andnegs), consdata->sconsanddatas);
   SCIPfreeBlockMemoryArray(scip, &(consdata->consanddatas), consdata->sconsanddatas);
 
   if( !SCIPisEQ(scip, consdata->lhs, newlhs) || !SCIPisEQ(scip, consdata->rhs, newrhs) )
   {
      consdata->upgradetried = FALSE;
      consdata->lhs = newlhs;
      consdata->rhs = newrhs;
   }
 
   consdata->consanddatas = newconsanddatas;
   consdata->andcoefs = newandcoefs;
   consdata->andnegs = newandnegs;
   consdata->nconsanddatas = nnewconsanddatas;
   consdata->sconsanddatas = snewconsanddatas;
 
   oldnvars = consdata->nlinvars;
   /* update number of linear variables without and-resultants */
   SCIP_CALL( getLinearConsNVars(scip, consdata->lincons, consdata->linconstype, &(consdata->nlinvars)) );
   consdata->nlinvars -= nnewconsanddatas;
 
   if( oldnvars != consdata->nlinvars )
   {
      consdata->changed = TRUE;
      consdata->upgradetried = FALSE;
      consdata->cliquesadded = FALSE;
      consdata->propagated = FALSE;
      consdata->presolved = FALSE;
   }
 
#ifndef NDEBUG
   consanddatas = consdata->consanddatas;
   nconsanddatas = consdata->nconsanddatas;
   assert(nconsanddatas == 0 || consanddatas != NULL);
 
   /* check that consanddata objects are sorted with respect to the problem index of the corresponding resultants */
   for( c = nconsanddatas - 1; c > 0; --c )
   {
      SCIP_VAR* res1;
      SCIP_VAR* res2;
      SCIP_Bool resneg1;
      SCIP_Bool resneg2;
      int resind1;
      int resind2;
 
      assert(consanddatas[c] != NULL);
      assert(consanddatas[c]->cons != NULL);
      res1 = SCIPgetResultantAnd(scip, consanddatas[c]->cons);
      assert(res1 != NULL);
      assert(consanddatas[c - 1] != NULL);
      assert(consanddatas[c - 1]->cons != NULL);
      res2 = SCIPgetResultantAnd(scip, consanddatas[c - 1]->cons);
      assert(res2 != NULL);
      resneg1 = SCIPvarIsNegated(res1);
      if( resneg1 )
      {
         res1 = SCIPvarGetNegatedVar(res1);
         assert(res1 != NULL);
      }
      resneg2 = SCIPvarIsNegated(res2);
      if( resneg2 )
      {
         res2 = SCIPvarGetNegatedVar(res2);
         assert(res2 != NULL);
      }
      resind1 = SCIPvarGetProbindex(res1);
      resind2 = SCIPvarGetProbindex(res2);
      if( resind1 == -1 && resind2 == -1 )
      {
         resind1 = SCIPvarGetIndex(res1);
         resind2 = SCIPvarGetIndex(res2);
      }
 
      if( resind1 <= resind2 )
      {
         assert(resind1 == resind2);
         assert(!resneg1);
         assert(resneg2);
      }
   }
#endif
 
   return SCIP_OKAY;
}
 
/** adds cliques of the pseudoboolean constraint to the global clique table */
static
SCIP_RETCODE addCliques(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< pseudoboolean constraint */
   SCIP_Bool*const       cutoff,             /**< pointer to store whether the node can be cut off */
   int*const             naggrvars,          /**< pointer to count the number of aggregated variables */
   int*const             nchgbds             /**< pointer to count the number of performed bound changes */
   )
{
   SCIP_CONSDATA* consdata;
   SCIP_VAR** vars;
   int nvars;
   SCIP_VAR** linvars;
   SCIP_VAR* andres;
   SCIP_VAR* andres2;
   int nlinvars;
   int nandress;
   int c;
   int v2;
   int v1;
   int nchgbdslocal;
 
   assert(scip != NULL);
   assert(cons != NULL);
   assert(cutoff != NULL);
   assert(naggrvars != NULL);
   assert(nchgbds != NULL);
   assert(SCIPconsIsActive(cons));
 
   *cutoff = FALSE;
 
   consdata = SCIPconsGetData(cons);
   assert(consdata != NULL);
   /* if we have no and-constraints left, we should not be here and this constraint should be deleted (only the linaer should survive) */
   assert(consdata->nconsanddatas > 0);
 
   /* check whether the cliques have already been added */
   if( consdata->cliquesadded )
      return SCIP_OKAY;
 
   consdata->cliquesadded = TRUE;
 
   checkConsConsistency(scip, cons);
 
   /* check standard pointers and sizes */
   assert(consdata->lincons != NULL);
   assert(SCIPconsIsActive(consdata->lincons));
   assert(consdata->linconstype > SCIP_LINEARCONSTYPE_INVALIDCONS);
   assert(consdata->consanddatas != NULL);
   assert(consdata->nconsanddatas > 0);
   assert(consdata->nconsanddatas <= consdata->sconsanddatas);
 
   /* check number of linear variables */
   SCIP_CALL( getLinearConsNVars(scip, consdata->lincons, consdata->linconstype, &nvars) );
   assert(nvars == consdata->nlinvars + consdata->nconsanddatas);
 
   /* get temporary memory */
   SCIP_CALL( SCIPallocBufferArray(scip, &vars, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &linvars, nvars) );
 
   /* get variables and coefficients */
   SCIP_CALL( getLinearConsVarsData(scip, consdata->lincons, consdata->linconstype, vars, NULL, &nvars) );
 
   /* calculate all not artificial linear variables and all artificial and-resultants
    * @todo should we take into accout the negation status of the cliques?
    */
   SCIP_CALL( getLinVarsAndAndRess(scip, cons, vars, NULL, nvars, linvars, NULL, &nlinvars,
         NULL, NULL, NULL, &nandress) );
 
   assert(nandress == consdata->nconsanddatas);
   assert(consdata->consanddatas != NULL);
 
   /* find cliques from linear variable to and-resultant */
   for( c = nandress - 1; c >= 0; --c )
   {
      CONSANDDATA* consanddata;
      SCIP_VAR** andvars;
      int nandvars;
 
      consanddata = consdata->consanddatas[c];
      assert(consanddata != NULL);
 
      andres = SCIPgetResultantAnd(scip, consanddata->cons);
 
      /* choose correct variable array */
      if( consanddata->nnewvars > 0 )
      {
         andvars = consanddata->newvars;
         nandvars = consanddata->nnewvars;
      }
      else
      {
         andvars = consanddata->vars;
         nandvars = consanddata->nvars;
      }
 
      for( v1 = nandvars - 1; v1 >= 0; --v1 )
      {
         SCIP_VAR* var1;
         SCIP_Bool values[2];
 
         var1 = andvars[v1];
         if( !SCIPvarIsActive(var1) && (!SCIPvarIsNegated(var1) || !SCIPvarIsActive(SCIPvarGetNegationVar(var1))) )
            continue;
 
         /* get active counterpart to check for common cliques */
         if( SCIPvarGetStatus(var1) == SCIP_VARSTATUS_NEGATED )
         {
            var1 = SCIPvarGetNegationVar(var1);
            values[0] = FALSE;
         }
         else
            values[0] = TRUE;
 
         for( v2 = nlinvars - 1; v2 >= 0; --v2 )
         {
            SCIP_VAR* var2;
 
            var2 = linvars[v2];
            if( !SCIPvarIsActive(var2) && (!SCIPvarIsNegated(var2) || !SCIPvarIsActive(SCIPvarGetNegationVar(var2))) )
               continue;
 
            /* get active counterpart to check for common cliques */
            if( SCIPvarGetStatus(var2) == SCIP_VARSTATUS_NEGATED )
            {
               var2 = SCIPvarGetNegationVar(var2);
               values[1] = FALSE;
            }
            else
               values[1] = TRUE;
 
            /* if variable in and-constraint1 is the negated variable of a normal linear variable, than we can add a
             * clique between the and-resultant and the normal linear variable, negated variables are not save in
             * cliquetables
             *
             * set r_1 = var1 * z; (z is some product)
             * var1 == ~var2
             *
             * if:
             * var1 + ~var1 <= 1;          r_1
             *    0 +     1 <= 1             0   \
             *    1 +     0 <= 1   ==>  1 or 0    >   ==>    r_1 + var2 <= 1
             *    0 +     0 <= 1             0   /
             */
            if( values[0] != values[1] && var1 == var2 )
            {
               SCIP_CONS* newcons;
               SCIP_VAR* clqvars[2];
               char consname[SCIP_MAXSTRLEN];
 
               clqvars[0] = andres;
               clqvars[1] = values[1] ? var2 : SCIPvarGetNegatedVar(var2);
               assert(clqvars[1] != NULL);
 
               /* @todo: check whether it is better to only add the clique or to add the setppc constraint or do both */
 
               /* add clique */
               SCIP_CALL( SCIPaddClique(scip, clqvars, NULL, 2, FALSE, cutoff, &nchgbdslocal) );
               if( *cutoff )
                  goto TERMINATE;
 
               *nchgbds += nchgbdslocal;
 
               (void) SCIPsnprintf(consname, SCIP_MAXSTRLEN, "%s_clq_%s_%s", SCIPconsGetName(cons), SCIPvarGetName(clqvars[0]), SCIPvarGetName(clqvars[1]) );
               SCIP_CALL( SCIPcreateConsSetpack(scip, &newcons, consname, 2, clqvars,
                     SCIPconsIsInitial(cons), SCIPconsIsSeparated(cons), SCIPconsIsEnforced(cons),
                     FALSE, SCIPconsIsPropagated(cons),
                     SCIPconsIsLocal(cons), SCIPconsIsModifiable(cons),
                     SCIPconsIsDynamic(cons), SCIPconsIsRemovable(cons), SCIPconsIsStickingAtNode(cons)) );
 
               SCIP_CALL( SCIPaddCons(scip, newcons) );
               SCIPdebugMsg(scip, "added a clique/setppc constraint <%s> \n", SCIPconsGetName(newcons));
               SCIPdebugPrintCons(scip, newcons, NULL);
 
               SCIP_CALL( SCIPreleaseCons(scip, &newcons) );
            }
            /* if a variable in an and-constraint is in a clique with another normal linear variable, we can add the
             * clique between the linear variable and the and-resultant
             *
             * set r_1 = var1 * z; (z is some product)
             *
             * if:
             * var1 + var2 <= 1;          r_1
             *    0 +    1 <= 1             0   \
             *    1 +    0 <= 1   ==>  1 or 0    >   ==>    r_1 + var2 <= 1
             *    0 +    0 <= 1             0   /
             */
            if( (var1 != var2) && SCIPvarsHaveCommonClique(var1, values[0], var2, values[1], TRUE) )
            {
               SCIP_CONS* newcons;
               SCIP_VAR* clqvars[2];
               char consname[SCIP_MAXSTRLEN];
 
               clqvars[0] = andres;
               clqvars[1] = values[1] ? var2 : SCIPvarGetNegatedVar(var2);
               assert(clqvars[1] != NULL);
 
               /* @todo: check whether it is better to only add the clique or to add the setppc constraint or do both */
 
               /* add clique */
               SCIP_CALL( SCIPaddClique(scip, clqvars, NULL, 2, FALSE, cutoff, &nchgbdslocal) );
               if( *cutoff )
                  goto TERMINATE;
 
               *nchgbds += nchgbdslocal;
 
               (void) SCIPsnprintf(consname, SCIP_MAXSTRLEN, "%s_clq_%s_%s", SCIPconsGetName(cons), SCIPvarGetName(clqvars[0]), SCIPvarGetName(clqvars[1]) );
               SCIP_CALL( SCIPcreateConsSetpack(scip, &newcons, consname, 2, clqvars,
                     SCIPconsIsInitial(cons), SCIPconsIsSeparated(cons), SCIPconsIsEnforced(cons),
                     FALSE, SCIPconsIsPropagated(cons),
                     SCIPconsIsLocal(cons), SCIPconsIsModifiable(cons),
                     SCIPconsIsDynamic(cons), SCIPconsIsRemovable(cons), SCIPconsIsStickingAtNode(cons)) );
 
               SCIP_CALL( SCIPaddCons(scip, newcons) );
               SCIPdebugMsg(scip, "added a clique/setppc constraint <%s> \n", SCIPconsGetName(newcons));
               SCIPdebugPrintCons(scip, newcons, NULL);
 
               SCIP_CALL( SCIPreleaseCons(scip, &newcons) );
            }
         }
      }
   }
 
   /* find cliques over variables which are in different and-constraints */
   for( c = nandress - 1; c > 0; --c )
   {
      CONSANDDATA* consanddata1;
      CONSANDDATA* consanddata2;
      SCIP_VAR** andvars1;
      int nandvars1;
      SCIP_VAR** andvars2;
      int nandvars2;
 
      consanddata1 = consdata->consanddatas[c];
      assert(consanddata1 != NULL);
      consanddata2 = consdata->consanddatas[c - 1];
      assert(consanddata2 != NULL);
 
      andres = SCIPgetResultantAnd(scip, consanddata1->cons);
      andres2 = SCIPgetResultantAnd(scip, consanddata2->cons);
 
      /* choose correct variable array of consanddata object 1 */
      if( consanddata1->nnewvars > 0 )
      {
         andvars1 = consanddata1->newvars;
         nandvars1 = consanddata1->nnewvars;
      }
      else
      {
         andvars1 = consanddata1->vars;
         nandvars1 = consanddata1->nvars;
      }
 
      /* choose correct variable array of consanddata object 2 */
      if( consanddata2->nnewvars > 0 )
      {
         andvars2 = consanddata2->newvars;
         nandvars2 = consanddata2->nnewvars;
      }
      else
      {
         andvars2 = consanddata2->vars;
         nandvars2 = consanddata2->nvars;
      }
 
      /* compare both terms for finding new aggregated variables and new cliques */
      for( v1 = nandvars1 - 1; v1 >= 0; --v1 )
      {
         SCIP_VAR* var1;
         SCIP_Bool values[2];
 
         var1 = andvars1[v1];
         if( !SCIPvarIsActive(var1) && (!SCIPvarIsNegated(var1) || !SCIPvarIsActive(SCIPvarGetNegationVar(var1))) )
            continue;
 
         /* get active counterpart to check for common cliques */
         if( SCIPvarGetStatus(var1) == SCIP_VARSTATUS_NEGATED )
         {
            var1 = SCIPvarGetNegationVar(var1);
            values[0] = FALSE;
         }
         else
            values[0] = TRUE;
 
         for( v2 = nandvars2 - 1; v2 >= 0; --v2 )
         {
            SCIP_VAR* var2;
 
            var2 = andvars2[v2];
            if( !SCIPvarIsActive(var2) && (!SCIPvarIsNegated(var2) || !SCIPvarIsActive(SCIPvarGetNegationVar(var2))) )
               continue;
 
            /* get active counterpart to check for common cliques */
            if( SCIPvarGetStatus(var2) == SCIP_VARSTATUS_NEGATED )
            {
               var2 = SCIPvarGetNegationVar(var2);
               values[1] = FALSE;
            }
            else
               values[1] = TRUE;
 
            /* if a variable in and-constraint1 is the negated variable of a variable in and-constraint2, than we can
             * add a clique between both and-resultants, negated variables are not save in cliquetables
             *
             * set r_1 = var1 * z_1; (z_1 is some product)
             * set r_2 = var2 * z_2; (z_2 is some product)
             * var1 == ~var2
             *
             * if:
             * var1 + ~var1 <= 1;          r_1     r_2
             *    0 +     1 <= 1             0  1 or 0   \
             *    1 +     0 <= 1   ==>  1 or 0       0    >   ==>    r_1 + r_2 <= 1
             *    0 +     0 <= 1             0       0   /
             */
            if( values[0] != values[1] && var1 == var2 )
            {
               SCIP_CONS* newcons;
               SCIP_VAR* clqvars[2];
               char consname[SCIP_MAXSTRLEN];
 
               clqvars[0] = andres;
               clqvars[1] = andres2;
 
               /* @todo: check whether it is better to only add the clique or to add the setppc constraint or do both */
 
               /* add clique */
               SCIP_CALL( SCIPaddClique(scip, clqvars, NULL, 2, FALSE, cutoff, &nchgbdslocal) );
               if( *cutoff )
                  goto TERMINATE;
 
               *nchgbds += nchgbdslocal;
 
               (void) SCIPsnprintf(consname, SCIP_MAXSTRLEN, "%s_clq_%s_%s", SCIPconsGetName(cons), SCIPvarGetName(clqvars[0]), SCIPvarGetName(clqvars[1]) );
               SCIP_CALL( SCIPcreateConsSetpack(scip, &newcons, consname, 2, clqvars,
                     SCIPconsIsInitial(cons), SCIPconsIsSeparated(cons), SCIPconsIsEnforced(cons),
                     FALSE, SCIPconsIsPropagated(cons),
                     SCIPconsIsLocal(cons), SCIPconsIsModifiable(cons),
                     SCIPconsIsDynamic(cons), SCIPconsIsRemovable(cons), SCIPconsIsStickingAtNode(cons)) );
 
               SCIP_CALL( SCIPaddCons(scip, newcons) );
               SCIPdebugMsg(scip, "added a clique/setppc constraint <%s> \n", SCIPconsGetName(newcons));
               SCIPdebugPrintCons(scip, newcons, NULL);
 
               SCIP_CALL( SCIPreleaseCons(scip, &newcons) );
            }
            /* if a variable in an and-constraint is in a clique with a variable in another and-constraint, we can add
             * the clique between both and-resultant
             *
             * let r_1 = var1 * z_1; (z_1 is some product)
             * let r_2 = var2 * z_2; (z_2 is some product)
             *
             * if:
             * var1 + var2 <= 1;          r_1     r_2
             *    0 +    1 <= 1             0  1 or 0   \
             *    1 +    0 <= 1   ==>  1 or 0       0    >   ==>    r_1 + r_2 <= 1
             *    0 +    0 <= 1             0       0   /
             */
            else if( SCIPvarsHaveCommonClique(var1, values[0], var2, values[1], TRUE) && (var1 != var2) )
            {
               SCIP_CONS* newcons;
               SCIP_VAR* clqvars[2];
               char consname[SCIP_MAXSTRLEN];
 
               clqvars[0] = andres;
               clqvars[1] = values[1] ? var2 : SCIPvarGetNegatedVar(var2);
               assert(clqvars[1] != NULL);
 
               /* @todo: check whether it is better to only add the clique or to add the setppc constraint or do both */
 
               /* add clique */
               SCIP_CALL( SCIPaddClique(scip, clqvars, NULL, 2, FALSE, cutoff, &nchgbdslocal) );
               if( *cutoff )
                  goto TERMINATE;
 
               *nchgbds += nchgbdslocal;
 
               (void) SCIPsnprintf(consname, SCIP_MAXSTRLEN, "%s_clq_%s_%s", SCIPconsGetName(cons), SCIPvarGetName(clqvars[0]), SCIPvarGetName(clqvars[1]) );
               SCIP_CALL( SCIPcreateConsSetpack(scip, &newcons, consname, 2, clqvars,
                     SCIPconsIsInitial(cons), SCIPconsIsSeparated(cons), SCIPconsIsEnforced(cons),
                     FALSE, SCIPconsIsPropagated(cons),
                     SCIPconsIsLocal(cons), SCIPconsIsModifiable(cons),
                     SCIPconsIsDynamic(cons), SCIPconsIsRemovable(cons), SCIPconsIsStickingAtNode(cons)) );
 
               SCIP_CALL( SCIPaddCons(scip, newcons) );
               SCIPdebugMsg(scip, "added a clique/setppc constraint <%s> \n", SCIPconsGetName(newcons));
               SCIPdebugPrintCons(scip, newcons, NULL);
 
               SCIP_CALL( SCIPreleaseCons(scip, &newcons) );
            }
         }
      }
   }
 
 TERMINATE:
   /* free temporary memory */
   SCIPfreeBufferArray(scip, &linvars);
   SCIPfreeBufferArray(scip, &vars);
 
   return SCIP_OKAY;
}
 
/** propagation method for pseudoboolean constraints */
static
SCIP_RETCODE propagateCons(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< knapsack constraint */
   SCIP_Bool*const       cutoff,             /**< pointer to store whether the node can be cut off */
   int*const             ndelconss           /**< pointer to count number of deleted constraints */
   )
{
   SCIP_CONSDATA* consdata;
 
   assert(scip != NULL);
   assert(cons != NULL);
   assert(cutoff != NULL);
   assert(ndelconss != NULL);
 
   *cutoff = FALSE;
 
   consdata = SCIPconsGetData(cons);
   assert(consdata != NULL);
   assert(consdata->lincons != NULL);
 
   /* if linear constraint is redundant, than pseudoboolean constraint is redundant too */
   if( SCIPconsIsDeleted(consdata->lincons) )
   {
      SCIP_CALL( SCIPdelConsLocal(scip, cons) );
      ++(*ndelconss);
   }
 
   /* check if the constraint was already propagated */
   if( consdata->propagated )
      return SCIP_OKAY;
 
   /* mark the constraint propagated */
   consdata->propagated = TRUE;
 
   return SCIP_OKAY;
}
 
/** update and-constraint flags due to pseudoboolean constraint flags */
static
SCIP_RETCODE updateAndConss(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons                /**< pseudoboolean constraint */
   )
{
   CONSANDDATA** consanddatas;
   int nconsanddatas;
   SCIP_CONSDATA* consdata;
   int c;
 
   assert(scip != NULL);
   assert(cons != NULL);
 
   consdata = SCIPconsGetData(cons);
   assert(consdata != NULL);
 
   consanddatas = consdata->consanddatas;
   nconsanddatas = consdata->nconsanddatas;
   assert(nconsanddatas == 0 || consanddatas != NULL);
 
   if( !SCIPconsIsActive(cons) )
      return SCIP_OKAY;
 
   /* release and-constraints and change check flag of and-constraint */
   for( c = nconsanddatas - 1; c >= 0; --c )
   {
      SCIP_CONS* andcons;
 
      assert(consanddatas[c] != NULL);
 
      if( !consanddatas[c]->istransformed )
         continue;
 
      andcons = consanddatas[c]->cons;
      assert(andcons != NULL);
 
      SCIP_CALL( SCIPsetConsChecked(scip, andcons, SCIPconsIsChecked(cons)) );
   }
 
   return SCIP_OKAY;
}
 
/** delete unused information in constraint handler data */
static
SCIP_RETCODE correctConshdlrdata(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONSHDLRDATA*const conshdlrdata,     /**< pseudoboolean constraint handler data */
   int*const             ndelconss           /**< pointer to count number of deleted constraints */
   )
{
   CONSANDDATA** allconsanddatas;
   CONSANDDATA* consanddata;
   SCIP_VAR** fixedvars = SCIPgetFixedVars(scip);
   SCIP_VAR** activevars;
   SCIP_Real* activescalars;
   SCIP_Real activeconstant;
   int nvars = SCIPgetNVars(scip);
   int nfixedvars = SCIPgetNFixedVars(scip);
   int c;
 
   assert(scip != NULL);
   assert(conshdlrdata != NULL);
   assert(ndelconss != NULL);
 
   if( conshdlrdata->nallconsanddatas == 0 )
      return SCIP_OKAY;
 
   allconsanddatas = conshdlrdata->allconsanddatas;
   assert(allconsanddatas != NULL);
   assert(conshdlrdata->nallconsanddatas >= 1);
   assert(conshdlrdata->nallconsanddatas <= conshdlrdata->sallconsanddatas);
 
   if( nfixedvars >= 1 && nvars >= 1 )
   {
      SCIP_CALL( SCIPallocBufferArray(scip, &activevars, nvars) );
      SCIP_CALL( SCIPallocBufferArray(scip, &activescalars, nvars) );
   }
   else
   {
      activevars = NULL;
      activescalars = NULL;
   }
 
   for( c = conshdlrdata->nallconsanddatas - 1; c >= 0; --c )
   {
      SCIP_VAR** tmpvars;
      int stmpvars;
      SCIP_CONS* cons;
      int v;
 
      consanddata = allconsanddatas[c];
 
      assert(consanddata->nvars == 0 || (consanddata->vars != NULL && consanddata->svars > 0));
      assert(consanddata->nnewvars == 0 || (consanddata->newvars != NULL && consanddata->snewvars > 0));
 
      if( !consanddata->istransformed )
      {
         assert(consanddata->vars == NULL || consanddata->origcons != NULL);
         assert(consanddata->nvars == 0 || consanddata->origcons != NULL);
         assert(consanddata->svars == 0 || consanddata->origcons != NULL);
         assert(consanddata->newvars == NULL);
         assert(consanddata->nnewvars == 0);
         assert(consanddata->snewvars == 0);
 
         continue;
      }
 
      /* if no variables are left, delete variables arrays */
      if( consanddata->nvars == 0 )
      {
         SCIP_VAR* resvar = SCIPgetResultantAnd(scip, consanddata->cons);
 
         /* if we have no old variables, than also no new variables */
         assert(consanddata->nnewvars == 0);
         assert(consanddata->nuses > 0);
         assert(resvar != NULL);
 
         /* delete and-constraint */
         SCIP_CALL( SCIPdelCons(scip, consanddata->cons) );
         ++(*ndelconss);
 
         SCIP_CALL( transformToOrig(scip, consanddata, conshdlrdata) );
 
         /* release and-constraint */
         SCIP_CALL( SCIPreleaseCons(scip, &consanddata->cons) );
         consanddata->nuses = 0;
 
         /* remove consanddata from hashtable, if it existed only in transformed space */
         if( consanddata->origcons == NULL )
         {
            assert(SCIPhashtableExists(conshdlrdata->hashtable, (void*)consanddata));
            SCIP_CALL( SCIPhashtableRemove(conshdlrdata->hashtable, (void*)consanddata) );
         }
         assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)resvar));
         SCIP_CALL( SCIPhashmapRemove(conshdlrdata->hashmap, (void*)resvar) );
 
         continue;
      }
 
      /* the consanddata object is not used anymore, so extract the and constraint and delete other data */
      if( consanddata->nuses == 0 )
      {
         SCIP_Bool looseorcolumn;
         SCIP_VARSTATUS varstatus;
 
         if( consanddata->cons == NULL )
         {
            assert(!consanddata->istransformed || consanddata->noriguses > 0);
            assert((consanddata->noriguses > 0) == (consanddata->origcons != NULL));
            assert(consanddata->vars == NULL || consanddata->origcons != NULL);
            assert(consanddata->nvars == 0 || consanddata->origcons != NULL);
            assert(consanddata->svars == 0 || consanddata->origcons != NULL);
            assert(consanddata->newvars == NULL);
            assert(consanddata->nnewvars == 0);
            assert(consanddata->snewvars == 0);
 
            continue;
         }
 
         SCIP_CALL( transformToOrig(scip, consanddata, conshdlrdata) );
 
         varstatus = SCIPvarGetStatus(SCIPgetResultantAnd(scip, consanddata->cons));
         looseorcolumn = (varstatus == SCIP_VARSTATUS_LOOSE || varstatus == SCIP_VARSTATUS_COLUMN);
 
         /* @note due to aggregations or fixings the resultant may need to be propagated later on, so we can only
          *       delete the and-constraint if the resultant is of column or loose status
          *       and is not an active variable of another (multi-)aggregated/negated variable
          */
         if( looseorcolumn )
         {
            SCIP_VAR* resvar = SCIPgetResultantAnd(scip, consanddata->cons);
            SCIP_Bool del = TRUE;
            int w;
 
            assert(nvars >= 1);
 
            /* we need to check all active representatives */
            for( w = 0; w < nfixedvars && del; ++w )
            {
               int nactivevars;
               int requiredsize;
               int i;
 
               assert(fixedvars != NULL);
               assert(activevars != NULL);
               assert(activescalars != NULL);
               activevars[0] = fixedvars[w];
               activescalars[0] = 1.0;
               activeconstant = 0.0;
               nactivevars = 1;
               SCIP_CALL( SCIPgetProbvarLinearSum(scip, activevars, activescalars, &nactivevars, nvars,
                     &activeconstant, &requiredsize, TRUE) );
               assert(requiredsize <= nvars);
 
               for( i = 0; i < nactivevars && del; ++i )
               {
                  assert(SCIPvarGetStatus(activevars[i]) == SCIP_VARSTATUS_LOOSE || SCIPvarGetStatus(activevars[i]) == SCIP_VARSTATUS_COLUMN || SCIPvarGetStatus(activevars[i]) == SCIP_VARSTATUS_FIXED);
 
                  if( activevars[i] == resvar )
                     del = FALSE;
               }
            }
 
            if( del )
            {
               SCIP_CALL( SCIPdelCons(scip, consanddata->cons) );
            }
         }
 
         if( !SCIPconsIsDeleted(consanddata->cons) )
         {
            /* change flags */
            if( !looseorcolumn )
            {
               SCIP_CALL( SCIPsetConsInitial(scip, consanddata->cons, FALSE) );
            }
            SCIP_CALL( SCIPsetConsChecked(scip, consanddata->cons, TRUE) );
         }
 
         /* remove consanddata from hashtable, if it existed only in transformed space */
         if( consanddata->origcons == NULL )
         {
            assert(SCIPhashtableExists(conshdlrdata->hashtable, (void*)consanddata));
            SCIP_CALL( SCIPhashtableRemove(conshdlrdata->hashtable, (void*)consanddata) );
         }
         assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddata->cons)));
         SCIP_CALL( SCIPhashmapRemove(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddata->cons)) );
 
         SCIP_CALL( SCIPreleaseCons(scip, &(consanddata->cons)) );
         ++(*ndelconss);
 
         continue;
      }
 
      cons = consanddata->cons;
      assert(cons != NULL);
 
      /* if and-constraint is deleted, delete variables arrays */
      if( SCIPconsIsDeleted(cons) )
      {
         SCIP_VAR* resvar = SCIPgetResultantAnd(scip, consanddata->cons);
 
         assert(consanddata->nuses > 0);
         assert(resvar != NULL);
 
         SCIP_CALL( transformToOrig(scip, consanddata, conshdlrdata) );
 
         /* release and-constraint */
         SCIP_CALL( SCIPreleaseCons(scip, &consanddata->cons) );
         consanddata->nuses = 0;
 
         /* remove consanddata from hashtable, if it existed only in transformed space */
         if( consanddata->origcons == NULL )
         {
            assert(SCIPhashtableExists(conshdlrdata->hashtable, (void*)consanddata));
            SCIP_CALL( SCIPhashtableRemove(conshdlrdata->hashtable, (void*)consanddata) );
         }
         assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)resvar));
         SCIP_CALL(