abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions
sswCnf.c File Reference
#include "sswInt.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START
Ssw_Sat_t * 		Ssw_SatStart (int fPolarFlip)
 DECLARATIONS ///. More...
 
void Ssw_SatStop (Ssw_Sat_t *p)
 
void Ssw_AddClausesMux (Ssw_Sat_t *p, Aig_Obj_t *pNode)
 
void Ssw_AddClausesSuper (Ssw_Sat_t *p, Aig_Obj_t *pNode, Vec_Ptr_t *vSuper)
 
void Ssw_CollectSuper_rec (Aig_Obj_t *pObj, Vec_Ptr_t *vSuper, int fFirst, int fUseMuxes)
 
void Ssw_CollectSuper (Aig_Obj_t *pObj, int fUseMuxes, Vec_Ptr_t *vSuper)
 
void Ssw_ObjAddToFrontier (Ssw_Sat_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vFrontier)
 
void Ssw_CnfNodeAddToSolver (Ssw_Sat_t *p, Aig_Obj_t *pObj)
 
int Ssw_CnfGetNodeValue (Ssw_Sat_t *p, Aig_Obj_t *pObj)
 

Function Documentation

void Ssw_AddClausesMux ( Ssw_Sat_t *  p,
Aig_Obj_t *  pNode 
)

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

