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

Go to the source code of this file.

Data Structures

struct  Inter_Check_t_
 DECLARATIONS ///. More...
 

Functions

Aig_Man_tInter_ManUnrollFrames (Aig_Man_t *pAig, int nFrames)
 FUNCTION DEFINITIONS ///. More...
 
Inter_Check_tInter_CheckStart (Aig_Man_t *pTrans, int nFramesK)
 MACRO DEFINITIONS ///. More...
 
void Inter_CheckStop (Inter_Check_t *p)
 
void Inter_CheckAddOrGate (Inter_Check_t *p, int iVarA, int iVarB, int iVarC)
 
void Inter_CheckAddEqual (Inter_Check_t *p, int iVarA, int iVarB)
 
int Inter_CheckPerform (Inter_Check_t *p, Cnf_Dat_t *pCnfInt, abctime nTimeNewOut)
 

Function Documentation

void Inter_CheckAddEqual ( Inter_Check_t p,
int  iVarA,
int  iVarB 
)

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

Synopsis [Creates equality: A = B.]

Description []

SideEffects []

SeeAlso []

Definition at line 194 of file intCheck.c.

195 {
196  int RetValue, pLits[3];
197  // add A => B or !A + B
198  pLits[0] = toLitCond(iVarA, 1);
199  pLits[1] = toLitCond(iVarB, 0);
200  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
201  assert( RetValue );
202  // add B => A or !B + A
203  pLits[0] = toLitCond(iVarB, 1);
204  pLits[1] = toLitCond(iVarA, 0);
205  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
206  assert( RetValue );
207 }
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
static lit toLitCond(int v, int c)
Definition: satVec.h:143
#define assert(ex)
Definition: util_old.h:213
sat_solver * pSat
Definition: intCheck.c:37
void Inter_CheckAddOrGate ( Inter_Check_t p,
int  iVarA,
int  iVarB,
int  iVarC 
)

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

Synopsis [Creates one OR-gate: A + B = C.]

Description []

SideEffects []

SeeAlso []

Definition at line 162 of file intCheck.c.

163 {
164  int RetValue, pLits[3];
165  // add A => C or !A + C
166  pLits[0] = toLitCond(iVarA, 1);
167  pLits[1] = toLitCond(iVarC, 0);
168  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
169  assert( RetValue );
170  // add B => C or !B + C
171  pLits[0] = toLitCond(iVarB, 1);
172  pLits[1] = toLitCond(iVarC, 0);
173  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
174  assert( RetValue );
175  // add !A & !B => !C or A + B + !C
176  pLits[0] = toLitCond(iVarA, 0);
177  pLits[1] = toLitCond(iVarB, 0);
178  pLits[2] = toLitCond(iVarC, 1);
179  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
180  assert( RetValue );
181 }
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
static lit toLitCond(int v, int c)
Definition: satVec.h:143
#define assert(ex)
Definition: util_old.h:213
sat_solver * pSat
Definition: intCheck.c:37
int Inter_CheckPerform ( Inter_Check_t p,
Cnf_Dat_t pCnfInt,
abctime  nTimeNewOut 
)

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

Synopsis [Perform the checking.]

Description [Returns 1 if the check has passed.]

SideEffects []

SeeAlso []

Definition at line 220 of file intCheck.c.

