abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
satProof2.h File Reference
#include "misc/vec/vec.h"

Go to the source code of this file.

Data Structures

struct  Prf_Man_t_
 

Typedefs

typedef
typedefABC_NAMESPACE_HEADER_START
struct Prf_Man_t_ 
Prf_Man_t
 INCLUDES ///. More...
 

Functions

static int Prf_BitWordNum (int nWidth)
 GLOBAL VARIABLES ///. More...
 
static int Prf_ManSize (Prf_Man_t *p)
 
static void Prf_ManClearNewInfo (Prf_Man_t *p)
 
static wordPrf_ManClauseInfo (Prf_Man_t *p, int Id)
 
static Prf_Man_tPrf_ManAlloc ()
 FUNCTION DECLARATIONS ///. More...
 
static void Prf_ManStop (Prf_Man_t *p)
 
static void Prf_ManStopP (Prf_Man_t **p)
 
static double Prf_ManMemory (Prf_Man_t *p)
 
static void Prf_ManRestart (Prf_Man_t *p, Vec_Int_t *vId2Pr, int iFirst, int nWidth)
 
static void Prf_ManGrow (Prf_Man_t *p, int nWidth)
 
static void Prf_ManShrink (Prf_Man_t *p, int iClause)
 
static void Prf_ManAddSaved (Prf_Man_t *p, int i, int iNew)
 
static void Prf_ManCompact (Prf_Man_t *p, int iNew)
 
static void Prf_ManChainResolve (Prf_Man_t *p, clause *c)
 
static void Prf_ManChainStart (Prf_Man_t *p, clause *c)
 
static int Prf_ManChainStop (Prf_Man_t *p)
 
static Vec_Int_tPrf_ManUnsatCore (Prf_Man_t *p)
 

Typedef Documentation

typedef typedefABC_NAMESPACE_HEADER_START struct Prf_Man_t_ Prf_Man_t

INCLUDES ///.

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

FileName [satProof2.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT solver.]

Synopsis [Proof logging.]

Author [Alan Mishchenko alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 1, 2004.]

Revision [

Id:
satProof2.h,v 1.0 2004/01/01 1:00:00 alanmi Exp

]PARAMETERS ///STRUCTURE DEFINITIONS ///

Definition at line 40 of file satProof2.h.

Function Documentation

static int Prf_BitWordNum ( int  nWidth)
inlinestatic

GLOBAL VARIABLES ///.

MACRO DEFINITIONS ///

Definition at line 60 of file satProof2.h.

60 { return (nWidth >> 6) + ((nWidth & 63) > 0); }
static void Prf_ManAddSaved ( Prf_Man_t p,
int  i,
int  iNew 
)
inlinestatic

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 175 of file satProof2.h.

