de.uka.ilkd.key.smt

Class SMTProblem

java.lang.Object

de.uka.ilkd.key.smt.SMTProblem

public class SMTProblem
extends java.lang.Object

Represents a problem that can be passed to a solver. This class was introduced because the SMT module must handle both goals and terms.
Each SMTProblem is related to a set of solvers that are used to solve this problem.

Field Summary

Fields

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 Summary

Constructors

Constructor and Description
SMTProblem(Goal goal)
SMTProblem(Sequent s, Services services)
SMTProblem(Term t)

Method Summary

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)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

term

private Term term

solvers

private java.util.Collection<SMTSolver> solvers

goal

private final Goal goal

sequent

private Sequent sequent

name

private java.lang.String name

Constructor Detail

SMTProblem

public SMTProblem(Goal goal)

SMTProblem

public SMTProblem(Sequent s,
                  Services services)

SMTProblem

public SMTProblem(Term t)

Method Detail

createSMTProblems

public static java.util.Collection<SMTProblem> createSMTProblems(Proof proof)

Creates out of a proof object several SMT problems. For each open goal a new SMT problem is created.

getTerm

public Term getTerm()

Returns the term that is related to this problem. If the problem was initialized with a goal, the goal is transformed to the term that can be accessed by this method.

getSolvers

public java.util.Collection<SMTSolver> getSolvers()

Returns the solvers that are related to the problem

getGoal

public Goal getGoal()

getSequent

public Sequent getSequent()

getFinalResult

public SMTSolverResult getFinalResult()

Returns the result of the problem. If more than one solver have been applied on the problem it computes the result from the results of the solvers. In case that one solver returned a positive result (valid) and another one a negative result (falsifiable) an excpetion is thrown.

getName

public java.lang.String getName()

addSolver

void addSolver(SMTSolver solver)

Relates a solver to the problem

Parameters:

solver -

sequentToTerm

private static Term sequentToTerm(Sequent s,
                                  Services services)

sequentToTerm

private Term sequentToTerm(Sequent s)

goalToTerm

private Term goalToTerm(Goal g)