ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
pdrSat.c File Reference
#include "pdrInt.h"
Include dependency graph for pdrSat.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START sat_solver * Pdr_ManCreateSolver (Pdr_Man_t *p, int k)
 DECLARATIONS ///.
 
sat_solver * Pdr_ManFetchSolver (Pdr_Man_t *p, int k)
 
Vec_Int_t * Pdr_ManLitsToCube (Pdr_Man_t *p, int k, int *pArray, int nArray)
 
Vec_Int_t * Pdr_ManCubeToLits (Pdr_Man_t *p, int k, Pdr_Set_t *pCube, int fCompl, int fNext)
 
void Pdr_ManSetPropertyOutput (Pdr_Man_t *p, int k)
 
void Pdr_ManSolverAddClause (Pdr_Man_t *p, int k, Pdr_Set_t *pCube)
 
void Pdr_ManCollectValues (Pdr_Man_t *p, int k, Vec_Int_t *vObjIds, Vec_Int_t *vValues)
 
int Pdr_ManCheckCubeCs (Pdr_Man_t *p, int k, Pdr_Set_t *pCube)
 
int Pdr_ManCheckCube (Pdr_Man_t *p, int k, Pdr_Set_t *pCube, Pdr_Set_t **ppPred, int nConfLimit, int fTryConf, int fUseLit)
 

Function Documentation

◆ Pdr_ManCheckCube()

int Pdr_ManCheckCube ( Pdr_Man_t * p,
int k,
Pdr_Set_t * pCube,
Pdr_Set_t ** ppPred,
int nConfLimit,
int fTryConf,
int fUseLit )

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

Synopsis [Checks if the cube holds (UNSAT) in the given timeframe.]

Description [Return 1/0 if cube or property are proved to hold/fail in k-th timeframe. Returns the predecessor bad state in ppPred.]

SideEffects []

SeeAlso []

Definition at line 290 of file pdrSat.c.

