SatSolverFactory

The SAT solver factory of a Bitwuzla instance.

By default, Bitwuzla maintains an internal SAT solver factory to create SAT solver instances and no user intervention is required.

However, optionally, Bitwuzla also supports configuring an external, user-provided SAT solver factory via class bitwuzla::SatSolverFactory. If configured, this factory generates new bitwuzla::SatSolver instances.

An external SAT solver factory is configured via constructor bitwuzla::Bitwuzla bitwuzla::Bitwuzla::Bitwuzla(TermManager&, SatSolverFactory&, const Options&).

• class bitwuzla::SatSolverFactory

namespace bitwuzla {

class SatSolverFactory

The interface for an external (user-provided) SAT solver factory.

Warning

This interface is experimental and may change in future versions.

Public Functions

inline SatSolverFactory()

Constructor.

virtual std::unique_ptr<SatSolver> new_sat_solver() = 0

Create new (external) SAT solver instance.

Returns:

The SAT solver instance.

virtual bool has_terminator_support() = 0

Determine if configured SAT solver has terminator support.

}