SATSolver.cpp File Reference

#include "circt/Support/SATSolver.h"
#include "llvm/ADT/ArrayRef.h"
#include "llvm/ADT/SmallVector.h"
#include "llvm/Support/ErrorHandling.h"
#include "llvm/Support/SMTAPI.h"
#include <cassert>
#include <cstdlib>
#include <string>

Include dependency graph for SATSolver.cpp:

Go to the source code of this file.

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.