m114p.h File Reference

#include "m114p_types.h"

Include dependency graph for m114p.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Macros
#define	M114p_SolverForEachRoot(s, ppLits, nLits, i)
#define	M114p_SolverForEachChain(s, ppClauses, ppVars, nVars, i)

Functions
ABC_NAMESPACE_HEADER_START M114p_Solver_t	M114p_SolverNew (int fRecordProof)
void	M114p_SolverDelete (M114p_Solver_t s)
void	M114p_SolverPrintStats (M114p_Solver_t s, double Time)
void	M114p_SolverSetVarNum (M114p_Solver_t s, int nVars)
int	M114p_SolverAddClause (M114p_Solver_t s, lit *begin, lit *end)
int	M114p_SolverSimplify (M114p_Solver_t s)
int	M114p_SolverSolve (M114p_Solver_t s, lit *begin, lit *end, int nConfLimit)
int	M114p_SolverGetConflictNum (M114p_Solver_t s)
int	M114p_SolverProofIsReady (M114p_Solver_t s)
void	M114p_SolverProofSave (M114p_Solver_t s, char *pFileName)
int	M114p_SolverProofClauseNum (M114p_Solver_t s)
int	M114p_SolverGetFirstRoot (M114p_Solver_t s, int **ppLits)
int	M114p_SolverGetNextRoot (M114p_Solver_t s, int **ppLits)
int	M114p_SolverGetFirstChain (M114p_Solver_t s, int **ppClauses, int **ppVars)
int	M114p_SolverGetNextChain (M114p_Solver_t s, int **ppClauses, int **ppVars)

Macro Definition Documentation

M114p_SolverForEachChain

#define M114p_SolverForEachChain	(		s,
			ppClauses,
			ppVars,
			nVars,
			i )

Value:

    for ( i = 0, nVars = M114p_SolverGetFirstChain(s, ppClauses, ppVars); nVars; \
          i++, nVars = M114p_SolverGetNextChain(s, ppClauses, ppVars) )

Definition at line 39 of file m114p.h.

#define M114p_SolverForEachChain( s, ppClauses, ppVars, nVars, i )               \
    for ( i = 0, nVars = M114p_SolverGetFirstChain(s, ppClauses, ppVars); nVars; \
          i++, nVars = M114p_SolverGetNextChain(s, ppClauses, ppVars) )

M114p_SolverForEachRoot

#define M114p_SolverForEachRoot	(		s,
			ppLits,
			nLits,
			i )

Value:

    for ( i = 0, nLits = M114p_SolverGetFirstRoot(s, ppLits); nLits;             \
          i++, nLits = M114p_SolverGetNextRoot(s, ppLits) )

Definition at line 34 of file m114p.h.

#define M114p_SolverForEachRoot( s, ppLits, nLits, i )                           \
    for ( i = 0, nLits = M114p_SolverGetFirstRoot(s, ppLits); nLits;             \
          i++, nLits = M114p_SolverGetNextRoot(s, ppLits) )

Function Documentation

M114p_SolverAddClause()

int M114p_SolverAddClause ( M114p_Solver_t s, lit * begin, lit * end )

extern

M114p_SolverDelete()

void M114p_SolverDelete ( M114p_Solver_t s )

extern

M114p_SolverGetConflictNum()

int M114p_SolverGetConflictNum ( M114p_Solver_t s )

extern

M114p_SolverGetFirstChain()

int M114p_SolverGetFirstChain ( M114p_Solver_t s, int ** ppClauses, int ** ppVars )

extern

M114p_SolverGetFirstRoot()

int M114p_SolverGetFirstRoot ( M114p_Solver_t s, int ** ppLits )

extern

M114p_SolverGetNextChain()

int M114p_SolverGetNextChain ( M114p_Solver_t s, int ** ppClauses, int ** ppVars )

extern

M114p_SolverGetNextRoot()

int M114p_SolverGetNextRoot ( M114p_Solver_t s, int ** ppLits )

extern

M114p_SolverNew()

ABC_NAMESPACE_HEADER_START M114p_Solver_t M114p_SolverNew ( int fRecordProof )

extern

M114p_SolverPrintStats()

void M114p_SolverPrintStats ( M114p_Solver_t s, double Time )

extern

M114p_SolverProofClauseNum()

int M114p_SolverProofClauseNum ( M114p_Solver_t s )

extern

M114p_SolverProofIsReady()

int M114p_SolverProofIsReady ( M114p_Solver_t s )

extern

M114p_SolverProofSave()

void M114p_SolverProofSave ( M114p_Solver_t s, char * pFileName )

extern

M114p_SolverSetVarNum()

void M114p_SolverSetVarNum ( M114p_Solver_t s, int nVars )

extern

M114p_SolverSimplify()

int M114p_SolverSimplify ( M114p_Solver_t s )

extern

M114p_SolverSolve()

int M114p_SolverSolve ( M114p_Solver_t s, lit * begin, lit * end, int nConfLimit )

extern