221 {
222  Aig_Obj_t * pObj, * pObj2;
223  int i, f, VarA, VarB, RetValue, Entry, status;
224  int nRegs = Aig_ManCiNum(pCnfInt->pMan);
225  assert( Aig_ManCoNum(p->pCnf->pMan) == p->nFramesK * nRegs );
226  assert( Aig_ManCoNum(pCnfInt->pMan) == 1 );
227 
228  // set runtime limit
229  if ( nTimeNewOut )
230  sat_solver_set_runtime_limit( p->pSat, nTimeNewOut );
231 
232  // add clauses to the SAT solver
233  Cnf_DataLift( pCnfInt, p->nVars );
234  for ( f = 0; f <= p->nFramesK; f++ )
235  {
236  // add clauses to the solver
237  for ( i = 0; i < pCnfInt->nClauses; i++ )
238  {
239  RetValue = sat_solver_addclause( p->pSat, pCnfInt->pClauses[i], pCnfInt->pClauses[i+1] );
240  assert( RetValue );
241  }
242  // add equality clauses for the flop variables
243  Aig_ManForEachCi( pCnfInt->pMan, pObj, i )
244  {
245  pObj2 = f ? Aig_ManCo(p->pFrames, i + (f-1) * nRegs) : Aig_ManCi(p->pFrames, i);
246  Inter_CheckAddEqual( p, pCnfInt->pVarNums[pObj->Id], p->pCnf->pVarNums[pObj2->Id] );
247  }
248  // add final clauses
249  if ( f < p->nFramesK )
250  {
251  if ( f == Vec_IntSize(p->vOrLits) ) // find time here
252  {
253  // add literal to this frame
254  VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ];
255  Vec_IntPush( p->vOrLits, VarB );
256  }
257  else
258  {
259  // add OR gate for this frame
260  VarA = Vec_IntEntry( p->vOrLits, f );
261  VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ];
262  Inter_CheckAddOrGate( p, VarA, VarB, p->nVars + pCnfInt->nVars );
263  Vec_IntWriteEntry( p->vOrLits, f, p->nVars + pCnfInt->nVars ); // using var ID!
264  }
265  }
266  else
267  {
268  // add AND gate for this frame
269  VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ];
270  Vec_IntPush( p->vAndLits, VarB );
271  }
272  // update variable IDs
273  Cnf_DataLift( pCnfInt, pCnfInt->nVars + 1 );
274  p->nVars += pCnfInt->nVars + 1;
275  }
276  Cnf_DataLift( pCnfInt, -p->nVars );
277  assert( Vec_IntSize(p->vOrLits) == p->nFramesK );
278 
279  // collect the assumption literals
280  Vec_IntClear( p->vAssLits );
281  Vec_IntForEachEntry( p->vOrLits, Entry, i )
282  Vec_IntPush( p->vAssLits, toLitCond(Entry, 0) );
283  Vec_IntForEachEntry( p->vAndLits, Entry, i )
284  Vec_IntPush( p->vAssLits, toLitCond(Entry, 1) );
285 /*
286  if ( pCnfInt->nLiterals == 3635 )
287  {
288  int s = 0;
289  }
290 */
291  // call the SAT solver
292  status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssLits),
293  Vec_IntArray(p->vAssLits) + Vec_IntSize(p->vAssLits),
294  (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
295 
296  return status == l_False;
297 }
static abctime sat_solver_set_runtime_limit(sat_solver *s, abctime Limit)
Definition: satSolver.h:233
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Vec_Int_t * vOrLits
Definition: intCheck.c:38
void Inter_CheckAddOrGate(Inter_Check_t *p, int iVarA, int iVarB, int iVarC)
Definition: intCheck.c:162
Vec_Int_t * vAssLits
Definition: intCheck.c:40
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
int nClauses
Definition: cnf.h:61
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
int nVars
Definition: cnf.h:59
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
int * pVarNums
Definition: cnf.h:63
Aig_Man_t * pMan
Definition: cnf.h:58
Cnf_Dat_t * pCnf
Definition: intCheck.c:36
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
int ** pClauses
Definition: cnf.h:62
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
static lit toLitCond(int v, int c)
Definition: satVec.h:143
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Definition: aig.h:69
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Aig_Man_t * pFrames
Definition: intCheck.c:35
void Cnf_DataLift(Cnf_Dat_t *p, int nVarsPlus)
Definition: cnfMan.c:205
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Vec_Int_t * vAndLits
Definition: intCheck.c:39
#define l_False
Definition: SolverTypes.h:85
void Inter_CheckAddEqual(Inter_Check_t *p, int iVarA, int iVarB)
Definition: intCheck.c:194
#define assert(ex)
Definition: util_old.h:213
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
int Id
Definition: aig.h:85
sat_solver * pSat
Definition: intCheck.c:37
Inter_Check_t* Inter_CheckStart ( Aig_Man_t pTrans,
int  nFramesK 
)

MACRO DEFINITIONS ///.

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

