#include "congruence.h"
#include "dense.h"
#include "fifo.h"
#include "inline.h"
#include "inlinevector.h"
#include "internal.h"
#include "logging.h"
#include "print.h"
#include "proprobe.h"
#include "rank.h"
#include "reference.h"
#include "report.h"
#include "sort.h"
#include "terminate.h"
#include "trail.h"
#include "utilities.h"
#include <stddef.h>
#include <stdint.h>
#include <string.h>

Include dependency graph for congruence.c:

Classes
struct	gate

struct	hash_ref

struct	closure

struct	offsetsize

struct	refsize

Macros
#define	MERGE_CONDITIONAL_EQUIVALENCES

#define	AND_GATE 0

#define	XOR_GATE 1

#define	ITE_GATE 2

#define	LD_MAX_ARITY 26

#define	MAX_ARITY ((1 << LD_MAX_ARITY) - 1)

#define	REMOVED ((gate *) (~(uintptr_t) 0))

#define	BEGIN_RHS(G)

#define	END_RHS(G)

#define	all_rhs_literals_in_gate(LIT, G)

#define	SIZE_NONCES 16

#define	CLOGANDGATE(G, ...)

#define	CLOGXORGATE(G, ...)

#define	CLOGITEGATE(G, ...)

#define	CLOGREPR(L)

#define	LOGATE(G, ...)

#define	check_lits_sorted(...)

#define	check_and_lits_normalized check_lits_sorted

#define	check_xor_lits_normalized check_lits_sorted

#define	check_ite_lits_normalized check_lits_sorted

#define	LESS_LIT(A, B)

#define	MAX_HASH_TABLE_SIZE ((size_t) 1 << 32)

#define	check_and_gate_implied(...)

#define	check_xor_gate_implied check_and_gate_implied

#define	check_ternary check_and_gate_implied

#define	check_ite_implied check_and_gate_implied

#define	check_ite_gate_implied check_and_gate_implied

#define	add_xor_matching_proof_chain(...)

#define	delete_proof_chain(...)

#define	add_ite_matching_proof_chain(...)

#define	add_ite_turned_and_binary_clauses add_ite_matching_proof_chain

#define	add_xor_shrinking_proof_chain(...)

#define	RANK_OTHER(A)

#define	LESS_OTHER(A, B)

#define	SMALLER_NEGATED_BIN_COUNT(A, B)

#define	RADIDX_SORT_PAIR_LIMIT 32

#define	RANKREFSIZE(REFSIZE)

Typedefs
typedef struct gate	gate

typedef struct gate_hash_table	gate_hash_table

typedef struct closure	closure

typedef struct offsetsize	offsetsize

typedef struct refsize	refsize

Functions
typedef	STACK (gate *)

void	reset_gate_hash_table (closure *closure)

typedef	STACK (refsize)

bool	kissat_congruence (kissat *solver)

Macro Definition Documentation

◆ add_ite_matching_proof_chain

#define add_ite_matching_proof_chain ( ... )

Value:

do { \

} while (0)

Definition at line 1294 of file congruence.c.

#define add_ite_matching_proof_chain(...) \
  do { \
  } while (0)

◆ add_ite_turned_and_binary_clauses

#define add_ite_turned_and_binary_clauses add_ite_matching_proof_chain

Definition at line 1298 of file congruence.c.

◆ add_xor_matching_proof_chain

#define add_xor_matching_proof_chain ( ... )

Value:

do { \

} while (0)

Definition at line 1163 of file congruence.c.

#define add_xor_matching_proof_chain(...) \
  do { \
  } while (0)

◆ add_xor_shrinking_proof_chain

#define add_xor_shrinking_proof_chain ( ... )

Value:

do { \

} while (0)

Definition at line 1682 of file congruence.c.

#define add_xor_shrinking_proof_chain(...) \
  do { \
  } while (0)

◆ all_rhs_literals_in_gate

#define all_rhs_literals_in_gate	(		LIT,
			G )

Value:

  unsigned LIT, \
      *LIT##_PTR = BEGIN_RHS (G), *const LIT##_END = END_RHS (G); \
  LIT##_PTR != LIT##_END && ((LIT = *LIT##_PTR), true); \
  ++LIT##_PTR

Definition at line 66 of file congruence.c.