291{
292 //int fUseLit = 0;
293 int fLitUsed = 0;
294 sat_solver * pSat;
295 Vec_Int_t * vLits;
296 int Lit, RetValue;
297 abctime clk, Limit;
298 p->nCalls++;
299 pSat = Pdr_ManFetchSolver( p, k );
300 if ( pCube == NULL ) // solve the property
301 {
302 clk = Abc_Clock();
303 Lit = Abc_Var2Lit( Pdr_ObjSatVar(p, k, 2, Aig_ManCo(p->pAig, p->iOutCur)), 0 ); // pos literal (property fails)
304 Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
305 RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 );
306 sat_solver_set_runtime_limit( pSat, Limit );
307 if ( RetValue == l_Undef )
308 return -1;
309 }
310 else // check relative containment in terms of next states
311 {
312 if ( fUseLit )
313 {
314 fLitUsed = 1;
315 Vec_IntAddToEntry( p->vActVars, k, 1 );
316 // add the cube in terms of current state variables
317 vLits = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
318 // add activation literal
319 Lit = Abc_Var2Lit( Pdr_ManFreeVar(p, k), 0 );
320 // add activation literal
321 Vec_IntPush( vLits, Lit );
322 RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
323 assert( RetValue == 1 );
324 sat_solver_compress( pSat );
325 // create assumptions
326 vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
327 // add activation literal
328 Vec_IntPush( vLits, Abc_LitNot(Lit) );
329 }
330 else
331 vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
332
333 // solve
334 clk = Abc_Clock();
335 Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
336 RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), fTryConf ? p->pPars->nConfGenLimit : nConfLimit, 0, 0, 0 );
337 sat_solver_set_runtime_limit( pSat, Limit );
338 if ( RetValue == l_Undef )
339 {
340 if ( fTryConf && p->pPars->nConfGenLimit )
341 RetValue = l_True;
342 else
343 return -1;
344 }
345 }
346 clk = Abc_Clock() - clk;
347 p->tSat += clk;
348 assert( RetValue != l_Undef );
349 if ( RetValue == l_False )
350 {
351 p->tSatUnsat += clk;
352 p->nCallsU++;
353 if ( ppPred )
354 *ppPred = NULL;
355 RetValue = 1;
356 }
357 else // if ( RetValue == l_True )
358 {
359 p->tSatSat += clk;
360 p->nCallsS++;
361 if ( ppPred )
362 {
363 abctime clk = Abc_Clock();
364 if ( p->pPars->fNewXSim )
365 *ppPred = Txs3_ManTernarySim( p->pTxs3, k, pCube );
366 else
367 *ppPred = Pdr_ManTernarySim( p, k, pCube );
368 p->tTsim += Abc_Clock() - clk;
369 p->nXsimLits += (*ppPred)->nLits;
370 p->nXsimRuns++;
371 }
372 RetValue = 0;
373 }
374
375/* // for some reason, it does not work...
376 if ( fLitUsed )
377 {
378 int RetValue;
379 Lit = Abc_LitNot(Lit);
380 RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
381 assert( RetValue == 1 );
382 sat_solver_compress( pSat );
383 }
384*/
385 return RetValue;
386}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
l_True
#define l_True
Definition bmcBmcS.c:35
l_Undef
#define l_Undef
Definition bmcBmcS.c:34
l_False
#define l_False
Definition bmcBmcS.c:36
sat_solver_addclause
#define sat_solver_addclause
Definition cecSatG2.c:37
sat_solver
#define sat_solver
Definition cecSatG2.c:34
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
p
Cube * p
Definition exorList.c:222
Pdr_ManFreeVar
int Pdr_ManFreeVar(Pdr_Man_t *p, int k)
Definition pdrCnf.c:332
Pdr_ObjSatVar
int Pdr_ObjSatVar(Pdr_Man_t *p, int k, int Pol, Aig_Obj_t *pObj)
FUNCTION DECLARATIONS ///.
Definition pdrCnf.c:241
Txs3_ManTernarySim
Pdr_Set_t * Txs3_ManTernarySim(Txs3_Man_t *p, int k, Pdr_Set_t *pCube)
Definition pdrTsim3.c:188
Pdr_ManTernarySim
Pdr_Set_t * Pdr_ManTernarySim(Pdr_Man_t *p, int k, Pdr_Set_t *pCube)
Definition pdrTsim.c:351
Pdr_ManFetchSolver
sat_solver * Pdr_ManFetchSolver(Pdr_Man_t *p, int k)
Definition pdrSat.c:77
Pdr_ManCubeToLits
Vec_Int_t * Pdr_ManCubeToLits(Pdr_Man_t *p, int k, Pdr_Set_t *pCube, int fCompl, int fNext)
Definition pdrSat.c:144
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Pdr_ManCheckCubeCs()

int Pdr_ManCheckCubeCs ( Pdr_Man_t * p,
int k,
Pdr_Set_t * pCube )

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

Synopsis [Checks if the cube holds (UNSAT) in the given timeframe.]

Description [Return 1/0 if cube or property are proved to hold/fail in k-th timeframe. Returns the predecessor bad state in ppPred.]

SideEffects []

SeeAlso []

Definition at line 262 of file pdrSat.c.

263{
264 sat_solver * pSat;
265 Vec_Int_t * vLits;
266 abctime Limit;
267 int RetValue;
268 pSat = Pdr_ManFetchSolver( p, k );
269 vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 0 );
270 Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
271 RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
272 sat_solver_set_runtime_limit( pSat, Limit );
273 if ( RetValue == l_Undef )
274 return -1;
275 return (RetValue == l_False);
276}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Pdr_ManCollectValues()

void Pdr_ManCollectValues ( Pdr_Man_t * p,
int k,
Vec_Int_t * vObjIds,
Vec_Int_t * vValues )

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

