org.evosuite.symbolic.solver

Class Solver

java.lang.Object

org.evosuite.symbolic.solver.Solver

Direct Known Subclasses:

EvoSuiteSolver, SubProcessSolver

public abstract class Solver
extends Object

Interface for SMT solvers

Author:

Gordon Fraser

Constructor Summary

Constructors

Constructor and Description
Solver()
Solver(boolean addMissingVariables)

Method Summary

Modifier and Type	Method and Description
protected boolean	addMissingVariables()
protected static boolean	checkSAT(Collection<Constraint<?>> constraints, SolverResult satResult)
protected static Map<String,Object>	getConcreteValues(Set<Variable<?>> variables) Returns a mapping from variables to their current concrete values.
protected static Set<Variable<?>>	getVariables(Collection<Constraint<?>> constraints) Creates a set with all the variables in the constraints.
protected static void	setConcreteValues(Set<Variable<?>> variables, Map<String,Object> concrete_values) Restore all concrete values of the variables using the concrete_values mapping.
abstract SolverResult	solve(Collection<Constraint<?>> constraints)

Methods inherited from class java.lang.Object

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

Constructor Detail

Solver

public Solver()

Solver

public Solver(boolean addMissingVariables)

Method Detail

addMissingVariables

protected boolean addMissingVariables()

solve

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

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

getConcreteValues

protected static Map<String,Object> getConcreteValues(Set<Variable<?>> variables)

Returns a mapping from variables to their current concrete values.

Parameters:

variables -

Returns:

a mapping from variables to their current concrete values.

getVariables

protected static Set<Variable<?>> getVariables(Collection<Constraint<?>> constraints)

Creates a set with all the variables in the constraints.

Parameters:

constraints - the constraint system

Returns:

the set of variables in the constraint system

setConcreteValues

protected static void setConcreteValues(Set<Variable<?>> variables,
                                        Map<String,Object> concrete_values)

Restore all concrete values of the variables using the concrete_values mapping.

Parameters:

variables -

concrete_values -

checkSAT

protected static boolean checkSAT(Collection<Constraint<?>> constraints,
                                  SolverResult satResult)