#define all_rhs_literals_in_gate(LIT, G) \
  unsigned LIT, \
      *LIT##_PTR = BEGIN_RHS (G), *const LIT##_END = END_RHS (G); \
  LIT##_PTR != LIT##_END && ((LIT = *LIT##_PTR), true); \
  ++LIT##_PTR

◆ AND_GATE

#define AND_GATE 0

Definition at line 28 of file congruence.c.

◆ BEGIN_RHS

#define BEGIN_RHS ( G )

Value:

((G)->rhs)

Definition at line 63 of file congruence.c.

◆ check_and_gate_implied

#define check_and_gate_implied ( ... )

Value:

do { \

} while (0)

Definition at line 723 of file congruence.c.

#define check_and_gate_implied(...) \
  do { \
  } while (0)

◆ check_and_lits_normalized

#define check_and_lits_normalized check_lits_sorted

Definition at line 337 of file congruence.c.

◆ check_ite_gate_implied

#define check_ite_gate_implied check_and_gate_implied

Definition at line 730 of file congruence.c.

◆ check_ite_implied

#define check_ite_implied check_and_gate_implied

Definition at line 729 of file congruence.c.

◆ check_ite_lits_normalized

#define check_ite_lits_normalized check_lits_sorted

Definition at line 339 of file congruence.c.

◆ check_lits_sorted

#define check_lits_sorted ( ... )

Value:

do { \

} while (0)

Definition at line 333 of file congruence.c.

#define check_lits_sorted(...) \
  do { \
  } while (0)

◆ check_ternary

#define check_ternary check_and_gate_implied

Definition at line 728 of file congruence.c.

◆ check_xor_gate_implied

#define check_xor_gate_implied check_and_gate_implied

Definition at line 727 of file congruence.c.

◆ check_xor_lits_normalized

#define check_xor_lits_normalized check_lits_sorted

Definition at line 338 of file congruence.c.

◆ CLOGANDGATE

#define CLOGANDGATE	(		G,
			... )

Value:

  do { \
    KISSAT_assert ((G)->tag == AND_GATE); \
    LOGANDGATE ((G)->id, closure->repr, (G)->lhs, (G)->arity, (G)->rhs, \
                __VA_ARGS__); \
  } while (0)

Definition at line 193 of file congruence.c.

#define CLOGANDGATE(G, ...) \
  do { \
    KISSAT_assert ((G)->tag == AND_GATE); \
    LOGANDGATE ((G)->id, closure->repr, (G)->lhs, (G)->arity, (G)->rhs, \
                __VA_ARGS__); \
  } while (0)

◆ CLOGITEGATE

#define CLOGITEGATE	(		G,
			... )

Value:

  do { \
    KISSAT_assert ((G)->tag == ITE_GATE); \
    LOGITEGATE ((G)->id, closure->repr, (G)->lhs, (G)->rhs[0], \
                (G)->rhs[1], (G)->rhs[2], __VA_ARGS__); \
  } while (0)

Definition at line 207 of file congruence.c.

#define CLOGITEGATE(G, ...) \
  do { \
    KISSAT_assert ((G)->tag == ITE_GATE); \
    LOGITEGATE ((G)->id, closure->repr, (G)->lhs, (G)->rhs[0], \
                (G)->rhs[1], (G)->rhs[2], __VA_ARGS__); \
  } while (0)

◆ CLOGREPR

#define CLOGREPR ( L )

Value:

LOGREPR ((L), closure->repr)

Definition at line 214 of file congruence.c.

◆ CLOGXORGATE

#define CLOGXORGATE	(		G,
			... )

Value:

  do { \
    KISSAT_assert ((G)->tag == XOR_GATE); \
    LOGXORGATE ((G)->id, closure->repr, (G)->lhs, (G)->arity, (G)->rhs, \
                __VA_ARGS__); \
  } while (0)

Definition at line 200 of file congruence.c.

#define CLOGXORGATE(G, ...) \
  do { \
    KISSAT_assert ((G)->tag == XOR_GATE); \
    LOGXORGATE ((G)->id, closure->repr, (G)->lhs, (G)->arity, (G)->rhs, \
                __VA_ARGS__); \
  } while (0)

◆ delete_proof_chain

#define delete_proof_chain ( ... )

Value:

do { \

} while (0)

Definition at line 1167 of file congruence.c.

#define delete_proof_chain(...) \
  do { \
  } while (0)

◆ END_RHS

#define END_RHS ( G )

Value:

