CBMC
Public Member Functions | Public Attributes | List of all members
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: