Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Allow '-' to be passed as input and output. #8

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Allow '-' to be passed as input and output. #8

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
52 changes: 31 additions & 21 deletions minisat/core/Main.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,10 +41,10 @@ static void SIGINT_interrupt(int) { solver->interrupt(); }
// destructors and may cause deadlocks if a malloc/free function happens to be running (these
// functions are guarded by locks for multithreaded use).
static void SIGINT_exit(int) {
printf("\n"); printf("*** INTERRUPTED ***\n");
fprintf(stderr, "\n"); fprintf(stderr, "*** INTERRUPTED ***\n");
if (solver->verbosity > 0){
solver->printStats();
printf("\n"); printf("*** INTERRUPTED ***\n"); }
fprintf(stderr, "\n"); fprintf(stderr, "*** INTERRUPTED ***\n"); }
_exit(1); }


Expand Down Expand Up @@ -82,28 +82,38 @@ int main(int argc, char** argv)
if (mem_lim != 0) limitMemory(mem_lim);

if (argc == 1)
printf("Reading from standard input... Use '--help' for help.\n");

gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb");
fprintf(stderr, "Reading from standard input... Use '--help' for help.\n");

gzFile in;
bool is_stdin = false;
if (argc == 1 || strcmp(argv[1], "-") == 0) {
in = gzdopen(0, "rb");
is_stdin = true;
}
else
in = gzopen(argv[1], "rb");

if (in == NULL)
printf("ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : argv[1]), exit(1);
fprintf(stderr, "ERROR! Could not open file: %s\n", is_stdin ? "<stdin>" : argv[1]), exit(1);

if (S.verbosity > 0){
printf("============================[ Problem Statistics ]=============================\n");
printf("| |\n"); }
fprintf(stderr, "============================[ Problem Statistics ]=============================\n");
fprintf(stderr, "| |\n"); }

parse_DIMACS(in, S, (bool)strictp);
gzclose(in);
FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL;
FILE* res = NULL;
if (argc >= 3)
res = (strcmp(argv[2], "-") == 0) ? stdout : fopen(argv[2], "wb");

if (S.verbosity > 0){
printf("| Number of variables: %12d |\n", S.nVars());
printf("| Number of clauses: %12d |\n", S.nClauses()); }
fprintf(stderr, "| Number of variables: %12d |\n", S.nVars());
fprintf(stderr, "| Number of clauses: %12d |\n", S.nClauses()); }

double parsed_time = cpuTime();
if (S.verbosity > 0){
printf("| Parse time: %12.2f s |\n", parsed_time - initial_time);
printf("| |\n"); }
fprintf(stderr, "| Parse time: %12.2f s |\n", parsed_time - initial_time);
fprintf(stderr, "| |\n"); }

// Change to signal-handlers that will only notify the solver and allow it to terminate
// voluntarily:
Expand All @@ -112,20 +122,20 @@ int main(int argc, char** argv)
if (!S.simplify()){
if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res);
if (S.verbosity > 0){
printf("===============================================================================\n");
printf("Solved by unit propagation\n");
fprintf(stderr, "===============================================================================\n");
fprintf(stderr, "Solved by unit propagation\n");
S.printStats();
printf("\n"); }
printf("UNSATISFIABLE\n");
fprintf(stderr, "\n"); }
fprintf(stderr, "UNSATISFIABLE\n");
exit(20);
}