(BEGIN_RHS (G) + (G)->arity)

Definition at line 64 of file congruence.c.

◆ ITE_GATE

#define ITE_GATE 2

Definition at line 30 of file congruence.c.

◆ LD_MAX_ARITY

#define LD_MAX_ARITY 26

Definition at line 32 of file congruence.c.

◆ LESS_LIT

#define LESS_LIT	(		A,
			B )

Value:

((A) < (B))

Definition at line 343 of file congruence.c.

◆ LESS_OTHER

#define LESS_OTHER	(		A,
			B )

Value:

(RANK_OTHER (A) < RANK_OTHER (B))

RANK_OTHER

#define RANK_OTHER(A)

Definition congruence.c:2189

Definition at line 2190 of file congruence.c.

◆ LOGATE

#define LOGATE	(		G,
			... )

Value:

  do { \
    if ((G)->tag == AND_GATE) \
      CLOGANDGATE (G, __VA_ARGS__); \
    else if ((G)->tag == XOR_GATE) \
      CLOGXORGATE (G, __VA_ARGS__); \
    else { \
      KISSAT_assert ((G)->tag == ITE_GATE); \
      CLOGITEGATE (G, __VA_ARGS__); \
    } \
  } while (0)

Definition at line 216 of file congruence.c.

#define LOGATE(G, ...) \
  do { \
    if ((G)->tag == AND_GATE) \
      CLOGANDGATE (G, __VA_ARGS__); \
    else if ((G)->tag == XOR_GATE) \
      CLOGXORGATE (G, __VA_ARGS__); \
    else { \
      KISSAT_assert ((G)->tag == ITE_GATE); \
      CLOGITEGATE (G, __VA_ARGS__); \
    } \
  } while (0)

◆ MAX_ARITY

#define MAX_ARITY ((1 << LD_MAX_ARITY) - 1)

Definition at line 33 of file congruence.c.

◆ MAX_HASH_TABLE_SIZE

#define MAX_HASH_TABLE_SIZE ((size_t) 1 << 32)

Definition at line 395 of file congruence.c.

◆ MERGE_CONDITIONAL_EQUIVALENCES

#define MERGE_CONDITIONAL_EQUIVALENCES

Definition at line 26 of file congruence.c.

◆ RADIDX_SORT_PAIR_LIMIT

#define RADIDX_SORT_PAIR_LIMIT 32

Definition at line 3440 of file congruence.c.

◆ RANK_OTHER

#define RANK_OTHER ( A )

Value:

((A).lits[1])

Definition at line 2189 of file congruence.c.

◆ RANKREFSIZE

#define RANKREFSIZE ( REFSIZE )

Value:

((REFSIZE).size)

◆ REMOVED

#define REMOVED ((gate *) (~(uintptr_t) 0))

Definition at line 61 of file congruence.c.

◆ SIZE_NONCES

#define SIZE_NONCES 16

Definition at line 107 of file congruence.c.

◆ SMALLER_NEGATED_BIN_COUNT

#define SMALLER_NEGATED_BIN_COUNT	(		A,
			B )

Value:

smaller_negated_bin_count (negbincount, A, B)

Definition at line 2472 of file congruence.c.

2472#define SMALLER_NEGATED_BIN_COUNT(A, B) \

2473 smaller_negated_bin_count (negbincount, A, B)

◆ XOR_GATE

#define XOR_GATE 1

Definition at line 29 of file congruence.c.

Typedef Documentation

◆ closure

typedef struct closure closure

Definition at line 145 of file congruence.c.

◆ gate

typedef struct gate gate

Definition at line 50 of file congruence.c.

◆ gate_hash_table

typedef struct gate_hash_table gate_hash_table

Definition at line 59 of file congruence.c.

◆ offsetsize

typedef struct offsetsize offsetsize

Definition at line 2187 of file congruence.c.

◆ refsize

typedef struct refsize refsize

Definition at line 4449 of file congruence.c.

Function Documentation

◆ kissat_congruence()

bool kissat_congruence ( kissat * solver )

