lrat-check.c

/************************************************************************************[lrat-check.c]
Copyright (c) 2017-2021 Marijn Heule, Carnegie Mellon University
Last edit: September 12, 2021

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 <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include <limits.h>
#include <sys/time.h>

#define PRINT		0
#define DELETED		-1
#define CONFLICT	2
#define SUCCESS		1
#define FAILED		0
#define CNF		100
#define LRAT		200
#define CLRAT		300
#define BUCKET		8192
#define INIT		1024

void usage(char *name) {
  printf("Usage: %s FILE1.cnf FILE2.lrat [optional: FILE3.drat]\n", name);
  exit(0);
}

#ifdef LONGTYPE
  typedef long long ltype;
#else
  typedef int ltype;
#endif
typedef int mtype;

ltype added_clauses = 0;
ltype deleted_clauses = 0;
ltype live_clauses = 0;
ltype max_live_clauses = 0;

ltype *mask, *intro, now, lastIndex;

int maxBucket;

int *clsList, clsAlloc, clsLast;
int *table, tableSize, tableAlloc, maskAlloc;
int *litList, litCount, litAlloc;
int *inBucket;
int *topTable, topAlloc;

int  getType   (int* list) { return list[1]; }
int  getIndex  (int* list) { return list[0]; }
int  getLength (int* list) { int i = 2; while (list[i]) i++; return i - 2; }
int* getHints  (int* list) { return list + getLength (list) + 2; }
int  getRATs   (int* list) { int c = 0; while (*list) if ((*list++) < 0) c++; return c; }

int convertLit (int lit)   { return (abs(lit) * 2) + (lit < 0); }
int printLit   (int lit)   { return (lit >> 1) * (-2 * (lit&1) + 1); }

inline int getClause (int index) {
  int bucket = index / BUCKET;
  int offset = index % BUCKET;
  return clsList[topTable[bucket]*BUCKET + offset]; }

inline void setClause (int index, int value) {
  int bucket = index / BUCKET;
  int offset = index % BUCKET;
  clsList[topTable[bucket]*BUCKET + offset] = value; }

void printClause (int* clause) {
  while (*clause) printf ("%i ", *clause++); printf ("0\n"); }

int checkRedundancy (int pivot, int start, int *hints, ltype thisMask, int print) {
  int res = abs(*hints++);
  assert (start <= res);


  if (print) printf ("c check redundancy res: %i pivot: %i start: %i\n", res, printLit(pivot), start);
  if (res != 0) {
    while (start < res) {
      if (getClause(start++) != DELETED) {
        int *clause = table + getClause(start-1);
        while (*clause) {
          int clit = convertLit (*clause++);
          if (clit == (pivot^1)) { printf ("c FAILED tautology %i\n", pivot); return FAILED; } } } }
    if (getClause(res) == DELETED) { printf ("c ERROR: using DELETED clause %i\n", res); return FAILED; };
    int flag = 0, *clause = table + getClause(res);
    while (*clause) {
      int clit = convertLit (*clause++);
      if (clit == (pivot^1)) { flag = 1; continue; }
      if (mask[clit  ] >= thisMask) continue;       // lit is falsified
      if (mask[clit^1] >= thisMask) return SUCCESS; // blocked
      mask[clit] = thisMask; }
    if (flag == 0) { printf ("c FAILED: pivot %i not found\n", pivot); return FAILED; } }

  while (*hints > 0) {
    if (print) {
      printf ("c hint %i\nc ", *hints);
      int* c = table + getClause(*hints); printClause (c); }
    if (getClause(*hints) == DELETED) { printf ("c ERROR: using DELETED hint clause %i\n", *hints); printf ("c %i\n", topTable[*hints/BUCKET]); return FAILED; };
    int unit = 0, *clause = table + getClause(*(hints++));
    while (*clause) {
      int clit = convertLit (*(clause++));
      if (mask[clit] >= thisMask) continue; // lit is falsified
      if (unit != 0) { printf ("c FAILED: multiple literals unassigned in hint %i: %i %i\n", hints[-1], unit%2?(-unit >> 1):(unit>>1), clit%2?(-clit >> 1):(clit>>1));
                       return FAILED; }
      unit = clit; }
    if (print) {
      if (unit != 0) printf ("c unit %i\n", printLit(unit));
      else           printf ("c detected conflict\n"); }
    if (unit == 0) return CONFLICT;  // detected conflict
    if (mask[unit^1] == thisMask) printf ("c WARNING hint already satisfied in lemma with index %lli\n", (long long) lastIndex);
    mask[unit^1] = thisMask; }

  if (res == 0) return SUCCESS;
  return FAILED; }

int checkClause (int* list, int size, int* hints, int print) {
  now++;
  int pivot = convertLit (list[0]);

  int RATs = getRATs (hints + 1); // the number of negated hints
  for (int i = 0; i < size; i++) { // assign all literals in the clause to false
    int clit = convertLit (list[i]);
    if (clit >= maskAlloc) { // in case we encountered a new literal
      int old = maskAlloc;  // need to set intro?
      maskAlloc = (clit * 3) >> 1;
      if (maskAlloc % 2) maskAlloc++;
      mask  = (ltype *) realloc (mask,  sizeof (ltype) * maskAlloc);
      intro = (ltype *) realloc (intro, sizeof (ltype) * maskAlloc);
      if (!mask || !intro) { printf ("c Memory allocation failure\n"); exit (1); }
      for (int j = old; j < maskAlloc; j++) mask[j] = intro[j] = 0; }
    mask [clit] = now + RATs; } // mark all literals in lemma with mask

  int res = checkRedundancy (pivot, 0, hints, now + RATs, print);
  if (res == CONFLICT) { return SUCCESS; }
  if (res == FAILED  ) { return FAILED;  }

  int *first = hints; first++; while (*first > 0) first++;
  int start = intro[pivot ^ 1];

  if (RATs == 0)      {
    if (print) printf ("c start %i first %i\n", start, -first[0]);
    if (start != 0) return FAILED;
    return SUCCESS; }

  while (start < -first[0]) {  // check whether no clause before -first[0] has -pivot.
    if (getClause(start) != DELETED) {
      int *clause = table + getClause(start);
      while (*clause) {
        int clit = convertLit (*clause++);
        if (clit == (pivot^1)) return FAILED; } }
    start++; }
  intro[pivot ^ 1] = -first[0];


  if (start == 0) return SUCCESS;
  while (1) {
    hints++; now++; while (*hints > 0) hints++;
    if (*hints == 0) break;
    if (-hints[0] < start) printf ("c %i %i\n", -hints[0], start);
    assert (-hints[0] >= start);
    if (checkRedundancy (pivot, start, hints, now, print) == FAILED) return FAILED;
    start = abs(*hints) + 1; }

  while (start <= clsLast) {
    if (getClause(start++) != DELETED) {
      int *clause = table + getClause(start-1);
      while (*clause) {
        int clit = convertLit (*clause++);
        if (clit == (pivot^1)) { printf("c FAILED: tautology %i\n", pivot); return FAILED; } } } }

  return SUCCESS; }

void addClause (int index, int* literals, int size, FILE* drat) {

//  printf ("c index %i\n", index);
  if (index >= topAlloc * BUCKET) {
    int old = topAlloc;
    topAlloc = (topAlloc * 3) >> 1;
    printf ("c topTable reallocation from %i to %i\n", old, topAlloc);
    topTable = (int*) realloc (topTable, sizeof(int) * topAlloc);
    for (int j = old; j < topAlloc; j++) topTable[j] = -1; }

  int count = 0, bucket = topTable[index/BUCKET];
  if (bucket >= 0) count = inBucket[bucket];
  if (bucket == -1) {
//  if (count == 0 || bucket == -1) {
//    printf ("c count %i %i\n", count, topTable[index/BUCKET]);
    for (bucket = 0; bucket < maxBucket; bucket++)
      if (inBucket[bucket] == 0) { topTable[index/BUCKET] = bucket; break; }
//    printf ("c index %i will be in bucket %i\n", index, bucket);
  }

  if (bucket == maxBucket) {
    maxBucket = (maxBucket * 3) >> 1;
    printf ("c increasing the number of buckets from %i to %i\n", bucket, maxBucket);
    inBucket = (int*) realloc (inBucket, sizeof(int) * maxBucket);
    for (int j = bucket; j < maxBucket; j++) inBucket[j] = 0;
    clsList = (int*) realloc (clsList, sizeof(int) * maxBucket * BUCKET);
    for (int i = bucket * BUCKET; i < maxBucket * BUCKET; i++) clsList[i] = DELETED; // is this required?
  }

  topTable[index/BUCKET] = bucket;

  if (tableSize + size >= tableAlloc) {
    tableAlloc = (tableAlloc * 3) >> 1;
    table = (int*) realloc (table, sizeof (int) * tableAlloc); }

  setClause (index, tableSize);
  for (int i = 0; i < size; i++) {
    int clit = convertLit (literals[i]);
    if (intro[clit] == 0) intro[clit] = index;
    if (drat != NULL) fprintf (drat, "%i ", literals[i]);
    table[tableSize++] = literals[i]; }
  if (drat != NULL) fprintf (drat, "0\n");
  table[tableSize++] = 0;
  clsLast = index;

  bucket = topTable[index/BUCKET];
  inBucket[bucket]++;

  added_clauses++;
  live_clauses++;
  if (live_clauses > max_live_clauses)
      max_live_clauses = live_clauses;
}

void deleteClauses (int* list, FILE* drat) {
  while (*list) {
    int index = *list++;
    if (getClause(index) == DELETED) {
      printf ("c WARNING: clause %i is already deleted\n", index); }
    else {
      if (drat) {
        int* clause = table + getClause(index);
        fprintf (drat, "d ");
        while (*clause) fprintf (drat, "%i ", *clause++);
        fprintf (drat, "0\n"); }
      setClause (index, DELETED);
      int bucket = topTable[index/BUCKET];
      inBucket[bucket]--;
      if (inBucket[bucket] == 0) {
        topTable[index/BUCKET] = -1;
//        printf ("c bucket %i is empty\n", bucket);
      }
      deleted_clauses++;
      live_clauses--; }
  }
}

void compress (int index, int print) {
   int* newTable = table;
   int n = 0;
   for (int i = 0; i < topAlloc; i++) {
     if (topTable[i] == -1) continue;
//     int b = topTable[i];
//     printf ("c bucket: %i size: %i\n", b, inBucket[b]);
//     assert (inBucket[b]);
     for (int j = 0; j < BUCKET; j++) {
       int c = i*BUCKET+j;
       if (getClause(c) == DELETED) continue;
       int* clause = table + getClause(c);
       setClause (c, n);
       while (*clause != 0) { newTable[n++] = *clause++; }
       newTable[n++] = 0; }
   }

/*
   for (int i = 0; i < maxBucket; i++) {
     if (inBucket[i] == 0) continue;
     for (int j = 0; j < BUCKET; j++) {
       int c = i*BUCKET+j;
       if (getClause(c) == DELETED) continue;
       int* clause = table + getClause(c);
       setClause (c, n);
       while (*clause != 0) { newTable[n++] = *clause++; }
       newTable[n++] = 0; }
   }
*/
   if (print)
     printf ("c compress at index %i: tableSize reduced from %i to %i\n", index, tableSize, n);
   tableSize = n;
}

static void addLit (int lit) {
  if (litCount >= litAlloc) {
    litAlloc = (litAlloc * 3) >> 1;
    litList = (int*) realloc (litList, sizeof (int) * litAlloc); }
  litList[litCount++] = lit; }

int parseLine (FILE* file, int mode, int line) {
  int lit, tmp;
  litCount = 0;
  char c = 0;
  while (1) {
    tmp = fscanf (file, " c%c", &c);
    if (tmp == EOF) return 0;
    if (tmp ==   0) break;
    while (1) {
      if (tmp == EOF ) return 0;
      if (c   == '\n') break;
      tmp = fscanf (file, "%c", &c); } }

  if (mode == CNF) {
    line++;
    while (1) {
      tmp = fscanf (file, " %i ", &lit);
      if (tmp == 0 || tmp == EOF) return 0;
      int clit = convertLit (lit);
      if (intro[clit] == 0) {
//        printf ("c setting intro[%i] = %i\n", lit, line - 1);
        intro[clit] = line - 1; }
      addLit (lit);
      if (lit == 0) return litCount; } }

  if (mode == LRAT) {
    int index;
    int zeros = 2;
    tmp = fscanf (file, " %i ", &index);
//    printf ("%lli ", index);
//    assert (index > 0);
    if (tmp == 0 || tmp == EOF) return 0;
    addLit ((int) index);

    tmp = fscanf (file, " d %i ", &lit);
    if (tmp == 1) {
      addLit ((int) 'd');
      addLit (lit);
      zeros--;
      if (lit   == 0) zeros--;
      if (zeros == 0) {
	  //	  printf("Processed line %d %c.  Length = %d\n", litList[1], litList[2], litCount);
	  return litCount; }
    }
    else { addLit((int) 'a'); }

    while (1) {
      tmp = fscanf (file, " %i ", &lit);
      if (tmp == 0 || tmp == EOF) return 0;
      addLit(lit);
      if (lit   == 0) zeros--;
      if (zeros == 0) {
	  //	  printf("Processed line %d %c.  Length = %d\n", litList[0], litList[1], litCount);
	  return litCount; }
    }
  }
  return 0; }