vec<Lit> dummy;
lbool ret = S.solveLimited(dummy);
if (S.verbosity > 0){
S.printStats();
printf("\n"); }
printf(ret == l_True ? "SATISFIABLE\n" : ret == l_False ? "UNSATISFIABLE\n" : "INDETERMINATE\n");
fprintf(stderr, "\n"); }
fprintf(stderr, ret == l_True ? "SATISFIABLE\n" : ret == l_False ? "UNSATISFIABLE\n" : "INDETERMINATE\n");
if (res != NULL){
if (ret == l_True){
fprintf(res, "SAT\n");
Expand All @@ -146,8 +156,8 @@ int main(int argc, char** argv)
return (ret == l_True ? 10 : ret == l_False ? 20 : 0);
#endif
} catch (OutOfMemoryException&){
printf("===============================================================================\n");
printf("INDETERMINATE\n");
fprintf(stderr, "===============================================================================\n");
fprintf(stderr, "INDETERMINATE\n");
exit(0);
}
}
30 changes: 15 additions & 15 deletions minisat/core/Solver.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -737,7 +737,7 @@ lbool Solver::search(int nof_conflicts)
max_learnts *= learntsize_inc;

if (verbosity >= 1)
printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n",
fprintf(stderr, "| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n",
(int)conflicts,
(int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals,
(int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100);
Expand Down Expand Up @@ -853,10 +853,10 @@ lbool Solver::solve_()
lbool status = l_Undef;

if (verbosity >= 1){
printf("============================[ Search Statistics ]==============================\n");
printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n");
printf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | |\n");
printf("===============================================================================\n");
fprintf(stderr, "============================[ Search Statistics ]==============================\n");
fprintf(stderr, "| Conflicts | ORIGINAL | LEARNT | Progress |\n");
fprintf(stderr, "| | Vars Clauses Literals | Limit Clauses Lit/Cl | |\n");
fprintf(stderr, "===============================================================================\n");
}

// Search:
Expand All @@ -869,7 +869,7 @@ lbool Solver::solve_()
}

if (verbosity >= 1)
printf("===============================================================================\n");
fprintf(stderr, "===============================================================================\n");


if (status == l_True){
Expand Down Expand Up @@ -984,21 +984,21 @@ void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
toDimacs(f, ca[clauses[i]], map, max);

if (verbosity > 0)
printf("Wrote DIMACS with %d variables and %d clauses.\n", max, cnt);
fprintf(stderr, "Wrote DIMACS with %d variables and %d clauses.\n", max, cnt);
}


void Solver::printStats() const
{
double cpu_time = cpuTime();
double mem_used = memUsedPeak();
printf("restarts : %"PRIu64"\n", starts);
printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", conflicts , conflicts /cpu_time);
printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions /cpu_time);
printf("propagations : %-12"PRIu64" (%.0f /sec)\n", propagations, propagations/cpu_time);
printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals);
if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used);
printf("CPU time : %g s\n", cpu_time);
fprintf(stderr, "restarts : %"PRIu64"\n", starts);
fprintf(stderr, "conflicts : %-12"PRIu64" (%.0f /sec)\n", conflicts , conflicts /cpu_time);
fprintf(stderr, "decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions /cpu_time);
fprintf(stderr, "propagations : %-12"PRIu64" (%.0f /sec)\n", propagations, propagations/cpu_time);
fprintf(stderr, "conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals);
if (mem_used != 0) fprintf(stderr, "Memory used : %.2f MB\n", mem_used);
fprintf(stderr, "CPU time : %g s\n", cpu_time);
}


Expand Down Expand Up @@ -1060,7 +1060,7 @@ void Solver::garbageCollect()

relocAll(to);
if (verbosity >= 2)
printf("| Garbage collection: %12d bytes => %12d bytes |\n",
fprintf(stderr, "| Garbage collection: %12d bytes => %12d bytes |\n",
ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
to.moveTo(ca);
}
54 changes: 32 additions & 22 deletions minisat/simp/Main.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,10 +41,10 @@ static void SIGINT_interrupt(int) { solver->interrupt(); }
// destructors and may cause deadlocks if a malloc/free function happens to be running (these
// functions are guarded by locks for multithreaded use).
static void SIGINT_exit(int) {
printf("\n"); printf("*** INTERRUPTED ***\n");
fprintf(stderr, "\n"); fprintf(stderr, "*** INTERRUPTED ***\n");
if (solver->verbosity > 0){
solver->printStats();
printf("\n"); printf("*** INTERRUPTED ***\n"); }
fprintf(stderr, "\n"); fprintf(stderr, "*** INTERRUPTED ***\n"); }
_exit(1); }


Expand Down Expand Up @@ -86,27 +86,37 @@ int main(int argc, char** argv)
if (mem_lim != 0) limitMemory(mem_lim);

if (argc == 1)
printf("Reading from standard input... Use '--help' for help.\n");
fprintf(stderr, "Reading from standard input... Use '--help' for help.\n");

gzFile in;
bool is_stdin = false;
if (argc == 1 || strcmp(argv[1], "-") == 0) {
in = gzdopen(0, "rb");
is_stdin = true;
}
else
in = gzopen(argv[1], "rb");

gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb");
if (in == NULL)
printf("ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : argv[1]), exit(1);
fprintf(stderr, "ERROR! Could not open file: %s\n", is_stdin ? "<stdin>" : argv[1]), exit(1);

if (S.verbosity > 0){
printf("============================[ Problem Statistics ]=============================\n");
printf("| |\n"); }
fprintf(stderr, "============================[ Problem Statistics ]=============================\n");
fprintf(stderr, "| |\n"); }

parse_DIMACS(in, S, (bool)strictp);
gzclose(in);
FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL;
FILE* res = NULL;
if (argc >= 3)
res = (strcmp(argv[2], "-") == 0) ? stdout : fopen(argv[2], "wb");

if (S.verbosity > 0){
printf("| Number of variables: %12d |\n", S.nVars());
printf("| Number of clauses: %12d |\n", S.nClauses()); }
fprintf(stderr, "| Number of variables: %12d |\n", S.nVars());
fprintf(stderr, "| Number of clauses: %12d |\n", S.nClauses()); }