Definition at line 4591 of file congruence.c.

                                        {
  if (solver->inconsistent)
    return false;
  kissat_check_statistics (solver);
  KISSAT_assert (!solver->level);
  KISSAT_assert (solver->probing);
  KISSAT_assert (solver->watching);
  if (!GET_OPTION (congruence))
    return false;
  if (!GET_OPTION (congruenceands) && !GET_OPTION (congruenceites) &&
      !GET_OPTION (congruencexors))
    return false;
  if (GET_OPTION (congruenceonce) && solver->statistics_.closures)
    return false;
  if (TERMINATED (congruence_terminated_8))
    return false;
  if (DELAYING (congruence))
    return false;
  START (congruence);
  INC (closures);
  closure closure;
  init_closure (solver, &closure);
  extract_gates (&closure);
  bool reset = false;
  if (!solver->inconsistent && !TERMINATED (congruence_terminated_9)) {
    find_units (&closure);
    if (!solver->inconsistent && !TERMINATED (congruence_terminated_10)) {
      find_equivalences (&closure);
      if (!solver->inconsistent && !TERMINATED (congruence_terminated_11)) {
        size_t propagated = propagate_units_and_equivalences (&closure);
        if (!solver->inconsistent && propagated &&
            !TERMINATED (congruence_terminated_12)) {
          forward_subsume_matching_clauses (&closure);
          reset = true;
        }
      }
    }
  }
  if (!reset)
    reset_closure (&closure);
  unsigned equivalent = reset_repr (&closure);
  kissat_phase (solver, "congruence", GET (closures),
                "merged %u equivalent variables %.2f%%", equivalent,
                kissat_percent (equivalent, solver->active));
  KISSAT_assert (solver->active >= equivalent);
#ifndef KISSAT_QUIET
  solver->active -= equivalent;
  REPORT (!equivalent, 'c');
  if (!solver->inconsistent)
    solver->active += equivalent;
#endif
  if (kissat_average (equivalent, solver->active) < 0.001)
    BUMP_DELAY (congruence);
  else
    REDUCE_DELAY (congruence);
  STOP (congruence);
  kissat_check_statistics (solver);
  return equivalent;
}

◆ reset_gate_hash_table()

void reset_gate_hash_table ( closure * closure )

Definition at line 236 of file congruence.c.

                                              {
  kissat *const solver = closure->solver;
  gate **table = closure->hash.table;
  for (size_t pos = 0; pos != closure->hash.size; pos++) {
    gate *g = table[pos];
    if (g && g != REMOVED && !g->garbage)
      delete_gate (closure, g);
  }
  DEALLOC (table, closure->hash.size);
}

◆ STACK() [1/2]

typedef STACK ( gate * )

Definition at line 51 of file congruence.c.

                       {
  gate **table;
  size_t size;
  size_t entries;
};

◆ STACK() [2/2]

typedef STACK ( refsize )

Definition at line 4450 of file congruence.c.

                                                                  {
  RADIX_STACK (refsize, unsigned, *candidates, RANKREFSIZE);
}

Classes

Macros

Typedefs

Functions

Macro Definition Documentation

◆ add_ite_matching_proof_chain

◆ add_ite_turned_and_binary_clauses

◆ add_xor_matching_proof_chain

◆ add_xor_shrinking_proof_chain

◆ all_rhs_literals_in_gate

◆ AND_GATE

◆ BEGIN_RHS

◆ check_and_gate_implied

◆ check_and_lits_normalized

◆ check_ite_gate_implied

◆ check_ite_implied

◆ check_ite_lits_normalized

◆ check_lits_sorted

◆ check_ternary

◆ check_xor_gate_implied

◆ check_xor_lits_normalized

◆ CLOGANDGATE

◆ CLOGITEGATE

◆ CLOGREPR

◆ CLOGXORGATE

◆ delete_proof_chain

◆ END_RHS

◆ ITE_GATE

◆ LD_MAX_ARITY

◆ LESS_LIT

◆ LESS_OTHER

◆ LOGATE

◆ MAX_ARITY

◆ MAX_HASH_TABLE_SIZE

◆ MERGE_CONDITIONAL_EQUIVALENCES

◆ RADIDX_SORT_PAIR_LIMIT

◆ RANK_OTHER

◆ RANKREFSIZE

◆ REMOVED

◆ SIZE_NONCES

◆ SMALLER_NEGATED_BIN_COUNT

◆ XOR_GATE

Typedef Documentation

◆ closure

◆ gate

◆ gate_hash_table

◆ offsetsize

◆ refsize

Function Documentation

◆ kissat_congruence()

◆ reset_gate_hash_table()

◆ STACK() [1/2]

◆ STACK() [2/2]