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.

Parameters:
var the variable id in Dimacs format
Returns:
the truth value of that variable in the model
Since:
1.6
See also:
model()

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