abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
giaQbf.c File Reference
#include "gia.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "misc/extra/extra.h"

Go to the source code of this file.

Data Structures

struct  Qbf_Man_t_
 

Typedefs

typedef
typedefABC_NAMESPACE_IMPL_START
struct Qbf_Man_t_ 
Qbf_Man_t
 DECLARATIONS ///. More...
 

Functions

Cnf_Dat_tMf_ManGenerateCnf (Gia_Man_t *pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose)
 
int Gia_ManSatEnum (Gia_Man_t *pGia, int nConfLimit, int nTimeOut, int fVerbose)
 FUNCTION DEFINITIONS ///. More...
 
void Gia_QbfDumpFile (Gia_Man_t *pGia, int nPars)
 
Qbf_Man_tGia_QbfAlloc (Gia_Man_t *pGia, int nPars, int fVerbose)
 
void Gia_QbfFree (Qbf_Man_t *p)
 
Gia_Man_tGia_QbfQuantify (Gia_Man_t *p, int nPars)
 
Gia_Man_tGia_QbfCofactor (Gia_Man_t *p, int nPars, Vec_Int_t *vValues, Vec_Int_t *vParMap)
 
int Gia_QbfAddCofactor (Qbf_Man_t *p, Gia_Man_t *pCof)
 
void Gia_QbfOnePattern (Qbf_Man_t *p, Vec_Int_t *vValues)
 
void Gia_QbfPrint (Qbf_Man_t *p, Vec_Int_t *vValues, int Iter)
 
int Gia_QbfVerify (Qbf_Man_t *p, Vec_Int_t *vValues)
 
void Gia_QbfAddSpecialConstr (Qbf_Man_t *p)
 
void Gia_QbfLearnConstraint (Qbf_Man_t *p, Vec_Int_t *vValues)
 
int Gia_QbfSolve (Gia_Man_t *pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int fVerbose)
 

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Qbf_Man_t_ Qbf_Man_t

DECLARATIONS ///.

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

FileName [giaQbf.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis [QBF solver.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - October 18, 2014.]

Revision [

Id:
giaQbf.c,v 1.00 2014/10/18 00:00:00 alanmi Exp

]

Definition at line 33 of file giaQbf.c.

Function Documentation

int Gia_ManSatEnum ( Gia_Man_t pGia,
int  nConfLimit,
int  nTimeOut,
int  fVerbose 
)

FUNCTION DEFINITIONS ///.

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

Synopsis [Naive way to enumerate SAT assignments.]

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file giaQbf.c.

69 {
70  Cnf_Dat_t * pCnf;
71  sat_solver * pSat;
72  Vec_Int_t * vLits;
73  int i, iLit, iParVarBeg, Iter;
74  int nSolutions = 0, RetValue = 0;
75  abctime clkStart = Abc_Clock();
76  pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 );
77  pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
78  iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia) - 1;
79  Cnf_DataFree( pCnf );
80  // iterate through the SAT assignment
81  vLits = Vec_IntAlloc( Gia_ManPiNum(pGia) );
82  for ( Iter = 1 ; ; Iter++ )
83  {
84  int status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, 0, 0 );
85  if ( status == l_False ) { RetValue = 1; break; }
86  if ( status == l_Undef ) { RetValue = 0; break; }
87  nSolutions++;
88  // extract SAT assignment
89  Vec_IntClear( vLits );
90  for ( i = 0; i < Gia_ManPiNum(pGia); i++ )
91  Vec_IntPush( vLits, Abc_Var2Lit(iParVarBeg+i, sat_solver_var_value(pSat, iParVarBeg+i)) );
92  if ( fVerbose )
93  {
94  printf( "%5d : ", Iter );
95  Vec_IntForEachEntry( vLits, iLit, i )
96  printf( "%d", !Abc_LitIsCompl(iLit) );
97  printf( "\n" );
98  }
99  // add clause
100  if ( !sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ) )
101  { RetValue = 1; break; }
102  if ( nTimeOut && (Abc_Clock() - clkStart)/CLOCKS_PER_SEC >= nTimeOut ) { RetValue = 0; break; }
103  }
104  sat_solver_delete( pSat );
105  Vec_IntFree( vLits );
106  if ( nTimeOut && (Abc_Clock() - clkStart)/CLOCKS_PER_SEC >= nTimeOut )
107  printf( "Enumerated %d assignments when timeout (%d sec) was reached. ", nSolutions, nTimeOut );
108  else if ( nConfLimit && !RetValue )
109  printf( "Enumerated %d assignments when conflict limit (%d) was reached. ", nSolutions, nConfLimit );
110  else
111  printf( "Enumerated the complete set of %d assignments. ", nSolutions );
112  Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
113  return RetValue;
114 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
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
#define l_Undef
Definition: SolverTypes.h:86
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
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
static abctime Abc_Clock()
Definition: abc_global.h:279
Definition: cnf.h:56
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
if(last==0)
Definition: sparse_int.h:34
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Cnf_Dat_t * Mf_ManGenerateCnf(Gia_Man_t *pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose)
Definition: giaMf.c:1629
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition: cnfMan.c:463
#define l_False
Definition: SolverTypes.h:85
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
ABC_INT64_T abctime
Definition: abc_global.h:278
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
int Gia_QbfAddCofactor ( Qbf_Man_t p,
Gia_Man_t pCof 
)

Definition at line 280 of file giaQbf.c.

281 {
282  Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pCof, 8, 0, 1, 0 );
283  int i, iFirstVar = sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof) - 1;
284  pCnf->pMan = NULL;
285  Cnf_DataLift( pCnf, sat_solver_nvars(p->pSatSyn) );
286  for ( i = 0; i < pCnf->nClauses; i++ )
287  if ( !sat_solver_addclause( p->pSatSyn, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
288  {
289  Cnf_DataFree( pCnf );
290  return 0;
291  }
292  Cnf_DataFree( pCnf );
293  // add connection clauses
294  for ( i = 0; i < Gia_ManPiNum(p->pGia); i++ )
295  if ( !sat_solver_add_buffer( p->pSatSyn, i, iFirstVar+i, 0 ) )
296  return 0;
297  return 1;
298 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
int nClauses
Definition: cnf.h:61
int nVars
Definition: cnf.h:59
Aig_Man_t * pMan
Definition: cnf.h:58
Definition: cnf.h:56
static int sat_solver_add_buffer(sat_solver *pSat, int iVarA, int iVarB, int fCompl)
Definition: satSolver.h:288
int ** pClauses
Definition: cnf.h:62
int sat_solver_nvars(sat_solver *s)
Definition: satSolver.c:1896
Cnf_Dat_t * Mf_ManGenerateCnf(Gia_Man_t *pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose)
Definition: giaMf.c:1629
void Cnf_DataLift(Cnf_Dat_t *p, int nVarsPlus)
Definition: cnfMan.c:205
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
void Gia_QbfAddSpecialConstr ( Qbf_Man_t p)

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

Synopsis [Constraint learning.]

Description []

SideEffects []

SeeAlso []

Definition at line 368 of file giaQbf.c.

369 {
370  int i, status, Lits[2];
371  for ( i = 0; i < 4*11; i++ )
372  if ( i % 4 == 0 )
373  {
374  assert( Vec_IntEntry(p->vParMap, i) == -1 );
375  Vec_IntWriteEntry( p->vParMap, i, (i % 4) == 3 );
376  Lits[0] = Abc_Var2Lit( i, (i % 4) != 3 );
377  status = sat_solver_addclause( p->pSatSyn, Lits, Lits+1 );
378  assert( status );
379  }
380 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
#define assert(ex)
Definition: util_old.h:213
Qbf_Man_t* Gia_QbfAlloc ( Gia_Man_t pGia,
int  nPars,
int  fVerbose 
)

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

Synopsis [Generate one SAT assignment of the problem.]

Description []

SideEffects []

SeeAlso []

Definition at line 170 of file giaQbf.c.

171 {
172  Qbf_Man_t * p;
173  Cnf_Dat_t * pCnf;
174  Gia_ObjFlipFaninC0( Gia_ManPo(pGia, 0) );
175  pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 );
176  Gia_ObjFlipFaninC0( Gia_ManPo(pGia, 0) );
177  p = ABC_CALLOC( Qbf_Man_t, 1 );
178  p->clkStart = Abc_Clock();
179  p->pGia = pGia;
180  p->nPars = nPars;
181  p->nVars = Gia_ManPiNum(pGia) - nPars;
182  p->fVerbose = fVerbose;
183  p->iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia) - 1;
184  p->pSatVer = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
185  p->pSatSyn = sat_solver_new();
186  p->vValues = Vec_IntAlloc( Gia_ManPiNum(pGia) );
187  p->vParMap = Vec_IntStartFull( nPars );
188  p->vLits = Vec_IntAlloc( nPars );
189  sat_solver_setnvars( p->pSatSyn, nPars );
190  Cnf_DataFree( pCnf );
191  return p;
192 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static Gia_Obj_t * Gia_ManPo(Gia_Man_t *p, int v)
Definition: gia.h:406
int nVars
Definition: cnf.h:59
static abctime Abc_Clock()
Definition: abc_global.h:279
Definition: cnf.h:56
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static void Gia_ObjFlipFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:472
typedefABC_NAMESPACE_IMPL_START struct Qbf_Man_t_ Qbf_Man_t
DECLARATIONS ///.
Definition: giaQbf.c:33
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
Cnf_Dat_t * Mf_ManGenerateCnf(Gia_Man_t *pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose)
Definition: giaMf.c:1629
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition: cnfMan.c:463
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Gia_Man_t* Gia_QbfCofactor ( Gia_Man_t p,
int  nPars,
Vec_Int_t vValues,
Vec_Int_t vParMap 
)

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

Synopsis [Create and add one cofactor.]

Description []

SideEffects []

SeeAlso []

Definition at line 253 of file giaQbf.c.

254 {
255  Gia_Man_t * pNew, * pTemp;
256  Gia_Obj_t * pObj; int i;
257  assert( Gia_ManPiNum(p) == nPars + Vec_IntSize(vValues) );
258  pNew = Gia_ManStart( Gia_ManObjNum(p) );
259  pNew->pName = Abc_UtilStrsav( p->pName );
260  Gia_ManHashAlloc( pNew );
261  Gia_ManConst0(p)->Value = 0;
262  Gia_ManForEachPi( p, pObj, i )
263  if ( i < nPars )
264  {
265  pObj->Value = Gia_ManAppendCi(pNew);
266  if ( Vec_IntEntry(vParMap, i) != -1 )
267  pObj->Value = Vec_IntEntry(vParMap, i);
268  }
269  else
270  pObj->Value = Vec_IntEntry(vValues, i - nPars);
271  Gia_ManForEachAnd( p, pObj, i )
272  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
273  Gia_ManForEachCo( p, pObj, i )
274  pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
275  pNew = Gia_ManCleanup( pTemp = pNew );
276  Gia_ManStop( pTemp );
277  assert( Gia_ManPiNum(pNew) == nPars );
278  return pNew;
279 }
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Definition: gia.h:75
char * pName
Definition: gia.h:97
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
if(last==0)
Definition: sparse_int.h:34
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Definition: gia.h:95
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
#define assert(ex)
Definition: util_old.h:213
unsigned Value
Definition: gia.h:87
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
void Gia_QbfDumpFile ( Gia_Man_t pGia,
int  nPars 
)

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

Synopsis [Dumps the original problem in QDIMACS format.]

Description []

SideEffects []

SeeAlso []

Definition at line 127 of file giaQbf.c.

128 {
129  // original problem: \exists p \forall x \exists y. M(p,x,y)
130  // negated problem: \forall p \exists x \exists y. !M(p,x,y)
131  Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 );
132  Vec_Int_t * vVarMap, * vForAlls, * vExists;
133  Gia_Obj_t * pObj;
134  char * pFileName;
135  int i, Entry;
136  // create var map
137  vVarMap = Vec_IntStart( pCnf->nVars );
138  Gia_ManForEachCi( pGia, pObj, i )
139  if ( i < nPars )
140  Vec_IntWriteEntry( vVarMap, pCnf->pVarNums[Gia_ManCiIdToId(pGia, i)], 1 );
141  // create various maps
142  vForAlls = Vec_IntAlloc( nPars );
143  vExists = Vec_IntAlloc( Gia_ManCiNum(pGia) - nPars );
144  Vec_IntForEachEntry( vVarMap, Entry, i )
145  if ( Entry )
146  Vec_IntPush( vForAlls, i );
147  else
148  Vec_IntPush( vExists, i );
149  // generate CNF
150  pFileName = Extra_FileNameGenericAppend( pGia->pSpec, ".qdimacs" );
151  Cnf_DataWriteIntoFile( pCnf, pFileName, 0, vForAlls, vExists );
152  Cnf_DataFree( pCnf );
153  Vec_IntFree( vForAlls );
154  Vec_IntFree( vExists );
155  Vec_IntFree( vVarMap );
156  printf( "The 2QBF formula was written into file \"%s\".\n", pFileName );
157 }
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
void Cnf_DataWriteIntoFile(Cnf_Dat_t *p, char *pFileName, int fReadable, Vec_Int_t *vForAlls, Vec_Int_t *vExists)
Definition: cnfMan.c:318
int nVars
Definition: cnf.h:59
Definition: cnf.h:56
Definition: gia.h:75
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
if(last==0)
Definition: sparse_int.h:34
else
Definition: sparse_int.h:55
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Cnf_Dat_t * Mf_ManGenerateCnf(Gia_Man_t *pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose)
Definition: giaMf.c:1629
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
char * Extra_FileNameGenericAppend(char *pBase, char *pSuffix)
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
static int Gia_ManCiIdToId(Gia_Man_t *p, int CiId)
Definition: gia.h:438
void Gia_QbfFree ( Qbf_Man_t p)

Definition at line 193 of file giaQbf.c.

194 {
195  sat_solver_delete( p->pSatVer );
196  sat_solver_delete( p->pSatSyn );
197  Vec_IntFree( p->vLits );
198  Vec_IntFree( p->vValues );
199  Vec_IntFree( p->vParMap );
200  ABC_FREE( p );
201 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
#define ABC_FREE(obj)
Definition: abc_global.h:232
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
void Gia_QbfLearnConstraint ( Qbf_Man_t p,
Vec_Int_t vValues 
)

Definition at line 381 of file giaQbf.c.

382 {
383  int i, status, Entry, Lits[2];
384  assert( Vec_IntSize(vValues) == p->nPars );
385  printf( " Pattern " );
386  Vec_IntPrintBinary( vValues );
387  printf( "\n" );
388  Vec_IntForEachEntry( vValues, Entry, i )
389  {
390  Lits[0] = Abc_Var2Lit( i, Entry );
391  status = sat_solver_solve( p->pSatSyn, Lits, Lits+1, 0, 0, 0, 0 );
392  printf( " Var =%4d ", i );
393  if ( status != l_True )
394  {
395  printf( "UNSAT\n" );
396  Lits[0] = Abc_LitNot(Lits[0]);
397  status = sat_solver_addclause( p->pSatSyn, Lits, Lits+1 );
398  assert( status );
399  continue;
400  }
401  Gia_QbfOnePattern( p, p->vLits );
402  Vec_IntPrintBinary( p->vLits );
403  printf( "\n" );
404  }
405  assert( Vec_IntSize(vValues) == p->nPars );
406 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Gia_QbfOnePattern(Qbf_Man_t *p, Vec_Int_t *vValues)
Definition: giaQbf.c:311
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
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
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
#define l_True
Definition: SolverTypes.h:84
static void Vec_IntPrintBinary(Vec_Int_t *vVec)
Definition: vecInt.h:1811
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define assert(ex)
Definition: util_old.h:213
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
void Gia_QbfOnePattern ( Qbf_Man_t p,
Vec_Int_t vValues 
)

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

Synopsis [Extract SAT assignment.]

Description []

SideEffects []

SeeAlso []

Definition at line 311 of file giaQbf.c.

312 {
313  int i;
314  Vec_IntClear( vValues );
315  for ( i = 0; i < p->nPars; i++ )
316  Vec_IntPush( vValues, sat_solver_var_value(p->pSatSyn, i) );
317 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
void Gia_QbfPrint ( Qbf_Man_t p,
Vec_Int_t vValues,
int  Iter 
)

Definition at line 318 of file giaQbf.c.

319 {
320  printf( "%5d : ", Iter );
321  assert( Vec_IntSize(vValues) == p->nVars );
322  Vec_IntPrintBinary( vValues ); printf( " " );
323  printf( "Var = %6d ", sat_solver_nvars(p->pSatSyn) );
324  printf( "Cla = %6d ", sat_solver_nclauses(p->pSatSyn) );
325  printf( "Conf = %6d ", sat_solver_nconflicts(p->pSatSyn) );
326  Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
327 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int sat_solver_nconflicts(sat_solver *s)
Definition: satSolver.c:1908
static abctime Abc_Clock()
Definition: abc_global.h:279
static void Vec_IntPrintBinary(Vec_Int_t *vVec)
Definition: vecInt.h:1811
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
int sat_solver_nvars(sat_solver *s)
Definition: satSolver.c:1896
int sat_solver_nclauses(sat_solver *s)
Definition: satSolver.c:1902
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define assert(ex)
Definition: util_old.h:213
int nVars
Definition: llb3Image.c:58
Gia_Man_t* Gia_QbfQuantify ( Gia_Man_t p,
int  nPars 
)

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

Synopsis [Create and add one cofactor.]

Description []

SideEffects []

SeeAlso []

Definition at line 214 of file giaQbf.c.

215 {
216  Gia_Man_t * pNew, * pTemp;
217  Gia_Obj_t * pObj;
218  int i, m, nMints = (1 << (Gia_ManPiNum(p) - nPars));
219  assert( Gia_ManPoNum(p) == 1 );
220  pNew = Gia_ManStart( Gia_ManObjNum(p) );
221  pNew->pName = Abc_UtilStrsav( p->pName );
222  Gia_ManHashAlloc( pNew );
223  Gia_ManConst0(p)->Value = 0;
224  for ( i = 0; i < nPars; i++ )
225  Gia_ManAppendCi(pNew);
226  for ( m = 0; m < nMints; m++ )
227  {
228  Gia_ManForEachPi( p, pObj, i )
229  pObj->Value = (i < nPars) ? Gia_Obj2Lit(pNew, Gia_ManPi(pNew, i)) : ((m >> (i - nPars)) & 1);
230  Gia_ManForEachAnd( p, pObj, i )
231  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
232  Gia_ManForEachCo( p, pObj, i )
233  pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
234  }
235  pNew = Gia_ManCleanup( pTemp = pNew );
236  Gia_ManStop( pTemp );
237  assert( Gia_ManPiNum(pNew) == nPars );
238  assert( Gia_ManPoNum(pNew) == nMints );
239  return pNew;
240 }
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Definition: gia.h:75
static Gia_Obj_t * Gia_ManPi(Gia_Man_t *p, int v)
Definition: gia.h:405
char * pName
Definition: gia.h:97
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
Definition: gia.h:95
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
#define assert(ex)
Definition: util_old.h:213
unsigned Value
Definition: gia.h:87
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
static int Gia_Obj2Lit(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:433
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
int Gia_QbfSolve ( Gia_Man_t pGia,
int  nPars,
int  nIterLimit,
int  nConfLimit,
int  nTimeOut,
int  fVerbose 
)

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

Synopsis [Performs QBF solving using an improved algorithm.]

Description []

SideEffects []

SeeAlso []

Definition at line 419 of file giaQbf.c.

420 {
421  Qbf_Man_t * p = Gia_QbfAlloc( pGia, nPars, fVerbose );
422  Gia_Man_t * pCof;
423  int i, status, RetValue = 0;
424  abctime clk;
425 // Gia_QbfAddSpecialConstr( p );
426  if ( fVerbose )
427  printf( "Solving QBF for \"%s\" with %d parameters, %d variables and %d AIG nodes.\n",
428  Gia_ManName(pGia), p->nPars, p->nVars, Gia_ManAndNum(pGia) );
429  assert( Gia_ManRegNum(pGia) == 0 );
430  Vec_IntFill( p->vValues, nPars, 0 );
431  for ( i = 0; Gia_QbfVerify(p, p->vValues); i++ )
432  {
433  // generate next constraint
434  assert( Vec_IntSize(p->vValues) == p->nVars );
435  pCof = Gia_QbfCofactor( pGia, nPars, p->vValues, p->vParMap );
436  status = Gia_QbfAddCofactor( p, pCof );
437  Gia_ManStop( pCof );
438  if ( status == 0 ) { RetValue = 1; break; }
439  // synthesize next assignment
440  clk = Abc_Clock();
441  status = sat_solver_solve( p->pSatSyn, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, 0, 0 );
442  p->clkSat += Abc_Clock() - clk;
443  if ( fVerbose )
444  Gia_QbfPrint( p, p->vValues, i );
445  if ( status == l_False ) { RetValue = 1; break; }
446  if ( status == l_Undef ) { RetValue = -1; break; }
447  // extract SAT assignment
448  Gia_QbfOnePattern( p, p->vValues );
449  assert( Vec_IntSize(p->vValues) == p->nPars );
450  // examine variables
451 // Gia_QbfLearnConstraint( p, p->vValues );
452 // Vec_IntPrintBinary( p->vValues ); printf( "\n" );
453  if ( nIterLimit && i+1 == nIterLimit ) { RetValue = -1; break; }
454  if ( nTimeOut && (Abc_Clock() - p->clkStart)/CLOCKS_PER_SEC >= nTimeOut ) { RetValue = -1; break; }
455  }
456  if ( RetValue == 0 )
457  {
458  printf( "Parameters: " );
459  assert( Vec_IntSize(p->vValues) == nPars );
460  Vec_IntPrintBinary( p->vValues );
461  printf( "\n" );
462  }
463  if ( RetValue == -1 && nTimeOut && (Abc_Clock() - p->clkStart)/CLOCKS_PER_SEC >= nTimeOut )
464  printf( "The problem timed out after %d sec. ", nTimeOut );
465  else if ( RetValue == -1 && nConfLimit )
466  printf( "The problem aborted after %d conflicts. ", nConfLimit );
467  else if ( RetValue == -1 && nIterLimit )
468  printf( "The problem aborted after %d iterations. ", nIterLimit );
469  else if ( RetValue == 1 )
470  printf( "The problem is UNSAT after %d iterations. ", i );
471  else
472  printf( "The problem is SAT after %d iterations. ", i );
473  if ( fVerbose )
474  {
475  printf( "\n" );
476  Abc_PrintTime( 1, "SAT ", p->clkSat );
477  Abc_PrintTime( 1, "Other", Abc_Clock() - p->clkStart - p->clkSat );
478  Abc_PrintTime( 1, "TOTAL", Abc_Clock() - p->clkStart );
479  }
480  else
481  Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
482  Gia_QbfFree( p );
483  return RetValue;
484 }
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Gia_QbfOnePattern(Qbf_Man_t *p, Vec_Int_t *vValues)
Definition: giaQbf.c:311
#define l_Undef
Definition: SolverTypes.h:86
static char * Gia_ManName(Gia_Man_t *p)
Definition: gia.h:382
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 Gia_QbfVerify(Qbf_Man_t *p, Vec_Int_t *vValues)
Definition: giaQbf.c:340
static abctime Abc_Clock()
Definition: abc_global.h:279
static void Vec_IntPrintBinary(Vec_Int_t *vVec)
Definition: vecInt.h:1811
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
Gia_Man_t * Gia_QbfCofactor(Gia_Man_t *p, int nPars, Vec_Int_t *vValues, Vec_Int_t *vParMap)
Definition: giaQbf.c:253
void Gia_QbfPrint(Qbf_Man_t *p, Vec_Int_t *vValues, int Iter)
Definition: giaQbf.c:318
typedefABC_NAMESPACE_IMPL_START struct Qbf_Man_t_ Qbf_Man_t
DECLARATIONS ///.
Definition: giaQbf.c:33
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Definition: gia.h:95
#define l_False
Definition: SolverTypes.h:85
int Gia_QbfAddCofactor(Qbf_Man_t *p, Gia_Man_t *pCof)
Definition: giaQbf.c:280
Qbf_Man_t * Gia_QbfAlloc(Gia_Man_t *pGia, int nPars, int fVerbose)
Definition: giaQbf.c:170
#define assert(ex)
Definition: util_old.h:213
ABC_INT64_T abctime
Definition: abc_global.h:278
void Gia_QbfFree(Qbf_Man_t *p)
Definition: giaQbf.c:193
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
int Gia_QbfVerify ( Qbf_Man_t p,
Vec_Int_t vValues 
)

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

Synopsis [Generate one SAT assignment in terms of functional vars.]

Description []

SideEffects []

SeeAlso []

Definition at line 340 of file giaQbf.c.

341 {
342  int i, Entry, RetValue;
343  assert( Vec_IntSize(vValues) == p->nPars );
344  Vec_IntClear( p->vLits );
345  Vec_IntForEachEntry( vValues, Entry, i )
346  Vec_IntPush( p->vLits, Abc_Var2Lit(p->iParVarBeg+i, !Entry) );
347  RetValue = sat_solver_solve( p->pSatVer, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits), 0, 0, 0, 0 );
348  if ( RetValue == l_True )
349  {
350  Vec_IntClear( vValues );
351  for ( i = 0; i < p->nVars; i++ )
352  Vec_IntPush( vValues, sat_solver_var_value(p->pSatVer, p->iParVarBeg+p->nPars+i) );
353  }
354  return RetValue == l_True ? 1 : 0;
355 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
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
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
#define l_True
Definition: SolverTypes.h:84
static int * Vec_IntLimit(Vec_Int_t *p)
Definition: vecInt.h:336
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
if(last==0)
Definition: sparse_int.h:34
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define assert(ex)
Definition: util_old.h:213
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
int nVars
Definition: llb3Image.c:58
Cnf_Dat_t* Mf_ManGenerateCnf ( Gia_Man_t pGia,
int  nLutSize,
int  fCnfObjIds,
int  fAddOrCla,
int  fVerbose 
)

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

Synopsis [CNF generation]

Description []

SideEffects []

SeeAlso []

Definition at line 1629 of file giaMf.c.

1630 {
1631  Gia_Man_t * pNew;
1632  Jf_Par_t Pars, * pPars = &Pars;
1633  assert( nLutSize >= 3 && nLutSize <= 8 );
1634  Mf_ManSetDefaultPars( pPars );
1635  pPars->fGenCnf = 1;
1636  pPars->fCoarsen = !fCnfObjIds;
1637  pPars->nLutSize = nLutSize;
1638  pPars->fCnfObjIds = fCnfObjIds;
1639  pPars->fAddOrCla = fAddOrCla;
1640  pPars->fVerbose = fVerbose;
1641  pNew = Mf_ManPerformMapping( pGia, pPars );
1642  Gia_ManStopP( &pNew );
1643 // Cnf_DataPrint( (Cnf_Dat_t *)pGia->pData, 1 );
1644  return pGia->pData;
1645 }
int nLutSize
Definition: gia.h:267
int fCnfObjIds
Definition: gia.h:285
void Gia_ManStopP(Gia_Man_t **p)
Definition: giaMan.c:177
Definition: gia.h:265
void * pData
Definition: gia.h:169
Gia_Man_t * Mf_ManPerformMapping(Gia_Man_t *pGia, Jf_Par_t *pPars)
Definition: giaMf.c:1575
void Mf_ManSetDefaultPars(Jf_Par_t *pPars)
Definition: giaMf.c:1380
Definition: gia.h:95
int fGenCnf
Definition: gia.h:284
#define assert(ex)
Definition: util_old.h:213
int fAddOrCla
Definition: gia.h:286
int fVerbose
Definition: gia.h:291
int fCoarsen
Definition: gia.h:281