solver.h File Reference

Go to the source code of this file.

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

solver

typedef typedefABC_NAMESPACE_HEADER_START struct solver_t solver

Definition at line 30 of file solver.h.

solver_lbool

typedef int solver_lbool

Definition at line 33 of file solver.h.

solver_Lit

typedef int solver_Lit

Definition at line 32 of file solver.h.

solver_Var

typedef int solver_Var

Definition at line 31 of file solver.h.

Function Documentation

solver_addClause()

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

solver_addClause_addLit()

void solver_addClause_addLit	(	solver *	s,
		solver_Lit	p )

solver_addClause_begin()

void solver_addClause_begin

(

solver *

s

)

solver_addClause_commit()

int solver_addClause_commit

(

solver *

s

)

solver_conflict_len()

int solver_conflict_len

(

solver *

s

)

solver_conflict_nthLit()

solver_Lit solver_conflict_nthLit	(	solver *	s,
		int	i )

solver_delete()

void solver_delete

(

solver *

s

)

solver_get_l_False()

solver_lbool solver_get_l_False

(

void

)

solver_get_l_True()

solver_lbool solver_get_l_True

(

void

)

solver_get_l_Undef()

solver_lbool solver_get_l_Undef

(

void

)

solver_mkLit()

solver_Lit solver_mkLit

(

solver_Var

x

)

solver_mkLit_args()

solver_Lit solver_mkLit_args	(	solver_Var	x,
		int	sign )

solver_modelValue_Lit()

solver_lbool solver_modelValue_Lit	(	solver *	s,
		solver_Lit	p )

solver_modelValue_Var()

solver_lbool solver_modelValue_Var	(	solver *	s,
		solver_Var	x )

solver_negate()

solver_Lit solver_negate

(

solver_Lit

p

)

solver_new()

solver * solver_new

(

void

)

solver_newLit()

solver_Lit solver_newLit

(

solver *

s

)

solver_newVar()

solver_Var solver_newVar

(

solver *

s

)

solver_num_assigns()

int solver_num_assigns

(

solver *

s

)

solver_num_clauses()

int solver_num_clauses

(

solver *

s

)

solver_num_conflicts()

int solver_num_conflicts

(

solver *

s

)

solver_num_freeVars()

int solver_num_freeVars

(

solver *

s

)

solver_num_learnts()

int solver_num_learnts

(

solver *

s

)

solver_num_vars()

int solver_num_vars

(

solver *

s

)

solver_okay()

int solver_okay

(

solver *

s

)

solver_set_verbosity()

void solver_set_verbosity	(	solver *	s,
		int	v )

solver_setDecisionVar()

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

solver_setPolarity()

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

solver_sign()

int solver_sign

(

solver_Lit

p

)

solver_simplify()

int solver_simplify

(

solver *

s

)

solver_solve()

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

solver_solve_addLit()

void solver_solve_addLit	(	solver *	s,
		solver_Lit	p )

solver_solve_begin()

void solver_solve_begin

(

solver *

s

)

solver_solve_commit()

int solver_solve_commit

(

solver *

s

)

solver_value_Lit()

solver_lbool solver_value_Lit	(	solver *	s,
		solver_Lit	p )

solver_value_Var()

solver_lbool solver_value_Var	(	solver *	s,
		solver_Var	x )

solver_var()

solver_Var solver_var

(

solver_Lit

p

)

Variable Documentation

solver_l_False

const solver_lbool solver_l_False

extern

solver_l_True

const solver_lbool solver_l_True

extern

solver_l_Undef

const solver_lbool solver_l_Undef

extern