SATProblem Class Reference

#include <passes/tags/sat.h>

Public Member Functions
void	Add (llvm::ArrayRef< ID< Lit >> pos, llvm::ArrayRef< ID< Lit >> neg)
bool	IsSatisfiable ()
bool	IsSatisfiableWith (ID< Lit > id)
void	dump (llvm::raw_ostream &os=llvm::errs())

Detailed Description

n-SAT solver based on DPLL.

Member Function Documentation

dump()

void SATProblem::dump

(

llvm::raw_ostream &

os = llvm::errs()

)

Print the constraint system.

IsSatisfiable()

bool SATProblem::IsSatisfiable

(

)

Return true if the system is satisfiable.

IsSatisfiableWith()

bool SATProblem::IsSatisfiableWith

(

ID< Lit >

id

)

Returns true if the system is satisfiable assuming an additional true lit.

---

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

• passes/tags/sat.h
• passes/tags/sat.cpp