minisat_prooft Class Reference

Inheritance diagram for minisat_prooft:

Collaboration diagram for minisat_prooft:

Public Member Functions
virtual void	root (const vec< Lit > &c)
virtual void	chain (const vec< ClauseId > &cs, const vec< Var > &xs)
virtual void	deleted (ClauseId c)
virtual void	done ()
virtual	~minisat_prooft ()

Public Attributes
simple_prooft	resolution_proof

Detailed Description

Definition at line 32 of file satcheck_minisat.cpp.

Constructor & Destructor Documentation

~minisat_prooft()

virtual minisat_prooft::~minisat_prooft ( )

inlinevirtual

Definition at line 55 of file satcheck_minisat.cpp.

Member Function Documentation

chain()

void minisat_prooft::chain ( const vec< ClauseId > &  cs, const vec< Var > &  xs  )

virtual

Definition at line 60 of file satcheck_minisat.cpp.

deleted()

virtual void minisat_prooft::deleted ( ClauseId  c )

inlinevirtual

Definition at line 53 of file satcheck_minisat.cpp.

done()

virtual void minisat_prooft::done ( )

inlinevirtual

Definition at line 54 of file satcheck_minisat.cpp.

root()

virtual void minisat_prooft::root ( const vec< Lit > &  c )

inlinevirtual

Definition at line 35 of file satcheck_minisat.cpp.

Member Data Documentation

resolution_proof

simple_prooft minisat_prooft::resolution_proof

Definition at line 57 of file satcheck_minisat.cpp.

---

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

• /home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_minisat.cpp