luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #380 from MyskYko/kissat 

support debug mode
This commit is contained in:
alanminko 2025-03-07 23:17:44 +07:00 committed by GitHub
parent cab003b277 8fb9fc5d0f
commit 383c16b690
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
7 changed files with 64 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/sat/kissat/VERSION Normal file
View File

@ -0,0 +1 @@
4.0.2

45
src/sat/kissat/check.c
View File

@ -16,6 +16,8 @@
#undef LOGPREFIX
#define LOGPREFIX "CHECK"
ABC_NAMESPACE_IMPL_START
void kissat_check_satisfying_assignment (kissat *solver) {
LOG ("checking satisfying assignment");
const int *const begin = BEGIN_STACK (solver->original);
@ -51,16 +53,20 @@ void kissat_check_satisfying_assignment (kissat *solver) {
LOG ("assignment satisfies all %zu original clauses", count);
}
ABC_NAMESPACE_IMPL_END
#include "allocate.h"
#include "inline.h"
#include "sort.h"
ABC_NAMESPACE_IMPL_START
typedef struct hash hash;
typedef struct bucket bucket;
// clang-format off
typedef STACK (bucket*) buckets;
typedef STACK (bucket*) buckets_;
// clang-format on
@ -82,7 +88,7 @@ struct checker {
bucket **table;
buckets *watches;
buckets_ *watches;
bool *marks;
bool *large;
bool *used;
@ -151,7 +157,7 @@ static void init_nonces (kissat *solver, checker *checker) {
void kissat_init_checker (kissat *solver) {
LOG ("initializing internal proof checker");
checker *checker = kissat_calloc (solver, 1, sizeof (struct checker));
checker *checker = (struct checker*)kissat_calloc (solver, 1, sizeof (struct checker));
solver->checker = checker;
init_nonces (solver, checker);
}
@ -172,7 +178,7 @@ static void release_watches (kissat *solver, checker *checker) {
for (unsigned i = 0; i < lits; i++)
RELEASE_STACK (checker->watches[i]);
kissat_dealloc (solver, checker->watches, 2 * checker->size,
sizeof (buckets));
sizeof (buckets_));
}
void kissat_release_checker (kissat *solver) {
@ -191,8 +197,12 @@ void kissat_release_checker (kissat *solver) {
#ifndef KISSAT_QUIET
ABC_NAMESPACE_IMPL_END
#include <inttypes.h>
ABC_NAMESPACE_IMPL_START
#define PERCENT_ADDED(NAME) kissat_percent (checker->NAME, checker->added)
#define PERCENT_CHECKED(NAME) \
kissat_percent (checker->NAME, checker->checked)
@ -249,7 +259,7 @@ static void resize_hash (kissat *solver, checker *checker) {
const unsigned old_hashed = checker->hashed;
KISSAT_assert (old_hashed < MAX_SIZE);
const unsigned new_hashed = old_hashed ? 2 * old_hashed : 1;
bucket **table = kissat_calloc (solver, new_hashed, sizeof (bucket *));
bucket **table = (bucket**) kissat_calloc (solver, new_hashed, sizeof (bucket *));
bucket **old_table = checker->table;
for (unsigned i = 0; i < old_hashed; i++) {
for (bucket *bucket = old_table[i], *next; bucket; bucket = next) {
@ -303,7 +313,7 @@ static void checker_assign (kissat *solver, checker *checker, unsigned lit,
PUSH_STACK (checker->trail, lit);
}
static buckets *checker_watches (checker *checker, unsigned lit) {
static buckets_ *checker_watches (checker *checker, unsigned lit) {
KISSAT_assert (VALID_CHECKER_LIT (lit));
return checker->watches + lit;
}
@ -311,14 +321,14 @@ static buckets *checker_watches (checker *checker, unsigned lit) {
static void watch_checker_literal (kissat *solver, checker *checker,
bucket *bucket, unsigned lit) {
LOGLINE3 ("checker watches %u in", lit);
buckets *buckets = checker_watches (checker, lit);
buckets_ *buckets = checker_watches (checker, lit);
PUSH_STACK (*buckets, bucket);
}
static void unwatch_checker_literal (kissat *solver, checker *checker,
bucket *bucket, unsigned lit) {
LOGLINE3 ("checker unwatches %u in", lit);
buckets *buckets = checker_watches (checker, lit);
buckets_ *buckets = checker_watches (checker, lit);
REMOVE_STACK (struct bucket *, *buckets, bucket);
#ifndef LOGGING
(void) solver;
@ -535,15 +545,15 @@ static void resize_checker (kissat *solver, checker *checker,
LOG3 ("resizing checker form %u to %u", size, new_size);
const unsigned size2 = 2 * size;
const unsigned new_size2 = 2 * new_size;
checker->marks = kissat_realloc (solver, checker->marks, size2,
checker->marks = (bool*)kissat_realloc (solver, checker->marks, size2,
new_size2 * sizeof (bool));
checker->used = kissat_realloc (solver, checker->used, size2,
checker->used = (bool*)kissat_realloc (solver, checker->used, size2,
new_size2 * sizeof (bool));
checker->large = kissat_realloc (solver, checker->large, size2,
checker->large = (bool*)kissat_realloc (solver, checker->large, size2,
new_size2 * sizeof (bool));
checker->values =
kissat_realloc (solver, checker->values, size2, new_size2);
checker->watches = kissat_realloc (
(signed char *)kissat_realloc (solver, checker->values, size2, new_size2);
checker->watches = (buckets_*)kissat_realloc (
solver, checker->watches, size2 * sizeof *checker->watches,
new_size2 * sizeof *checker->watches);
checker->size = new_size;
@ -685,7 +695,7 @@ static bool checker_propagate (kissat *solver, checker *checker) {
KISSAT_assert (values[lit] > 0);
KISSAT_assert (values[not_lit] < 0);
propagated++;
buckets *buckets = checker_watches (checker, not_lit);
buckets_ *buckets = checker_watches (checker, not_lit);
bucket **begin_of_lines = BEGIN_STACK (*buckets), **q = begin_of_lines;
bucket *const *end_of_lines = END_STACK (*buckets), *const *p = q;
while (p != end_of_lines) {
@ -793,7 +803,7 @@ static bool checker_blocked_literal (kissat *solver, checker *checker,
const unsigned not_lit = lit ^ 1;
if (checker->large[not_lit])
return false;
buckets *buckets = checker_watches (checker, not_lit);
buckets_ *buckets = checker_watches (checker, not_lit);
bucket *const *const begin_of_lines = BEGIN_STACK (*buckets);
bucket *const *const end_of_lines = END_STACK (*buckets);
bucket *const *p = begin_of_lines;
@ -1030,6 +1040,11 @@ void dump_checker (kissat *solver) {
dump_line (bucket);
}
ABC_NAMESPACE_IMPL_END
#else
ABC_NAMESPACE_IMPL_START
int kissat_check_dummy_to_avoid_warning;
ABC_NAMESPACE_IMPL_END
#endif

2
src/sat/kissat/definition.c
View File

@ -57,7 +57,7 @@ static void traverse_one_sided_core_lemma (void *state, bool learned,
const unsigned *lits) {
if (!learned)
return;
lemma_extractor *extractor = state;
lemma_extractor *extractor = (lemma_extractor*)state;
kissat *solver = extractor->solver;
const unsigned unit = extractor->unit;
unsigneds *added = &solver->added;

12
src/sat/kissat/dump.c
View File

@ -6,6 +6,8 @@
#include <inttypes.h>
ABC_NAMESPACE_IMPL_START
static void dump_literal (kissat *solver, unsigned ilit) {
const int elit = kissat_export_literal (solver, ilit);
printf ("%u(%d)", ilit, elit);
@ -279,17 +281,21 @@ int kissat_dump (kissat *solver) {
else
dump_queue (solver);
dump_values (solver);
printf ("binary = %" PRIu64 "\n", solver->statistics.clauses_binary);
printf ("binary = %" PRIu64 "\n", solver->statistics_.clauses_binary);
printf ("irredundant = %" PRIu64 "\n",
solver->statistics.clauses_irredundant);
solver->statistics_.clauses_irredundant);
printf ("redundant = %" PRIu64 "\n",
solver->statistics.clauses_redundant);
solver->statistics_.clauses_redundant);
dump_binaries (solver);
dump_clauses (solver);
dump_extend (solver);
return 0;
}
ABC_NAMESPACE_IMPL_END
#else
ABC_NAMESPACE_IMPL_START
int kissat_dump_dummy_to_avoid_warning;
ABC_NAMESPACE_IMPL_END
#endif

8
src/sat/kissat/global.h
View File

@ -1,13 +1,19 @@
#ifndef ABC_SAT_KISSAT_GLOBAL_H_
#define ABC_SAT_KISSAT_GLOBAL_H_
#define KISSAT_COMPACT
// comment out next line to enable kissat debug mode
#define KISSAT_NDEBUG
#define KISSAT_COMPACT
#define KISSAT_NOPTIONS
#define KISSAT_NPROOFS
#define KISSAT_QUIET
#ifdef KISSAT_NDEBUG
#define KISSAT_assert(ignore) ((void)0)
#else
#define KISSAT_assert(cond) assert(cond)
#endif
#include "misc/util/abc_global.h"

2
src/sat/kissat/kimits.c
View File

@ -99,7 +99,7 @@ static void init_enabled (kissat *solver) {
} while (0)
void kissat_init_limits (kissat *solver) {
KISSAT_assert (solver->statistics.searches == 1);
KISSAT_assert (solver->statistics_.searches == 1);
init_enabled (solver);

16
src/sat/kissat/statistics.c
View File

@ -15,6 +15,8 @@
#include <stdio.h>
#include <string.h>
ABC_NAMESPACE_IMPL_START
void kissat_print_glue_usage (kissat *solver) {
const int64_t stable = solver->statistics.clauses_used_stable;
const int64_t focused = solver->statistics.clauses_used_focused;
@ -346,8 +348,16 @@ kissat_statistics_print (kissat * solver, bool verbose)
// clang-format on
ABC_NAMESPACE_IMPL_END
#elif defined(KISSAT_NDEBUG)
ABC_NAMESPACE_IMPL_START
int kissat_statistics_dummy_to_avoid_warning;
ABC_NAMESPACE_IMPL_END
#endif
/*------------------------------------------------------------------------*/
@ -356,6 +366,8 @@ int kissat_statistics_dummy_to_avoid_warning;
#include "inlinevector.h"
ABC_NAMESPACE_IMPL_START
void kissat_check_statistics (kissat *solver) {
if (solver->inconsistent)
return;
@ -402,7 +414,7 @@ void kissat_check_statistics (kissat *solver) {
KISSAT_assert (!(binary & 1));
binary /= 2;
statistics *statistics = &solver->statistics;
statistics *statistics = &solver->statistics_;
KISSAT_assert (statistics->clauses_binary == binary);
KISSAT_assert (statistics->clauses_redundant == redundant);
KISSAT_assert (statistics->clauses_irredundant == irredundant);
@ -413,4 +425,6 @@ void kissat_check_statistics (kissat *solver) {
#endif
}
ABC_NAMESPACE_IMPL_END
#endif