ben_jose API declaration. More...

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

Macros
#define	RES_UNKNOWN_STR "unknown"
	String to print a bjr_unknown_satisf result.

#define	bj_solver_is_null(bjs) (bjs == NULL)
	Checks if a ben-jose solver object is NULL.

Typedefs
typedef void *	bj_solver_t
	A ben-jose solver object is of this tyoe.

Enumerations

Functions
void	bj_init_output (bj_output_t *the_out)

bj_solver_t	bj_solver_create (const char *bjs_dir_path)

void	bj_solver_release (bj_solver_t bjs)

void	bj_set_param_char (bj_solver_t bjs, bj_param_t prm, char val)

char	bj_get_param_char (bj_solver_t bjs, bj_param_t prm)

const char *	bj_get_database_path (bj_solver_t bjs)

bj_satisf_val_t	bj_solve_file (bj_solver_t bjs, const char *f_path)

bj_satisf_val_t	bj_solve_data (bj_solver_t bjs, long dat_sz, const char *dat)

bj_satisf_val_t	bj_solve_literals (bj_solver_t bjs, long num_vars, long num_cls, long lits_sz, long *lits)

bj_satisf_val_t	bj_get_result (bj_solver_t bjs)

bj_output_t	bj_get_output (bj_solver_t bjs)

const char *	bj_get_solve_file_path (bj_solver_t bjs)

const long *	bj_get_assig (bj_solver_t bjs)

const char *	bj_get_last_proof_path (bj_solver_t bjs)

const char *	bj_get_error_stack_str (bj_solver_t bjs)

const char *	bj_get_error_assert_str (bj_solver_t bjs)

const char *	bj_get_result_titles_string (bj_solver_t bjs)

const char *	bj_get_result_string (bj_solver_t bjs)

void	bj_parse_result_string (bj_solver_t bjs, const char *rslt_str)

void	bj_restart (bj_solver_t bjs)

void	bj_print_paths (bj_solver_t bjs)

const char *	bj_error_str (bj_error_t bje)

Detailed Description

ben_jose API declaration.

DO NOT free any pointer returned by these functions. They are pointers to the internal structure of a solver. A solver is an opaque structure to the user represented by objects of type obj_solver_t.

DO NOT release the memory of any returned pointer.

Function Documentation

void bj_init_output ( bj_output_t * the_out )

Init a bj_output_t structure

Parameters

the_out A pointer to the structure to be initialized

Here is the call graph for this function:

bj_solver_t bj_solver_create ( const char * bjs_dir_path )

Create a solver object to solve one or more CNFs

Parameters

bjs_dir_path A C string that represents the path of the database of CNFs.

Returns: A bj_solver_t object representing a solver.

void bj_solver_release ( bj_solver_t bjs )

Release a solver object created with bj_solver_create

Parameters

bjs	The solver object to be released.

void bj_set_param_char	(	bj_solver_t	bjs,
		bj_param_t	prm,
		char	val
	)

Set an input parameter in the solver

Parameters

bjs	The solver object to be used.
prm	The parameter.
val	The value. For boolen values it is 0 (false) or not 0 (true)

char bj_get_param_char	(	bj_solver_t	bjs,
		bj_param_t	prm
	)

Get the value of a previusly set (with bj_set_param_char) input parameter.

Parameters

bjs	The solver object to be used.
prm	The parameter.

Returns: The value. For boolen values it is 0 (false) or 1 (true)

const char* bj_get_database_path ( bj_solver_t bjs )

Get the value of a previusly set database path (with bj_solver_create).

Parameters

bjs	The solver object to be used.

Returns: The database directory path. Do not free the returned pointer.

bj_satisf_val_t bj_solve_file	(	bj_solver_t	bjs,
		const char *	f_path
	)

Solve a CNF given the DIMACS formated file path of the CNF.

Parameters

bjs	The solver object to be used.
f_path	The CNF file path. It must be in DIMACS format.

Returns: The solving result.

Here is the call graph for this function:

bj_satisf_val_t bj_solve_data	(	bj_solver_t	bjs,
		long	dat_sz,
		const char *	dat
	)

Solve a CNF given a DIMACS formated C ASCII characters array.

Parameters

bjs	The solver object to be used.
dat_sz	The number of ASCII characters in dat.
dat	The DIMACS formated C ASCII characters array. It can be the exact contents read of a valid DIMACS file.

Returns: The solving result.

Here is the call graph for this function:

bj_satisf_val_t bj_solve_literals	(	bj_solver_t	bjs,
		long	num_vars,
		long	num_cls,
		long	lits_sz,
		long *	lits
	)

