ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
cadicalSolver.h
Go to the documentation of this file.
1
20
21#ifndef ABC_SAT_CADICAL_SOLVER_H_
22#define ABC_SAT_CADICAL_SOLVER_H_
23
27
28#include "aig/gia/gia.h"
29#include "sat/cnf/cnf.h"
30
34
36
40
49
50
54
58
61extern int cadical_solver_addclause(cadical_solver* s, int* begin, int* end);
62extern int cadical_solver_solve(cadical_solver* s, int* begin, int* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
63extern int cadical_solver_final(cadical_solver* s, int** ppArray);
66extern void cadical_solver_setnvars(cadical_solver* s,int n);
68extern Vec_Int_t * cadical_solve_cnf( Cnf_Dat_t * pCnf, char * pArgs, int nConfs, int nTimeLimit, int fSat, int fUnsat, int fPrintCex, int fVerbose );
69
71
72#endif
73
#define ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Vec_Int_t * cadical_solve_cnf(Cnf_Dat_t *pCnf, char *pArgs, int nConfs, int nTimeLimit, int fSat, int fUnsat, int fPrintCex, int fVerbose)
int cadical_solver_final(cadical_solver *s, int **ppArray)
int cadical_solver_addclause(cadical_solver *s, int *begin, int *end)
int cadical_solver_get_var_value(cadical_solver *s, int v)
int cadical_solver_nvars(cadical_solver *s)
typedefABC_NAMESPACE_HEADER_START struct cadical_solver_ cadical_solver
INCLUDES ///.
void cadical_solver_setnvars(cadical_solver *s, int n)
int cadical_solver_addvar(cadical_solver *s)
int cadical_solver_solve(cadical_solver *s, int *begin, int *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
cadical_solver * cadical_solver_new(void)
MACRO DEFINITIONS ///.
void cadical_solver_delete(cadical_solver *s)
struct Cnf_Dat_t_ Cnf_Dat_t
Definition cnf.h:52
Vec_Int_t * vAssumptions
Vec_Int_t * vCore