klee

Manages constraints, e.g. optimisation. More...
#include <Constraints.h>
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 
Manages constraints, e.g. optimisation.
Definition at line 50 of file Constraints.h.

explicit 
Create constraint manager that modifies constraints
constraints 
Definition at line 163 of file Constraints.cpp.
Add constraint to the referenced constraint set
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().
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().

private 
Rewrite set of constraints using the visitor
visitor  constraint rewriter 
Definition at line 73 of file Constraints.cpp.
References addConstraintInternal(), constraints, klee::ConstraintSet::push_back(), and klee::ExprVisitor::visit().
Referenced by addConstraintInternal().

static 
Simplify expression expr based on constraints
constraints  set of constraints used for simplification 
expr  to simplify 
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().

private 
Definition at line 76 of file Constraints.h.
Referenced by addConstraint(), addConstraintInternal(), rewriteConstraints(), and simplifyExpr().