Synopsis [Addes clauses to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 104 of file sswCnf.c.

105 {
106  Aig_Obj_t * pNodeI, * pNodeT, * pNodeE;
107  int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
108 
109  assert( !Aig_IsComplement( pNode ) );
110  assert( Aig_ObjIsMuxType( pNode ) );
111  // get nodes (I = if, T = then, E = else)
112  pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
113  // get the variable numbers
114  VarF = Ssw_ObjSatNum(p,pNode);
115  VarI = Ssw_ObjSatNum(p,pNodeI);
116  VarT = Ssw_ObjSatNum(p,Aig_Regular(pNodeT));
117  VarE = Ssw_ObjSatNum(p,Aig_Regular(pNodeE));
118  // get the complementation flags
119  fCompT = Aig_IsComplement(pNodeT);
120  fCompE = Aig_IsComplement(pNodeE);
121 
122  // f = ITE(i, t, e)
123 
124  // i' + t' + f
125  // i' + t + f'
126  // i + e' + f
127  // i + e + f'
128 
129  // create four clauses
130  pLits[0] = toLitCond(VarI, 1);
131  pLits[1] = toLitCond(VarT, 1^fCompT);
132  pLits[2] = toLitCond(VarF, 0);
133  if ( p->fPolarFlip )
134  {
135  if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
136  if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
137  if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
138  }
139  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
140  assert( RetValue );
141  pLits[0] = toLitCond(VarI, 1);
142  pLits[1] = toLitCond(VarT, 0^fCompT);
143  pLits[2] = toLitCond(VarF, 1);
144  if ( p->fPolarFlip )
145  {
146  if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
147  if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
148  if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
149  }
150  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
151  assert( RetValue );
152  pLits[0] = toLitCond(VarI, 0);
153  pLits[1] = toLitCond(VarE, 1^fCompE);
154  pLits[2] = toLitCond(VarF, 0);
155  if ( p->fPolarFlip )
156  {
157  if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
158  if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
159  if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
160  }
161  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
162  assert( RetValue );
163  pLits[0] = toLitCond(VarI, 0);
164  pLits[1] = toLitCond(VarE, 0^fCompE);
165  pLits[2] = toLitCond(VarF, 1);
166  if ( p->fPolarFlip )
167  {
168  if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
169  if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
170  if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
171  }
172  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
173  assert( RetValue );
174 
175  // two additional clauses
176  // t' & e' -> f'
177  // t & e -> f
178 
179  // t + e + f'
180  // t' + e' + f
181 
182  if ( VarT == VarE )
183  {
184 // assert( fCompT == !fCompE );
185  return;
186  }
187 
188  pLits[0] = toLitCond(VarT, 0^fCompT);
189  pLits[1] = toLitCond(VarE, 0^fCompE);
190  pLits[2] = toLitCond(VarF, 1);
191  if ( p->fPolarFlip )
192  {
193  if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
194  if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
195  if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
196  }
197  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
198  assert( RetValue );
199  pLits[0] = toLitCond(VarT, 1^fCompT);
200  pLits[1] = toLitCond(VarE, 1^fCompE);
201  pLits[2] = toLitCond(VarF, 0);
202  if ( p->fPolarFlip )
203  {
204  if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
205  if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
206  if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
207  }
208  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
209  assert( RetValue );
210 }
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
lit_neg
static lit lit_neg(lit l)
Definition: satVec.h:144
Ssw_Sat_t_::pSat
sat_solver * pSat
Definition: sswInt.h:147
Aig_ObjRecognizeMux
Aig_Obj_t * Aig_ObjRecognizeMux(Aig_Obj_t *pObj, Aig_Obj_t **ppObjT, Aig_Obj_t **ppObjE)
Definition: aigUtil.c:387
toLitCond
static lit toLitCond(int v, int c)
Definition: satVec.h:143
Aig_Obj_t_
Definition: aig.h:69
Ssw_Sat_t_::fPolarFlip
int fPolarFlip
Definition: sswInt.h:146
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
Aig_ObjIsMuxType
int Aig_ObjIsMuxType(Aig_Obj_t *pObj)
Definition: aigUtil.c:307
Ssw_ObjSatNum
static int Ssw_ObjSatNum(Ssw_Sat_t *p, Aig_Obj_t *pObj)
MACRO DEFINITIONS ///.
Definition: sswInt.h:169
assert
#define assert(ex)
Definition: util_old.h:213
void Ssw_AddClausesSuper ( Ssw_Sat_t *  p,
Aig_Obj_t *  pNode,
Vec_Ptr_t *  vSuper 
)

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

Synopsis [Addes clauses to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 223 of file sswCnf.c.

224 {
225  Aig_Obj_t * pFanin;
226  int * pLits, nLits, RetValue, i;
227  assert( !Aig_IsComplement(pNode) );
228  assert( Aig_ObjIsNode( pNode ) );
229  // create storage for literals
230  nLits = Vec_PtrSize(vSuper) + 1;
231  pLits = ABC_ALLOC( int, nLits );
232  // suppose AND-gate is A & B = C
233  // add !A => !C or A + !C
234  Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
235  {
236  pLits[0] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
237  pLits[1] = toLitCond(Ssw_ObjSatNum(p,pNode), 1);
238  if ( p->fPolarFlip )
239  {
240  if ( Aig_Regular(pFanin)->fPhase ) pLits[0] = lit_neg( pLits[0] );
241  if ( pNode->fPhase ) pLits[1] = lit_neg( pLits[1] );
242  }
243  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
244  assert( RetValue );
245  }
246  // add A & B => C or !A + !B + C
247  Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
248  {
249  pLits[i] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
250  if ( p->fPolarFlip )
251  {
252  if ( Aig_Regular(pFanin)->fPhase ) pLits[i] = lit_neg( pLits[i] );
253  }
254  }
255  pLits[nLits-1] = toLitCond(Ssw_ObjSatNum(p,pNode), 0);
256  if ( p->fPolarFlip )
257  {
258  if ( pNode->fPhase ) pLits[nLits-1] = lit_neg( pLits[nLits-1] );
259  }
260  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
261  assert( RetValue );
262  ABC_FREE( pLits );
263 }
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
lit_neg
static lit lit_neg(lit l)
Definition: satVec.h:144
Ssw_Sat_t_::pSat
sat_solver * pSat
Definition: sswInt.h:147
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
toLitCond
static lit toLitCond(int v, int c)
Definition: satVec.h:143
Aig_Obj_t_
Definition: aig.h:69
Ssw_Sat_t_::fPolarFlip
int fPolarFlip
Definition: sswInt.h:146
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Ssw_ObjSatNum
static int Ssw_ObjSatNum(Ssw_Sat_t *p, Aig_Obj_t *pObj)
MACRO DEFINITIONS ///.
Definition: sswInt.h:169
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
int Ssw_CnfGetNodeValue ( Ssw_Sat_t *  p,
Aig_Obj_t *  pObj 
)

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

Synopsis [Copy pattern from the solver into the internal storage.]

Description []

SideEffects []

SeeAlso []

Definition at line 402 of file sswCnf.c.

403 {
404  int Value0, Value1, nVarNum;
405  assert( !Aig_IsComplement(pObj) );
406  nVarNum = Ssw_ObjSatNum( p, pObj );
407  if ( nVarNum > 0 )
408  return sat_solver_var_value( p->pSat, nVarNum );
409 // if ( pObj->fMarkA == 1 )
410 // return 0;
411  if ( Aig_ObjIsCi(pObj) )
412  return 0;
413  assert( Aig_ObjIsNode(pObj) );
414  Value0 = Ssw_CnfGetNodeValue( p, Aig_ObjFanin0(pObj) );
415  Value0 ^= Aig_ObjFaninC0(pObj);
416  Value1 = Ssw_CnfGetNodeValue( p, Aig_ObjFanin1(pObj) );
417  Value1 ^= Aig_ObjFaninC1(pObj);
418  return Value0 & Value1;
419 }
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
sat_solver_var_value
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
Ssw_Sat_t_::pSat
sat_solver * pSat
Definition: sswInt.h:147
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
Ssw_ObjSatNum
static int Ssw_ObjSatNum(Ssw_Sat_t *p, Aig_Obj_t *pObj)
MACRO DEFINITIONS ///.
Definition: sswInt.h:169
assert
#define assert(ex)
Definition: util_old.h:213
Ssw_CnfGetNodeValue
int Ssw_CnfGetNodeValue(Ssw_Sat_t *p, Aig_Obj_t *pObj)
Definition: sswCnf.c:402
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
void Ssw_CnfNodeAddToSolver ( Ssw_Sat_t *  p,
Aig_Obj_t *  pObj 
)

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

Synopsis [Updates the solver clause database.]

Description []

SideEffects []

SeeAlso []

Definition at line 351 of file sswCnf.c.

352 {
353  Vec_Ptr_t * vFrontier;
354  Aig_Obj_t * pNode, * pFanin;
355  int i, k, fUseMuxes = 1;
356  // quit if CNF is ready
357  if ( Ssw_ObjSatNum(p,pObj) )
358  return;
359  // start the frontier
360  vFrontier = Vec_PtrAlloc( 100 );
361  Ssw_ObjAddToFrontier( p, pObj, vFrontier );
362  // explore nodes in the frontier
363  Vec_PtrForEachEntry( Aig_Obj_t *, vFrontier, pNode, i )
364  {
365  // create the supergate
366  assert( Ssw_ObjSatNum(p,pNode) );
367  if ( fUseMuxes && Aig_ObjIsMuxType(pNode) )
368  {
369  Vec_PtrClear( p->vFanins );
370  Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) );
371  Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
372  Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
373  Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
374  Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k )
375  Ssw_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
376  Ssw_AddClausesMux( p, pNode );
377  }
378  else
379  {
380  Ssw_CollectSuper( pNode, fUseMuxes, p->vFanins );
381  Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k )
382  Ssw_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
383  Ssw_AddClausesSuper( p, pNode, p->vFanins );
384  }
385  assert( Vec_PtrSize(p->vFanins) > 1 );
386  }
387  Vec_PtrFree( vFrontier );
388 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Vec_PtrPushUnique
static int Vec_PtrPushUnique(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:656
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Ssw_AddClausesSuper
void Ssw_AddClausesSuper(Ssw_Sat_t *p, Aig_Obj_t *pNode, Vec_Ptr_t *vSuper)
Definition: sswCnf.c:223
Ssw_Sat_t_::vFanins
Vec_Ptr_t * vFanins
Definition: sswInt.h:150
else
else
Definition: sparse_int.h:55
Aig_Obj_t_
Definition: aig.h:69
Ssw_AddClausesMux
void Ssw_AddClausesMux(Ssw_Sat_t *p, Aig_Obj_t *pNode)
Definition: sswCnf.c:104
Ssw_CollectSuper
void Ssw_CollectSuper(Aig_Obj_t *pObj, int fUseMuxes, Vec_Ptr_t *vSuper)
Definition: sswCnf.c:303
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Aig_ObjIsMuxType
int Aig_ObjIsMuxType(Aig_Obj_t *pObj)
Definition: aigUtil.c:307
Ssw_ObjSatNum
static int Ssw_ObjSatNum(Ssw_Sat_t *p, Aig_Obj_t *pObj)
MACRO DEFINITIONS ///.
Definition: sswInt.h:169
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Ssw_ObjAddToFrontier
void Ssw_ObjAddToFrontier(Ssw_Sat_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vFrontier)
Definition: sswCnf.c:322
void Ssw_CollectSuper ( Aig_Obj_t *  pObj,
int  fUseMuxes,
Vec_Ptr_t *  vSuper 
)

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

Synopsis [Collects the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 303 of file sswCnf.c.

304 {
305  assert( !Aig_IsComplement(pObj) );
306  assert( !Aig_ObjIsCi(pObj) );
307  Vec_PtrClear( vSuper );
308  Ssw_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
309 }
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Ssw_CollectSuper_rec
void Ssw_CollectSuper_rec(Aig_Obj_t *pObj, Vec_Ptr_t *vSuper, int fFirst, int fUseMuxes)
Definition: sswCnf.c:276
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
void Ssw_CollectSuper_rec ( Aig_Obj_t *  pObj,
Vec_Ptr_t *  vSuper,
int  fFirst,
int  fUseMuxes 
)

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

Synopsis [Collects the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 276 of file sswCnf.c.

277 {
278  // if the new node is complemented or a PI, another gate begins
279  if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) ||
280  (!fFirst && Aig_ObjRefs(pObj) > 1) ||
281  (fUseMuxes && Aig_ObjIsMuxType(pObj)) )
282  {
283  Vec_PtrPushUnique( vSuper, pObj );
284  return;
285  }
286 // pObj->fMarkA = 1;
287  // go through the branches
288  Ssw_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes );
289  Ssw_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes );
290 }
Aig_ObjChild0
static Aig_Obj_t * Aig_ObjChild0(Aig_Obj_t *pObj)
Definition: aig.h:310
Vec_PtrPushUnique
static int Vec_PtrPushUnique(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:656
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Aig_ObjChild1
static Aig_Obj_t * Aig_ObjChild1(Aig_Obj_t *pObj)
Definition: aig.h:311
Ssw_CollectSuper_rec
void Ssw_CollectSuper_rec(Aig_Obj_t *pObj, Vec_Ptr_t *vSuper, int fFirst, int fUseMuxes)
Definition: sswCnf.c:276
Aig_ObjIsMuxType
int Aig_ObjIsMuxType(Aig_Obj_t *pObj)
Definition: aigUtil.c:307
Aig_ObjRefs
static int Aig_ObjRefs(Aig_Obj_t *pObj)
Definition: aig.h:300
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
void Ssw_ObjAddToFrontier ( Ssw_Sat_t *  p,
Aig_Obj_t *  pObj,
Vec_Ptr_t *  vFrontier 
)

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

Synopsis [Updates the solver clause database.]

Description []

SideEffects []

SeeAlso []

Definition at line 322 of file sswCnf.c.

323 {
324  assert( !Aig_IsComplement(pObj) );
325  if ( Ssw_ObjSatNum(p,pObj) )
326  return;
327  assert( Ssw_ObjSatNum(p,pObj) == 0 );
328  if ( Aig_ObjIsConst1(pObj) )
329  return;
330 // pObj->fMarkA = 1;
331  // save PIs (used by register correspondence)
332  if ( Aig_ObjIsCi(pObj) )
333  Vec_PtrPush( p->vUsedPis, pObj );
334  Ssw_ObjSetSatNum( p, pObj, p->nSatVars++ );
335  sat_solver_setnvars( p->pSat, 100 * (1 + p->nSatVars / 100) );
336  if ( Aig_ObjIsNode(pObj) )
337  Vec_PtrPush( vFrontier, pObj );
338 }
Ssw_Sat_t_::vUsedPis
Vec_Ptr_t * vUsedPis
Definition: sswInt.h:151
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Ssw_Sat_t_::pSat
sat_solver * pSat
Definition: sswInt.h:147
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Ssw_ObjSetSatNum
static void Ssw_ObjSetSatNum(Ssw_Sat_t *p, Aig_Obj_t *pObj, int Num)
Definition: sswInt.h:170
Ssw_ObjSatNum
static int Ssw_ObjSatNum(Ssw_Sat_t *p, Aig_Obj_t *pObj)
MACRO DEFINITIONS ///.
Definition: sswInt.h:169
assert
#define assert(ex)
Definition: util_old.h:213
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Ssw_Sat_t_::nSatVars
int nSatVars
Definition: sswInt.h:148
ABC_NAMESPACE_IMPL_START Ssw_Sat_t* Ssw_SatStart ( int  fPolarFlip)

DECLARATIONS ///.

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

FileName [sswCnf.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [Computation of CNF.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 1, 2008.]

Revision [

Id:
sswCnf.c,v 1.00 2008/09/01 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Starts the SAT manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file sswCnf.c.

46 {
47  Ssw_Sat_t * p;
48  int Lit;
49  p = ABC_ALLOC( Ssw_Sat_t, 1 );
50  memset( p, 0, sizeof(Ssw_Sat_t) );
51  p->pAig = NULL;
52  p->fPolarFlip = fPolarFlip;
53  p->vSatVars = Vec_IntStart( 10000 );
54  p->vFanins = Vec_PtrAlloc( 100 );
55  p->vUsedPis = Vec_PtrAlloc( 100 );
56  p->pSat = sat_solver_new();
57  sat_solver_setnvars( p->pSat, 1000 );
58  // var 0 is not used
59  // var 1 is reserved for const1 node - add the clause
60  p->nSatVars = 1;
61  Lit = toLit( p->nSatVars );
62  if ( fPolarFlip )
63  Lit = lit_neg( Lit );
64  sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
65 // Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ );
66  Vec_IntWriteEntry( p->vSatVars, 0, p->nSatVars++ );
67  return p;
68 }
memset
char * memset()
Ssw_Sat_t_::vUsedPis
Vec_Ptr_t * vUsedPis
Definition: sswInt.h:151
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Ssw_Sat_t_::vSatVars
Vec_Int_t * vSatVars
Definition: sswInt.h:149
lit_neg
static lit lit_neg(lit l)
Definition: satVec.h:144
Ssw_Sat_t_::pSat
sat_solver * pSat
Definition: sswInt.h:147
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Ssw_Sat_t_::vFanins
Vec_Ptr_t * vFanins
Definition: sswInt.h:150
toLit
static lit toLit(int v)
Definition: satVec.h:142
Ssw_Sat_t_::pAig
Aig_Man_t * pAig
Definition: sswInt.h:145
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
Ssw_Sat_t_::fPolarFlip
int fPolarFlip
Definition: sswInt.h:146
sat_solver_new
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Ssw_Sat_t_
Definition: sswInt.h:143
Ssw_Sat_t_::nSatVars
int nSatVars
Definition: sswInt.h:148
void Ssw_SatStop ( Ssw_Sat_t *  p)

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

Synopsis [Stop the SAT manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 81 of file sswCnf.c.

82 {
83 // Abc_Print( 1, "Recycling SAT solver with %d vars and %d restarts.\n",
84 // p->pSat->size, p->pSat->stats.starts );
85  if ( p->pSat )
86  sat_solver_delete( p->pSat );
87  Vec_IntFree( p->vSatVars );
88  Vec_PtrFree( p->vFanins );
89  Vec_PtrFree( p->vUsedPis );
90  ABC_FREE( p );
91 }
Ssw_Sat_t_::vUsedPis
Vec_Ptr_t * vUsedPis
Definition: sswInt.h:151
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Ssw_Sat_t_::vSatVars
Vec_Int_t * vSatVars
Definition: sswInt.h:149
Ssw_Sat_t_::pSat
sat_solver * pSat
Definition: sswInt.h:147
Ssw_Sat_t_::vFanins
Vec_Ptr_t * vFanins
Definition: sswInt.h:150
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223