struct Solver::Result

Declaration

struct Solver::Result { /* full declaration omitted */ };

Declared at: clang/include/clang/Analysis/FlowSensitive/Solver.h:28

Member Variables

private clang::dataflow::Solver::Result::Status SATCheckStatus

private llvm::Optional< llvm::DenseMap<AtomicBoolValue*, Assignment>> Solution

Method Overview

• private Result(enum Status SATCheckStatus, llvm::Optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution)
• public static clang::dataflow::Solver::Result Satisfiable(llvm::DenseMap<AtomicBoolValue *, Assignment> Solution)
• public static clang::dataflow::Solver::Result TimedOut()
• public static clang::dataflow::Solver::Result Unsatisfiable()
• public llvm::Optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> getSolution() const
• public clang::dataflow::Solver::Result::Status getStatus() const

Methods

¶Result(enum Status SATCheckStatus,
       llvm::Optional<
           llvm::DenseMap<AtomicBoolValue*,
                          Assignment>> Solution)

Declared at: clang/include/clang/Analysis/FlowSensitive/Solver.h:73

Parameters

enum Status SATCheckStatus

llvm::Optional< llvm::DenseMap<AtomicBoolValue*, Assignment>> Solution

¶static clang::dataflow::Solver::Result
Satisfiable(llvm::DenseMap<AtomicBoolValue*,
                           Assignment> Solution)

Description

Constructs a result indicating that the queried boolean formula is satisfiable. The result will hold a solution found by the solver.

Declared at: clang/include/clang/Analysis/FlowSensitive/Solver.h:49

Parameters

llvm::DenseMap<AtomicBoolValue*, Assignment> Solution

¶static clang::dataflow::Solver::Result TimedOut()

Description

Constructs a result indicating that satisfiability checking on the queried boolean formula was not completed.

Declared at: clang/include/clang/Analysis/FlowSensitive/Solver.h:59

¶static clang::dataflow::Solver::Result
Unsatisfiable()

Description

Constructs a result indicating that the queried boolean formula is unsatisfiable.

Declared at: clang/include/clang/Analysis/FlowSensitive/Solver.h:55

¶llvm::Optional<
    llvm::DenseMap<AtomicBoolValue*, Assignment>>
getSolution() const

Description

Returns a truth assignment to boolean values that satisfies the queried boolean formula if available. Otherwise, an empty optional is returned.

Declared at: clang/include/clang/Analysis/FlowSensitive/Solver.h:68

¶clang::dataflow::Solver::Result::Status
getStatus() const

Description

Returns the status of satisfiability checking on the queried boolean formula.

Declared at: clang/include/clang/Analysis/FlowSensitive/Solver.h:63