#include "llvm/ADT/ArrayRef.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 | |
| 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. | |
