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

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START Ssw_Sat_t * Ssw_SatStart (int fPolarFlip)
 DECLARATIONS ///.
 
void Ssw_SatStop (Ssw_Sat_t *p)
 
void Ssw_AddClausesMux (Ssw_Sat_t *p, Aig_Obj_t *pNode)
 
void Ssw_AddClausesSuper (Ssw_Sat_t *p, Aig_Obj_t *pNode, Vec_Ptr_t *vSuper)
 
void Ssw_CollectSuper_rec (Aig_Obj_t *pObj, Vec_Ptr_t *vSuper, int fFirst, int fUseMuxes)
 
void Ssw_CollectSuper (Aig_Obj_t *pObj, int fUseMuxes, Vec_Ptr_t *vSuper)
 
void Ssw_ObjAddToFrontier (Ssw_Sat_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vFrontier)
 
void Ssw_CnfNodeAddToSolver (Ssw_Sat_t *p, Aig_Obj_t *pObj)
 
int Ssw_CnfGetNodeValue (Ssw_Sat_t *p, Aig_Obj_t *pObj)
 

Function Documentation

◆ Ssw_AddClausesMux()

void Ssw_AddClausesMux ( Ssw_Sat_t * p,
Aig_Obj_t * pNode )

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

Synopsis [Addes clauses to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 104 of file sswCnf.c.

105{
106 Aig_Obj_t * pNodeI, * pNodeT, * pNodeE;
107 int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
108
109 assert( !Aig_IsComplement( pNode ) );
110 assert( Aig_ObjIsMuxType( pNode ) );
111 // get nodes (I = if, T = then, E = else)
112 pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
113 // get the variable numbers
114 VarF = Ssw_ObjSatNum(p,pNode);
115 VarI = Ssw_ObjSatNum(p,pNodeI);
116 VarT = Ssw_ObjSatNum(p,Aig_Regular(pNodeT));
117 VarE = Ssw_ObjSatNum(p,Aig_Regular(pNodeE));
118 // get the complementation flags
119 fCompT = Aig_IsComplement(pNodeT);
120 fCompE = Aig_IsComplement(pNodeE);
121
122 // f = ITE(i, t, e)
123
124 // i' + t' + f
125 // i' + t + f'
126 // i + e' + f
127 // i + e + f'
128
129 // create four clauses
130 pLits[0] = toLitCond(VarI, 1);
131 pLits[1] = toLitCond(VarT, 1^fCompT);
132 pLits[2] = toLitCond(VarF, 0);
133 if ( p->fPolarFlip )
134 {
135 if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
136 if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
137 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
138 }
139 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
140 assert( RetValue );
141 pLits[0] = toLitCond(VarI, 1);
142 pLits[1] = toLitCond(VarT, 0^fCompT);
143 pLits[2] = toLitCond(VarF, 1);
144 if ( p->fPolarFlip )
145 {
146 if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
147 if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
148 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
149 }
150 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
151 assert( RetValue );
152 pLits[0] = toLitCond(VarI, 0);
153 pLits[1] = toLitCond(VarE, 1^fCompE);
154 pLits[2] = toLitCond(VarF, 0);
155 if ( p->fPolarFlip )
156 {
157 if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
158 if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
159 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
160 }
161 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
162 assert( RetValue );
163 pLits[0] = toLitCond(VarI, 0);
164 pLits[1] = toLitCond(VarE, 0^fCompE);
165 pLits[2] = toLitCond(VarF, 1);
166 if ( p->fPolarFlip )
167 {
168 if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
169 if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
170 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
171 }
172 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
173 assert( RetValue );
174
175 // two additional clauses
176 // t' & e' -> f'
177 // t & e -> f
178
179 // t + e + f'
180 // t' + e' + f
181
182 if ( VarT == VarE )
183 {
184// assert( fCompT == !fCompE );
185 return;
186 }
187
188 pLits[0] = toLitCond(VarT, 0^fCompT);
189 pLits[1] = toLitCond(VarE, 0^fCompE);
190 pLits[2] = toLitCond(VarF, 1);
191 if ( p->fPolarFlip )
192 {
193 if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
194 if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
195 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
196 }
197 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
198 assert( RetValue );
199 pLits[0] = toLitCond(VarT, 1^fCompT);
200 pLits[1] = toLitCond(VarE, 1^fCompE);
201 pLits[2] = toLitCond(VarF, 0);
202 if ( p->fPolarFlip )
203 {
204 if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
205 if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
206 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
207 }
208 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
209 assert( RetValue );
210}
Aig_ObjRecognizeMux
Aig_Obj_t * Aig_ObjRecognizeMux(Aig_Obj_t *pObj, Aig_Obj_t **ppObjT, Aig_Obj_t **ppObjE)
Definition aigUtil.c:387
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Aig_ObjIsMuxType
int Aig_ObjIsMuxType(Aig_Obj_t *pObj)
Definition aigUtil.c:307
sat_solver_addclause
#define sat_solver_addclause
Definition cecSatG2.c:37
p
Cube * p
Definition exorList.c:222
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition aig.h:78
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:

◆ Ssw_AddClausesSuper()

void Ssw_AddClausesSuper ( Ssw_Sat_t * p,
Aig_Obj_t * pNode,
Vec_Ptr_t * vSuper )

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

Synopsis [Addes clauses to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 223 of file sswCnf.c.

224{
225 Aig_Obj_t * pFanin;
226 int * pLits, nLits, RetValue, i;
227 assert( !Aig_IsComplement(pNode) );
228 assert( Aig_ObjIsNode( pNode ) );
229 // create storage for literals
230 nLits = Vec_PtrSize(vSuper) + 1;
231 pLits = ABC_ALLOC( int, nLits );
232 // suppose AND-gate is A & B = C
233 // add !A => !C or A + !C
234 Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
235 {
236 pLits[0] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
237 pLits[1] = toLitCond(Ssw_ObjSatNum(p,pNode), 1);
238 if ( p->fPolarFlip )
239 {
240 if ( Aig_Regular(pFanin)->fPhase ) pLits[0] = lit_neg( pLits[0] );
241 if ( pNode->fPhase ) pLits[1] = lit_neg( pLits[1] );
242 }
243 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
244 assert( RetValue );
245 }
246 // add A & B => C or !A + !B + C
247 Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
248 {
249 pLits[i] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
250 if ( p->fPolarFlip )
251 {
252 if ( Aig_Regular(pFanin)->fPhase ) pLits[i] = lit_neg( pLits[i] );
253 }
254 }
255 pLits[nLits-1] = toLitCond(Ssw_ObjSatNum(p,pNode), 0);
256 if ( p->fPolarFlip )
257 {
258 if ( pNode->fPhase ) pLits[nLits-1] = lit_neg( pLits[nLits-1] );
259 }
260 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
261 assert( RetValue );
262 ABC_FREE( pLits );
263}
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Here is the caller graph for this function:

◆ Ssw_CnfGetNodeValue()

int Ssw_CnfGetNodeValue ( Ssw_Sat_t * p,
Aig_Obj_t * pObj )

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

Synopsis [Copy pattern from the solver into the internal storage.]

Description []

SideEffects []

SeeAlso []

Definition at line 402 of file sswCnf.c.

403{
404 int Value0, Value1, nVarNum;
405 assert( !Aig_IsComplement(pObj) );
406 nVarNum = Ssw_ObjSatNum( p, pObj );
407 if ( nVarNum > 0 )
408 return sat_solver_var_value( p->pSat, nVarNum );
409// if ( pObj->fMarkA == 1 )
410// return 0;
411 if ( Aig_ObjIsCi(pObj) )
412 return 0;
413 assert( Aig_ObjIsNode(pObj) );
414 Value0 = Ssw_CnfGetNodeValue( p, Aig_ObjFanin0(pObj) );
415 Value0 ^= Aig_ObjFaninC0(pObj);
416 Value1 = Ssw_CnfGetNodeValue( p, Aig_ObjFanin1(pObj) );
417 Value1 ^= Aig_ObjFaninC1(pObj);
418 return Value0 & Value1;
419}
Ssw_CnfGetNodeValue
int Ssw_CnfGetNodeValue(Ssw_Sat_t *p, Aig_Obj_t *pObj)
Definition sswCnf.c:402
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_CnfNodeAddToSolver()

void Ssw_CnfNodeAddToSolver ( Ssw_Sat_t * p,
Aig_Obj_t * pObj )

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

Synopsis [Updates the solver clause database.]

Description []

SideEffects []

SeeAlso []

Definition at line 351 of file sswCnf.c.

352{
353 Vec_Ptr_t * vFrontier;
354 Aig_Obj_t * pNode, * pFanin;
355 int i, k, fUseMuxes = 1;
356 // quit if CNF is ready
357 if ( Ssw_ObjSatNum(p,pObj) )
358 return;
359 // start the frontier
360 vFrontier = Vec_PtrAlloc( 100 );
361 Ssw_ObjAddToFrontier( p, pObj, vFrontier );
362 // explore nodes in the frontier
363 Vec_PtrForEachEntry( Aig_Obj_t *, vFrontier, pNode, i )
364 {
365 // create the supergate
366 assert( Ssw_ObjSatNum(p,pNode) );
367 if ( fUseMuxes && Aig_ObjIsMuxType(pNode) )
368 {
369 Vec_PtrClear( p->vFanins );
370 Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) );
371 Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
372 Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
373 Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
374 Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k )
375 Ssw_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
376 Ssw_AddClausesMux( p, pNode );
377 }
378 else
379 {
380 Ssw_CollectSuper( pNode, fUseMuxes, p->vFanins );
381 Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k )
382 Ssw_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
383 Ssw_AddClausesSuper( p, pNode, p->vFanins );
384 }
385 assert( Vec_PtrSize(p->vFanins) > 1 );
386 }
387 Vec_PtrFree( vFrontier );
388}
Ssw_CollectSuper
void Ssw_CollectSuper(Aig_Obj_t *pObj, int fUseMuxes, Vec_Ptr_t *vSuper)
Definition sswCnf.c:303
Ssw_AddClausesSuper
void Ssw_AddClausesSuper(Ssw_Sat_t *p, Aig_Obj_t *pNode, Vec_Ptr_t *vSuper)
Definition sswCnf.c:223
Ssw_ObjAddToFrontier
void Ssw_ObjAddToFrontier(Ssw_Sat_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vFrontier)
Definition sswCnf.c:322
Ssw_AddClausesMux
void Ssw_AddClausesMux(Ssw_Sat_t *p, Aig_Obj_t *pNode)
Definition sswCnf.c:104
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_CollectSuper()

