klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
klee::Query Struct Reference

#include <Solver.h>

Collaboration diagram for klee::Query:

Public Member Functions

 Query (const ConstraintManager &_constraints, ref< Expr > _expr)
 
Query withExpr (ref< Expr > _expr) const
 withExpr - Return a copy of the query with the given expression. More...
 
Query withFalse () const
 withFalse - Return a copy of the query with a false expression. More...
 
Query negateExpr () const
 negateExpr - Return a copy of the query with the expression negated. More...
 

Public Attributes

const ConstraintManagerconstraints
 
ref< Exprexpr
 

Detailed Description

Definition at line 22 of file Solver.h.

Constructor & Destructor Documentation

klee::Query::Query ( const ConstraintManager _constraints,
ref< Expr _expr 
)
inline

Definition at line 27 of file Solver.h.

Referenced by withExpr(), and withFalse().

Here is the caller graph for this function:

Member Function Documentation

Query klee::Query::negateExpr ( ) const
inline

negateExpr - Return a copy of the query with the expression negated.

Definition at line 42 of file Solver.h.

References klee::Expr::createIsZero(), expr, and withExpr().

Referenced by CexCachingSolver::computeTruth(), klee::SolverImpl::computeValidity(), klee::IncompleteSolver::computeValidity(), CachingSolver::computeValidity(), CexCachingSolver::computeValidity(), klee::StagedSolverImpl::computeValidity(), and klee::Solver::mustBeFalse().

Here is the call graph for this function:

Here is the caller graph for this function:

Query klee::Query::withExpr ( ref< Expr _expr) const
inline

withExpr - Return a copy of the query with the given expression.

Definition at line 32 of file Solver.h.

References constraints, and Query().

Referenced by ValidatingSolver::computeValue(), klee::Solver::getRange(), and negateExpr().

Here is the call graph for this function:

Here is the caller graph for this function:

Query klee::Query::withFalse ( ) const
inline

withFalse - Return a copy of the query with a false expression.

Definition at line 37 of file Solver.h.

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

Referenced by CexCachingSolver::computeValidity(), QueryLoggingSolver::computeValue(), CexCachingSolver::computeValue(), and STPSolverImpl::computeValue().

Here is the call graph for this function:

Here is the caller graph for this function:

Member Data Documentation


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