| assertions() const | Rose::BinaryAnalysis::SmtSolver | virtual |
| assertions(size_t level) const | Rose::BinaryAnalysis::SmtSolver | virtual |
| Availability typedef | Rose::BinaryAnalysis::SmtSolver | |
| availability() | Rose::BinaryAnalysis::SmtSolver | static |
| availableLinkages() | Rose::BinaryAnalysis::Z3Solver | static |
| bestAvailable() | Rose::BinaryAnalysis::SmtSolver | static |
| bestLinkage(unsigned linkages) | Rose::BinaryAnalysis::SmtSolver | static |
| 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::SmtSolver | virtual |
| checkExe() | Rose::BinaryAnalysis::SmtSolver | protectedvirtual |
| checkLib() override | Rose::BinaryAnalysis::Z3Solver | virtual |
| checkTrivial() | Rose::BinaryAnalysis::SmtSolver | virtual |
| classStatistics() | Rose::BinaryAnalysis::SmtSolver | static |
| classStats (defined in Rose::BinaryAnalysis::SmtSolver) | Rose::BinaryAnalysis::SmtSolver | protectedstatic |
| classStatsMutex (defined in Rose::BinaryAnalysis::SmtSolver) | Rose::BinaryAnalysis::SmtSolver | protectedstatic |
| clearEvidence() override | Rose::BinaryAnalysis::Z3Solver | virtual |
| create() const override | Rose::BinaryAnalysis::Z3Solver | virtual |
| Definitions typedef | Rose::BinaryAnalysis::SmtSolver | |
| errorIfReset() const | Rose::BinaryAnalysis::SmtSolver | inline |
| errorIfReset(bool b) | Rose::BinaryAnalysis::SmtSolver | inline |
| Evidence typedef | Rose::BinaryAnalysis::SmtSolver | |
| evidence() const | Rose::BinaryAnalysis::SmtSolver | |
| evidence_ (defined in Rose::BinaryAnalysis::SmtSolver) | Rose::BinaryAnalysis::SmtSolver | protected |
| evidenceByName() const | Rose::BinaryAnalysis::SmtSolver | |
| evidenceForAddress(uint64_t addr) | Rose::BinaryAnalysis::SmtSolver | virtual |
| evidenceForName(const std::string &) const | Rose::BinaryAnalysis::SmtSolver | virtual |
| evidenceForVariable(const SymbolicExpression::Ptr &var) | Rose::BinaryAnalysis::SmtSolver | inlinevirtual |
| evidenceForVariable(uint64_t varno) | Rose::BinaryAnalysis::SmtSolver | inlinevirtual |
| evidenceNames() const | Rose::BinaryAnalysis::SmtSolver | virtual |
| ExprExprMap typedef | Rose::BinaryAnalysis::SmtSolver | |
| ExprList typedef | Rose::BinaryAnalysis::SmtSolver | |
| findVariables(const SymbolicExpression::Ptr &, VariableSet &) override | Rose::BinaryAnalysis::SmtlibSolver | virtual |
| generateFile(std::ostream &, const std::vector< SymbolicExpression::Ptr > &exprs, Definitions *) override (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | virtual |
| Rose::BinaryAnalysis::SmtSolver::generateFile(std::ostream &, const ExprList &exprs, Definitions *)=0 | Rose::BinaryAnalysis::SmtSolver | pure virtual |
| getCommand(const std::string &configName) override | Rose::BinaryAnalysis::SmtlibSolver | virtual |
| getErrorMessage(int exitStatus) override | Rose::BinaryAnalysis::SmtlibSolver | virtual |
| initDiagnostics() | Rose::BinaryAnalysis::SmtSolver | static |
| insert(const SymbolicExpression::Ptr &) | Rose::BinaryAnalysis::SmtSolver | virtual |
| insert(const ExprList &) | Rose::BinaryAnalysis::SmtSolver | virtual |
| instance(unsigned linkages=LM_ANY) | Rose::BinaryAnalysis::Z3Solver | inlinestatic |
| Rose::BinaryAnalysis::SmtlibSolver::instance(const std::string &name, const boost::filesystem::path &executable, const std::string &shellArgs="", unsigned linkages=LM_EXECUTABLE) | Rose::BinaryAnalysis::SmtlibSolver | inlinestatic |
| Rose::BinaryAnalysis::SmtSolver::instance(const std::string &name) | Rose::BinaryAnalysis::SmtSolver | static |
| linkage() const | Rose::BinaryAnalysis::SmtSolver | inline |
| linkage_ (defined in Rose::BinaryAnalysis::SmtSolver) | Rose::BinaryAnalysis::SmtSolver | protected |
| LinkMode enum name | Rose::BinaryAnalysis::SmtSolver | |
| LM_ANY enum value | Rose::BinaryAnalysis::SmtSolver | |
| LM_EXECUTABLE enum value | Rose::BinaryAnalysis::SmtSolver | |
| LM_LIBRARY enum value | Rose::BinaryAnalysis::SmtSolver | |
| LM_NONE enum value | Rose::BinaryAnalysis::SmtSolver | |
| MEM_STATE enum value (defined in Rose::BinaryAnalysis::SmtSolver) | Rose::BinaryAnalysis::SmtSolver | |
| memoizer() const | Rose::BinaryAnalysis::SmtSolver | |
| memoizer(const Memoizer::Ptr &) | Rose::BinaryAnalysis::SmtSolver | |
| memoizer_ (defined in Rose::BinaryAnalysis::SmtSolver) | Rose::BinaryAnalysis::SmtSolver | protected |
| mlog | Rose::BinaryAnalysis::SmtSolver | static |
| mostType(const std::vector< SExprTypePair > &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| name() const | Rose::BinaryAnalysis::SmtSolver | inline |
| name(const std::string &s) | Rose::BinaryAnalysis::SmtSolver | inline |
| nAssertions(size_t backtrackingLevel) | Rose::BinaryAnalysis::SmtSolver | virtual |
| nAssertions() const | Rose::BinaryAnalysis::SmtSolver | virtual |
| nLevels() const | Rose::BinaryAnalysis::SmtSolver | inlinevirtual |
| NO_TYPE enum value (defined in Rose::BinaryAnalysis::SmtSolver) | Rose::BinaryAnalysis::SmtSolver | |
| normalizeVariables(const ExprList &, SymbolicExpression::ExprExprHashMap &index) | Rose::BinaryAnalysis::SmtSolver | protectedstatic |
| outputArithmeticShiftRight(const SymbolicExpression::InteriorPtr &) override (defined in Rose::BinaryAnalysis::Z3Solver) | Rose::BinaryAnalysis::Z3Solver | protectedvirtual |
| outputAssertion(std::ostream &, const SymbolicExpression::Ptr &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputBinary(const std::string &func, const SymbolicExpression::InteriorPtr &, Type rettype=NO_TYPE) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputBvxorFunctions(std::ostream &, const std::vector< SymbolicExpression::Ptr > &) override | Rose::BinaryAnalysis::Z3Solver | protectedvirtual |
| outputCast(const SExprTypePair &, Type to) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputCast(const std::vector< SExprTypePair > &, Type to) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputComments(std::ostream &, const std::vector< SymbolicExpression::Ptr > &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputCommonSubexpressions(std::ostream &, const std::vector< SymbolicExpression::Ptr > &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputComparisonFunctions(std::ostream &, const std::vector< SymbolicExpression::Ptr > &) override | Rose::BinaryAnalysis::Z3Solver | protectedvirtual |
| outputDivide(const SymbolicExpression::InteriorPtr &, const std::string &operation) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputExpression(const SymbolicExpression::Ptr &) override (defined in Rose::BinaryAnalysis::Z3Solver) | Rose::BinaryAnalysis::Z3Solver | protectedvirtual |
| outputExpressions(const std::vector< SymbolicExpression::Ptr > &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputExtract(const SymbolicExpression::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputIte(const SymbolicExpression::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputLeaf(const SymbolicExpression::LeafPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputLeftAssoc(const std::string &func, const SymbolicExpression::InteriorPtr &, Type rettype=NO_TYPE) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputLeftAssoc(const std::string &func, const std::vector< SExprTypePair > &, Type rettype=NO_TYPE) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputList(const std::string &name, const SymbolicExpression::InteriorPtr &, Type rettype=NO_TYPE) (defined in Rose::BinaryAnalysis::Z3Solver) | Rose::BinaryAnalysis::Z3Solver | protected |
| outputList(const std::string &name, const std::vector< SExprTypePair > &, Type rettype=NO_TYPE) (defined in Rose::BinaryAnalysis::Z3Solver) | Rose::BinaryAnalysis::Z3Solver | protected |
| outputLogicalShiftRight0(const SymbolicExpression::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputLogicalShiftRight1(const SymbolicExpression::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputModulo(const SymbolicExpression::InteriorPtr &, const std::string &operation) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputMultiply(const SymbolicExpression::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputNotEqual(const SymbolicExpression::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputRead(const SymbolicExpression::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputRotateLeft(const SymbolicExpression::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputRotateRight(const SymbolicExpression::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputSet(const SymbolicExpression::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputShiftLeft0(const SymbolicExpression::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputShiftLeft1(const SymbolicExpression::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputSignedCompare(const SymbolicExpression::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputSignExtend(const SymbolicExpression::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputText_ | Rose::BinaryAnalysis::SmtSolver | protected |
| outputUnary(const std::string &funcName, const SExprTypePair &arg) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputUnsignedCompare(const SymbolicExpression::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputUnsignedExtend(const SymbolicExpression::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputVariableDeclarations(std::ostream &, const VariableSet &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputWrite(const SymbolicExpression::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputXor(const SymbolicExpression::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| outputZerop(const SymbolicExpression::InteriorPtr &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| parsedOutput_ (defined in Rose::BinaryAnalysis::SmtSolver) | Rose::BinaryAnalysis::SmtSolver | protected |
| parseEvidence() override | Rose::BinaryAnalysis::Z3Solver | virtual |
| parseSExpressions(const std::string &) | Rose::BinaryAnalysis::SmtSolver | protected |
| pop() override | Rose::BinaryAnalysis::Z3Solver | virtual |
| printSExpression(std::ostream &, const SExpr::Ptr &) | Rose::BinaryAnalysis::SmtSolver | protectedstatic |
| progress() const | Rose::BinaryAnalysis::SmtSolver | |
| progress(const Progress::Ptr &progress) | Rose::BinaryAnalysis::SmtSolver | |
| progress_ (defined in Rose::BinaryAnalysis::SmtSolver) | Rose::BinaryAnalysis::SmtSolver | protected |
| Ptr typedef | Rose::BinaryAnalysis::SmtSolver | |
| push() | Rose::BinaryAnalysis::SmtSolver | virtual |
| requireLinkage(LinkMode) const | Rose::BinaryAnalysis::SmtSolver | |
| reset() override | Rose::BinaryAnalysis::Z3Solver | virtual |
| resetClassStatistics() | Rose::BinaryAnalysis::SmtSolver | static |
| resetStatistics() | Rose::BinaryAnalysis::SmtSolver | |
| SAT_NO enum value | Rose::BinaryAnalysis::SmtSolver | |
| SAT_UNKNOWN enum value | Rose::BinaryAnalysis::SmtSolver | |
| SAT_YES enum value | Rose::BinaryAnalysis::SmtSolver | |
| Satisfiable enum name | Rose::BinaryAnalysis::SmtSolver | |
| satisfiable(const SymbolicExpression::Ptr &) | Rose::BinaryAnalysis::SmtSolver | virtual |
| satisfiable(const ExprList &) | Rose::BinaryAnalysis::SmtSolver | virtual |
| selfTest() override | Rose::BinaryAnalysis::Z3Solver | virtual |
| SExprTypePair typedef (defined in Rose::BinaryAnalysis::SmtSolver) | Rose::BinaryAnalysis::SmtSolver | |
| 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::SmtlibSolver | inlineexplicitprotected |
| SmtSolver(const std::string &name, unsigned linkages) | Rose::BinaryAnalysis::SmtSolver | inlineprotected |
| statistics() const | Rose::BinaryAnalysis::SmtSolver | inline |
| stats (defined in Rose::BinaryAnalysis::SmtSolver) | Rose::BinaryAnalysis::SmtSolver | protected |
| StringTypePair typedef | Rose::BinaryAnalysis::SmtSolver | |
| TermNames typedef (defined in Rose::BinaryAnalysis::SmtSolver) | Rose::BinaryAnalysis::SmtSolver | |
| termNames_ (defined in Rose::BinaryAnalysis::SmtSolver) | Rose::BinaryAnalysis::SmtSolver | protected |
| timeout(boost::chrono::duration< double >) override | Rose::BinaryAnalysis::Z3Solver | virtual |
| timeout_ (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protected |
| triviallySatisfiable(const ExprList &exprs) | Rose::BinaryAnalysis::SmtSolver | virtual |
| Type enum name | Rose::BinaryAnalysis::SmtSolver | |
| typeName(const SymbolicExpression::Ptr &) (defined in Rose::BinaryAnalysis::SmtlibSolver) | Rose::BinaryAnalysis::SmtlibSolver | protectedvirtual |
| undoNormalization(const ExprList &, const SymbolicExpression::ExprExprHashMap &index) | Rose::BinaryAnalysis::SmtSolver | protectedstatic |
| varForSet(const SymbolicExpression::InteriorPtr &set, const SymbolicExpression::LeafPtr &var) | Rose::BinaryAnalysis::SmtlibSolver | protected |
| varForSet(const SymbolicExpression::InteriorPtr &set) | Rose::BinaryAnalysis::SmtlibSolver | protected |
| VariableSet typedef | Rose::BinaryAnalysis::SmtSolver | |
| Z3Solver(unsigned linkages=LM_ANY) (defined in Rose::BinaryAnalysis::Z3Solver) | Rose::BinaryAnalysis::Z3Solver | inlineexplicitprotected |
| Z3Solver(const boost::filesystem::path &exe, const std::string &shellArgs="") | Rose::BinaryAnalysis::Z3Solver | inlineexplicit |
| z3Update() | Rose::BinaryAnalysis::Z3Solver | virtual |
| ~SmtSolver() (defined in Rose::BinaryAnalysis::SmtSolver) | Rose::BinaryAnalysis::SmtSolver | virtual |
| ~Z3Solver() (defined in Rose::BinaryAnalysis::Z3Solver) | Rose::BinaryAnalysis::Z3Solver | inline |
