gratgen_splitwl.cpp File Reference

GRATgen main source file. More...

#include <cstdlib>
#include <iostream>
#include <fstream>
#include <sstream>
#include <vector>
#include <algorithm>
#include <cassert>
#include <functional>
#include <limits>
#include <unordered_map>
#include <cstdint>
#include <thread>
#include <atomic>
#include <chrono>
#include <boost/progress.hpp>

Include dependency graph for gratgen_splitwl.cpp:

Classes
struct	pos_t
	A relative position in the clause database. More...
struct	trail_item_t
	An item on the trail. More...
class	lit_map< T >
	Container class to store a mapping from literals to type T. More...
class	ClauseDB
	Stores the clauses and the certificate as an array of cdb_t items. More...
class	item_t
	A certificate item. More...
class	Global_Data
	Global data, which is constant after forward pass. More...
class	Synch_Data
	Global data, which is synchronized between threads, or joined after thread's execution from thread's local data. More...
class	Parser
	Parser that reads cnf and drat files. More...
class	Verifier
	Main functionality for DRAT certificate verification. More...
struct	push_clause_ids
	The functionality of appending clause IDs to a vector. More...
class	VController
	Encapsulates the functionality to control the multi-threaded checker. More...
class	Proof_Writer< binary >

Macros
#define	DBG_STAT(X)
	Only execute argument if statistics (WITH_DBG_STAT) are enabled.
Program configuration
Macros for static program configuration
#define	WITH_DBG_STAT
	Define this to include statistic counters. More...
#define	WITH_PROFILING
	Define this to get gperftools profiling. More...

Enumerations
enum	item_type : cdb_t {   INVALID = 0, UNIT_PROP = 1, DELETION = 2, RUP_LEMMA = 3,   RAT_LEMMA = 4, CONFLICT = 5, RAT_COUNTS = 6, INVALID = 0,   UNIT_PROP = 1, DELETION = 2, RUP_LEMMA = 3, RAT_LEMMA = 4,   CONFLICT = 5, RAT_COUNTS = 6 }
	GRAT item types. More...

Functions
void	print_usage ()
	Print usage information.
void	print_info ()
	Print sizes of data types used internally.
int	main (int argc, char **argv)
	Main function.
Auxiliary global functions
Assorted collection of global helper functions.
void	fail (string msg="")
	Abort checking with optional error message.
template<typename T >
void	set_resize (vector< T > &v, size_t i, T data)
	Set v[i]=data, resizing v as necessary.
template<typename S , typename T >
bool	del_from_list (vector< S > &v, T x)
	Delete one x from (unordered) list. More...
template<typename RT , typename T >
RT	with_timing (string name, T op, chrono::milliseconds *dp=nullptr, ostream &out=clog)
	Measure timing of operation, and print timing message to log. More...
template<typename T >
void	with_timing (string name, T op, chrono::milliseconds *dp=nullptr, ostream &out=clog)
	Measure timing of operation, and print timing message to log. More...
template<typename RT , typename T >
RT	with_timing_ml (string name, T op, chrono::milliseconds *dp=nullptr, ostream &out=clog)
	Measure timing of operation, and print timing message to log, allowing measured operation to print to log. More...
template<typename T >
void	with_timing_ml (string name, T op, chrono::milliseconds *dp=nullptr, ostream &out=clog)
	Measure timing of operation, and print timing message to log, allowing measured operation to print to log. More...
Statistics
These statistics are collected during every run of the program.
chrono::milliseconds	stat_parsing_time (0)
	Time required for parsing formula and DRAT certificate.
chrono::milliseconds	stat_checking_time (0)
	Time required for checking.
chrono::milliseconds	stat_bwd_checking_time (0)
	Part of checking time spent in backward pass.
chrono::milliseconds	stat_writing_time (0)
	Time required to write out the certificate.
chrono::milliseconds	stat_overall_time (0)
	Overall reqired (wall-clock) time.
chrono::milliseconds	stat_overall_vrf_time (0)
	Part of overall time, excluding time for certificate writing.
size_t	stat_itemlist_size (0)
	Size of item-list in bytes.
size_t	stat_pivots_size (0)
	Size of pivot map in bytes.
size_t	stat_db_size (0)
	Size of clause database in bytes.
size_t	stat_rup_lemmas (0)
	Number of RUP lemmas.
size_t	stat_rat_lemmas (0)
	Number of RAT lemmas.

Variables
Run-time configuration
bool	cfg_core_first = true
	Do core-first unit propagation.
bool	cfg_ignore_deletion = false
	Ignore clause deletion items.
bool	cfg_no_grat = false
	Do not produce a GRAT certificate.
bool	cfg_assume_nodup = false
	Assume that clauses contain no duplicate literals. More...
bool	cfg_show_progress_bar = true
	Display progress bar.
bool	cfg_summarize_deletions = true
	Summarize deletions.
size_t	cfg_out_buf_size_threshold = 16*1024
	Threshold for output buffer size.
