Logo Search packages:      
Sourcecode: sat4j version File versions

boolean org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>::model ( int  var  )  [inline]

Provide the truth value of a specific variable in the model. That method should be called AFTER isSatisfiable() if the formula is satisfiable. Else an exception UnsupportedOperationException is launched.

var the variable id in Dimacs format
the truth value of that variable in the model
See also:

Implements org::sat4j::specs::IProblem.

Definition at line 940 of file Solver.java.

            if (var <= 0 || var > nVars()) {
                  throw new IllegalArgumentException(
                              "Use a valid Dimacs var id as argument!"); //$NON-NLS-1$
            if (fullmodel == null) {
                  throw new UnsupportedOperationException(
                              "Call the solve method first!!!"); //$NON-NLS-1$
            return fullmodel[var - 1];

Generated by  Doxygen 1.6.0   Back to index