org.evosuite.symbolic.solver.cvc4

Class CVC4Solver

java.lang.Object

org.evosuite.symbolic.solver.Solver

org.evosuite.symbolic.solver.SubProcessSolver

org.evosuite.symbolic.solver.cvc4.CVC4Solver

public final class CVC4Solver
extends SubProcessSolver

Constructor Summary

Constructors

Constructor and Description
CVC4Solver()
CVC4Solver(boolean addMissingValues)

Method Summary

Modifier and Type	Method and Description
void	setRewriteNonLinearConstraints(boolean rewrite) If enabled the translation will approximate non-linear constraints with concrete values
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

CVC4Solver

public CVC4Solver(boolean addMissingValues)

CVC4Solver

public CVC4Solver()

Method Detail

setRewriteNonLinearConstraints

public void setRewriteNonLinearConstraints(boolean rewrite)

If enabled the translation will approximate non-linear constraints with concrete values

Parameters:

rewrite -

solve

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

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

SolverEmptyQueryException - the solver

SolverErrorException - the solver reported an error after its execution

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

IOException - an IOException occurred while executing the solver