luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Adding switch &qbf -q to quantify functional variables.

This commit is contained in:
Alan Mishchenko 2014-10-20 11:01:34 -07:00
parent bae5e26fb5
commit 83bc1148a2
1 changed files with 1 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/aig/gia/giaQbf.c
View File

@ -389,8 +389,7 @@ int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, i
Gia_QbfOnePattern( p, p->vValues );
assert( Vec_IntSize(p->vValues) == p->nPars );
// examine variables
if ( i % 50 == 49 )
Gia_QbfLearnConstraint( p, p->vValues );
// Gia_QbfLearnConstraint( p, p->vValues );
// Vec_IntPrintBinary( p->vValues ); printf( "\n" );
if ( nIterLimit && i+1 == nIterLimit ) { RetValue = -1; break; }
if ( nTimeOut && (Abc_Clock() - p->clkStart)/CLOCKS_PER_SEC >= nTimeOut ) { RetValue = -1; break; }