SATSolver.h File Reference

#include "llvm/ADT/ArrayRef.h"
#include "llvm/ADT/STLFunctionalExtras.h"
#include "llvm/ADT/SmallVector.h"
#include <memory>

Include dependency graph for SATSolver.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	circt::IndexedMaxHeap< T, ScoreFn >
	A max-heap of ids into caller-owned storage. More...
class	circt::IncrementalSATSolver
	Abstract interface for incremental SAT solvers with an IPASIR-style API. More...
struct	circt::CadicalSATSolverOptions

Namespaces
namespace	circt
	The InstanceGraph op interface, see InstanceGraphInterface.td for more details.

Functions
void	circt::addAndClauses (int outVar, llvm::ArrayRef< int > inputLits, llvm::function_ref< void(llvm::ArrayRef< int >)> addClause)
	Emit clauses encoding outVar <=> and(inputLits).
void	circt::addOrClauses (int outVar, llvm::ArrayRef< int > inputLits, llvm::function_ref< void(llvm::ArrayRef< int >)> addClause)
	Emit clauses encoding outVar <=> or(inputLits).
void	circt::addXorClauses (int outVar, int lhsLit, int rhsLit, llvm::function_ref< void(llvm::ArrayRef< int >)> addClause)
	Emit clauses encoding outVar <=> (lhsLit xor rhsLit).
void	circt::addParityClauses (int outVar, llvm::ArrayRef< int > inputLits, llvm::function_ref< void(llvm::ArrayRef< int >)> addClause, llvm::function_ref< int()> newVar)
	Emit clauses encoding outVar <=> parity(inputLits).
void	circt::addAtMostOneClauses (llvm::ArrayRef< int > inputLits, llvm::function_ref< void(llvm::ArrayRef< int >)> addClause, llvm::function_ref< int()> newVar)
	Emit clauses encoding that at most one literal in inputLits can be true.
void	circt::addExactlyOneClauses (llvm::ArrayRef< int > inputLits, llvm::function_ref< void(llvm::ArrayRef< int >)> addClause, llvm::function_ref< int()> newVar)
	Emit clauses encoding that exactly one literal in inputLits is true.
std::unique_ptr< IncrementalSATSolver >	circt::createZ3SATSolver ()
	Construct a Z3-backed incremental IPASIR-style SAT solver.
std::unique_ptr< IncrementalSATSolver >	circt::createCadicalSATSolver (const CadicalSATSolverOptions &options={})
	Construct a CaDiCaL-backed incremental IPASIR-style SAT solver.
bool	circt::hasIncrementalSATSolverBackend ()
	Return true when at least one incremental SAT backend is available.