klee::ConstraintManager Class Reference

Manages constraints, e.g. optimisation. More...

#include <Constraints.h>

Collaboration diagram for klee::ConstraintManager:

Public Member Functions
	ConstraintManager (ConstraintSet &constraints)
void	addConstraint (const ref< Expr > &constraint)

Static Public Member Functions
static ref< Expr >	simplifyExpr (const ConstraintSet &constraints, const ref< Expr > &expr)

Private Member Functions
bool	rewriteConstraints (ExprVisitor &visitor)
void	addConstraintInternal (const ref< Expr > &constraint)
	Add constraint to the set of constraints. More...

Private Attributes
ConstraintSet &	constraints

Detailed Description

Manages constraints, e.g. optimisation.

Definition at line 50 of file Constraints.h.

Constructor & Destructor Documentation

ConstraintManager()

ConstraintManager::ConstraintManager ( ConstraintSet &  constraints )

explicit

Create constraint manager that modifies constraints

Parameters

constraints

Definition at line 163 of file Constraints.cpp.

Member Function Documentation

addConstraint()

void ConstraintManager::addConstraint

(

const ref< Expr > &

constraint

)

Add constraint to the referenced constraint set

Parameters

constraint

Definition at line 158 of file Constraints.cpp.

References addConstraintInternal(), constraints, and simplifyExpr().

Referenced by klee::ExecutionState::addConstraint(), klee::Executor::getSymbolicSolution(), klee::ExecutionState::merge(), and klee::SeedInfo::patchSeed().

Here is the call graph for this function:

Here is the caller graph for this function:

addConstraintInternal()

void ConstraintManager::addConstraintInternal ( const ref< Expr > &  constraint )

private

Add constraint to the set of constraints.

Definition at line 118 of file Constraints.cpp.

References addConstraintInternal(), klee::Expr::And, klee::Expr::Constant, constraints, klee::Expr::Eq, klee::Expr::getKind(), klee::BinaryExpr::left, klee::ConstraintSet::push_back(), rewriteConstraints(), and klee::BinaryExpr::right.

Referenced by addConstraint(), addConstraintInternal(), and rewriteConstraints().

Here is the call graph for this function:

Here is the caller graph for this function:

rewriteConstraints()

bool ConstraintManager::rewriteConstraints ( ExprVisitor &  visitor )

private

Rewrite set of constraints using the visitor

Parameters

visitor

constraint rewriter

Returns

true iff any constraint has been changed

Definition at line 73 of file Constraints.cpp.

References addConstraintInternal(), constraints, klee::ConstraintSet::push_back(), and klee::ExprVisitor::visit().

Referenced by addConstraintInternal().

Here is the call graph for this function:

Here is the caller graph for this function:

simplifyExpr()

ref< Expr > ConstraintManager::simplifyExpr ( const ConstraintSet &  constraints, const ref< Expr > &  expr  )

static

Simplify expression expr based on constraints

Parameters

constraints	set of constraints used for simplification
expr	to simplify

Returns

simplified expression

Definition at line 92 of file Constraints.cpp.

References klee::ConstantExpr::alloc(), klee::Expr::Bool, constraints, and klee::ExprVisitor::visit().

Referenced by addConstraint(), klee::TimingSolver::evaluate(), klee::Executor::executeGetValue(), klee::Executor::executeMemoryOperation(), klee::TimingSolver::getValue(), klee::TimingSolver::mustBeTrue(), and klee::Executor::toConstant().

Here is the call graph for this function:

Here is the caller graph for this function:

Member Data Documentation

constraints

ConstraintSet& klee::ConstraintManager::constraints

private

Definition at line 76 of file Constraints.h.

Referenced by addConstraint(), addConstraintInternal(), rewriteConstraints(), and simplifyExpr().

---

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

• /Users/cristic/klee/include/klee/Expr/Constraints.h
• /Users/cristic/klee/lib/Expr/Constraints.cpp