abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
aigInter.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [aigInter.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [AIG package.]
8 
9  Synopsis [Interpolate two AIGs.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - April 28, 2007.]
16 
17  Revision [$Id: aigInter.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "aig.h"
22 #include "sat/cnf/cnf.h"
23 #include "sat/bsat/satStore.h"
24 
26 
27 
28 ////////////////////////////////////////////////////////////////////////
29 /// DECLARATIONS ///
30 ////////////////////////////////////////////////////////////////////////
31 
32 extern abctime timeCnf;
33 extern abctime timeSat;
34 extern abctime timeInt;
35 
36 ////////////////////////////////////////////////////////////////////////
37 /// FUNCTION DEFINITIONS ///
38 ////////////////////////////////////////////////////////////////////////
39 
40 /**Function*************************************************************
41 
42  Synopsis []
43 
44  Description []
45 
46  SideEffects []
47 
48  SeeAlso []
49 
50 ***********************************************************************/
51 void Aig_ManInterFast( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose )
52 {
53  sat_solver * pSat;
54  Cnf_Dat_t * pCnfOn, * pCnfOff;
55  Aig_Obj_t * pObj, * pObj2;
56  int Lits[3], status, i;
57 // abctime clk = Abc_Clock();
58 
59  assert( Aig_ManCiNum(pManOn) == Aig_ManCiNum(pManOff) );
60  assert( Aig_ManCoNum(pManOn) == Aig_ManCoNum(pManOff) );
61 
62  // derive CNFs
63  pManOn->nRegs = Aig_ManCoNum(pManOn);
64  pCnfOn = Cnf_Derive( pManOn, Aig_ManCoNum(pManOn) );
65  pManOn->nRegs = 0;
66 
67  pManOff->nRegs = Aig_ManCoNum(pManOn);
68  pCnfOff = Cnf_Derive( pManOff, Aig_ManCoNum(pManOff) );
69  pManOff->nRegs = 0;
70 
71 // pCnfOn = Cnf_DeriveSimple( pManOn, Aig_ManCoNum(pManOn) );
72 // pCnfOff = Cnf_DeriveSimple( pManOff, Aig_ManCoNum(pManOn) );
73  Cnf_DataLift( pCnfOff, pCnfOn->nVars );
74 
75  // start the solver
76  pSat = sat_solver_new();
77  sat_solver_setnvars( pSat, pCnfOn->nVars + pCnfOff->nVars );
78 
79  // add clauses of A
80  for ( i = 0; i < pCnfOn->nClauses; i++ )
81  {
82  if ( !sat_solver_addclause( pSat, pCnfOn->pClauses[i], pCnfOn->pClauses[i+1] ) )
83  {
84  Cnf_DataFree( pCnfOn );
85  Cnf_DataFree( pCnfOff );
86  sat_solver_delete( pSat );
87  return;
88  }
89  }
90 
91  // add clauses of B
92  for ( i = 0; i < pCnfOff->nClauses; i++ )
93  {
94  if ( !sat_solver_addclause( pSat, pCnfOff->pClauses[i], pCnfOff->pClauses[i+1] ) )
95  {
96  Cnf_DataFree( pCnfOn );
97  Cnf_DataFree( pCnfOff );
98  sat_solver_delete( pSat );
99  return;
100  }
101  }
102 
103  // add PI clauses
104  // collect the common variables
105  Aig_ManForEachCi( pManOn, pObj, i )
106  {
107  pObj2 = Aig_ManCi( pManOff, i );
108 
109  Lits[0] = toLitCond( pCnfOn->pVarNums[pObj->Id], 0 );
110  Lits[1] = toLitCond( pCnfOff->pVarNums[pObj2->Id], 1 );
111  if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
112  assert( 0 );
113  Lits[0] = toLitCond( pCnfOn->pVarNums[pObj->Id], 1 );
114  Lits[1] = toLitCond( pCnfOff->pVarNums[pObj2->Id], 0 );
115  if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
116  assert( 0 );
117  }
118  status = sat_solver_simplify( pSat );
119  assert( status != 0 );
120 
121  // solve incremental SAT problems
122  Aig_ManForEachCo( pManOn, pObj, i )
123  {
124  pObj2 = Aig_ManCo( pManOff, i );
125 
126  Lits[0] = toLitCond( pCnfOn->pVarNums[pObj->Id], 0 );
127  Lits[1] = toLitCond( pCnfOff->pVarNums[pObj2->Id], 0 );
128  status = sat_solver_solve( pSat, Lits, Lits+2, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
129  if ( status != l_False )
130  printf( "The incremental SAT problem is not UNSAT.\n" );
131  }
132  Cnf_DataFree( pCnfOn );
133  Cnf_DataFree( pCnfOff );
134  sat_solver_delete( pSat );
135 // ABC_PRT( "Fast interpolation time", Abc_Clock() - clk );
136 }
137 
138 /**Function*************************************************************
139 
140  Synopsis []
141 
142  Description []
143 
144  SideEffects []
145 
146  SeeAlso []
147 
148 ***********************************************************************/
149 Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fRelation, int fVerbose )
150 {
151  void * pSatCnf = NULL;
152  Inta_Man_t * pManInter;
153  Aig_Man_t * pRes;
154  sat_solver * pSat;
155  Cnf_Dat_t * pCnfOn, * pCnfOff;
156  Vec_Int_t * vVarsAB;
157  Aig_Obj_t * pObj, * pObj2;
158  int Lits[3], status, i;
159  abctime clk;
160  int iLast = -1; // Suppress "might be used uninitialized"
161 
162  assert( Aig_ManCiNum(pManOn) == Aig_ManCiNum(pManOff) );
163 
164 clk = Abc_Clock();
165  // derive CNFs
166 // pCnfOn = Cnf_Derive( pManOn, 0 );
167 // pCnfOff = Cnf_Derive( pManOff, 0 );
168  pCnfOn = Cnf_DeriveSimple( pManOn, 0 );
169  pCnfOff = Cnf_DeriveSimple( pManOff, 0 );
170  Cnf_DataLift( pCnfOff, pCnfOn->nVars );
171 timeCnf += Abc_Clock() - clk;
172 
173 clk = Abc_Clock();
174  // start the solver
175  pSat = sat_solver_new();
176  sat_solver_store_alloc( pSat );
177  sat_solver_setnvars( pSat, pCnfOn->nVars + pCnfOff->nVars );
178 
179  // add clauses of A
180  for ( i = 0; i < pCnfOn->nClauses; i++ )
181  {
182  if ( !sat_solver_addclause( pSat, pCnfOn->pClauses[i], pCnfOn->pClauses[i+1] ) )
183  {
184  Cnf_DataFree( pCnfOn );
185  Cnf_DataFree( pCnfOff );
186  sat_solver_delete( pSat );
187  return NULL;
188  }
189  }
191 
192  // update the last clause
193  if ( fRelation )
194  {
195  extern int sat_solver_store_change_last( sat_solver * pSat );
196  iLast = sat_solver_store_change_last( pSat );
197  }
198 
199  // add clauses of B
200  for ( i = 0; i < pCnfOff->nClauses; i++ )
201  {
202  if ( !sat_solver_addclause( pSat, pCnfOff->pClauses[i], pCnfOff->pClauses[i+1] ) )
203  {
204  Cnf_DataFree( pCnfOn );
205  Cnf_DataFree( pCnfOff );
206  sat_solver_delete( pSat );
207  return NULL;
208  }
209  }
210 
211  // add PI clauses
212  // collect the common variables
213  vVarsAB = Vec_IntAlloc( Aig_ManCiNum(pManOn) );
214  if ( fRelation )
215  Vec_IntPush( vVarsAB, iLast );
216 
217  Aig_ManForEachCi( pManOn, pObj, i )
218  {
219  Vec_IntPush( vVarsAB, pCnfOn->pVarNums[pObj->Id] );
220  pObj2 = Aig_ManCi( pManOff, i );
221 
222  Lits[0] = toLitCond( pCnfOn->pVarNums[pObj->Id], 0 );
223  Lits[1] = toLitCond( pCnfOff->pVarNums[pObj2->Id], 1 );
224  if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
225  assert( 0 );
226  Lits[0] = toLitCond( pCnfOn->pVarNums[pObj->Id], 1 );
227  Lits[1] = toLitCond( pCnfOff->pVarNums[pObj2->Id], 0 );
228  if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
229  assert( 0 );
230  }
231  Cnf_DataFree( pCnfOn );
232  Cnf_DataFree( pCnfOff );
234 
235 /*
236  status = sat_solver_simplify(pSat);
237  if ( status == 0 )
238  {
239  Vec_IntFree( vVarsAB );
240  Cnf_DataFree( pCnfOn );
241  Cnf_DataFree( pCnfOff );
242  sat_solver_delete( pSat );
243  return NULL;
244  }
245 */
246 
247  // solve the problem
248  status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
249 timeSat += Abc_Clock() - clk;
250  if ( status == l_False )
251  {
252  pSatCnf = sat_solver_store_release( pSat );
253 // printf( "unsat\n" );
254  }
255  else if ( status == l_True )
256  {
257 // printf( "sat\n" );
258  }
259  else
260  {
261 // printf( "undef\n" );
262  }
263  sat_solver_delete( pSat );
264  if ( pSatCnf == NULL )
265  {
266  printf( "The SAT problem is not unsat.\n" );
267  Vec_IntFree( vVarsAB );
268  return NULL;
269  }
270 
271  // create the resulting manager
272 clk = Abc_Clock();
273  pManInter = Inta_ManAlloc();
274  pRes = (Aig_Man_t *)Inta_ManInterpolate( pManInter, (Sto_Man_t *)pSatCnf, 0, vVarsAB, fVerbose );
275  Inta_ManFree( pManInter );
276 timeInt += Abc_Clock() - clk;
277 /*
278  // test UNSAT core computation
279  {
280  Intp_Man_t * pManProof;
281  Vec_Int_t * vCore;
282  pManProof = Intp_ManAlloc();
283  vCore = Intp_ManUnsatCore( pManProof, pSatCnf, 0 );
284  Intp_ManFree( pManProof );
285  Vec_IntFree( vCore );
286  }
287 */
288  Vec_IntFree( vVarsAB );
289  Sto_ManFree( (Sto_Man_t *)pSatCnf );
290 
291 // Ioa_WriteAiger( pRes, "inter2.aig", 0, 0 );
292  return pRes;
293 }
294 
295 ////////////////////////////////////////////////////////////////////////
296 /// END OF FILE ///
297 ////////////////////////////////////////////////////////////////////////
298 
299 
301 
Inta_Man_t * Inta_ManAlloc()
FUNCTION DEFINITIONS ///.
Definition: satInterA.c:106
void * Inta_ManInterpolate(Inta_Man_t *p, Sto_Man_t *pCnf, abctime TimeToStop, void *vVarsAB, int fVerbose)
Definition: satInterA.c:944
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Definition: cnfCore.c:165
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
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
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
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
void * sat_solver_store_release(sat_solver *s)
Definition: satSolver.c:1949
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
int * pVarNums
Definition: cnf.h:63
#define l_True
Definition: SolverTypes.h:84
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
static abctime Abc_Clock()
Definition: abc_global.h:279
Definition: cnf.h:56
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
int ** pClauses
Definition: cnf.h:62
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
void sat_solver_store_alloc(sat_solver *s)
Definition: satSolver.c:1916
static lit toLitCond(int v, int c)
Definition: satVec.h:143
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Definition: aig.h:69
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
void sat_solver_store_mark_clauses_a(sat_solver *s)
Definition: satSolver.c:1944
void Aig_ManInterFast(Aig_Man_t *pManOn, Aig_Man_t *pManOff, int fVerbose)
FUNCTION DEFINITIONS ///.
Definition: aigInter.c:51
void Cnf_DataLift(Cnf_Dat_t *p, int nVarsPlus)
Definition: cnfMan.c:205
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
void sat_solver_store_mark_roots(sat_solver *s)
Definition: satSolver.c:1939
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
Aig_Man_t * Aig_ManInter(Aig_Man_t *pManOn, Aig_Man_t *pManOff, int fRelation, int fVerbose)
Definition: aigInter.c:149
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
Cnf_Dat_t * Cnf_DeriveSimple(Aig_Man_t *p, int nOutputs)
Definition: cnfWrite.c:587
void Sto_ManFree(Sto_Man_t *p)
Definition: satStore.c:143
void Inta_ManFree(Inta_Man_t *p)
Definition: satInterA.c:250
#define l_False
Definition: SolverTypes.h:85
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
#define assert(ex)
Definition: util_old.h:213
int sat_solver_store_change_last(sat_solver *s)
Definition: satSolver.c:1933
abctime timeSat
Definition: abcDar.c:3799
ABC_NAMESPACE_IMPL_START abctime timeCnf
DECLARATIONS ///.
Definition: abcDar.c:3798
abctime timeInt
Definition: abcDar.c:3800
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
ABC_INT64_T abctime
Definition: abc_global.h:278
int Id
Definition: aig.h:85