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

#include "nusmv/core/be/be.h"
#include "nusmv/core/utils/object.h"
#include "nusmv/core/utils/utils.h"

Go to the source code of this file.

Data Structures
struct	TermFactoryCallbacks
Defines
#define	SAT_SOLVER(x)   ((SatSolver_ptr) x)
#define	SAT_SOLVER_CHECK_INSTANCE(x)   (nusmv_assert(SAT_SOLVER(x) != SAT_SOLVER(NULL)))
#define	Term   void *
	The header file for the SatSolver class.
#define	TermFactoryCallbacksUserData_ptr   void *
Typedefs
typedef struct SatSolver_TAG *	SatSolver_ptr
typedef nusmv_ptrint	SatSolverGroup
typedef nusmv_ptrint	SatSolverItpGroup
typedef TermFactoryCallbacks *	TermFactoryCallbacks_ptr
Enumerations
enum	SatSolverResult {   SAT_SOLVER_INTERNAL_ERROR = -1, SAT_SOLVER_TIMEOUT, SAT_SOLVER_MEMOUT, SAT_SOLVER_SATISFIABLE_PROBLEM,   SAT_SOLVER_UNSATISFIABLE_PROBLEM, SAT_SOLVER_UNAVAILABLE }

---

Define Documentation

#define SAT_SOLVER

(

x

)

((SatSolver_ptr) x)

Todo:

Missing synopsis

Todo:

Missing description

#define SAT_SOLVER_CHECK_INSTANCE

(

x

)

(nusmv_assert(SAT_SOLVER(x) != SAT_SOLVER(NULL)))

Todo:

Missing synopsis

Todo:

Missing description

#define Term   void *

The header file for the SatSolver class.

Author:

Andrei Tchaltsev A non-incremental SAT solver interface

Todo:

Missing synopsis

Todo:

Missing description

#define TermFactoryCallbacksUserData_ptr   void *

Todo:

Missing synopsis

Todo:

Missing description

---

Typedef Documentation

typedef struct SatSolver_TAG* SatSolver_ptr

typedef nusmv_ptrint SatSolverGroup

Todo:

Missing synopsis

Todo:

Missing description

typedef nusmv_ptrint SatSolverItpGroup

typedef TermFactoryCallbacks* TermFactoryCallbacks_ptr

Todo:

Missing synopsis

Todo:

Missing description

---

Enumeration Type Documentation

enum SatSolverResult

Enumerator:

SAT_SOLVER_INTERNAL_ERROR
SAT_SOLVER_TIMEOUT
SAT_SOLVER_MEMOUT
SAT_SOLVER_SATISFIABLE_PROBLEM
SAT_SOLVER_UNSATISFIABLE_PROBLEM
SAT_SOLVER_UNAVAILABLE