Synopsis [Collects values of the RO/RI variables in k-th SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 236 of file pdrSat.c.

237{
238 sat_solver * pSat;
239 Aig_Obj_t * pObj;
240 int iVar, i;
241 Vec_IntClear( vValues );
242 pSat = Pdr_ManSolver(p, k);
243 Aig_ManForEachObjVec( vObjIds, p->pAig, pObj, i )
244 {
245 iVar = Pdr_ObjSatVar( p, k, 3, pObj ); assert( iVar >= 0 );
246 Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
247 }
248}
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Aig_ManForEachObjVec
#define Aig_ManForEachObjVec(vIds, p, pObj, i)
Definition aig.h:408
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Pdr_ManCreateSolver()

ABC_NAMESPACE_IMPL_START sat_solver * Pdr_ManCreateSolver ( Pdr_Man_t * p,
int k )

DECLARATIONS ///.

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

FileName [pdrSat.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Property driven reachability.]

Synopsis [SAT solver procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - November 20, 2010.]

Revision [

Id
pdrSat.c,v 1.00 2010/11/20 00:00:00 alanmi Exp

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

Synopsis [Creates new SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file pdrSat.c.

46{
47 sat_solver * pSat;
48 Aig_Obj_t * pObj;
49 int i;
50 assert( Vec_PtrSize(p->vSolvers) == k );
51 assert( Vec_VecSize(p->vClauses) == k );
52 assert( Vec_IntSize(p->vActVars) == k );
53 // create new solver
54// pSat = sat_solver_new();
55 pSat = zsat_solver_new_seed(p->pPars->nRandomSeed);
56 pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
57 Vec_PtrPush( p->vSolvers, pSat );
58 Vec_VecExpand( p->vClauses, k );
59 Vec_IntPush( p->vActVars, 0 );
60 // add property cone
61 Saig_ManForEachPo( p->pAig, pObj, i )
62 Pdr_ObjSatVar( p, k, 1, pObj );
63 return pSat;
64}
Pdr_ManNewSolver
sat_solver * Pdr_ManNewSolver(sat_solver *pSat, Pdr_Man_t *p, int k, int fInit)
Definition pdrCnf.c:439
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition saig.h:93
zsat_solver_new_seed
sat_solver * zsat_solver_new_seed(double seed)
Definition satSolver.c:1202
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Pdr_ManCubeToLits()

Vec_Int_t * Pdr_ManCubeToLits ( Pdr_Man_t * p,
int k,
Pdr_Set_t * pCube,
int fCompl,
int fNext )

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

Synopsis [Converts the cube in terms of RO numbers into array of CNF literals.]

Description []

SideEffects []

SeeAlso []

Definition at line 144 of file pdrSat.c.

145{
146 Aig_Obj_t * pObj;
147 int i, iVar, iVarMax = 0;
148 abctime clk = Abc_Clock();
149 Vec_IntClear( p->vLits );
150// assert( !(fNext && fCompl) );
151 for ( i = 0; i < pCube->nLits; i++ )
152 {
153 if ( pCube->Lits[i] == -1 )
154 continue;
155 if ( fNext )
156 pObj = Saig_ManLi( p->pAig, Abc_Lit2Var(pCube->Lits[i]) );
157 else
158 pObj = Saig_ManLo( p->pAig, Abc_Lit2Var(pCube->Lits[i]) );
159 iVar = Pdr_ObjSatVar( p, k, fNext ? 2 - Abc_LitIsCompl(pCube->Lits[i]) : 3, pObj ); assert( iVar >= 0 );
160 iVarMax = Abc_MaxInt( iVarMax, iVar );
161 Vec_IntPush( p->vLits, Abc_Var2Lit( iVar, fCompl ^ Abc_LitIsCompl(pCube->Lits[i]) ) );
162 }
163// sat_solver_setnvars( Pdr_ManSolver(p, k), iVarMax + 1 );
164 p->tCnf += Abc_Clock() - clk;
165 return p->vLits;
166}
Pdr_Set_t_::Lits
int Lits[0]
Definition pdrInt.h:81
Pdr_Set_t_::nLits
int nLits
Definition pdrInt.h:80
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Pdr_ManFetchSolver()

sat_solver * Pdr_ManFetchSolver ( Pdr_Man_t * p,
int k )

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

Synopsis [Returns old or restarted solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 77 of file pdrSat.c.

78{
79 sat_solver * pSat;
80 Vec_Ptr_t * vArrayK;
81 Pdr_Set_t * pCube;
82 int i, j;
83 pSat = Pdr_ManSolver(p, k);
84 if ( Vec_IntEntry(p->vActVars, k) < p->pPars->nRecycle )
85 return pSat;
86 assert( k < Vec_PtrSize(p->vSolvers) - 1 );
87 p->nStarts++;
88// sat_solver_delete( pSat );
89// pSat = sat_solver_new();
90// sat_solver_restart( pSat );
91 zsat_solver_restart_seed( pSat, p->pPars->nRandomSeed );
92 // create new SAT solver
93 pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
94 // write new SAT solver
95 Vec_PtrWriteEntry( p->vSolvers, k, pSat );
96 Vec_IntWriteEntry( p->vActVars, k, 0 );
97 // set the property output
98 Pdr_ManSetPropertyOutput( p, k );
99 // add the clauses
100 Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, k )
101 Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j )
102 Pdr_ManSolverAddClause( p, k, pCube );
103 return pSat;
104}
Pdr_Set_t
struct Pdr_Set_t_ Pdr_Set_t
Definition pdrInt.h:74
Pdr_ManSetPropertyOutput
void Pdr_ManSetPropertyOutput(Pdr_Man_t *p, int k)
Definition pdrSat.c:179
Pdr_ManSolverAddClause
void Pdr_ManSolverAddClause(Pdr_Man_t *p, int k, Pdr_Set_t *pCube)
Definition pdrSat.c:213
zsat_solver_restart_seed
void zsat_solver_restart_seed(sat_solver *s, double seed)
Definition satSolver.c:1435
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Vec_VecForEachLevelStart
#define Vec_VecForEachLevelStart(vGlob, vVec, i, LevelStart)
Definition vecVec.h:57
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Pdr_ManLitsToCube()

Vec_Int_t * Pdr_ManLitsToCube ( Pdr_Man_t * p,
int k,
int * pArray,
int nArray )

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

Synopsis [Converts SAT variables into register IDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 117 of file pdrSat.c.

118{
119 int i, RegId;
120 Vec_IntClear( p->vLits );
121 for ( i = 0; i < nArray; i++ )
122 {
123 RegId = Pdr_ObjRegNum( p, k, Abc_Lit2Var(pArray[i]) );
124 if ( RegId == -1 )
125 continue;
126 assert( RegId >= 0 && RegId < Aig_ManRegNum(p->pAig) );
127 Vec_IntPush( p->vLits, Abc_Var2Lit(RegId, !Abc_LitIsCompl(pArray[i])) );
128 }
129 assert( Vec_IntSize(p->vLits) >= 0 && Vec_IntSize(p->vLits) <= nArray );
130 return p->vLits;
131}
Pdr_ObjRegNum
int Pdr_ObjRegNum(Pdr_Man_t *p, int k, int iSatVar)
Definition pdrCnf.c:312
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Pdr_ManSetPropertyOutput()

void Pdr_ManSetPropertyOutput ( Pdr_Man_t * p,
int k )

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

Synopsis [Sets the property output to 0 (sat) forever.]

Description []

SideEffects []

SeeAlso []

Definition at line 179 of file pdrSat.c.

180{
181 sat_solver * pSat;
182 Aig_Obj_t * pObj;
183 int Lit, RetValue, i;
184 if ( !p->pPars->fUsePropOut )
185 return;
186 pSat = Pdr_ManSolver(p, k);
187 Saig_ManForEachPo( p->pAig, pObj, i )
188 {
189 // skip solved outputs
190 if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
191 continue;
192 // skip timedout outputs
193 if ( p->pPars->vOutMap && Vec_IntEntry(p->pPars->vOutMap, i) == -1 )
194 continue;
195 Lit = Abc_Var2Lit( Pdr_ObjSatVar(p, k, 1, pObj), 1 ); // neg literal
196 RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
197 assert( RetValue == 1 );
198 }
199 sat_solver_compress( pSat );
200}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Pdr_ManSolverAddClause()

void Pdr_ManSolverAddClause ( Pdr_Man_t * p,
int k,
Pdr_Set_t * pCube )

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

Synopsis [Adds one clause in terms of ROs to the k-th SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 213 of file pdrSat.c.

214{
215 sat_solver * pSat;
216 Vec_Int_t * vLits;
217 int RetValue;
218 pSat = Pdr_ManSolver(p, k);
219 vLits = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
220 RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
221 assert( RetValue == 1 );
222 sat_solver_compress( pSat );
223}
Here is the call graph for this function:
Here is the caller graph for this function: