check.h

Go to the documentation of this file.

#ifndef _check_h_INCLUDED
#define _check_h_INCLUDED
 
#include <stdbool.h>
#include <stdlib.h>
 
#include "global.h"
ABC_NAMESPACE_HEADER_START
 
#ifndef KISSAT_NDEBUG
 
struct kissat;
 
void kissat_check_satisfying_assignment (struct kissat *);
 
typedef struct checker checker;
 
struct clause;
 
void kissat_init_checker (struct kissat *);
void kissat_release_checker (struct kissat *);
 
#ifndef KISSAT_QUIET
void kissat_print_checker_statistics (struct kissat *, bool verbose);
#endif
 
void kissat_add_unchecked_external (struct kissat *, size_t, const int *);
 
void kissat_check_and_add_binary (struct kissat *, unsigned, unsigned);
void kissat_check_and_add_clause (struct kissat *, struct clause *c);
void kissat_check_and_add_empty (struct kissat *);
void kissat_check_and_add_internal (struct kissat *, size_t,
                                    const unsigned *);
void kissat_check_and_add_unit (struct kissat *, unsigned);
 
void kissat_check_shrink_clause (struct kissat *, struct clause *,
                                 unsigned remove, unsigned keep);
 
void kissat_remove_checker_binary (struct kissat *, unsigned, unsigned);
void kissat_remove_checker_clause (struct kissat *, struct clause *c);
void kissat_remove_checker_external (struct kissat *, size_t, const int *);
 
void kissat_remove_checker_internal (struct kissat *, size_t,
                                     const unsigned *);
 
#define ADD_UNCHECKED_EXTERNAL(SIZE, LITS) \
  do { \
    if (GET_OPTION (check) > 1) \
      kissat_add_unchecked_external (solver, (SIZE), (LITS)); \
  } while (0)
 
#define CHECK_AND_ADD_BINARY(A, B) \
  do { \
    if (GET_OPTION (check) > 1) \
      kissat_check_and_add_binary (solver, (A), (B)); \
  } while (0)
 
#define CHECK_AND_ADD_TERNARY(A, B, C) \
  do { \
    if (GET_OPTION (check) > 1) { \
      unsigned CLAUSE[3] = {(A), (B), (C)}; \
      kissat_check_and_add_internal (solver, 3, CLAUSE); \
    } \
  } while (0)
 
#define CHECK_AND_ADD_CLAUSE(CLAUSE) \
  do { \
    if (GET_OPTION (check) > 1) \
      kissat_check_and_add_clause (solver, (CLAUSE)); \
  } while (0)
 
#define CHECK_AND_ADD_EMPTY() \
  do { \
    if (GET_OPTION (check) > 1) \
      kissat_check_and_add_empty (solver); \
  } while (0)
 
#define CHECK_AND_ADD_LITS(SIZE, LITS) \
  do { \
    if (GET_OPTION (check) > 1) \
      kissat_check_and_add_internal (solver, (SIZE), (LITS)); \
  } while (0)
 
#define CHECK_AND_ADD_STACK(S) \
  CHECK_AND_ADD_LITS (SIZE_STACK (S), BEGIN_STACK (S))
 
#define CHECK_AND_ADD_UNIT(A) \
  do { \
    if (GET_OPTION (check) > 1) \
      kissat_check_and_add_unit (solver, (A)); \
  } while (0)
 
#define CHECK_SHRINK_CLAUSE(C, REMOVE, KEEP) \
  do { \
    if (GET_OPTION (check) > 1) \
      kissat_check_shrink_clause (solver, (C), (REMOVE), (KEEP)); \
  } while (0)
 
#define REMOVE_CHECKER_BINARY(A, B) \
  do { \
    if (GET_OPTION (check) > 1) \
      kissat_remove_checker_binary (solver, (A), (B)); \
  } while (0)
 
#define REMOVE_CHECKER_TERNARY(A, B, C) \
  do { \
    if (GET_OPTION (check) > 1) { \
      unsigned CLAUSE[3] = {(A), (B), (C)}; \
      kissat_remove_checker_internal (solver, 3, CLAUSE); \
    } \
  } while (0)
 
#define REMOVE_CHECKER_CLAUSE(CLAUSE) \
  do { \
    if (GET_OPTION (check) > 1) \
      kissat_remove_checker_clause (solver, (CLAUSE)); \
  } while (0)
 
#define REMOVE_CHECKER_LITS(SIZE, LITS) \
  do { \
    if (GET_OPTION (check) > 1) \
      kissat_remove_checker_internal (solver, (SIZE), (LITS)); \
  } while (0)
 
#define REMOVE_CHECKER_STACK(S) \
  do { \
    if (GET_OPTION (check) > 1) \
      kissat_remove_checker_internal (solver, SIZE_STACK (S), \
                                      BEGIN_STACK (S)); \
  } while (0)
 
#else
 
#define ADD_UNCHECKED_EXTERNAL(...) \
  do { \
  } while (0)
#define CHECK_AND_ADD_BINARY(...) \
  do { \
  } while (0)
#define CHECK_AND_ADD_TERNARY(...) \
  do { \
  } while (0)
#define CHECK_AND_ADD_CLAUSE(...) \
  do { \
  } while (0)
#define CHECK_AND_ADD_EMPTY(...) \
  do { \
  } while (0)
#define CHECK_AND_ADD_LITS(...) \
  do { \
  } while (0)
#define CHECK_AND_ADD_STACK(...) \
  do { \
  } while (0)
#define CHECK_AND_ADD_UNIT(...) \
  do { \
  } while (0)
#define CHECK_SHRINK_CLAUSE(...) \
  do { \
  } while (0)
#define REMOVE_CHECKER_BINARY(...) \
  do { \
  } while (0)
#define REMOVE_CHECKER_TERNARY(...) \
  do { \
  } while (0)
#define REMOVE_CHECKER_CLAUSE(...) \
  do { \
  } while (0)
#define REMOVE_CHECKER_LITS(...) \
  do { \
  } while (0)
#define REMOVE_CHECKER_STACK(...) \
  do { \
  } while (0)
 
#endif
 
ABC_NAMESPACE_HEADER_END
 
#endif