abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
resSat.c File Reference
#include "base/abc/abc.h"
#include "resInt.h"
#include "aig/hop/hop.h"
#include "sat/bsat/satSolver.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START int Res_SatAddConst1 (sat_solver *pSat, int iVar, int fCompl)
 DECLARATIONS ///. More...
 
int Res_SatAddEqual (sat_solver *pSat, int iVar0, int iVar1, int fCompl)
 
int Res_SatAddAnd (sat_solver *pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1)
 
void * Res_SatProveUnsat (Abc_Ntk_t *pAig, Vec_Ptr_t *vFanins)
 FUNCTION DEFINITIONS ///. More...
 
void * Res_SatSimulateConstr (Abc_Ntk_t *pAig, int fOnSet)
 
int Res_SatSimulate (Res_Sim_t *p, int nPatsLimit, int fOnSet)
 

Function Documentation

int Res_SatAddAnd ( sat_solver pSat,
int  iVar,
int  iVar0,
int  iVar1,
int  fCompl0,
int  fCompl1 
)

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

Synopsis [Adds constraints for the two-input AND-gate.]

Description []

SideEffects []

SeeAlso []

Definition at line 385 of file resSat.c.

386 {
387  lit Lits[3];
388 
389  Lits[0] = toLitCond( iVar, 1 );
390  Lits[1] = toLitCond( iVar0, fCompl0 );
391  if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
392  return 0;
393 
394  Lits[0] = toLitCond( iVar, 1 );
395  Lits[1] = toLitCond( iVar1, fCompl1 );
396  if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
397  return 0;
398 
399  Lits[0] = toLitCond( iVar, 0 );
400  Lits[1] = toLitCond( iVar0, !fCompl0 );
401  Lits[2] = toLitCond( iVar1, !fCompl1 );
402  if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
403  return 0;
404 
405  return 1;
406 }
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
int lit
Definition: satVec.h:130
static lit toLitCond(int v, int c)
Definition: satVec.h:143
int Res_SatAddConst1 ( sat_solver pSat,
int  iVar,
int  fCompl 
)

DECLARATIONS ///.

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

FileName [resSat.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Resynthesis package.]

Synopsis [Interface with the SAT solver.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 15, 2007.]

Revision [

Id:
resSat.c,v 1.00 2007/01/15 00:00:00 alanmi Exp

]

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

Synopsis [Asserts equality of the variable to a constant.]

Description []

SideEffects []

SeeAlso []

Definition at line 338 of file resSat.c.

339 {
340  lit Lit = toLitCond( iVar, fCompl );
341  if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) )
342  return 0;
343  return 1;
344 }
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
int lit
Definition: satVec.h:130
static lit toLitCond(int v, int c)
Definition: satVec.h:143
int Res_SatAddEqual ( sat_solver pSat,
int  iVar0,
int  iVar1,
int  fCompl 
)

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

