Uses of Interface

Packages that use IConstr
org.sat4j.minisat.constraints Implementations of various constraints for MiniSAT. 
org.sat4j.minisat.constraints.card Implementations of cardinality contraints. 
org.sat4j.minisat.constraints.cnf Implementations of clausal contraints. 
org.sat4j.minisat.constraints.pb Implementations of pseudo boolean contraints. 
org.sat4j.minisat.core Implementation of the MiniSAT solver skeleton. 
org.sat4j.minisat.uip Various ways to compute an asserting clause (containing one Unique Implication Point). 
org.sat4j.specs Those classes are intented for users dealing with SAT solvers as blackboxes. Tools to be used on top of an ISolver. 

Uses of IConstr in org.sat4j.minisat.constraints

Methods in org.sat4j.minisat.constraints that return IConstr
 IConstr AbstractPBDataStructureFactory.createUnregisteredPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)

Uses of IConstr in org.sat4j.minisat.constraints.card

Classes in org.sat4j.minisat.constraints.card that implement IConstr
 class AtLeast
 class MaxWatchCard
 class MinWatchCard

Uses of IConstr in org.sat4j.minisat.constraints.cnf

Classes in org.sat4j.minisat.constraints.cnf that implement IConstr
 class BinaryClauses
 class CBClause
 class MixableCBClause
          Counter Based clauses that can be mixed with WLCLauses
 class TernaryClauses
 class WLClause
          Lazy data structure for clause using Watched Literals.

Uses of IConstr in org.sat4j.minisat.constraints.pb

Classes in org.sat4j.minisat.constraints.pb that implement IConstr
 class MaxWatchPb
 class MinWatchPb
 class WatchPb

Methods in org.sat4j.minisat.constraints.pb that return IConstr
 IConstr IInternalPBConstraintCreator.createUnregisteredPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)

Uses of IConstr in org.sat4j.minisat.core

Subinterfaces of IConstr in org.sat4j.minisat.core
 interface Constr

Methods in org.sat4j.minisat.core that return IConstr
 IConstr Solver.addAtLeast(IVecInt literals, int degree)
 IConstr Solver.addAtMost(IVecInt literals, int degree)
 IConstr Solver.addClause(IVecInt literals)
 IConstr Solver.addPseudoBoolean(IVecInt literals, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger degree)
 IConstr Solver.getIthConstr(int i)
          returns the ith constraint in the solver.

Methods in org.sat4j.minisat.core with parameters of type IConstr
 boolean AssertingClauseGenerator.clauseNonAssertive(IConstr reason)
          method indicating if an asserting clause has been built. note that this method is called right after a resolution step is finished.
 boolean Solver.removeConstr(IConstr co)

Uses of IConstr in org.sat4j.minisat.uip

Methods in org.sat4j.minisat.uip with parameters of type IConstr
 boolean FirstUIP.clauseNonAssertive(IConstr reason)
 boolean DecisionUIP.clauseNonAssertive(IConstr reason)

Uses of IConstr in org.sat4j.specs

Methods in org.sat4j.specs that return IConstr
 IConstr ISolver.addAtLeast(IVecInt literals, int degree)
          Create a cardinality constraint of the type "at least n of those literals must be satisfied"
 IConstr ISolver.addAtMost(IVecInt literals, int degree)
          Create a cardinality constraint of the type "at most n of those literals must be satisfied"
 IConstr ISolver.addClause(IVecInt literals)
          Create a clause from a set of literals The literals are represented by non null integers such that opposite literals a represented by opposite values.
 IConstr ISolver.addPseudoBoolean(IVecInt lits, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger d)
          Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied"

Methods in org.sat4j.specs with parameters of type IConstr
 boolean ISolver.removeConstr(IConstr c)
          Remove a constraint returned by one of the add method from the solver.

Uses of IConstr in

Methods in that return IConstr
 IConstr SolverDecorator.addAtLeast(IVecInt literals, int degree)
 IConstr SolverDecorator.addAtMost(IVecInt literals, int degree)
 IConstr SolverDecorator.addClause(IVecInt literals)
 IConstr SolverDecorator.addPseudoBoolean(IVecInt literals, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger degree)

Methods in with parameters of type IConstr
 boolean SolverDecorator.removeConstr(IConstr c)