DECLARATIONS ///. More...

Collaboration diagram for Inter_Check_t_:

[legend]

Public Attributes
int	nFramesK

int	nVars

Aig_Man_t *	pFrames

Cnf_Dat_t *	pCnf

sat_solver *	pSat

Vec_Int_t *	vOrLits

Vec_Int_t *	vAndLits

Vec_Int_t *	vAssLits

Detailed Description

DECLARATIONS ///.

CFile****************************************************************

FileName [intCheck.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Interpolation engine.]

Synopsis [Procedures to perform incremental inductive check.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 24, 2008.]

Revision [

Id: intCheck.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 31 of file intCheck.c.

Member Data Documentation

◆ nFramesK

int Inter_Check_t_::nFramesK

Definition at line 33 of file intCheck.c.

◆ nVars

int Inter_Check_t_::nVars

Definition at line 34 of file intCheck.c.

◆ pCnf

Cnf_Dat_t* Inter_Check_t_::pCnf

Definition at line 36 of file intCheck.c.

◆ pFrames

Aig_Man_t* Inter_Check_t_::pFrames

Definition at line 35 of file intCheck.c.

◆ pSat

sat_solver* Inter_Check_t_::pSat

Definition at line 37 of file intCheck.c.

◆ vAndLits

Vec_Int_t* Inter_Check_t_::vAndLits

Definition at line 39 of file intCheck.c.

◆ vAssLits

Vec_Int_t* Inter_Check_t_::vAssLits

Definition at line 40 of file intCheck.c.

◆ vOrLits

Vec_Int_t* Inter_Check_t_::vOrLits

Definition at line 38 of file intCheck.c.

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

src/proof/int/intCheck.c

Public Attributes