Interface with a SAT solver. More...

#include <spot/misc/satsolver.hh>

Collaboration diagram for spot::satsolver:

Public Types
typedef std::vector< bool >	solution

typedef std::pair< int, solution >	solution_pair

Public Member Functions
	satsolver ()
	Construct the sat solver and initialize variables. If no satsolver is provided through SPOT_SATSOLVER env var, a distributed version of PicoSAT will be used. More...

void	adjust_nvars (int nvars)
	Adjust the number of variables used in the cnf formula. More...

void	set_nassumptions_vars (int nassumptions_vars)
	Declare the number of vars reserved for assumptions. More...

void	add (std::initializer_list< int > values)
	Add a list of lit. to the current clause. More...

void	add (int v)
	Add a single lit. to the current clause. More...

int	get_nb_clauses () const
	Get the current number of clauses. More...

int	get_nb_vars () const
	Get the current number of variables. More...

std::pair< int, int >	stats () const
	Returns std::pair<nvars, nclauses>;. More...

template<typename T >
void	comment_rec (T single)
	Add a comment. It should be used only in debug mode after providing a satsolver. More...

template<typename T , typename... Args>
void	comment_rec (T first, Args... args)
	Add comments. It should be used only in debug mode after providing a satsolver. More...

template<typename T >
void	comment (T single)
	Add a comment. It will start with "c ". It should be used only in debug mode after providing a satsolver. More...

template<typename T , typename... Args>
void	comment (T first, Args... args)
	Add comments. It will start with "c ". It should be used only in debug mode after providing a satsolver. More...

void	assume (int lit)
	Assume a literal value. Must only be used with distributed picolib. More...

solution_pair	get_solution ()
	Return std::vector<solving_return_code, solution>. More...

Detailed Description

Interface with a SAT solver.

This class provides the necessary functions to add clauses, comments. Depending on SPOT_SATSOLVER, it will use either picosat solver (default) or the given satsolver.

Now that spot is distributed with a satsolver (PicoSAT), it is used by default. But another satsolver can be configured via the SPOT_SATSOLVER environment variable. It must be set following this: "satsolver [options] %I > %O" where I and O are replaced by input and output files.

Constructor & Destructor Documentation

◆ satsolver()

spot::satsolver::satsolver ( )

Construct the sat solver and initialize variables. If no satsolver is provided through SPOT_SATSOLVER env var, a distributed version of PicoSAT will be used.

Member Function Documentation

◆ add() [1/2]

void spot::satsolver::add ( int v )

Add a single lit. to the current clause.

◆ add() [2/2]

void spot::satsolver::add ( std::initializer_list< int > values )

Add a list of lit. to the current clause.

◆ adjust_nvars()

void spot::satsolver::adjust_nvars ( int nvars )

Adjust the number of variables used in the cnf formula.

◆ assume()

void spot::satsolver::assume ( int lit )

Assume a literal value. Must only be used with distributed picolib.

◆ comment() [1/2]

template<typename T , typename... Args>

void spot::satsolver::comment	(	T	first,
		Args...	args
	)

Add comments. It will start with "c ". It should be used only in debug mode after providing a satsolver.

References comment_rec().

◆ comment() [2/2]

template<typename T >

void spot::satsolver::comment ( T single )

Add a comment. It will start with "c ". It should be used only in debug mode after providing a satsolver.

◆ comment_rec() [1/2]

template<typename T , typename... Args>

void spot::satsolver::comment_rec	(	T	first,
		Args...	args
	)

Add comments. It should be used only in debug mode after providing a satsolver.

References comment_rec().

◆ comment_rec() [2/2]

template<typename T >

void spot::satsolver::comment_rec ( T single )

Add a comment. It should be used only in debug mode after providing a satsolver.

Referenced by comment(), and comment_rec().

◆ get_nb_clauses()

int spot::satsolver::get_nb_clauses ( ) const

Get the current number of clauses.

◆ get_nb_vars()

int spot::satsolver::get_nb_vars ( ) const

Get the current number of variables.

◆ get_solution()

solution_pair spot::satsolver::get_solution ( )

Return std::vector<solving_return_code, solution>.

◆ set_nassumptions_vars()

void spot::satsolver::set_nassumptions_vars ( int nassumptions_vars )

Declare the number of vars reserved for assumptions.

◆ stats()

std::pair< int, int > spot::satsolver::stats ( ) const

Returns std::pair<nvars, nclauses>;.

The documentation for this class was generated from the following file:

spot/misc/satsolver.hh

Public Types

Public Member Functions