Logo Search packages:      
Sourcecode: sat4j version File versions

org::sat4j::pb::constraints::pb::ConflictMap Class Reference

Inheritance diagram for org::sat4j::pb::constraints::pb::ConflictMap:

org::sat4j::pb::constraints::pb::MapPb

List of all members.


Detailed Description

Author:
parrain TODO To change the template for this generated type comment go to Window - Preferences - Java - Code Style - Code Templates

Definition at line 42 of file ConflictMap.java.


Public Member Functions

void buildConstraintFromConflict (IVecInt resLits, IVec< BigInteger > resCoefs)
void buildConstraintFromMapPb (int[] resLits, BigInteger[] resCoefs)
BigInteger cuttingPlane (int lits[], BigInteger[] reducedCoefs, BigInteger degreeCons, BigInteger coefMult)
BigInteger cuttingPlane (int[] lits, BigInteger[] reducedCoefs, BigInteger deg)
BigInteger cuttingPlane (PBConstr cpb, BigInteger degreeCons, BigInteger[] reducedCoefs, BigInteger coefMult, VarActivityListener val)
BigInteger cuttingPlane (PBConstr cpb, BigInteger deg, BigInteger[] reducedCoefs, VarActivityListener val)
int getBacktrackLevel (int maxLevel)
BigInteger getDegree ()
boolean isAssertive (int dl)
boolean isCardinality ()
int oldGetBacktrackLevel (int maxLevel)
boolean oldIsAssertive (int dl)
BigInteger reduceInConstraint (WatchPb wpb, final BigInteger[] coefsBis, final int indLitImplied, final BigInteger degreeBis)
BigInteger resolve (PBConstr cpb, int litImplied, VarActivityListener val)
BigInteger saturation ()
int size ()
BigInteger slackConflict ()
boolean slackIsCorrect (int dl)
String toString ()
void updateSlack (int level)

Static Public Member Functions

static IConflict createConflict (PBConstr cpb, int level)

Protected Member Functions

BigInteger reduceUntilConflict (int litImplied, int ind, BigInteger[] reducedCoefs, WatchPb wpb)

Static Protected Member Functions

static BigInteger ppcm (BigInteger a, BigInteger b)

Protected Attributes

VecInt[] byLevel
BigInteger coefMult = BigInteger.ZERO
BigInteger coefMultCons = BigInteger.ZERO
int currentLevel
BigInteger currentSlack
BigInteger degree
InternalMapPBStructure weightedLits

Package Functions

void changeCoef (int indLit, BigInteger newValue)
 ConflictMap (PBConstr cpb, int level)
void decreaseCoef (int lit, BigInteger decCoef)
void increaseCoef (int lit, BigInteger incCoef)
void removeCoef (int lit)
void setCoef (int lit, BigInteger newValue)

Static Package Functions

static BigInteger saturation (BigInteger[] coefs, BigInteger degree)

Private Member Functions

BigInteger computeSlack (int dl)
int getLevelByLevel (int lit)
void initStructures ()
boolean isImplyingLiteral (BigInteger slack)
boolean isImplyingLiteralOrdered (int dl, BigInteger slack)

Static Private Member Functions

static final int indexToLevel (int indLevel)
static final int levelToIndex (int level)
static boolean positiveCoefs (final BigInteger[] coefsCons)

Private Attributes

final ILits voc

The documentation for this class was generated from the following file:

Generated by  Doxygen 1.6.0   Back to index