Solve a CNF given the DIMACS values of a CNF.

Parameters

bjs	The solver object to be used.
num_vars	The number of variables in used in lits. It is the value as read in a cnf declaration of a DIMACS file.
num_cls	The number of clauses found in lits. It is the value as read in a cnf declaration of a DIMACS file.
lits_sz	The size of the lits parameter.
lits	THe array containing a set of clauses separated by zeros. Ej: [1 2 0 3 4 5 0] representes two clauses: [1 2] and [3 4 5].

Returns: The solving result.

Here is the call graph for this function:

bj_satisf_val_t bj_get_result ( bj_solver_t bjs )

Get the result of a solving process. A bj_solve_ function must have been previusly called.

Parameters

bjs	The solver object to be used.

Returns: The solving result. It has the same value returned by the previusly called bj_solve_ function.

bj_output_t bj_get_output ( bj_solver_t bjs )

Get all the output a solving process. A bj_solve_ function must have been previusly called.

Parameters

bjs	The solver object to be used.

Returns: The solving output.

See also: bj_output_t

Here is the call graph for this function:

const char* bj_get_solve_file_path ( bj_solver_t bjs )

Returns the value passed to bj_solve_file. A bj_solve_ function must have been previusly called.

Parameters

bjs	The solver object to be used.

Returns: The value passed to bj_solve_file or null otherwise (other bj_solve_ function was called).

const long* bj_get_assig ( bj_solver_t bjs )

Get the assignation to variables that satisfies the CNF. A bj_solve_ function must have been previusly called.

Parameters

bjs	The solver object to be used.

Returns: An array (here called 'assig') with the assignation to variables that satisfies the CNF.

'assig' always ends with a 0.

No memory after that 0 should be accessed.

Let vv = assig[ii]. Then:

If vv is positive it means the the variable represented by abs(vv) is assigned true
If vv is negative it means the the variable represented by abs(vv) is assigned false

Example: [-20 4 -12 6 9 0]

Means:

set var 20 to false
set var 4 to true
set var 12 to false
set var 6 to true
set var 9 to true

And that assignation satisfies the whole CNF (it might have more than 20 variables).

const char* bj_get_last_proof_path ( bj_solver_t bjs )

Returns the last written proof path. A bj_solve_ function must have been previusly called.

Parameters

bjs	The solver object to be used.

Returns: The path to the last written GSON proof file.

NULL is returned if the parameter bjp_write_proofs was not used before calling a bj_solve_ function.

const char* bj_get_error_stack_str ( bj_solver_t bjs )

Get the stack when the error ocurred. A bj_solve_ function must have been previusly called.

Parameters

bjs	The solver object to be used.

Returns: The stack when the error ocurred.

Funtion for debugging purposes. Only returns a valid value if an error has ocurred during solving.

const char* bj_get_error_assert_str ( bj_solver_t bjs )

Get the assert that failed. A bj_solve_ function must have been previusly called.

Parameters

bjs	The solver object to be used.

Returns: The assert that failed.

Funtion for debugging purposes. Only returns a valid value if an assert has failed.

const char* bj_get_result_titles_string ( bj_solver_t bjs )

Get a string with the titles of a result string fields.

Parameters

bjs	The solver object to be used.

Returns: A string with the titles of a result string fields.

Funtion for testing purposes.

const char* bj_get_result_string ( bj_solver_t bjs )

Get a string with the result string. A bj_solve_ function must have been previusly called.

Parameters

bjs	The solver object to be used.

Returns: A string with the result string.

Funtion for testing purposes. It contains a concatenation of the string representation of some fields obtained otherwise with the bj_get_output funtion.

void bj_parse_result_string	(	bj_solver_t	bjs,
		const char *	rslt_str
	)

Sets internal values in the solver with a result string previusly returned by bj_get_result_string.

Parameters

bjs	The solver object to be used.
rslt_str	A string with the result string.

Funtion for testing purposes. It sets internal values in the solver so that a call to bj_get_output will return the parsed values.

void bj_restart ( bj_solver_t bjs )

Resets all internal values in the solver.

Parameters

bjs	The solver object to be used.

void bj_print_paths ( bj_solver_t bjs )

Prints all paths used by the solver.

Parameters

bjs	The solver object to be used.

const char* bj_error_str ( bj_error_t bje )

Gets a string representing the error. A bj_solve_ function must have been previusly called.

Parameters

bjs	The solver object to be used.

Returns: A string representing the error.

Macros

Typedefs

Enumerations

Functions

Detailed Description

DO NOT release the memory of any returned pointer.

Function Documentation