Synopsis [Asserts equality of two variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 357 of file resSat.c.

358 {
359  lit Lits[2];
360 
361  Lits[0] = toLitCond( iVar0, 0 );
362  Lits[1] = toLitCond( iVar1, !fCompl );
363  if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
364  return 0;
365 
366  Lits[0] = toLitCond( iVar0, 1 );
367  Lits[1] = toLitCond( iVar1, fCompl );
368  if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
369  return 0;
370 
371  return 1;
372 }
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
int lit
Definition: satVec.h:130
static lit toLitCond(int v, int c)
Definition: satVec.h:143
void* Res_SatProveUnsat ( Abc_Ntk_t pAig,
Vec_Ptr_t vFanins 
)

FUNCTION DEFINITIONS ///.

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

Synopsis [Loads AIG into the SAT solver for checking resubstitution.]

Description []

SideEffects []

SeeAlso []

Definition at line 52 of file resSat.c.

53 {
54  void * pCnf = NULL;
55  sat_solver * pSat;
56  Vec_Ptr_t * vNodes;
57  Abc_Obj_t * pObj;
58  int i, nNodes, status;
59 
60  // make sure fanins contain POs of the AIG
61  pObj = (Abc_Obj_t *)Vec_PtrEntry( vFanins, 0 );
62  assert( pObj->pNtk == pAig && Abc_ObjIsPo(pObj) );
63 
64  // collect reachable nodes
65  vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize );
66 
67  // assign unique numbers to each node
68  nNodes = 0;
69  Abc_AigConst1(pAig)->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
70  Abc_NtkForEachPi( pAig, pObj, i )
71  pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
72  Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
73  pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
74  Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pObj, i ) // useful POs
75  pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
76 
77  // start the solver
78  pSat = sat_solver_new();
79  sat_solver_store_alloc( pSat );
80 
81  // add clause for the constant node
82  Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)Abc_AigConst1(pAig)->pCopy, 0 );
83  // add clauses for AND gates
84  Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
85  Res_SatAddAnd( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy,
86  (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, (int)(ABC_PTRUINT_T)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
87  Vec_PtrFree( vNodes );
88  // add clauses for POs
89  Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pObj, i )
90  Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy,
91  (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
92  // add trivial clauses
93  pObj = (Abc_Obj_t *)Vec_PtrEntry(vFanins, 0);
94  Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 0 ); // care-set
95  pObj = (Abc_Obj_t *)Vec_PtrEntry(vFanins, 1);
96  Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 0 ); // on-set
97 
98  // bookmark the clauses of A
100 
101  // duplicate the clauses
102  pObj = (Abc_Obj_t *)Vec_PtrEntry(vFanins, 1);
103  Sat_SolverDoubleClauses( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy );
104  // add the equality constraints
105  Vec_PtrForEachEntryStart( Abc_Obj_t *, vFanins, pObj, i, 2 )
106  Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, ((int)(ABC_PTRUINT_T)pObj->pCopy) + nNodes, 0 );
107 
108  // bookmark the roots
110 
111  // solve the problem
112  status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)10000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
113  if ( status == l_False )
114  {
115  pCnf = sat_solver_store_release( pSat );
116 // printf( "unsat\n" );
117  }
118  else if ( status == l_True )
119  {
120 // printf( "sat\n" );
121  }
122  else
123  {
124 // printf( "undef\n" );
125  }
126  sat_solver_delete( pSat );
127  return pCnf;
128 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
static Abc_Obj_t * Abc_ObjFanin1(Abc_Obj_t *pObj)
Definition: abc.h:374
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition: vecPtr.h:57
ABC_DLL Abc_Obj_t * Abc_AigConst1(Abc_Ntk_t *pNtk)
Definition: abcAig.c:683
static int Abc_ObjFaninC1(Abc_Obj_t *pObj)
Definition: abc.h:378
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
void * sat_solver_store_release(sat_solver *s)
Definition: satSolver.c:1949
int Res_SatAddEqual(sat_solver *pSat, int iVar0, int iVar1, int fCompl)
Definition: resSat.c:357
static int Abc_ObjFaninC0(Abc_Obj_t *pObj)
Definition: abc.h:377
#define l_True
Definition: SolverTypes.h:84
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
int Res_SatAddAnd(sat_solver *pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1)
Definition: resSat.c:385
Abc_Obj_t * pCopy
Definition: abc.h:148
void sat_solver_store_alloc(sat_solver *s)
Definition: satSolver.c:1916
if(last==0)
Definition: sparse_int.h:34
void sat_solver_store_mark_clauses_a(sat_solver *s)
Definition: satSolver.c:1944
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
void sat_solver_store_mark_roots(sat_solver *s)
Definition: satSolver.c:1939
Abc_Ntk_t * pNtk
Definition: abc.h:130
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
#define l_False
Definition: SolverTypes.h:85
static int Abc_ObjIsPo(Abc_Obj_t *pObj)
Definition: abc.h:348
ABC_NAMESPACE_IMPL_START int Res_SatAddConst1(sat_solver *pSat, int iVar, int fCompl)
DECLARATIONS ///.
Definition: resSat.c:338
#define assert(ex)
Definition: util_old.h:213
ABC_DLL Vec_Ptr_t * Abc_NtkDfsNodes(Abc_Ntk_t *pNtk, Abc_Obj_t **ppNodes, int nNodes)
Definition: abcDfs.c:120
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
void Sat_SolverDoubleClauses(sat_solver *p, int iVar)
Definition: satUtil.c:308
#define Abc_NtkForEachPi(pNtk, pPi, i)
Definition: abc.h:513
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
int Res_SatSimulate ( Res_Sim_t p,
int  nPatsLimit,
int  fOnSet 
)

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