double parsed_time = cpuTime();
if (S.verbosity > 0)
printf("| Parse time: %12.2f s |\n", parsed_time - initial_time);
fprintf(stderr, "| Parse time: %12.2f s |\n", parsed_time - initial_time);

// Change to signal-handlers that will only notify the solver and allow it to terminate
// voluntarily:
Expand All @@ -115,17 +125,17 @@ int main(int argc, char** argv)
S.eliminate(true);
double simplified_time = cpuTime();
if (S.verbosity > 0){
printf("| Simplification time: %12.2f s |\n", simplified_time - parsed_time);
printf("| |\n"); }
fprintf(stderr, "| Simplification time: %12.2f s |\n", simplified_time - parsed_time);
fprintf(stderr, "| |\n"); }

if (!S.okay()){
if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res);
if (S.verbosity > 0){
printf("===============================================================================\n");
printf("Solved by simplification\n");
fprintf(stderr, "===============================================================================\n");
fprintf(stderr, "Solved by simplification\n");
S.printStats();
printf("\n"); }
printf("UNSATISFIABLE\n");
fprintf(stderr, "\n"); }
fprintf(stderr, "UNSATISFIABLE\n");
exit(20);
}

Expand All @@ -135,15 +145,15 @@ int main(int argc, char** argv)
vec<Lit> dummy;
ret = S.solveLimited(dummy);
}else if (S.verbosity > 0)
printf("===============================================================================\n");
fprintf(stderr, "===============================================================================\n");

if (dimacs && ret == l_Undef)
S.toDimacs((const char*)dimacs);

if (S.verbosity > 0){
S.printStats();
printf("\n"); }
printf(ret == l_True ? "SATISFIABLE\n" : ret == l_False ? "UNSATISFIABLE\n" : "INDETERMINATE\n");
fprintf(stderr, "\n"); }
fprintf(stderr, ret == l_True ? "SATISFIABLE\n" : ret == l_False ? "UNSATISFIABLE\n" : "INDETERMINATE\n");
if (res != NULL){
if (ret == l_True){
fprintf(res, "SAT\n");
Expand All @@ -164,8 +174,8 @@ int main(int argc, char** argv)
return (ret == l_True ? 10 : ret == l_False ? 20 : 0);
#endif
} catch (OutOfMemoryException&){
printf("===============================================================================\n");
printf("INDETERMINATE\n");
fprintf(stderr, "===============================================================================\n");
fprintf(stderr, "INDETERMINATE\n");
exit(0);
}
}
14 changes: 7 additions & 7 deletions minisat/simp/SimpSolver.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -130,7 +130,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
if (result == l_True)
result = Solver::solve_();
else if (verbosity >= 1)
printf("===============================================================================\n");
fprintf(stderr, "===============================================================================\n");

if (result == l_True && extend_model)
extendModel();
Expand Down Expand Up @@ -366,7 +366,7 @@ bool SimpSolver::backwardSubsumptionCheck(bool verbose)
if (c.mark()) continue;

if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)
printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);
fprintf(stderr, "subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);

assert(c.size() > 1 || value(c[0]) == l_True); // Unit-clauses should have been propagated before this point.

Expand Down Expand Up @@ -604,7 +604,7 @@ bool SimpSolver::eliminate(bool turn_off_elim)
while (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0){

gatherTouchedClauses();
// printf(" ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
// fprintf(stderr, " ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) &&
!backwardSubsumptionCheck(true)){
ok = false; goto cleanup; }
Expand All @@ -617,7 +617,7 @@ bool SimpSolver::eliminate(bool turn_off_elim)
elim_heap.clear();
goto cleanup; }

// printf(" ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
// fprintf(stderr, " ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
for (int cnt = 0; !elim_heap.empty(); cnt++){
Var elim = elim_heap.removeMin();

Expand All @@ -626,7 +626,7 @@ bool SimpSolver::eliminate(bool turn_off_elim)
if (isEliminated(elim) || value(elim) != l_Undef) continue;

if (verbosity >= 2 && cnt % 100 == 0)
printf("elimination left: %10d\r", elim_heap.size());
fprintf(stderr, "elimination left: %10d\r", elim_heap.size());

if (use_asymm){
// Temporarily freeze variable. Otherwise, it would immediately end up on the queue again:
Expand Down Expand Up @@ -670,7 +670,7 @@ bool SimpSolver::eliminate(bool turn_off_elim)
}

if (verbosity >= 1 && elimclauses.size() > 0)
printf("| Eliminated clauses: %10.2f Mb |\n",
fprintf(stderr, "| Eliminated clauses: %10.2f Mb |\n",
double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));

return ok;
Expand Down Expand Up @@ -719,7 +719,7 @@ void SimpSolver::garbageCollect()
relocAll(to);
Solver::relocAll(to);
if (verbosity >= 2)
printf("| Garbage collection: %12d bytes => %12d bytes |\n",
fprintf(stderr, "| Garbage collection: %12d bytes => %12d bytes |\n",
ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
to.moveTo(ca);
}
4 changes: 3 additions & 1 deletion minisat/utils/Options.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,10 +39,12 @@ void Minisat::parseOptions(int& argc, char** argv, bool strict)
for (int k = 0; !parsed_ok && k < Option::getOptionList().size(); k++){
parsed_ok = Option::getOptionList()[k]->parse(argv[i]);

// fprintf(stderr, "checking %d: %s against flag <%s> (%s)\n", i, argv[i], Option::getOptionList()[k]->name, parsed_ok ? "ok" : "skip");
//fprintf(stderr, "checking %d: %s against flag <%s> (%s)\n", i, argv[i], Option::getOptionList()[k]->name, parsed_ok ? "ok" : "skip");
}

if (!parsed_ok){
if (strcmp(argv[i], "-") == 0)
break;
if (strict && match(argv[i], "-"))
fprintf(stderr, "ERROR! Unknown flag \"%s\". Use '--%shelp' for help.\n", argv[i], Option::getHelpPrefixString()), exit(1);
else
Expand Down
Loading