proof.h

Go to the documentation of this file.

#ifndef _proof_h_INCLUDED
#define _proof_h_INCLUDED
 
#include <stdbool.h>
#include <stdlib.h>
 
#include "global.h"
ABC_NAMESPACE_HEADER_START
 
#ifndef KISSAT_NPROOFS
 
typedef struct proof proof;
 
struct clause;
struct file;
 
void kissat_init_proof (struct kissat *, struct file *, bool binary);
void kissat_release_proof (struct kissat *);
 
#ifndef KISSAT_QUIET
void kissat_print_proof_statistics (struct kissat *, bool verbose);
#endif
 
void kissat_add_binary_to_proof (struct kissat *, unsigned, unsigned);
void kissat_add_clause_to_proof (struct kissat *, const struct clause *c);
void kissat_add_empty_to_proof (struct kissat *);
void kissat_add_lits_to_proof (struct kissat *, size_t, const unsigned *);
void kissat_add_unit_to_proof (struct kissat *, unsigned);
 
void kissat_shrink_clause_in_proof (struct kissat *, const struct clause *,
                                    unsigned remove, unsigned keep);
 
void kissat_delete_binary_from_proof (struct kissat *, unsigned, unsigned);
void kissat_delete_clause_from_proof (struct kissat *,
                                      const struct clause *c);
void kissat_delete_external_from_proof (struct kissat *, size_t,
                                        const int *);
void kissat_delete_internal_from_proof (struct kissat *, size_t,
                                        const unsigned *);
 
#define ADD_BINARY_TO_PROOF(A, B) \
  do { \
    if (solver->proof) \
      kissat_add_binary_to_proof (solver, (A), (B)); \
  } while (0)
 
#define ADD_TERNARY_TO_PROOF(A, B, C) \
  do { \
    if (solver->proof) { \
      unsigned CLAUSE[3] = {(A), (B), (C)}; \
      kissat_add_lits_to_proof (solver, 3, CLAUSE); \
    } \
  } while (0)
 
#define ADD_CLAUSE_TO_PROOF(CLAUSE) \
  do { \
    if (solver->proof) \
      kissat_add_clause_to_proof (solver, (CLAUSE)); \
  } while (0)
 
#define ADD_EMPTY_TO_PROOF() \
  do { \
    if (solver->proof) \
      kissat_add_empty_to_proof (solver); \
  } while (0)
 
#define ADD_LITS_TO_PROOF(SIZE, LITS) \
  do { \
    if (solver->proof) \
      kissat_add_lits_to_proof (solver, (SIZE), (LITS)); \
  } while (0)
 
#define ADD_STACK_TO_PROOF(S) \
  ADD_LITS_TO_PROOF (SIZE_STACK (S), BEGIN_STACK (S))
 
#define ADD_UNIT_TO_PROOF(A) \
  do { \
    if (solver->proof) \
      kissat_add_unit_to_proof (solver, (A)); \
  } while (0)
 
#define SHRINK_CLAUSE_IN_PROOF(C, REMOVE, KEEP) \
  do { \
    if (solver->proof) \
      kissat_shrink_clause_in_proof (solver, (C), (REMOVE), (KEEP)); \
  } while (0)
 
#define DELETE_BINARY_FROM_PROOF(A, B) \
  do { \
    if (solver->proof) \
      kissat_delete_binary_from_proof (solver, (A), (B)); \
  } while (0)
 
#define DELETE_TERNARY_FROM_PROOF(A, B, C) \
  do { \
    if (solver->proof) { \
      unsigned CLAUSE[3] = {(A), (B), (C)}; \
      kissat_delete_internal_from_proof (solver, 3, CLAUSE); \
    } \
  } while (0)
 
#define DELETE_CLAUSE_FROM_PROOF(CLAUSE) \
  do { \
    if (solver->proof) \
      kissat_delete_clause_from_proof (solver, (CLAUSE)); \
  } while (0)
 
#define DELETE_LITS_FROM_PROOF(SIZE, LITS) \
  do { \
    if (solver->proof) \
      kissat_delete_internal_from_proof (solver, (SIZE), (LITS)); \
  } while (0)
 
#define DELETE_STACK_FROM_PROOF(S) \
  do { \
    if (solver->proof) \
      kissat_delete_internal_from_proof (solver, SIZE_STACK (S), \
                                         BEGIN_STACK (S)); \
  } while (0)
 
#else
 
#define ADD_BINARY_TO_PROOF(...) \
  do { \
  } while (0)
#define ADD_TERNARY_TO_PROOF(...) \
  do { \
  } while (0)
#define ADD_CLAUSE_TO_PROOF(...) \
  do { \
  } while (0)
#define ADD_LITS_TO_PROOF(...) \
  do { \
  } while (0)
#define ADD_EMPTY_TO_PROOF(...) \
  do { \
  } while (0)
#define ADD_STACK_TO_PROOF(...) \
  do { \
  } while (0)
#define ADD_UNIT_TO_PROOF(...) \
  do { \
  } while (0)
 
#define SHRINK_CLAUSE_IN_PROOF(...) \
  do { \
  } while (0)
 
#define DELETE_BINARY_FROM_PROOF(...) \
  do { \
  } while (0)
#define DELETE_TERNARY_FROM_PROOF(...) \
  do { \
  } while (0)
#define DELETE_CLAUSE_FROM_PROOF(...) \
  do { \
  } while (0)
#define DELETE_LITS_FROM_PROOF(...) \
  do { \
  } while (0)
#define DELETE_STACK_FROM_PROOF(...) \
  do { \
  } while (0)
 
#endif
 
ABC_NAMESPACE_HEADER_END
 
#endif