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/LICENSE | 20 + test/monniaux/picosat-965/NEWS | 162 + test/monniaux/picosat-965/README | 5 + test/monniaux/picosat-965/VERSION | 1 + test/monniaux/picosat-965/app.c | 1210 ++++ test/monniaux/picosat-965/configure.sh | 150 + test/monniaux/picosat-965/dm_configure.sh | 1 + test/monniaux/picosat-965/main.c | 7 + test/monniaux/picosat-965/make.log | 554 ++ test/monniaux/picosat-965/makefile.in | 59 + test/monniaux/picosat-965/mkconfig.sh | 35 + test/monniaux/picosat-965/picogcnf.c | 165 + test/monniaux/picosat-965/picomcs.c | 334 ++ test/monniaux/picosat-965/picomus.c | 407 ++ test/monniaux/picosat-965/picosat.c | 8506 +++++++++++++++++++++++++++++ test/monniaux/picosat-965/picosat.h | 658 +++ test/monniaux/picosat-965/version.c | 14 + 17 files changed, 12288 insertions(+) create mode 100644 test/monniaux/picosat-965/LICENSE create mode 100644 test/monniaux/picosat-965/NEWS create mode 100644 test/monniaux/picosat-965/README create mode 100644 test/monniaux/picosat-965/VERSION create mode 100644 test/monniaux/picosat-965/app.c create mode 100755 test/monniaux/picosat-965/configure.sh create mode 100755 test/monniaux/picosat-965/dm_configure.sh create mode 100644 test/monniaux/picosat-965/main.c create mode 100644 test/monniaux/picosat-965/make.log create mode 100644 test/monniaux/picosat-965/makefile.in create mode 100755 test/monniaux/picosat-965/mkconfig.sh create mode 100644 test/monniaux/picosat-965/picogcnf.c create mode 100644 test/monniaux/picosat-965/picomcs.c create mode 100644 test/monniaux/picosat-965/picomus.c create mode 100644 test/monniaux/picosat-965/picosat.c create mode 100644 test/monniaux/picosat-965/picosat.h create mode 100644 test/monniaux/picosat-965/version.c (limited to 'test/monniaux/picosat-965') diff --git a/test/monniaux/picosat-965/LICENSE b/test/monniaux/picosat-965/LICENSE new file mode 100644 index 00000000..96739de2 --- /dev/null +++ b/test/monniaux/picosat-965/LICENSE @@ -0,0 +1,20 @@ +Copyright (c) 2006 - 2014, 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. + diff --git a/test/monniaux/picosat-965/NEWS b/test/monniaux/picosat-965/NEWS new file mode 100644 index 00000000..7ad60b53 --- /dev/null +++ b/test/monniaux/picosat-965/NEWS @@ -0,0 +1,162 @@ +news for release 965 since 959 +------------------------------ + +* ADC code works again (spotted by Himanshu Jain) +* include into R projects (with Christoph Muessel) (--rcode) +* fixed 'undefined' + 'ptrdiff_' issues (thanks to Christoph Muessel) +* added 'picosat_set_interrupt' and '-a ' command line option +* fixed various issues pointed out by Stefan Hengelein: + - fixed incremental usage of 'picosat_adjust' + - added CPP fixes (STATS, NO_BINARY_CLAUSE versus TRACE mix-ups) + - removed redundant explicit set to zero on reset +* fixed various usage bugs with 'picomus' (thanks to Stefan Hengelein) +* removed '-fno-strict-aliasing' (thanks to Jerry James) + +news for release 959 since 953 +------------------------------ + +* fixed header comments + +* fixed minor compilation issues + +* fixed unitialized memory access problem for 'picosat_deref_partial' + and another issue with partial models + +* added 'picosat_add_arg' and 'picosat_add_lits' + +* '--plain' and 'picosat_set_plain' to disable failed literal probing + +* new '#define PICOSAT_REENTRANT_API' in 'picosat.h' + +* added manager so no more global variables + (allows multiple instances, requires manager object) + +news for release 951 since 941 +------------------------------ + +* cleaned up code (based on comments by Donald Knuth) + +* lreduce=O(conflicts^.5) + +* added 'picosat_visits' and 'picosat_decisions' + +* added '--partial' command line option + +* added 'picosat_deref_partial' and 'picosat_save_original_clauses' + +* added 'picomcs' as example for MSS computation + +news for release 941 since 936 +------------------------------ + +* added 'picogcnf' + +* added All-SAT mode ('--all' command line option) + +* statistics include time spent in failed literal preprocessing (probing) + +* 'picosat_failed_context' for 'push & pop' + (and tested failed assumptions for 'push & pop') + +* 'picosat_simplify' for forced garbage collection + +* undefined NFL, defined NADC (= failed literals on, ADC's off) + +* 'picosat_push' and 'picosat_pop' (beta version) + +* fixed some issues related to binary clause handling and + generating list of failed assumptions + +news for release 936 since 935 +------------------------------ + +* simple minimal unsatisfiable core (MUS) extractor 'picomus' + (example for using 'picosat_mus_assumptions' and 'picosat_coreclause') + +* added 'picosat_mus_assumptions' + +* added 'picosat_{set_}propagations' + +* new 'int' return value for 'picosat_enable_trace_generation' to + check for trace code being compiled + +news for release 935 since 926 +------------------------------ + +* added 'picosat_failed_assumptions' (plural) + +* new '-A ' command line option + +* fixed failed assumption issues + +* added 'picosat_remove_learned' + +* added 'picosat_reset_{phases,scores}' + +* added 'picosat_set_less_important_lit' + +* added 'picosat_res' + +news for release 926 since 846 +------------------------------ + +* random initial phase (API of 'picosat_set_default_phase' changed) + +* fixed accumulative failed assumption (multiple times) + +* fixed missing original clause in core generation with assumptions + +* fixed debugging code for memory allocation + +* shared library in addition to static library + +* removed potential UNKNOWN result without decision limit + +* added picosat_set_more_important_lit + +* added picosat_coreclause + +* propagation of binary clauses until completion + +* fixed API usage 'assume;sat;sat' + +* literals move to front (LMTF) during traversal of visited clauses + +* switched from inner/outer to Luby style restart scheduling + +* less agressive reduce schedule + +* replaced watched literals with head and tail pointers + +* add 'picosat_failed_assumption', which allows to avoid tracing and core + generation, if one is only interested in assumptions in the core + +* fixed a BUG in the generic iterator code of clauses + (should rarely happen unless you use a very sophisticated malloc lib) + +news for release 846 since 632 +------------------------------ + +* cleaned up assumption handling (actually removed buggy optimization) + +* incremental core generation + +* experimental 'all different constraint' handling as in our FMCAD'08 paper + +* new API calls: + + - picosat_add_ado_lit (add all different object literal) + - picosat_deref_top_level (deref top level assignment) + - picosat_changed (check whether extension was possible) + - picosat_measure_all_calls (per default do not measure adding time) + - picosat_set_prefix (set prefix for messages) + +* 64 bit port (and compilation options) + +* optional NVSIDS visualization code + +* resource controlled failed literal implementation + +* disconnect long clauses satisfied at lower decision level + +* controlling restarts diff --git a/test/monniaux/picosat-965/README b/test/monniaux/picosat-965/README new file mode 100644 index 00000000..05b84396 --- /dev/null +++ b/test/monniaux/picosat-965/README @@ -0,0 +1,5 @@ +These are the sources of the PicoSAT solver. +The preprocessor is not included. +To compile run './configure.sh && make'. +The API is document in 'picosat.h'. +See also 'NEWS' and 'LICENSE'. diff --git a/test/monniaux/picosat-965/VERSION b/test/monniaux/picosat-965/VERSION new file mode 100644 index 00000000..aa5bea4e --- /dev/null +++ b/test/monniaux/picosat-965/VERSION @@ -0,0 +1 @@ +965 diff --git a/test/monniaux/picosat-965/app.c b/test/monniaux/picosat-965/app.c new file mode 100644 index 00000000..19409b61 --- /dev/null +++ b/test/monniaux/picosat-965/app.c @@ -0,0 +1,1210 @@ +#include "picosat.h" + +#include +#include +#include +#include +#include +#include +#include + +#define GUNZIP "gunzip -c %s" +#define BUNZIP2 "bzcat %s" +#define GZIP "gzip -c -f > %s" + +#define NALARM + +FILE * popen (const char *, const char*); +int pclose (FILE *); + +static PicoSAT * picosat; + +static int lineno; +static FILE *input; +static int inputid; +static FILE *output; +static int verbose; +static int sargc; +static char ** sargv; +static char buffer[100]; +static char *bhead = buffer; +static const char *eob = buffer + 80; +static FILE * incremental_rup_file; +static signed char * sol; + +extern void picosat_enter (PicoSAT *); +extern void picosat_leave (PicoSAT *); + +static int +next (void) +{ + int res = getc (input); + if (res == '\n') + lineno++; + + return res; +} + +static const char * +parse (PicoSAT * picosat, int force) +{ + int ch, sign, lit, vars, clauses; + + lineno = 1; + inputid = fileno (input); + +SKIP_COMMENTS: + ch = next (); + if (ch == 'c') + { + while ((ch = next ()) != EOF && ch != '\n') + ; + goto SKIP_COMMENTS; + } + + if (isspace (ch)) + goto SKIP_COMMENTS; + + if (ch != 'p') +INVALID_HEADER: + return "missing or invalid 'p cnf ' header"; + + if (!isspace (next ())) + goto INVALID_HEADER; + + while (isspace (ch = next ())) + ; + + if (ch != 'c' || next () != 'n' || next () != 'f' || !isspace (next ())) + goto INVALID_HEADER; + + while (isspace (ch = next ())) + ; + + if (!isdigit (ch)) + goto INVALID_HEADER; + + vars = ch - '0'; + while (isdigit (ch = next ())) + vars = 10 * vars + (ch - '0'); + + if (!isspace (ch)) + goto INVALID_HEADER; + + while (isspace (ch = next ())) + ; + + if (!isdigit (ch)) + goto INVALID_HEADER; + + clauses = ch - '0'; + while (isdigit (ch = next ())) + clauses = 10 * clauses + (ch - '0'); + + if (!isspace (ch) && ch != '\n' ) + goto INVALID_HEADER; + + if (verbose) + { + fprintf (output, "c parsed header 'p cnf %d %d'\n", vars, clauses); + fflush (output); + } + + picosat_adjust (picosat, vars); + + if (incremental_rup_file) + picosat_set_incremental_rup_file (picosat, incremental_rup_file, vars, clauses); + + lit = 0; +READ_LITERAL: + ch = next (); + + if (ch == 'c') + { + while ((ch = next ()) != EOF && ch != '\n') + ; + goto READ_LITERAL; + } + + if (ch == EOF) + { + if (lit) + return "trailing 0 missing"; + + if (clauses && !force) + return "clause missing"; + + return 0; + } + + if (isspace (ch)) + goto READ_LITERAL; + + sign = 1; + if (ch == '-') + { + sign = -1; + ch = next (); + } + + if (!isdigit (ch)) + return "expected number"; + + lit = ch - '0'; + while (isdigit (ch = next ())) + lit = 10 * lit + (ch - '0'); + + if (!clauses && !force) + return "too many clauses"; + + if (lit) + { + if (lit > vars && !force) + return "maximal variable index exceeded"; + + lit *= sign; + } + else + clauses--; + + picosat_add (picosat, lit); + + goto READ_LITERAL; +} + +static void +bflush (void) +{ + *bhead = 0; + fputs (buffer, output); + fputc ('\n', output); + bhead = buffer; +} + +static void +printi (int i) +{ + char *next; + int l; + +REENTER: + if (bhead == buffer) + *bhead++ = 'v'; + + l = sprintf (bhead, " %d", i); + next = bhead + l; + + if (next >= eob) + { + bflush (); + goto REENTER; + } + else + bhead = next; +} + +static void +printa (PicoSAT * picosat, int partial) +{ + int max_idx = picosat_variables (picosat), i, lit, val; + + assert (bhead == buffer); + + for (i = 1; i <= max_idx; i++) + { + if (partial) + { + val = picosat_deref_partial (picosat, i); + if (!val) + continue; + } + else + val = picosat_deref (picosat, i); + lit = (val > 0) ? i : -i; + printi (lit); + } + + printi (0); + if (bhead > buffer) + bflush (); +} + +static void +blocksol (PicoSAT * picosat) +{ + int max_idx = picosat_variables (picosat), i; + + if (!sol) + { + sol = malloc (max_idx + 1); + memset (sol, 0, max_idx + 1); + } + + for (i = 1; i <= max_idx; i++) + sol[i] = (picosat_deref (picosat, i) > 0) ? 1 : -1; + + for (i = 1; i <= max_idx; i++) + picosat_add (picosat, (sol[i] < 0) ? i : -i); + + picosat_add (picosat, 0); +} + +static int +has_suffix (const char *str, const char *suffix) +{ + const char *tmp = strstr (str, suffix); + if (!tmp) + return 0; + + return str + strlen (str) - strlen (suffix) == tmp; +} + +static void +write_core_variables (PicoSAT * picosat, FILE * file) +{ + int i, max_idx = picosat_variables (picosat), count = 0; + for (i = 1; i <= max_idx; i++) + if (picosat_corelit (picosat, i)) + { + fprintf (file, "%d\n", i); + count++; + } + + if (verbose) + fprintf (output, "c found and wrote %d core variables\n", count); +} + +static int +next_assumption (int start) +{ + char * arg, c; + int res; + res = start + 1; + while (res < sargc) + { + arg = sargv[res++]; + if (!strcmp (arg, "-a")) + { + assert (res < sargc); + break; + } + + if (arg[0] == '-') { + c = arg[1]; + if (c == 'l' || c == 'i' || c == 's' || c == 'o' || c == 't' || + c == 'T' || c == 'r' || c == 'R' || c == 'c' || c == 'V' || + c == 'U' || c == 'A') res++; + } + } + if (res >= sargc) res = 0; + return res; +} + +static void +write_failed_assumptions (PicoSAT * picosat, FILE * file) +{ + int i, lit, count = 0; +#ifndef NDEBUG + int max_idx = picosat_variables (picosat); +#endif + i = 0; + while ((i = next_assumption (i))) { + lit = atoi (sargv[i]); + if (!picosat_failed_assumption (picosat, lit)) continue; + fprintf (file, "%d\n", lit); + count++; + } + if (verbose) + fprintf (output, "c found and wrote %d failed assumptions\n", count); +#ifndef NDEBUG + for (i = 1; i <= max_idx; i++) + if (picosat_failed_assumption (picosat, i)) + count--; +#endif + assert (!count); +} + +static void +write_to_file (PicoSAT * picosat, + const char *name, + const char *type, + void (*writer) (PicoSAT *, FILE *)) +{ + int pclose_file, zipped = has_suffix (name, ".gz"); + FILE *file; + char *cmd; + + if (zipped) + { +#if ZIP + cmd = malloc (strlen (GZIP) + strlen (name)); + sprintf (cmd, GZIP, name); + file = popen (cmd, "w"); + free (cmd); + pclose_file = 1; +#else + file = NULL; +#endif + } + else + { + file = fopen (name, "w"); + pclose_file = 0; + } + + if (file) + { + if (verbose) + fprintf (output, + "c\nc writing %s%s to '%s'\n", + zipped ? "gzipped " : "", type, name); + + writer (picosat, file); + + if (pclose_file) + pclose (file); + else + fclose (file); + } + else + fprintf (output, "*** picosat: can not write to '%s'\n", name); +} + +static int catched; + +static void (*sig_int_handler); +static void (*sig_segv_handler); +static void (*sig_abrt_handler); +static void (*sig_term_handler); +#ifndef NALLSIGNALS +static void (*sig_kill_handler); +static void (*sig_xcpu_handler); +static void (*sig_xfsz_handler); +#endif + +static void +resetsighandlers (void) +{ + (void) signal (SIGINT, sig_int_handler); + (void) signal (SIGSEGV, sig_segv_handler); + (void) signal (SIGABRT, sig_abrt_handler); + (void) signal (SIGTERM, sig_term_handler); +#ifndef NALLSIGNALS + (void) signal (SIGKILL, sig_kill_handler); + (void) signal (SIGXCPU, sig_xcpu_handler); + (void) signal (SIGXFSZ, sig_xfsz_handler); +#endif +} + +static int time_limit_in_seconds; +static void (*sig_alarm_handler); +static int ought_to_be_interrupted, interrupt_notified; + +static void +alarm_triggered (int sig) +{ + (void) sig; + assert (sig == SIGALRM); + assert (time_limit_in_seconds); + assert (!ought_to_be_interrupted); + ought_to_be_interrupted = 1; + assert (!interrupt_notified); +} + +static int +interrupt_call_back (void * dummy) +{ + (void) dummy; + if (!ought_to_be_interrupted) + return 0; + if (!interrupt_notified) + { + if (verbose) + { + picosat_message (picosat, 1, ""); + picosat_message (picosat, 1, + "*** TIME LIMIT OF %d SECONDS REACHED ***", + time_limit_in_seconds); + picosat_message (picosat, 1, ""); + } + interrupt_notified = 1; + } + return 1; +} + +static void +setalarm () +{ +#ifndef NALARM + assert (time_limit_in_seconds > 0); + sig_alarm_handler = signal (SIGALRM, alarm_triggered); + alarm (time_limit_in_seconds); + assert (picosat); + picosat_set_interrupt (picosat, 0, interrupt_call_back); +#endif +} + +static void +resetalarm () +{ + assert (time_limit_in_seconds > 0); + (void) signal (SIGALRM, sig_term_handler); +} + +static void +message (int sig) +{ + picosat_message (picosat, 1, ""); + picosat_message (picosat, 1, "*** CAUGHT SIGNAL %d ***", sig); + picosat_message (picosat, 1, ""); +} + +static void +catch (int sig) +{ + if (!catched) + { + message (sig); + catched = 1; + picosat_stats (picosat); + message (sig); + } + + resetsighandlers (); + raise (sig); +} + +static void +setsighandlers (void) +{ + sig_int_handler = signal (SIGINT, catch); + sig_segv_handler = signal (SIGSEGV, catch); + sig_abrt_handler = signal (SIGABRT, catch); + sig_term_handler = signal (SIGTERM, catch); +#ifndef NALLSIGNALS + sig_kill_handler = signal (SIGKILL, catch); + sig_xcpu_handler = signal (SIGXCPU, catch); + sig_xfsz_handler = signal (SIGXFSZ, catch); +#endif +} + +#define USAGE \ +"usage: picosat [