public final class Solution extends Object
formula: Formula // the formula being solved
bounds: Bounds // the bounds on the formula
Modifier and Type  Class and Description 

static class 
Solution.Outcome
Enumerates the possible outcomes of an attempt
to find a model for a FOL formula.

Modifier and Type  Method and Description 

Instance 
instance()
Returns a satisfiying instance for this.formula, if the
value returned by
this.outcome() is either
SATISFIABLE or TRIVIALLY_SATISFIABLE. 
Solution.Outcome 
outcome()
Returns the outcome of the attempt to find
a model for this.formula.

Proof 
proof()
Returns a proof of this.formula's unsatisfiability if the value
returned by
this.outcome() is UNSATISFIABLE or
TRIVIALLY_UNSATISFIABLE, translation logging was enabled during solving,
and a core extracting sat solver (if any)
was used to determine unsatisfiability. 
boolean 
sat()
Returns true iff this solution has a (trivially) satisfiable outcome.

Statistics 
stats()
Returns the statistics gathered while solving
this.formula.

String 
toString()
Returns a string representation of this Solution.

boolean 
unsat()
Returns true iff this solution has a (trivially) unsatisfiable outcome.

public Instance instance()
this.outcome()
is either
SATISFIABLE or TRIVIALLY_SATISFIABLE. Otherwise returns null.public Solution.Outcome outcome()
instance()
.
If the formula is UNSATISFIABLE, a proof of unsatisfiability
can be obtained by calling proof()
provided that
translation logging was enabled and the unsatisfiability was
determined using a core extracting
sat solver
.
Lastly, if the returned Outcome is
or TRIVIALLY_UNSATISFIABLE, a proof of unsatisfiability can
be obtained by calling proof()
provided that
translation logging was enabled.public Proof proof()
this.outcome()
is UNSATISFIABLE or
TRIVIALLY_UNSATISFIABLE, translation logging was enabled during solving,
and a core extracting sat solver
(if any)
was used to determine unsatisfiability.
Otherwise, null is returned.public final boolean sat()
public Statistics stats()
public String toString()
public final boolean unsat()
© Emina Torlak 20052012