ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
bmcEnum.c File Reference
#include "bmc.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"
Include dependency graph for bmcEnum.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START Gia_Man_t * Gia_ManDeriveOne (Gia_Man_t *p, Vec_Int_t *vValues)
 DECLARATIONS ///.
 
Gia_Man_t * Gia_ManDeriveOneTest2 (Gia_Man_t *p)
 
void Gia_ManDeriveOneTest (Gia_Man_t *p)
 

Function Documentation

◆ Gia_ManDeriveOne()

ABC_NAMESPACE_IMPL_START Gia_Man_t * Gia_ManDeriveOne ( Gia_Man_t * p,
Vec_Int_t * vValues )

DECLARATIONS ///.

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

FileName [bmcEnum.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based bounded model checking.]

Synopsis [Enumeration.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file bmcEnum.c.

48{
49 Gia_Man_t * pNew;
50 Gia_Obj_t * pObj; int i, fPhase0, fPhase1;
51 assert( Vec_IntSize(vValues) == Gia_ManCiNum(p) );
52 // propagate forward
53 Gia_ManForEachCi( p, pObj, i )
54 pObj->fPhase = Vec_IntEntry(vValues, i);
55 Gia_ManForEachAnd( p, pObj, i )
56 {
57 fPhase0 = Gia_ObjPhase(Gia_ObjFanin0(pObj)) ^ Gia_ObjFaninC0(pObj);
58 fPhase1 = Gia_ObjPhase(Gia_ObjFanin1(pObj)) ^ Gia_ObjFaninC1(pObj);
59 pObj->fPhase = fPhase0 & fPhase1;
60 }
61 // propagate backward
62 Gia_ManCleanMark0(p);
63 Gia_ManForEachCo( p, pObj, i )
64 Gia_ObjFanin0(pObj)->fMark0 = 1;
65 Gia_ManForEachAndReverse( p, pObj, i )
66 {
67 if ( !pObj->fMark0 )
68 continue;
69 fPhase0 = Gia_ObjPhase(Gia_ObjFanin0(pObj)) ^ Gia_ObjFaninC0(pObj);
70 fPhase1 = Gia_ObjPhase(Gia_ObjFanin1(pObj)) ^ Gia_ObjFaninC1(pObj);
71 if ( fPhase0 == fPhase1 )
72 {
73 assert( (int)pObj->fPhase == fPhase0 );
74 Gia_ObjFanin0(pObj)->fMark0 = 1;
75 Gia_ObjFanin1(pObj)->fMark0 = 1;
76 }
77 else if ( fPhase0 )
78 {
79 assert( fPhase1 == 0 );
80 assert( pObj->fPhase == 0 );
81 Gia_ObjFanin1(pObj)->fMark0 = 1;
82 }
83 else if ( fPhase1 )
84 {
85 assert( fPhase0 == 0 );
86 assert( pObj->fPhase == 0 );
87 Gia_ObjFanin0(pObj)->fMark0 = 1;
88 }
89 }
90 // create new
91 Gia_ManFillValue( p );
92 pNew = Gia_ManStart( Gia_ManObjNum(p) );
93 pNew->pName = Abc_UtilStrsav( p->pName );
94 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
95 Gia_ManConst0(p)->Value = 0;
96 Gia_ManForEachCi( p, pObj, i )
97 pObj->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), !Vec_IntEntry(vValues, i) );
98 Gia_ManForEachAnd( p, pObj, i )
99 {
100 if ( !pObj->fMark0 )
101 continue;
102 fPhase0 = Gia_ObjPhase(Gia_ObjFanin0(pObj)) ^ Gia_ObjFaninC0(pObj);
103 fPhase1 = Gia_ObjPhase(Gia_ObjFanin1(pObj)) ^ Gia_ObjFaninC1(pObj);
104 if ( fPhase0 == fPhase1 )
105 {
106 assert( (int)pObj->fPhase == fPhase0 );
107 if ( pObj->fPhase )
108 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
109 else
110 pObj->Value = Gia_ManAppendOr( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
111 }
112 else if ( fPhase0 )
113 {
114 assert( fPhase1 == 0 );
115 assert( pObj->fPhase == 0 );
116 pObj->Value = Gia_ObjFanin1(pObj)->Value;
117 }
118 else if ( fPhase1 )
119 {
120 assert( fPhase0 == 0 );
121 assert( pObj->fPhase == 0 );
122 pObj->Value = Gia_ObjFanin0(pObj)->Value;
123 }
124 }
125 Gia_ManForEachCo( p, pObj, i )
126 Gia_ManAppendCo( pNew, Gia_ObjFanin0(pObj)->Value );
127 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
128 Gia_ManCleanMark0(p);
129 return pNew;
130}
p
Cube * p
Definition exorList.c:222
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Gia_ManForEachAndReverse
#define Gia_ManForEachAndReverse(p, pObj, i)
Definition gia.h:1222
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition giaMan.c:764
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition giaUtil.c:369
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManCleanMark0
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition giaUtil.c:256
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition gia.h:1228
Gia_Man_t_::pSpec
char * pSpec
Definition gia.h:100
Gia_Man_t_::pName
char * pName
Definition gia.h:99
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
Gia_Obj_t_::fPhase
unsigned fPhase
Definition gia.h:87
Gia_Obj_t_::fMark0
unsigned fMark0
Definition gia.h:81
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:

