clang::dataflow::WatchedLiteralsSolverImpl Class Reference

Public Member Functions
	WatchedLiteralsSolverImpl (const llvm::ArrayRef< const Formula * > &Vals)
std::pair< Solver::Result, std::int64_t >	solve (std::int64_t MaxIterations) &&

Detailed Description

Definition at line 447 of file WatchedLiteralsSolver.cpp.

Constructor & Destructor Documentation

WatchedLiteralsSolverImpl()

clang::dataflow::WatchedLiteralsSolverImpl::WatchedLiteralsSolverImpl ( const llvm::ArrayRef< const Formula * > &  Vals )

inlineexplicit

Definition at line 502 of file WatchedLiteralsSolver.cpp.

References clang::dataflow::CNFFormula::LargestVar, clang::dataflow::negLit(), clang::dataflow::NullVar, and clang::dataflow::posLit().

Member Function Documentation

solve()

std::pair< Solver::Result, std::int64_t > clang::dataflow::WatchedLiteralsSolverImpl::solve ( std::int64_t  MaxIterations ) &&

inline

Definition at line 525 of file WatchedLiteralsSolver.cpp.

References clang::dataflow::CNFFormula::KnownContradictory, clang::dataflow::negLit(), clang::dataflow::posLit(), clang::dataflow::Solver::Result::Satisfiable, clang::dataflow::Solver::Result::TimedOut(), and clang::dataflow::Solver::Result::Unsatisfiable().

Referenced by clang::dataflow::WatchedLiteralsSolver::solve().

---

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

• lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp