162 lines
3.3 KiB
C
162 lines
3.3 KiB
C
#ifndef NPROOFS
|
|
|
|
#include "test.h"
|
|
#include "testcnfs.h"
|
|
|
|
#include "../src/file.h"
|
|
|
|
#ifdef _POSIX_C_SOURCE
|
|
|
|
#define MAX_COMPRESSED 10
|
|
|
|
static const char *compressions[MAX_COMPRESSED];
|
|
static unsigned size_compressions;
|
|
|
|
#define NEW_COMPRESSION(NAME,SUFFIX) \
|
|
do { \
|
|
if (!tissat_found_ ## NAME) \
|
|
break; \
|
|
assert (size_compressions < MAX_COMPRESSED); \
|
|
compressions[size_compressions++] = SUFFIX; \
|
|
} while (0)
|
|
|
|
static void
|
|
init_compression (void)
|
|
{
|
|
// *INDENT-OFF*
|
|
NEW_COMPRESSION (bzip2, ".bz2");
|
|
NEW_COMPRESSION (gzip, ".gz");
|
|
// NEW_COMPRESSION (lzma, ".lzma");
|
|
NEW_COMPRESSION (7z, ".7z");
|
|
NEW_COMPRESSION (xz, ".xz");
|
|
// *INDENT-ON*
|
|
}
|
|
|
|
static unsigned compressed;
|
|
|
|
#endif
|
|
|
|
static unsigned scheduled;
|
|
|
|
static void
|
|
schedule_prove_job_with_option (int expected,
|
|
const char *opt,
|
|
const char *cnf, const char *name)
|
|
{
|
|
char cmd[256];
|
|
if (!kissat_file_readable (cnf))
|
|
{
|
|
tissat_warning ("Skipping unreadable '%s'", cnf);
|
|
return;
|
|
}
|
|
|
|
bool drat_trim;
|
|
bool drabt;
|
|
|
|
if (!strcmp (name, "false"))
|
|
{
|
|
drabt = tissat_found_drabt;
|
|
drat_trim = false;
|
|
}
|
|
else if (tissat_big)
|
|
{
|
|
drabt = tissat_found_drabt;
|
|
drat_trim = tissat_found_drat_trim;
|
|
}
|
|
else if (tissat_found_drabt && !tissat_found_drat_trim)
|
|
{
|
|
drabt = true;
|
|
drat_trim = false;
|
|
}
|
|
else if (!tissat_found_drabt && tissat_found_drat_trim)
|
|
{
|
|
drabt = false;
|
|
drat_trim = true;
|
|
}
|
|
else
|
|
{
|
|
assert (tissat_found_drabt);
|
|
assert (tissat_found_drat_trim);
|
|
drabt = scheduled & 1;
|
|
drat_trim = !drabt;
|
|
}
|
|
|
|
const char *suffix = "";
|
|
|
|
#ifdef _POSIX_C_SOURCE
|
|
bool compress;
|
|
if (!size_compressions)
|
|
compress = false;
|
|
else if (drat_trim)
|
|
compress = false;
|
|
else if (drabt)
|
|
compress = (scheduled & 2);
|
|
else
|
|
compress = true;
|
|
|
|
if (compress)
|
|
suffix = compressions[compressed++ % size_compressions];
|
|
#endif
|
|
char proof[96];
|
|
sprintf (proof, "%s.proof%u%s", name, scheduled, suffix);
|
|
|
|
const char *binary = (scheduled % 5) ? "" : "--no-binary ";
|
|
sprintf (cmd, "%s%s%s %s", opt, binary, cnf, proof);
|
|
tissat_job *job = tissat_schedule_application (expected, cmd);
|
|
scheduled++;
|
|
|
|
if (drabt)
|
|
{
|
|
if (expected == 10)
|
|
sprintf (cmd, "drabt -S %s %s", cnf, proof);
|
|
else
|
|
sprintf (cmd, "drabt %s %s", cnf, proof);
|
|
assert (strlen (cmd) < sizeof cmd);
|
|
|
|
tissat_schedule_command (0, cmd, job);
|
|
}
|
|
|
|
if (drat_trim)
|
|
{
|
|
if (expected == 10)
|
|
sprintf (cmd, "drat-trim %s %s -S", cnf, proof);
|
|
else
|
|
sprintf (cmd, "drat-trim %s %s", cnf, proof);
|
|
assert (strlen (cmd) < sizeof cmd);
|
|
|
|
tissat_schedule_command (0, cmd, job);
|
|
}
|
|
}
|
|
|
|
static void
|
|
schedule_prove_job (int expected, const char *cnf, const char *name)
|
|
{
|
|
if (tissat_big)
|
|
{
|
|
for (all_tissat_options (opt))
|
|
schedule_prove_job_with_option (expected, opt, cnf, name);
|
|
}
|
|
else
|
|
{
|
|
const char *opt = tissat_next_option (scheduled);
|
|
schedule_prove_job_with_option (expected, opt, cnf, name);
|
|
}
|
|
}
|
|
|
|
void
|
|
tissat_schedule_prove (void)
|
|
{
|
|
#ifdef _POSIX_C_SOURCE
|
|
init_compression ();
|
|
#endif
|
|
#define CNF(EXPECTED,NAME,BIG) \
|
|
if (!BIG || tissat_big) \
|
|
schedule_prove_job (EXPECTED, "../test/cnf/" #NAME ".cnf", #NAME);
|
|
CNFS
|
|
#undef CNF
|
|
}
|
|
|
|
#else
|
|
int tissat_prove_do_avoid_warning;
|
|
#endif
|