void Ssw_CollectSuper ( Aig_Obj_t * pObj,
int fUseMuxes,
Vec_Ptr_t * vSuper )

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

Synopsis [Collects the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 303 of file sswCnf.c.

304{
305 assert( !Aig_IsComplement(pObj) );
306 assert( !Aig_ObjIsCi(pObj) );
307 Vec_PtrClear( vSuper );
308 Ssw_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
309}
Ssw_CollectSuper_rec
void Ssw_CollectSuper_rec(Aig_Obj_t *pObj, Vec_Ptr_t *vSuper, int fFirst, int fUseMuxes)
Definition sswCnf.c:276
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_CollectSuper_rec()

void Ssw_CollectSuper_rec ( Aig_Obj_t * pObj,
Vec_Ptr_t * vSuper,
int fFirst,
int fUseMuxes )

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

Synopsis [Collects the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 276 of file sswCnf.c.

277{
278 // if the new node is complemented or a PI, another gate begins
279 if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) ||
280 (!fFirst && Aig_ObjRefs(pObj) > 1) ||
281 (fUseMuxes && Aig_ObjIsMuxType(pObj)) )
282 {
283 Vec_PtrPushUnique( vSuper, pObj );
284 return;
285 }
286// pObj->fMarkA = 1;
287 // go through the branches
288 Ssw_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes );
289 Ssw_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes );
290}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_ObjAddToFrontier()

void Ssw_ObjAddToFrontier ( Ssw_Sat_t * p,
Aig_Obj_t * pObj,
Vec_Ptr_t * vFrontier )

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

Synopsis [Updates the solver clause database.]

Description []

SideEffects []

SeeAlso []

Definition at line 322 of file sswCnf.c.

323{
324 assert( !Aig_IsComplement(pObj) );
325 if ( Ssw_ObjSatNum(p,pObj) )
326 return;
327 assert( Ssw_ObjSatNum(p,pObj) == 0 );
328 if ( Aig_ObjIsConst1(pObj) )
329 return;
330// pObj->fMarkA = 1;
331 // save PIs (used by register correspondence)
332 if ( Aig_ObjIsCi(pObj) )
333 Vec_PtrPush( p->vUsedPis, pObj );
334 Ssw_ObjSetSatNum( p, pObj, p->nSatVars++ );
335 sat_solver_setnvars( p->pSat, 100 * (1 + p->nSatVars / 100) );
336 if ( Aig_ObjIsNode(pObj) )
337 Vec_PtrPush( vFrontier, pObj );
338}
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition satSolver.c:1272
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_SatStart()

ABC_NAMESPACE_IMPL_START Ssw_Sat_t * Ssw_SatStart ( int fPolarFlip)

