From 4ef8259d18add24bb589a185d050f4a524385f1f Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 27 Jan 2019 16:09:47 +0100 Subject: picosat induces bug in register allocation --- test/monniaux/picosat-965/picogcnf.c | 165 +++++++++++++++++++++++++++++++++++ 1 file changed, 165 insertions(+) create mode 100644 test/monniaux/picosat-965/picogcnf.c (limited to 'test/monniaux/picosat-965/picogcnf.c') diff --git a/test/monniaux/picosat-965/picogcnf.c b/test/monniaux/picosat-965/picogcnf.c new file mode 100644 index 00000000..4d91bfae --- /dev/null +++ b/test/monniaux/picosat-965/picogcnf.c @@ -0,0 +1,165 @@ +/**************************************************************************** +Copyright (c) 2011-2012, 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 +#include +#include +#include +#include + +#if 1 +#define LOG(ARGS...) do { } while (0) +#else +#define LOG(ARGS...) do { printf (##ARGS); } while (0) +#endif + +static int reductions, ngroups; + +static PicoSAT * ps; + +static void die (const char * fmt, ...) { + va_list ap; + fprintf (stderr, "*** picogcnf: "); + va_start (ap, fmt); + vfprintf (stderr, fmt, ap); + va_end (ap); + fputc ('\n', stderr); + exit (1); +} + +static void msg (const char * fmt, ...) { + va_list ap; + printf ("c [picogcnf] %.2f seconds: ", picosat_time_stamp ()); + va_start (ap, fmt); + vprintf (fmt, ap); + va_end (ap); + fputc ('\n', stdout); + fflush (stdout); +} + +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; + remaining = 0; + for (p = mus; *p; p++) remaining++; + assert (remaining <= ngroups); + msg ("<%d> reduction to %d out of %d (%.0f%%)", + ++reductions, remaining, ngroups, percent (remaining, ngroups)); +} + +int main (int argc, char ** argv) { + int ch, nvars, sclauses, nclauses, sign, lit, group, res; + const int * mus, * p; + FILE * file; + if (argc != 2) die ("usage: picogcnf "); + if (!(file = fopen (argv[1], "r"))) die ("can not read '%s'", argv[1]); + ps = picosat_init (); +HEADER: + ch = getc (file); + if (ch == 'c') { + while ((ch = getc (file)) != '\n') + if (ch == EOF) die ("unexpected EOF"); + goto HEADER; + } + if (ch != 'p' || + getc (file) != ' ' || + fscanf (file, "gcnf %d %d %d", &nvars, &sclauses, &ngroups) != 3) + die ("invalid header"); + nclauses = lit = 0; + group = INT_MAX; + LOG ("p gcnf %d %d %d\n", nvars, sclauses, ngroups); +LIT: + ch = getc (file); + if (ch == EOF) { + if (lit) die ("zero missing"); + if (nclauses < sclauses) die ("clauses missing"); + goto DONE; + } + if (ch == ' ' || ch == '\t' || ch == '\n' || ch == '\r') goto LIT; + if (lit) { + if (ch == '-') { + sign = -1; + ch = getc (file); + } else sign = 1; + lit = ch - '0'; + while (isdigit (ch = getc (file))) + lit = 10 * lit + ch - '0'; + if (lit > nvars) die ("maximum variable exceeded"); + lit *= sign; + if (lit) { + LOG ("%d ", lit); + } else { + LOG ("0\n"); + group = INT_MAX; + nclauses++; + } + picosat_add (ps, lit); + } else if (ch == '{') { + if (nclauses == sclauses) die ("too many clauses"); + if (group < INT_MAX) die ("multiple groups per clause"); +GROUP: + ch = getc (file); + if (ch == ' ' || ch == '\t' || ch == '\n' || ch == '\r') goto GROUP; + if (!isdigit (ch)) die ("group does not start with digit"); + group = ch - '0'; + while (isdigit (ch = getc (file))) + group = 10 * group + (ch - '0'); + if (group > ngroups) die ("maximal group exceeded"); + while (ch == ' ' || ch == '\t' || ch == '\n' || ch == '\r') + ch = getc (file); + if (ch != '}') die ("expected '}'"); + LOG ("{%d} ", group); + if (group) picosat_add (ps, -(nvars + group)); + lit = INT_MAX; + } else die ("expected '{'"); + goto LIT; +DONE: + fclose (file); + for (lit = nvars + 1; lit <= nvars + ngroups; lit++) picosat_assume (ps, lit); + res = picosat_sat (ps, -1); + msg ("first call to SAT solver returned"); + if (res == 10) printf ("s SATISFIABLE\n"); + else if (res == 20) printf ("s UNSATISFIABLE\n"); + else printf ("s UNKNOWN\n"); + fflush (stdout); + if (res == 20) { + mus = picosat_mus_assumptions (ps, 0, callback, 1); + assert (mus); + printf ("v"); + for (p = mus; (lit = *p); p++) { + assert (nvars + 1 <= lit && lit <= nvars + ngroups); + printf (" %d", lit - nvars); + } + printf (" 0\n"); + fflush (stdout); + } + msg ("max memory %.1f MB", + picosat_max_bytes_allocated (ps) / (double)(1<<20)); + picosat_reset (ps); + msg ("%d reductions", reductions); + return res; +} -- cgit