diff options
Diffstat (limited to 'test/monniaux/picosat-965/picomcs.c')
| -rw-r--r-- | test/monniaux/picosat-965/picomcs.c | 334 |
1 files changed, 334 insertions, 0 deletions
diff --git a/test/monniaux/picosat-965/picomcs.c b/test/monniaux/picosat-965/picomcs.c new file mode 100644 index 00000000..3acf7bd7 --- /dev/null +++ b/test/monniaux/picosat-965/picomcs.c @@ -0,0 +1,334 @@ +#include <assert.h> +#include <stdlib.h> +#include <stdio.h> +#include <stdarg.h> +#include <ctype.h> +#include <string.h> +#include <unistd.h> + +#include "picosat.h" + +typedef struct Clause { int cid, * lits; struct Clause * next; } Clause; +typedef struct MCS { int mid, * clauses; struct MCS * next; } MCS; + +static int nvars; +static char * marked; + +static Clause * first_clause, * last_clause; +static int nclauses, first_cid, last_cid; + +static MCS * first_mcs, * last_mcs; +static int nmcs; + +static int * stk, szstk, nstk; + +static int verbose, join, noprint; + +static int lineno = 1, close_input; +static const char * input_name; +static FILE * input; + +static PicoSAT * ps; + +static void release_clauses (void) { + Clause * p, * next; + for (p = first_clause; p; p = next) { + next = p->next; + free (p->lits); + free (p); + } +} + +static void release_mss (void) { + MCS * p, * next; + for (p = first_mcs; p; p = next) { + next = p->next; + free (p->clauses); + free (p); + } +} + +static void release (void) { + release_clauses (); + release_mss (); + free (marked); + free (stk); +} + +static void push_stack (int n) { + if (nstk == szstk) + stk = realloc (stk, (szstk = szstk ? 2*szstk : 1) * sizeof *stk); + stk[nstk++] = n; +} + +static void push_clause (void) { + Clause * clause; + size_t bytes; + clause = malloc (sizeof *clause); + clause->cid = ++nclauses; + clause->next = 0; + push_stack (0); + bytes = nstk * sizeof *clause->lits; + clause->lits = malloc (bytes); + memcpy (clause->lits, stk, bytes); + if (last_clause) last_clause->next = clause; + else first_clause = clause; + last_clause = clause; + nstk = 0; +} + +static void push_mcs (void) { + MCS * mcs; + size_t bytes; + mcs = malloc (sizeof *mcs); + mcs->mid = ++nmcs; + mcs->next = 0; + push_stack (0); + bytes = nstk * sizeof *mcs->clauses; + mcs->clauses = malloc (bytes); + memcpy (mcs->clauses, stk, bytes); + if (last_mcs) last_mcs->next = mcs; + else first_mcs = mcs; + last_mcs = mcs; + nstk = 0; +} + +static int nextch (void) { + int res = getc (input); + if (res == '\n') lineno++; + return res; +} + +static void msg (int level, const char * fmt, ...) { + va_list ap; + if (level > verbose) return; + printf ("c [picomcs] "); + va_start (ap, fmt); + vprintf (fmt, ap); + va_end (ap); + fputc ('\n', stdout); + fflush (stdout); +} + +static const char * parse (void) { + int ch, expclauses, lit, sign; + size_t bytes; + msg (1, "parsing %s", input_name); +COMMENTS: + ch = nextch (); + if (ch == 'c') { + while ((ch = nextch ()) != '\n') + if (ch == EOF) return "out of file in comment"; + goto COMMENTS; + } + if (ch != 'p') +INVALID_HEADER: + return "invalid header"; + ungetc (ch, input); + if (fscanf (input, "p cnf %d %d", &nvars, &expclauses) != 2) + goto INVALID_HEADER; + msg (1, "found 'p cnf %d %d' header", nvars, expclauses); + bytes = (1 + nvars + expclauses) * sizeof *marked; + marked = malloc (bytes); + memset (marked, 0, bytes); +LIT: + ch = nextch (); + if (ch == ' ' || ch == '\n' || ch == '\t' || ch == '\r') goto LIT; + if (ch == EOF) { + assert (nclauses <= expclauses); + if (nclauses < expclauses) return "clauses missing"; + return 0; + } + if (ch == '-') { + ch = nextch (); + if (!isdigit (ch)) return "expected digit after '-'"; + if (ch == '0') return "expected positive digit after '-'"; + sign = -1; + } else if (!isdigit (ch)) return "expected '-' or digit"; + else sign = 1; + lit = ch - '0'; + while (isdigit (ch = nextch ())) + lit = 10*lit + (ch - '0'); + if (lit) { + if (lit > nvars) return "maximum variable index exceeded"; + if (nclauses == expclauses) return "too many clauses"; + push_stack (sign * lit); + } else { + assert (nclauses < expclauses); + push_clause (); + } + goto LIT; +} + +#ifndef NDEBUG +static void dump_clause (Clause * c) { + int * p, lit; + for (p = c->lits; (lit = *p); p++) + printf ("%d ", lit); + printf ("0\n"); +} + +void dump (void) { + Clause * p; + printf ("p cnf %d %d\n", nvars, nclauses); + for (p = first_clause; p; p = p->next) + dump_clause (p); +} +#endif + +static int clause2selvar (Clause * c) { + int res = c->cid + nvars; + assert (first_cid <= res && res <= last_cid); + return res; +} + +static void encode_clause (Clause * c) { + int * p, lit; + if (verbose >= 2) { + printf ("c [picomcs] encode clause %d :", c->cid); + printf (" %d", -clause2selvar (c)); + for (p = c->lits; (lit = *p); p++) printf (" %d", lit); + fputc ('\n', stdout), fflush (stdout); + } + picosat_add (ps, -clause2selvar (c)); + for (p = c->lits; (lit = *p); p++) picosat_add (ps, lit); + picosat_add (ps, 0); +} + +static void encode (void) { + Clause * p; + first_cid = nvars + 1; + last_cid = nvars + nclauses; + msg (2, "selector variables range %d to %d", first_cid, last_cid); + for (p = first_clause; p; p = p->next) + encode_clause (p); + msg (1, "encoded %d clauses", nclauses); +} + +static void camcs (void) { + int cid, i; + const int * mcs, * p; + msg (1, "starting to compute all minimal correcting sets"); + while ((mcs = picosat_next_minimal_correcting_subset_of_assumptions (ps))) { + for (p = mcs; (cid = *p); p++) + push_stack (cid); + if (verbose >= 2) { + printf ("c [picomcs] mcs %d :", nmcs); + for (i = 0; i < nstk; i++) printf (" %d", stk[i] - nvars); + fputc ('\n', stdout); + fflush (stdout); + } else if (verbose && isatty (1)) { + printf ("\rc [picomcs] mcs %d", nmcs); + fflush (stdout); + } + push_mcs (); + } + if (verbose && isatty (1)) fputc ('\r', stdout); + msg (1, "found %d minimal correcting sets", nmcs); +} + +static void cumcscb (void * state, int nmcs, int nhumus) { + int * ptr = state; + *ptr = nmcs; + ptr[0] = nmcs, ptr[1] = nhumus; + if (!verbose || (!isatty (1) && verbose == 1)) return; + if (verbose == 1) fputc ('\r', stdout); + printf ("c [picomcs] mcs %d humus %d", nmcs, nhumus); + if (verbose >= 2) fputc ('\n', stdout); + fflush (stdout); +} + +static void cumcs (void) { + int stats[2], count, cid; + const int * humus, * p; + stats[0] = stats[1] = 0; + humus = picosat_humus (ps, cumcscb, stats); + if (isatty (1) && verbose == 1) fputc ('\n', stdout); + count = 0; + for (p = humus; (cid = *p); p++) { + if (marked[cid]) continue; + marked[cid] = 1; + count++; + } + assert (count == stats[1]); + msg (1, + "computed union of minimal correcting sets of size %d with %d mcs", + stats[1], stats[0]); +} + +static void +print_umcs (void) { + int cid; + printf ("v"); + for (cid = first_cid; cid <= last_cid; cid++) + if (marked[cid]) + printf (" %d", cid - nvars); + printf (" 0\n"); +} + +static void +print_mcs (MCS * mcs) +{ + const int * p; + int cid; + printf ("v"); + for (p = mcs->clauses; (cid = *p); p++) + printf (" %d", cid - nvars); + printf (" 0\n"); +} + +static void +print_all_mcs (void) +{ + MCS * p; + for (p = first_mcs; p; p = p->next) + print_mcs (p); +} + +int main (int argc, char ** argv) { + const char * perr; + int i, res; + for (i = 1; i < argc; i++) { + if (!strcmp (argv[i], "-h")) { + printf ("usage: picomcs [-h][-v][-j][-n][<input>]\n"); + exit (0); + } + else if (!strcmp (argv[i], "-v")) verbose++; + else if (!strcmp (argv[i], "-j")) join = 1; + else if (!strcmp (argv[i], "-n")) noprint = 1; + else if (argv[i][0] == '-') { + fprintf (stderr, "*** picomcs: invalid option '%s'\n", argv[i]); + exit (1); + } else if (input_name) { + fprintf (stderr, "*** picomcs: two input files specified\n"); + exit (1); + } else if (!(input = fopen ((input_name = argv[i]), "r"))) { + fprintf (stderr, "*** picomcs: can not read '%s'\n", argv[i]); + exit (1); + } else close_input = 1; + } + if (!input_name) input_name = "<stdin>", input = stdin; + if ((perr = parse ())) { + fprintf (stderr, "%s:%d: parse error: %s\n", input_name, lineno, perr); + exit (1); + } + if (close_input) fclose (input); + ps = picosat_init (); + picosat_set_prefix (ps, "c [picosat] "); + encode (); + for (i = first_cid; i <= last_cid; i++) + picosat_set_default_phase_lit (ps, i, 1); + for (i = first_cid; i <= last_cid; i++) picosat_assume (ps, i); + res = picosat_sat (ps, -1); + if (res == 10) printf ("s SATISFIABLE\n"); + else printf ("s UNSATISFIABLE\n"); + fflush (stdout); + if (join) cumcs (); else camcs (); + if (verbose) picosat_stats (ps); + picosat_reset (ps); + if (!noprint) { + if (join) print_umcs (); else print_all_mcs (); + } + release (); + return res; +} |