NuSMV/code/nusmv/core/sat/sat.h File Reference

#include "nusmv/core/utils/utils.h"
#include "nusmv/core/be/be.h"
#include "nusmv/core/node/node.h"
#include "nusmv/core/sat/SatSolver.h"
#include "nusmv/core/sat/SatIncSolver.h"

Go to the source code of this file.

Defines
#define	NUSMV_HAVE_INCREMENTAL_SAT   0
	The public interface for the sat package.
Functions
SatIncSolver_ptr	Sat_CreateIncProofSolver (const NuSMVEnv_ptr env, const char *satSolver)
	Creates an incremental proof logging SAT solver instance of a given name.
SatIncSolver_ptr	Sat_CreateIncSolver (const NuSMVEnv_ptr env, const char *satSolver)
	Creates an incremental SAT solver instance of a given name.
SatSolver_ptr	Sat_CreateNonIncProofSolver (const NuSMVEnv_ptr env, const char *satSolver)
	Creates a SAT solver (non-incremental) of a given name. Proof-logging may be enabled if needed.
SatSolver_ptr	Sat_CreateNonIncSolver (const NuSMVEnv_ptr env, const char *satSolver)
	Creates a SAT solver (non-incremental) of a given name.
char *	Sat_GetAvailableSolversString (void)
	Retrieves a string with the sat solvers names the system currently supplies.
const char *	Sat_NormalizeSatSolverName (const char *solverName)
	Given a string representing the name of a sat solver, returns a normalized solver name -- just potential changes in character cases.
void	Sat_PrintAvailableSolvers (FILE *file)
	Prints out the sat solvers names the system currently supplies.

---

Define Documentation

#define NUSMV_HAVE_INCREMENTAL_SAT   0

The public interface for the sat package.

Author:

Andrei Tchaltsev, Roberto Cavada This package contains the generic interface to access to sat solvers. A set of specific Sat solvers implementation are internally kept, and are not accessible

A flag indicating that there is at least one incremental SAT solver

---

Function Documentation

SatIncSolver_ptr Sat_CreateIncProofSolver	(	const NuSMVEnv_ptr	env,
		const char *	satSolver
	)

Creates an incremental proof logging SAT solver instance of a given name.

The name of a solver is case-insensitive. Returns NULL if requested sat solver is not available.

SatIncSolver_ptr Sat_CreateIncSolver	(	const NuSMVEnv_ptr	env,
		const char *	satSolver
	)

Creates an incremental SAT solver instance of a given name.

The name of a solver is case-insensitive. Returns NULL if requested sat solver is not available.

SatSolver_ptr Sat_CreateNonIncProofSolver	(	const NuSMVEnv_ptr	env,
		const char *	satSolver
	)

Creates a SAT solver (non-incremental) of a given name. Proof-logging may be enabled if needed.

The name of a solver is case-insensitive. Returns NULL if requested sat solver is not available. Proof logging is currently available only with MiniSat.

SatSolver_ptr Sat_CreateNonIncSolver	(	const NuSMVEnv_ptr	env,
		const char *	satSolver
	)

Creates a SAT solver (non-incremental) of a given name.

The name of a solver is case-insensitive. Returns NULL if requested sat solver is not available.

char* Sat_GetAvailableSolversString

(

void

)

Retrieves a string with the sat solvers names the system currently supplies.

Returned string must be freed

See also:

Sat_PrintAvailableSolvers

const char* Sat_NormalizeSatSolverName

(

const char *

solverName

)

Given a string representing the name of a sat solver, returns a normalized solver name -- just potential changes in character cases.

In case of an error, if an input string does not represented any solver, returns (const char*) NULL. Returned string must not be freed.

void Sat_PrintAvailableSolvers

(

FILE *

file

)

Prints out the sat solvers names the system currently supplies.

See also:

Sat_GetAvailableSolversString