public class SMTProblem
extends java.lang.Object
SMTProblem
is related to a set of solvers that are used to
solve this problem.Modifier and Type | Field and Description |
---|---|
private Goal |
goal |
private java.lang.String |
name |
private Sequent |
sequent |
private java.util.Collection<SMTSolver> |
solvers |
private Term |
term |
Constructor and Description |
---|
SMTProblem(Goal goal) |
SMTProblem(Sequent s,
Services services) |
SMTProblem(Term t) |
Modifier and Type | Method and Description |
---|---|
(package private) void |
addSolver(SMTSolver solver)
Relates a solver to the problem
|
static java.util.Collection<SMTProblem> |
createSMTProblems(Proof proof)
Creates out of a proof object several SMT problems.
|
SMTSolverResult |
getFinalResult()
Returns the result of the problem.
|
Goal |
getGoal() |
java.lang.String |
getName() |
Sequent |
getSequent() |
java.util.Collection<SMTSolver> |
getSolvers()
Returns the solvers that are related to the problem
|
Term |
getTerm()
Returns the term that is related to this problem.
|
private Term |
goalToTerm(Goal g) |
private Term |
sequentToTerm(Sequent s) |
private static Term |
sequentToTerm(Sequent s,
Services services) |
private Term term
private java.util.Collection<SMTSolver> solvers
private final Goal goal
private Sequent sequent
private java.lang.String name
public static java.util.Collection<SMTProblem> createSMTProblems(Proof proof)
public Term getTerm()
public java.util.Collection<SMTSolver> getSolvers()
public Goal getGoal()
public Sequent getSequent()
public SMTSolverResult getFinalResult()
public java.lang.String getName()
void addSolver(SMTSolver solver)
solver
-