From 8a9d7fce8f894631954052a118dec81c9bed59aa Mon Sep 17 00:00:00 2001 From: Utz-Uwe Haus Date: Mon, 30 May 2016 13:05:06 +0200 Subject: [PATCH] Import PicoSAT-965 from http://fmv.jku.at/picosat/ Signed-off-by: Utz-Uwe Haus --- backends/picosat/LICENSE | 4 + backends/picosat/NEWS | 121 + backends/picosat/README | 4 + backends/picosat/VERSION | 4 + backends/picosat/app.c | 642 ++++ backends/picosat/configure.sh | 150 + backends/picosat/main.c | 9 + backends/picosat/makefile.in | 50 + backends/picosat/mkconfig.sh | 35 + backends/picosat/picogcnf.c | 165 + backends/picosat/picomcs.c | 334 ++ backends/picosat/picomus.c | 407 +++ backends/picosat/picosat.c | 6927 ++++++++++++++++++++++++++++++++++++++++- backends/picosat/picosat.h | 485 +++ 14 files changed, 9290 insertions(+), 47 deletions(-) create mode 100755 backends/picosat/configure.sh create mode 100755 backends/picosat/mkconfig.sh create mode 100644 backends/picosat/picogcnf.c create mode 100644 backends/picosat/picomcs.c create mode 100644 backends/picosat/picomus.c diff --git a/backends/picosat/LICENSE b/backends/picosat/LICENSE index 8896295..cfb3454 100644 --- a/backends/picosat/LICENSE +++ b/backends/picosat/LICENSE @@ -1,4 +1,8 @@ +<<<<<<< HEAD Copyright (c) 2006 - 2009, Armin Biere, Johannes Kepler University. +======= +Copyright (c) 2006 - 2014, Armin Biere, Johannes Kepler University. +>>>>>>> 7a0fcd7... Import PicoSAT-965 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to diff --git a/backends/picosat/NEWS b/backends/picosat/NEWS index fa99703..fc1d96c 100644 --- a/backends/picosat/NEWS +++ b/backends/picosat/NEWS @@ -1,6 +1,127 @@ +<<<<<<< HEAD news for release 91x since 846 ------------------------------ +======= +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 + +>>>>>>> 7a0fcd7... Import PicoSAT-965 * propagation of binary clauses until completion * fixed API usage 'assume;sat;sat' diff --git a/backends/picosat/README b/backends/picosat/README index 89d6ea5..275bf72 100644 --- a/backends/picosat/README +++ b/backends/picosat/README @@ -1,5 +1,9 @@ These are the sources of the PicoSAT solver. The preprocessor is not included. +<<<<<<< HEAD To compile run './configure && make'. +======= +To compile run './configure.sh && make'. +>>>>>>> 7a0fcd7... Import PicoSAT-965 The API is document in 'picosat.h'. See also 'NEWS' and 'LICENSE'. diff --git a/backends/picosat/VERSION b/backends/picosat/VERSION index d6904a9..d30959e 100644 --- a/backends/picosat/VERSION +++ b/backends/picosat/VERSION @@ -1 +1,5 @@ +<<<<<<< HEAD 913 +======= +965 +>>>>>>> 7a0fcd7... Import PicoSAT-965 diff --git a/backends/picosat/app.c b/backends/picosat/app.c index 4b6abbf..70659b9 100644 --- a/backends/picosat/app.c +++ b/backends/picosat/app.c @@ -1,25 +1,48 @@ #include "picosat.h" #include +<<<<<<< HEAD #include #include #include #define GUNZIP "gunzip -c %s" +======= +#include +#include +#include +#include +#include +#include + +#define GUNZIP "gunzip -c %s" +#define BUNZIP2 "bzcat %s" +>>>>>>> 7a0fcd7... Import PicoSAT-965 #define GZIP "gzip -c -f > %s" FILE * popen (const char *, const char*); int pclose (FILE *); +<<<<<<< HEAD +======= +static PicoSAT * picosat; + +>>>>>>> 7a0fcd7... Import PicoSAT-965 static int lineno; static FILE *input; static int inputid; static FILE *output; static int verbose; +<<<<<<< HEAD +======= +static int sargc; +static char ** sargv; +>>>>>>> 7a0fcd7... Import PicoSAT-965 static char buffer[100]; static char *bhead = buffer; static const char *eob = buffer + 80; static FILE * incremental_rup_file; +<<<<<<< HEAD extern void picosat_enter (void); extern void picosat_leave (void); @@ -27,10 +50,17 @@ extern void picosat_leave (void); static char page[4096]; static char * top; static char * end; +======= +static signed char * sol; + +extern void picosat_enter (PicoSAT *); +extern void picosat_leave (PicoSAT *); +>>>>>>> 7a0fcd7... Import PicoSAT-965 static int next (void) { +<<<<<<< HEAD size_t bytes; int res; @@ -49,6 +79,9 @@ next (void) res = *top++; +======= + int res = getc (input); +>>>>>>> 7a0fcd7... Import PicoSAT-965 if (res == '\n') lineno++; @@ -56,7 +89,11 @@ next (void) } static const char * +<<<<<<< HEAD parse (int force) +======= +parse (PicoSAT * picosat, int force) +>>>>>>> 7a0fcd7... Import PicoSAT-965 { int ch, sign, lit, vars, clauses; @@ -120,10 +157,17 @@ INVALID_HEADER: fflush (output); } +<<<<<<< HEAD picosat_adjust (vars); if (incremental_rup_file) picosat_set_incremental_rup_file (incremental_rup_file, vars, clauses); +======= + picosat_adjust (picosat, vars); + + if (incremental_rup_file) + picosat_set_incremental_rup_file (picosat, incremental_rup_file, vars, clauses); +>>>>>>> 7a0fcd7... Import PicoSAT-965 lit = 0; READ_LITERAL: @@ -177,7 +221,11 @@ READ_LITERAL: else clauses--; +<<<<<<< HEAD picosat_add (lit); +======= + picosat_add (picosat, lit); +>>>>>>> 7a0fcd7... Import PicoSAT-965 goto READ_LITERAL; } @@ -214,15 +262,33 @@ REENTER: } static void +<<<<<<< HEAD printa (void) { int max_idx = picosat_variables (), i, lit; +======= +printa (PicoSAT * picosat, int partial) +{ + int max_idx = picosat_variables (picosat), i, lit, val; +>>>>>>> 7a0fcd7... Import PicoSAT-965 assert (bhead == buffer); for (i = 1; i <= max_idx; i++) { +<<<<<<< HEAD lit = (picosat_deref (i) > 0) ? i : -i; +======= + if (partial) + { + val = picosat_deref_partial (picosat, i); + if (!val) + continue; + } + else + val = picosat_deref (picosat, i); + lit = (val > 0) ? i : -i; +>>>>>>> 7a0fcd7... Import PicoSAT-965 printi (lit); } @@ -231,6 +297,29 @@ printa (void) bflush (); } +<<<<<<< HEAD +======= +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); +} + +>>>>>>> 7a0fcd7... Import PicoSAT-965 static int has_suffix (const char *str, const char *suffix) { @@ -242,6 +331,7 @@ has_suffix (const char *str, const char *suffix) } static void +<<<<<<< HEAD write_core_variables (FILE * file) { int i, max_idx = picosat_variables (); @@ -252,6 +342,77 @@ write_core_variables (FILE * file) static void write_to_file (const char *name, const char *type, void (*writer) (FILE *)) +======= +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 *)) +>>>>>>> 7a0fcd7... Import PicoSAT-965 { int pclose_file, zipped = has_suffix (name, ".gz"); FILE *file; @@ -278,7 +439,11 @@ write_to_file (const char *name, const char *type, void (*writer) (FILE *)) "c\nc writing %s%s to '%s'\n", zipped ? "gzipped " : "", type, name); +<<<<<<< HEAD writer (file); +======= + writer (picosat, file); +>>>>>>> 7a0fcd7... Import PicoSAT-965 if (pclose_file) pclose (file); @@ -289,6 +454,125 @@ write_to_file (const char *name, const char *type, void (*writer) (FILE *)) fprintf (output, "*** picosat: can not write to '%s'\n", name); } +<<<<<<< HEAD +======= +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 () +{ + 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); +} + +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 +} + +>>>>>>> 7a0fcd7... Import PicoSAT-965 #define USAGE \ "usage: picosat [