STPSolver - A complete solver based on STP. More...

#include <STPSolver.h>

Inheritance diagram for klee::STPSolver:

Collaboration diagram for klee::STPSolver:

Public Member Functions
	STPSolver (bool useForkedSTP, bool optimizeDivides=true)

virtual char *	getConstraintLog (const Query &)

virtual void	setCoreSolverTimeout (time::Span timeout)

Public Member Functions inherited from klee::Solver
	Solver (SolverImpl *_impl)

virtual	~Solver ()

bool	evaluate (const Query &, Validity &result)

bool	mustBeTrue (const Query &, bool &result)

bool	mustBeFalse (const Query &, bool &result)

bool	mayBeTrue (const Query &, bool &result)

bool	mayBeFalse (const Query &, bool &result)

bool	getValue (const Query &, ref< ConstantExpr > &result)

bool	getInitialValues (const Query &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &result)

virtual std::pair< ref< Expr >, ref< Expr > >	getRange (const Query &)

virtual char *	getConstraintLog (const Query &query)

virtual void	setCoreSolverTimeout (time::Span timeout)

Additional Inherited Members
Public Types inherited from klee::Solver
enum	Validity { True = 1 , False = -1 , Unknown = 0 }

Static Public Member Functions inherited from klee::Solver
static const char *	validity_to_str (Validity v)
	validity_to_str - Return the name of given Validity enum value. More...

Public Attributes inherited from klee::Solver
SolverImpl *	impl

Detailed Description

STPSolver - A complete solver based on STP.

Definition at line 18 of file STPSolver.h.

Constructor & Destructor Documentation

STPSolver - Construct a new STPSolver.

Parameters

useForkedSTP	- Whether STP should be run in a separate process (required for using timeouts).
optimizeDivides	- Whether constant division operations should be optimized into add/shift/multiply operations.

virtual char * klee::STPSolver::getConstraintLog ( const Query & )

virtual

getConstraintLog - Return the constraint log for the given state in CVC format.

Reimplemented from klee::Solver.

virtual void klee::STPSolver::setCoreSolverTimeout ( time::Span timeout )

virtual

setCoreSolverTimeout - Set constraint solver timeout delay to the given value; 0 is off.

Reimplemented from klee::Solver.

The documentation for this class was generated from the following file: