ROSE  0.9.10.89
Rose::BinaryAnalysis::Z3Solver Member List

This is the complete list of members for Rose::BinaryAnalysis::Z3Solver, including all inherited members.

assertions() const Rose::BinaryAnalysis::SmtSolvervirtual
assertions(size_t level) const Rose::BinaryAnalysis::SmtSolvervirtual
Availability typedefRose::BinaryAnalysis::SmtSolver
availability()Rose::BinaryAnalysis::SmtSolverstatic
availableLinkages()Rose::BinaryAnalysis::Z3Solverstatic
bestAvailable()Rose::BinaryAnalysis::SmtSolverstatic
bestLinkage(unsigned linkages)Rose::BinaryAnalysis::SmtSolverstatic
BIT_VECTOR enum value (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolver
BOOLEAN enum value (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolver
check()Rose::BinaryAnalysis::SmtSolvervirtual
checkExe()Rose::BinaryAnalysis::SmtSolverprotectedvirtual
checkLib() ROSE_OVERRIDERose::BinaryAnalysis::Z3Solvervirtual
checkTrivial()Rose::BinaryAnalysis::SmtSolvervirtual
classStatistics()Rose::BinaryAnalysis::SmtSolverstatic
classStats (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolverprotectedstatic
classStatsMutex (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolverprotectedstatic
clear_evidence() ROSE_DEPRECATED("use clearEvidence") (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolvervirtual
clearEvidence() ROSE_OVERRIDERose::BinaryAnalysis::Z3Solvervirtual
clearMemoization() ROSE_OVERRIDERose::BinaryAnalysis::SmtlibSolvervirtual
create() const Rose::BinaryAnalysis::Z3Solverinlinevirtual
Definitions typedefRose::BinaryAnalysis::SmtSolver
doMemoization_ (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolverprotected
evidence (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotected
evidence_for_address(uint64_t addr) ROSE_DEPRECATED("use evidenceForAddress") (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolvervirtual
evidence_for_name(const std::string &) ROSE_DEPRECATED("use evidenceForName") (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolvervirtual
evidence_for_variable(uint64_t varno) ROSE_DEPRECATED("use evidenceForVariable") (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolvervirtual
evidence_for_variable(const SymbolicExpr::Ptr &var) ROSE_DEPRECATED("use evidenceForVariable") (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolvervirtual
evidence_names() ROSE_DEPRECATED("use evidenceNames") (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolvervirtual
evidenceForAddress(uint64_t addr)Rose::BinaryAnalysis::SmtSolvervirtual
evidenceForName(const std::string &) ROSE_OVERRIDERose::BinaryAnalysis::SmtlibSolvervirtual
evidenceForVariable(const SymbolicExpr::Ptr &var)Rose::BinaryAnalysis::SmtSolverinlinevirtual
evidenceForVariable(uint64_t varno)Rose::BinaryAnalysis::SmtSolverinlinevirtual
evidenceNames() ROSE_OVERRIDERose::BinaryAnalysis::SmtlibSolvervirtual
ExprExprMap typedefRose::BinaryAnalysis::SmtSolver
findVariables(const SymbolicExpr::Ptr &) ROSE_OVERRIDERose::BinaryAnalysis::SmtlibSolvervirtual
generate_file(std::ostream &, const std::vector< SymbolicExpr::Ptr > &exprs, Definitions *) ROSE_DEPRECATED("use generateFile") (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolverprotectedvirtual
generateFile(std::ostream &, const std::vector< SymbolicExpr::Ptr > &exprs, Definitions *) ROSE_OVERRIDERose::BinaryAnalysis::SmtlibSolvervirtual
get_class_stats() ROSE_DEPRECATED("use classStatistics") (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolverstatic
get_command(const std::string &config_name) ROSE_DEPRECATED("use getCommand") (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolverprotectedvirtual
get_stats() const ROSE_DEPRECATED("use statistics") (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolver
getCommand(const std::string &configName) ROSE_OVERRIDERose::BinaryAnalysis::SmtlibSolvervirtual
getErrorMessage(int exitStatus) ROSE_OVERRIDERose::BinaryAnalysis::SmtlibSolvervirtual
initDiagnostics()Rose::BinaryAnalysis::SmtSolverstatic
insert(const SymbolicExpr::Ptr &)Rose::BinaryAnalysis::SmtSolvervirtual
insert(const std::vector< SymbolicExpr::Ptr > &)Rose::BinaryAnalysis::SmtSolvervirtual
instance(unsigned linkages=LM_ANY)Rose::BinaryAnalysis::Z3Solverinlinestatic
Rose::BinaryAnalysis::SmtlibSolver::instance(const std::string &name, const boost::filesystem::path &executable, const std::string &shellArgs="", unsigned linkages=LM_EXECUTABLE)Rose::BinaryAnalysis::SmtlibSolverinlinestatic
Rose::BinaryAnalysis::SmtSolver::instance(const std::string &name)Rose::BinaryAnalysis::SmtSolverstatic
latestMemoizationId() const Rose::BinaryAnalysis::SmtSolverinline
latestMemoizationId_ (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolverprotected
latestMemoizationRewrite_ (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolverprotected
linkage() const Rose::BinaryAnalysis::SmtSolverinline
linkage_ (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolverprotected
LinkMode enum nameRose::BinaryAnalysis::SmtSolver
LM_ANY enum valueRose::BinaryAnalysis::SmtSolver
LM_EXECUTABLE enum valueRose::BinaryAnalysis::SmtSolver
LM_LIBRARY enum valueRose::BinaryAnalysis::SmtSolver
LM_NONE enum valueRose::BinaryAnalysis::SmtSolver
MEM_STATE enum value (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolver
Memoization typedef (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolver
memoization() const Rose::BinaryAnalysis::SmtSolverinline
memoization(bool b)Rose::BinaryAnalysis::SmtSolverinline
memoization_ (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolverprotected
memoizationNEntries() const Rose::BinaryAnalysis::SmtSolverinlinevirtual
MemoizedEvidence typedef (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotected
memoizedEvidence (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotected
mlogRose::BinaryAnalysis::SmtSolverstatic
mostType(const std::vector< SExprTypePair > &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
name() const Rose::BinaryAnalysis::SmtSolverinline
name(const std::string &s)Rose::BinaryAnalysis::SmtSolverinline
nAssertions(size_t backtrackingLevel)Rose::BinaryAnalysis::SmtSolvervirtual
nLevels() const Rose::BinaryAnalysis::SmtSolverinlinevirtual
NO_TYPE enum value (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolver
normalizeVariables(const std::vector< SymbolicExpr::Ptr > &, SymbolicExpr::ExprExprHashMap &index)Rose::BinaryAnalysis::SmtSolverprotectedstatic
operator=(const SharedObject &)Sawyer::SharedObjectinline
outputArithmeticShiftRight(const SymbolicExpr::InteriorPtr &) ROSE_OVERRIDE (defined in Rose::BinaryAnalysis::Z3Solver)Rose::BinaryAnalysis::Z3Solverprotectedvirtual
outputAssertion(std::ostream &, const SymbolicExpr::Ptr &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputBinary(const std::string &func, const SymbolicExpr::InteriorPtr &, Type rettype=NO_TYPE) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputBvxorFunctions(std::ostream &, const std::vector< SymbolicExpr::Ptr > &) ROSE_OVERRIDERose::BinaryAnalysis::Z3Solverprotectedvirtual
outputCast(const SExprTypePair &, Type to) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputCast(const std::vector< SExprTypePair > &, Type to) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputComments(std::ostream &, const std::vector< SymbolicExpr::Ptr > &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputCommonSubexpressions(std::ostream &, const std::vector< SymbolicExpr::Ptr > &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputComparisonFunctions(std::ostream &, const std::vector< SymbolicExpr::Ptr > &) ROSE_OVERRIDERose::BinaryAnalysis::Z3Solverprotectedvirtual
outputDivide(const SymbolicExpr::InteriorPtr &, const std::string &operation) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputExpression(const SymbolicExpr::Ptr &) ROSE_OVERRIDE (defined in Rose::BinaryAnalysis::Z3Solver)Rose::BinaryAnalysis::Z3Solverprotectedvirtual
outputExpressions(const std::vector< SymbolicExpr::Ptr > &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputExtract(const SymbolicExpr::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputIte(const SymbolicExpr::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputLeaf(const SymbolicExpr::LeafPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputLeftAssoc(const std::string &func, const SymbolicExpr::InteriorPtr &, Type rettype=NO_TYPE) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputLeftAssoc(const std::string &func, const std::vector< SExprTypePair > &, Type rettype=NO_TYPE) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputList(const std::string &name, const SymbolicExpr::InteriorPtr &, Type rettype=NO_TYPE) (defined in Rose::BinaryAnalysis::Z3Solver)Rose::BinaryAnalysis::Z3Solverprotected
outputList(const std::string &name, const std::vector< SExprTypePair > &, Type rettype=NO_TYPE) (defined in Rose::BinaryAnalysis::Z3Solver)Rose::BinaryAnalysis::Z3Solverprotected
outputLogicalShiftRight(const SymbolicExpr::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputModulo(const SymbolicExpr::InteriorPtr &, const std::string &operation) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputMultiply(const SymbolicExpr::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputNotEqual(const SymbolicExpr::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputRead(const SymbolicExpr::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputRotateLeft(const SymbolicExpr::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputRotateRight(const SymbolicExpr::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputSet(const SymbolicExpr::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputShiftLeft(const SymbolicExpr::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputSignedCompare(const SymbolicExpr::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputSignExtend(const SymbolicExpr::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputText_Rose::BinaryAnalysis::SmtSolverprotected
outputUnary(const std::string &funcName, const SExprTypePair &arg) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputUnsignedCompare(const SymbolicExpr::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputUnsignedExtend(const SymbolicExpr::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputVariableDeclarations(std::ostream &, const VariableSet &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputWrite(const SymbolicExpr::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputXor(const SymbolicExpr::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
outputZerop(const SymbolicExpr::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
parse_evidence() ROSE_DEPRECATED("use parseEvidence") (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolverprotectedvirtual
parsedOutput_ (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolverprotected
parseEvidence() ROSE_OVERRIDERose::BinaryAnalysis::Z3Solvervirtual
parseSExpressions(const std::string &)Rose::BinaryAnalysis::SmtSolverprotected
pop() ROSE_OVERRIDERose::BinaryAnalysis::Z3Solvervirtual
printSExpression(std::ostream &, const SExpr::Ptr &)Rose::BinaryAnalysis::SmtSolverprotectedstatic
Ptr typedefRose::BinaryAnalysis::SmtSolver
push()Rose::BinaryAnalysis::SmtSolvervirtual
requireLinkage(LinkMode) const Rose::BinaryAnalysis::SmtSolver
reset() ROSE_OVERRIDERose::BinaryAnalysis::Z3Solvervirtual
reset_class_stats() ROSE_DEPRECATED("use resetClassStatistics") (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolver
reset_stats() ROSE_DEPRECATED("use resetStatistics") (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolver
resetClassStatistics()Rose::BinaryAnalysis::SmtSolverstatic
resetStatistics()Rose::BinaryAnalysis::SmtSolver
SAT_NO enum valueRose::BinaryAnalysis::SmtSolver
SAT_UNKNOWN enum valueRose::BinaryAnalysis::SmtSolver
SAT_YES enum valueRose::BinaryAnalysis::SmtSolver
Satisfiable enum nameRose::BinaryAnalysis::SmtSolver
satisfiable(const SymbolicExpr::Ptr &)Rose::BinaryAnalysis::SmtSolvervirtual
satisfiable(const std::vector< SymbolicExpr::Ptr > &)Rose::BinaryAnalysis::SmtSolvervirtual
selfTest() ROSE_OVERRIDERose::BinaryAnalysis::Z3Solvervirtual
SExprTypePair typedef (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolver
SharedObject()Sawyer::SharedObjectinline
SharedObject(const SharedObject &)Sawyer::SharedObjectinline
SmtlibSolver(const std::string &name, const boost::filesystem::path &executable, const std::string &shellArgs="", unsigned linkages=LM_EXECUTABLE) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverinlineexplicitprotected
SmtSolver(const std::string &name, unsigned linkages)Rose::BinaryAnalysis::SmtSolverinlineprotected
statistics() const Rose::BinaryAnalysis::SmtSolverinline
stats (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolverprotected
StringTypePair typedefRose::BinaryAnalysis::SmtSolver
TermNames typedef (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolver
termNames_ (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolverprotected
trivially_satisfiable(const std::vector< SymbolicExpr::Ptr > &exprs) ROSE_DEPRECATED("use triviallySatisfiable") (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolvervirtual
triviallySatisfiable(const std::vector< SymbolicExpr::Ptr > &exprs)Rose::BinaryAnalysis::SmtSolvervirtual
Type enum nameRose::BinaryAnalysis::SmtSolver
typeName(const SymbolicExpr::Ptr &) (defined in Rose::BinaryAnalysis::SmtlibSolver)Rose::BinaryAnalysis::SmtlibSolverprotectedvirtual
undoNormalization(const std::vector< SymbolicExpr::Ptr > &, const SymbolicExpr::ExprExprHashMap &index)Rose::BinaryAnalysis::SmtSolverprotectedstatic
varForSet(const SymbolicExpr::InteriorPtr &set, const SymbolicExpr::LeafPtr &var)Rose::BinaryAnalysis::SmtlibSolverprotected
varForSet(const SymbolicExpr::InteriorPtr &set)Rose::BinaryAnalysis::SmtlibSolverprotected
VariableSet typedefRose::BinaryAnalysis::SmtSolver
Z3Solver(unsigned linkages=LM_ANY) (defined in Rose::BinaryAnalysis::Z3Solver)Rose::BinaryAnalysis::Z3Solverinlineexplicitprotected
Z3Solver(const boost::filesystem::path &exe, const std::string &shellArgs="")Rose::BinaryAnalysis::Z3Solverinlineexplicit
z3Update()Rose::BinaryAnalysis::Z3Solvervirtual
~SharedObject()Sawyer::SharedObjectinlinevirtual
~SmtSolver() (defined in Rose::BinaryAnalysis::SmtSolver)Rose::BinaryAnalysis::SmtSolvervirtual