SatSolver

The SAT solver instance of a Bitwuzla instance.

By default, Bitwuzla creates bitwuzla::SatSolver instances internally and no user intervention is required.

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

• class bitwuzla::SatSolver

namespace bitwuzla {

class SatSolver

The SAT solver interface.

Warning

This interface is experimental and may change in future versions.

Public Functions

inline SatSolver()

Constructor.

inline virtual ~SatSolver()

Destructor.

virtual void add(int32_t lit, int64_t cgroup_id = 0) = 0

Add valid literal to current clause.

Parameters:

• lit – The literal to add, 0 to terminate clause..

• cgroup_id – The “clause group” id, associates a clause with a clause group. This is only relevant for interpolation where this labeling allows for mapping back clauses to the corresponding nodes in the bit-level circuit. It can be left at its default value, otherwise.

virtual void assume(int32_t lit) = 0

Assume valid (non-zero) literal for next call to ‘check_sat’.

Parameters:

lit – The literal to assume.

virtual int32_t value(int32_t lit) = 0

Get value of valid non-zero literal.

Parameters:

lit – The literal to query.

Returns:

The value of the literal (-1 = false, 1 = true, 0 = unknown).

virtual bool failed(int32_t lit) = 0

Determine if the valid non-zero literal is in the unsat core.

Parameters:

lit – The literal to query.

Returns:

True if the literal is in the core, and false otherwise.

virtual int32_t fixed(int32_t lit) = 0

Determine if the given literal is implied by the formula.

Returns:

1 if it is implied, -1 if it is not implied and 0 if unknown.

virtual Result solve() = 0

Check satisfiability of current formula.

Returns:

The result of the satisfiability check.

virtual void configure_terminator(Terminator *terminator) = 0

Configure a termination callback function via a terminator.

Parameters:

terminator – The terminator.

virtual const char *get_name() const = 0

Get the name of this SAT solver.

Returns:

The name of this SAT solver.

virtual const char *get_version() const = 0

Get the version of this SAT solver.

Returns:

The version of the underly ing SAT solver.

}