DECLARATIONS ///.

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

FileName [sswCnf.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [Computation of CNF.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 1, 2008.]

Revision [

Id
sswCnf.c,v 1.00 2008/09/01 00:00:00 alanmi Exp

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

Synopsis [Starts the SAT manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file sswCnf.c.

46{
47 Ssw_Sat_t * p;
48 int Lit;
49 p = ABC_ALLOC( Ssw_Sat_t, 1 );
50 memset( p, 0, sizeof(Ssw_Sat_t) );
51 p->pAig = NULL;
52 p->fPolarFlip = fPolarFlip;
53 p->vSatVars = Vec_IntStart( 10000 );
54 p->vFanins = Vec_PtrAlloc( 100 );
55 p->vUsedPis = Vec_PtrAlloc( 100 );
56 p->pSat = sat_solver_new();
57 sat_solver_setnvars( p->pSat, 1000 );
58 // var 0 is not used
59 // var 1 is reserved for const1 node - add the clause
60 p->nSatVars = 1;
61 Lit = toLit( p->nSatVars );
62 if ( fPolarFlip )
63 Lit = lit_neg( Lit );
64 sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
65// Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ );
66 Vec_IntWriteEntry( p->vSatVars, 0, p->nSatVars++ );
67 return p;
68}
sat_solver_new
sat_solver * sat_solver_new(void)
Definition satSolver.c:1137
Ssw_Sat_t
struct Ssw_Sat_t_ Ssw_Sat_t
Definition sswInt.h:49
memset
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_SatStop()

void Ssw_SatStop ( Ssw_Sat_t * p)

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

Synopsis [Stop the SAT manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 81 of file sswCnf.c.

82{
83// Abc_Print( 1, "Recycling SAT solver with %d vars and %d restarts.\n",
84// p->pSat->size, p->pSat->stats.starts );
85 if ( p->pSat )
86 sat_solver_delete( p->pSat );
87 Vec_IntFree( p->vSatVars );
88 Vec_PtrFree( p->vFanins );
89 Vec_PtrFree( p->vUsedPis );
90 ABC_FREE( p );
91}
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition satSolver.c:1341
Here is the call graph for this function:
Here is the caller graph for this function: