SatMinisat_ptr SatMinisat_create( const char* name, boolean enable_proof_logging )
SatMinisat.c
void SatMinisat_destroy( SatMinisat_ptr self )
SatMinisat.c
SatZchaff_ptr SatZchaff_create( const char* name )
SatZchaff.c
void SatZchaff_destroy( SatZchaff_ptr self )
SatZchaff.c
static int _get_clause_size( const int * clause )
SatMinisat.c
static int _get_clause_size( const int * clause )
SatZchaff.c
void sat_minisat_add( const SatSolver_ptr solver, const Be_Cnf_ptr cnfProb, SatSolverGroup group )
SatMinisat.c
void sat_minisat_clear_preferred_variables( const SatSolver_ptr solver )
SatSolver_set_preferred_variables
SatMinisat.c
int sat_minisat_cnfLiteral2minisatLiteral( SatMinisat_ptr self, int cnfLiteral )
sat_minisat_minisatLiteral2cnfLiteral
SatMinisat.c
SatSolverGroup sat_minisat_create_group( const SatIncSolver_ptr solver )
SatIncSolver_destroy_group
SatIncSolver_move_to_permanent_and_destroy_group
SatMinisat.c
static SatSolverItpGroup sat_minisat_curr_itp_group( SatSolver_ptr solver )
SatMinisat.c
void sat_minisat_deinit( SatMinisat_ptr self )
SatMinisat.c
void sat_minisat_destroy_group( const SatIncSolver_ptr solver, SatSolverGroup group )
SatIncSolver_create_group
SatMinisat.c
void sat_minisat_enlarge_minisatClause( const SatMinisat_ptr self, unsigned int minSize )
sat_minisat_add
SatMinisat.c
static Term sat_minisat_extract_interpolant( SatSolver_ptr solver, int nof_ga_groups, SatSolverItpGroup* ga_groups, TermFactoryCallbacks_ptr callbacks, TermFactoryCallbacksUserData_ptr user_data )
SatMinisat.c
static void sat_minisat_finalize( Object_ptr object, void* dummy )
SatMinisat.c
Slist_ptr sat_minisat_get_conflicts( const SatSolver_ptr solver )
sat_minisat_solve_permanent_group_assume
sat_minisat_make_conflicts
SatMinisat.c
int sat_minisat_get_minisatClauseSize( const SatMinisat_ptr self )
SatMinisat.c
int* sat_minisat_get_minisatClause( const SatMinisat_ptr self )
SatMinisat.c
int sat_minisat_get_polarity_mode( const SatSolver_ptr solver )
SatMinisat.c
void sat_minisat_init( SatMinisat_ptr self, const char* name, boolean enable_proof_logging )
SatMinisat.c
Slist_ptr sat_minisat_make_conflicts( const SatMinisat_ptr self )
sat_minisat_solve_permanent_group_assume
sat_minisat_get_conflict
SatMinisat.c
Slist_ptr sat_minisat_make_model( const SatSolver_ptr solver )
SatMinisat.c
int sat_minisat_minisatLiteral2cnfLiteral( SatMinisat_ptr self, int minisatLiteral )
sat_minisat_cnfLiteral2minisatLiteral
SatMinisat.c
void sat_minisat_move_to_permanent_and_destroy_group( const SatIncSolver_ptr solver, SatSolverGroup group )
SatIncSolver_create_group
SatSolver_get_permanent_group
SatMinisat.c
static SatSolverItpGroup sat_minisat_new_itp_group( SatSolver_ptr solver )
SatMinisat.c
void sat_minisat_set_polarity_mode( SatSolver_ptr solver, int mode )
SatMinisat.c
void sat_minisat_set_polarity( const SatSolver_ptr solver, const Be_Cnf_ptr cnfProb, int polarity, SatSolverGroup group )
SatMinisat.c
void sat_minisat_set_preferred_variables( const SatSolver_ptr solver, const Slist_ptr cnfVars )
SatSolver_clear_preferred_variables
SatMinisat.c
void sat_minisat_set_random_mode( SatSolver_ptr solver, double seed )
SatMinisat.c
SatSolverResult sat_minisat_solve_all_groups( const SatSolver_ptr solver )
SatMinisat.c
SatSolverResult sat_minisat_solve_groups( const SatIncSolver_ptr solver, const Olist_ptr groups )
SatMinisat.c
SatSolverResult sat_minisat_solve_permanent_group_assume( const SatSolver_ptr sol, const Slist_ptr assumptions )
sat_minisat_get_conflict
sat_minisat_make_conflicts
SatMinisat.c
SatSolverResult sat_minisat_solve_without_groups( const SatIncSolver_ptr solver, const Olist_ptr groups )
SatSolverResult
SatSolver_get_permanent_group
SatIncSolver_create_group
SatSolver_get_model
SatMinisat.c
void sat_zchaff_add( const SatSolver_ptr solver, const Be_Cnf_ptr cnfProb, SatSolverGroup group )
SatZchaff.c
void sat_zchaff_clear_preferred_variables( const SatSolver_ptr solver )
sat_zchaff_set_preferred_variables
SatZchaff.c
int sat_zchaff_cnfLiteral2zchaffLiteral( SatZchaff_ptr self, int cnfLiteral )
sat_zchaff_zchaffLiteral2cnfLiteral
SatZchaff.c
SatSolverGroup sat_zchaff_create_group( const SatIncSolver_ptr solver )
SatIncSolver_destroy_group
SatIncSolver_move_to_permanent_and_destroy_group
SatZchaff.c
void sat_zchaff_deinit( SatZchaff_ptr self )
SatZchaff.c
void sat_zchaff_destroy_group( const SatIncSolver_ptr solver, SatSolverGroup group )
SatIncSolver_create_group
SatZchaff.c
static void sat_zchaff_finalize( Object_ptr object, void* dummy )
SatZchaff.c
Slist_ptr sat_zchaff_get_conflicts( const SatSolver_ptr self )
sat_minisat_solve_permanent_group_assume
sat_minisat_make_conflict
SatZchaff.c
void sat_zchaff_init( SatZchaff_ptr self, const char* name )
SatZchaff.c
Slist_ptr sat_zchaff_make_conflicts( const SatZchaff_ptr self )
sat_zchaff_solve_permanent_group_assume
sat_zchaff_get_conflict
SatZchaff.c
Slist_ptr sat_zchaff_make_model( const SatSolver_ptr solver )
SatZchaff.c
void sat_zchaff_move_to_permanent_and_destroy_group( const SatIncSolver_ptr solver, SatSolverGroup group )
SatIncSolver_create_group
SatSolver_get_permanent_group
SatZchaff.c
void sat_zchaff_set_polarity( const SatSolver_ptr solver, const Be_Cnf_ptr cnfProb, int polarity, SatSolverGroup group )
SatZchaff.c
void sat_zchaff_set_preferred_variables( const SatSolver_ptr solver, const Slist_ptr cnfVars )
sat_zchaff_clear_preferred_variables
SatZchaff.c
SatSolverResult sat_zchaff_solve_all_groups( const SatSolver_ptr solver )
SatZchaff.c
SatSolverResult sat_zchaff_solve_groups( const SatIncSolver_ptr solver, const Olist_ptr groups )
SatZchaff.c
SatSolverResult sat_zchaff_solve_permanent_group_assume( const SatSolver_ptr self, const Slist_ptr assumptions )
sat_zchaff_get_conflict
sat_zchaff_make_conflict
SatZchaff.c
SatSolverResult sat_zchaff_solve_without_groups( const SatIncSolver_ptr solver, const Olist_ptr groups )
SatSolverResult
SatSolver_get_permanent_group
SatIncSolver_create_group
SatSolver_get_model
SatZchaff.c
int sat_zchaff_zchaffLiteral2cnfLiteral( SatZchaff_ptr self, int zchaffLiteral )
sat_zchaff_cnfLiteral2zchaffLiteral
SatZchaff.c