Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct solver_t	solver

typedef int	solver_Var

typedef int	solver_Lit

typedef int	solver_lbool

Functions
solver *	solver_new (void)

void	solver_delete (solver *s)

solver_Var	solver_newVar (solver *s)

solver_Lit	solver_newLit (solver *s)

solver_Lit	solver_mkLit (solver_Var x)

solver_Lit	solver_mkLit_args (solver_Var x, int sign)

solver_Lit	solver_negate (solver_Lit p)

solver_Var	solver_var (solver_Lit p)

int	solver_sign (solver_Lit p)

int	solver_addClause (solver s, int len, solver_Lit ps)

void	solver_addClause_begin (solver *s)

void	solver_addClause_addLit (solver *s, solver_Lit p)

int	solver_addClause_commit (solver *s)

int	solver_simplify (solver *s)

int	solver_solve (solver s, int len, solver_Lit ps)

void	solver_solve_begin (solver *s)

void	solver_solve_addLit (solver *s, solver_Lit p)

int	solver_solve_commit (solver *s)

int	solver_okay (solver *s)

void	solver_setPolarity (solver *s, solver_Var v, int b)

void	solver_setDecisionVar (solver *s, solver_Var v, int b)

solver_lbool	solver_get_l_True (void)

solver_lbool	solver_get_l_False (void)

solver_lbool	solver_get_l_Undef (void)

solver_lbool	solver_value_Var (solver *s, solver_Var x)

solver_lbool	solver_value_Lit (solver *s, solver_Lit p)

solver_lbool	solver_modelValue_Var (solver *s, solver_Var x)

solver_lbool	solver_modelValue_Lit (solver *s, solver_Lit p)

int	solver_num_assigns (solver *s)

int	solver_num_clauses (solver *s)

int	solver_num_learnts (solver *s)

int	solver_num_vars (solver *s)

int	solver_num_freeVars (solver *s)

int	solver_conflict_len (solver *s)

solver_Lit	solver_conflict_nthLit (solver *s, int i)

void	solver_set_verbosity (solver *s, int v)

int	solver_num_conflicts (solver *s)

Variables
const solver_lbool	solver_l_True

const solver_lbool	solver_l_False

const solver_lbool	solver_l_Undef

Typedef Documentation

typedef typedefABC_NAMESPACE_HEADER_START struct solver_t solver

Definition at line 30 of file solver.h.

typedef int solver_lbool

Definition at line 33 of file solver.h.

typedef int solver_Lit

Definition at line 32 of file solver.h.

typedef int solver_Var

Definition at line 31 of file solver.h.

Function Documentation

int solver_addClause	(	solver *	s,
		int	len,
		solver_Lit *	ps
	)

void solver_addClause_addLit	(	solver *	s,
		solver_Lit	p
	)

void solver_addClause_begin ( solver * s )

int solver_addClause_commit ( solver * s )

int solver_conflict_len ( solver * s )

solver_Lit solver_conflict_nthLit	(	solver *	s,
		int	i
	)

void solver_delete ( solver * s )

solver_lbool solver_get_l_False ( void )

solver_lbool solver_get_l_True ( void )

solver_lbool solver_get_l_Undef ( void )

solver_Lit solver_mkLit ( solver_Var x )

solver_Lit solver_mkLit_args	(	solver_Var	x,
		int	sign
	)

solver_lbool solver_modelValue_Lit	(	solver *	s,
		solver_Lit	p
	)

solver_lbool solver_modelValue_Var	(	solver *	s,
		solver_Var	x
	)

solver_Lit solver_negate ( solver_Lit p )

solver* solver_new ( void )

solver_Lit solver_newLit ( solver * s )

solver_Var solver_newVar ( solver * s )

int solver_num_assigns ( solver * s )

int solver_num_clauses ( solver * s )

int solver_num_conflicts ( solver * s )

int solver_num_freeVars ( solver * s )

int solver_num_learnts ( solver * s )

int solver_num_vars ( solver * s )

int solver_okay ( solver * s )

void solver_set_verbosity	(	solver *	s,
		int	v
	)

void solver_setDecisionVar	(	solver *	s,
		solver_Var	v,
		int	b
	)

void solver_setPolarity	(	solver *	s,
		solver_Var	v,
		int	b
	)

int solver_sign ( solver_Lit p )

int solver_simplify ( solver * s )

int solver_solve	(	solver *	s,
		int	len,
		solver_Lit *	ps
	)

void solver_solve_addLit	(	solver *	s,
		solver_Lit	p
	)

void solver_solve_begin ( solver * s )

int solver_solve_commit ( solver * s )

solver_lbool solver_value_Lit	(	solver *	s,
		solver_Lit	p
	)

solver_lbool solver_value_Var	(	solver *	s,
		solver_Var	x
	)

solver_Var solver_var ( solver_Lit p )

Variable Documentation

const solver_lbool solver_l_False

const solver_lbool solver_l_True

const solver_lbool solver_l_Undef

Typedefs

Functions

Variables

Typedef Documentation

Function Documentation

Variable Documentation