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

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START
sat_solver
Inter_ManDeriveSatSolver (Aig_Man_t *pInter, Cnf_Dat_t *pCnfInter, Aig_Man_t *pAig, Cnf_Dat_t *pCnfAig, Aig_Man_t *pFrames, Cnf_Dat_t *pCnfFrames, Vec_Int_t *vVarsAB, int fUseBackward)
 DECLARATIONS ///. More...
 
int Inter_ManPerformOneStep (Inter_Man_t *p, int fUseBias, int fUseBackward, abctime nTimeNewOut)
 

Function Documentation

ABC_NAMESPACE_IMPL_START sat_solver* Inter_ManDeriveSatSolver ( Aig_Man_t pInter,
Cnf_Dat_t pCnfInter,
Aig_Man_t pAig,
Cnf_Dat_t pCnfAig,
Aig_Man_t pFrames,
Cnf_Dat_t pCnfFrames,
Vec_Int_t vVarsAB,
int  fUseBackward 
)

DECLARATIONS ///.

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

FileName [intM114.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Interpolation engine.]

Synopsis [Intepolation using ABC's proof generator added to MiniSat-1.14c.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 24, 2008.]

Revision [

Id:
intM114.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

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

Synopsis [Returns the SAT solver for one interpolation run.]

Description [pInter is the previous interpolant. pAig is one time frame. pFrames is the unrolled time frames.]

SideEffects []

SeeAlso []

Definition at line 46 of file intM114.c.

51 {
52  sat_solver * pSat;
53  Aig_Obj_t * pObj, * pObj2;
54  int i, Lits[2];
55 
56 //Aig_ManDumpBlif( pInter, "out_inter.blif", NULL, NULL );
57 //Aig_ManDumpBlif( pAig, "out_aig.blif", NULL, NULL );
58 //Aig_ManDumpBlif( pFrames, "out_frames.blif", NULL, NULL );
59 
60  // sanity checks
61  assert( Aig_ManRegNum(pInter) == 0 );
62  assert( Aig_ManRegNum(pAig) > 0 );
63  assert( Aig_ManRegNum(pFrames) == 0 );
64  assert( Aig_ManCoNum(pInter) == 1 );
65  assert( Aig_ManCoNum(pFrames) == fUseBackward? Saig_ManRegNum(pAig) : 1 );
66  assert( fUseBackward || Aig_ManCiNum(pInter) == Aig_ManRegNum(pAig) );
67 // assert( (Aig_ManCiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
68 
69  // prepare CNFs
70  Cnf_DataLift( pCnfAig, pCnfFrames->nVars );
71  Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars );
72 
73  // start the solver
74  pSat = sat_solver_new();
75  sat_solver_store_alloc( pSat );
76  sat_solver_setnvars( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars );
77 
78  // add clauses of A
79  // interpolant
80  for ( i = 0; i < pCnfInter->nClauses; i++ )
81  {
82  if ( !sat_solver_addclause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ) )
83  {
84  sat_solver_delete( pSat );
85  // return clauses to the original state
86  Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
87  Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );
88  return NULL;
89  }
90  }
91  // connector clauses
92  if ( fUseBackward )
93  {
94  Saig_ManForEachLi( pAig, pObj2, i )
95  {
96  if ( Saig_ManRegNum(pAig) == Aig_ManCiNum(pInter) )
97  pObj = Aig_ManCi( pInter, i );
98  else
99  {
100  assert( Aig_ManCiNum(pAig) == Aig_ManCiNum(pInter) );
101  pObj = Aig_ManCi( pInter, Aig_ManCiNum(pAig)-Saig_ManRegNum(pAig) + i );
102  }
103 
104  Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
105  Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
106  if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
107  assert( 0 );
108  Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 );
109  Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
110  if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
111  assert( 0 );
112  }
113  }
114  else
115  {
116  Aig_ManForEachCi( pInter, pObj, i )
117  {
118  pObj2 = Saig_ManLo( pAig, i );
119 
120  Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
121  Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
122  if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
123  assert( 0 );
124  Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 );
125  Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
126  if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
127  assert( 0 );
128  }
129  }
130  // one timeframe
131  for ( i = 0; i < pCnfAig->nClauses; i++ )
132  {
133  if ( !sat_solver_addclause( pSat, pCnfAig->pClauses[i], pCnfAig->pClauses[i+1] ) )
134  assert( 0 );
135  }
136  // connector clauses
137  Vec_IntClear( vVarsAB );
138  if ( fUseBackward )
139  {
140  Aig_ManForEachCo( pFrames, pObj, i )
141  {
142  assert( pCnfFrames->pVarNums[pObj->Id] >= 0 );
143  Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
144 
145  pObj2 = Saig_ManLo( pAig, i );
146  Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 );
147  Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
148  if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
149  assert( 0 );
150  Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 );
151  Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
152  if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
153  assert( 0 );
154  }
155  }
156  else
157  {
158  Aig_ManForEachCi( pFrames, pObj, i )
159  {
160  if ( i == Aig_ManRegNum(pAig) )
161  break;
162  Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
163 
164  pObj2 = Saig_ManLi( pAig, i );
165  Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 );
166  Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
167  if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
168  assert( 0 );
169  Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 );
170  Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
171  if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
172  assert( 0 );
173  }
174  }
175  // add clauses of B
177  for ( i = 0; i < pCnfFrames->nClauses; i++ )
178  {
179  if ( !sat_solver_addclause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) )
180  {
181  pSat->fSolved = 1;
182  break;
183  }
184  }
186  // return clauses to the original state
187  Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
188  Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );
189  return pSat;
190 }
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
int nClauses
Definition: cnf.h:61
static Aig_Obj_t * Saig_ManLo(Aig_Man_t *p, int i)
Definition: saig.h:79
int nVars
Definition: cnf.h:59
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
int * pVarNums
Definition: cnf.h:63
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
int ** pClauses
Definition: cnf.h:62
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
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
static Aig_Obj_t * Saig_ManLi(Aig_Man_t *p, int i)
Definition: saig.h:80
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
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
void Cnf_DataLift(Cnf_Dat_t *p, int nVarsPlus)
Definition: cnfMan.c:205
void sat_solver_store_mark_roots(sat_solver *s)
Definition: satSolver.c:1939
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
#define assert(ex)
Definition: util_old.h:213
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
int Id
Definition: aig.h:85
int Inter_ManPerformOneStep ( Inter_Man_t p,
int  fUseBias,
int  fUseBackward,
abctime  nTimeNewOut 
)

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

Synopsis [Performs one SAT run with interpolation.]

Description [Returns 1 if proven. 0 if failed. -1 if undecided.]

SideEffects []

SeeAlso []

Definition at line 203 of file intM114.c.

204 {
205  sat_solver * pSat;
206  void * pSatCnf = NULL;
207  Inta_Man_t * pManInterA;
208 // Intb_Man_t * pManInterB;
209  int * pGlobalVars;
210  int status, RetValue;
211  int i, Var;
212  abctime clk;
213 // assert( p->pInterNew == NULL );
214 
215  // derive the SAT solver
216  pSat = Inter_ManDeriveSatSolver( p->pInter, p->pCnfInter, p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, p->vVarsAB, fUseBackward );
217  if ( pSat == NULL )
218  {
219  p->pInterNew = NULL;
220  return 1;
221  }
222 
223  // set runtime limit
224  if ( nTimeNewOut )
225  sat_solver_set_runtime_limit( pSat, nTimeNewOut );
226 
227  // collect global variables
228  pGlobalVars = ABC_CALLOC( int, sat_solver_nvars(pSat) );
229  Vec_IntForEachEntry( p->vVarsAB, Var, i )
230  pGlobalVars[Var] = 1;
231  pSat->pGlobalVars = fUseBias? pGlobalVars : NULL;
232 
233  // solve the problem
234 clk = Abc_Clock();
235  status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)p->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
236  p->nConfCur = pSat->stats.conflicts;
237 p->timeSat += Abc_Clock() - clk;
238 
239  pSat->pGlobalVars = NULL;
240  ABC_FREE( pGlobalVars );
241  if ( status == l_False )
242  {
243  pSatCnf = sat_solver_store_release( pSat );
244  RetValue = 1;
245  }
246  else if ( status == l_True )
247  {
248  RetValue = 0;
249  }
250  else
251  {
252  RetValue = -1;
253  }
254  sat_solver_delete( pSat );
255  if ( pSatCnf == NULL )
256  return RetValue;
257 
258  // create the resulting manager
259 clk = Abc_Clock();
260 /*
261  if ( !fUseIp )
262  {
263  pManInterA = Inta_ManAlloc();
264  p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 );
265  Inta_ManFree( pManInterA );
266  }
267  else
268  {
269  Aig_Man_t * pInterNew2;
270  int RetValue;
271 
272  pManInterA = Inta_ManAlloc();
273  p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 );
274 // Inter_ManVerifyInterpolant1( pManInterA, pSatCnf, p->pInterNew );
275  Inta_ManFree( pManInterA );
276 
277  pManInterB = Intb_ManAlloc();
278  pInterNew2 = Intb_ManInterpolate( pManInterB, pSatCnf, p->vVarsAB, 0 );
279  Inter_ManVerifyInterpolant2( pManInterB, pSatCnf, pInterNew2 );
280  Intb_ManFree( pManInterB );
281 
282  // check relationship
283  RetValue = Inter_ManCheckEquivalence( pInterNew2, p->pInterNew );
284  if ( RetValue )
285  printf( "Equivalence \"Ip == Im\" holds\n" );
286  else
287  {
288 // printf( "Equivalence \"Ip == Im\" does not hold\n" );
289  RetValue = Inter_ManCheckContainment( pInterNew2, p->pInterNew );
290  if ( RetValue )
291  printf( "Containment \"Ip -> Im\" holds\n" );
292  else
293  printf( "Containment \"Ip -> Im\" does not hold\n" );
294 
295  RetValue = Inter_ManCheckContainment( p->pInterNew, pInterNew2 );
296  if ( RetValue )
297  printf( "Containment \"Im -> Ip\" holds\n" );
298  else
299  printf( "Containment \"Im -> Ip\" does not hold\n" );
300  }
301 
302  Aig_ManStop( pInterNew2 );
303  }
304 */
305 
306  pManInterA = Inta_ManAlloc();
307  p->pInterNew = (Aig_Man_t *)Inta_ManInterpolate( pManInterA, (Sto_Man_t *)pSatCnf, nTimeNewOut, p->vVarsAB, 0 );
308  Inta_ManFree( pManInterA );
309 
310 p->timeInt += Abc_Clock() - clk;
311  Sto_ManFree( (Sto_Man_t *)pSatCnf );
312  if ( p->pInterNew == NULL )
313  RetValue = -1;
314  return RetValue;
315 }
static abctime sat_solver_set_runtime_limit(sat_solver *s, abctime Limit)
Definition: satSolver.h:233
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
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static Llb_Mgr_t * p
Definition: llb3Image.c:950
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
#define l_True
Definition: SolverTypes.h:84
static abctime Abc_Clock()
Definition: abc_global.h:279
int sat_solver_nvars(sat_solver *s)
Definition: satSolver.c:1896
if(last==0)
Definition: sparse_int.h:34
ABC_NAMESPACE_IMPL_START sat_solver * Inter_ManDeriveSatSolver(Aig_Man_t *pInter, Cnf_Dat_t *pCnfInter, Aig_Man_t *pAig, Cnf_Dat_t *pCnfAig, Aig_Man_t *pFrames, Cnf_Dat_t *pCnfFrames, Vec_Int_t *vVarsAB, int fUseBackward)
DECLARATIONS ///.
Definition: intM114.c:46
void Sto_ManFree(Sto_Man_t *p)
Definition: satStore.c:143
#define ABC_FREE(obj)
Definition: abc_global.h:232
void Inta_ManFree(Inta_Man_t *p)
Definition: satInterA.c:250
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
#define l_False
Definition: SolverTypes.h:85
int Var
Definition: SolverTypes.h:42
abctime timeSat
Definition: abcDar.c:3799
ABC_INT64_T abctime
Definition: abc_global.h:278
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54