org.evosuite.symbolic.solver.z3

Class Z3Solver

java.lang.Object

org.evosuite.symbolic.solver.Solver

org.evosuite.symbolic.solver.SubProcessSolver

org.evosuite.symbolic.solver.z3.Z3Solver

public class Z3Solver
extends SubProcessSolver

Constructor Summary

Constructors

Constructor and Description
Z3Solver()
Z3Solver(boolean addMissingVariables)

Method Summary

Modifier and Type	Method and Description
SolverResult	solve(Collection<Constraint<?>> constraints)

Methods inherited from class org.evosuite.symbolic.solver.SubProcessSolver

launchNewProcess

Methods inherited from class org.evosuite.symbolic.solver.Solver

addMissingVariables, checkSAT, getConcreteValues, getVariables, setConcreteValues

Methods inherited from class java.lang.Object

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

Constructor Detail

Z3Solver

public Z3Solver()

Z3Solver

public Z3Solver(boolean addMissingVariables)

Method Detail

solve

public SolverResult solve(Collection<Constraint<?>> constraints)
                   throws SolverTimeoutException,
                          IOException,
                          SolverParseException,
                          SolverEmptyQueryException,
                          SolverErrorException

Specified by:

solve in class Solver

Parameters:

constraints - a constraint system to be solved

Returns:

a non-null result that is SAT or UNSAT

Throws:

SolverTimeoutException - a timeout occurred while executing the solver

IOException - an IOException occurred while executing the solver

SolverParseException - the solver's result could not be parsed into a valid SolverResult

SolverEmptyQueryException - the solver

SolverErrorException - the solver reported an error after its execution