176 {
177  assert( p->iFirst >= 0 );
178  if ( i < p->iFirst )
179  return;
180  if ( Vec_IntSize(p->vSaved) == 0 )
181  {
182  assert( p->iFirst2 == -1 );
183  p->iFirst2 = iNew;
184  }
185  Vec_IntPush( p->vSaved, i );
186 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define assert(ex)
Definition: util_old.h:213
static Prf_Man_t* Prf_ManAlloc ( )
inlinestatic

FUNCTION DECLARATIONS ///.

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 81 of file satProof2.h.

82 {
83  Prf_Man_t * p;
84  p = ABC_CALLOC( Prf_Man_t, 1 );
85  p->iFirst = -1;
86  p->iFirst2 = -1;
87  p->vInfo = Vec_WrdAlloc( 1000 );
88  p->vSaved = Vec_IntAlloc( 1000 );
89  return p;
90 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_HEADER_START struct Prf_Man_t_ Prf_Man_t
INCLUDES ///.
Definition: satProof2.h:40
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static Vec_Wrd_t * Vec_WrdAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecWrd.h:80
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
static void Prf_ManChainResolve ( Prf_Man_t p,
clause c 
)
inlinestatic

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 222 of file satProof2.h.

223 {
224  assert( p->iFirst >= 0 );
225  assert( p->pInfo != NULL );
226  // add to proof info
227  if ( c->lrn ) // learned clause
228  {
229  if ( clause_id(c) >= p->iFirst )
230  {
231  word * pProofStart;
232  int w;
233  assert( clause_id(c) - p->iFirst >= 0 );
234  assert( clause_id(c) - p->iFirst < Prf_ManSize(p) );
235  pProofStart = Prf_ManClauseInfo( p, clause_id(c) - p->iFirst );
236  for ( w = 0; w < p->nWords; w++ )
237  p->pInfo[w] |= pProofStart[w];
238  }
239  }
240  else // problem clause
241  {
242  if ( clause_id(c) >= 0 ) // has proof ID
243  {
244  int Entry;
245  if ( p->vId2Pr == NULL )
246  Entry = clause_id(c);
247  else
248  Entry = Vec_IntEntry( p->vId2Pr, clause_id(c) );
249  if ( Entry >= 0 )
250  {
251  assert( Entry < 64 * p->nWords );
252  Abc_InfoSetBit( (unsigned *)p->pInfo, Entry );
253  }
254  }
255  }
256 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int clause_id(clause *c)
Definition: satClause.h:144
int nWords
Definition: abcNpn.c:127
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
static word * Prf_ManClauseInfo(Prf_Man_t *p, int Id)
Definition: satProof2.h:63
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
unsigned lrn
Definition: satClause.h:51
#define assert(ex)
Definition: util_old.h:213
static int Prf_ManSize(Prf_Man_t *p)
Definition: satProof2.h:61
static void Prf_ManChainStart ( Prf_Man_t p,
clause c 
)
inlinestatic

Definition at line 257 of file satProof2.h.

258 {
259  assert( p->iFirst >= 0 );
260  // prepare info for new clause
262  // get pointer to the proof
263  assert( p->pInfo == NULL );
264  p->pInfo = Prf_ManClauseInfo( p, Prf_ManSize(p)-1 );
265  // add to proof info
266  Prf_ManChainResolve( p, c );
267 }
static void Prf_ManClearNewInfo(Prf_Man_t *p)
Definition: satProof2.h:62
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static void Prf_ManChainResolve(Prf_Man_t *p, clause *c)
Definition: satProof2.h:222
static word * Prf_ManClauseInfo(Prf_Man_t *p, int Id)
Definition: satProof2.h:63
#define assert(ex)
Definition: util_old.h:213
static int Prf_ManSize(Prf_Man_t *p)
Definition: satProof2.h:61
static int Prf_ManChainStop ( Prf_Man_t p)
inlinestatic

Definition at line 268 of file satProof2.h.

269 {
270  assert( p->pInfo != NULL );
271  p->pInfo = NULL;
272  return 0;
273 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define assert(ex)
Definition: util_old.h:213
static word* Prf_ManClauseInfo ( Prf_Man_t p,
int  Id 
)
inlinestatic

Definition at line 63 of file satProof2.h.

63 { return Vec_WrdEntryP( p->vInfo, Id * p->nWords ); }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static word * Vec_WrdEntryP(Vec_Wrd_t *p, int i)
Definition: vecWrd.h:401
static void Prf_ManClearNewInfo ( Prf_Man_t p)
inlinestatic

Definition at line 62 of file satProof2.h.

62 { int w; for ( w = 0; w < p->nWords; w++ ) Vec_WrdPush( p->vInfo, 0 ); }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static void Vec_WrdPush(Vec_Wrd_t *p, word Entry)
Definition: vecWrd.h:618
static void Prf_ManCompact ( Prf_Man_t p,
int  iNew 
)
inlinestatic

Definition at line 187 of file satProof2.h.

188 {
189  int i, w, k = 0, Entry, nSize;
190  assert( p->iFirst >= 0 );
191  assert( p->pInfo == NULL );
192  nSize = Prf_ManSize( p );
193  Vec_IntForEachEntry( p->vSaved, Entry, i )
194  {
195  assert( Entry - p->iFirst >= 0 && Entry - p->iFirst < nSize );
196  p->pInfo = Prf_ManClauseInfo( p, Entry - p->iFirst );
197  for ( w = 0; w < p->nWords; w++ )
198  Vec_WrdWriteEntry( p->vInfo, k++, p->pInfo[w] );
199  }
200  Vec_WrdShrink( p->vInfo, k );
201  Vec_IntClear( p->vSaved );
202  p->pInfo = NULL;
203  // update first
204  if ( p->iFirst2 == -1 )
205  p->iFirst = iNew;
206  else
207  p->iFirst = p->iFirst2;
208  p->iFirst2 = -1;
209 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static void Vec_WrdShrink(Vec_Wrd_t *p, int nSizeNew)
Definition: vecWrd.h:585
static void Vec_WrdWriteEntry(Vec_Wrd_t *p, int i, word Entry)
Definition: vecWrd.h:418
static word * Prf_ManClauseInfo(Prf_Man_t *p, int Id)
Definition: satProof2.h:63
#define assert(ex)
Definition: util_old.h:213
static int Prf_ManSize(Prf_Man_t *p)
Definition: satProof2.h:61
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
static void Prf_ManGrow ( Prf_Man_t p,
int  nWidth 
)
inlinestatic

Definition at line 129 of file satProof2.h.

130 {
131  Vec_Wrd_t * vInfoNew;
132  int i, w, nSize, nWordsNew;
133  assert( p->iFirst >= 0 );
134  assert( p->pInfo == NULL );
135  if ( nWidth < 64 * p->nWords )
136  return;
137  // get word count after resizing
138  nWordsNew = Abc_MaxInt( Prf_BitWordNum(nWidth), 2 * p->nWords );
139  // remap the entries
140  nSize = Prf_ManSize( p );
141  vInfoNew = Vec_WrdAlloc( (nSize + 1000) * nWordsNew );
142  for ( i = 0; i < nSize; i++ )
143  {
144  p->pInfo = Prf_ManClauseInfo( p, i );
145  for ( w = 0; w < p->nWords; w++ )
146  Vec_WrdPush( vInfoNew, p->pInfo[w] );
147  for ( ; w < nWordsNew; w++ )
148  Vec_WrdPush( vInfoNew, 0 );
149  }
150  Vec_WrdFree( p->vInfo );
151  p->vInfo = vInfoNew;
152  p->nWords = nWordsNew;
153  p->pInfo = NULL;
154 
155 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static void Vec_WrdPush(Vec_Wrd_t *p, word Entry)
Definition: vecWrd.h:618
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
int nWords
Definition: abcNpn.c:127
static word * Prf_ManClauseInfo(Prf_Man_t *p, int Id)
Definition: satProof2.h:63
static void Vec_WrdFree(Vec_Wrd_t *p)
Definition: vecWrd.h:260
static Vec_Wrd_t * Vec_WrdAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecWrd.h:80
static int Prf_BitWordNum(int nWidth)
GLOBAL VARIABLES ///.
Definition: satProof2.h:60
#define assert(ex)
Definition: util_old.h:213
static int Prf_ManSize(Prf_Man_t *p)
Definition: satProof2.h:61
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition: vecWrd.h:42
static double Prf_ManMemory ( Prf_Man_t p)
inlinestatic

Definition at line 104 of file satProof2.h.

105 {
106  return Vec_WrdMemory(p->vInfo) + Vec_IntMemory(p->vSaved) + sizeof(Prf_Man_t);
107 }
static double Vec_IntMemory(Vec_Int_t *p)
Definition: vecInt.h:384
static double Vec_WrdMemory(Vec_Wrd_t *p)
Definition: vecWrd.h:368
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_HEADER_START struct Prf_Man_t_ Prf_Man_t
INCLUDES ///.
Definition: satProof2.h:40
static void Prf_ManRestart ( Prf_Man_t p,
Vec_Int_t vId2Pr,
int  iFirst,
int  nWidth 
)
inlinestatic

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 120 of file satProof2.h.

121 {
122  assert( p->iFirst == -1 );
123  p->iFirst = iFirst;
124  p->nWords = Prf_BitWordNum( nWidth );
125  p->vId2Pr = vId2Pr;
126  p->pInfo = NULL;
127  Vec_WrdClear( p->vInfo );
128 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static void Vec_WrdClear(Vec_Wrd_t *p)
Definition: vecWrd.h:602
static int Prf_BitWordNum(int nWidth)
GLOBAL VARIABLES ///.
Definition: satProof2.h:60
#define assert(ex)
Definition: util_old.h:213
static void Prf_ManShrink ( Prf_Man_t p,
int  iClause 
)
inlinestatic

Definition at line 156 of file satProof2.h.

157 {
158  assert( p->iFirst >= 0 );
159  assert( iClause - p->iFirst >= 0 );
160  assert( iClause - p->iFirst < Prf_ManSize(p) );
161  Vec_WrdShrink( p->vInfo, (iClause - p->iFirst) * p->nWords );
162 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static void Vec_WrdShrink(Vec_Wrd_t *p, int nSizeNew)
Definition: vecWrd.h:585
#define assert(ex)
Definition: util_old.h:213
static int Prf_ManSize(Prf_Man_t *p)
Definition: satProof2.h:61
static int Prf_ManSize ( Prf_Man_t p)
inlinestatic

Definition at line 61 of file satProof2.h.

61 { return Vec_WrdSize( p->vInfo ) / p->nWords; }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Vec_WrdSize(Vec_Wrd_t *p)
Definition: vecWrd.h:336
static void Prf_ManStop ( Prf_Man_t p)
inlinestatic

Definition at line 91 of file satProof2.h.

92 {
93  if ( p == NULL )
94  return;
95  Vec_IntFree( p->vSaved );
96  Vec_WrdFree( p->vInfo );
97  ABC_FREE( p );
98 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static void Vec_WrdFree(Vec_Wrd_t *p)
Definition: vecWrd.h:260
#define ABC_FREE(obj)
Definition: abc_global.h:232
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static void Prf_ManStopP ( Prf_Man_t **  p)
inlinestatic

Definition at line 99 of file satProof2.h.

100 {
101  Prf_ManStop( *p );
102  *p = NULL;
103 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static void Prf_ManStop(Prf_Man_t *p)
Definition: satProof2.h:91
static Vec_Int_t* Prf_ManUnsatCore ( Prf_Man_t p)
inlinestatic

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 287 of file satProof2.h.

288 {
289  Vec_Int_t * vCore;
290  int i, Entry;
291  assert( p->iFirst >= 0 );
292  assert( p->pInfo == NULL );
293  assert( Prf_ManSize(p) > 0 );
294  vCore = Vec_IntAlloc( 64 * p->nWords );
295  p->pInfo = Prf_ManClauseInfo( p, Prf_ManSize(p)-1 );
296  if ( p->vId2Pr == NULL )
297  {
298  for ( i = 0; i < 64 * p->nWords; i++ )
299  if ( Abc_InfoHasBit( (unsigned *)p->pInfo, i ) )
300  Vec_IntPush( vCore, i );
301  }
302  else
303  {
304  Vec_IntForEachEntry( p->vId2Pr, Entry, i )
305  {
306  if ( Entry < 0 )
307  continue;
308  assert( Entry < 64 * p->nWords );
309  if ( Abc_InfoHasBit( (unsigned *)p->pInfo, Entry ) )
310  Vec_IntPush( vCore, i );
311  }
312  }
313  p->pInfo = NULL;
314  Vec_IntSort( vCore, 1 );
315  return vCore;
316 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
static void Vec_IntSort(Vec_Int_t *p, int fReverse)
Definition: vecInt.h:1293
int nWords
Definition: abcNpn.c:127
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static word * Prf_ManClauseInfo(Prf_Man_t *p, int Id)
Definition: satProof2.h:63
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
#define assert(ex)
Definition: util_old.h:213
static int Prf_ManSize(Prf_Man_t *p)
Definition: satProof2.h:61
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54