Synopsis [Loads AIG into the SAT solver for constrained simulation.]

Description [Returns 1 if the required number of patterns are found. Returns 0 if the solver ran out of time or proved a constant. In the latter, case one of the flags, fConst0 or fConst1, are set to 1.]

SideEffects []

SeeAlso []

Definition at line 212 of file resSat.c.

213 {
214  Vec_Int_t * vLits;
215  Vec_Ptr_t * vPats;
216  sat_solver * pSat;
217  int RetValue = -1; // Suppress "might be used uninitialized"
218  int i, k, value, status, Lit, Var, iPat;
219  abctime clk = Abc_Clock();
220 
221 //printf( "Looking for %s: ", fOnSet? "onset " : "offset" );
222 
223  // decide what problem should be solved
224  Lit = toLitCond( (int)(ABC_PTRUINT_T)Abc_NtkPo(p->pAig,1)->pCopy, !fOnSet );
225  if ( fOnSet )
226  {
227  iPat = p->nPats1;
228  vPats = p->vPats1;
229  }
230  else
231  {
232  iPat = p->nPats0;
233  vPats = p->vPats0;
234  }
235  assert( iPat < nPatsLimit );
236 
237  // derive the SAT solver
238  pSat = (sat_solver *)Res_SatSimulateConstr( p->pAig, fOnSet );
239  pSat->fSkipSimplify = 1;
240  status = sat_solver_simplify( pSat );
241  if ( status == 0 )
242  {
243  if ( iPat == 0 )
244  {
245 // if ( fOnSet )
246 // p->fConst0 = 1;
247 // else
248 // p->fConst1 = 1;
249  RetValue = 0;
250  }
251  goto finish;
252  }
253 
254  // enumerate through the SAT assignments
255  RetValue = 1;
256  vLits = Vec_IntAlloc( 32 );
257  for ( k = iPat; k < nPatsLimit; k++ )
258  {
259  // solve with the assumption
260 // status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)10000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
261  status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)10000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
262  if ( status == l_False )
263  {
264 //printf( "Const %d\n", !fOnSet );
265  if ( k == 0 )
266  {
267  if ( fOnSet )
268  p->fConst0 = 1;
269  else
270  p->fConst1 = 1;
271  RetValue = 0;
272  }
273  break;
274  }
275  else if ( status == l_True )
276  {
277  // save the pattern
278  Vec_IntClear( vLits );
279  for ( i = 0; i < p->nTruePis; i++ )
280  {
281  Var = (int)(ABC_PTRUINT_T)Abc_NtkPi(p->pAig,i)->pCopy;
282 // value = (int)(pSat->model.ptr[Var] == l_True);
283  value = sat_solver_var_value(pSat, Var);
284  if ( value )
285  Abc_InfoSetBit( (unsigned *)Vec_PtrEntry(vPats, i), k );
286  Lit = toLitCond( Var, value );
287  Vec_IntPush( vLits, Lit );
288 // printf( "%d", value );
289  }
290 // printf( "\n" );
291 
292  status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
293  if ( status == 0 )
294  {
295  k++;
296  RetValue = 1;
297  break;
298  }
299  }
300  else
301  {
302 //printf( "Undecided\n" );
303  if ( k == 0 )
304  RetValue = 0;
305  else
306  RetValue = 1;
307  break;
308  }
309  }
310  Vec_IntFree( vLits );
311 //printf( "Found %d patterns\n", k - iPat );
312 
313  // set the new number of patterns
314  if ( fOnSet )
315  p->nPats1 = k;
316  else
317  p->nPats0 = k;
318 
319 finish:
320 
321  sat_solver_delete( pSat );
322 p->timeSat += Abc_Clock() - clk;
323  return RetValue;
324 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
int fSkipSimplify
Definition: satSolver.h:175
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vec_Ptr_t * vPats0
Definition: resInt.h:86
int nTruePis
Definition: resInt.h:73
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
#define l_True
Definition: SolverTypes.h:84
static abctime Abc_Clock()
Definition: abc_global.h:279
void * Res_SatSimulateConstr(Abc_Ntk_t *pAig, int fOnSet)
Definition: resSat.c:141
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
Abc_Obj_t * pCopy
Definition: abc.h:148
Abc_Ntk_t * pAig
Definition: resInt.h:72
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static lit toLitCond(int v, int c)
Definition: satVec.h:143
Vec_Ptr_t * vPats1
Definition: resInt.h:87
int nPats1
Definition: resInt.h:90
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
int fConst1
Definition: resInt.h:75
abctime timeSat
Definition: resInt.h:94
int fConst0
Definition: resInt.h:74
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static Abc_Obj_t * Abc_NtkPo(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:316
#define l_False
Definition: SolverTypes.h:85
int Var
Definition: SolverTypes.h:42
int value
#define assert(ex)
Definition: util_old.h:213
static Abc_Obj_t * Abc_NtkPi(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:315
int nPats0
Definition: resInt.h:89
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
ABC_INT64_T abctime
Definition: abc_global.h:278
void* Res_SatSimulateConstr ( Abc_Ntk_t pAig,
int  fOnSet 
)

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

Synopsis [Loads AIG into the SAT solver for constrained simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 141 of file resSat.c.

142 {
143  sat_solver * pSat;
144  Vec_Ptr_t * vFanins;
145  Vec_Ptr_t * vNodes;
146  Abc_Obj_t * pObj;
147  int i, nNodes;
148 
149  // start the array
150  vFanins = Vec_PtrAlloc( 2 );
151  pObj = Abc_NtkPo( pAig, 0 );
152  Vec_PtrPush( vFanins, pObj );
153  pObj = Abc_NtkPo( pAig, 1 );
154  Vec_PtrPush( vFanins, pObj );
155 
156  // collect reachable nodes
157  vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize );
158 
159  // assign unique numbers to each node
160  nNodes = 0;
161  Abc_AigConst1(pAig)->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
162  Abc_NtkForEachPi( pAig, pObj, i )
163  pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
164  Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
165  pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
166  Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pObj, i ) // useful POs
167  pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
168 
169  // start the solver
170  pSat = sat_solver_new();
171 
172  // add clause for the constant node
173  Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)Abc_AigConst1(pAig)->pCopy, 0 );
174  // add clauses for AND gates
175  Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
176  Res_SatAddAnd( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy,
177  (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, (int)(ABC_PTRUINT_T)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
178  Vec_PtrFree( vNodes );
179  // add clauses for the first PO
180  pObj = Abc_NtkPo( pAig, 0 );
181  Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy,
182  (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
183  // add clauses for the second PO
184  pObj = Abc_NtkPo( pAig, 1 );
185  Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy,
186  (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
187 
188  // add trivial clauses
189  pObj = Abc_NtkPo( pAig, 0 );
190  Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 0 ); // care-set
191 
192  pObj = Abc_NtkPo( pAig, 1 );
193  Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, !fOnSet ); // on-set
194 
195  Vec_PtrFree( vFanins );
196  return pSat;
197 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
static Abc_Obj_t * Abc_ObjFanin1(Abc_Obj_t *pObj)
Definition: abc.h:374
ABC_DLL Abc_Obj_t * Abc_AigConst1(Abc_Ntk_t *pNtk)
Definition: abcAig.c:683
static int Abc_ObjFaninC1(Abc_Obj_t *pObj)
Definition: abc.h:378
int Res_SatAddEqual(sat_solver *pSat, int iVar0, int iVar1, int fCompl)
Definition: resSat.c:357
static int Abc_ObjFaninC0(Abc_Obj_t *pObj)
Definition: abc.h:377
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
int Res_SatAddAnd(sat_solver *pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1)
Definition: resSat.c:385
Abc_Obj_t * pCopy
Definition: abc.h:148
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
static Abc_Obj_t * Abc_NtkPo(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:316
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
ABC_NAMESPACE_IMPL_START int Res_SatAddConst1(sat_solver *pSat, int iVar, int fCompl)
DECLARATIONS ///.
Definition: resSat.c:338
ABC_DLL Vec_Ptr_t * Abc_NtkDfsNodes(Abc_Ntk_t *pNtk, Abc_Obj_t **ppNodes, int nNodes)
Definition: abcDfs.c:120
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
#define Abc_NtkForEachPi(pNtk, pPi, i)
Definition: abc.h:513
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223