summaryrefslogtreecommitdiff
path: root/src/prop/bvpicosat/picomus.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/bvpicosat/picomus.c')
-rw-r--r--src/prop/bvpicosat/picomus.c340
1 files changed, 0 insertions, 340 deletions
diff --git a/src/prop/bvpicosat/picomus.c b/src/prop/bvpicosat/picomus.c
deleted file mode 100644
index bf98dc644..000000000
--- a/src/prop/bvpicosat/picomus.c
+++ /dev/null
@@ -1,340 +0,0 @@
-/****************************************************************************
-Copyright (c) 2010, Armin Biere, Johannes Kepler University.
-
-Permission is hereby granted, free of charge, to any person obtaining a copy
-of this software and associated documentation files (the "Software"), to
-deal in the Software without restriction, including without limitation the
-rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
-sell copies of the Software, and to permit persons to whom the Software is
-furnished to do so, subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in
-all copies or substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
-FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
-AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
-LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
-IN THE SOFTWARE.
-****************************************************************************/
-
-#include "picosat.h"
-
-#include <stdio.h>
-#include <assert.h>
-#include <string.h>
-#include <stdarg.h>
-#include <ctype.h>
-
-#define MAXNONREDROUNDS 3
-#define MINCOREROUNDS 5
-#define MAXCOREROUNDS 100
-
-typedef struct Cls { int lit, red, * lits; } Cls;
-
-static int verbose;
-static int fclose_input, pclose_input, close_output;
-static FILE * input_file, * output_file;
-static const char * input_name, * output_name;
-static int lineno = 1;
-static int nvars, nclauses;
-static Cls * clauses;
-static int * lits, nlits, szlits;
-static double start;
-static int reductions;
-
-static int next (void) {
- int res = fgetc (input_file);
- if (res == '\n') lineno++;
- return res;
-}
-
-static void msg (const char * fmt, ...) {
- va_list ap;
- if (!verbose) return;
- fputs ("c [picomus] ", stderr);
- va_start (ap, fmt);
- vfprintf (stderr, fmt, ap);
- va_end (ap);
- fputc ('\n', stderr);
- fflush (stderr);
-}
-
-static const char * parse (void) {
- int ch, n, lit, sign, i;
- Cls * c;
-HEADER:
- ch = next ();
- if (ch == 'c') {
- while ((ch = next ()) != '\n')
- if (ch == EOF) return "EOF after 'c'";
- goto HEADER;
- }
- if (ch == '\r') goto HEADER;
- if (ch != 'p') return "expected 'c' or 'p'";
- if (fscanf (input_file, " cnf %d %d", &nvars, &nclauses) != 2)
- return "invalid header";
- msg ("p cnf %d %d", nvars, nclauses);
- clauses = calloc (nclauses, sizeof *clauses);
- lit = n = 0;
-LIT:
- ch = next ();
- if (ch == ' ' || ch == '\n' || ch == '\t' || ch == '\r') goto LIT;
- if (ch == 'c') {
- while ((ch = next ()) != '\n')
- if (ch == EOF) return "EOF after 'c'";
- goto LIT;
- }
- if (ch == EOF) {
- if (lit) return "zero missing";
- if (n < nclauses) return "clauses missing";
- return 0;
- }
- if (n == nclauses) return "too many clauses";
- if (ch == '-') {
- sign = -1;
- ch = next ();
- if (!isdigit (ch)) return "expected digit after '-'";
- } else sign = 1;
- if (!isdigit (ch)) return "expected digit";
- lit = ch - '0';
- while (isdigit (ch = next ()))
- lit = 10 * lit + (ch - '0');
- if (lit > nvars) return "maximum variable index exceeded";
- if (lit) {
- lit *= sign;
- if (nlits == szlits) {
- szlits = szlits ? 2 * szlits : 1;
- lits = realloc (lits, szlits * sizeof *lits);
- }
- lits[nlits++] = lit;
- } else {
- c = clauses + n++;
- c->lits = malloc ((nlits + 1) * sizeof *c->lits);
- for (i = 0; i < nlits; i++)
- c->lits[i] = lits[i];
- c->lits[i] = 0;
- nlits = 0;
- }
- goto LIT;
-}
-
-static void die (const char * fmt, ...) {
- va_list ap;
- fputs ("*** picomus: ", stderr);
- va_start (ap, fmt);
- vfprintf (stderr, fmt, ap);
- va_end (ap);
- fputc ('\n', stderr);
- fflush (stderr);
- exit (1);
-}
-
-static double percent (double a, double b) { return b?100.0*a/b:0.0; }
-
-static void callback (void * dummy, const int * mus) {
- int remaining;
- const int * p;
- (void) dummy;
- if (!verbose) return;
- remaining = 0;
- for (p = mus; *p; p++) remaining++;
- assert (remaining <= nclauses);
- reductions++;
- msg ("reduction %d to %d out of %d (%.0f%%) after %.1f sec",
- reductions,
- remaining, nclauses, percent (remaining, nclauses),
- picosat_time_stamp () - start);
-}
-
-int main (int argc, char ** argv) {
- int i, * p, n, oldn, red, nonred, tmp, res, round, printed, len;
- const char * err;
- const int * q;
- char * cmd;
- Cls * c;
- start = picosat_time_stamp ();
- for (i = 1; i < argc; i++) {
- if (!strcmp (argv[i], "-h")) {
- printf (
- "picomus [-v][-h][<input>[<output>]]\n"
- "\n"
- "This tool is a SAT solver that uses the PicoSAT library to\n"
- "generate a 'minimal unsatisfiable core' also known as 'minimal\n"
- "unsatisfiable set' (MUS) of a CNF in DIMACS format.\n"
- "\n"
- "Both file argumetns can be \"-\" and then denote <stdin> resp.\n"
- "<stdout>. If no input file is given <stdin> is used. If no\n"
- "output file is specified the MUS is only computed, but not\n"
- "printed.\n"
- "\n"
- "Otherwise the output conforms to the standard SAT solver\n"
- "format used at SAT competitions.\n"
- "\n"
-#ifndef TRACE
- "WARNING: PicosSAT is compiled without trace support.\n"
- "\n"
- "This typically slows down this MUS extractor, since\n"
- "it only relies on clause selector variables and\n"
- "can not make use of core extraction. To enable\n"
- "trace generation use './configure --trace' or\n"
- "'./configure -O --trace' when building PicoSAT.\n"
-#else
- "Since trace generation code is included, this binary\n"
- "uses both core extraction and clause selector variables.\n"
-#endif
- );
- exit (0);
- } else if (!strcmp (argv[i], "-v")) verbose++;
- else if (output_name) die ("too many arguments");
- else if (!input_name) input_name = argv[i];
- else output_name = argv[i];
- }
- if (input_name && strcmp (input_name, "-")) {
- len = strlen (input_name);
- if (len >= 3 && !strcmp (input_name + len - 3, ".gz")) {
- cmd = malloc (len + 20);
- sprintf (cmd, "gunzip -c %s 2>/dev/null", input_name);
- input_file = popen (cmd, "r");
- pclose_input = 1;
- free (cmd);
- } else input_file = fopen (input_name, "r"), fclose_input = 1;
- if (!input_file) die ("can not read '%s'", input_name);
- } else input_file = stdin, input_name = "-";
- if ((err = parse ())) {
- fprintf (stderr, "%s:%d: %s\n", input_name, lineno, err);
- fflush (stderr);
- exit (1);
- }
- if (fclose_input) fclose (input_file);
- if (pclose_input) pclose (input_file);
- picosat_init ();
- picosat_set_prefix ("c [picosat] ");
- picosat_set_output (stderr);
- if (verbose > 1) picosat_set_verbosity (verbose - 1);
- printed = 0;
- if (picosat_enable_trace_generation ()) {
- n = nclauses;
- nonred = 0;
- for (round = 1; round <= MAXCOREROUNDS; round++) {
- if (verbose > 1)
- msg ("starting core extraction round %d", round);
- picosat_set_seed (round);
- for (i = 0; i < nclauses; i++) {
- c = clauses + i;
- if (c->red) {
- picosat_add (1);
- picosat_add (-1);
- } else {
- for (p = c->lits; *p; p++)
- picosat_add (*p);
- }
- tmp = picosat_add (0);
- assert (tmp == i);
- }
- res = picosat_sat (-1);
- if (res == 10) { assert (round == 1); goto SAT; }
- assert (res == 20);
- if (!printed) {
- assert (round == 1);
- printed = 1;
- printf ("s UNSATISFIABLE\n");
- fflush (stdout);
- }
- for (i = 0; i < nclauses; i++) {
- c = clauses + i;
- if (c->red) { assert (!picosat_coreclause (i)); continue; }
- if (picosat_coreclause (i)) continue;
- c->red = 1;
- }
- oldn = n;
- n = 0;
- for (i = 0; i < nclauses; i++) if (!clauses[i].red) n++;
- msg ("extracted core %d of size %d out of %d (%.0f%%) after %.1f sec",
- round, n, nclauses, percent (n, nclauses),
- picosat_time_stamp () - start);
- assert (oldn >= n);
- picosat_reset ();
- picosat_init ();
- picosat_set_prefix ("c [picosat] ");
- picosat_set_output (stderr);
- if (round >= MINCOREROUNDS) {
- red = oldn - n;
- if (red < 10 && (100*red + 99)/oldn < 2) {
- nonred++;
- if (nonred > MAXNONREDROUNDS) break;
- }
- }
- if (round < MAXCOREROUNDS) picosat_enable_trace_generation ();
- }
- }
- for (i = 0; i < nclauses; i++) {
- c = clauses + i;
- if (c->red) {
- picosat_add (1);
- picosat_add (-1);
- tmp = picosat_add (0);
- assert (tmp == i);
- continue;
- }
- c->lit = nvars + i + 1;
- picosat_add (-c->lit);
- for (p = c->lits; *p; p++)
- (void) picosat_add (*p);
- tmp = picosat_add (0);
- assert (tmp == i);
- }
- for (i = 0; i < nclauses; i++) {
- c = clauses + i;
- if (c->red) continue;
- picosat_assume (c->lit);
- }
- res = picosat_sat (-1);
- if (res == 20) {
- if (!printed) printf ("s UNSATISFIABLE\n"), fflush (stdout);
- for (i = 0; i < nclauses; i++) clauses[i].red = 1;
- q = picosat_mus_assumptions (0, callback, 1);
- while ((i = *q++)) {
- i -= nvars + 1;
- assert (0 <= i && i < nclauses);
- clauses[i].red = 0;
- }
- } else {
-SAT:
- assert (res == 10);
- printf ("s SATISFIABLE\n"); fflush (stdout);
- for (i = 1; i <= nvars; i++)
- printf ("v %d\n", ((picosat_deref (i) < 0) ? -1 : 1) * i);
- printf ("v 0\n");
- }
- if (verbose) picosat_stats ();
- picosat_reset ();
- n = 0;
- for (i = 0; i < nclauses; i++) if (!clauses[i].red) n++;
- red = nclauses - n;
- msg ("found %d redundant clauses %.0f%%", red, percent (red, nclauses));
- if (output_name && strcmp (output_name, "-")) {
- output_file = fopen (output_name, "w");
- if (!output_file) die ("can not write '%s'", output_name);
- close_output = 1;
- } else if (output_name && !strcmp (output_name, "-")) output_file = stdout;
- if (output_file) {
- fprintf (output_file, "p cnf %d %d\n", nvars, n);
- for (i = 0; i < nclauses; i++)
- if (!clauses[i].red) {
- for (p = clauses[i].lits; *p; p++) fprintf (output_file, "%d ", *p);
- fprintf (output_file, "0\n");
- }
- if (close_output) fclose (output_file);
- }
- msg ("%s %d irredundant clauses %.0f%%",
- output_file ? "printed" : "computed", n, percent (n, nclauses));
- for (i = 0; i < nclauses; i++) free (clauses[i].lits);
- free (clauses);
- free (lits);
- msg ("%d reductions in %.1f seconds",
- reductions, picosat_time_stamp () - start);
- return res;
-}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback