klee
Public Member Functions | Public Attributes | List of all members
klee::Query Struct Reference

#include <Solver.h>

Collaboration diagram for klee::Query:
Collaboration graph
[legend]

Public Member Functions

 Query (const ConstraintSet &_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...
 
void dump () const
 Dump query. More...
 

Public Attributes

const ConstraintSet & constraints
 
ref< Expr > expr
 

Detailed Description

Definition at line 32 of file Solver.h.

Constructor & Destructor Documentation

◆ Query()

klee::Query::Query ( const ConstraintSet &  _constraints,
ref< Expr >  _expr 
)
inline

Definition at line 37 of file Solver.h.

Referenced by withExpr(), and withFalse().

Here is the caller graph for this function:

Member Function Documentation

◆ dump()

void Query::dump ( ) const

Dump query.

Definition at line 224 of file Solver.cpp.

References constraints, klee::Expr::dump(), and expr.

Referenced by CexCachingSolver::getAssignment().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ negateExpr()

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

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

Definition at line 52 of file Solver.h.

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

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

Here is the call graph for this function:
Here is the caller graph for this function:

◆ withExpr()

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

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

Definition at line 42 of file Solver.h.

References constraints, and Query().

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

Here is the call graph for this function:
Here is the caller graph for this function:

◆ withFalse()

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

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

Definition at line 47 of file Solver.h.

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

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

Here is the call graph for this function:
Here is the caller graph for this function:

Member Data Documentation

◆ constraints

const ConstraintSet& klee::Query::constraints

Definition at line 34 of file Solver.h.

Referenced by assertCreatedPointEvaluatesToTrue(), CachingSolver::cacheInsert(), CachingSolver::cacheLookup(), klee::AssignmentValidatingSolver::computeInitialValues(), klee::ValidatingSolver::computeInitialValues(), dump(), klee::AssignmentValidatingSolver::dumpAssignmentQuery(), getAllIndependentConstraintsSets(), getIndependentConstraints(), CexCachingSolver::lookupAssignment(), klee::ExprSMTLIBPrinter::printHumanReadableQuery(), KQueryLoggingSolver::printQuery(), klee::ExprSMTLIBPrinter::printQueryInSingleAssert(), propogateValues(), klee::ExprSMTLIBPrinter::scanAll(), withExpr(), and withFalse().

◆ expr

ref<Expr> klee::Query::expr

Definition at line 35 of file Solver.h.

Referenced by assertCreatedPointEvaluatesToTrue(), CachingSolver::cacheInsert(), CachingSolver::cacheLookup(), klee::AssignmentValidatingSolver::computeInitialValues(), klee::ValidatingSolver::computeInitialValues(), IndependentSolver::computeTruth(), CexCachingSolver::computeValidity(), IndependentSolver::computeValidity(), CexCachingSolver::computeValue(), FastCexSolver::computeValue(), IndependentSolver::computeValue(), klee::ValidatingSolver::computeValue(), dump(), klee::AssignmentValidatingSolver::dumpAssignmentQuery(), klee::Solver::evaluate(), getAllIndependentConstraintsSets(), getIndependentConstraints(), klee::Solver::getRange(), klee::Solver::getValue(), CexCachingSolver::lookupAssignment(), klee::Solver::mustBeTrue(), negateExpr(), klee::ExprSMTLIBPrinter::printHumanReadableQuery(), KQueryLoggingSolver::printQuery(), klee::ExprSMTLIBPrinter::printQueryInSingleAssert(), propogateValues(), and klee::ExprSMTLIBPrinter::scanAll().

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