User's API

Enumerations

Detailed Description

The basic interaction is best described by the bj-hello-world.c program

#include <stdio.h>
#include "ben_jose.h"

int main(int argc, char** argv)
{
    if(argc < 2){
        printf("args: <cnf_file_path> [<db_dir>]\n");
        return 1;
    }
    char* dd = ".";
    char* ff = argv[1];
    if(argc > 2){
        dd = argv[2];
    }
    
    bj_solver_t ss = bj_solver_create(dd);
    
    bj_satisf_val_t  vv = bj_solve_file(ss, ff);
    switch(vv){
        case bjr_yes_satisf:
            printf("%s is SAT instance\n", ff);
            break;
        case bjr_no_satisf:
            printf("%s is UNS instance\n", ff);
            break;
        case bjr_error:
            {
                printf("ERROR ! in %s\n", ff);
                bj_output_t oo = bj_get_output(ss);
                const char* e_str = bj_error_str(oo.bjo_error);
                printf("%s\n", e_str);
            }
            break;
        default:
            printf("FATAL ERROR ! in %s\n", ff);
            break;
    }
    
    // more info with this functions
    //bj_output_t oo = bj_get_output(ss);
    //const long* aa = bj_get_assig(ss);
    
    bj_solver_release(ss);
    return 0;
}

Enumeration Type Documentation

enum bj_satisf_val_t

Posible final results of the solving process.

Enumerator
bjr_unknown_satisf	Unknown result.
bjr_yes_satisf	Satisfiable CNF.
bjr_no_satisf	Unsatisfiable CNF.
bjr_error	Error result.

enum bj_error_t

Posible errors of the solving process.

Enumerator
bje_no_error	No error.
bje_internal	Internal.
bje_internal_ex	Internal with explanation.
bje_memout	Out of memory.
bje_timeout	Timeout.
bje_instance_cannot_load	Can not load instance.
bje_file_cannot_open	Can not open file.
bje_file_corrupted	Corrupted file.
bje_file_too_big	Too big file (must fit in memory)
bje_path_too_long	Path too long.
bje_invalid_root_directory	Invalid root (database) directory.
bje_parse_bad_number	Found a non number where a number is expected.
bje_dimacs_no_cnf_declaration	Bad DIMACS format. Non existant cnf declaration line.
bje_dimacs_bad_cls_num	Bad DIMACS format. Inconsistent clause count with cnf declaration.
bje_dimacs_format_err	Bad DIMACS format. General format error.
bje_dimacs_zero_vars	Bad DIMACS format. No variables found.
bje_dimacs_zero_clauses	Bad DIMACS format. No clauses found.
bje_dimacs_bad_literal	Bad DIMACS format. Invalid clause literal.
bje_dimacs_clause_too_long	Bad DIMACS format. Clause too long.

enum bj_param_t

Posible parameters for the solving process.

Enumerator
bjp_invalid	Invalid parameter.
bjp_as_release	Run debug version of library as release version. Assumes linking with the debug version.
bjp_only_deduc	Run only deduction (do not use training). For debugging purposes only.
bjp_write_proofs	Write a JSON proof if the CNF is unsatisfiable.
bjp_test_result	Compare results to an existing .test file or write one if not found.