Synopsis [This procedure sets default values of interpolation parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 105 of file intCheck.c.

106 {
107  Inter_Check_t * p;
108  // create solver
109  p = ABC_CALLOC( Inter_Check_t, 1 );
110  p->vOrLits = Vec_IntAlloc( 100 );
111  p->vAndLits = Vec_IntAlloc( 100 );
112  p->vAssLits = Vec_IntAlloc( 100 );
113  // generate the timeframes
114  p->pFrames = Inter_ManUnrollFrames( pTrans, nFramesK );
115  assert( Aig_ManCiNum(p->pFrames) == nFramesK * Saig_ManPiNum(pTrans) + Saig_ManRegNum(pTrans) );
116  assert( Aig_ManCoNum(p->pFrames) == nFramesK * Saig_ManRegNum(pTrans) );
117  // convert to CNF
118  p->pCnf = Cnf_Derive( p->pFrames, Aig_ManCoNum(p->pFrames) );
119  p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
120  // assign parameters
121  p->nFramesK = nFramesK;
122  p->nVars = p->pCnf->nVars;
123  return p;
124 }
Vec_Int_t * vOrLits
Definition: intCheck.c:38
Vec_Int_t * vAssLits
Definition: intCheck.c:40
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Definition: cnfCore.c:165
static Llb_Mgr_t * p
Definition: llb3Image.c:950
DECLARATIONS ///.
Definition: intCheck.c:31
int nVars
Definition: cnf.h:59
Cnf_Dat_t * pCnf
Definition: intCheck.c:36
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Aig_Man_t * pFrames
Definition: intCheck.c:35
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition: cnfMan.c:463
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
Vec_Int_t * vAndLits
Definition: intCheck.c:39
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Aig_Man_t * Inter_ManUnrollFrames(Aig_Man_t *pAig, int nFrames)
FUNCTION DEFINITIONS ///.
Definition: intCheck.c:59
#define assert(ex)
Definition: util_old.h:213
sat_solver * pSat
Definition: intCheck.c:37
void Inter_CheckStop ( Inter_Check_t p)

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

Synopsis [This procedure sets default values of interpolation parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 137 of file intCheck.c.

138 {
139  if ( p == NULL )
140  return;
141  Vec_IntFree( p->vOrLits );
142  Vec_IntFree( p->vAndLits );
143  Vec_IntFree( p->vAssLits );
144  Cnf_DataFree( p->pCnf );
145  Aig_ManStop( p->pFrames );
146  sat_solver_delete( p->pSat );
147  ABC_FREE( p );
148 }
Vec_Int_t * vOrLits
Definition: intCheck.c:38
Vec_Int_t * vAssLits
Definition: intCheck.c:40
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Cnf_Dat_t * pCnf
Definition: intCheck.c:36
Aig_Man_t * pFrames
Definition: intCheck.c:35
#define ABC_FREE(obj)
Definition: abc_global.h:232
Vec_Int_t * vAndLits
Definition: intCheck.c:39
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
sat_solver * pSat
Definition: intCheck.c:37
Aig_Man_t* Inter_ManUnrollFrames ( Aig_Man_t pAig,
int  nFrames 
)

FUNCTION DEFINITIONS ///.

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

Synopsis [Create timeframes of the manager for interpolation.]

Description [The resulting manager is combinational. The primary inputs corresponding to register outputs are ordered first.]

SideEffects []

SeeAlso []

Definition at line 59 of file intCheck.c.

60 {
61  Aig_Man_t * pFrames;
62  Aig_Obj_t * pObj, * pObjLi, * pObjLo;
63  int i, f;
64  assert( Saig_ManRegNum(pAig) > 0 );
65  pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
66  // map the constant node
67  Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
68  // create variables for register outputs
69  Saig_ManForEachLo( pAig, pObj, i )
70  pObj->pData = Aig_ObjCreateCi( pFrames );
71  // add timeframes
72  for ( f = 0; f < nFrames; f++ )
73  {
74  // create PI nodes for this frame
75  Saig_ManForEachPi( pAig, pObj, i )
76  pObj->pData = Aig_ObjCreateCi( pFrames );
77  // add internal nodes of this frame
78  Aig_ManForEachNode( pAig, pObj, i )
79  pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
80  // save register inputs
81  Saig_ManForEachLi( pAig, pObj, i )
82  pObj->pData = Aig_ObjChild0Copy(pObj);
83  // transfer to register outputs
84  Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
85  {
86  pObjLo->pData = pObjLi->pData;
87  Aig_ObjCreateCo( pFrames, (Aig_Obj_t *)pObjLo->pData );
88  }
89  }
90  Aig_ManCleanup( pFrames );
91  return pFrames;
92 }
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
void * pData
Definition: aig.h:87
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
for(p=first;p->value< newval;p=p->next)
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Definition: aig.h:69
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
#define assert(ex)
Definition: util_old.h:213
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91