int getInt() {
if (offset>=length) {
- ssize_t ptr;
offset = 0;
- do {
- ptr=read(0, buffer, sizeof(int)*IS_BUFFERSIZE);
- if (ptr == -1)
- exit(-1);
- } while(ptr==0);
+ ssize_t ptr=read(0, buffer, sizeof(int)*IS_BUFFERSIZE);
+ if (ptr == -1 || ptr == 0)
+ exit(-1);
+
ssize_t bytestoread=(4-(ptr & 3)) & 3;
while(bytestoread != 0) {
ssize_t p=read(0, &((char *)buffer)[ptr], bytestoread);
- if (p == -1)
+ if (p == -1 || p == 0)
exit(-1);
bytestoread -= p;
ptr += p;
vec<Lit> clause;
int numvars = solver->nVars();
bool haveClause = false;
+ fprintf(stderr,"Let's read clauses ...\n");
while(true) {
int lit=getInt();
if (lit!=0) {
+// fprintf(stderr,"%d ", lit);
int var = abs(lit) - 1;
while (var >= numvars) {
numvars++;
clause.push( (lit>0) ? mkLit(var) : ~mkLit(var));
haveClause = true;
} else {
+// fprintf(stderr, "\n");
if (haveClause) {
solver->addClause_(clause);
haveClause = false;
clause.clear();
} else {
+// fprintf(stderr, "****************************************************************\n");
//done with clauses
return;
}
switch(command) {
case IS_FREEZE: {
int var=getInt()-1;
+// fprintf(stderr, "Freezing %d\n", var);
solver->setFrozen(var, true);
break;
}
case IS_RUNSOLVER: {
vec<Lit> dummy;
+// SimpSolver* solver2 = (SimpSolver*)solver->clone();
+ double time1 = cpuTime();
lbool ret = solver->solveLimited(dummy);
+// double time2 = cpuTime();
+// vec<Lit> dummy2;
+// lbool ret2 = solver2->solveLimited(dummy2);
+// double time3 = cpuTime();
+// fprintf( stderr, "First execution time: %f\t second execution time: %f\n", time2 - time1, time3-time2);
if (ret == l_True) {
putInt(IS_SAT);
putInt(solver->nVars());
}
} else if (ret == l_False) {
putInt(IS_UNSAT);
+ putInt(solver->assumptionsSize());
+ fprintf(stderr, "assumption size = %d\nConflict Array: ",solver->assumptionsSize());
+ for(int i=0;i<solver->conflict.size();i++) {
+ fprintf(stderr, "%d = %d, ", i, sign(solver->conflict[i])==true);
+ }
+ fprintf(stderr, "\n***********************\n");
+ for(int i=0;i<solver->assumptionsSize();i++) {
+ putInt(sign(solver->conflict[i])==true);
+ }
} else {
putInt(IS_INDETER);
}
#endif
// Extra options:
//
- IntOption verb ("MAIN", "verb", "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2));
+ IntOption verb ("MAIN", "verb", "Verbosity level (0=silent, 1=some, 2=more).", 0, IntRange(0, 2));
BoolOption mod ("MAIN", "model", "show model.", false);
IntOption vv ("MAIN", "vv", "Verbosity every vv conflicts", 10000, IntRange(1,INT32_MAX));
BoolOption pre ("MAIN", "pre", "Completely turn on/off any preprocessing.", true);