Inheritance diagram for clause_hardness_collectort:

Public Member Functions
virtual void	register_clause (const bvt &bv, const bvt &cnf, const size_t cnf_clause_index, bool register_cnf)=0
	Called e.g. More...

virtual	~clause_hardness_collectort ()

Detailed Description

Definition at line 23 of file hardness_collector.h.

Constructor & Destructor Documentation

virtual clause_hardness_collectort::~clause_hardness_collectort ( )

inlinevirtual

Definition at line 39 of file hardness_collector.h.

virtual void clause_hardness_collectort::register_clause	(	const bvt &	bv,
		const bvt &	cnf,
		const size_t	cnf_clause_index,
		bool	register_cnf
	)

pure virtual

Called e.g.

from the satcheck_minisat2::lcnf, this function adds the complexity statistics from the last SAT query to the current_ssa_key.

Parameters

bv	the clause (vector of literals)
cnf	processed clause
cnf_clause_index	index of clause in dimacs output
register_cnf	negation of boolean variable tracking if the clause can be eliminated

The documentation for this class was generated from the following file: