public class SMTProblem extends 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 String |
name |
private Sequent |
sequent |
private 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 Collection<SMTProblem> |
createSMTProblems(Proof proof)
Creates out of a proof object several SMT problems.
|
SMTSolverResult |
getFinalResult()
Returns the result of the problem.
|
Goal |
getGoal() |
String |
getName() |
Sequent |
getSequent() |
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 Collection<SMTSolver> solvers
private final Goal goal
private Sequent sequent
private String name
public static Collection<SMTProblem> createSMTProblems(Proof proof)
public Term getTerm()
public Collection<SMTSolver> getSolvers()
public Goal getGoal()
public Sequent getSequent()
public SMTSolverResult getFinalResult()
public String getName()
void addSolver(SMTSolver solver)
solver
-