From 2e08fe478f6179cea444882c01190fda5f81f10a Mon Sep 17 00:00:00 2001 From: Utz-Uwe Haus Date: Sun, 30 May 2010 19:41:39 +0200 Subject: [PATCH] Import precosat-465r2-2ce82ba-100514 Signed-off-by: Utz-Uwe Haus --- backends/INVENTORY | 1 + backends/precosat/LICENSE | 19 + backends/precosat/NEWS | 16 + backends/precosat/README | 6 + backends/precosat/VERSION | 1 + backends/precosat/configure | 59 + backends/precosat/makefile.in | 16 + backends/precosat/mkconfig | 41 + backends/precosat/precobnr.cc | 65 + backends/precosat/precobnr.hh | 29 + backends/precosat/precomain.cc | 360 ++++ backends/precosat/precosat.cc | 4628 ++++++++++++++++++++++++++++++++++++++++ backends/precosat/precosat.hh | 732 +++++++ 13 files changed, 5973 insertions(+) create mode 100644 backends/INVENTORY create mode 100644 backends/precosat/LICENSE create mode 100644 backends/precosat/NEWS create mode 100644 backends/precosat/README create mode 100644 backends/precosat/VERSION create mode 100755 backends/precosat/configure create mode 100644 backends/precosat/makefile.in create mode 100755 backends/precosat/mkconfig create mode 100644 backends/precosat/precobnr.cc create mode 100644 backends/precosat/precobnr.hh create mode 100644 backends/precosat/precomain.cc create mode 100644 backends/precosat/precosat.cc create mode 100644 backends/precosat/precosat.hh diff --git a/backends/INVENTORY b/backends/INVENTORY new file mode 100644 index 0000000..927b622 --- /dev/null +++ b/backends/INVENTORY @@ -0,0 +1 @@ +precosat is precosat-465r2-2ce82ba-100514 diff --git a/backends/precosat/LICENSE b/backends/precosat/LICENSE new file mode 100644 index 0000000..8ba05d5 --- /dev/null +++ b/backends/precosat/LICENSE @@ -0,0 +1,19 @@ +Copyright (c) 2009, 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/backends/precosat/NEWS b/backends/precosat/NEWS new file mode 100644 index 0000000..08f0346 --- /dev/null +++ b/backends/precosat/NEWS @@ -0,0 +1,16 @@ +new features in 465r2 +--------------------- + +fixedto incremental usage of blocked clauses + +new features in 465 since 236 +----------------------------- +blocked clause elimination +glucose glueing +preprocessing run-to-completion mode +stand alone preprocessing +on-the-fly subsumption +allow one proper inverse arc but disabled +application interface similar to PicoSAT without assumptions yet +added backward subsumption and strengthening for learned clauses +removed hash table for binary clauses diff --git a/backends/precosat/README b/backends/precosat/README new file mode 100644 index 0000000..2b9a406 --- /dev/null +++ b/backends/precosat/README @@ -0,0 +1,6 @@ +These are the sources of the SAT solver PrecoSAT. +To build issue + +./configure && make + +for compilation options see './configure -h'. diff --git a/backends/precosat/VERSION b/backends/precosat/VERSION new file mode 100644 index 0000000..52411df --- /dev/null +++ b/backends/precosat/VERSION @@ -0,0 +1 @@ +465r2 diff --git a/backends/precosat/configure b/backends/precosat/configure new file mode 100755 index 0000000..bf255ce --- /dev/null +++ b/backends/precosat/configure @@ -0,0 +1,59 @@ +#!/bin/sh + +cpt=no # enforces competition settings if set to yes + +rm -f makefile + +if [ ! x"$cpt" = xyes ] +then +cov=no;dbg=no;log=no;m32=no;opt=no;chk=no;stc=no;sts=no +while [ $# -gt 0 ] +do + case $1 in + -h) +echo "usage: configure [-h|-g|-O|-l|-c|-m32|-static|--check|--stats]" +echo "-h print this command line option summary" +echo "-g compiling with debugging information" +echo "-O heavy optimizations through compiler" +echo "-l enable logging" +echo "-c enable coverage" +echo "-m32 enforce 32 bit binary even on 64 bit machine" +echo "-s|-static|--static static compilation" +echo "--check enable expensive assertion checking" +echo "--stats enable slightly more expensive statistics" +exit 0 +;; + -g) dbg=yes;opt=no;sts=yes;; + -O) dbg=no;opt=yes;sts=no;; + -l) log=yes;; + -c) cov=yes;; + -m32) m32=yes;; + -s|-static|--static) stc=yes;; + --check) chk=yes;; + --stats) sts=yes;; + *) echo "*** configure: invalid option" 1>&2; exit 1;; + esac + shift +done +else +cov=no;dbg=no;log=no;m32=yes;opt=yes;chk=no;stc=yes;sts=no +fi + +[ $cov = yes ] && dbg=yes +[ $chk = yes ] && opt=no +[ x"$CXX" = x ] && CXX=g++ +[ $dbg = yes ] && CXXFLAGS="-g" +[ $dbg = no ] && CXXFLAGS="-O3" +[ $m32 = yes ] && CXXFLAGS="$CXXFLAGS -m32" +[ $stc = yes ] && CXXFLAGS="$CXXFLAGS -static" +CXXFLAGS="$CXXFLAGS -Wall -Wextra" +[ $dbg = no -a $chk = no ] && CXXFLAGS="$CXXFLAGS -DNDEBUG" +[ $log = no ] && CXXFLAGS="$CXXFLAGS -DNLOGPRECO" +[ $sts = no ] && CXXFLAGS="$CXXFLAGS -DNSTATSPRECO" +[ $opt = yes ] && CXXFLAGS="$CXXFLAGS -finline-limit=10000000" +[ $opt = yes ] && CXXFLAGS="$CXXFLAGS -fomit-frame-pointer" +[ $opt = yes ] && CXXFLAGS="$CXXFLAGS -fno-exceptions" +[ $cov = yes ] && CXXFLAGS="$CXXFLAGS -fprofile-arcs -ftest-coverage" +echo "$CXX $CXXFLAGS" + +sed -e "s,@CXX@,$CXX," -e "s,@CXXFLAGS@,$CXXFLAGS,g" makefile.in > makefile diff --git a/backends/precosat/makefile.in b/backends/precosat/makefile.in new file mode 100644 index 0000000..c012e10 --- /dev/null +++ b/backends/precosat/makefile.in @@ -0,0 +1,16 @@ +CXX=@CXX@ +CXXFLAGS=@CXXFLAGS@ +all: precosat +clean: + rm -f precosat *.o makefile precocfg.hh + rm -f *.gcno *.gcda cscope.out gmon.out *.gcov +precosat: precomain.o precosat.o precobnr.o + $(CXX) $(CXXFLAGS) -o precosat precomain.o precosat.o precobnr.o +precosat.o: precosat.hh precosat.cc makefile + $(CXX) $(CXXFLAGS) -c precosat.cc +precobnr.o: precobnr.cc precobnr.hh precocfg.hh + $(CXX) $(CXXFLAGS) -c precobnr.cc +precomain.o: precomain.cc precocfg.hh precobnr.hh + $(CXX) $(CXXFLAGS) -c precomain.cc +precocfg.hh: makefile VERSION mkconfig precosat.hh precosat.cc + rm -f $@; ./mkconfig > $@ diff --git a/backends/precosat/mkconfig b/backends/precosat/mkconfig new file mode 100755 index 0000000..0eac247 --- /dev/null +++ b/backends/precosat/mkconfig @@ -0,0 +1,41 @@ +#!/bin/sh + +die () { + echo "*** mkconfig: $*" 1>&2 + exit 1 +} + +[ -f makefile ] || die "can not find 'makefile'" + +cat< +#include + +const char * precosat_version () { + return PRECOSAT_VERSION " " PRECOSAT_ID; +} + +void precosat_banner () { + printf ("c PrecoSAT Version %s %s\n", PRECOSAT_VERSION, PRECOSAT_ID); + printf ("c Copyright (C) 2009, Armin Biere, JKU, Linz, Austria." + " All rights reserved.\n"); + printf ("c Released on %s\n", PRECOSAT_RELEASED); + printf ("c Compiled on %s\n", PRECOSAT_COMPILED); + printf ("c %s\n", PRECOSAT_CXX); + const char * p = PRECOSAT_CXXFLAGS; + assert (*p); + for (;;) { + fputs ("c ", stdout); + const char * q; + for (q = p; *q && *q != ' '; q++) + ; + if (*q && q - p < 76) { + for (;;) { + const char * n; + for (n = q + 1; *n && *n != ' '; n++) + ; + if (n - p >= 76) break; + q = n; + if (!*n) break; + } + } + while (p < q) fputc (*p++, stdout); + fputc ('\n', stdout); + if (!*p) break; + assert(*p == ' '); + p++; + } + printf ("c %s\n", PRECOSAT_OS); + fflush (stdout); +} diff --git a/backends/precosat/precobnr.hh b/backends/precosat/precobnr.hh new file mode 100644 index 0000000..730d613 --- /dev/null +++ b/backends/precosat/precobnr.hh @@ -0,0 +1,29 @@ +/*************************************************************************** +Copyright (c) 2009, 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. +****************************************************************************/ + +#ifndef precobnr_hh_INCLUDED +#define precobnr_hh_INCLUDED + +void precosat_banner (); +const char * precosat_version (); + +#endif diff --git a/backends/precosat/precomain.cc b/backends/precosat/precomain.cc new file mode 100644 index 0000000..66e86b4 --- /dev/null +++ b/backends/precosat/precomain.cc @@ -0,0 +1,360 @@ +/*************************************************************************** +Copyright (c) 2009, 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 "precosat.hh" +#include "precobnr.hh" + +extern "C" { +#include +#include +#include +#include +}; + +using namespace PrecoSat; + +static Solver * solverptr; +static bool catchedsig; +static int verbose, quiet; + +static void (*sig_int_handler)(int); +static void (*sig_segv_handler)(int); +static void (*sig_abrt_handler)(int); +static void (*sig_term_handler)(int); + +static bool hasgzsuffix (const char * str) + { return strlen (str) >= 3 && !strcmp (str + strlen (str) - 3, ".gz"); } + +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); +} + +static void caughtsigmsg (int sig) { + if (verbose) printf ("c\n"); + if (!quiet) printf ("c *** CAUGHT SIGNAL %d ***\n", sig); + if (verbose) printf ("c\n"); + fflush (stdout); +} + +static void catchsig (int sig) { + if (!catchedsig) { + catchedsig = true; + caughtsigmsg (sig); + if (verbose) solverptr->prstats (), caughtsigmsg (sig); + } + + resetsighandlers (); + raise (sig); +} + +static void +setsighandlers (void) { + sig_int_handler = signal (SIGINT, catchsig); + sig_segv_handler = signal (SIGSEGV, catchsig); + sig_abrt_handler = signal (SIGABRT, catchsig); + sig_term_handler = signal (SIGTERM, catchsig); +} + +static const char * usage = +"usage: precosat [-h|-v|-n][-l ][--[no-][=]] []\n" +"\n" +" -h this command line summary\n" +" -v increase verbosity\n" +" -q be quiet and only set exit code\n" +" -n do not print witness\n" +" -N do not print witness nor result line\n" +" -l set decision limit\n" +" -p print CNF after first simplification \n" +" -s simplify and print (same as '-N -p -l 0')\n" +" -e satelite only style preprocessing\n" +" -k blocked clause only style preprocessing\n" +" -o set output file for '-p' respectively '-s'\n" +" dimacs input file (default stdin)\n" +"\n" +" -- set internal option to 1\n" +" --no- set internal option to 0\n" +" --= set internal option to integer value \n" +; + +int main (int argc, char ** argv) { + bool fclosefile=false,pclosefile=false,nowit=false,nores=false,simp=false; + int print=0, decision_limit=INT_MAX; + const char * name = 0, * output = 0; + bool satelite=false,blocked=false; + FILE * file = stdin; + for (int i = 1; i < argc; i++) { + if (!strcmp (argv[i], "-h")) { + fputs (usage, stdout); + exit (0); + } + if (!strcmp (argv[i], "-v")) { + if (verbose >= 2) { + fprintf (stderr, "*** precosat: too many '-v'\n"); + exit (1); + } + verbose++; + continue; + } + if (!strcmp (argv[i], "--verbose")) { verbose=1; continue; } + if (!strcmp (argv[i], "--no-verbose")) { verbose=0; continue; } + if (!strcmp (argv[i], "--verbose=0")) { verbose=0; continue; } + if (!strcmp (argv[i], "--verbose=1")) { verbose=1; continue; } + if (!strcmp (argv[i], "--verbose=2")) { verbose=2; continue; } + if (!strcmp (argv[i], "-q")) { quiet = 1; continue; } + if (!strcmp (argv[i], "-p")) { print = 1; continue; } + if (!strcmp (argv[i], "-s")) { simp = true; continue; } + if (!strcmp (argv[i], "--quiet")) { quiet = 1; continue; } + if (!strcmp (argv[i], "--no-quiet")) { quiet = 0; continue; } + if (!strcmp (argv[i], "--quiet=0")) { quiet = 0; continue; } + if (!strcmp (argv[i], "--quiet=1")) { quiet = 1; continue; } + if (!strcmp (argv[i], "-n")) { nowit = true; continue; } + if (!strcmp (argv[i], "-N")) { nores = true; continue; } + if (!strcmp (argv[i], "-k")) { blocked = true; continue; } + if (!strcmp (argv[i], "-e")) { satelite = true; continue; } + if (!strcmp (argv[i], "-l")) { + if (i + 1 == argc) { + fprintf (stderr, "*** precosat: argument to '-l' missing\n"); + exit (1); + } + decision_limit = atoi (argv[++i]); + continue; + } + if (!strcmp (argv[i], "-o")) { + if (i + 1 == argc) { + fprintf (stderr, "*** precosat: argument to '-o' missing\n"); + exit (1); + } + output = argv[++i]; + continue; + } + if (argv[i][0] == '-' && argv[i][1] == '-') continue; + if (argv[i][0] == '-' || name) { + fprintf (stderr, "*** precosat: invalid usage (try '-h')\n"); + exit (1); + } + name = argv[i]; + if (hasgzsuffix (name)) { + char * cmd = (char*) malloc (strlen(name) + 100); + sprintf (cmd, "gunzip -c %s 2>/dev/null", name); + if ((file = popen (cmd, "r"))) + pclosefile = true; + free (cmd); + } else if ((file = fopen (name, "r"))) + fclosefile = true; + } + if (!name) name = ""; + if (!file) { + fprintf (stderr, "*** precosat: can not read '%s'\n", name); + exit (1); + } + if (blocked && satelite) die ("can not use both '-e' and '-k'"); + if (nores) nowit = true; + if (blocked || satelite) simp = true; + if (simp) nowit = nores = true, print = 1, decision_limit = 0; + if (quiet) verbose = 0, nowit = true; + if (verbose) { + precosat_banner (); + printf ("c\nc reading %s\n", name); + fflush (stdout); + } + int ch; + while ((ch = getc (file)) == 'c') + while ((ch = getc (file)) != '\n' && ch != EOF) + ; + if (ch == EOF) + goto INVALID_HEADER; + ungetc (ch, file); + int m, n; + if (fscanf (file, "p cnf %d %d\n", &m, &n) != 2) { +INVALID_HEADER: + fprintf (stderr, "*** precosat: invalid header\n"); + exit (1); + } + if (verbose) { + printf ("c found header 'p cnf %d %d'\n", m, n); + fflush (stdout); + } + Solver solver; + solver.init (m); + solverptr = &solver; + setsighandlers (); + for (int i = 1; i < argc; i++) { + bool ok = true; + if (argv[i][0] == '-' && argv[i][1] == '-') { + if (argv[i][2] == 'n' && argv[i][3] == 'o' && argv[i][4] == '-') { + if (!solver.set (argv[i] + 5, 0)) ok = false; + } else { + const char * arg = argv[i] + 2, * p; + for (p = arg; *p && *p != '='; p++) + ; + if (*p) { + assert (*p == '='); + char * opt = strndup (arg, p - arg); + if (!strcmp (opt, "output")) ok = solver.set (opt, p + 1); + else ok = solver.set (opt, atoi (p + 1)); + free (opt); + } else ok = solver.set (argv[i] + 2, 1); + } + } + if (!ok) { + fprintf (stderr, "*** precosat: invalid option '%s'\n", argv[i]); + exit (1); + } + } + solver.set ("verbose", verbose); + solver.set ("quiet", quiet); + solver.set ("print", print); + if (output) solver.set ("output", output); + if (blocked || satelite) { + assert (simp); + solver.set ("decompose",0); + solver.set ("probe",0); + solver.set ("otfs",0); + solver.set ("elimasym", 0); + } + if (blocked) solver.set ("elim",0), solver.set ("blockrtc",2); + if (satelite) solver.set ("block",0), solver.set ("elimrtc",2); + solver.fxopts (); + int lit, sign; + int res = 0; + + ch = getc (file); + +NEXT: + + if (ch == 'c') { + while ((ch = getc (file)) != '\n') + if (ch == EOF) { + fprintf (stderr, "*** precosat: EOF in comment\n"); + resetsighandlers (); + exit (1); + } + goto NEXT; + } + + if (ch == ' ' || ch == '\n') { + ch = getc (file); + goto NEXT; + } + + if (ch == EOF) goto DONE; + + if (!n) { + fprintf (stderr, "*** precosat: too many clauses\n"); + res = 1; + goto EXIT; + } + + if ((sign = (ch == '-'))) ch = getc (file); + + if (!isdigit (ch) || (sign && ch == '0')) { + fprintf (stderr, "*** precosat: expected digit\n"); + res = 1; + goto EXIT; + } + + lit = (ch - '0'); + while (isdigit (ch = getc (file))) lit = 10 * lit + (ch - '0'); + + if (lit > m) { + fprintf (stderr, "*** precosat: variables exceeded\n"); + res = 1; + goto EXIT; + } + + lit = 2 * lit + sign; + solver.add (lit); + if (!lit) n--; + + goto NEXT; + +DONE: + + if (n) { + fprintf (stderr, "*** precosat: clauses missing\n"); + res = 1; + goto EXIT; + } + + if (pclosefile) pclose (file); + if (fclosefile) fclose (file); + + if (verbose) { + printf ("c finished parsing\n"); + printf ("c\n"); solver.propts (); printf ("c\n"); + printf ("c starting search after %.1f seconds\n", solver.seconds ()); + if (decision_limit == INT_MAX) printf ("c no decision limit\n"); + else printf ("c search limited to %d decisions\n", decision_limit); + fflush (stdout); + } + + res = solver.solve (decision_limit); + + if (verbose) { + printf ("c\n"); + fflush (stdout); + } + + if (res > 0) { + if (!solver.satisfied ()) { + if (!quiet) printf ("c ERROR\n"); + abort (); + } + if (!quiet && !nores) printf ("s SATISFIABLE\n"); + if (!nowit) { + fflush (stdout); + if (m) fputs ("v", stdout); + for (int i = 1; i <= m; i++) { + if (i % 8) fputc (' ', stdout); + else fputs ("\nv ", stdout); + printf ("%d", (solver.val (2 * i) < 0) ? -i : i); + } + if (m) fputc ('\n', stdout); + fputs ("v 0\n", stdout); + } + res = 10; + } else if (res < 0) { + assert (res < 0); + if (!quiet && !nores) printf ("s UNSATISFIABLE\n"); + res = 20; + } else if (!quiet && !nores) + printf ("s UNKNOWN\n"); + + if (!quiet) fflush (stdout); + +EXIT: + resetsighandlers (); + if (verbose) { + printf ("c\n"); + solver.prstats (); + } + +#ifndef NDEBUG + solver.reset (); +#endif + + return res; +} diff --git a/backends/precosat/precosat.cc b/backends/precosat/precosat.cc new file mode 100644 index 0000000..d3413d7 --- /dev/null +++ b/backends/precosat/precosat.cc @@ -0,0 +1,4628 @@ +/*************************************************************************** +Copyright (c) 2009, 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 "precosat.hh" +#include "precobnr.hh" + +#include +#include +#include + +extern "C" { +#include +#include +#include +#include +#include +#include +}; + +#ifndef NLOGPRECO +#include +#define LOG(code) \ + do { std::cout << prfx << "LOG " << code << std::endl; } while (false) +#else +#define LOG(code) do { } while (false) +#endif + +#if 0 +#include +#define COVER(code) \ + do { std::cout << prfx << "COVER " << __FUNCTION__ << ' ' \ + << __LINE__ << ' ' << code << std::endl; } while (false) +#else +#define COVER(code) do { } while (false) +#endif + +//#define PRECOCHECK +#ifdef PRECOCHECK +#warning "PRECOCHECK enabled" +#endif + +#ifndef NSTATSPRECO +#define INC(s) do { stats.s++; } while (0) +#else +#define INC(s) do { } while (0) +#endif + +namespace PrecoSat { + +template inline static void swap (T & a, T & b) + { T tmp = a; a = b; b = tmp; } + +template inline static const T min (const T a, const T b) + { return a < b ? a : b; } + +template inline static const T max (const T a, const T b) + { return a > b ? a : b; } + +template inline static void fix (T * & p, long moved) + { char * q = (char*) p; q += moved; p = (T*) q; } + +inline static int logsize (int size) { return (128 >> size) + 1; } + +static inline Val lit2val (int lit) { return (lit & 1) ? -1 : 1; } + +static inline Cls * lit2conflict (Cls & bins, int a, int b) { + bins.lits[0] = a; + bins.lits[1] = b; + assert (!bins.lits[2]); + return &bins; +} + +static inline unsigned ggt (unsigned a, unsigned b) + { while (b) { unsigned r = a % b; a = b, b = r; } return a; } + +inline static unsigned minuscap (unsigned a, unsigned b) + { return (a <= b) ? 0 : (a - b); } + +static inline double mb (size_t bytes) + { return bytes / (double) (1<<20); } + +static inline bool sigsubs (unsigned s, unsigned t) + { return !(s&~t); } + +static inline unsigned listig (int lit) + { return (1u << (31u & (unsigned)(lit/2))); } + +static inline double average (double a, double b) { return b ? a/b : 0; } + +static inline double percent (double a, double b) { return 100*average(a,b); } + +static bool parity (unsigned x) + { bool res = false; while (x) res = !res, x &= x-1; return res; } +} + +using namespace PrecoSat; + +inline unsigned RNG::next () { + unsigned res = state; + state *= 1664525u; + state += 1013904223u; + return res; +} + +inline bool RNG::oneoutof (unsigned spread) { + return spread ? !(next () % spread) : true; +} + +inline size_t Cls::bytes (int n) { + return sizeof (Cls) + (n - 3 + 1) * sizeof (int); +} + +inline size_t Cls::bytes () const { return bytes (size); } + +inline Anchor & Solver::anchor (Cls * c) { + if (c->binary) return binary; + if (!c->lnd) return original; + if (c->fresh) return fresh; + return learned[c->glue]; +} + +inline int Cls::minlit () const { + int res = INT_MAX, other; + for (const int * p = lits; (other = *p); p++) + if (other < res) res = other; + return res; +} + +inline bool Cls::contains (int lit) const { + if (!(sig & listig (lit))) return false; + for (const int * p = lits; *p; p++) + if (*p == lit) return true; + return false; +} + +inline void Solver::setsig (Cls * cls) { + int except = cls->minlit (), lit; + unsigned fwsig = 0, bwsig = 0; + for (const int * p = cls->lits; (lit = *p); p++) { + unsigned sig = listig (lit); + bwsig |= sig; + if (lit != except) fwsig |= sig; + } + cls->sig = bwsig; + for (const int * p = cls->lits; (lit = *p); p++) + bwsigs[lit] |= bwsig; + if (fwsigs) + fwsigs[except] |= fwsig; +} + +inline unsigned Solver::litsig () { + unsigned res = 0; + for (int i = 0; i < lits; i++) + res |= listig (lits[i]); + return res; +} + +inline bool Solver::clt (int a, int b) const { + Var & u = vars[a/2], &v = vars[b/2]; + int l = u.dlevel, k = v.dlevel; + if (l < 0) return false; + if (k < 0) return true; + if (l < k) return true; + if (l > k) return false; + Val r = vals[a], s = vals[b]; + if (r < s) return true; + return false; +} + +inline void Solver::connect (Cls * c) { + for (int i = 0; i <= 1; i++) { + int lit, * r = c->lits + i, * q = r, best = *q; + for (int * p = q + 1; (lit = *p); p++) + if (clt (best, lit)) q = p, best = lit; + *q = *r, *r = best; + } + assert (c->lits[0] && c->lits[1]); + Anchor & a = anchor (c); + if (!connected (a, c)) push (a, c); + if (c->binary) { + for (int i = 0; i <= 1; i++) + occs[c->lits[i]].bins.push (mem, c->lits[!i]); + } else { + for (int i = 0; i <= 1; i++) + occs[c->lits[i]].large.push (mem, Occ (c->lits[!i], c)); + } + if (orgs) + for (const int * p = c->lits; *p; p++) + orgs[*p].push (mem, c); + if (fwds) fwds[c->minlit ()].push (mem, c); + setsig (c); +} + +inline void Solver::disconnect (Cls * c) { + assert (!c->locked && !c->dirty && !c->trash); + int l0 = c->lits[0], l1 = c->lits[1]; + assert (l0 && l1); + Anchor & a = anchor (c); + if (connected (a, c)) dequeue (a, c); + if (c->binary) { + occs[l0].bins.remove(l1); + occs[l1].bins.remove(l0); + } else { + occs[l0].large.remove(Occ(0,c)); + occs[l1].large.remove(Occ(0,c)); + } + if (fwds) fwds[c->minlit ()].remove (c); + if (!orgs || c->lnd) return; + for (const int * p = c->lits; *p; p++) + orgs[*p].remove (c); +} + +inline Rnk * Solver::prb (const Rnk * r) { return prbs + (r - rnks); } +inline Rnk * Solver::rnk (const Var * v) { return rnks + (v - vars); } +inline Var * Solver::var (const Rnk * r) { return vars + (r - rnks); } + +inline Val Solver::fixed (int lit) const { + return vars[lit/2].dlevel ? 0 : vals[lit]; +} + +inline void Solver::collect (Cls * cls) { + assert (!cls->locked && !cls->dirty && !cls->trash && !cls->gate); + if (cls->binary) assert (stats.clauses.bin), stats.clauses.bin--; + else if (cls->lnd) assert (stats.clauses.lnd), stats.clauses.lnd--; + else assert (stats.clauses.orig), stats.clauses.orig--; + if (!cls->lnd) assert (stats.clauses.irr), stats.clauses.irr--; + size_t bytes = cls->bytes (); +#ifdef PRECOCHECK + if (!cls->lnd) { + for (const int * p = cls->lits; *p; p++) + check.push (mem, *p); + check.push (mem, 0); + } +#endif +#ifndef NLOGPRECO + dbgprint ("LOG recycle clause ", cls); +#endif + mem.deallocate (cls, bytes); + stats.collected += bytes; + simplified = true; +} + +void Solver::touchblkd (int lit) { + assert (blkmode); + int idx = lit/2, notlit = lit^1; + Var * v = vars + idx; + if (v->type != FREE) return; + assert (!val (lit) && !repr[lit]); + Rnk * r = blks + notlit; + assert (orgs); + int nh = -orgs[lit], oh = r->heat; r->heat = nh; + if (oh == nh && schedule.block.contains (r)) return; + if (oh == nh) LOG ("touchblkd " << notlit << " again " << nh); + else LOG ("touchblkd " << notlit << " from " << oh << " to " << nh); + if (!schedule.block.contains (r)) schedule.block.push (mem, r); + else if (nh > oh) schedule.block.up (r); + else if (nh < oh) schedule.block.down (r); +} + +void Solver::touchelim (int lit) { + assert (elimode); + lit &= ~1; + int idx = lit/2; + Var * v = vars + idx; + if (v->type != FREE) return; + assert (!val (lit) && !repr[lit]); + if (idx == elimvar) return; + Rnk * r = elms + idx; + assert (orgs); + int pos = orgs[lit]; + int neg = orgs[1^lit]; + long long tmp = -(((long long)pos) * (long long) neg); + int nh = (tmp >= INT_MIN) ? (int) tmp : INT_MIN; + int oh = r->heat; r->heat = nh; + if (oh == nh && schedule.elim.contains (r)) return; + if (oh == nh) LOG ("touchelim " << lit << " again " << nh); + else LOG ("touchelim " << lit << " from " << oh << " to " << nh); + if (pos > 1 && neg > 1 && nh <= opts.elimin) { + if (schedule.elim.contains (r)) { + schedule.elim.remove (r); + } + } else if (!schedule.elim.contains (r)) schedule.elim.push (mem, r); + else if (nh > oh) schedule.elim.up (r); + else if (nh < oh) schedule.elim.down (r); +} + +void Solver::touchpure (int lit) { + assert (puremode); + int idx = lit/2; + Var * v = vars + idx; + if (v->onplits) return; + LOG ("touchpure " << lit); + v->onplits = true; + plits.push (mem, idx); +} + +void Solver::touch (int lit) { + assert (elimode + blkmode == 1); + if (elimode) touchelim (lit); + else touchblkd (lit); + if (puremode) touchpure (lit); +} + +void Solver::touch (Cls * c) { + assert (asymode || !c->lnd); + assert (elimode || blkmode); + for (int * p = c->lits; *p; p++) + touch (*p); +} + +inline void Solver::recycle (Cls * c) { + stats.clauses.gc++; + disconnect (c); + if (c->trash) trash.remove (c); + if (c->gate) cleangate (); + if (c->str) strnd.remove (c); + if (elimode || blkmode) touch (c); + collect (c); +} + +inline void Solver::dump (Cls * c) { + assert (!c->dirty); + if (c->trash) return; + c->trash = true; + trash.push (mem, c); +} + +inline void Solver::cleantrash () { + if (!trash) return; + int old = stats.clauses.orig; + while (trash) { + Cls * cls = trash.pop (); + assert (cls->trash); + cls->trash = false; + recycle (cls); + } + shrink (old); +} + +inline void Solver::gcls (Cls * c) { + assert (!c->gate); + c->gate = true; + gate.push (mem, c); +} + +inline void Solver::strcls (Cls * c) { + assert (!c->str); + c->str = true; + strnd.push (mem, c); +} + +inline void Solver::cleangate () { + while (gate) { + Cls * cls = gate.pop (); + assert (cls->gate); cls->gate = false; + } + gatepivot = 0; + gatestats = 0; + gatelen = 0; +} + +inline void Solver::recycle (int lit) { + LOG ("recycle literal " << lit); + assert (!level); +#ifndef NDEBUG + Var * v = vars + (lit/2); Vrt t = v->type; + assert (t == FIXED || t == PURE || t == ZOMBIE || t == ELIM); +#endif + if (!orgs) return; + while (int size = orgs[lit]) recycle (orgs[lit][size - 1]); + orgs[lit].release (mem); + occs[lit].bins.release (mem); + occs[lit].large.release (mem); +} + +Opt::Opt (const char * n, int v, int * vp, int mi, int ma) : +name (n), valptr (vp), min (mi), max (ma) +{ + assert (min <= v); + assert (v <= max); + *vp = v; +} + +bool Opts::set (const char * opt, int val) { + for (Opt * o = opts.begin (); o < opts.end (); o++) + if (!strcmp (o->name, opt)) { + if (val < o->min) return false; + if (val > o->max) return false; + *o->valptr = val; + return true; + } + return false; +} + +bool Opts::set (const char * opt, const char * val) { + if (strcmp (opt, "output")) return false; + output = val; + return true; +} + +void Opts::add (Mem & mem, const char * n, int v, int * vp, int mi, int ma) { + opts.push (mem, Opt (n, v, vp, mi, ma)); +} + +void Opts::printoptions (FILE * file, const char * prfx) const { + assert (prfx); + int lenprfx = strlen (prfx); + fputs (prfx, file); int pos = 0; + const Opt * o = opts.begin (); + while (o < opts.end ()) { + char line[80]; + sprintf (line, " --%s=%d", o->name, *o->valptr); + int len = strlen (line); assert (len < 80); + if (len + pos >= 77 - lenprfx) { + fprintf (file, "\n%s", prfx); + pos = lenprfx; + } + fputs (line, file); + pos += len; + o++; + } + fputc ('\n', file); + + if (output) + fprintf (file, "%s\n%s --output=%s\n", prfx, prfx, output); +} + +void Solver::initbwsigs () { + assert (!bwsigs); + size_t bytes = 2 * size * sizeof *bwsigs; + bwsigs = (unsigned*) mem.callocate (bytes); +} + +void Solver::rszbwsigs (int newsize) { + assert (bwsigs); + size_t old_bytes = 2 * size * sizeof *bwsigs; + size_t new_bytes = 2 * newsize * sizeof *bwsigs; + bwsigs = (unsigned*) mem.recallocate (bwsigs, old_bytes, new_bytes); +} + +void Solver::clrbwsigs () { + size_t bytes = 2 * size * sizeof *bwsigs; + memset (bwsigs, 0, bytes); +} + +void Solver::delbwsigs () { + size_t bytes = 2 * size * sizeof *bwsigs; + mem.deallocate (bwsigs, bytes); + bwsigs = 0; +} + +void Solver::initorgs () { + size_t bytes = 2 * (maxvar + 1) * sizeof *orgs; + orgs = (Orgs*) mem.callocate (bytes); +} + +void Solver::delorgs () { + for (int lit = 2; lit <= 2*maxvar+1; lit++) orgs[lit].release (mem); + size_t bytes = 2 * (maxvar + 1) * sizeof *orgs; + mem.deallocate (orgs, bytes); + orgs = 0; +} + +void Solver::initfwds () { + size_t bytes = 2 * (maxvar + 1) * sizeof *fwds; + fwds = (Fwds*) mem.callocate (bytes); +} + +void Solver::delfwds () { + for (int lit = 2; lit <= 2*maxvar+1; lit++) fwds[lit].release (mem); + size_t bytes = 2 * (maxvar + 1) * sizeof *fwds; + mem.deallocate (fwds, bytes); + fwds = 0; +} + +void Solver::initfwsigs () { + assert (!fwsigs); + size_t bytes = 2 * (maxvar + 1) * sizeof *fwsigs; + fwsigs = (unsigned*) mem.callocate (bytes); +} + +void Solver::delfwsigs () { + size_t bytes = 2 * (maxvar + 1) * sizeof *fwsigs; + mem.deallocate (fwsigs, bytes); + fwsigs = 0; +} + +void Solver::initprfx (const char * newprfx) { + prfx = (char*) mem.allocate (strlen (newprfx) + 1); + strcpy (prfx, newprfx); +} + +void Solver::delprfx () { + assert (prfx); + mem.deallocate (prfx, strlen (prfx) + 1); +} + +#define OPT(n,v,mi,ma) \ +do { opts.add (mem, # n, v, &opts.n, mi, ma); } while (0) + +void Solver::initerm (void) { + terminal = (out == stdout) && isatty(1); +} + +void Solver::init (int initialmaxvar) +{ + maxvar = initialmaxvar; + size = 1; + while (maxvar >= size) + size *= 2; + queue = 0; + queue2 = 0; + level = 0; + conflict = 0; + hinc = 128; + agility = 0; + typecount = 1; + lastype = 0; + out = stdout; + initerm (); + measure = true; + iterating = false; + elimode = false; + blkmode = false; + puremode = false; + asymode = false; + extending = false; + assert (!initialized); + + vars = (Var*) mem.callocate (size * sizeof *vars); + for (int i = 1; i <= maxvar; i++) + vars[i].dlevel = -1; + + iirfs = 0; + + blks = (Rnk*) mem.allocate (2 * size * sizeof *blks); + elms = (Rnk*) mem.allocate (size * sizeof *elms); + jwhs = (int*) mem.callocate (2 * size * sizeof *jwhs); + occs = (Occs*) mem.callocate (2 * size * sizeof *occs); + prbs = (Rnk*) mem.allocate (size * sizeof *prbs); + repr = (int*) mem.callocate (2 * size * sizeof *repr); + rnks = (Rnk*) mem.allocate (size * sizeof *rnks); + vals = (Val*) mem.callocate (2 * size * sizeof *vals); + + for (Rnk * p = rnks + maxvar; p > rnks; p--) + p->heat = 0, p->pos = -1, schedule.decide.push (mem, p); + + for (Rnk * p = prbs + maxvar; p > prbs; p--) p->heat = 0, p->pos = -1; + for (Rnk * p = elms + maxvar; p > elms; p--) p->heat = 0, p->pos = -1; + for (Rnk * p = blks + 2*maxvar+1; p > blks+1; p--) p->heat = 0, p->pos = -1; + + bwsigs = 0; + initbwsigs (); + + orgs = 0; + fwds = 0; + fwsigs = 0; + + frames.push (mem, Frame (trail)); + + empty.lits[0] = 0; + dummy.lits[2] = 0; + + int m = INT_MIN, M = INT_MAX; + OPT (plain,0,0,1); + OPT (rtc,0,0,2); + OPT (quiet,0,0,1); + OPT (verbose,0,0,2); + OPT (print,0,0,1); + OPT (check,0,0,2); + OPT (order,3,1,9); + OPT (simprd,20,0,M); OPT (simpinc,26,0,100); OPT (simprtc,0,0,2); + OPT (merge,1,0,1); + OPT (dominate,1,0,1); + OPT (maxdoms,5*1000*1000,0,M); + OPT (otfs,1,0,1); + OPT (block,1,0,1); + OPT (blockrtc,0,0,2); OPT (blockimpl,1,0,1); + OPT (blockprd,10,1,M); OPT (blockint,300*1000,0,M); + OPT (blockotfs,1,0,1); + OPT (blockreward,100,0,10000); + OPT (blockboost,3,0,100); + OPT (heatinc,10,0,100); + OPT (luby,1,0,1); + OPT (restart,1,0,1); OPT (restartint,100,1,M); + OPT (restartinner,10,0,1000); OPT (restartouter,10,0,1000); + OPT (rebias,1,0,1); OPT (rebiasint,1000,1,M); + OPT (probe,1,0,1); + OPT (probeint,100*1000,1000,M); OPT (probeprd,10,1,M); + OPT (probertc,0,0,2); OPT (probereward,2000,0,10000); + OPT (probeboost,5,0,10000); + OPT (decompose,1,0,1); + OPT (inverse,0,0,1); OPT (inveager,0,0,1); + OPT (mtfall,0,0,1); OPT (mtfrev,1,0,1); + OPT (bumpuip,1,0,1); + OPT (bumpsort,1,0,1); OPT (bumprev,1,0,1); + OPT (bumpturbo,0,0,1); OPT (bumpbulk,0,0,1); + OPT (fresh,50,0,100); + OPT (glue,Cls::MAXGLUE,0,Cls::MAXGLUE); + OPT (slim,1,0,1); OPT (sticky,1,0,Cls::MAXGLUE); + OPT (redsub,2,0,M); + OPT (minimize,4,0,4); OPT (maxdepth,1000,2,10000); OPT (strength,100,0,M); + OPT (elim,1,0,1); + OPT (elimgain,0,m/2,M/2); + OPT (elimint,300*1000,0,M); OPT (elimprd,20,1,M); + OPT (elimrtc,0,0,2); + OPT (elimin,-10000,-m,M); + OPT (elimclim,20,0,M); + OPT (elimboost,1,0,100); + OPT (elimreward,100,0,10000); + OPT (elimasym,2,1,100); + OPT (elimasymint,100000,100,M); + OPT (elimasymreward,1000,0,M); + OPT (fwmaxlen,100,0,M);OPT (bwmaxlen,1000,0,M); OPT (reslim,20,0,M); + OPT (blkmaxlen,1000,0,M); + OPT (subst,1,0,1); OPT (ands,1,0,1); OPT (xors,1,0,1); OPT (ites,1,0,1); + OPT (minlimit,500,10,10000); OPT (maxlimit,3*1000*1000,100,M); + OPT (dynred,4,-1,100000); + OPT (liminitmode,1,0,1); + OPT (limincmode,0,0,1); + OPT (liminitconst,2000,0,1000*1000); + OPT (liminitmax,20000,0,10*1000*1000); + OPT (liminitpercent,10,0,1000); + OPT (liminconst1,2000,0,100*1000); + OPT (liminconst2,1000,0,100*1000); + OPT (limincpercent,10,0,1000); + OPT (enlinc,20,0,1000); + OPT (shrink,2,0,2); OPT (shrinkfactor,100,1,1000); + OPT (random,1,0,1); OPT (spread,2000,0,M); OPT (seed,0,0,M); + OPT (skip,25,0,100); + opts.set ("output", (const char*) 0); + + initprfx ("c "); + initialized = true; +} + +void Solver::initiirfs () { + if (opts.order < 2) return; + size_t bytes = size * (opts.order - 1) * sizeof *iirfs; + iirfs = (int *) mem.allocate (bytes); + for (Var * v = vars + 1; v <= vars + maxvar; v++) + for (int i = 1; i < opts.order; i++) + iirf (v, i) = -1; +} + +void Solver::rsziirfs (int newsize) { + if (opts.order < 2) return; + size_t old_bytes = size * (opts.order - 1) * sizeof *iirfs; + size_t new_bytes = newsize * (opts.order - 1) * sizeof *iirfs; + iirfs = (int *) mem.reallocate (iirfs, old_bytes, new_bytes); +} + +void Solver::deliirfs () { + assert (iirfs); + assert (opts.order >= 2); + size_t bytes = size * (opts.order - 1) * sizeof *iirfs; + mem.deallocate (iirfs, bytes); + iirfs = 0; +} + +void Solver::delclauses (Anchor & anchor) { + Cls * prev; + for (Cls * p = anchor.head; p; p = prev) { + p->bytes (); prev = p->prev; mem.deallocate (p, p->bytes ()); + } + anchor.head = anchor.tail = 0; +} + +void Solver::reset () { + assert (initialized); + initialized = false; +#ifndef NDEBUG + delprfx (); + size_t bytes; + for (int lit = 2; lit <= 2 * maxvar + 1; lit++) occs[lit].bins.release (mem); + for (int lit = 2; lit <= 2 * maxvar + 1; lit++) occs[lit].large.release (mem); + bytes = 2 * size * sizeof *occs; mem.deallocate (occs, bytes); + bytes = 2 * size * sizeof *vals; mem.deallocate (vals, bytes); + bytes = 2 * size * sizeof *repr; mem.deallocate (repr, bytes); + bytes = 2 * size * sizeof *jwhs; mem.deallocate (jwhs, bytes); + bytes = 2 * size * sizeof *blks; mem.deallocate (blks, bytes); + bytes = size * sizeof *vars; mem.deallocate (vars, bytes); + bytes = size * sizeof *prbs; mem.deallocate (prbs, bytes); + bytes = size * sizeof *rnks; mem.deallocate (rnks, bytes); + bytes = size * sizeof *elms; mem.deallocate (elms, bytes); + delclauses (original); + delclauses (binary); + for (int glue = 0; glue <= opts.glue; glue++) + delclauses (learned[glue]); + delclauses (fresh); + if (iirfs) deliirfs (); + if (orgs) delorgs (); + if (fwds) delfwds (); + if (bwsigs) delbwsigs (); + if (fwsigs) delfwsigs (); + schedule.block.release (mem); + schedule.elim.release (mem); + schedule.decide.release (mem); + schedule.probe.release (mem); + opts.opts.release (mem); + trail.release (mem); + frames.release (mem); + levels.release (mem); + trash.release (mem); + gate.release (mem); + strnd.release (mem); + saved.release (mem); + elits.release (mem); + plits.release (mem); +#ifdef PRECOCHECK + check.release (mem); +#endif + units.release (mem); + lits.release (mem); + seen.release (mem); + assert (!mem); +#endif +} + +void Solver::fxopts () { + assert (!opts.fixed); + opts.fixed = true; + initiirfs (); + if (!opts.plain) return; + opts.merge = 0; + opts.block = 0; + opts.dominate = 0; + opts.rebias = 0; + opts.probe = 0; + opts.decompose = 0; + opts.minimize = 2; + opts.elim = 0; + opts.random = 0; +} + +void Solver::propts () { + assert (opts.fixed); + opts.printoptions (out, prfx); + fflush (out); +} + +void Solver::prstats () { + double overalltime = stats.seconds (); + fprintf (out, "%s%d conflicts, %d decisions, %d random\n", prfx, + stats.conflicts, stats.decisions, stats.random); + fprintf (out, "%s%d iterations, %d restarts, %d skipped\n", prfx, + stats.iter, stats.restart.count, stats.restart.skipped); + fprintf (out, "%s%d enlarged, %d shrunken, %d rescored, %d rebiased\n", prfx, + stats.enlarged, stats.shrunken, stats.rescored, stats.rebias.count); + fprintf (out, "%s%d simplifications, %d reductions\n", prfx, + stats.simps, stats.reductions); + fprintf (out, "%s\n", prfx); + fprintf (out, "%svars: %d fixed, %d equiv, %d elim, %d pure, %d zombies\n", + prfx, + stats.vars.fixed, stats.vars.equiv, + stats.vars.elim, stats.vars.pure, stats.vars.zombies); + fprintf (out, "%selim: %lld resolutions, %d phases, %d rounds\n", prfx, + stats.elim.resolutions, stats.elim.phases, stats.elim.rounds); + fprintf (out, "%sextd: %d forced, %d assumed, %d flipped\n", prfx, + stats.extend.forced, stats.extend.assumed, stats.extend.flipped); + fprintf (out, "%ssbst: %.0f%% subst, " + "%.1f%% nots, %.1f%% ands, %.1f%% xors, %.1f%% ites\n", prfx, + percent (stats.vars.subst,stats.vars.elim), + percent (stats.subst.nots.count,stats.vars.subst), + percent (stats.subst.ands.count,stats.vars.subst), + percent (stats.subst.xors.count,stats.vars.subst), + percent (stats.subst.ites.count,stats.vars.subst)); + fprintf (out, "%sarty: %.2f ands %.2f xors average arity\n", prfx, + average (stats.subst.ands.len, stats.subst.ands.count), + average (stats.subst.xors.len, stats.subst.xors.count)); + fprintf (out, "%sprbe: %d probed, %d phases, %d rounds\n", prfx, + stats.probe.variables, stats.probe.phases, stats.probe.rounds); + fprintf (out, "%sprbe: %d failed, %d lifted, %d merged\n", prfx, + stats.probe.failed, stats.probe.lifted, stats.probe.merged); + fprintf (out, "%ssccs: %d non trivial, %d fixed, %d merged\n", prfx, + stats.sccs.nontriv, stats.sccs.fixed, stats.sccs.merged); +#ifndef NSTATSPRECO + long long l1s = stats.sigs.bw.l1.srch + stats.sigs.fw.l1.srch; + long long l1h = stats.sigs.bw.l1.hits + stats.sigs.fw.l1.hits; + long long l2s = stats.sigs.bw.l2.srch + stats.sigs.fw.l2.srch; + long long l2h = stats.sigs.bw.l2.hits + stats.sigs.fw.l2.hits; + long long bws = stats.sigs.bw.l1.srch + stats.sigs.bw.l2.srch; + long long bwh = stats.sigs.bw.l1.hits + stats.sigs.bw.l2.hits; + long long fws = stats.sigs.fw.l1.srch + stats.sigs.fw.l2.srch; + long long fwh = stats.sigs.fw.l1.hits + stats.sigs.fw.l2.hits; + long long hits = bwh + fwh, srch = bws + fws; + if (opts.verbose > 1) { + fprintf (out, "%ssigs: %13lld srch %3.0f%% hits, %3.0f%% L1, %3.0f%% L2\n", + prfx, + srch, percent (hits,srch), percent (l1h,l1s), percent(l2h,l2s)); + fprintf (out, + "%s fw: %13lld %3.0f%% %3.0f%% hits, %3.0f%% L1, %3.0f%% L2\n", + prfx, + fws, percent (fws,srch), percent (fwh,fws), + percent (stats.sigs.fw.l1.hits, stats.sigs.fw.l1.srch), + percent (stats.sigs.fw.l2.hits, stats.sigs.fw.l2.srch)); + fprintf (out, + "%s bw: %13lld %3.0f%% %3.0f%% hits, %3.0f%% L1, %3.0f%% L2\n", + prfx, + bws, percent (bws,srch), percent (bwh,bws), + percent (stats.sigs.bw.l1.hits, stats.sigs.bw.l1.srch), + percent (stats.sigs.bw.l2.hits, stats.sigs.bw.l2.srch)); + } else + fprintf (out, + "%ssigs: %lld searched, %.0f%% hits, %.0f%% L1, %.0f%% L2\n", + prfx, + srch, percent (hits,srch), percent (l1h,l1s), percent(l2h,l2s)); +#endif + long long alllits = stats.lits.added + stats.mins.deleted; + fprintf (out, + "%smins: %lld lrnd, %.0f%% del, %lld strng, %lld inv, %d dpth\n", + prfx, + stats.lits.added, + percent (stats.mins.deleted, alllits), + stats.mins.strong, stats.mins.inverse, stats.mins.depth); + fprintf (out, + "%ssubs: %d fw, %d bw, %d dynamic, %d org, %d doms, %d gc\n", + prfx, + stats.subs.fw, stats.subs.bw, + stats.subs.dyn, stats.subs.org, + stats.subs.doms, stats.subs.red); + fprintf (out, + "%sblkd: %lld resolutions, %d phases, %d rounds\n", + prfx, + stats.blkd.resolutions, + stats.blkd.phases, stats.blkd.rounds); + fprintf (out, + "%sblkd: %d = %d implicit + %d explicit\n", + prfx, + stats.blkd.impl + stats.blkd.expl, + stats.blkd.impl, stats.blkd.expl); + assert (stats.vars.pure == + stats.pure.elim + stats.pure.blkd + stats.pure.expl); + fprintf (out, "%spure: %d = %d explicit + %d elim + %d blkd\n", + prfx, + stats.vars.pure, + stats.pure.expl, stats.pure.elim, stats.pure.blkd); + assert (stats.vars.zombies == + stats.zombies.elim + stats.zombies.blkd + stats.zombies.expl); + fprintf (out, "%szmbs: %d = %d explicit + %d elim + %d blkd\n", + prfx, + stats.vars.zombies, + stats.zombies.expl, stats.zombies.elim, stats.zombies.blkd); + fprintf (out, + "%sstrs: %d forward, %d backward, %d dynamic, %d org, %d asym\n", + prfx, + stats.str.fw, stats.str.bw, stats.str.dyn, + stats.str.org, stats.str.asym); + fprintf (out, "%sotfs: dynamic %d = %d bin + %d trn + %d large\n", + prfx, + stats.otfs.dyn.bin + stats.otfs.dyn.trn + stats.otfs.dyn.large, + stats.otfs.dyn.bin, stats.otfs.dyn.trn, stats.otfs.dyn.large); + fprintf (out, "%sotfs: static %d = %d bin + %d trn + %d large\n", + prfx, + stats.otfs.stat.bin + stats.otfs.stat.trn + stats.otfs.stat.large, + stats.otfs.stat.bin, stats.otfs.stat.trn, stats.otfs.stat.large); + fprintf (out, + "%sglue: %.2f avg, %lld slimmed = %.2f per conflict\n", + prfx, + average (stats.glue.sum, stats.glue.count), + stats.glue.slimmed, + average (stats.glue.slimmed, stats.conflicts)); + assert (stats.doms.count >= stats.doms.level1); + assert (stats.doms.level1 >= stats.doms.probing); + fprintf (out, "%sdoms: %d dominators, %d high, %d low\n", prfx, + stats.doms.count, + stats.doms.count - stats.doms.level1, + stats.doms.level1 - stats.doms.probing); + long long props = stats.props.srch + stats.props.simp; + fprintf (out, "%svsts: %lld visits, %.2f per prop, %.0f%% blkd", + prfx, + stats.visits, average (stats.visits, props), + percent (stats.blocked, stats.visits)); +#ifndef NSTATSPRECO + fprintf (out, ", %.0f%% trn", + percent (stats.ternaryvisits, stats.visits)); +#endif + fputc ('\n', out); + double othrtime = overalltime - stats.simptime - stats.srchtime; + fprintf (out, "%stime: " + "%.1f = " + "%.1f srch (%.0f%%) + " + "%.1f simp (%.0f%%) + " + "%.1f othr (%.0f%%)\n", + prfx, + overalltime, + stats.srchtime, percent (stats.srchtime, overalltime), + stats.simptime, percent (stats.simptime, overalltime), + othrtime, percent (othrtime, overalltime)); + fprintf (out, "%sprps: %lld srch props, %.2f megaprops per second\n", + prfx, stats.props.srch, + (stats.srchtime>0) ? stats.props.srch/1e6/stats.srchtime : 0); + fprintf (out, "%sclss: %d recycled\n", prfx, + stats.clauses.gc); + fprintf (out, "%s\n", prfx); + fprintf (out, "%s%.1f seconds, %.0f MB max, %.0f MB recycled\n", prfx, + overalltime, mb (mem.getMax ()), mb (stats.collected)); + fflush (out); +} + +inline void Solver::assign (int lit) { + assert (!vals [lit]); + vals[lit] = 1; vals[lit^1] = -1; + Var & v = vars[lit/2]; + assert ((v.type == ELIM) == extending); + if (!(v.dlevel = level)) { + if (v.type == EQUIV) { + assert (repr[lit]); + assert (stats.vars.equiv); + stats.vars.equiv--; + stats.vars.fixed++; + v.type = FIXED; + } else { + assert (!repr[lit]); + if (v.type == FREE) { + stats.vars.fixed++; + v.type = FIXED; + } else assert (v.type == ZOMBIE || v.type == PURE); + } + simplified = true; + } + if (measure) { + Val val = lit2val (lit); + agility -= agility/10000; + if (v.phase && v.phase != val) agility += 1000; + v.phase = val; + } + v.tlevel = trail; + trail.push (mem, lit); +#ifndef NLOGPRECO + printf ("%sLOG assign %d at level %d <=", prfx, lit, level); + if (v.binary) printf (" %d %d\n", lit, v.reason.lit); + else if (v.reason.cls) + printf (" %d %d %d%s\n", + v.reason.cls->lits[0], + v.reason.cls->lits[1], + v.reason.cls->lits[2], + v.reason.cls->size > 3 ? " ..." : ""); + else if (!level) printf (" top level\n"); + else printf (" decision\n"); +#endif +} + +inline void Solver::assume (int lit, bool inclevel) { + if (inclevel) { + frames.push (mem, Frame (trail)); + level++; + LOG ("assume new level " << level); + assert (level + 1 == frames); + LOG ("assuming " << lit); + } else { + assert (!level); + LOG ("permanently assume " << lit << " on top level"); + } + Var & v = vars[lit/2]; v.binary = false; v.reason.cls = 0; + v.dominator = lit; + assign (lit); +} + +inline void Solver::imply (int lit, int reason) { + assert (lit/2 != reason/2); + assert (vals[reason] < 0); + assert (vars[reason/2].dlevel == level); + Var & v = vars[lit/2]; + if (level) v.binary = true, v.reason.lit = reason; + else v.binary = false, v.reason.lit = 0; + if (level) v.dominator = vars[reason/2].dominator; + assign (lit); +} + +inline int Solver::dominator (int lit, Cls * reason, bool & contained) { + if (!opts.dominate) return 0; + if (asymode) return 0; + if (opts.maxdoms <= stats.doms.count) return 0; + contained = false; + assert (level > 0); + int vdom = 0, other, oldvdom; + Var * u; + for (const int * p = reason->lits; vdom >= 0 && (other = *p); p++) { + if (other == lit) continue; + u = vars + (other/2); + if (!u->dlevel) continue; + if (u->dlevel < level) { vdom = -1; break; } + int udom = u->dominator; + assert (udom); + if (vdom) { + assert (vdom > 0); + if (udom != vdom) vdom = -1; + } else vdom = udom; + } + assert (vdom); + if (vdom <= 0) return vdom; + assert (vals[vdom] > 0); + LOG (vdom << " dominates " << lit); + for (const int * p = reason->lits; !contained && (other = *p); p++) + contained = (other^1) == vdom; + if (contained) goto DONE; + oldvdom = vdom; vdom = 0; + for (const int * p = reason->lits; (other = *p); p++) { + if (other == lit) continue; + assert (vals[other] < 0); + u = vars + other/2; + if (!u->dlevel) continue; + assert (u->dlevel == level); + assert (u->dominator == oldvdom); + other ^= 1; + assert (other != oldvdom); + if (other == vdom) continue; + if (vdom) { + while (!u->mark && + (other = (assert (u->binary), 1^u->reason.lit)) != oldvdom && + other != vdom) { + assert (vals[other] > 0); + u = vars + other/2; + assert (u->dlevel == level); + assert (u->dominator == oldvdom); + } + while (vdom != other) { + u = vars + (vdom/2); + assert (u->mark); + u->mark = 0; + assert (u->binary); + vdom = 1^u->reason.lit; + } + if (vdom == oldvdom) break; + } else { + vdom = 1^u->reason.lit; + if (vdom == oldvdom) break; + assert (vals[vdom] > 0); + other = vdom; + do { + u = vars + other/2; + assert (u->dlevel == level); + assert (u->dominator == oldvdom); + assert (!u->mark); + u->mark = 1; + assert (u->binary); + other = 1^u->reason.lit; + assert (vals[other] > 0); + } while (other != oldvdom); + } + } + other = vdom; + while (other != oldvdom) { + u = vars + other/2; + assert (u->dlevel == level); + assert (u->dominator == oldvdom); + assert (u->mark); + u->mark = 0; + assert (u->binary); + other = 1^u->reason.lit; + assert (vals[other] > 0); + } + + if (vdom == oldvdom) goto DONE; + + assert (vdom); + LOG (vdom << " also dominates " << lit); + assert (!contained); + for (const int * p = reason->lits; !contained && (other = *p); p++) + contained = (other^1) == vdom; + +DONE: + stats.doms.count++; + if (level == 1) stats.doms.level1++; + if (!measure) { assert (level == 1); stats.doms.probing++; } + if (contained) { + reason->garbage = true; + stats.subs.doms++; + LOG ("dominator clause is subsuming"); + } + + return vdom; +} + +inline void Solver::unit (int lit) { + Var * v; + Val val = vals[lit]; + assert (!level); + if (val < 0) { + LOG ("conflict after adding unit"); conflict = ∅ return; + } + if (!val) { + v = vars + (lit/2); + v->binary = false, v->reason.cls = 0; + assign (lit); + } + int other = find (lit); + if (other == lit) return; + val = vals[other]; + if (val < 0) { + LOG ("conflict after adding unit"); conflict = ∅ return; + } + if (val) return; + v = vars + (other/2); + v->binary = false, v->reason.cls = 0; + assign (other); +} + +inline unsigned Solver::gluelits () { + const int * eol = lits.end (); + int lit, found = 0; + unsigned res = 0; + assert (uip); + for (const int * p = lits.begin (); p < eol; p++) { + lit = *p; + assert (val (lit) < 0); + Var * v = vars + (lit/2); + int dlevel = v->dlevel; + if (dlevel == level) { assert (!found); found = lit; continue; } + assert (dlevel > 0); + Frame * f = &frames[dlevel]; + if (f->contained) continue; + f->contained = true; + res++; + } + assert (found == uip); + for (const int * p = lits.begin (); p < eol; p++) + frames[vars[*p/2].dlevel].contained = false; + return res; +} + +inline void Solver::slim (Cls * cls) { + if (!opts.slim) return; + if (!level) return; + assert (cls); + if (!cls->lnd) return; + assert (!cls->binary); + unsigned oldglue = cls->glue; + if (!oldglue) return; + const int * p = cls->lits; + unsigned newglue = 0; + int lit, nonfalse = 0; + while ((lit = *p++)) { + Val val = vals[lit]; + if (val >= 0 && nonfalse++) { newglue = oldglue; break; } + Var * v = vars + (lit/2); + int dlevel = v->dlevel; + if (dlevel <= 0) continue; + assert (dlevel < frames); + Frame * f = &frames[dlevel]; + if (f->contained) continue; + if (++newglue >= oldglue) break; + f->contained = true; + } + while (p > cls->lits) { + lit = *--p; + if (!lit) continue; + Var * v = vars + (lit/2); + int dlevel = v->dlevel; + if (dlevel <= 0) continue; + assert (dlevel < frames); + Frame * f = &frames[dlevel]; + f->contained = false; + } + if (cls->glued) { + assert (oldglue >= newglue); + if (oldglue == newglue) return; + assert (newglue >= 1); + LOG ("slimmed glue from " << oldglue << " to " << newglue); + } else LOG ("new glue " << newglue); + assert (newglue <= (unsigned) opts.glue); + if (!cls->fresh) dequeue (anchor (cls), cls); + cls->glue = newglue; + if (!cls->fresh) push (anchor (cls), cls); + if (cls->glued) stats.glue.slimmed++; + stats.glue.count++; + stats.glue.sum += newglue; + cls->glued = true; +} + +inline void Solver::force (int lit, Cls * reason) { + assert (reason); + assert (!reason->binary); + Val val = vals[lit]; + if (val < 0) { LOG ("conflict forcing literal"); conflict = reason; } + if (val) return; +#ifndef NDEBUG + for (const int * p = reason->lits; *p; p++) + if (*p != lit) assert (vals[*p] < 0); +#endif + Var * v = vars + (lit/2); + int vdom; + bool sub; + if (!level) { + v->binary = false, v->reason.cls = 0; + } else if (!lits && (vdom = dominator (lit, reason, sub)) > 0) { + v->dominator = vdom; + assert (vals[vdom] > 0); + vdom ^= 1; + LOG ("dominating learned clause " << vdom << ' ' << lit); + assert (!lits); + lits.push (mem, vdom); + lits.push (mem, lit); + bool lnd = reason->lnd || !sub; + clause (lnd, lnd); + v->binary = true, v->reason.lit = vdom; + } else { + v->binary = false, v->reason.cls = reason; + reason->locked = true; + if (reason->lnd) stats.clauses.lckd++; + v->dominator = lit; + } + assign (lit); +} + +inline void Solver::jwh (Cls * cls) { + //if (cls->lnd) return; // TODO better not ? + int * p; + for (p = cls->lits; *p; p++) + ; + int size = p - cls->lits; + int inc = logsize (size); + while (p > cls->lits) { + int l = *--p; + jwhs[l] += inc; + if (jwhs[l] < 0) die ("maximum large JWH score exceeded"); + } +} + +int Solver::find (int a) { + assert (2 <= a && a <= 2 * maxvar + 1); + int res, tmp; + for (res = a; (tmp = repr[res]); res = tmp) + ; + for (int fix = a; (tmp = repr[fix]) && tmp != res; fix = tmp) + repr[fix] = res, repr[fix^1] = res^1; + return res; +} + +inline void Solver::merge (int l, int k, int & merged) { + int a, b; + if (!opts.merge) return; + assert (!elimode); + assert (!blkmode); + if ((a = find (l)) == (b = find (k))) return; + assert (a/2 != b/2); +#ifndef NLOGPRECO + int m = min (a, b); + LOG ("merge " << l << " and " << k << " to " << m); + if (k != m) LOG ("learned clause " << k << ' ' << (m^1)); + if (k != m) LOG ("learned clause " << (k^1) << ' ' << m); + if (l != m) LOG ("learned clause " << l << ' ' << (m^1)); + if (l != m) LOG ("learned clause " << (l^1) << ' ' << m); +#endif + if (a < b) repr[k] = repr[b] = a, repr[k^1] = repr[b^1] = a^1; + else repr[l] = repr[a] = b, repr[l^1] = repr[a^1] = b^1; + assert (vars[a/2].type == FREE && vars[b/2].type == FREE); + vars[max (a,b)/2].type = EQUIV; + stats.vars.merged++; + stats.vars.equiv++; + simplified = true; + merged++; +} + +Cls * Solver::clause (bool lnd, unsigned glue) { + assert (asymode || !elimode || !lnd); + assert (lnd || !glue); + Cls * res = 0; +#ifndef NLOGPRECO + std::cout << prfx << "LOG " << (lnd ? "learned" : "original") << " clause"; + for (const int * p = lits.begin (); p < lits.end (); p++) + std::cout << ' ' << *p; + std::cout << std::endl; +#endif +#ifndef NDEBUG + for (int i = 0; i < lits; i++) + assert (vars[lits[i]/2].type != ELIM); +#endif + if (lits == 0) { + LOG ("conflict after added empty clause"); + conflict = ∅ + } else if (lits == 1) { + int lit = lits[0]; + Val val; + if ((val = vals[lit]) < 0) { + LOG ("conflict after adding falsified unit clause"); + conflict = ∅ + } else if (!val) unit (lit); + } else { + if (lits >= (int)Cls::MAXSZ) die ("maximal clause size exceeded"); + size_t bytes = Cls::bytes (lits); + res = (Cls *) mem.callocate (bytes); + res->lnd = lnd; + if (!lnd) stats.clauses.irr++; + res->size = lits; + int * q = res->lits, * eol = lits.end (); + for (const int * p = lits.begin (); p < eol; p++) + *q++ = *p; + *q = 0; + if (lits == 2) res->binary = true, stats.clauses.bin++; + else { + res->glue = min ((unsigned)opts.glue,glue); + res->fresh = res->lnd; + if (lnd) stats.clauses.lnd++; + else stats.clauses.orig++; + } + connect (res); + } + lits.shrink (); + simplified = true; + return res; +} + +inline void Solver::marklits () { + for (const int * p = lits.begin (); p < lits.end (); p++) + vars[*p/2].mark = lit2val (*p); +} + +inline void Solver::unmarklits () { + for (const int * p = lits.begin (); p < lits.end (); p++) + vars[*p/2].mark = 0; +} + +inline bool Solver::bwsub (unsigned sig, Cls * c) { + assert (!c->trash && !c->dirty && !c->garbage); + limit.budget.bw.sub--; + int count = lits; + if (c->size < (unsigned) count) return false; + INC (sigs.bw.l1.srch); + if (!sigsubs (sig, c->sig)) { INC (sigs.bw.l1.hits); return false; } + int lit; + for (int * p = c->lits; count && (lit = *p); p++) { + Val u = lit2val (lit), v = vars[lit/2].mark; + if (u == v) count--; + } + return !count; +} + +int Solver::bwstr (unsigned sig, Cls * c) { + assert (!c->trash && !c->dirty && !c->garbage); + limit.budget.bw.str--; + int count = lits; + if (c->size < (unsigned) count) return 0; + INC (sigs.bw.l1.srch); + if (!sigsubs (sig, c->sig)) { INC (sigs.bw.l1.hits); return 0; } + int lit, res = 0; + for (int * p = c->lits; count && (lit = *p); p++) { + Val u = lit2val (lit), v = vars[lit/2].mark; + if (abs (u) != abs (v)) continue; + if (u == -v) { if (res) return 0; res = lit; } + count--; + } + assert (count >= 0); + res = count ? 0 : res; + + return res; +} + +void Solver::remove (int del, Cls * c) { + assert (!c->trash && !c->garbage && !c->dirty && !c->gate); + assert (c->lits[0] && c->lits[1]); + if (c->binary) { + int pos = (c->lits[1] == del); + assert (c->lits[pos] == del); + LOG ("will not remove " << del << " but will simply produce unit instead"); + unit (c->lits[!pos]); + } else { + disconnect (c); + int * p = c->lits, lit; + while ((lit = *p) != del) assert (lit), p++; + while ((lit = *++p)) p[-1] = lit; + p[-1] = 0; + assert (p - c->lits >= 3); + if (p - c->lits == 3) { + if (c->lnd) { + assert (stats.clauses.lnd > 0); + stats.clauses.lnd--; + } else { + assert (stats.clauses.orig > 0); + stats.clauses.orig--; + } + c->binary = true; + stats.clauses.bin++; + } + setsig (c); + connect (c); + if (elimode || blkmode) touch (del); + simplified = true; +#ifndef NLOGPRECO + LOG ("removed " << del << " and got"); + dbgprint ("LOG learned clause ", c); +#endif + } +} + +void Solver::bworgs () { + if (lits <= 1) return; + limit.budget.bw.str += 2; + limit.budget.bw.sub += 4; + marklits (); + int first = 0; + int minlen = INT_MAX; + for (int i = 0; i < lits; i++) { + int other = lits[i]; + int len = orgs[other]; + if (len < minlen) first = other, minlen = len; + } + unsigned sig = litsig (); + assert (first); + INC (sigs.bw.l2.srch); + if (!sigsubs (sig, bwsigs[first])) INC (sigs.bw.l2.hits); + else if (orgs[first] <= opts.bwmaxlen) + for (int i = 0; limit.budget.bw.sub >= 0 && i < orgs[first]; i++) { + Cls * other = orgs[first][i]; + assert (!other->locked); + if (other->trash || other->dirty || other->garbage) continue; + if (!bwsub (sig, other)) continue; +#ifndef NLOGPRECO + dbgprint ("LOG static backward subsumed clause ", other); +#endif + stats.subs.bw++; + limit.budget.bw.sub += 12; + dump (other); + } + int second = 0; + minlen = INT_MAX; + for (int i = 0; i < lits; i++) { + int other = lits[i]; + if (other == first) continue; + int len = orgs[other]; + if (len < minlen) second = other, minlen = len; + } + assert (second); + if (orgs[first^1] < minlen) second = (first^1); + for (int round = 0; round <= 1; round++) { + int start = round ? second : first; + INC (sigs.bw.l2.srch); + if (!sigsubs (sig, bwsigs[start])) { INC (sigs.bw.l2.hits); continue; } + Orgs & org = orgs[start]; + if (org > opts.bwmaxlen) continue; + for (int i = 0; limit.budget.bw.str >= 0 && i < org; i++) { + Cls * other = org[i]; + assert (!other->locked); + if (other->trash || other->dirty || other->garbage) continue; + int del = bwstr (sig, other); + if (!del) continue; + LOG ("static backward strengthened clause by removing " << del); + stats.str.bw++; + limit.budget.bw.str += 10; + remove (del, other); + assert (litsig () == sig); + } + } + unmarklits (); +} + +void Solver::bwoccs (bool & lnd) { + if (lits <= 1) return; + limit.budget.bw.sub += lnd ? 30 : 10; + limit.budget.bw.str += lnd ? 20 : 8; + marklits (); + unsigned sig = litsig (); + for (int i = 0; i < lits; i++) { + int first = lits[i]; + if (limit.budget.bw.sub >= 0) { + INC (sigs.bw.l2.srch); + if (!sigsubs (sig, bwsigs[first])) INC (sigs.bw.l2.hits); + else if (occs[first].large <= opts.bwmaxlen) { + for (int i = 0; + limit.budget.bw.sub >= 0 && i < occs[first].large; i++) { + Cls * other = occs[first].large[i].cls; + assert (!other->dirty && !other->trash); + if (other->garbage) continue; + if (!bwsub (sig, other)) continue; + if (!other->lnd && lnd) lnd = false; + LOG ((level ? "dynamic" : "static") + << " backward subsumed " + << (other->lnd ? "learned" : "original") + << " clause"); +#ifndef NLOGPRECO + { + std::cout << prfx << "LOG subsumed clause"; + for (const int * p = other->lits; *p; p++) + std::cout << ' ' << *p; + std::cout << std::endl; + } +#endif + if (level) { + stats.subs.dyn++; + if (!other->lnd) stats.subs.org++; + } else stats.subs.bw++; + limit.budget.bw.sub += 20; + if (other->locked) other->garbage = true; else recycle (other); + } + } + } + if (limit.budget.bw.str >= 0) { + INC (sigs.bw.l2.srch); + if (!sigsubs (sig, bwsigs[first])) INC (sigs.bw.l2.hits); + else if (occs[first].large <= opts.bwmaxlen) { + for (int i = 0; + limit.budget.bw.sub >= 0 && i < occs[first].large; + i++) { + Cls* other = occs[first].large[i].cls; + assert (!other->dirty && !other->trash); + if (other->locked || other->garbage) continue; + int del = bwstr (sig, other); + if (!del) continue; + LOG ((level ? "dynamic" : "static") + << " backward strengthened " + << (other->lnd ? "learned" : "original") + << " clause by removing " + << del); +#ifndef NLOGPRECO + { + std::cout << prfx << "LOG strengthened clause"; + for (const int * p = other->lits; *p; p++) + std::cout << ' ' << *p; + std::cout << std::endl; + } +#endif + if (level) { + stats.str.dyn++; + if (!other->lnd) stats.str.org++; + } else stats.str.bw++; + limit.budget.bw.str += 15; + remove (del, other); + if (level) strcls (other); + } + } + } + } + unmarklits (); +} + +inline bool Solver::fwsub (unsigned sig, Cls * c) { + assert (!c->trash && !c->dirty && !c->garbage); + limit.budget.fw.sub--; + INC (sigs.fw.l1.srch); + if (!sigsubs (c->sig, sig)) { INC (sigs.fw.l1.hits); return false; } + int lit; + for (const int * p = c->lits; (lit = *p); p++) { + Val u = lit2val (lit), v = vars[lit/2].mark; + if (u != v) return false; + } + return true; +} + +inline int Solver::fwstr (unsigned sig, Cls * c) { + assert (!c->trash && !c->dirty && !c->garbage); + limit.budget.fw.str--; + INC (sigs.fw.l1.srch); + if (!sigsubs (c->sig, sig)) { INC (sigs.fw.l1.hits); return 0; } + int res = 0, lit; + for (const int * p = c->lits; (lit = *p); p++) { + Val u = lit2val (lit), v = vars[lit/2].mark; + if (u == v) continue; + if (u != -v) return 0; + if (res) return 0; + res = (lit^1); + } + return res; +} + +bool Solver::fworgs () { + if (lits <= 1) return false; + limit.budget.fw.str += 3; + limit.budget.fw.sub += 5; + assert (fwds); + marklits (); + unsigned sig = litsig (); + bool res = false; + if (lits >= 2) { + for (int i = 0; !res && limit.budget.fw.sub >= 0 && i < lits; i++) { + int lit = lits[i]; + INC (sigs.fw.l2.srch); + if (!(fwsigs[lit] & sig)) { INC (sigs.fw.l2.hits); continue; } + Fwds & f = fwds[lit]; + if (f > opts.fwmaxlen) continue; + for (int j = 0; !res && limit.budget.fw.sub >= 0 && j < f; j++) { + Cls * c = f[j]; + if (c->trash || c->dirty || c->garbage) continue; + res = fwsub (sig, c); + } + } + if (res) { + LOG ("new clause is subsumed"); + stats.subs.fw++; + limit.budget.fw.sub += 5; + } + } + if (!res) + for (int sign = 0; sign <= 1; sign++) + for (int i = 0; limit.budget.fw.str >= 0 && i < lits; i++) { + int lit = lits[i]; + INC (sigs.fw.l2.srch); + if (!(fwsigs[lit] & sig)) { INC (sigs.fw.l2.hits); continue; } + lit ^= sign; + Fwds & f = fwds[lit]; + if (f > opts.fwmaxlen) continue; + int del = 0; + for (int j = 0; !del && limit.budget.fw.str >= 0 && j < f; j++) { + Cls * c = f[j]; + if (c->trash || c->dirty || c->garbage) continue; + del = fwstr (sig, c); + } + if (!del) continue; + assert (sign || del/2 != lit/2); + LOG ("strengthen new clause by removing " << del); + stats.str.fw++; + limit.budget.fw.str += 8; + assert (vars[del/2].mark == lit2val (del)); + vars[del/2].mark = 0; + lits.remove (del); + sig = litsig (); + i = -1; + } + unmarklits (); + return res; +} + +void Solver::resize (int newmaxvar) { + assert (maxvar < size); + assert (newmaxvar > maxvar); + int newsize = size; + while (newsize <= newmaxvar) + newsize *= 2; + if (newsize > size) { + size_t o, n; + + o = size * sizeof * vars; + n = newsize * sizeof * vars; + vars = (Var *) mem.recallocate (vars, o, n); + + o = 2 * size * sizeof *repr; + n = 2 * newsize * sizeof *repr; + repr = (int*) mem.recallocate (repr, o, n); + + o = 2 * size * sizeof *jwhs; + n = 2 * newsize * sizeof *jwhs; + jwhs = (int*) mem.recallocate (jwhs, o, n); + + o = 2 * size * sizeof *vals; + n = 2 * newsize * sizeof *vals; + vals = (Val*) mem.recallocate (vals, o, n); + + o = 2 * size * sizeof *occs; + n = 2 * newsize * sizeof *occs; + occs = (Occs*) mem.recallocate (occs, o, n); + + ptrdiff_t diff; + char * c; + + o = size * sizeof *rnks; + n = newsize * sizeof *rnks; + c = (char *) rnks; + rnks = (Rnk*) mem.reallocate (rnks, o, n); + diff = c - (char *) rnks; + schedule.decide.fix (diff); + + o = size * sizeof *prbs; + n = newsize * sizeof *prbs; + c = (char *) prbs; + prbs = (Rnk*) mem.reallocate (prbs, o, n); + diff = c - (char *) prbs; + schedule.probe.fix (diff); + + o = size * sizeof *elms; + n = newsize * sizeof *elms; + c = (char *) elms; + elms = (Rnk*) mem.reallocate (elms, o, n); + diff = c - (char *) elms; + schedule.elim.fix (diff); + + o = 2 * size * sizeof *elms; + n = 2 * newsize * sizeof *elms; + c = (char *) blks; + blks = (Rnk*) mem.reallocate (blks, o, n); + diff = c - (char *) blks; + schedule.block.fix (diff); + + rszbwsigs (newsize); + rsziirfs (newsize); + size = newsize; + } + assert (newmaxvar < size); + while (maxvar < newmaxvar) { + Var * v = vars + ++maxvar; + v->dlevel = -1; + + for (int i = 1; i < opts.order; i++) + iirf (v, i) = -1; + + Rnk * r = rnks + maxvar; + r->heat = 0, r->pos = -1, schedule.decide.push (mem, r); + + Rnk * p = prbs + maxvar; + p->heat = 0, p->pos = -1; + + Rnk * e = elms + maxvar; + e->heat = 0, e->pos = -1; + + Rnk * b = blks + 2*maxvar; + b[0].heat = b[1].heat = 0; + b[0].pos = b[1].pos = -1; + } + assert (maxvar < size); +} + +void Solver::import () { + bool trivial = false; + int * q = lits.begin (); + const int * p, * eol = lits.end (); + for (p = lits.begin (); !trivial && p < eol; p++) { + int lit = *p, v = lit/2; + assert (1 <= v); + if (v > maxvar) resize (v); + Val tmp = vals[lit]; + if (!tmp) { + int prev = vars[v].mark; + int val = lit2val (lit); + if (prev) { + if (val == prev) continue; + assert (val == -prev); + trivial = 1; + } else { + vars[v].mark = val; + *q++ = lit; + } + } else if (tmp > 0) + trivial = true; + } + + while (p > lits.begin ()) vars[*--p/2].mark = 0; + + if (!trivial) { + lits.shrink (q); + bool lnd = false; + bwoccs (lnd); + assert (!lnd); + clause (lnd, lnd); + } + lits.shrink (); +} + +inline bool Solver::satisfied (const Cls * c) { + int lit; + for (const int * p = c->lits; (lit = *p); p++) + if (val (lit) > 0) return true; + return false; +} + +inline bool Solver::satisfied (Anchor & anchor) { + for (const Cls * p = anchor.head; p; p = p->prev) + if (!satisfied (p)) return false; + return true; +} + +bool Solver::satisfied () { + if (!satisfied (binary)) return false; + if (!satisfied (original)) return false; +#ifndef NDEBUG + for (int glue = 0; glue <= opts.glue; glue++) + if (!satisfied (learned[glue])) return false; + if (!satisfied (fresh)) return false; +#endif +#ifdef PRECOCHECK + for (const int * p = check.begin (); p < check.end (); p++) { + bool found = false; + int lit; + while ((lit = *p)) { + if (val (lit) > 0) found = true; + p++; + } + if (!found) return false; + } +#endif + return true; +} + +inline void Solver::prop2 (int lit) { + assert (vals[lit] < 0); + LOG ("prop2 " << lit); + const Stack & os = occs[lit].bins; + const int * eos = os.end (); + for (const int * p = os.begin (); p < eos; p++) { + int other = *p; + Val val = vals[other]; + if (val > 0) continue; + if (!val) { imply (other, lit); continue; } + LOG ("conflict in binary clause while propagating " << (1^lit)); + conflict = lit2conflict (dummy, lit, other); + LOG ("conflicting clause " << lit << ' ' << other); + } +} + +inline void Solver::propl (int lit) { + assert (vals[lit] < 0); + LOG ("propl " << lit); + Stack & os = occs[lit].large; + Occ * a = os.begin (), * t = os.end (), * p = a, * q = a; +CONTINUE_OUTER_LOOP: + while (p < t) { + int blit = p->blit; + Cls * cls = p++->cls; + *q++ = Occ (blit, cls); + stats.visits++; + Val val = vals[blit]; + if (val > 0) { stats.blocked++; continue; } +#ifndef NSTATSPRECO + if (cls->lits[2] && !*(cls->lits + 3)) INC (ternaryvisits); +#endif + int sum = cls->lits[0]^cls->lits[1]; + int other = sum^lit; + val = vals[other]; + q[-1].blit = other; + if (val > 0) continue; + int prev = lit, next, *l, *lits2 = cls->lits+2; + for (l = lits2; (next = *l); l++) { + *l = prev; prev = next; + if (vals[next] < 0) continue; + occs[next].large.push (mem, Occ (other, cls)); + int pos = (cls->lits[1] == lit); + cls->lits[pos] = next; + q--; goto CONTINUE_OUTER_LOOP; + } + while (l > lits2) { next = *--l; *l = prev; prev = next; } + slim (cls); + if (val) { + LOG ("conflict in large clause while propagating " << (1^lit)); + conflict = cls; +#ifndef NLOGPRECO + dbgprint ("LOG conflicting clause ", cls); +#endif + break; + } + force (other, cls); + long moved = ((char*)os.begin ()) - (char*)a; + if (moved) fix (p,moved), fix (q,moved), fix (t,moved), a = os.begin (); + } + while (p < t) *q++ = *p++; + os.shrink (q - a); +} + +bool Solver::bcp () { + if (conflict) return false; + if (!level && units) flushunits (); + if (conflict) return false; + int lit, props = 0; + for (;;) { + if (queue2 < trail) { + props++; + lit = 1^trail[queue2++]; + prop2 (lit); + if (!measure && conflict) break; + } else if (queue < trail) { + if (conflict) break; + lit = 1^trail[queue++]; + propl (lit); + if (conflict) break; + } else + break; + } + if (measure) stats.props.srch += props; + else stats.props.simp += props; + return !conflict; +} + +inline bool Solver::needtoflush () const { + return queue2 < trail; +} + +bool Solver::flush () { + assert (!level); + int fixed = queue2; + if (!bcp ()) return false; + while (fixed < trail) { + int lit = trail[fixed++]; + recycle (lit); + } + assert (!conflict); + return true; +} + +inline int Solver::phase (Var * v) { + int lit = 2 * (v - vars) + 1; + if (v->phase > 0 || + (!v->phase && (jwhs[lit^1] > jwhs[lit]))) lit ^= 1; + return lit; +} + +void Solver::extend () { + report (2, 't'); + extending = true; + int n = elits; + while (n > 0) { + int unblock = elits[--n]; + int lit = elits[--n]; + if (unblock) { + LOG ("unblocking " << lit); + Val valit = val (lit); + assert (valit); + bool forced = (valit < 0); + int other; + while ((other = elits[--n])) { + if (!forced) continue; + other = find (other); + Val v = val (other); + assert (v); + forced = (v < 0); + } + if (!forced) continue; + // TODO make this in an assertion ... + // We have 'in principle' a proof that this can not happen. + if (repr[lit]) die ("internal error extending assignment"); + LOG ("assign " << (1^lit) << " at level " << level << " <= unblock"); + vals[lit] = 1, vals[lit^1] = -1; + assert (trail[vars[lit/2].tlevel] == (1^lit)); + trail[vars[lit/2].tlevel] = lit; + stats.extend.flipped++; + } else { + LOG ("extending " << lit); + assert (!repr [lit]); + while (elits[n-1]) { + bool forced = true; + int other; + while ((other = elits[--n])) { + if (!forced) continue; + other = find (other); + if (other == lit) continue; + if (other == (lit^1)) { forced = false; continue; } + Val v = val (other); + if (v > 0) forced = false; + } + if (!forced) continue; + Val v = val (lit); + if (v) assert (v > 0); + else { assume (lit); stats.extend.forced++; } + } + if (!val (lit)) { assume (lit^1); stats.extend.assumed++; } + n--; + } + } +#ifndef NDEBUG + for (int lit = 2; lit <= 2 * maxvar + 1; lit += 2) + assert (val (lit)); +#endif + extending = false; +} + +bool Solver::decide () { + Rnk * r; + for (;;) { + if (!schedule.decide) { extend (); return false; } + r = schedule.decide.max (); + int idx = r - rnks; + int lit = 2 * idx; + if (vars[idx].type == FREE && !vals[lit]) break; + (void) schedule.decide.pop (); + } + assert (r); + stats.decisions++; + stats.sumheight += level; + if (opts.random && agility <= 10 * 100000 && rng.oneoutof (opts.spread)) { + stats.random++; + unsigned n = schedule.decide; assert (n); + unsigned s = rng.next () % n, d = rng.next () % n; + while (ggt (n, d) != 1) { + d++; if (d >= n) d = 1; + } + for (;;) { + r = schedule.decide[s]; + int lit = 2 * (r - rnks); + if (vars[lit/2].type == FREE && !vals[lit]) break; + s += d; if (s >= n) s -= n; + } + } + int lit = phase (var (r)); + assert (!vals[lit]); + LOG ("decision " << lit); + assume (lit); + iterating = false; + return true; +} + +inline bool Solver::min2 (int lit, int other, int depth) { + assert (lit != other && vals[lit] > 0); + if (vals[other] >= 0) return false; + Var * v = vars + (lit/2); + if (v->binary && v->reason.lit == other) { + Var * d = vars + (v->dominator/2); + //assert (d != v); + assert (depth); + if (d->removable) return true; + if (d->mark) return true; + } + Var * u = vars + (other/2); + assert (opts.minimize > Opts::RECUR || u->tlevel < v->tlevel); + if (u->tlevel > v->tlevel) return false; + if (u->mark) return true; + if (u->removable) return true; + if (u->poison) return false; + return minimize (u, depth); +} + +inline bool Solver::minl (int lit, Cls * cls, int depth) { + assert (vals[lit] > 0); + assert (cls->locked || cls->lits[0] == lit || cls->lits[1] == lit); + Var * v = vars + (lit/2); + int other; + for (const int * p = cls->lits; (other = *p); p++) { + if (other == lit) continue; + if (vals[other] >= 0) return false; + Var * u = vars + (other/2); + assert (opts.minimize > Opts::RECUR || u->tlevel < v->tlevel); + if (u->tlevel > v->tlevel) { + if (!opts.inveager) return false; + if (u != vars + uip/2 && (u->binary || u->reason.cls)) + return false; + } + if (u->mark) continue; + if (u->removable) continue; + if (u->poison) return false; + int l = u->dlevel; + if (!l) continue; + if (!frames[l].pulled) return false; + } + //int old = pulled; + for (const int * p = cls->lits; (other = *p); p++) { + if (other == lit) continue; + Var * u = vars + other/2; + if (u->mark) continue; + if (u->removable) continue; + if (u->poison) return false; + int l = u->dlevel; + if (!l) continue; + if (!minimize (u, depth)) { /*cleanpulled (old); */ return false; } + } + return true; +} + +inline bool Solver::strengthen (int lit, int depth) { + assert (vals[lit] > 0); + assert (opts.minimize >= Opts::STRONG); + const Stack & os2 = occs[lit].bins; + const int * eos2 = os2.end (); + for (const int * o = os2.begin (); o < eos2 && limit.strength-- >= 0; o++) + if (min2 (lit, *o, depth)) return true; + if (opts.minimize < Opts::STRONGER) return false; + const Stack & osl = occs[lit].large; + const Occ * eosl = osl.end (); + for (const Occ * o = osl.begin (); o < eosl && limit.strength-- >= 0; o++) + if (minl (lit, o->cls, depth)) { + if (opts.mtfall && depth == 1 && o->cls->lnd) + mtf (anchor (o->cls), o->cls); + return true; + } + return false; +} + +bool Solver::minimize (Var * v, int depth) { + if (!depth) limit.strength = opts.strength; + if (depth > stats.mins.depth) stats.mins.depth = depth; + assert (v->dlevel != level); + if (v->removable) return true; + if (depth && v->mark) return true; + if (v->poison) return false; + int l = v->dlevel; + if (!l) return true; + if (opts.minimize == Opts::NONE) return false; + if (depth && opts.minimize == Opts::LOCAL) return false; + if (!v->binary && !v->reason.cls) return false; + if (!frames[l].pulled) return false; + if (depth++ >= opts.maxdepth) return false; + assert (!v->onstack); + v->onstack = true; + bool res = false; + int lit = 2 * (v - vars); + Val val = vals[lit]; + if (val < 0) lit ^= 1; + assert (vals[lit] > 0); + if (v->binary) res = min2 (lit, v->reason.lit, depth); + else if ((res = minl (lit, v->reason.cls, depth))) { + if (opts.mtfall && depth == 1 && v->reason.cls->lnd) + mtf (anchor (v->reason.cls), v->reason.cls); + } + if (opts.minimize >= Opts::STRONG && !res) + if ((res = strengthen (lit, depth))) + stats.mins.strong++; + v->onstack = false; + if (res) v->removable = true; + else v->poison = true; + seen.push (mem, v); + return res; +} + +bool Solver::inverse (int lit) { + assert (vals[lit] > 0); + Var * v = vars + (lit/2); + if (v->dlevel != jlevel) return false; + const Stack & osl = occs[lit].large; + const Occ * eosl = osl.end (); + bool foundlit = false, founduip = false; + for (const Occ * o = osl.begin (); o < eosl; o++) { + Cls * c = o->cls; + int other = 0; + for (const int * p = c->lits; (other = *p); p++) { + if (other == lit) { foundlit = true; continue; } + if (other == uip) { founduip = true; continue; } + if (vals[other] >= 0) break; + Var * u = vars + (other/2); + if (u->dlevel >= jlevel) break; + if (!u->mark) break; + } + if (other) continue; + assert (founduip); + assert (foundlit); +#ifndef NLOGPRECO + dbgprint ("LOG inverse arc ", c); +#endif + if (opts.mtfall && c->lnd) mtf (anchor (c), c); + return true; + } + return false; +} + +void Solver::undo (int newlevel, bool save) { + LOG ("undo " << newlevel); + assert (newlevel <= level); + if (newlevel == level) return; + if (save) saved.shrink (); + int tlevel = frames[newlevel+1].tlevel; + while (tlevel < trail) { + int lit = trail.pop (); + assert (vals[lit] > 0); + vals[lit] = vals[lit^1] = 0; + LOG("unassign " << lit); + if (!repr[lit]) { + if (save) saved.push (mem, lit); + Rnk & r = rnks[lit/2]; + if (!schedule.decide.contains (&r)) schedule.decide.push (mem, &r); + } + int idx = lit/2; + Var & v = vars[idx]; + v.dlevel = -1; + if (v.binary) continue; + Cls * c = v.reason.cls; + if (!c) continue; + c->locked = false; + if (!c->lnd) continue; + assert (stats.clauses.lckd > 0); + stats.clauses.lckd--; + } + frames.shrink (newlevel + 1); + level = newlevel; + queue = queue2 = trail; + conflict = 0; + LOG ("backtrack new level " << newlevel); +} + +inline int & Solver::iirf (Var * v, int t) { + assert (1 <= t && t < opts.order && 2 <= opts.order); + return iirfs[(opts.order - 1) * (v - vars) + (t - 1)]; +} + +inline void Solver::rescore () { + stats.rescored++; + hinc >>= 14; + for (Rnk * s = rnks + 1; s <= rnks + maxvar; s++) s->heat >>= 14; + schedule.decide.construct (); +} + +inline void Solver::bump (Var * v, int add) { + assert (stats.conflicts > 0); + int inc = hinc; + if (opts.order >= 2) { + inc /= 2; + int w = inc, c = stats.conflicts - 1, s = 512, l = 9; + for (int i = 1; i <= opts.order - 1; i++) { + w >>= 1, l--; + for (int j = 1; j <= opts.order - 1; j++) { + int d = iirf (v, j); + if (d > c) continue; + if (d == c) inc += w, s += (1< 1; i--) + iirf (v, i) = iirf (v, i - 1); + iirf (v, 1) = stats.conflicts; + assert ((hinc >> (opts.order-1)) <= inc && inc <= hinc); + } + Rnk * r = rnk (v); + r->heat += inc + add; + LOG ("bump " << 2*(v - vars) << " by " << inc << " new score " << r->heat); + schedule.decide.up (r); + assert (hinc < (1<<28)); + if (r->heat >= (1<<24)) { + if (opts.bumpbulk) needrescore = true; + else rescore (); + } +} + +inline void Solver::pull (int lit) { + Var * v = vars + (lit/2); + assert (v->dlevel && !v->mark); + LOG ("pulling " << lit << " open " << open); + v->mark = 1; + seen.push (mem, v); + if (v->dlevel == level) open++; + else { + lits.push (mem, lit); + if (!frames[v->dlevel].pulled) { + frames[v->dlevel].pulled = true; + levels.push (mem, v->dlevel); + } + } +} + +void Solver::cleanlevels () { + while (levels) { + int l = levels.pop (); + assert (frames[l].pulled); + frames[l].pulled = false; + } +} + +void Solver::jump () { + jlevel = 0; + int * eolits = lits.end (); + for (const int * p = lits.begin(); p < eolits; p++) { + Var * v = vars + (*p/2); + if (v->dlevel < level && v->dlevel > jlevel) + jlevel = v->dlevel; + } + LOG ("new jump level " << jlevel); +} + +void Solver::cleanseen () { + Var ** eos = seen.end (); + for (Var ** p = seen.begin(); p < eos; p++) { + Var * v = *p; v->mark = 0; v->removable = v->poison = false; + } + seen.shrink (); +} + +void Solver::bump (Cls * c) { + if (c == &dummy) return; + assert (c); + if (c->garbage) return; + if (!c->lnd) return; + assert (!c->binary); + mtf (anchor (c), c); +#ifndef NLOGPRECO + int lit; + for (const int * p = c->lits; (lit = *p); p++) + if (val (lit) > 0) break; + if (lit) { + char buffer[100]; + sprintf (buffer, "LOG bump %d forcing clause ", lit); + dbgprint (buffer, c); + } else dbgprint ("LOG bump conflicting clause ", c); +#endif +} + +static int revcmptlevel (const void * p, const void * q) { + Var * u = *(Var**) p, * v = *(Var**) q; + return v->tlevel - u->tlevel; +} + +void Solver::bump () { + assert (conflict); + Var ** start, ** end, ** bos = seen.begin (), ** eos = seen.end (); + if (opts.bumpsort) qsort (bos, seen, sizeof *bos, revcmptlevel); +#ifndef NDEBUG + for (Var ** p = bos; p < eos; p++) + if (p+1 < eos) assert (p[0]->tlevel > p[1]->tlevel); +#endif + Var * uipvar = vars + (uip/2), * except = opts.bumpuip ? 0 : uipvar; + int dir; + if (opts.mtfrev) start = bos, end = eos, dir = 1; + else start = eos-1, end = bos-1, dir = -1; + if (opts.mtfrev) bump (conflict); + for (Var ** p = start; p != end; p += dir) { + Var * v = *p; + if (v == uipvar) continue; + if (v->dlevel < level) continue; + if (v->binary) continue; + Cls * r = v->reason.cls; + if (!r) continue; + bump (r); + } + if (!opts.mtfrev) bump (conflict); + // NOTE: this case split is actually redundant since + // we use the variable index order as tie breaker anyhow. + // TODO not really true, since rescore may happen? + if (opts.bumpbulk) needrescore = false; + if (opts.bumprev) start = eos-1, end = bos-1, dir = -1; + else start = bos, end = eos, dir = 1; + int turbo = opts.bumpturbo ? eos - bos - 1 : 0; + for (Var ** p = start; p != end; p += dir) { + Var * v = *p; + if (v == except) continue; + bump (v, turbo); + if (opts.bumpturbo) turbo--; + } + if (opts.bumpbulk && needrescore) rescore (); +} + +bool Solver::analyze () { +RESTART: + assert (conflict); + stats.conflicts++; + if (!level) return false; + assert (!lits); assert (!seen); assert (!levels); + int i = trail, lit; + bool unit = false; + resolved = open = 0; + Var * u = 0; + uip = 0; + do { + assert (seen >= resolved); + int otf = seen - resolved; + if (uip) { + LOG ("resolving " << uip); + resolved++; + } + if (!u || !u->binary) { + Cls * r = (u ? u->reason.cls : conflict); assert (r); + for (const int * p = r->lits; (lit = *p); p++) { + Var * v = vars + (lit/2); + if (!v->dlevel) continue; + if (!v->mark) { pull (lit); otf = INT_MAX; } + else if (v->tlevel <= i) otf--; + else otf = INT_MAX; + } + if (level > 0 && opts.otfs && otf <= 0 && r != &dummy) { +#ifndef NLOGPRECO + printf ("%sLOG on-the-fly strengthened %s clause ", + prfx, r->lnd ? "learned" : "original"); + r->print (); + printf ("%sLOG on-the-fly strengthening resolvent", prfx); + for (Var ** p = seen.begin (); p < seen.end (); p++) + if ((*p)->tlevel <= i) { + int lit = 2 * (*p - vars); + int val = vals[lit]; + assert (val); + if (val > 0) lit++; + printf (" %d", lit); + } + fputc ('\n', stdout); +#endif +#ifndef NDEBUG + assert (u); + if (opts.check) { + for (Var ** p = seen.begin (); p < seen.end (); p++) { + Var * v = *p; + assert (v->mark); + if (v->tlevel > i) continue; + int idx = v - vars, * q; + for (q = r->lits; *q; q++) if (*q/2 == idx) break; + assert (*q); + } + } +#endif + lit = 2 * (u - vars); + int val = vals[lit]; + assert (val); + if (val < 0) lit++; + assert (r->locked); + assert (u->reason.cls == r); + u->reason.cls = 0; + r->locked = false; + if (r->lnd) { + assert (stats.clauses.lckd > 0); + stats.clauses.lckd--; + } + bump (); + if (r->garbage) r->garbage = false; + remove (lit, r); + if (r->binary) { + conflict = lit2conflict (dummy, r->lits[0], r->lits[1]); + stats.otfs.dyn.trn++; + } else { + conflict = r; + slim (r); + stats.otfs.dyn.large++; + } + cleanlevels (); + cleanseen (); + lits.shrink (); + goto RESTART; + } + } else { + assert (u && u->binary); + otf--; + lit = u->reason.lit; + Var * v = vars + (lit/2); + if (v->dlevel) { + if (v->mark) { if (v->tlevel < i) otf--; } + else { pull (lit); otf = INT_MAX; } + } + + if (level > 0 && opts.otfs && otf <= 0) { + stats.otfs.dyn.bin++; + unit = true; + } + } + + for (;;) { + assert (i > 0); + uip = trail[--i]; + u = vars + (uip/2); + if (!u->mark) continue; + assert (u->dlevel == level); + assert (open > 0); + open--; + break; + } + } while (open); + assert (uip); + LOG ("uip " << uip); + uip ^= 1; + lits.push (mem, uip); + +#ifndef NLOGPRECO + printf ("%sLOG 1st uip clause", prfx); + for (const int * p = lits.begin (); p < lits.end (); p++) + printf (" %d", *p); + fputc ('\n', stdout); +#endif + bump (); +#ifndef NDEBUG + for (Var **p = seen.begin (); p < seen.end (); p++) { + Var * v = *p; assert (v->mark && !v->removable && !v->poison); + } +#endif + int * q = lits.begin (), * eolits = lits.end (); + for (const int * p = q; p < eolits; p++) { + lit = *p; Var * v = vars + (lit/2); + assert ((v->dlevel == level) == (lit == uip)); + if (v->dlevel < level && minimize (v, 0)) { + LOG ("removing 1st uip literal " << lit); + stats.mins.deleted++; + } else *q++ = lit; + } + lits.shrink (q); + jump (); + int cjlevel = 0; + eolits = lits.end (); + for (const int * p = lits.begin(); p < eolits; p++) { + lit = *p; + Var * v = vars + (lit/2); + if (v->dlevel != jlevel) continue; + LOG ("literal " << lit << " on jump level " << jlevel); + cjlevel++; + } + LOG (cjlevel << + " variables in minimized 1st UIP clause on jump level " << jlevel); + + if (opts.inverse && cjlevel == 1) { + q = lits.begin (), eolits = lits.end (); + { + int * p; + for (p = q; p < eolits; p++) { + if (inverse (1^*p)) { + stats.mins.inverse++; + stats.mins.deleted++; + LOG ("literal " << *p << " removed due to inverse arc"); + assert (cjlevel > 0); + cjlevel--; + p++; + break; + } else *q++ = *p; + } + while (p < eolits) + *q++ = *p++; + if (!cjlevel) { + LOG ("inverse arc decreases jump level"); + jump (); + } + } + lits.shrink (q); + } + + unsigned glue = gluelits (); + + cleanseen (); + cleanlevels (); + + stats.lits.added += lits; +#ifndef NLOGPRECO + printf ("%sLOG minimized clause", prfx); + for (const int * p = lits.begin (); p < lits.end (); p++) + printf (" %d", *p); + fputc ('\n', stdout); +#endif + +#ifndef NDEBUG + for (const int * p = lits.begin (); p < lits.end (); p++) + assert (*p == uip || vars[*p/2].dlevel < level); + if (unit) assert (!jlevel); +#endif +#ifndef NLOGPRECO + if (jlevel + 1 < level) LOG ("backjump to " << jlevel); + else LOG ("backtrack to " << jlevel); +#endif + undo (jlevel); + if (!jlevel) iterating = true; + + assert (!conflict); + bool lnd = true; + bwoccs (lnd); + int strlevel = jlevel; + bool skip = false; + if (strnd) { + LOG ("analyzing " << strnd << " strengthened clauses"); + for (Cls ** p = strnd.begin (); p < strnd.end (); p++) { + Cls * c = *p; + int countnonfalse = 0, maxlevel = 0; + for (int * q = c->lits; (lit = *q); q++) { + int val = vals[lit]; + if (val > 0) break; + if (!val && ++countnonfalse >= 2) break; + } + if (lit || countnonfalse >= 2) continue; + for (int * q = c->lits; (lit = *q); q++) { + int tmp = vars[lit/2].dlevel; + if (tmp > maxlevel) maxlevel = tmp; + } + int newstrlevel = 0; + for (int * q = c->lits; (lit = *q); q++) { + int tmp = vars[lit/2].dlevel; + if (tmp == maxlevel) continue; + assert (tmp < maxlevel); + if (tmp > newstrlevel) newstrlevel = tmp; + } + if (newstrlevel < strlevel) strlevel = newstrlevel; + } + if (strlevel < jlevel) { + LOG ("strengthened backtrack level " << strlevel); + undo (strlevel); + } + marklits (); + unsigned sig = litsig (); + for (Cls ** p = strnd.begin (); !skip && p < strnd.end (); p++) + if (fwsub (sig, *p)) skip = true; + unmarklits (); + if (skip) + LOG ("learned clause subsumed by strengthened clause"); + for (Cls ** p = strnd.begin (); p < strnd.end (); p++) { + Cls * c = *p; + int unit = 0; + for (int * q = c->lits; (lit = *q); q++) { + Val val = vals[lit]; + if (val < 0) continue; + if (val > 0) break; + if (unit) break; + unit = lit; + } + if (lit) continue; + assert (unit); + assert (!c->garbage); + if (c->binary) { + int other = c->lits[0] + c->lits[1]; + other -= unit; + imply (unit, other); + } else force (unit, c); + if (skip) continue; + skip = true; + LOG ("learned clause skipped because of forcing strengthened clause"); + } + for (Cls ** p = strnd.begin (); p < strnd.end (); p++) + assert ((*p)->str), (*p)->str = false; + strnd.shrink (); + } + if (!skip || !lnd) { + for (Frame * f = frames.begin (); f < frames.end (); f++) + assert (!f->contained); + Cls * cls = clause (lnd, lnd ? glue : 0); //TODO: move before if? + if (!vals[uip] && strlevel == jlevel) { + if (cls) { + if (cls->binary) { + int other = cls->lits[0] + cls->lits[1]; + other -= uip; + imply (uip, other); + } else { + force (uip, cls); + slim (cls); + } + } + } + if (lnd) { + while (fresh.count > limit.reduce.fresh && fresh.tail) { + Cls * f = fresh.tail; + dequeue (fresh, f); + assert (f->fresh); + assert (!f->binary); + assert (f->lnd); + f->fresh = false; + push (anchor (f), f); + } + int count = opts.dynred; + Cls * ctc; + for (int glue = opts.glue; + glue >= opts.sticky && count >= 0 && recycling (); + glue--) { + ctc = learned[glue].tail; + while (ctc && count-- >= 0 && recycling ()) { + Cls * next = ctc->next; + assert (!ctc->binary); + if (ctc != cls && !ctc->locked) recycle (ctc); + ctc = next; + } + } + } + } else lits.shrink (); + + long long tmp = hinc; + tmp *= 100 + opts.heatinc; tmp /= 100; + assert (tmp <= INT_MAX); + hinc = tmp; + + return true; +} + +int Solver::luby (int i) { + int k; + for (k = 1; k < 32; k++) + if (i == (1 << k) - 1) + return 1 << (k-1); + + for (k = 1;; k++) + if ((1 << (k-1)) <= i && i < (1 << k) - 1) + return luby (i - (1u << (k-1)) + 1); +} + +inline double Stats::height () { + return decisions ? sumheight / (double) decisions : 0.0; +} + +void Solver::increp () { + if ((stats.reports++ % 19)) return; + fprintf (out, +"%s .\n" +"%s ." +" clauses fixed eliminated learned agility" +"\n" +"%s ." +" seconds variables equivalent conflicts height MB" +"\n" +"%s .\n", prfx, prfx, prfx, prfx); +} + +int Solver::remvars () const { + int res = maxvar; + res -= stats.vars.fixed; + res -= stats.vars.equiv; + res -= stats.vars.elim; + res -= stats.vars.pure; + res -= stats.vars.zombies; + assert (res >= 0); + return res; +} + +void Solver::report (int v, char type) { + if (opts.quiet || v > opts.verbose) return; + char countch[2]; + countch[0] = countch[1] = ' '; + if (terminal && type == lastype) { + typecount++; + if (type != 'e' && type != 'p' && type != 'k') { + countch[0] = '0' + (typecount % 10); + if (typecount >= 10) countch[1] = '0' + (typecount % 100)/10; + } + } else { + typecount = 1; + if (terminal && lastype) fputc ('\n', out); + increp (); + } + assert (maxvar >= stats.vars.fixed + stats.vars.equiv + stats.vars.elim); + fprintf (out, "%s%c%c%c%7.1f %7d %7d %6d %6d %6d %7d %6d %6.1f %2.0f %4.0f", + prfx, + countch[1], countch[0], type, stats.seconds (), + stats.clauses.irr, + remvars (), + stats.vars.fixed, stats.vars.equiv, + stats.vars.elim, + type=='e'?schedule.elim: + (type=='p'?schedule.probe: + (type=='k'?schedule.block:stats.conflicts)), + (type=='F'?limit.reduce.fresh: + (type=='l' || type=='+' || type == '-') ? + limit.reduce.learned : stats.clauses.lnd), + stats.height (), + agility / 100000.0, + mem / (double) (1<<20)); + if (!terminal || type=='0' || type=='1' || type=='?') fputc ('\n', out); + else fputc ('\r', out); + fflush (out); + lastype = type; +} + +void Solver::restart () { + int skip = agility >= opts.skip * 100000; + if (skip) stats.restart.skipped++; + else stats.restart.count++; + limit.restart.conflicts = stats.conflicts; + int delta; + if (opts.luby) delta = opts.restartint * luby (++limit.restart.lcnt); + else { + if (limit.restart.inner >= limit.restart.outer) { + limit.restart.inner = opts.restartint; + limit.restart.outer *= 100 + opts.restartouter; + limit.restart.outer /= 100; + } else { + limit.restart.inner *= 100 + opts.restartinner; + limit.restart.inner /= 100; + } + delta = limit.restart.inner; + } + limit.restart.conflicts += delta; + if (!skip) undo (0); + if (stats.restart.maxdelta < delta) { + stats.restart.maxdelta = delta; + report (1, skip ? 'N' : 'R'); + } else + report (2, skip ? 'n' :'r'); +} + +void Solver::rebias () { + limit.rebias.conflicts = stats.conflicts; + int delta = opts.rebiasint * luby (++limit.rebias.lcnt); + limit.rebias.conflicts += delta; + if (!opts.rebias) return; + stats.rebias.count++; + for (Var * v = vars + 1; v <= vars + maxvar; v++) v->phase = 0; + jwh (); + if (stats.rebias.maxdelta >= delta) report (2, 'b'); + else stats.rebias.maxdelta = delta, report (1, 'B'); +} + +inline int Solver::redundant (Cls * c) { + assert (!level); + assert (!c->locked); + assert (!c->garbage); +#ifndef NDEBUG + for (const int * p = c->lits; *p; p++) { + Var * v = vars + (*p/2); + assert (!v->mark); + assert (v->type != ELIM); + } +#endif + int res = 0, * p, lit; +#ifdef PRECOCHECK + bool shrink = false; + for (p = c->lits; !res && (lit = *p); p++) { + int other = find (lit); + Var * v = vars + (other/2); + assert ((v->type != ELIM)); + Val val = vals[other]; + if (val > 0 && !v->dlevel) res = 1; + else if (val < 0 && !v->dlevel) shrink = true; + else { + val = lit2val (other); + if (v->mark == val) { shrink = true; continue; } + else if (v->mark == -val) res = 1; + else v->mark = val; + } + } + while (p > c->lits) vars[find (*--p)/2].mark = 0; +#ifndef NDEBUG + for (p = c->lits; *p; p++) assert (!vars[find (*p)/2].mark); +#endif + if (shrink || res) { + for (p = c->lits; *p; p++) check.push (mem, *p); + check.push (mem, 0); + } + if (res) return res; +#endif + p = c->lits; int * q = p; + while (!res && (lit = *p)) { + p++; + int other = find (lit); + if (other != lit) simplified = true; + Var * v = vars + (other/2); + assert (v->type != ELIM); + Val val = vals[other]; + if (val && !v->dlevel) { + if (val > 0) res = 1; + } else { + val = lit2val (other); + if (v->mark == val) continue; + if (v->mark == -val) res = 1; + else { assert (!v->mark); v->mark = val; *q++ = other; } + } + } + *q = 0; + + if (!res) assert (!*q && !*p); + + int newsize = q - c->lits; + + if (!res && + newsize > 1 && + newsize <= opts.redsub && + (!c->lnd || c->binary)) { + limit.budget.red += 10; + setsig (c); + for (p = c->lits; !res && (lit = *p) && limit.budget.red >= 0; p++) { + INC (sigs.fw.l2.srch); + if (!(fwsigs[lit] & c->sig)) { INC (sigs.fw.l2.hits); continue; } + if (fwds[lits] > opts.fwmaxlen) continue; + for (int i = 0; !res && i < fwds[lit] && limit.budget.red >= 0; i++) { + limit.budget.red--; + Cls * d = fwds[lit][i]; + assert (!d->trash); + if (d->garbage) continue; + if (d->size > (unsigned) newsize) continue; + if (d->size > (unsigned) opts.redsub) continue; + if (!c->lnd && d->lnd && !d->binary) continue; + INC (sigs.fw.l1.srch); + if (!sigsubs (d->sig, c->sig)) { INC (sigs.fw.l1.hits); continue; }; + int other; + for (const int * r = d->lits; (other = *r); r++) { + Val u = lit2val (other), v = vars[other/2].mark; + if (u != v) break; + } + if ((res = !other)) { + stats.subs.red++; + limit.budget.red += 20; + if (!c->lnd && d->lnd) { + assert (d->binary); + d->lnd = false; + stats.clauses.irr++; + } + } + } + } + } + + while (q-- > c->lits) { + assert (vars[*q/2].mark); vars[*q/2].mark = 0; + } + + if (res) return res; + + if (newsize > 1 && newsize <= opts.redsub && (!c->lnd || c->binary)) + fwds[c->minlit ()].push (mem, c); + + res = newsize <= 1; + if (!newsize) conflict = ∅ + else if (newsize == 1) { + LOG ("learned clause " << c->lits[0]); + unit (c->lits[0]); + } else if (newsize == 2 && !c->binary && 2 < c->size) { + if (c->lnd) assert (stats.clauses.lnd), stats.clauses.lnd--; + else assert (stats.clauses.orig), stats.clauses.orig--; + stats.clauses.bin++; + c->binary = true; + push (binary, c); + res = -1; + } else assert (!res); + + return res; +} + +void Solver::checkvarstats () { +#ifndef NDEBUG + assert (!level); + int fixed = 0, equivalent = 0, eliminated = 0, pure = 0, zombies = 0; + for (Var * v = vars + 1; v <= vars + maxvar; v++) { + int lit = 2 * (v - vars); + if (v->type == ELIM) eliminated++; + else if (v->type == PURE) pure++; + else if (v->type == ZOMBIE) zombies++; + else if (vals[lit]) { assert (v->type == FIXED); fixed++; } + else if (repr[lit]) { assert (v->type == EQUIV); equivalent++; } + else assert (v->type == FREE); + } + assert (fixed == stats.vars.fixed); + assert (eliminated == stats.vars.elim); + assert (pure == stats.vars.pure); + assert (zombies == stats.vars.zombies); + assert (equivalent == stats.vars.equiv); +#endif +} + +void Solver::decompose () { + assert (!level); + if (!opts.decompose) return; + report (2, 'd'); + int n = 0; + size_t bytes = 2 * (maxvar + 1) * sizeof (SCC); + SCC * sccs = (SCC*) mem.callocate (bytes); + Stack work; + saved.shrink (); + int dfsi = 0; + LOG ("starting scc decomposition"); + for (int root = 2; !conflict && root <= 2*maxvar + 1; root++) { + if (sccs[root].idx) { assert (sccs[root].done); continue; } + assert (!work); + work.push (mem, root); + LOG ("new scc root " << root); + while (!conflict && work) { + int lit = work.top (); + if (sccs[lit^1].idx && !sccs[lit^1].done) { + Val val = vals[lit]; + if (val < 0) { + LOG ("conflict while learning unit in scc"); + conflict = ∅ + } else if (!val) { + LOG ("learned clause " << lit); + unit (lit); + stats.sccs.fixed++; + flush (); + } + } + if (conflict) break; + Stack & os = occs[1^lit].bins; + unsigned i = os; + if (!sccs[lit].idx) { + assert (!sccs[lit].done); + sccs[lit].idx = sccs[lit].min = ++dfsi; + saved.push (mem, lit); + while (i) { + int other = os[--i]; + if (sccs[other].idx) continue; + work.push (mem, other); + } + } else { + work.pop (); + if (!sccs[lit].done) { + while (i) { + int other = os[--i]; + if (sccs[other].done) continue; + sccs[lit].min = min (sccs[lit].min, sccs[other].min); + } + SCC * scc = sccs + lit; + unsigned min = scc->min; + if (min != scc->idx) { assert (min < scc->idx); continue; } + n++; LOG ("new scc " << n); + int m = 0, prev = 0, other = 0; + while (!conflict && other != lit) { + other = saved.pop (); + sccs[other].done = true; + LOG ("literal " << other << " added to scc " << n); + if (prev) { + int a = find (prev), b = find (other); + if (a == b) continue; + if (a == (1^b)) { + LOG ("conflict while merging scc"); + conflict = ∅ + } else if (val (a) || val (b)) { + assert (val (a) == val (b)); + } else { + merge (prev, other, stats.sccs.merged); + m++; + } + } else prev = other; + } + if (m) stats.sccs.nontriv++; + } + } + } + } + + LOG ("found " << n << " sccs"); + assert (conflict || dfsi <= 2 * maxvar); + work.release (mem); + mem.deallocate (sccs, bytes); + flush (); +#ifndef NDEBUG + checkvarstats (); +#endif + report (2, 'd'); +} + +void Solver::disconnect () { + cleangate (), cleantrash (); + for (int lit = 2; lit <= 2*maxvar + 1; lit++) + occs[lit].bins.release (mem), occs[lit].large.release (mem); + assert (!orgs && !fwds && !fwsigs); + clrbwsigs (); +} + +void Solver::connect (Anchor & anchor, bool orgonly) { + for (Cls * p = anchor.tail; p; p = p->next) { + assert (&anchor == &this->anchor (p)); + if (!orgonly || !p->lnd) connect (p); + } +} + +void Solver::gc (Anchor & anchor, const char * type) { + limit.budget.red = 10000; + Cls * p = anchor.tail; + int collected = 0; + anchor.head = anchor.tail = 0; + anchor.count = 0; + while (p) { + Cls * next = p->next; +#ifndef NDEBUG + p->next = p->prev = 0; +#endif + int red = 1; + if (!p->garbage) { + red = redundant (p); + if (red > 0) p->garbage = true; + } + if (p->garbage) { collect (p); collected++; } + else if (!red) push (anchor, p); + else assert (connected (binary, p)); + p = next; + } +#ifndef NLOGPRECO + if (collected) + LOG ("collected " << collected << ' ' << type << " clauses"); +#else + (void) type; +#endif +} + +inline void Solver::checkclean () { +#ifndef NDEBUG + if (opts.check) { + for (int i = 0; i <= 3 + opts.glue; i++) { + Cls * p; + if (i == 0) p = original.head; + if (i == 1) p = binary.head; + if (i == 2) p = fresh.head; + if (i >= 3) p = learned[i-3].head; + while (p) { + for (int * q = p->lits; *q; q++) { + int lit = *q; + assert (!repr[lit]); + assert (!vals[lit]); + Var * v = vars + (lit/2); + assert (v->type == FREE); + } + p = p->prev; + } + } + } +#endif +} + +void Solver::gc () { +#ifndef NLOGPRECO + size_t old = stats.collected; +#endif + report (2, 'g'); + undo (0); + disconnect (); + initfwds (); + initfwsigs (); + gc (binary, "binary"); + gc (original, "original"); + gc (fresh, "fresh"); + for (int glue = 0; glue <= opts.glue; glue++) { + char buffer[80]; + sprintf (buffer, "learned[%u]", glue); + gc (learned[glue], buffer); + } + delfwds (); + delfwsigs (); + connect (binary); + connect (original); + for (int glue = 0; glue <= opts.glue; glue++) + connect (learned[glue]); + connect (fresh); + checkclean (); +#ifndef NLOGPRECO + size_t bytes = stats.collected - old; + LOG ("collected " << bytes << " bytes"); + dbgprint (); +#endif + flush (); + stats.gcs++; + report (2, 'c'); +} + +inline int Solver::recyclelimit () const { + return limit.reduce.learned + stats.clauses.lckd; +} + +inline bool Solver::recycling () const { + return stats.clauses.lnd >= recyclelimit (); +} + +void Solver::reduce () { + assert (!conflict); + assert (trail == queue); + stats.reductions++; + Cls * f; + while ((f = fresh.tail)) { + dequeue (fresh, f); + assert (f->fresh); + assert (!f->binary); + assert (f->lnd); + f->fresh = false; + push (anchor (f), f); + } + int goal = (stats.clauses.lnd - stats.clauses.lckd)/2, count = 0; + for (int glue = opts.glue; glue >= opts.sticky && count < goal; glue--) { + Cls * next; + for (Cls * p = learned[glue].tail; p && count < goal; p = next) { + next = p->next; + if (p->locked) continue; + p->garbage = true; + count++; + } + } + gc (); + jwh (); + if (count >= goal/2) report (1, '/'); + else report (1, '='), enlarge (); +} + +inline void Solver::checkeliminated () { +#ifndef NDEBUG + if (opts.check) { + for (int i = 0; i <= 3 + (int)opts.glue; i++) { + Cls * p; + if (i == 0) p = original.head; + if (i == 1) p = binary.head; + if (i == 1) p = fresh.head; + if (i >= 3) p = learned[i-3].head; + while (p) { + for (int * q = p->lits; *q; q++) { + int lit = *q; + Var * v = vars + (lit/2); + assert (v->type != ELIM); + } + p = p->prev; + } + } + } +#endif +} + +void Solver::probe () { + stats.sw2simp (); + assert (!conflict); + assert (queue2 == trail); + undo (0); + stats.probe.phases++; + measure = false; + for (const Rnk * r = rnks + 1; r <= rnks + maxvar; r++) { + Rnk * p = prb (r); + int lit = 2 * (r - rnks); + int old_heat = p->heat; + int new_heat = jwhs[lit] + jwhs[lit^1]; + if (new_heat < 0) new_heat = INT_MAX; + p->heat = new_heat; + if (schedule.probe.contains (p)) { + if (new_heat > old_heat) schedule.probe.up (p); + else if (new_heat < old_heat) schedule.probe.down (p); + } + } + int repcounter = 111; + long long bound; + if (opts.rtc == 2 || opts.probertc == 2 || + ((opts.rtc == 1 || opts.probertc == 1) && !stats.probe.rounds)) + bound = LLONG_MAX; + else { + bound = stats.props.simp + opts.probeint; + for (int i = stats.probe.phases; i <= opts.probeboost; i++) + bound += opts.probeint; + } + int last = -1, filled = 0; + if (!schedule.probe) { +FILL: + filled++; + for (int idx = 1; idx <= maxvar; idx++) { + Var & v = vars[idx]; + if (v.type != FREE && v.type != EQUIV) continue; + int lit = 2 * idx; + assert (!vals[lit]); + if (repr[lit]) continue; +#if 0 + // TODO replace && by '==' for incremental scc computation + if (!occs[lit].bins == !occs[lit^1].bins) continue; +#else + if (!occs[lit].bins && !occs[lit^1].bins) continue; +#endif + Rnk * p = prbs + idx; + schedule.probe.push (mem, p); + } + } + report (2, 'p'); + while (stats.props.simp < bound && !conflict) { + if (!--repcounter) { + if (terminal) report (2, 'p'); + repcounter = 111; + } + assert (!level); + if (!schedule.probe) { + stats.probe.rounds++; + if (last == filled) goto FILL; + break; + } + Rnk * p = schedule.probe.pop (); + int idx = p - prbs; + Var & v = vars[idx]; + if (v.type != FREE && v.type != EQUIV) continue; + int lit = 2*idx; + assert (!vals[lit]); + if (repr[lit]) continue; + assert (!level); + long long old = stats.props.simp; + LOG ("probing " << lit); + stats.probe.variables++; + assume (lit); + bool ok = bcp (); + undo (0, ok); + if (!ok) goto FAILEDLIT; + lit ^= 1; + LOG ("probing " << lit); + assume (lit); + stats.probe.variables++; + if (!bcp ()) { undo (0); goto FAILEDLIT; } + { + int * q = saved.begin (), * eos = saved.end (); + for (const int * p = q; p < eos; p++) { + int other = *p; + if (other == (lit^1)) continue; + if (vals[other] < 0) merge (lit, other^1, stats.probe.merged); + if (vals[other] <= 0) continue; + *q++ = other; + } + undo (0); + if (q == saved.begin ()) continue; + saved.shrink (q); + for (const int * p = saved.begin (); p < q; p++) { + stats.probe.lifted++; + last = filled; + int other = *p; + LOG ("lifting " << other); + LOG ("learned clause " << other); + unit (other); + } + } + goto BCPANDINCBOUND; +FAILEDLIT: + stats.probe.failed++; + last = filled; + LOG ("learned clause " << (1^lit)); + unit (1^lit); +BCPANDINCBOUND: + flush (); + if (bound != LLONG_MAX) + bound += opts.probereward + (stats.props.simp - old); + } + measure = true; + limit.props.probe = opts.probeprd; + limit.props.probe *= opts.probeint; + limit.props.probe += stats.props.srch; + limit.fixed.probe = stats.vars.fixed; + checkvarstats (); + report (2, 'p'); + stats.sw2srch (); +} + +bool Solver::andgate (int lit) { + // TODO L2 sigs? + assert (vars[lit/2].type != ELIM); + assert (!gate && !gatestats); + if (!opts.subst) return false; + if (!opts.ands) return false; + if (!orgs[lit] || !orgs[1^lit]) return false; + Cls * b = 0; + int other, notlit = (1^lit), bound = 1000; + for (int i = 0; !b && i < orgs[lit] && bound-- >= 0; i++) { + Cls * c = orgs[lit][i]; + if (!sigsubs (c->sig, bwsigs[lit^1])) continue; + assert (!gate); + gcls (c); + gatelen = 0; + bool hit = false; + for (const int * p = c->lits; (other = *p); p++) { + if (lit == other) { hit = true; continue; } + assert (!vars[other/2].mark); + vars[other/2].mark = -lit2val (other); + gatelen++; + } + assert (hit); + assert (gatelen); + int count = gatelen; + for (int j = 0; j < orgs[notlit] && bound-- >= 0; j++) { + if (orgs[notlit] - j < count) break; + Cls * d = orgs[notlit][j]; + if (d->lits[2]) continue; + int pos = (d->lits[1] == notlit); + assert (d->lits[pos] == notlit); + assert (d->binary); + other = d->lits[!pos]; + if (vars[other/2].mark != lit2val (other)) continue; + vars[other/2].mark = 0; + gcls (d); + if (!--count) break; + } + for (const int * p = c->lits; (other = *p); p++) + vars[other/2].mark = 0; + if (count) cleangate (); else b = c; + } + if (!b) { assert (!gate); return false; } + assert (gate == gatelen + 1); + gatestats = (gatelen >= 2) ? &stats.subst.ands : &stats.subst.nots; + gatepivot = lit; + posgate = 1; +#ifndef NLOGPRECO + printf ("%sLOG %s gate %d = ", prfx, (gatelen >= 2) ? "and" : "not", lit); + for (const int * p = b->lits; (other = *p); p++) { + if (other == lit) continue; + printf ("%d", (1^other)); + if (p[1] && (p[1] != lit || p[2])) fputs (" & ", stdout); + } + fputc ('\n', stdout); + dbgprintgate (); +#endif + return true; +} + +bool Solver::xorgate (int lit) { + // TODO L2 sigs + assert (vars[lit/2].type != ELIM); + assert (!gate && !gatestats); + if (!opts.subst) return false; + if (!opts.xors) return false; + if (orgs[lit] < 2 || orgs[1^lit] < 2) return false; + if (orgs[lit] > orgs[1^lit]) lit ^= 1; + Cls * b = 0; + int len = 0, other, bound = 600; + for (int i = 0; i < orgs[lit] && !b && bound-- >= 0; i++) { + Cls * c = orgs[lit][i]; + const int maxlen = 20; + assert (maxlen < 31); + if (c->size > (unsigned) maxlen) continue; + if (!c->lits[2]) continue; + assert (!c->binary); + if (!sigsubs (c->sig, bwsigs[lit^1])) continue; + int * p; + for (p = c->lits; *p; p++) + ; + len = p - c->lits; + assert (len >= 3); + int required = (1 << (len-1)); + for (p = c->lits; (other = *p); p++) { + if (other == lit) continue; + if (orgs[other] < required) break; + if (orgs[other^1] < required) break; + if (!sigsubs (c->sig, bwsigs[other])) break; + if (!sigsubs (c->sig, bwsigs[1^other])) break; + } + if (other) continue; + assert (!gate); + assert (0 < len && len <= maxlen); + unsigned signs; + for (signs = 0; signs < (1u<= 0; signs++) { + if (parity (signs)) continue; + int start = 0, startlen = INT_MAX, s = 0; + for (p = c->lits; (other = *p); p++, s++) { + if ((signs & (1u<= startlen) continue; + startlen = tmp; + start = other; + } + assert (s == len && start && startlen < INT_MAX); + int j; + Cls * found = 0; + for (j = 0; !found && j < orgs[start] && bound-- >= 0; j++) { + Cls * d = orgs[start][j]; + if (d->sig != c->sig) continue; + for (p = d->lits; *p; p++) + ; + if (p - d->lits != len) continue; + bool hit = false; + s = 0; + for (p = c->lits; (other = *p); p++, s++) { + if ((signs & (1u<contains (other)) break; + } + assert (other || hit); + if (!other) found = d; + } + assert (bound < 0 || signs || found); + if (!found) break; + assert (required); + required--; + gcls (found); + } + if (signs == (1u<= 3); + assert (gate == (1<<(len-1))); + gatepivot = lit; + gatestats = &stats.subst.xors; + gatelen = len - 1; + int pos = -1, neg = gate; + for (;;) { + while (pos+1 < neg && gate[pos+1]->contains (lit)) pos++; + assert (pos >= gate || gate[pos+1]->contains(1^lit)); + if (pos+1 == neg) break; + while (pos < neg-1 && gate[neg-1]->contains ((1^lit))) neg--; + assert (neg < 0 || gate[neg-1]->contains(lit)); + if (pos+1 == neg) break; + assert (pos < neg); + swap (gate[++pos], gate[--neg]); + } + posgate = pos + 1; +#ifndef NLOGPRECO + printf ("%sLOG %d-ary xor gate %d = ", prfx, len-1, (lit^1)); + for (const int * p = b->lits; (other = *p); p++) { + if (other == lit) continue; + printf ("%d", other); + if (p[1] && (p[1] != lit || p[2])) fputs (" ^ ", stdout); + } + fputc ('\n', stdout); + dbgprintgate (); +#endif + return true; +} + +Cls * Solver::find (int a, int b, int c) { + unsigned sig = listig (a) | listig (b) | listig (c); + unsigned all = bwsigs[a] & bwsigs[b] & bwsigs[c]; + if (!sigsubs (sig, all)) return 0; + int start = a; + if (orgs[start] > orgs[b]) start = b; + if (orgs[start] > orgs[c]) start = c; + for (int i = 0; i < orgs[start]; i++) { + Cls * res = orgs[start][i]; + if (res->sig != sig) continue; + assert (res->lits[0] && res->lits[1]); + if (!res->lits[2]) continue; + assert (!res->binary); + if (res->lits[3]) continue; + int l0 = res->lits[0], l1 = res->lits[1], l2 = res->lits[2]; + if ((a == l0 && b == l1 && c == l2) || + (a == l0 && b == l2 && c == l1) || + (a == l1 && b == l0 && c == l2) || + (a == l1 && b == l2 && c == l0) || + (a == l2 && b == l0 && c == l1) || + (a == l2 && b == l1 && c == l2)) return res; + } + return 0; +} + +int Solver::itegate (int lit, int cond, int t) { + Cls * c = find (lit^1, cond, t^1); + if (!c) return 0; + int start = lit, nc = (cond^1), bound = 200; + if (orgs[nc] < orgs[start]) start = nc; + unsigned sig = listig (lit) | listig (nc); + for (int i = 0; i < orgs[start] && --bound >= 0; i++) { + Cls * d = orgs[start][i]; + if (!sigsubs (sig, d->sig)) continue; + assert (d->lits[0] && d->lits[1]); + if (!d->lits[2]) continue; + assert (!d->binary); + if (d->lits[3]) continue; + int l0 = d->lits[0], l1 = d->lits[1], l2 = d->lits[2], res; + if (l0 == lit && l1 == nc) res = l2; + else if (l1 == lit && l0 == nc) res = l2; + else if (l0 == lit && l2 == nc) res = l1; + else if (l2 == lit && l0 == nc) res = l1; + else if (l1 == lit && l2 == nc) res = l0; + else if (l2 == lit && l1 == nc) res = l0; + else continue; + Cls * e = find (lit^1, nc, res^1); + if (!e) continue; + gcls (d); + gcls (c); + gcls (e); + return res; + } + return 0; +} + +bool Solver::itegate (int lit) { + // TODO L2 sigs + assert (vars[lit/2].type != ELIM); + assert (!gate && !gatestats); + if (!opts.subst) return false; + if (!opts.ites) return false; + if (orgs[lit] < 2 || orgs[1^lit] < 2) return false; + if (orgs[lit] > orgs[1^lit]) lit ^= 1; + Cls * b = 0; + int cond = 0, t = 0, e = 0; + for (int i = 0; i < orgs[lit] && !b; i++) { + Cls * c = orgs[lit][i]; + assert (c->lits[0] && c->lits[1]); + if (!c->lits[2]) continue; + assert (!c->binary); + if (c->lits[3]) continue; + assert (!gate); + int o0, o1, l0 = c->lits[0], l1 = c->lits[1], l2 = c->lits[2]; + if (lit == l0) o0 = l1, o1 = l2; + else if (lit == l1) o0 = l0, o1 = l2; + else assert (lit == l2), o0 = l0, o1 = l1; + assert (!gate); + gcls (c); + if ((e = itegate (lit, cond = o0, t = o1)) || + (e = itegate (lit, cond = o1, t = o0))) b = c; + else cleangate (); + } + if (!b) { assert (!gate); return false; } + assert (cond && t && e); + assert (gate == 4); + gatestats = &stats.subst.ites; + gatepivot = lit; + posgate = 2; +#ifndef NLOGPRECO + LOG ("ite gate " << lit << " = " << + (1^cond) << " ? " << (1^t) << " : " << (1^e)); + dbgprintgate (); +#endif + return true; +} + +bool Solver::resolve (Cls * c, int pivot, Cls * d, bool tryonly) { + if (tryonly) resotfs = reslimhit = false; + assert (tryonly || (c->dirty && d->dirty)); + assert (tryonly != (vars[pivot/2].type == ELIM)); + assert (!vals[pivot] && !repr[pivot]); + if (!tryonly && gate && c->gate == d->gate) return false; + if (elimode) stats.elim.resolutions++; + else { assert (blkmode); stats.blkd.resolutions++; } + int other, notpivot = (1^pivot), clits = 0, dlits = 0; + bool found = false, res = true; + const int * p; + assert (!lits); + for (p = c->lits; (other = *p); p++) { + if (other == pivot) { found = true; continue; } + assert (other != notpivot); + assert (find (other) == other); + assert (other != notpivot); + if (other == pivot) continue; + Val v = vals [other]; + if (v < 0) continue; + if (v > 0) { res = false; goto DONE; } + assert (!vars[other/2].mark); + Val u = lit2val (other); + vars[other/2].mark = u; + lits.push (mem, other); + clits++; + } + assert (found); + found = false; + for (p = d->lits; (other = *p); p++) { + if (other == notpivot) { found = true; continue; } + assert (other != pivot); + assert (find (other) == other); + assert (other != pivot); + if (other == notpivot) continue; + Val v = vals[other]; + if (v < 0) continue; + if (v > 0) { res = false; goto DONE; } + dlits++; + v = vars[other/2].mark; + Val u = lit2val (other); + if (!v) { + vars[other/2].mark = u; + lits.push (mem, other); + } else if (v != u) { res = false; goto DONE; } + } + assert (found); + if (opts.otfs && tryonly) { +#ifndef NLOGPRECO + bool logresolvent = false; +#endif + if (lits == clits && (!blkmode || opts.blockotfs)) { +#ifndef NLOGPRECO + dbgprint ("LOG static on-the-fly strengthened clause ", c); + dbgprint ("LOG static on-the-fly antecedent ", d); + logresolvent = true; +#endif + if (c->gate) cleangate (); + remove (pivot, c); + resotfs = true; + if (clits == 1) stats.otfs.stat.bin++; + else if (clits == 2) stats.otfs.stat.trn++; + else stats.otfs.stat.large++; + } + if (lits == dlits && (!blkmode || opts.blockotfs)) { +#ifndef NLOGPRECO + dbgprint ("LOG static on-the-fly strengthened clause ", d); + dbgprint ("LOG static on-the-fly antecedent ", c); + logresolvent = true; +#endif + if (d->gate) cleangate (); + remove (notpivot, d); + resotfs = true; + if (dlits == 1) stats.otfs.stat.bin++; + else if (dlits == 2) stats.otfs.stat.trn++; + else stats.otfs.stat.large++; + } +#ifndef NLOGPRECO + if (logresolvent) { + printf ("%sLOG static on-the-fly subsuming resolvent", prfx); + for (p = lits.begin (); p < lits.end (); p++) printf (" %d", *p); + fputc ('\n', stdout); + } +#endif + } +DONE: + for (p = lits.begin (); p < lits.end (); p++) { + Var * u = vars + (*p/2); + assert (u->mark); + u->mark = 0; + } + if (res) { + if (!lits) { + LOG ("conflict in resolving clauses"); + conflict = ∅ + res = false; + } else if (lits == 1) { + LOG ("learned clause " << lits[0]); + unit (lits[0]); + res = false; + } else if (!tryonly) { + if (!fworgs ()) { + bworgs (); + clause (false, 0); + } + } else { + if (lits > opts.reslim) reslimhit = true; + } + } + lits.shrink (); + return res; +} + +inline void Solver::checkgate () { +#ifndef NDEBUG + for (int i = 0; i < posgate; i++) assert (gate[i]->contains (gatepivot)); + for (int i = posgate; i < gate; i++) assert (gate[i]->contains (1^gatepivot)); + for (int i = 0; i < posgate; i++) + for (int j = posgate; j < gate; j++) + assert (!resolve (gate[i], gatepivot, gate[j], true)); +#endif +} + +inline void Solver::block (Cls * c, int lit) { + assert (opts.block); +#ifndef NLOGPRECO + dbgprint ("LOG blocked clause ", c); + LOG ("blocked on literal " << lit); +#endif + assert (!blklit); + blklit = lit; + if (c->gate) cleangate (); + elits.push (mem, 0); + bool found = false; + int other; + for (const int * p = c->lits; (other = *p); p++) { + if (other == lit) { found = true; continue; } + elits.push (mem, other); + } + assert (found); + elits.push (mem, lit); + elits.push (mem, INT_MAX); + // NOTE: we can not simply turn binary blocked clauses + // into learned clauses, which can be removed without + // any further check in the future, because adding + // resolvents to the CNF (either through learning, + // elimination, dominator clauses etc) may unblock + // clauses. These binary clauses would need to + // be treated differently in all operations that + // remove clauses from the CNF. + recycle (c); + blklit = 0; +} + +bool Solver::trelim (int idx) { + assert (!elimvar); + assert (!conflict); + assert (queue == trail); + assert (vars[idx].type == FREE); +RESTART: + int lit = 2*idx, pos = orgs[lit], neg = orgs[lit^1]; + if (val (lit)) return false; + if (opts.elimgain <= 1 && (pos <= 1 || neg <= 1)) return true; + if (opts.elimgain <= 0 && pos <= 2 && neg <= 2) return true; + LOG ("trelim " << lit << " bound " << elms[idx].heat); + if (gate) LOG ("actually trelim gate for " << gatepivot); + for (int sign = 0; sign <= 1; sign++) + for (int i = 0; i < orgs[lit^sign]; i++) + if (orgs[lit^sign][i]->size > (unsigned)opts.elimclim) + return false; + int gain = pos + neg, l = opts.elimgain, found, i, j; + Cls * c, * d; + if (gate) { + assert (gatepivot/2 == lit/2); + int piv, s0, e0, s1, e1; + piv = gatepivot; + s0 = 0, e0 = posgate; + s1 = posgate, e1 = gate; + for (i = s0; !conflict && i < e0 && gain >= l; i++) { + found = 0; + c = gate[i]; + for (j = 0; !conflict && gain >= l && j < orgs[piv^1]; j++) { + d = orgs[piv^1][j]; + if (d->gate) continue; + if (resolve (c, piv, d, true)) gain--, found++; + if (needtoflush ()) { if (!flush ()) return false; goto RESTART; } + if (val (piv)) return false; + if (resotfs) goto RESTART; + if (reslimhit) gain = INT_MIN, found++; + } + if (opts.block && opts.blockimpl && !found) { lit = piv; goto BLKD; } + } + for (i = s1; !conflict && i < e1 && gain >= l; i++) { + found = 0; + c = gate[i]; + for (j = 0; !conflict && gain >= l && j < orgs[piv]; j++) { + d = orgs[piv][j]; + if (d->gate) continue; + if (resolve (d, piv, c, true)) gain--, found++; + if (needtoflush ()) { if (!flush ()) return false; goto RESTART; } + if (val (piv)) return false; + if (resotfs) goto RESTART; + if (reslimhit) gain = INT_MIN, found++; + } + if (opts.block && opts.blockimpl && !found) { lit = 1^piv; goto BLKD; } + } + } else { + for (i = 0; !conflict && gain >= l && i < orgs[lit]; i++) { + found = 0; + c = orgs[lit][i]; + for (j = 0; !conflict && gain >= l && j < orgs[lit^1]; j++) { + d = orgs[lit^1][j]; + if (resolve (c, lit, d, true)) gain--, found++; + if (needtoflush ()) { if (!flush ()) return false; goto RESTART; } + if (val (lit)) return false; + if (resotfs) goto RESTART; + if (reslimhit) gain = INT_MIN, found++; + } + if (opts.block && opts.blockimpl && !found) { +BLKD: + block (c, lit); + stats.blkd.impl++; + goto RESTART; + } + } + } + if (conflict) return false; + LOG ("approximated gain for " << lit << " is " << gain); + if (!val (lit) && gain < l) { + measure = false; + asymode = true; +ASYMMAGAIN: + for (int sign = 0; sign <= 1; sign++, lit^=1) { + if (orgs[lit] < 2) goto DONE; + assert (!val (lit)); + if (orgs[lit] <= opts.elimasym) { + if (limit.props.asym < 0) goto DONE; + long long old = stats.props.simp; + LOG ("trying to eliminate one out of " << orgs[lit] << + " occurences of " << lit); + for (i = orgs[lit]-1; !conflict && i >= 0; i--) { + Cls * c = orgs[lit][i]; + if (c->gate) continue; +#ifndef NLOGPRECO + dbgprint ("LOG trying to eliminate literal from ", c); +#endif + assert (c->lits[1]); + assume (lit); + bool ok = bcp (), fl = true; + int other; + for (const int * p = c->lits; ok && (other = *p); p++) { + if (val (other)) continue; + assert (other != lit); + assume (other^1); + ok = bcp (); + fl = false; + } + undo (0); + if (ok) { + limit.props.asym -= stats.props.simp - old; + continue; + } + stats.str.asym++; + LOG ("asymmetric branching eliminates literal " << lit); + if (fl) assign (lit^1); else remove (lit, c); + limit.props.asym += opts.elimasymreward; + if (val (lit)) goto DONE; + if (needtoflush ()) { + if (!flush ()) goto DONE; + if (val (lit)) goto DONE; + goto ASYMMAGAIN; + } + if (orgs[lit] < 2) goto DONE; + if (orgs[lit] == 2 && orgs[lit^1] == 2) goto DONE; + } + } + } +DONE: + measure = true; + asymode = false; + if (conflict) return false; + if (vals[lit]) return false; + if (opts.elimgain <= 1 && (orgs[lit] <= 1 || orgs[1^lit] <= 1)) + return true; + if (opts.elimgain <= 0 && orgs[lit] <= 2 && orgs[1^lit] <= 2) + return true; + } + return gain >= l; +} + +void Solver::elim (int idx) { + assert (!elimvar); + elimvar = idx; + int lit = 2 * idx; + assert (!conflict); + assert (!units); + assert (queue == trail); + assert (vars[idx].type == FREE); + assert (!vals[lit]); + assert (!repr[lit]); +#if 0 +#ifndef NLOGPRECO + dbgprint (); +#endif +#endif + LOG ("elim " << lit); + assert (!vals[lit] && !repr[lit]); + { + int slit; + Cls ** begin, ** end; + if (gate) { + slit = gatepivot; + int pos = posgate; + int neg = gate - pos; + assert (pos > 0 && neg > 0); + begin = gate.begin (); + if (pos < neg) end = begin + posgate; + else begin += posgate, end = gate.end (), slit ^= 1; + } else { + slit = lit; + int pos = orgs[lit]; + int neg = orgs[lit^1]; + if (!pos && !neg) zombie (vars + idx); + else if (!pos) pure (lit^1); + else if (!neg) pure (lit); + if (!pos || !neg) { elimvar = 0; return; } + if (pos < neg) begin = orgs[lit].begin (), end = orgs[lit].end (); + else begin = orgs[1^lit].begin (), end = orgs[1^lit].end (), slit ^= 1; + } + elits.push (mem, 0); + LOG ("elit 0"); + for (Cls ** p = begin; p < end; p++) { + elits.push (mem, 0); + LOG ("elit 0"); + Cls * c = *p; + int other; + for (int * p = c->lits; (other = *p); p++) { + if (other == (slit)) continue; + assert (other != (1^slit)); + elits.push (mem, other); + LOG ("elit " << other); + } + } + elits.push (mem, slit); + LOG ("elit " << slit); + elits.push (mem, 0); + } + + vars[idx].type = ELIM; + stats.vars.elim++; + + for (int sign = 0; sign <= 1; sign++) + for (int i = 0; i < orgs[lit^sign]; i++) { + Cls * c = orgs[lit^sign][i]; + c->dirty = true; + } + + int gatecount = gate; + if (gatecount) { + LOG ("actually elim gate for " << gatepivot); + assert (gatepivot/2 == lit/2); + int piv = gatepivot; + for (int i = 0; !conflict && i < posgate; i++) + for (int j = 0; !conflict && j < orgs[piv^1]; j++) + resolve (gate[i], piv, orgs[piv^1][j], false); + for (int i = posgate; !conflict && i < gate; i++) + for (int j = 0; !conflict && j < orgs[piv]; j++) + resolve (orgs[piv][j], piv, gate[i], false); + } else { + for (int i = 0; !conflict && i < orgs[lit]; i++) + for (int j = 0; !conflict && j < orgs[lit^1]; j++) + resolve (orgs[lit][i], lit, orgs[lit^1][j], false); + } + + for (int sign = 0; sign <= 1; sign++) + for (int i = 0; i < orgs[lit^sign]; i++) + orgs[lit^sign][i]->dirty = false; + + assert (gate == gatecount); + cleangate (), cleantrash (); + + for (int sign = 0; sign <= 1; sign++) + recycle (lit^sign); + + elimvar = 0; +} + +inline long long Solver::clauses () const { + return stats.clauses.orig + stats.clauses.lnd + stats.clauses.bin; +} + +inline bool Solver::hasgate (int idx) { + assert (0 < idx && idx <= maxvar); + assert (!gate); + int lit = 2*idx; + if (andgate (lit)) return true; + if (andgate (1^lit)) return true; + if (xorgate (lit)) return true; + if (itegate (lit)) return true; + return false; +} + +void Solver::cleans () { + assert (!level); + assert (elimode || blkmode); + assert (orgs); + for (int i = 0; i <= 3 + (int)opts.glue; i++) { + Cls * p = 0; + if (i == 0) p = binary.head; + if (i == 1) p = original.head; + if (i == 2) p = fresh.head; + if (i >= 3) p = learned[i-3].head; + while (p) { + assert (!p->locked); assert (!p->garbage); + Cls * prev = p->prev; + int other; + for (int * q = p->lits; (other = *q); q++) { + Var * v = vars + (other/2); + if (v->type == FREE) continue; + if (v->type == FIXED) continue; + break; + } + if (other) { /*assert (p->lnd);*/ p->garbage = true; } + p = prev; + } + } +} + +void Solver::elim () { + if (!eliminating ()) return; + stats.elim.phases++; + elimode = true; + elimvar = 0; + checkclean (); + disconnect (); + initorgs (); + initfwds (); + initfwsigs (); + clrbwsigs (); + connect (binary, true); + connect (original, true); + if (!flush ()) return; + int repcounter = 111; + long long bound; + limit.budget.bw.sub = limit.budget.fw.sub = opts.elimint; + limit.budget.bw.str = limit.budget.fw.str = opts.elimint; + if (opts.rtc == 2 || opts.elimrtc == 2 || + ((opts.rtc == 1 || opts.elimrtc == 1) && !stats.elim.rounds)) + bound = LLONG_MAX; + else { + bound = stats.elim.resolutions + opts.elimint; + for (int i = stats.elim.phases; i <= opts.elimboost; i++) + bound += opts.elimint; + } + limit.props.asym = opts.elimasymint; + if (schedule.elim) { + for (int idx = 1; idx <= maxvar; idx++) { + int lit = 2*idx, pos = orgs[lit], neg = orgs[lit^1]; + if (pos <= 2 || neg <= 2 || schedule.elim.contains (elms + idx)) + touch (lit); + } + } else { + for (int idx = 1; idx <= maxvar; idx++) touch (2*idx); + } + pure (); + report (2, 'e'); + while (!conflict && schedule.elim) { + Rnk * e = schedule.elim.max (); + int idx = e - elms, lit = 2*idx, pos = orgs[lit], neg = orgs[1^lit]; + if (pos > 1 && neg > 1 && (pos > 2 || neg > 2)) + if (stats.elim.resolutions > bound) break; + if (!--repcounter) { + if (terminal) report (2, 'e'); + repcounter = 111; + } + (void) schedule.elim.pop (); + Var * v = vars + idx; + if (v->type != FREE) continue; + if (!pos && !neg) zombie (vars + idx); + else if (!pos) pure (lit^1); + else if (!neg) pure (lit); + else { + if (hasgate (idx)) assert (gatestats), checkgate (); + bool eliminate = trelim (idx); + if (needtoflush () && !flush ()) break; + if (!eliminate || vals[lit]) { cleangate (); continue; } + if (gatestats) { + gatestats->count += 1; + gatestats->len += gatelen; + stats.vars.subst++; + } + elim (idx); + if (needtoflush () && !flush ()) break; + if (bound != LLONG_MAX) bound += opts.elimreward; + } + } + + report (2, 'e'); + +#ifndef NDEBUG + for (int idx = 1; !conflict && idx <= maxvar; idx++) { + if (vars[idx].type != FREE) continue; + if (elms[idx].pos == -1) continue; + int lit = 2*idx, pos = orgs[lit], neg = orgs[lit+1]; + assert (pos >= 2); + assert (neg >= 2); + assert (pos != 2 || neg != 2); + } +#endif + + if (conflict) return; + + assert (!gate); + assert (!trash); + + if (bound != LLONG_MAX) pure (); + cleans (); + delorgs (); + delfwds (); + delfwsigs (); + gc (); + checkeliminated (); + elimode = false; + + if (!schedule.elim) { + stats.elim.rounds++; + limit.fixed.elim = remvars (); + } + limit.props.elim = opts.elimprd; + limit.props.elim *= opts.elimint; + limit.props.elim += stats.props.srch; + checkvarstats (); +} + +void Solver::zombie (Var * v) { + assert (elimode || blkmode); + assert (!level); + assert (v->type == FREE); + int idx = v - vars, lit = 2*idx; + assert (!val (lit)); + assert (!orgs[lit]); + assert (!orgs[lit^1]); + assert (!repr [lit]); + if (puremode) { + LOG ("explicit zombie literal " << lit); + stats.zombies.expl++; + } else if (blkmode) { + LOG ("blocking zombie literal " << lit); + stats.zombies.blkd++; + } else { + assert (elimode); + LOG ("eliminating zombie literal " << lit); + stats.zombies.elim++; + } + stats.vars.zombies++; + v->type = ZOMBIE; + assume (lit, false); + recycle (lit); + recycle (lit^1); + flush (); + assert (!conflict); +} + +void Solver::pure (int lit) { + assert (elimode || blkmode); + assert (!level); + assert (!val (lit)); + assert (!orgs[lit^1]); + assert (!repr [lit]); + Var * v = vars + (lit/2); + assert (v->type == FREE); + if (puremode) { + LOG ("explicit pure literal " << lit); + stats.pure.expl++; + } else if (blkmode) { + LOG ("blocking pure literal " << lit); + stats.pure.blkd++; + } else { + assert (elimode); + LOG ("eliminating pure literal " << lit); + stats.pure.elim++; + } + stats.vars.pure++; + v->type = PURE; + assume (lit, false); + flush (); + assert (!conflict); +} + +void Solver::block () { + if (!blocking ()) return; + stats.blkd.phases++; + blkmode = true; + blklit = 0; + checkclean (); + disconnect (); + initorgs (); + connect (binary, true); + connect (original, true); + if (!flush ()) return; + int repcounter = 111; + long long bound; + if (opts.rtc == 2 || opts.blockrtc == 2 || + ((opts.rtc == 1 || opts.blockrtc == 1) && !stats.blkd.rounds)) { + bound = LLONG_MAX; + } else { + bound = stats.blkd.resolutions + opts.blockint; + for (int i = stats.blkd.phases; i <= opts.blockboost; i++) + bound += opts.blockint; + } + if (schedule.block) { + for (int lit = 2; lit <= 2*maxvar+1; lit++) + if (schedule.block.contains (blks + lit)) touchblkd (lit); + } else { + for (int lit = 2; lit <= 2*maxvar+1; lit++) touchblkd (lit); + } + pure (); + report (2, 'k'); + while (!conflict && schedule.block && stats.blkd.resolutions <= bound) { + Rnk * b = schedule.block.pop (); + int lit = b - blks; + if (!repcounter--) { + if (terminal) report (2, 'k'); + repcounter = 111; + } +RESTART: + Var * v = vars + (lit/2); + if (v->type != FREE) continue; + int pos = orgs[lit], neg = orgs[1^lit]; + if (!pos && !neg) zombie (v); + else if (!pos) pure (1^lit); + else if (!neg) pure (lit); + else if (orgs[lit] <= opts.blkmaxlen || orgs[1^lit] <= opts.blkmaxlen) { + assert (!val (lit)); + if (orgs[1^lit] > opts.blkmaxlen) continue; + LOG ("tryblk " << lit); + for (int i = orgs[lit]-1; !conflict && i >= 0; i--) { + Cls * c = orgs[lit][i]; + bool blocked = true; + for (int j = 0; !conflict && blocked && j < orgs[lit^1]; j++) { + blocked = !resolve (c, lit, orgs[lit^1][j], true); + if (needtoflush ()) { if (!flush ()) goto DONE; goto RESTART; } + if (blocked && resotfs) goto RESTART; + } + if (!blocked) continue; + if (conflict) break; + if (val (lit)) break; + block (c, lit); + stats.blkd.expl++; + if (bound != LLONG_MAX) bound += opts.blockreward; + } + } + } +DONE: + report (2, 'k'); + if (conflict) return; + assert (schedule.block || stats.clauses.irr != 1); + if (bound != LLONG_MAX) pure (); + cleans (); + delorgs (); + gc (); + blkmode = false; + + if (!schedule.block) { + stats.blkd.rounds++; + limit.fixed.block = remvars (); + } + limit.props.block = opts.blockprd; + limit.props.block *= opts.blockint; + limit.props.block += stats.props.srch; + checkvarstats (); +} + +void Solver::pure () { + assert (orgs); + assert (blkmode || elimode); + assert (!puremode); + if (!flush ()) return; + puremode = true; + assert (!plits); + report (2, 'u'); + for (int idx = 1; idx <= maxvar; idx++) { + Var * v = vars + idx; + assert (!v->onplits); + if (v->type != FREE) continue; + plits.push (mem, idx); + v->onplits = true; + } + while (plits) { + int idx = plits.pop (), lit = 2*idx; + Var * v = vars + idx; + assert (v->type == FREE); + assert (v->onplits); + if (!orgs[lit] && !orgs[lit^1]) zombie (v); + else if (!orgs[lit]) pure (1^lit); + else if (!orgs[1^lit]) pure (lit); + v->onplits = false; + } + puremode = false; + report (2, 'u'); +} + +void Solver::jwh () { + memset (jwhs, 0, 2 * (maxvar + 1) * sizeof *jwhs); + for (Cls * p = original.head; p; p = p->prev) jwh (p); + for (Cls * p = binary.head; p; p = p->prev) jwh (p); + for (Cls * p = fresh.head; p; p = p->prev) jwh (p); + for (int glue = 0; glue <= opts.glue; glue++) + for (Cls * p = learned[glue].head; p; p = p->prev) jwh (p); +} + +void Solver::initfresh () { + limit.reduce.fresh = (opts.fresh * limit.reduce.learned + 99) / 100; + report (2, 'F'); +} + +void Solver::initreduce () { + int l; + if (opts.liminitmode) l = (opts.liminitpercent*stats.clauses.orig + 99)/100; + else l = opts.liminitconst; + if (l > opts.liminitmax) l = opts.liminitmax; + if (l > opts.maxlimit) l = opts.maxlimit; + if (l < opts.minlimit) l = opts.minlimit; + limit.enlarge.conflicts = limit.enlarge.inc = limit.enlarge.init = l; + limit.reduce.learned = limit.reduce.init = l; + initfresh (); + report (1, 'l'); +} + +void Solver::enlarge () { + stats.enlarged++; + if (opts.limincmode) { + limit.reduce.learned = + ((100 + opts.limincpercent) * limit.reduce.learned + 99) / 100; + limit.enlarge.inc = ((100 + opts.enlinc) * limit.enlarge.inc + 99) / 100; + limit.enlarge.conflicts = stats.conflicts + limit.enlarge.inc; + } else { + limit.enlarge.inc += opts.liminconst1; + limit.enlarge.conflicts += limit.enlarge.inc; + limit.reduce.learned += opts.liminconst2; + } + if (limit.reduce.learned > opts.maxlimit) { + limit.reduce.learned = opts.maxlimit; + limit.enlarge.conflicts = INT_MAX; + } + initfresh (); + report (1, '+'); +} + +void Solver::shrink (int old) { + if (!opts.shrink) return; + if (limit.reduce.learned <= opts.minlimit) return; + + int now = stats.clauses.orig; + if (!now) return; + old /= 100, now /= 100; + if (old <= now) return; + assert (old); + + int red = (100 * (old - now)) / old; + assert (red <= 100); + if (!red) return; + + int rl = limit.reduce.learned, drl; + drl = (opts.shrink < 2) ? limit.reduce.init : rl; + drl *= (opts.shrinkfactor*red+99)/100; + rl -= drl/100; + if (rl < opts.minlimit) rl = opts.minlimit; + if (limit.reduce.learned == rl) return; + + limit.reduce.learned = rl; + stats.shrunken++; + + initfresh (); + report (1, '-'); +} + +void Solver::simplify () { + stats.sw2simp (); + int old = stats.clauses.orig, inc, rv; + undo (0); +RESTART: + simplified = false; + decompose (); + if (conflict) goto DONE; + gc (); + if (conflict) goto DONE; + block (); + if (conflict) goto DONE; + elim (); + if (conflict) goto DONE; + if (simplified && + ((opts.rtc == 2 || opts.simprtc == 2) || + ((opts.rtc == 1 || opts.simprtc == 1) && !stats.simps))) + goto RESTART; + jwh (); + limit.props.simp = stats.props.srch + simprd * clauses (); + limit.simp = stats.vars.fixed + stats.vars.merged; + limit.fixed.simp = stats.vars.fixed; + rv = remvars (); + inc = opts.simpinc; + if (rv) while (rv < 1000000) rv *= 10, inc /= 2; + simprd *= 100 + inc; simprd += 99; simprd /= 100; + report (1, 's'); + if (!stats.simps) initreduce (); + else shrink (old); +DONE: + if (opts.print) print (); + stats.simps++; + stats.sw2srch (); +} + +void Solver::flushunits () { + assert (units); + undo (0); + while (units && !conflict) unit (units.pop ()); + flush (); +} + +void Solver::initrestart () { + int delta; + limit.restart.conflicts = stats.conflicts; + if (opts.luby) delta = opts.restartint * luby (limit.restart.lcnt = 1); + else delta = limit.restart.inner = limit.restart.outer = opts.restartint; + limit.restart.conflicts += delta; +} + +void Solver::initbias () { + jwh (); + limit.rebias.conflicts = opts.rebiasint * luby (limit.rebias.lcnt = 1); + limit.rebias.conflicts += stats.conflicts; +} + +void Solver::iteration () { + assert (!level); + assert (iterating); + assert (limit.fixed.iter < trail); + stats.iter++; + initrestart (); + int old = stats.clauses.orig; + while (limit.fixed.iter < trail) { + int lit = trail[limit.fixed.iter++]; + recycle (lit); + } + iterating = false; + report (2, 'i'); + shrink (old); +} + +inline bool Solver::reducing () const { + int learned_not_locked = stats.clauses.lnd; + learned_not_locked -= stats.clauses.lckd; + return 2 * learned_not_locked > 3 * limit.reduce.learned; +} + +inline bool Solver::eliminating () const { + if (!opts.elim) return false; + if (!stats.elim.phases) return true; + if (opts.rtc == 2 || opts.simprtc == 2 || + ((opts.rtc == 1 || opts.simprtc == 1) && !stats.simps)) return true; + if (schedule.elim) return true; + if (stats.props.srch <= limit.props.elim) return false; + return remvars () < limit.fixed.elim; +} + +inline bool Solver::blocking () const { + if (!opts.block) return false; + if (!stats.elim.phases) return true; + if (opts.rtc == 2 || opts.simprtc == 2 || + ((opts.rtc == 1 || opts.simprtc == 1) && !stats.simps)) return true; + if (schedule.block) return true; + if (stats.props.srch <= limit.props.block) return false; + return remvars () < limit.fixed.block; +} + +inline bool Solver::simplifying () const { + if (!stats.simps) return true; + if (stats.props.srch < limit.props.simp) return false; + return limit.simp < stats.vars.fixed + stats.vars.merged; +} + +inline bool Solver::restarting () const { + return level >= 2 && limit.restart.conflicts <= stats.conflicts; +} + +inline bool Solver::rebiasing () const { + return limit.rebias.conflicts <= stats.conflicts; +} + +inline bool Solver::probing () const { + if (!opts.probe) return false; + if (stats.props.srch < limit.props.probe) return false; + if (!level) return true; + if (schedule.probe) return true; + return limit.fixed.probe < stats.vars.fixed; +} + +inline bool Solver::enlarging () const { + if (limit.reduce.learned >= opts.maxlimit) return false; + return stats.conflicts >= limit.enlarge.conflicts; +} + +inline bool Solver::exhausted () const { + return stats.decisions >= limit.decisions; +} + +int Solver::search () { + stats.entered2 = seconds (); + for (;;) + if (!bcp ()) { if (!analyze ()) return -1; } + else if (iterating) iteration (); + else if (units) flushunits (); + else if (probing ()) probe (); + else if (simplifying ()) simplify (); + else if (rebiasing ()) rebias (); + else if (restarting ()) restart (); + else if (reducing ()) reduce (); + else if (enlarging ()) enlarge (); + else if (exhausted ()) return 0; + else if (!decide ()) return 1; + stats.srchtime += seconds () - stats.entered2; +} + +void Solver::initlimit (int decision_limit) { + memset (&limit, 0, sizeof limit); + limit.decisions = decision_limit; + simprd = opts.simprd; + rng.init (opts.seed); +} + +void Solver::initsearch (int decision_limit) { + assert (opts.fixed); + initlimit (decision_limit); + initbias (); + initrestart (); + report (1, '*'); +} + +int Solver::solve (int decision_limit) { + initsearch (decision_limit); + int res = search (); + report (1, res < 0 ? '0' : (res ? '1' : '?')); + if (!stats.simps && opts.print) print (); + return res; +} + +double Stats::now () { + struct rusage u; + if (getrusage (RUSAGE_SELF, &u)) + return 0; + double res = u.ru_utime.tv_sec + 1e-6 * u.ru_utime.tv_usec; + res += u.ru_stime.tv_sec + 1e-6 * u.ru_stime.tv_usec; + return res; +} + +double Stats::seconds () { + double t = now (), delta = t - entered; + delta = (delta < 0) ? 0 : delta; + time += delta; + entered = t; + return time; +} + +void Stats::sw2srch () { + double t = seconds (); + simptime += t - entered2; + entered2 = t; +} + +void Stats::sw2simp () { + double t = seconds (); + srchtime += t - entered2; + entered2 = t; +} + +Stats::Stats () { + memset (this, 0, sizeof *this); + entered = now (); +} + +Limit::Limit () { + memset (this, 0, sizeof *this); + budget.fw.sub = budget.bw.sub = budget.bw.str = budget.fw.str = 10000; +} + +void PrecoSat::die (const char * msg, ...) { + va_list ap; + fprintf (stdout, "c\nc\nc "); + va_start (ap, msg); + vfprintf (stdout, msg, ap); + va_end (ap); + fputs ("\nc\nc\n", stdout); + fflush (stdout); + abort (); +} + +void Solver::print () { + bool close_file; + FILE * file; + if (opts.output) { + file = fopen (opts.output, "w"); + if (!file) die ("can not write '%s'", opts.output); + close_file = true; + } else file = stdout, close_file = false; + + assert (!level); + + int m, n; + if (conflict) fprintf (file, "p cnf 0 1\n0\n"), m=0, n=1; + else { + size_t bytes = 2*(maxvar+1) * sizeof (int); + int * map = (int*) mem.callocate (bytes); + m = 0; + for (int idx = 1; idx <= maxvar; idx++) + if (vars[idx].type == FREE) map[idx] = ++m; + + assert (m == remvars ()); + + n = 0; + for (int i = 0; i <= 1; i++) + for (Cls * p = (i ? original : binary).tail; p; p = p->next) + if (!p->lnd && !satisfied (p)) n++; + + fprintf (file, "p cnf %d %d\n", m, n); + fflush (file); + + for (int i = 0; i <= 1; i++) + for (Cls * p = (i ? binary : original).tail; p; p = p->next) { + if (p->lnd) continue; + if (satisfied (p)) continue; + int lit; + for (int * q = p->lits; (lit = *q); q++) { + Val tmp = val (lit); + if (tmp < 0) continue; + assert (!tmp); + int ilit = map[lit/2]; + if (lit&1) ilit = -ilit; + fprintf (file, "%d ", ilit); + } + fputs ("0\n", file); + } + mem.deallocate (map, bytes); + } + if (close_file) fclose (file); + + report (1, 'w'); +} + +void Cls::print (const char * prefix) const { + fputs (prefix, stdout); + for (const int * p = lits; *p; p++) { + if (p != lits) fputc (' ', stdout); + printf ("%d", *p); + } + fputc ('\n', stdout); +} + +void Solver::dbgprint (const char * type, Anchor& anchor) { + size_t len = strlen (type) + strlen (prfx) + 80; + char * str = (char*) mem.allocate (len); + sprintf (str, "%sPRINT %s clause ", prfx, type); + for (Cls * p = anchor.tail; p; p = p->next) p->print (str); + mem.deallocate (str, len); +} + +void Solver::dbgprint (const char * type, Cls * cls) { + size_t len = strlen (type) + strlen (prfx) + 1; + char * str = (char*) mem.allocate (len); + sprintf (str, "%s%s", prfx, type); + cls->print (str); + mem.deallocate (str, len); +} + +void Solver::dbgprint () { + dbgprint ("binary", binary); + dbgprint ("original", original); + for (int glue = 0; glue <= opts.glue; glue++) { + char buffer[80]; + sprintf (buffer, "learned[%u]", glue); + dbgprint (buffer, learned[glue]); + } + dbgprint ("fresh", fresh); +} + +void Solver::dbgprintgate () { + for (Cls ** p = gate.begin(); p < gate.end (); p++) { + printf ("%sLOG gate clause", prfx); + Cls * c = *p; + for (const int * q = c->lits; *q; q++) + printf (" %d", *q); + printf ("\n"); + } +} diff --git a/backends/precosat/precosat.hh b/backends/precosat/precosat.hh new file mode 100644 index 0000000..0b95058 --- /dev/null +++ b/backends/precosat/precosat.hh @@ -0,0 +1,732 @@ +/*************************************************************************** +Copyright (c) 2009, 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. +****************************************************************************/ + +#ifndef PrecoSat_hh_INCLUDED +#define PrecoSat_hh_INCLUDED + +#include +#include +#include +#include +#include +#include + +namespace PrecoSat { + +void die (const char *, ...); + +class Mem { +public: + typedef void * (*NewFun)(void *, size_t); + typedef void (*DeleteFun)(void *, void*, size_t); + typedef void * (*ResizeFun)(void *, void *, size_t, size_t); +private: + size_t cur, max; + void * emgr; NewFun newfun; DeleteFun deletefun; ResizeFun resizefun; + void operator += (size_t b) { if ((cur += b) > max) max = cur; } + void operator -= (size_t b) { assert (cur >= b); cur -= b; } +public: + Mem () : cur(0), max(0), emgr(0), newfun(0), deletefun(0), resizefun(0) { } + void set (void * e, NewFun n, DeleteFun d, ResizeFun r) { + assert (e && n && d && r); + emgr = e; newfun = n; deletefun = d; resizefun = r; + } + operator size_t () const { return cur; } + size_t getCurrent () const { return cur; } + size_t getMax () const { return max; } + void * allocate (size_t bytes) { + size_t mb = bytes >> 20; + void * res; + res = newfun ? newfun (emgr, bytes) : malloc (bytes); + if (!res) die ("out of memory allocating %d MB", mb); + *this += bytes; + return res; + } + void * callocate (size_t bytes) { + void * res = allocate (bytes); + memset (res, 0, bytes); + return res; + } + void * reallocate (void * ptr, size_t old_bytes, size_t new_bytes) { + size_t mb = new_bytes >> 20; + *this -= old_bytes; + void * res = resizefun ? resizefun (emgr, ptr, old_bytes, new_bytes) : + realloc (ptr, new_bytes); + if (!res) die ("out of memory reallocating %ld MB", (long) mb); + *this += new_bytes; + return res; + } + void * recallocate (void * ptr, size_t o, size_t n) { + char * res = (char*) reallocate (ptr, o, n); + if (n > o) memset (res + o, 0, n - o); + return (void*) res; + } + void deallocate (void * ptr, size_t bytes) { + *this -= bytes; + if (deletefun) deletefun (emgr, ptr, bytes); + else free (ptr); + } +}; + +template class Stack { + T * a, * t, * e; + int size () const { return e - a; } +public: + size_t bytes () const { return size () * sizeof (T); } +private: + void enlarge (Mem & m) { + assert (t == e); + size_t ob = bytes (); + int o = size (); + int s = o ? 2 * o : 1; + size_t nb = s * sizeof (T); + a = (T*) m.reallocate (a, ob, nb); + t = a + o; + e = a + s; + } +public: + Stack () : a (0), t (0), e (0) { } + ~Stack () { free (a); } + operator int () const { return t - a; } + void push (Mem & m, const T & d) { if (t == e) enlarge (m); *t++ = d; } + const T & pop () { assert (a < t); return *--t; } + const T & top () { assert (a < t); return t[-1]; } + T & operator [] (int i) { assert (i < *this); return a[i]; } + void shrink (int m = 0) { assert (m <= *this); t = a + m; } + void shrink (T * nt) { assert (a <= nt); assert (nt <= t); t = nt; } + void release (Mem & m) { m.deallocate (a, bytes ()); a = t = e = 0; } + const T * begin () const { return a; } + const T * end () const { return t; } + T * begin () { return a; } + T * end () { return t; } + void remove (const T & d) { + assert (t > a); + T prev = *--t; + if (prev == d) return; + T * p = t; + for (;;) { + assert (p > a); + T next = *--p; + *p = prev; + if (next == d) return; + prev = next; + } + } +}; + +template class Heap { + Stack stack; + static int left (int p) { return 2 * p + 1; } + static int right (int p) { return 2 * p + 2; } + static int parent (int c) { return (c - 1) / 2; } + static void fix (T * & ptr, ptrdiff_t diff) { + char * charptr = (char *) ptr; + charptr -= diff; + ptr = (T *) charptr; + } +public: + void release (Mem & mem) { stack.release (mem); } + operator int () const { return stack; } + T * operator [] (int i) { return stack[i]; } + bool contains (T * e) const { return e->pos >= 0; } + void up (T * e) { + int epos = e->pos; + while (epos > 0) { + int ppos = parent (epos); + T * p = stack [ppos]; + if (L (p, e)) break; + stack [epos] = p, stack [ppos] = e; + p->pos = epos, epos = ppos; + } + e->pos = epos; + } + void down (T * e) { + assert (contains (e)); + int epos = e->pos, size = stack; + for (;;) { + int cpos = left (epos); + if (cpos >= size) break; + T * c = stack [cpos], * o; + int opos = right (epos); + if (L (e, c)) { + if (opos >= size) break; + o = stack [opos]; + if (L (e, o)) break; + cpos = opos, c = o; + } else if (opos < size) { + o = stack [opos]; + if (!L (c, o)) { cpos = opos; c = o; } + } + stack [cpos] = e, stack [epos] = c; + c->pos = epos, epos = cpos; + } + e->pos = epos; + } + void check () { +#ifndef NDEBUG + for (int ppos = 0; ppos < stack; ppos++) { + T * p = stack[ppos]; + int lpos = left (ppos); + if (lpos < stack) { + T * l = stack[lpos]; + assert (!L (l, p)); + } else break; + int rpos = right (ppos); + if (rpos < stack) { + T * r = stack[rpos]; + assert (!L (r, p)); + } else break; + } +#endif + } + void construct () { + for (int cpos = parent (stack-1); cpos >= 0; cpos--) { + T * e = stack[cpos]; assert (cpos >= 0); down (e); + } + check (); + } + T * max () { assert (stack); return stack[0]; } + void push (Mem & mem, T * e) { + assert (!contains (e)); + e->pos = stack; + stack.push (mem, e); + up (e); + } + T * pop () { + int size = stack; + assert (size); + T * res = stack[0]; + assert (!res->pos); + if (--size) { + T * other = stack[size]; + assert (other->pos == size); + stack[0] = other, other->pos = 0; + stack.shrink (size); + down (other); + } else + stack.shrink (); + res->pos = -1; + return res; + } + void remove (T * e) { + int size = stack; + assert (size > 0); + assert (contains (e)); + int epos = e->pos; + e->pos = -1; + if (--size == epos) { + stack.shrink (size); + } else { + T * last = stack[size]; + if (size == epos) return; + stack[last->pos = epos] = last; + stack.shrink (size); + up (last); + down (last); + } + } + void fix (ptrdiff_t diff) { + for (T ** p = stack.begin (); p < stack.end (); p++) + fix (*p, diff); + } +}; + +template +void dequeue (A & anchor, E * e) { + if (anchor.head == e) { assert (!e->next); anchor.head = e->prev; } + else { assert (e->next); e->next->prev = e->prev; } + if (anchor.tail == e) { assert (!e->prev); anchor.tail = e->next; } + else { assert (e->prev); e->prev->next = e->next; } + e->prev = e->next = 0; + assert (anchor.count > 0); + anchor.count--; +} + +template +bool connected (A & anchor, E * e) { + if (e->prev) return true; + if (e->next) return true; + return anchor.head == e; +} + +template +void push (A & anchor, E * e) { + e->next = 0; + if (anchor.head) anchor.head->next = e; + e->prev = anchor.head; + anchor.head = e; + if (!anchor.tail) anchor.tail = e; + anchor.count++; +} + +template +void enqueue (A & anchor, E * e) { + e->prev = 0; + if (anchor.tail) anchor.tail->prev = e; + e->next = anchor.tail; + anchor.tail = e; + if (!anchor.head) anchor.head = e; + anchor.count++; +} + +template +void mtf (A & a, E * e) { dequeue (a, e); push (a, e); } + +struct Cls; + +template struct Anchor { + E * head, * tail; + long count; + Anchor () : head (0), tail (0), count (0) { } +}; + +struct Rnk { int heat; int pos; }; + +struct Hotter { + Rnk * a, * b; + Hotter (Rnk * r, Rnk * s) : a (r), b (s) { } + operator bool () const { + if (a->heat > b->heat) return true; + if (a->heat < b->heat) return false; + return a < b; + } +}; + +typedef signed char Val; + +enum Vrt { + FREE = 0, + ZOMBIE = 1, + PURE = 2, + ELIM = 3, + EQUIV = 4, + FIXED = 5, +}; + +typedef enum Vrt Vrt; + +struct Var { + Val phase:2, mark:2; + bool onstack:1,removable:1,poison:1; + bool binary:1; + bool onplits:1; + Vrt type : 3; + int tlevel, dlevel, dominator; + union { Cls * cls; int lit; } reason; +}; + +struct Cls { + static const unsigned LDMAXGLUE = 4, MAXGLUE = (1< opts; + Opts () : fixed (false) { } + bool set (const char *, int); + bool set (const char *, const char *); + void add (Mem &, const char * name, int, int *, int, int); + void printoptions (FILE *, const char *prfx) const; +}; + +struct SCC { unsigned idx, min : 31; bool done : 1; }; + +class RNG { + unsigned state; +public: + RNG () : state (0) { } + unsigned next (); + bool oneoutof (unsigned); + void init (unsigned seed) { state = seed; } +}; + +struct Occ { + int blit; + Cls * cls; + Occ (int b, Cls * c) : blit (b), cls (c) { } + bool operator == (const Occ & o) const + { return cls ? o.cls == cls : o.blit == blit; } +}; + +struct Occs { + Stack bins; + Stack large; +}; + +typedef Stack Orgs; +typedef Stack Fwds; + +class Solver { + bool initialized; + Val * vals; + Var * vars; + int * jwhs, * repr, * iirfs; + Occs * occs; + Orgs * orgs; + Fwds * fwds; + unsigned * bwsigs, * fwsigs; + Rnk * rnks, * prbs, * elms, * blks; + struct { Heap decide, probe, elim, block; } schedule; + int maxvar, size, queue, queue2, level, jlevel, uip, open, resolved; + Stack trail, lits, units, levels, saved, elits, plits, check; + Stack frames; + Stack seen; + Stack trash, gate, strnd; + Cls * conflict, empty, dummy; + Anchor original, binary, fresh, learned[Cls::MAXGLUE+1]; + int hinc, simprd, agility, spread, posgate, gatepivot, gatelen, typecount; + int elimvar, blklit; + char lastype; + GateStats * gatestats; + bool terminal, iterating, blkmode, extending; + bool resotfs, reslimhit, simplified, needrescore; + bool measure, elimode, bkdmode, puremode, asymode; + RNG rng; + Stats stats; + Limit limit; + char * prfx; + FILE * out; + Opts opts; + Mem mem; + + Rnk * prb (const Rnk *); + Rnk * rnk (const Var *); + Var * var (const Rnk *); + + int & iirf (Var *, int); + + Val fixed (int lit) const; + + void initerm (); + void initfwds (); + void initfwsigs (); + void initbwsigs (); + void initorgs (); + void initiirfs (); + void clrbwsigs (); + void rszbwsigs (int newsize); + void rsziirfs (int newsize); + void delorgs (); + void delfwds (); + void delfwsigs (); + void delbwsigs (); + void deliirfs (); + void delclauses (Anchor &); + Anchor & anchor (Cls *); + + void initprfx (const char *); + void delprfx (); + + void resize (int); + + void initreduce (); + void initfresh (); + void initbias (); + void initrestart (); + void initlimit (int); + void initsearch (int); + + long long clauses () const; + int recyclelimit () const; + bool recycling () const; + bool reducing () const; + bool eliminating () const; + bool blocking () const; + bool simplifying () const; + bool restarting () const; + bool rebiasing () const; + bool probing () const; + bool enlarging () const; + bool exhausted () const; + + int remvars () const; + + void marklits (Cls *); + void marklits (); + void unmarklits (); + void unmarklits (Cls *); + bool fworgs (); + void bworgs (); + bool fwoccs (); + void bwoccs (bool & learned); + Cls * clause (bool learned, unsigned glue); + unsigned litsig (); + int redundant (Cls *); + void recycle (Cls *); + void recycle (int); + void setsig (Cls *); + void slim (Cls *); + unsigned gluelits (); + bool clt (int, int) const; + void connect (Cls *); + void connect (Anchor&, bool orgonly = false); + void disconnect (Cls *); + void disconnect (); + void collect (Cls *); + int bwstr (unsigned sig, Cls *); + int fwstr (unsigned sig, Cls *); + void remove (int lit, Cls *); + bool fwsub (unsigned sig, Cls *); + bool bwsub (unsigned sig, Cls *); + void assign (int l); + void assume (int l, bool inclevel = true); + void imply (int l, int reason); + int dominator (int l, Cls * reason, bool &); + void force (int l, Cls * reason); + void unit (int l); + bool min2 (int lit, int other, int depth); + bool minl (int lit, Cls *, int depth); + bool strengthen (int lit, int depth); + bool inverse (int lit); + bool minimize (Var *, int depth); + int luby (int); + void report (int v, char ch); + void prop2 (int lit); + void propl (int lit); + void flushunits (); + bool bcp (); + bool needtoflush () const; + bool flush (); + void touchpure (int lit); + void touchelim (int lit); + void touchblkd (int lit); + void touch (int lit); + void touch (Cls *); + void rescore (); + void bump (Cls *); + void bump (Var *, int add); + void bump (); + int phase (Var *); + bool decide (); + void extend (); + void increp (); + void probe (); + int find (int lit); + void merge (int, int, int & merged); + void shrink (int); + void enlarge (); + void checkvarstats (); + void decompose (); + bool resolve (int l, int pivot, int k, bool tryonly); + bool resolve (int l, int pivot, Cls *, bool tryonly); + bool resolve (Cls *, int pivot, Cls *, bool tryonly); + bool andgate (int lit); + Cls * find (int a, int b, int c); + int itegate (int lit, int cond, int t); + bool itegate (int lit); + bool xorgate (int lit); + bool hasgate (int idx); + bool trelim (int idx); + void elim (int idx); + void elim (); + void block (Cls *, int lit); + void block (int lit); + void block (); + void zombie (Var*); + void pure (int lit); + void pure (); + void cleantrash (); + void cleangate (); + void cleanlevels (); + void cleanseen (); + void jump (); + void dump (Cls *); + void gcls (Cls *); + void strcls (Cls *c); + void gc (Anchor &, const char*); + void gc (); + void jwh (Cls *); + void jwh (); + void reduce (); + void simplify (); + void iteration (); + void restart (); + void rebias (); + void undo (int newlevel, bool save = false); + void pull (int lit); + bool analyze (); + + void checkeliminated (); + void cleans (); + void checkclean (); + + void import (); + int search (); + bool satisfied (const Cls*); + bool satisfied (Anchor &); + + void print (); + + void dbgprint (const char *, Cls *); + void dbgprint (const char *, Anchor &); + void dbgprint (); + void dbgprintgate (); + + void checkgate (); + +public: + + Solver () : initialized (false) { } + + void set (void * e, Mem::NewFun n, Mem::DeleteFun d, Mem::ResizeFun r) { + mem.set (e, n, d, r); + } + void setprfx (const char* newprfx) { delprfx (); initprfx (newprfx); } + bool set (const char * option, int arg) { return opts.set (option, arg); } + bool set (const char * o, const char * a) { return opts.set (o, a); } + void set (FILE * file) { out = file; initerm (); } + + void init (int initial_maxvar = 0); + void fxopts (); + + void add (int lit) { if (lit) lits.push (mem, lit); else import (); } + int next () { int res = maxvar + 1; resize (res); return res; } + int solve (int decision_limit = INT_MAX); + int val (int l) { return vals[find (l)]; } + double seconds () { return stats.seconds (); } + bool satisfied (); + void prstats (); + void propts (); + void reset (); + int getMaxVar () const { return maxvar; } +}; + +}; + +#endif -- 2.11.4.GIT