37 #define READER_NAME "cnfreader" 38 #define READER_DESC "file reader for SAT problems in conjunctive normal form" 39 #define READER_EXTENSION "cnf" 41 #define MAXLINELEN 65536 62 const char* warningmsg
82 assert(buffer != NULL);
84 assert(linecount != NULL);
92 linelen = (int)strlen(line);
93 if( linelen == size-1 )
104 while( line != NULL && (*line ==
'c' || *line ==
'\n') );
106 if( line != NULL && linelen >= 2 && line[linelen-2] ==
'\n' )
107 line[linelen-2] =
'\0';
108 else if( linelen == 0 )
111 assert((line == NULL) == (*buffer ==
'\0'));
156 assert(scip != NULL);
157 assert(file != NULL);
165 readError(scip, linecount,
"problem declaration line expected");
169 if( sscanf(line,
"p %8s %d %d", format, &nvars, &nclauses) != 3 )
171 readError(scip, linecount,
"invalid problem declaration (must be 'p cnf <nvars> <nclauses>')");
174 if( strcmp(format,
"cnf") != 0 )
206 for( v = 0; v < nvars; ++v )
210 NULL, NULL, NULL, NULL, NULL) );
220 retcode =
readCnfLine(scip, file, line, (
int)
sizeof(line), &linecount);
224 if( *line !=
'\0' && *line !=
'%' )
226 tok =
SCIPstrtok(line,
" \f\n\r\t", &nexttok);
230 if( sscanf(tok,
"%d", &v) != 1 )
243 readWarning(scip, linecount,
"empty clause detected in line -- problem infeasible");
270 for( i = 0; i < clauselen; ++i )
283 else if( v >= -nvars && v <= nvars )
285 if( clauselen >= nvars )
287 readError(scip, linecount,
"too many literals in clause");
301 clausevars[clauselen] = vars[varnum];
315 tok =
SCIPstrtok(NULL,
" \f\n\r\t", &nexttok);
319 while( *line !=
'\0' && *line !=
'%' );
324 SCIPwarningMessage(scip,
"found %d additional literals after last clause\n", clauselen);
328 if( clausenum != nclauses )
336 for( v = 0; v < nvars; ++v )
362 assert(
scip != NULL);
363 assert(reader != NULL);
380 assert(reader != NULL);
382 assert(filename != NULL);
383 assert(result != NULL);
429 "reading/cnfreader/useobj",
"should an artificial objective, depending on the number of clauses a variable appears in, be used?",
static void readWarning(SCIP *scip, int linecount, const char *warningmsg)
SCIP_CONSHDLR * SCIPfindConshdlr(SCIP *scip, const char *name)
static SCIP_DECL_READERCOPY(readerCopyCnf)
SCIP_RETCODE SCIPcreateProb(SCIP *scip, const char *name, SCIP_DECL_PROBDELORIG((*probdelorig)), SCIP_DECL_PROBTRANS((*probtrans)), SCIP_DECL_PROBDELTRANS((*probdeltrans)), SCIP_DECL_PROBINITSOL((*probinitsol)), SCIP_DECL_PROBEXITSOL((*probexitsol)), SCIP_DECL_PROBCOPY((*probcopy)), SCIP_PROBDATA *probdata)
static SCIP_RETCODE readCnfLine(SCIP *scip, SCIP_FILE *file, char *buffer, int size, int *linecount)
SCIP_RETCODE SCIPcreateConsSetcover(SCIP *scip, SCIP_CONS **cons, const char *name, int nvars, SCIP_VAR **vars, SCIP_Bool initial, SCIP_Bool separate, SCIP_Bool enforce, SCIP_Bool check, SCIP_Bool propagate, SCIP_Bool local, SCIP_Bool modifiable, SCIP_Bool dynamic, SCIP_Bool removable, SCIP_Bool stickingatnode)
const char * SCIPreaderGetName(SCIP_READER *reader)
SCIP_RETCODE SCIPreleaseVar(SCIP *scip, SCIP_VAR **var)
SCIP_Real SCIPinfinity(SCIP *scip)
int SCIPsnprintf(char *t, int len, const char *s,...)
enum SCIP_Retcode SCIP_RETCODE
static SCIP_RETCODE readCnf(SCIP *scip, SCIP_FILE *file)
#define SCIPfreeBufferArray(scip, ptr)
Constraint handler for the set partitioning / packing / covering constraints .
void SCIPwarningMessage(SCIP *scip, const char *formatstr,...)
SCIP_FILE * SCIPfopen(const char *path, const char *mode)
SCIP_RETCODE SCIPsetObjsense(SCIP *scip, SCIP_OBJSENSE objsense)
SCIP_RETCODE SCIPaddCons(SCIP *scip, SCIP_CONS *cons)
Constraint handler for logicor constraints (equivalent to set covering, but algorithms are suited fo...
struct SCIP_File SCIP_FILE
char * SCIPfgets(char *s, int size, SCIP_FILE *stream)
SCIP_RETCODE SCIPgetBoolParam(SCIP *scip, const char *name, SCIP_Bool *value)
SCIP_RETCODE SCIPchgVarObj(SCIP *scip, SCIP_VAR *var, SCIP_Real newobj)
SCIP_RETCODE SCIPincludeReaderCnf(SCIP *scip)
#define SCIPallocBufferArray(scip, ptr, num)
public data structures and miscellaneous methods
SCIP_RETCODE SCIPincludeReaderBasic(SCIP *scip, SCIP_READER **readerptr, const char *name, const char *desc, const char *extension, SCIP_READERDATA *readerdata)
void SCIPprintSysError(const char *message)
SCIP_RETCODE SCIPcreateVar(SCIP *scip, SCIP_VAR **var, const char *name, SCIP_Real lb, SCIP_Real ub, SCIP_Real obj, SCIP_VARTYPE vartype, SCIP_Bool initial, SCIP_Bool removable, SCIP_DECL_VARDELORIG((*vardelorig)), SCIP_DECL_VARTRANS((*vartrans)), SCIP_DECL_VARDELTRANS((*vardeltrans)), SCIP_DECL_VARCOPY((*varcopy)), SCIP_VARDATA *vardata)
Constraint handler for linear constraints in their most general form, .
SCIP_RETCODE SCIPcreateConsLogicor(SCIP *scip, SCIP_CONS **cons, const char *name, int nvars, SCIP_VAR **vars, SCIP_Bool initial, SCIP_Bool separate, SCIP_Bool enforce, SCIP_Bool check, SCIP_Bool propagate, SCIP_Bool local, SCIP_Bool modifiable, SCIP_Bool dynamic, SCIP_Bool removable, SCIP_Bool stickingatnode)
SCIP_RETCODE SCIPsetReaderCopy(SCIP *scip, SCIP_READER *reader, SCIP_DECL_READERCOPY((*readercopy)))
SCIP_RETCODE SCIPcreateConsLinear(SCIP *scip, SCIP_CONS **cons, const char *name, int nvars, SCIP_VAR **vars, SCIP_Real *vals, SCIP_Real lhs, SCIP_Real rhs, SCIP_Bool initial, SCIP_Bool separate, SCIP_Bool enforce, SCIP_Bool check, SCIP_Bool propagate, SCIP_Bool local, SCIP_Bool modifiable, SCIP_Bool dynamic, SCIP_Bool removable, SCIP_Bool stickingatnode)
static SCIP_DECL_READERREAD(readerReadCnf)
SCIP_RETCODE SCIPaddVar(SCIP *scip, SCIP_VAR *var)
SCIP_RETCODE SCIPreleaseCons(SCIP *scip, SCIP_CONS **cons)
static void readError(SCIP *scip, int linecount, const char *errormsg)
SCIP_RETCODE SCIPsetReaderRead(SCIP *scip, SCIP_READER *reader, SCIP_DECL_READERREAD((*readerread)))
int SCIPfclose(SCIP_FILE *fp)
char * SCIPstrtok(char *s, const char *delim, char **ptrptr)
SCIP_RETCODE SCIPgetNegatedVar(SCIP *scip, SCIP_VAR *var, SCIP_VAR **negvar)
SCIP_RETCODE SCIPaddBoolParam(SCIP *scip, const char *name, const char *desc, SCIP_Bool *valueptr, SCIP_Bool isadvanced, SCIP_Bool defaultvalue, SCIP_DECL_PARAMCHGD((*paramchgd)), SCIP_PARAMDATA *paramdata)