ben_jose.h

Go to the documentation of this file.

/*************************************************************

This file is part of ben-jose.

ben-jose is free software: you can redistribute it and/or modify
it under the terms of the version 3 of the GNU General Public 
License as published by the Free Software Foundation.

ben-jose is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with ben-jose.  If not, see <http://www.gnu.org/licenses/>.

------------------------------------------------------------

Copyright (C) 2007-2012, 2014-2016. QUIROGA BELTRAN, Jose Luis.
Id (cedula): 79523732 de Bogota - Colombia.
See https://github.com/joseluisquiroga/ben-jose

ben-jose is free software thanks to The Glory of Our Lord 
    Yashua Melej Hamashiaj.
Our Resurrected and Living, both in Body and Spirit, 
    Prince of Peace.

-------------------------------------------------------------- */
//--------------------------------------------------------------

#ifndef BEN_JOSE_H
#define BEN_JOSE_H

#ifdef __cplusplus
extern "C" {
#endif
    
//============================================================
#define RES_UNKNOWN_STR "unknown"
#define RES_YES_SATISF_STR "yes_satisf"
#define RES_NO_SATISF_STR "no_satisf"
#define RES_ERROR_STR "error"

#define RESULT_FIELD_SEP        "|"
#define RESULT_FIELD_SEP_CHAR       '|'

//=============================================================================
typedef enum {
    bjr_unknown_satisf,     
    bjr_yes_satisf,         
    bjr_no_satisf,          
    bjr_error               
} bj_satisf_val_t;

//=============================================================================
typedef enum {
    bje_no_error,   
    bje_internal,   
    bje_internal_ex,    
    bje_memout, 
    bje_timeout,    
    bje_instance_cannot_load,   
    bje_file_cannot_open,   
    bje_file_corrupted, 
    bje_file_too_big,   
    bje_path_too_long,  
    bje_invalid_root_directory, 
    bje_parse_bad_number,   
    bje_dimacs_no_cnf_declaration,  
    bje_dimacs_bad_cls_num, 
    bje_dimacs_format_err,  
    bje_dimacs_zero_vars,   
    bje_dimacs_zero_clauses,    
    bje_dimacs_bad_literal, 
    bje_dimacs_clause_too_long  
} bj_error_t;

//=============================================================================
typedef enum {
    bjp_invalid,    
    bjp_as_release, 
    bjp_only_deduc, 
    bjp_write_proofs,   
    bjp_test_result 
} bj_param_t;

//=============================================================================
typedef struct {
    bj_satisf_val_t     bjo_result; 
    
    double      bjo_solve_time; 
    long        bjo_num_vars;   
    long        bjo_num_ccls;   
    long        bjo_num_lits;   
    
    double      bjo_num_laps;   
    double      bjo_num_recoils;    
    
    double      bjo_load_time;  
    double      bjo_num_cnf_saved;  
    double      bjo_num_cnf_finds;  
    double      bjo_quick_discards; 
    
    bj_error_t  bjo_error;  
    char        bjo_err_char;   
    long        bjo_err_line;   
    long        bjo_err_pos;    
    long        bjo_err_num_decl_cls;   
    long        bjo_err_num_decl_vars;  
    long        bjo_err_num_read_cls;   
    long        bjo_err_bad_lit;    
    
    char        bjo_dbg_enabled;    
    char        bjo_dbg_never_write;    
    char        bjo_dbg_never_find; 
    char        bjo_dbg_min_trainable;  
    char        bjo_dbg_as_release; 
} bj_output_t;

typedef void*   bj_solver_t;

#define bj_solver_is_null(bjs) (bjs == NULL)

// TO USER: DO NOT FREE OUTPUT POINTERS when calling these 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);
//void      bj_set_param_str(bj_solver_t bjs, bj_param_t prm, char* val);



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);

// TO USER: DO NOT FREE OUTPUT POINTERS when calling these functions

#ifdef __cplusplus
}
#endif

#endif      // BEN_JOSE_H