bool	cfg_premark_formula = false
	Mark all clauses of initial formula, to prefer them in unit propagation.

Variables and Literals
Types and functions for variables and literals. As in the DIMACS format, variables are represented by positive integer numbers. Literals are represented by non-zero integers, negative numbers representing negated variables.
typedef int	cdb_t
	Type of clause database entry.
typedef cdb_t	lit_t
	Type of literals.
size_t	var_of (lit_t l)
	Return variable of literal.

Detailed Description

GRATgen main source file.

Author

Peter Lammich

Macro Definition Documentation

#define WITH_DBG_STAT

Define this to include statistic counters.

Attention

Use for debugging only: This will add properly synchronized statistic counters to some inner loops, and thus significantly slow down the checker!

#define WITH_PROFILING

Define this to get gperftools profiling.

gperftools/profiler.h must be on include path!

Enumeration Type Documentation

enum item_type : cdb_t

GRAT item types.

Enumerator
INVALID	Unused.
UNIT_PROP	Unit propagation item. Contains a zero-terminated list of unit-clause IDs: id* 0
DELETION	Deletion item. Contains a zero-terminated list of clause IDs to be deleted: id* 0
RUP_LEMMA	Lemma with RUP-certificate. Contains the new ID for the lemma, the clause, a list of unit clause IDs, and a conflict clause: id lit* 0 id* 0 id
RAT_LEMMA	Lemma with RAT-certificate. Contains the pivot-literal, the new ID for the lemma, a list of unit-clauses IDs, and a list of candidate proofs: lit id lit* 0 id* 0 (id id* 0 id)* 0 Each candidate proof contains the ID of the candidate lemma, a list of unit clause IDs, and a conflict clause ID.
CONFLICT	Indicates a root conflict. Contains the ID of the conflict clause: id
RAT_COUNTS	Item to store RAT literal counts. Contains a list of pairs of literals and positive numbers: (lit num)* 0
INVALID	Unused.
UNIT_PROP	Unit propagation item. Contains a zero-terminated list of unit-clause IDs: id* 0
DELETION	Deletion item. Contains a zero-terminated list of clause IDs to be deleted: id* 0
RUP_LEMMA	Lemma with RUP-certificate. Contains the new ID for the lemma, the clause, a list of unit clause IDs, and a conflict clause: id lit* 0 id* 0 id
RAT_LEMMA	Lemma with RAT-certificate. Contains the pivot-literal, the new ID for the lemma, a list of unit-clauses IDs, and a list of candidate proofs: lit id lit* 0 id* 0 (id id* 0 id)* 0 Each candidate proof contains the ID of the candidate lemma, a list of unit clause IDs, and a conflict clause ID.
CONFLICT	Indicates a root conflict. Contains the ID of the conflict clause: id
RAT_COUNTS	Item to store RAT literal counts. Contains a list of pairs of literals and positive numbers: (lit num)* 0

Function Documentation

template<typename S , typename T >

bool del_from_list	(	vector< S > &	v,
		T	x
	)

Delete one x from (unordered) list.

Returns true if an x was deleted, false if no x was found.

template<typename RT , typename T >

RT with_timing	(	string	name,
		T	op,
		chrono::milliseconds *	dp = nullptr,
		ostream &	out = clog
	)

Measure timing of operation, and print timing message to log.

Parameters

name	name that is printed as operation name
op	operation, invoked as op()
dp	Pointer to time to be incremented. nullptr if no time to be stored
out	Stream to print message to, clog by default

Returns

return value of op()

template<typename T >

void with_timing	(	string	name,
		T	op,
		chrono::milliseconds *	dp = nullptr,
		ostream &	out = clog
	)

Measure timing of operation, and print timing message to log.

Specialized for op() returning void.

Parameters

name	name that is printed as operation name
op	operation, invoked as op()
dp	Pointer to time to be incremented. nullptr if no time to be stored
out	Stream to print message to, clog by default

template<typename RT , typename T >

RT with_timing_ml	(	string	name,
		T	op,
		chrono::milliseconds *	dp = nullptr,
		ostream &	out = clog
	)

Measure timing of operation, and print timing message to log, allowing measured operation to print to log.

Parameters

name	name that is printed as operation name
op	operation, invoked as op()
dp	Pointer to time to be incremented. nullptr if no time to be stored
out	Stream to print message to, clog by default

Returns

return value of op()

template<typename T >

void with_timing_ml	(	string	name,
		T	op,
		chrono::milliseconds *	dp = nullptr,
		ostream &	out = clog
	)

Measure timing of operation, and print timing message to log, allowing measured operation to print to log.

Specialized for op() returning void.

Parameters

name	name that is printed as operation name
op	operation, invoked as op()
dp	Pointer to time to be incremented. nullptr if no time to be stored
out	Stream to print message to, clog by default

Variable Documentation

bool cfg_assume_nodup = false

Assume that clauses contain no duplicate literals.

Attention

You're on your own if they do nevertheless!