int main (int argc, char** argv) {
  if (argc < 3)
     usage(argv[0]);
  struct timeval start_time, finish_time;
  int found_error = 0; // encountered an error?
  int found_empty_clause = 0; // encountered derivation of empty clause?
  gettimeofday(&start_time, NULL);
  now = 0, clsLast = 0;

  int nVar = 0, nCls = 0;
  char ignore[1024];
  FILE* cnf   = fopen (argv[1], "r");
  if (!cnf) {
      printf("Couldn't open file '%s'\n", argv[1]);
      exit(1); }

  for (;;) {
    fscanf (cnf, " p cnf %i %i ", &nVar, &nCls);
    if (nVar > 0) break;
    fgets (ignore, sizeof (ignore), cnf);
    int j; for (j = 0; j < 1024; j++) { if (ignore[j] == '\n') break; }
    if (j == 1024) {
      printf ("c ERROR: comment longer than 1024 characters: %s\n", ignore); exit (0); } }

  topAlloc = INIT;
  topTable = (int*) malloc (sizeof(int) * topAlloc);
  for (int i = 0; i < topAlloc; i++) topTable[i] = -1;

  maxBucket = topAlloc;
  inBucket = (int*) malloc (sizeof(int) * maxBucket);
  for (int i = 0; i < maxBucket; i++) inBucket[i] = 0;
  clsList  = (int*) malloc (sizeof(int) * maxBucket * BUCKET);
  for (int i = 0; i < maxBucket * BUCKET; i++) clsList[i] = DELETED;

  tableSize  = 0;
  tableAlloc = nCls * 2;
  table = (int *) malloc (sizeof(int) * tableAlloc);

  litAlloc = nVar * 10;
  litList = (int*) malloc (sizeof (int) * litAlloc);

  maskAlloc = 20 * nVar;
  mask  = (ltype*) malloc (sizeof(ltype) * maskAlloc);
  intro = (ltype*) malloc (sizeof(ltype) * maskAlloc);
  for (int i = 0; i < maskAlloc; i++) mask[i] = intro[i] = 0;

  int index = 1;
  while (1) {
    int size = parseLine (cnf, CNF, index);
    if (size == 0) break;
    addClause (index++, litList, size, NULL); }
  fclose (cnf);

  printf ("c parsed a formula with %i variables and %i clauses\n", nVar, nCls);

  FILE* proof = fopen (argv[2], "r");
  if (!proof) {
    printf("c Couldn't open file '%s'\n", argv[2]);
    exit(1); }

  FILE* drat = NULL;
  if (argc > 3) {
    drat = fopen (argv[3], "w");
    if (!drat) {
      printf("c Couldn't open file '%s'\n", argv[3]);
      exit(1); } }

  int print = PRINT;
  int mode = LRAT;
  int line = 0;
  ltype del = 0;
  while (1) {
    if (live_clauses < 5 * (deleted_clauses - del)) {
      compress (line, print);
      del = deleted_clauses; }

    int size = parseLine (proof, LRAT, 0);
    if (size == 0) break;

    if (getType (litList) == (int) 'd') {
      deleteClauses (litList + 2, drat); }
    else if (getType (litList) == (int) 'a') {
      line  = getIndex  (litList);
      lastIndex = line;
      int  length = getLength (litList);
      int* hints  = getHints  (litList);

      if (checkClause (litList + 2, length, hints, print) == SUCCESS) {
        addClause (line, litList + 2, length, drat); }
      else {
        printf("c failed while checking clause: "); printClause (litList + 2);
        checkClause (litList + 2, length, hints, 1);
        found_error = 1;
        break;
      }
      if (length == 0)
        found_empty_clause = 1;
    }
    else {
      printf ("c failed type\n");
      found_error = 1;
      break;
    }
  }

  int return_code;
  if (found_empty_clause && !found_error) {
    printf ("c VERIFIED\n");
    return_code = 0;
  } else {
    if (!found_error) {
      // print why the proof failed
      printf ("c checking ended before empty clause was found\n");
    }
    printf ("c NOT VERIFIED\n");
    return_code = 1;
  }

  printf ("c allocated %i %i %i\n", maxBucket, tableAlloc, litAlloc);

  gettimeofday(&finish_time, NULL);
  double secs = (finish_time.tv_sec + 1e-6 * finish_time.tv_usec) -
      (start_time.tv_sec + 1e-6 * start_time.tv_usec);
  printf("c Added clauses = %lld.  Deleted clauses = %lld.  Max live clauses = %lld\n",
	 (long long) added_clauses, (long long) deleted_clauses, (long long) max_live_clauses);
  printf("c verification time = %.2f secs\n", secs);
  return return_code;
}