◆ Gia_ManDeriveOneTest()

void Gia_ManDeriveOneTest ( Gia_Man_t * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 164 of file bmcEnum.c.

165{
166 int fVerbose = 1;
167 Gia_Man_t * pNew;
168 Gia_Obj_t * pObj, * pRoot;
169 Vec_Int_t * vValues = Vec_IntStart( Gia_ManCiNum(p) );
170 Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
171 int i, iVar, nIter, iPoVarBeg = pCnf->nVars - Gia_ManCiNum(p);
172 sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
173 Vec_Int_t * vLits = Vec_IntAlloc( 100 );
174 Vec_IntPush( vLits, Abc_Var2Lit( 1, 1 ) );
175 for ( nIter = 0; nIter < 10000; nIter++ )
176 {
177 int status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), 0, 0, 0, 0 );
178 if ( status == l_False )
179 break;
180 // derive new set
181 assert( status == l_True );
182 for ( i = 0; i < Gia_ManCiNum(p); i++ )
183 {
184 Vec_IntWriteEntry( vValues, i, sat_solver_var_value(pSat, iPoVarBeg+i) );
185 printf( "%d", sat_solver_var_value(pSat, iPoVarBeg+i) );
186 }
187 printf( " : " );
188
189 pNew = Gia_ManDeriveOne( p, vValues );
190 // assign variables
191 Gia_ManForEachCi( pNew, pObj, i )
192 pObj->Value = iPoVarBeg+i;
193 iVar = sat_solver_nvars(pSat);
194 Gia_ManForEachAnd( pNew, pObj, i )
195 pObj->Value = iVar++;
196 sat_solver_setnvars( pSat, iVar );
197 // create new clauses
198 Gia_ManForEachAnd( pNew, pObj, i )
199 sat_solver_add_and( pSat, pObj->Value, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
200 // add to the assumptions
201 pRoot = Gia_ManCo(pNew, 0);
202 Vec_IntPush( vLits, Abc_Var2Lit(Gia_ObjFanin0(pRoot)->Value, !Gia_ObjFaninC0(pRoot)) );
203 if ( fVerbose )
204 {
205 printf( "Iter = %5d : ", nIter );
206 printf( "And = %4d ", Gia_ManAndNum(pNew) );
207 printf( "\n" );
208 }
209 Gia_ManStop( pNew );
210 }
211 Vec_IntFree( vLits );
212 Vec_IntFree( vValues );
213 Cnf_DataFree( pCnf );
214 sat_solver_delete( pSat );
215}
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_False
#define l_False
Definition bmcBmcS.c:36
Gia_ManDeriveOne
ABC_NAMESPACE_IMPL_START Gia_Man_t * Gia_ManDeriveOne(Gia_Man_t *p, Vec_Int_t *vValues)
DECLARATIONS ///.
Definition bmcEnum.c:47
sat_solver_add_and
#define sat_solver_add_and
Definition cecSatG2.c:38
sat_solver
#define sat_solver
Definition cecSatG2.c:34
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
Cnf_Dat_t
struct Cnf_Dat_t_ Cnf_Dat_t
Definition cnf.h:52
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition cnfMan.c:207
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Mf_ManGenerateCnf
void * Mf_ManGenerateCnf(Gia_Man_t *pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fMapping, int fVerbose)
Definition giaMf.c:1877
Cnf_DataWriteIntoSolver
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition cnfMan.c:579
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition satSolver.c:1272
sat_solver_nvars
int sat_solver_nvars(sat_solver *s)
Definition satSolver.c:2369
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition satSolver.c:1341
Cnf_Dat_t_::nVars
int nVars
Definition cnf.h:59
Here is the call graph for this function:

◆ Gia_ManDeriveOneTest2()

Gia_Man_t * Gia_ManDeriveOneTest2 ( Gia_Man_t * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 143 of file bmcEnum.c.

144{
145 Gia_Man_t * pNew;
146 Vec_Int_t * vValues = Vec_IntStart( Gia_ManCiNum(p) );
147 //Vec_IntFill( vValues, Gia_ManCiNum(p), 1 );
148 pNew = Gia_ManDeriveOne( p, vValues );
149 Vec_IntFree( vValues );
150 return pNew;
151}
Here is the call graph for this function: