abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
fraClaus.c File Reference
#include "fra.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"

Go to the source code of this file.

Data Structures

struct  Clu_Man_t_
 

Typedefs

typedef
typedefABC_NAMESPACE_IMPL_START
struct Clu_Man_t_ 
Clu_Man_t
 DECLARATIONS ///. More...
 

Functions

int Fra_ClausRunBmc (Clu_Man_t *p)
 FUNCTION DEFINITIONS ///. More...
 
int Fra_ClausRunSat (Clu_Man_t *p)
 
int Fra_ClausRunSat0 (Clu_Man_t *p)
 
void transpose32a (unsigned a[32])
 
int Fra_ClausProcessClausesCut (Clu_Man_t *p, Fra_Sml_t *pSimMan, Dar_Cut_t *pCut, int *pScores)
 
int Fra_ClausProcessClausesCut2 (Clu_Man_t *p, Fra_Sml_t *pSimMan, Dar_Cut_t *pCut, int *pScores)
 
void Fra_ClausProcessClausesCut3 (Clu_Man_t *p, Fra_Sml_t *pSimMan, Aig_Cut_t *pCut, int *pScores)
 
int Fra_ClausSelectClauses (Clu_Man_t *p)
 
void Fra_ClausRecordClause (Clu_Man_t *p, Dar_Cut_t *pCut, int iMint, int Cost)
 
void Fra_ClausRecordClause2 (Clu_Man_t *p, Aig_Cut_t *pCut, int iMint, int Cost)
 
int Fra_ClausSmlNodeIsConst (Fra_Sml_t *pSeq, Aig_Obj_t *pObj)
 
int Fra_ClausSmlNodesAreImp (Fra_Sml_t *pSeq, Aig_Obj_t *pObj1, Aig_Obj_t *pObj2)
 
int Fra_ClausSmlNodesAreImpC (Fra_Sml_t *pSeq, Aig_Obj_t *pObj1, Aig_Obj_t *pObj2)
 
int Fra_ClausCollectLatchClauses (Clu_Man_t *p, Fra_Sml_t *pSeq)
 
int Fra_ClausProcessClauses (Clu_Man_t *p, int fRefs)
 
int Fra_ClausProcessClauses2 (Clu_Man_t *p, int fRefs)
 
int Fra_ClausBmcClauses (Clu_Man_t *p)
 
void Fra_ClausSimInfoClean (Clu_Man_t *p)
 
void Fra_ClausSimInfoRealloc (Clu_Man_t *p)
 
void Fra_ClausSimInfoRecord (Clu_Man_t *p, int *pModel)
 
int Fra_ClausSimInfoCheck (Clu_Man_t *p, int *pLits, int nLits)
 
int Fra_ClausInductiveClauses (Clu_Man_t *p)
 
Clu_Man_tFra_ClausAlloc (Aig_Man_t *pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fTarget, int fVerbose, int fVeryVerbose)
 
void Fra_ClausFree (Clu_Man_t *p)
 
void Fra_ClausAddToStorage (Clu_Man_t *p)
 
void Fra_ClausPrintIndClauses (Clu_Man_t *p)
 
Aig_Obj_tFra_ClausGetLiteral (Clu_Man_t *p, int *pVar2Id, int Lit)
 
void Fra_ClausWriteIndClauses (Clu_Man_t *p)
 
void Fra_ClausEstimateCoverageOne (Fra_Sml_t *pSim, int *pLits, int nLits, int *pVar2Id, unsigned *pResult)
 
void Fra_ClausEstimateCoverage (Clu_Man_t *p)
 
int Fra_Claus (Aig_Man_t *pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fTarget, int fVerbose, int fVeryVerbose)
 

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Clu_Man_t_ Clu_Man_t

DECLARATIONS ///.

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

FileName [fraClaus.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis [Induction with clause strengthening.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id:
fraClau.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

]

Definition at line 32 of file fraClaus.c.

Function Documentation

int Fra_Claus ( Aig_Man_t pAig,
int  nFrames,
int  nPref,
int  nClausesMax,
int  nLutSize,
int  nLevels,
int  nCutsMax,
int  nBatches,
int  fStepUp,
int  fBmc,
int  fRefs,
int  fTarget,
int  fVerbose,
int  fVeryVerbose 
)

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

Synopsis [Converts AIG into the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 1682 of file fraClaus.c.

1683 {
1684  Clu_Man_t * p;
1685  abctime clk, clkTotal = Abc_Clock(), clkInd;
1686  int b, Iter, Counter, nPrefOld;
1687  int nClausesBeg = 0;
1688 
1689  // create the manager
1690  p = Fra_ClausAlloc( pAig, nFrames, nPref, nClausesMax, nLutSize, nLevels, nCutsMax, nBatches, fStepUp, fTarget, fVerbose, fVeryVerbose );
1691 if ( p->fVerbose )
1692 {
1693  printf( "PARAMETERS: Frames = %d. Pref = %d. Clauses max = %d. Cut size = %d.\n", nFrames, nPref, nClausesMax, nLutSize );
1694  printf( "Level max = %d. Cuts max = %d. Batches = %d. Increment cut size = %s.\n", nLevels, nCutsMax, nBatches, fStepUp? "yes":"no" );
1695 //ABC_PRT( "Sim-seq", Abc_Clock() - clk );
1696 }
1697 
1698  assert( !p->fTarget || Aig_ManCoNum(pAig) - Aig_ManRegNum(pAig) == 1 );
1699 
1700 clk = Abc_Clock();
1701  // derive CNF
1702 // if ( p->fTarget )
1703 // p->pAig->nRegs++;
1704  p->pCnf = Cnf_DeriveSimple( p->pAig, Aig_ManCoNum(p->pAig) );
1705 // if ( p->fTarget )
1706 // p->pAig->nRegs--;
1707 if ( fVerbose )
1708 {
1709 //ABC_PRT( "CNF ", Abc_Clock() - clk );
1710 }
1711 
1712  // check BMC
1713 clk = Abc_Clock();
1714  p->pSatBmc = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nPref + p->nFrames, 1 );
1715  if ( p->pSatBmc == NULL )
1716  {
1717  printf( "Error: BMC solver is unsat.\n" );
1718  Fra_ClausFree( p );
1719  return 1;
1720  }
1721  if ( p->fTarget && !Fra_ClausRunBmc( p ) )
1722  {
1723  printf( "Problem fails the base case after %d frame expansion.\n", p->nPref + p->nFrames );
1724  Fra_ClausFree( p );
1725  return 1;
1726  }
1727 if ( fVerbose )
1728 {
1729 //ABC_PRT( "SAT-bmc", Abc_Clock() - clk );
1730 }
1731 
1732  // start the SAT solver
1733 clk = Abc_Clock();
1734  p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 );
1735  if ( p->pSatMain == NULL )
1736  {
1737  printf( "Error: Main solver is unsat.\n" );
1738  Fra_ClausFree( p );
1739  return 1;
1740  }
1741 
1742 
1743  for ( b = 0; b < p->nBatches; b++ )
1744  {
1745 // if ( fVerbose )
1746  printf( "*** BATCH %d: ", b+1 );
1747  if ( b && p->nLutSize < 12 && (!p->fFiltering || p->fNothingNew || p->fStepUp) )
1748  p->nLutSize++;
1749  printf( "Using %d-cuts.\n", p->nLutSize );
1750 
1751  // try solving without additional clauses
1752  if ( p->fTarget && Fra_ClausRunSat( p ) )
1753  {
1754  printf( "Problem is inductive without strengthening.\n" );
1755  Fra_ClausFree( p );
1756  return 1;
1757  }
1758  if ( fVerbose )
1759  {
1760 // ABC_PRT( "SAT-ind", Abc_Clock() - clk );
1761  }
1762 
1763  // collect the candidate inductive clauses using 4-cuts
1764  clk = Abc_Clock();
1765  nPrefOld = p->nPref; p->nPref = 0; p->nSimWordsPref = 0;
1766  // Fra_ClausProcessClauses( p, fRefs );
1767  Fra_ClausProcessClauses2( p, fRefs );
1768  p->nPref = nPrefOld;
1769  p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames;
1770  nClausesBeg = p->nClauses;
1771 
1772  //ABC_PRT( "Clauses", Abc_Clock() - clk );
1773 
1774 
1775  // check clauses using BMC
1776  if ( fBmc )
1777  {
1778  clk = Abc_Clock();
1779  Counter = Fra_ClausBmcClauses( p );
1780  p->nClauses -= Counter;
1781  if ( fVerbose )
1782  {
1783  printf( "BMC disproved %d clauses. ", Counter );
1784  ABC_PRT( "Time", Abc_Clock() - clk );
1785  }
1786  }
1787 
1788 
1789  // prove clauses inductively
1790  clkInd = clk = Abc_Clock();
1791  Counter = 1;
1792  for ( Iter = 0; Counter > 0; Iter++ )
1793  {
1794  if ( fVerbose )
1795  printf( "Iter %3d : Begin = %5d. ", Iter, p->nClauses );
1796  Counter = Fra_ClausInductiveClauses( p );
1797  if ( Counter > 0 )
1798  p->nClauses -= Counter;
1799  if ( fVerbose )
1800  {
1801  printf( "End = %5d. Exs = %5d. ", p->nClauses, p->nCexes );
1802  // printf( "\n" );
1803  ABC_PRT( "Time", Abc_Clock() - clk );
1804  }
1805  clk = Abc_Clock();
1806  }
1807  // add proved clauses to storage
1808  Fra_ClausAddToStorage( p );
1809  // report the results
1810  if ( p->fTarget )
1811  {
1812  if ( Counter == -1 )
1813  printf( "Fra_Claus(): Internal error. " );
1814  else if ( p->fFail )
1815  printf( "Property FAILS during refinement. " );
1816  else
1817  printf( "Property HOLDS inductively after strengthening. " );
1818  ABC_PRT( "Time ", Abc_Clock() - clkTotal );
1819  if ( !p->fFail )
1820  break;
1821  }
1822  else
1823  {
1824  printf( "Finished proving inductive clauses. " );
1825  ABC_PRT( "Time ", Abc_Clock() - clkTotal );
1826  }
1827  }
1828 
1829  // verify the computed interpolant
1830  Fra_InvariantVerify( pAig, nFrames, p->vClausesProven, p->vLitsProven );
1831 // printf( "THIS COMMAND IS KNOWN TO HAVE A BUG!\n" );
1832 
1833 // if ( !p->fTarget && p->fVerbose )
1834  if ( p->fVerbose )
1835  {
1838  }
1839 
1840  if ( !p->fTarget )
1841  {
1843  }
1844 /*
1845  // print the statistic into a file
1846  {
1847  FILE * pTable;
1848  assert( p->nBatches == 1 );
1849  pTable = fopen( "stats.txt", "a+" );
1850  fprintf( pTable, "%s ", pAig->pName );
1851  fprintf( pTable, "%d ", Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig) );
1852  fprintf( pTable, "%d ", Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig) );
1853  fprintf( pTable, "%d ", Aig_ManRegNum(pAig) );
1854  fprintf( pTable, "%d ", Aig_ManNodeNum(pAig) );
1855  fprintf( pTable, "%d ", p->nCuts );
1856  fprintf( pTable, "%d ", nClausesBeg );
1857  fprintf( pTable, "%d ", p->nClauses );
1858  fprintf( pTable, "%d ", Iter );
1859  fprintf( pTable, "%.2f ", (float)(clkInd-clkTotal)/(float)(CLOCKS_PER_SEC) );
1860  fprintf( pTable, "%.2f ", (float)(Abc_Clock()-clkInd)/(float)(CLOCKS_PER_SEC) );
1861  fprintf( pTable, "%.2f ", (float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC) );
1862  fprintf( pTable, "\n" );
1863  fclose( pTable );
1864  }
1865 */
1866  // clean the manager
1867  Fra_ClausFree( p );
1868  return 1;
1869 }
Clu_Man_t * Fra_ClausAlloc(Aig_Man_t *pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fTarget, int fVerbose, int fVeryVerbose)
Definition: fraClaus.c:1365
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int Fra_ClausRunBmc(Clu_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition: fraClaus.c:94
void Fra_ClausEstimateCoverage(Clu_Man_t *p)
Definition: fraClaus.c:1620
int Fra_ClausRunSat(Clu_Man_t *p)
Definition: fraClaus.c:122
void Fra_ClausFree(Clu_Man_t *p)
Definition: fraClaus.c:1410
static abctime Abc_Clock()
Definition: abc_global.h:279
void Fra_ClausPrintIndClauses(Clu_Man_t *p)
Definition: fraClaus.c:1483
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
void Fra_ClausWriteIndClauses(Clu_Man_t *p)
Definition: fraClaus.c:1540
static int Counter
typedefABC_NAMESPACE_IMPL_START struct Clu_Man_t_ Clu_Man_t
DECLARATIONS ///.
Definition: fraClaus.c:32
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition: cnfMan.c:463
Cnf_Dat_t * Cnf_DeriveSimple(Aig_Man_t *p, int nOutputs)
Definition: cnfWrite.c:587
#define ABC_PRT(a, t)
Definition: abc_global.h:220
void Fra_ClausAddToStorage(Clu_Man_t *p)
Definition: fraClaus.c:1436
int Fra_ClausBmcClauses(Clu_Man_t *p)
Definition: fraClaus.c:897
#define assert(ex)
Definition: util_old.h:213
ABC_INT64_T abctime
Definition: abc_global.h:278
int Fra_ClausInductiveClauses(Clu_Man_t *p)
Definition: fraClaus.c:1098
int Fra_InvariantVerify(Aig_Man_t *p, int nFrames, Vec_Int_t *vClauses, Vec_Int_t *vLits)
DECLARATIONS ///.
Definition: fraIndVer.c:46
int Fra_ClausProcessClauses2(Clu_Man_t *p, int fRefs)
Definition: fraClaus.c:724
void Fra_ClausAddToStorage ( Clu_Man_t p)

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

Synopsis [Converts AIG into the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 1436 of file fraClaus.c.

1437 {
1438  int * pStart;
1439  int Beg, End, Counter, i, k;
1440  Beg = 0;
1441  Counter = 0;
1442  pStart = Vec_IntArray( p->vLits );
1443  Vec_IntForEachEntry( p->vClauses, End, i )
1444  {
1445  if ( Vec_IntEntry( p->vCosts, i ) == -1 )
1446  {
1447  Beg = End;
1448  continue;
1449  }
1450  assert( Vec_IntEntry( p->vCosts, i ) > 0 );
1451  assert( End - Beg <= p->nLutSize );
1452  for ( k = Beg; k < End; k++ )
1453  Vec_IntPush( p->vLitsProven, pStart[k] );
1454  Vec_IntPush( p->vClausesProven, Vec_IntSize(p->vLitsProven) );
1455  Beg = End;
1456  Counter++;
1457 
1458  if ( i < p->nOneHots )
1459  p->nOneHotsProven++;
1460  }
1461  if ( p->fVerbose )
1462  printf( "Added to storage %d proved clauses (including %d one-hot clauses)\n", Counter, p->nOneHotsProven );
1463 
1464  Vec_IntClear( p->vClauses );
1465  Vec_IntClear( p->vLits );
1466  Vec_IntClear( p->vCosts );
1467  p->nClauses = 0;
1468 
1469  p->fNothingNew = (int)(Counter == 0);
1470 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Counter
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
Clu_Man_t* Fra_ClausAlloc ( Aig_Man_t pAig,
int  nFrames,
int  nPref,
int  nClausesMax,
int  nLutSize,
int  nLevels,
int  nCutsMax,
int  nBatches,
int  fStepUp,
int  fTarget,
int  fVerbose,
int  fVeryVerbose 
)

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

Synopsis [Converts AIG into the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 1365 of file fraClaus.c.

1366 {
1367  Clu_Man_t * p;
1368  p = ABC_ALLOC( Clu_Man_t, 1 );
1369  memset( p, 0, sizeof(Clu_Man_t) );
1370  p->pAig = pAig;
1371  p->nFrames = nFrames;
1372  p->nPref = nPref;
1373  p->nClausesMax = nClausesMax;
1374  p->nLutSize = nLutSize;
1375  p->nLevels = nLevels;
1376  p->nCutsMax = nCutsMax;
1377  p->nBatches = nBatches;
1378  p->fStepUp = fStepUp;
1379  p->fTarget = fTarget;
1380  p->fVerbose = fVerbose;
1381  p->fVeryVerbose = fVeryVerbose;
1382  p->nSimWords = 512;//1024;//64;
1383  p->nSimFrames = 32;//8;//32;
1384  p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames;
1385 
1386  p->vLits = Vec_IntAlloc( 1<<14 );
1387  p->vClauses = Vec_IntAlloc( 1<<12 );
1388  p->vCosts = Vec_IntAlloc( 1<<12 );
1389 
1390  p->vLitsProven = Vec_IntAlloc( 1<<14 );
1391  p->vClausesProven= Vec_IntAlloc( 1<<12 );
1392 
1393  p->nCexesAlloc = 1024;
1394  p->vCexes = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pAig)+1, p->nCexesAlloc/32 );
1395  Vec_PtrCleanSimInfo( p->vCexes, 0, p->nCexesAlloc/32 );
1396  return p;
1397 }
char * memset()
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static void Vec_PtrCleanSimInfo(Vec_Ptr_t *vInfo, int iWord, int nWords)
Definition: vecPtr.h:968
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
typedefABC_NAMESPACE_IMPL_START struct Clu_Man_t_ Clu_Man_t
DECLARATIONS ///.
Definition: fraClaus.c:32
static Vec_Ptr_t * Vec_PtrAllocSimInfo(int nEntries, int nWords)
Definition: vecPtr.h:929
int Fra_ClausBmcClauses ( Clu_Man_t p)

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

Synopsis [Converts AIG into the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 897 of file fraClaus.c.

898 {
899  int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f;
900 /*
901  for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
902  printf( "%d ", p->vLits->pArray[i] );
903  printf( "\n" );
904 */
905  // add the clauses
906  Counter = 0;
907  // skip through the prefix variables
908  if ( p->nPref )
909  {
910  nLitsTot = p->nPref * 2 * p->pCnf->nVars;
911  for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
912  p->vLits->pArray[i] += nLitsTot;
913  }
914  // go through the timeframes
915  nLitsTot = 2 * p->pCnf->nVars;
916  pStart = Vec_IntArray(p->vLits);
917  for ( f = 0; f < p->nFrames; f++ )
918  {
919  Beg = 0;
920  Vec_IntForEachEntry( p->vClauses, End, i )
921  {
922  if ( Vec_IntEntry( p->vCosts, i ) == -1 )
923  {
924  Beg = End;
925  continue;
926  }
927  assert( Vec_IntEntry( p->vCosts, i ) > 0 );
928  assert( End - Beg <= p->nLutSize );
929 
930  for ( k = Beg; k < End; k++ )
931  pStart[k] = lit_neg( pStart[k] );
932  RetValue = sat_solver_solve( p->pSatBmc, pStart + Beg, pStart + End, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
933  for ( k = Beg; k < End; k++ )
934  pStart[k] = lit_neg( pStart[k] );
935 
936  if ( RetValue != l_False )
937  {
938  Beg = End;
939  Vec_IntWriteEntry( p->vCosts, i, -1 );
940  Counter++;
941  continue;
942  }
943 /*
944  // add the clause
945  RetValue = sat_solver_addclause( p->pSatBmc, pStart + Beg, pStart + End );
946  // assert( RetValue == 1 );
947  if ( RetValue == 0 )
948  {
949  printf( "Error: Solver is UNSAT after adding BMC clauses.\n" );
950  return -1;
951  }
952 */
953  Beg = End;
954 
955  // simplify the solver
956  if ( p->pSatBmc->qtail != p->pSatBmc->qhead )
957  {
958  RetValue = sat_solver_simplify(p->pSatBmc);
959  assert( RetValue != 0 );
960  assert( p->pSatBmc->qtail == p->pSatBmc->qhead );
961  }
962  }
963  // increment literals
964  for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
965  p->vLits->pArray[i] += nLitsTot;
966  }
967 
968  // return clauses back to normal
969  nLitsTot = (p->nPref + p->nFrames) * nLitsTot;
970  for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
971  p->vLits->pArray[i] -= nLitsTot;
972 /*
973  for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
974  printf( "%d ", p->vLits->pArray[i] );
975  printf( "\n" );
976 */
977  return Counter;
978 }
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 lit lit_neg(lit l)
Definition: satVec.h:144
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
static int Counter
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define l_False
Definition: SolverTypes.h:85
#define assert(ex)
Definition: util_old.h:213
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
int nVars
Definition: llb3Image.c:58
int Fra_ClausCollectLatchClauses ( Clu_Man_t p,
Fra_Sml_t pSeq 
)

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

Synopsis [Processes the clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 513 of file fraClaus.c.

514 {
515  Aig_Obj_t * pObj1, * pObj2;
516  unsigned * pSims1, * pSims2;
517  int CostMax, i, k, nCountConst, nCountImps;
518 
519  nCountConst = nCountImps = 0;
520  CostMax = p->nSimWords * 32;
521 /*
522  // add the property
523  {
524  Aig_Obj_t * pObj;
525  int Lits[1];
526  pObj = Aig_ManCo( p->pAig, 0 );
527  Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 1 );
528  Vec_IntPush( p->vLits, Lits[0] );
529  Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
530  Vec_IntPush( p->vCosts, CostMax );
531  nCountConst++;
532 // printf( "Added the target property to the set of clauses to be inductively checked.\n" );
533  }
534 */
535 
536  pSeq->nWordsPref = p->nSimWordsPref;
537  Aig_ManForEachLoSeq( p->pAig, pObj1, i )
538  {
539  pSims1 = Fra_ObjSim( pSeq, pObj1->Id );
540  if ( Fra_ClausSmlNodeIsConst( pSeq, pObj1 ) )
541  {
542  Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 ) );
543  Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
544  Vec_IntPush( p->vCosts, CostMax );
545  nCountConst++;
546  continue;
547  }
548  Aig_ManForEachLoSeq( p->pAig, pObj2, k )
549  {
550  pSims2 = Fra_ObjSim( pSeq, pObj2->Id );
551  if ( Fra_ClausSmlNodesAreImp( pSeq, pObj1, pObj2 ) )
552  {
553  Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 ) );
554  Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj2->Id], 0 ) );
555  Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
556  Vec_IntPush( p->vCosts, CostMax );
557  nCountImps++;
558  continue;
559  }
560  if ( Fra_ClausSmlNodesAreImp( pSeq, pObj2, pObj1 ) )
561  {
562  Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj2->Id], 1 ) );
563  Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 0 ) );
564  Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
565  Vec_IntPush( p->vCosts, CostMax );
566  nCountImps++;
567  continue;
568  }
569  if ( Fra_ClausSmlNodesAreImpC( pSeq, pObj1, pObj2 ) )
570  {
571  Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 ) );
572  Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj2->Id], 1 ) );
573  Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
574  Vec_IntPush( p->vCosts, CostMax );
575  nCountImps++;
576  continue;
577  }
578  }
579  if ( nCountConst + nCountImps > p->nClausesMax / 2 )
580  break;
581  }
582  pSeq->nWordsPref = 0;
583  if ( p->fVerbose )
584  printf( "Collected %d register constants and %d one-hotness implications.\n", nCountConst, nCountImps );
585  p->nOneHots = nCountConst + nCountImps;
586  p->nOneHotsProven = 0;
587  return 0;
588 }
Aig_Man_t * pAig
Definition: llb3Image.c:49
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int Fra_ClausSmlNodesAreImp(Fra_Sml_t *pSeq, Aig_Obj_t *pObj1, Aig_Obj_t *pObj2)
Definition: fraClaus.c:467
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
static lit toLitCond(int v, int c)
Definition: satVec.h:143
Definition: aig.h:69
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
int Fra_ClausSmlNodeIsConst(Fra_Sml_t *pSeq, Aig_Obj_t *pObj)
Definition: fraClaus.c:445
int Fra_ClausSmlNodesAreImpC(Fra_Sml_t *pSeq, Aig_Obj_t *pObj1, Aig_Obj_t *pObj2)
Definition: fraClaus.c:490
#define Aig_ManForEachLoSeq(p, pObj, i)
Definition: aig.h:441
int nWordsPref
Definition: fra.h:178
int Id
Definition: aig.h:85
void Fra_ClausEstimateCoverage ( Clu_Man_t p)

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

Synopsis [Estimates the coverage of state space by clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 1620 of file fraClaus.c.

1621 {
1622  int nCombSimWords = (1<<11);
1623  Fra_Sml_t * pComb;
1624  unsigned * pResultTot, * pResultOne;
1625  int nCovered, Beg, End, i, w;
1626  int * pStart, * pVar2Id;
1627  abctime clk = Abc_Clock();
1628  // simulate the circuit with nCombSimWords * 32 = 64K patterns
1629 // srand( 0xAABBAABB );
1630  Aig_ManRandom(1);
1631  pComb = Fra_SmlSimulateComb( p->pAig, nCombSimWords, 0 );
1632  // create mapping from SAT vars to node IDs
1633  pVar2Id = ABC_ALLOC( int, p->pCnf->nVars );
1634  memset( pVar2Id, 0, sizeof(int) * p->pCnf->nVars );
1635  for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
1636  if ( p->pCnf->pVarNums[i] >= 0 )
1637  {
1638  assert( p->pCnf->pVarNums[i] < p->pCnf->nVars );
1639  pVar2Id[ p->pCnf->pVarNums[i] ] = i;
1640  }
1641  // get storage for one assignment and all assignments
1642  assert( Aig_ManCoNum(p->pAig) > 2 );
1643  pResultOne = Fra_ObjSim( pComb, Aig_ManCo(p->pAig, 0)->Id );
1644  pResultTot = Fra_ObjSim( pComb, Aig_ManCo(p->pAig, 1)->Id );
1645  // start the OR of don't-cares
1646  for ( w = 0; w < nCombSimWords; w++ )
1647  pResultTot[w] = 0;
1648  // check clauses
1649  Beg = 0;
1650  pStart = Vec_IntArray( p->vLitsProven );
1651  Vec_IntForEachEntry( p->vClausesProven, End, i )
1652  {
1653  Fra_ClausEstimateCoverageOne( pComb, pStart + Beg, End-Beg, pVar2Id, pResultOne );
1654  Beg = End;
1655  for ( w = 0; w < nCombSimWords; w++ )
1656  pResultTot[w] |= pResultOne[w];
1657  }
1658  // count the total number of patterns contained in the don't-care
1659  nCovered = 0;
1660  for ( w = 0; w < nCombSimWords; w++ )
1661  nCovered += Aig_WordCountOnes( pResultTot[w] );
1662  Fra_SmlStop( pComb );
1663  ABC_FREE( pVar2Id );
1664  // print the result
1665  printf( "Care states ratio = %f. ", 1.0 * (nCombSimWords * 32 - nCovered) / (nCombSimWords * 32) );
1666  printf( "(%d out of %d patterns) ", nCombSimWords * 32 - nCovered, nCombSimWords * 32 );
1667  ABC_PRT( "Time", Abc_Clock() - clk );
1668 }
char * memset()
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Aig_Man_t * pAig
Definition: llb3Image.c:49
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
unsigned Aig_ManRandom(int fReset)
Definition: aigUtil.c:1157
static abctime Abc_Clock()
Definition: abc_global.h:279
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
static int Aig_WordCountOnes(unsigned uWord)
Definition: aig.h:229
Fra_Sml_t * Fra_SmlSimulateComb(Aig_Man_t *pAig, int nWords, int fCheckMiter)
Definition: fraSim.c:856
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
#define ABC_FREE(obj)
Definition: abc_global.h:232
#define ABC_PRT(a, t)
Definition: abc_global.h:220
#define assert(ex)
Definition: util_old.h:213
ABC_INT64_T abctime
Definition: abc_global.h:278
void Fra_ClausEstimateCoverageOne(Fra_Sml_t *pSim, int *pLits, int nLits, int *pVar2Id, unsigned *pResult)
Definition: fraClaus.c:1592
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
int Id
Definition: aig.h:85
int nVars
Definition: llb3Image.c:58
void Fra_SmlStop(Fra_Sml_t *p)
Definition: fraSim.c:839
void Fra_ClausEstimateCoverageOne ( Fra_Sml_t pSim,
int *  pLits,
int  nLits,
int *  pVar2Id,
unsigned *  pResult 
)

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

Synopsis [Checks if the clause holds using the given simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 1592 of file fraClaus.c.

1593 {
1594  unsigned * pSims[16];
1595  int iVar, i, w;
1596  for ( i = 0; i < nLits; i++ )
1597  {
1598  iVar = lit_var(pLits[i]);
1599  pSims[i] = Fra_ObjSim( pSim, pVar2Id[iVar] );
1600  }
1601  for ( w = 0; w < pSim->nWordsTotal; w++ )
1602  {
1603  pResult[w] = ~(unsigned)0;
1604  for ( i = 0; i < nLits; i++ )
1605  pResult[w] &= (lit_sign(pLits[i])? pSims[i][w] : ~pSims[i][w]);
1606  }
1607 }
static int lit_var(lit l)
Definition: satVec.h:145
int nWordsTotal
Definition: fra.h:177
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
static int lit_sign(lit l)
Definition: satVec.h:146
void Fra_ClausFree ( Clu_Man_t p)

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

Synopsis [Converts AIG into the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 1410 of file fraClaus.c.

1411 {
1412  if ( p->vCexes ) Vec_PtrFree( p->vCexes );
1413  if ( p->vLits ) Vec_IntFree( p->vLits );
1414  if ( p->vClauses ) Vec_IntFree( p->vClauses );
1415  if ( p->vLitsProven ) Vec_IntFree( p->vLitsProven );
1416  if ( p->vClausesProven ) Vec_IntFree( p->vClausesProven );
1417  if ( p->vCosts ) Vec_IntFree( p->vCosts );
1418  if ( p->pCnf ) Cnf_DataFree( p->pCnf );
1419  if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
1420  if ( p->pSatBmc ) sat_solver_delete( p->pSatBmc );
1421  ABC_FREE( p );
1422 }
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
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Aig_Obj_t* Fra_ClausGetLiteral ( Clu_Man_t p,
int *  pVar2Id,
int  Lit 
)

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

Synopsis [Writes the clauses into an AIGER file.]

Description []

SideEffects []

SeeAlso []

Definition at line 1520 of file fraClaus.c.

1521 {
1522  Aig_Obj_t * pLiteral;
1523  int NodeId = pVar2Id[ lit_var(Lit) ];
1524  assert( NodeId >= 0 );
1525  pLiteral = (Aig_Obj_t *)Aig_ManObj( p->pAig, NodeId )->pData;
1526  return Aig_NotCond( pLiteral, lit_sign(Lit) );
1527 }
Aig_Man_t * pAig
Definition: llb3Image.c:49
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void * pData
Definition: aig.h:87
static int lit_var(lit l)
Definition: satVec.h:145
static Aig_Obj_t * Aig_ManObj(Aig_Man_t *p, int i)
Definition: aig.h:270
Definition: aig.h:69
static int lit_sign(lit l)
Definition: satVec.h:146
#define assert(ex)
Definition: util_old.h:213
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
int Fra_ClausInductiveClauses ( Clu_Man_t p)

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

Synopsis [Converts AIG into the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 1098 of file fraClaus.c.

1099 {
1100 // Aig_Obj_t * pObjLi, * pObjLo;
1101  int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f, fFlag;//, Lits[2];
1102  p->fFail = 0;
1103 
1104  // reset the solver
1105  if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
1106  p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 );
1107  if ( p->pSatMain == NULL )
1108  {
1109  printf( "Error: Main solver is unsat.\n" );
1110  return -1;
1111  }
1113 
1114 /*
1115  // check if the property holds
1116  if ( Fra_ClausRunSat0( p ) )
1117  printf( "Property holds without strengthening.\n" );
1118  else
1119  printf( "Property does not hold without strengthening.\n" );
1120 */
1121 /*
1122  // add constant registers
1123  Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
1124  if ( Aig_ObjFanin0(pObjLi) == Aig_ManConst1(p->pAig) )
1125  {
1126  for ( k = 0; k < p->nFrames; k++ )
1127  {
1128  Lits[0] = k * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObjLo->Id], Aig_ObjFaninC0(pObjLi) );
1129  RetValue = sat_solver_addclause( p->pSatMain, Lits, Lits + 1 );
1130  if ( RetValue == 0 )
1131  {
1132  printf( "Error: Solver is UNSAT after adding constant-register clauses.\n" );
1133  return -1;
1134  }
1135  }
1136  }
1137 */
1138 
1139 
1140  // add the proven clauses
1141  nLitsTot = 2 * p->pCnf->nVars;
1142  pStart = Vec_IntArray(p->vLitsProven);
1143  for ( f = 0; f < p->nFrames; f++ )
1144  {
1145  Beg = 0;
1146  Vec_IntForEachEntry( p->vClausesProven, End, i )
1147  {
1148  assert( End - Beg <= p->nLutSize );
1149  // add the clause to all timeframes
1150  RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
1151  if ( RetValue == 0 )
1152  {
1153  printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
1154  return -1;
1155  }
1156  Beg = End;
1157  }
1158  // increment literals
1159  for ( i = 0; i < Vec_IntSize(p->vLitsProven); i++ )
1160  p->vLitsProven->pArray[i] += nLitsTot;
1161  }
1162  // return clauses back to normal
1163  nLitsTot = (p->nFrames) * nLitsTot;
1164  for ( i = 0; i < Vec_IntSize(p->vLitsProven); i++ )
1165  p->vLitsProven->pArray[i] -= nLitsTot;
1166 
1167 /*
1168  // add the proven clauses
1169  nLitsTot = 2 * p->pCnf->nVars;
1170  pStart = Vec_IntArray(p->vLitsProven);
1171  Beg = 0;
1172  Vec_IntForEachEntry( p->vClausesProven, End, i )
1173  {
1174  assert( End - Beg <= p->nLutSize );
1175  // add the clause to all timeframes
1176  RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
1177  if ( RetValue == 0 )
1178  {
1179  printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
1180  return -1;
1181  }
1182  Beg = End;
1183  }
1184 */
1185 
1186  // add the clauses
1187  nLitsTot = 2 * p->pCnf->nVars;
1188  pStart = Vec_IntArray(p->vLits);
1189  for ( f = 0; f < p->nFrames; f++ )
1190  {
1191  Beg = 0;
1192  Vec_IntForEachEntry( p->vClauses, End, i )
1193  {
1194  if ( Vec_IntEntry( p->vCosts, i ) == -1 )
1195  {
1196  Beg = End;
1197  continue;
1198  }
1199  assert( Vec_IntEntry( p->vCosts, i ) > 0 );
1200  assert( End - Beg <= p->nLutSize );
1201  // add the clause to all timeframes
1202  RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
1203  if ( RetValue == 0 )
1204  {
1205  printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
1206  return -1;
1207  }
1208  Beg = End;
1209  }
1210  // increment literals
1211  for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
1212  p->vLits->pArray[i] += nLitsTot;
1213  }
1214 
1215  // simplify the solver
1216  if ( p->pSatMain->qtail != p->pSatMain->qhead )
1217  {
1218  RetValue = sat_solver_simplify(p->pSatMain);
1219  assert( RetValue != 0 );
1220  assert( p->pSatMain->qtail == p->pSatMain->qhead );
1221  }
1222 
1223  // check if the property holds
1224  if ( p->fTarget )
1225  {
1226  if ( Fra_ClausRunSat0( p ) )
1227  {
1228  if ( p->fVerbose )
1229  printf( " Property holds. " );
1230  }
1231  else
1232  {
1233  if ( p->fVerbose )
1234  printf( " Property fails. " );
1235  // return -2;
1236  p->fFail = 1;
1237  }
1238  }
1239 
1240 /*
1241  // add the property for the first K frames
1242  for ( i = 0; i < p->nFrames; i++ )
1243  {
1244  Aig_Obj_t * pObj;
1245  int Lits[2];
1246  // set the output literals
1247  pObj = Aig_ManCo(p->pAig, 0);
1248  Lits[0] = i * nLitsTot + toLitCond( p->pCnf->pVarNums[pObj->Id], 1 );
1249  // add the clause
1250  RetValue = sat_solver_addclause( p->pSatMain, Lits, Lits + 1 );
1251 // assert( RetValue == 1 );
1252  if ( RetValue == 0 )
1253  {
1254  printf( "Error: Solver is UNSAT after adding property for the first K frames.\n" );
1255  return -1;
1256  }
1257  }
1258 */
1259 
1260  // simplify the solver
1261  if ( p->pSatMain->qtail != p->pSatMain->qhead )
1262  {
1263  RetValue = sat_solver_simplify(p->pSatMain);
1264  assert( RetValue != 0 );
1265  assert( p->pSatMain->qtail == p->pSatMain->qhead );
1266  }
1267 
1268 
1269  // check the clause in the last timeframe
1270  Beg = 0;
1271  Counter = 0;
1272  Vec_IntForEachEntry( p->vClauses, End, i )
1273  {
1274  if ( Vec_IntEntry( p->vCosts, i ) == -1 )
1275  {
1276  Beg = End;
1277  continue;
1278  }
1279  assert( Vec_IntEntry( p->vCosts, i ) > 0 );
1280  assert( End - Beg <= p->nLutSize );
1281 
1282  if ( Fra_ClausSimInfoCheck(p, pStart + Beg, End - Beg) )
1283  {
1284  fFlag = 1;
1285 // printf( "s-" );
1286 
1287  Beg = End;
1288  Vec_IntWriteEntry( p->vCosts, i, -1 );
1289  Counter++;
1290  continue;
1291  }
1292  else
1293  {
1294  fFlag = 0;
1295 // printf( "s?" );
1296  }
1297 
1298  for ( k = Beg; k < End; k++ )
1299  pStart[k] = lit_neg( pStart[k] );
1300  RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1301  for ( k = Beg; k < End; k++ )
1302  pStart[k] = lit_neg( pStart[k] );
1303 
1304  // the problem is not solved
1305  if ( RetValue != l_False )
1306  {
1307 // printf( "S- " );
1308 // Fra_ClausSimInfoRecord( p, (int*)p->pSatMain->model.ptr + p->nFrames * p->pCnf->nVars );
1309  Fra_ClausSimInfoRecord( p, (int*)p->pSatMain->model + p->nFrames * p->pCnf->nVars );
1310 // RetValue = Fra_ClausSimInfoCheck(p, pStart + Beg, End - Beg);
1311 // assert( RetValue );
1312 
1313  Beg = End;
1314  Vec_IntWriteEntry( p->vCosts, i, -1 );
1315  Counter++;
1316  continue;
1317  }
1318 // printf( "S+ " );
1319 // assert( !fFlag );
1320 
1321 /*
1322  // add the clause
1323  RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
1324 // assert( RetValue == 1 );
1325  if ( RetValue == 0 )
1326  {
1327  printf( "Error: Solver is UNSAT after adding proved clauses.\n" );
1328  return -1;
1329  }
1330 */
1331  Beg = End;
1332 
1333  // simplify the solver
1334  if ( p->pSatMain->qtail != p->pSatMain->qhead )
1335  {
1336  RetValue = sat_solver_simplify(p->pSatMain);
1337  assert( RetValue != 0 );
1338  assert( p->pSatMain->qtail == p->pSatMain->qhead );
1339  }
1340  }
1341 
1342  // return clauses back to normal
1343  nLitsTot = p->nFrames * nLitsTot;
1344  for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
1345  p->vLits->pArray[i] -= nLitsTot;
1346 
1347 // if ( fFail )
1348 // return -2;
1349  return Counter;
1350 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
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 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
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
int Fra_ClausSimInfoCheck(Clu_Man_t *p, int *pLits, int nLits)
Definition: fraClaus.c:1056
void Fra_ClausSimInfoRecord(Clu_Man_t *p, int *pModel)
Definition: fraClaus.c:1028
static lit lit_neg(lit l)
Definition: satVec.h:144
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
void Fra_ClausSimInfoClean(Clu_Man_t *p)
Definition: fraClaus.c:991
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static int Counter
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
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
int Fra_ClausRunSat0(Clu_Man_t *p)
Definition: fraClaus.c:153
#define assert(ex)
Definition: util_old.h:213
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
int nVars
Definition: llb3Image.c:58
void Fra_ClausPrintIndClauses ( Clu_Man_t p)

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

Synopsis [Converts AIG into the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 1483 of file fraClaus.c.

1484 {
1485  int Counters[9] = {0};
1486  int * pStart;
1487  int Beg, End, i;
1488  Beg = 0;
1489  pStart = Vec_IntArray( p->vLitsProven );
1490  Vec_IntForEachEntry( p->vClausesProven, End, i )
1491  {
1492  if ( End - Beg >= 8 )
1493  Counters[8]++;
1494  else
1495  Counters[End - Beg]++;
1496 //printf( "%d ", End-Beg );
1497  Beg = End;
1498  }
1499  printf( "SUMMARY: Total proved clauses = %d. ", Vec_IntSize(p->vClausesProven) );
1500  printf( "Clause per lit: " );
1501  for ( i = 0; i < 8; i++ )
1502  if ( Counters[i] )
1503  printf( "%d=%d ", i, Counters[i] );
1504  if ( Counters[8] )
1505  printf( ">7=%d ", Counters[8] );
1506  printf( "\n" );
1507 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
int Fra_ClausProcessClauses ( Clu_Man_t p,
int  fRefs 
)

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

Synopsis [Processes the clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 601 of file fraClaus.c.

602 {
603  Aig_MmFixed_t * pMemCuts;
604 // Aig_ManCut_t * pManCut;
605  Fra_Sml_t * pComb, * pSeq;
606  Aig_Obj_t * pObj;
607  Dar_Cut_t * pCut;
608  int Scores[16], uScores, i, k, j, nCuts = 0;
609  abctime clk;
610 
611  // simulate the AIG
612 clk = Abc_Clock();
613 // srand( 0xAABBAABB );
614  Aig_ManRandom(1);
615  pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames, 1 );
616  if ( p->fTarget && pSeq->fNonConstOut )
617  {
618  printf( "Property failed after sequential simulation!\n" );
619  Fra_SmlStop( pSeq );
620  return 0;
621  }
622 if ( p->fVerbose )
623 {
624 ABC_PRT( "Sim-seq", Abc_Clock() - clk );
625 }
626 
627 
628 clk = Abc_Clock();
629  if ( fRefs )
630  {
632 if ( p->fVerbose )
633 {
634 ABC_PRT( "Lat-cla", Abc_Clock() - clk );
635 }
636  }
637 
638 
639  // generate cuts for all nodes, assign cost, and find best cuts
640 clk = Abc_Clock();
641  pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 0, 1 );
642 // pManCut = Aig_ComputeCuts( p->pAig, 10, 4, 0, 1 );
643 if ( p->fVerbose )
644 {
645 ABC_PRT( "Cuts ", Abc_Clock() - clk );
646 }
647 
648  // collect sequential info for each cut
649 clk = Abc_Clock();
650  Aig_ManForEachNode( p->pAig, pObj, i )
651  Dar_ObjForEachCut( pObj, pCut, k )
652  if ( pCut->nLeaves > 1 )
653  {
654  pCut->uTruth = Fra_ClausProcessClausesCut( p, pSeq, pCut, Scores );
655 // uScores = Fra_ClausProcessClausesCut2( p, pSeq, pCut, Scores );
656 // if ( uScores != pCut->uTruth )
657 // {
658 // int x = 0;
659 // }
660  }
661 if ( p->fVerbose )
662 {
663 ABC_PRT( "Infoseq", Abc_Clock() - clk );
664 }
665  Fra_SmlStop( pSeq );
666 
667  // perform combinational simulation
668 clk = Abc_Clock();
669 // srand( 0xAABBAABB );
670  Aig_ManRandom(1);
671  pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref, 0 );
672 if ( p->fVerbose )
673 {
674 ABC_PRT( "Sim-cmb", Abc_Clock() - clk );
675 }
676 
677  // collect combinational info for each cut
678 clk = Abc_Clock();
679  Aig_ManForEachNode( p->pAig, pObj, i )
680  Dar_ObjForEachCut( pObj, pCut, k )
681  if ( pCut->nLeaves > 1 )
682  {
683  nCuts++;
684  uScores = Fra_ClausProcessClausesCut( p, pComb, pCut, Scores );
685  uScores &= ~pCut->uTruth; pCut->uTruth = 0;
686  if ( uScores == 0 )
687  continue;
688  // write the clauses
689  for ( j = 0; j < (1<<pCut->nLeaves); j++ )
690  if ( uScores & (1 << j) )
691  Fra_ClausRecordClause( p, pCut, j, Scores[j] );
692 
693  }
694  Fra_SmlStop( pComb );
695  Aig_MmFixedStop( pMemCuts, 0 );
696 // Aig_ManCutStop( pManCut );
697 if ( p->fVerbose )
698 {
699 ABC_PRT( "Infocmb", Abc_Clock() - clk );
700 }
701 
702  if ( p->fVerbose )
703  printf( "Node = %5d. Non-triv cuts = %7d. Clauses = %6d. Clause per cut = %6.2f.\n",
704  Aig_ManNodeNum(p->pAig), nCuts, Vec_IntSize(p->vClauses), 1.0*Vec_IntSize(p->vClauses)/nCuts );
705 
706  if ( Vec_IntSize(p->vClauses) > p->nClausesMax )
708  else
709  p->nClauses = Vec_IntSize( p->vClauses );
710  return 1;
711 }
int fNonConstOut
Definition: fra.h:179
Aig_Man_t * pAig
Definition: llb3Image.c:49
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Fra_Sml_t * Fra_SmlSimulateSeq(Aig_Man_t *pAig, int nPref, int nFrames, int nWords, int fCheckMiter)
Definition: fraSim.c:1021
void Fra_ClausRecordClause(Clu_Man_t *p, Dar_Cut_t *pCut, int iMint, int Cost)
Definition: fraClaus.c:405
void Aig_MmFixedStop(Aig_MmFixed_t *p, int fVerbose)
Definition: aigMem.c:132
unsigned Aig_ManRandom(int fReset)
Definition: aigUtil.c:1157
static abctime Abc_Clock()
Definition: abc_global.h:279
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
int Fra_ClausSelectClauses(Clu_Man_t *p)
Definition: fraClaus.c:350
DECLARATIONS ///.
Definition: aigMem.c:30
Aig_MmFixed_t * Dar_ManComputeCuts(Aig_Man_t *pAig, int nCutsMax, int fSkipTtMin, int fVerbose)
Definition: darCore.c:287
#define Dar_ObjForEachCut(pObj, pCut, i)
Definition: darInt.h:121
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Fra_Sml_t * Fra_SmlSimulateComb(Aig_Man_t *pAig, int nWords, int fCheckMiter)
Definition: fraSim.c:856
int Fra_ClausProcessClausesCut(Clu_Man_t *p, Fra_Sml_t *pSimMan, Dar_Cut_t *pCut, int *pScores)
Definition: fraClaus.c:202
if(last==0)
Definition: sparse_int.h:34
Definition: aig.h:69
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define ABC_PRT(a, t)
Definition: abc_global.h:220
int Fra_ClausCollectLatchClauses(Clu_Man_t *p, Fra_Sml_t *pSeq)
Definition: fraClaus.c:513
ABC_INT64_T abctime
Definition: abc_global.h:278
void Fra_SmlStop(Fra_Sml_t *p)
Definition: fraSim.c:839
int Fra_ClausProcessClauses2 ( Clu_Man_t p,
int  fRefs 
)

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

Synopsis [Processes the clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 724 of file fraClaus.c.

725 {
726 // Aig_MmFixed_t * pMemCuts;
727  Aig_ManCut_t * pManCut;
728  Fra_Sml_t * pComb, * pSeq;
729  Aig_Obj_t * pObj;
730  Aig_Cut_t * pCut;
731  int i, k, j, nCuts = 0;
732  abctime clk;
733  int ScoresSeq[1<<12], ScoresComb[1<<12];
734  assert( p->nLutSize < 13 );
735 
736  // simulate the AIG
737 clk = Abc_Clock();
738 // srand( 0xAABBAABB );
739  Aig_ManRandom(1);
740  pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames, 1 );
741  if ( p->fTarget && pSeq->fNonConstOut )
742  {
743  printf( "Property failed after sequential simulation!\n" );
744  Fra_SmlStop( pSeq );
745  return 0;
746  }
747 if ( p->fVerbose )
748 {
749 //ABC_PRT( "Sim-seq", Abc_Clock() - clk );
750 }
751 
752  // perform combinational simulation
753 clk = Abc_Clock();
754 // srand( 0xAABBAABB );
755  Aig_ManRandom(1);
756  pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref, 0 );
757 if ( p->fVerbose )
758 {
759 //ABC_PRT( "Sim-cmb", Abc_Clock() - clk );
760 }
761 
762 
763 clk = Abc_Clock();
764  if ( fRefs )
765  {
767 if ( p->fVerbose )
768 {
769 //ABC_PRT( "Lat-cla", Abc_Clock() - clk );
770 }
771  }
772 
773 
774  // generate cuts for all nodes, assign cost, and find best cuts
775 clk = Abc_Clock();
776 // pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 0, 1 );
777  pManCut = Aig_ComputeCuts( p->pAig, p->nCutsMax, p->nLutSize, 0, p->fVerbose );
778 if ( p->fVerbose )
779 {
780 //ABC_PRT( "Cuts ", Abc_Clock() - clk );
781 }
782 
783  // collect combinational info for each cut
784 clk = Abc_Clock();
785  Aig_ManForEachNode( p->pAig, pObj, i )
786  {
787  if ( pObj->Level > (unsigned)p->nLevels )
788  continue;
789  Aig_ObjForEachCut( pManCut, pObj, pCut, k )
790  if ( pCut->nFanins > 1 )
791  {
792  nCuts++;
793  Fra_ClausProcessClausesCut3( p, pSeq, pCut, ScoresSeq );
794  Fra_ClausProcessClausesCut3( p, pComb, pCut, ScoresComb );
795  // write the clauses
796  for ( j = 0; j < (1<<pCut->nFanins); j++ )
797  if ( ScoresComb[j] != 0 && ScoresSeq[j] == 0 )
798  Fra_ClausRecordClause2( p, pCut, j, ScoresComb[j] );
799 
800  }
801  }
802  Fra_SmlStop( pSeq );
803  Fra_SmlStop( pComb );
804  p->nCuts = nCuts;
805 // Aig_MmFixedStop( pMemCuts, 0 );
806  Aig_ManCutStop( pManCut );
807  p->pAig->pManCuts = NULL;
808 
809  if ( p->fVerbose )
810  {
811  printf( "Node = %5d. Cuts = %7d. Clauses = %6d. Clause/cut = %6.2f.\n",
812  Aig_ManNodeNum(p->pAig), nCuts, Vec_IntSize(p->vClauses), 1.0*Vec_IntSize(p->vClauses)/nCuts );
813  ABC_PRT( "Processing sim-info to find candidate clauses (unoptimized)", Abc_Clock() - clk );
814  }
815 
816  // filter out clauses that are contained in the already proven clauses
817  assert( p->nClauses == 0 );
818  p->nClauses = Vec_IntSize( p->vClauses );
819  if ( Vec_IntSize( p->vClausesProven ) > 0 )
820  {
821  int RetValue, k, Beg;
822  int End = -1; // Suppress "might be used uninitialized"
823  int * pStart;
824  // reset the solver
825  if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
826  p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
827  if ( p->pSatMain == NULL )
828  {
829  printf( "Error: Main solver is unsat.\n" );
830  return -1;
831  }
832 
833  // add the proven clauses
834  Beg = 0;
835  pStart = Vec_IntArray(p->vLitsProven);
836  Vec_IntForEachEntry( p->vClausesProven, End, i )
837  {
838  assert( End - Beg <= p->nLutSize );
839  // add the clause to all timeframes
840  RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
841  if ( RetValue == 0 )
842  {
843  printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
844  return -1;
845  }
846  Beg = End;
847  }
848  assert( End == Vec_IntSize(p->vLitsProven) );
849 
850  // check the clauses
851  Beg = 0;
852  pStart = Vec_IntArray(p->vLits);
853  Vec_IntForEachEntry( p->vClauses, End, i )
854  {
855  assert( Vec_IntEntry( p->vCosts, i ) >= 0 );
856  assert( End - Beg <= p->nLutSize );
857  // check the clause
858  for ( k = Beg; k < End; k++ )
859  pStart[k] = lit_neg( pStart[k] );
860  RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
861  for ( k = Beg; k < End; k++ )
862  pStart[k] = lit_neg( pStart[k] );
863  // the clause holds
864  if ( RetValue == l_False )
865  {
866  Vec_IntWriteEntry( p->vCosts, i, -1 );
867  p->nClauses--;
868  }
869  Beg = End;
870  }
871  assert( End == Vec_IntSize(p->vLits) );
872  if ( p->fVerbose )
873  printf( "Already proved clauses filtered out %d candidate clauses (out of %d).\n",
874  Vec_IntSize(p->vClauses) - p->nClauses, Vec_IntSize(p->vClauses) );
875  }
876 
877  p->fFiltering = 0;
878  if ( p->nClauses > p->nClausesMax )
879  {
881  p->fFiltering = 1;
882  }
883  return 1;
884 }
int fNonConstOut
Definition: fra.h:179
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
unsigned Level
Definition: aig.h:82
Aig_Man_t * pAig
Definition: llb3Image.c:49
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Fra_Sml_t * Fra_SmlSimulateSeq(Aig_Man_t *pAig, int nPref, int nFrames, int nWords, int fCheckMiter)
Definition: fraSim.c:1021
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
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
unsigned Aig_ManRandom(int fReset)
Definition: aigUtil.c:1157
static abctime Abc_Clock()
Definition: abc_global.h:279
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
void Fra_ClausProcessClausesCut3(Clu_Man_t *p, Fra_Sml_t *pSimMan, Aig_Cut_t *pCut, int *pScores)
Definition: fraClaus.c:290
int Fra_ClausSelectClauses(Clu_Man_t *p)
Definition: fraClaus.c:350
void Aig_ManCutStop(Aig_ManCut_t *p)
Definition: aigCuts.c:86
static lit lit_neg(lit l)
Definition: satVec.h:144
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
void Fra_ClausRecordClause2(Clu_Man_t *p, Aig_Cut_t *pCut, int iMint, int Cost)
Definition: fraClaus.c:425
Aig_ManCut_t * Aig_ComputeCuts(Aig_Man_t *pAig, int nCutsMax, int nLeafMax, int fTruth, int fVerbose)
Definition: aigCuts.c:631
Fra_Sml_t * Fra_SmlSimulateComb(Aig_Man_t *pAig, int nWords, int fCheckMiter)
Definition: fraSim.c:856
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
if(last==0)
Definition: sparse_int.h:34
Definition: aig.h:69
char nFanins
Definition: aig.h:187
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 ABC_PRT(a, t)
Definition: abc_global.h:220
#define l_False
Definition: SolverTypes.h:85
int Fra_ClausCollectLatchClauses(Clu_Man_t *p, Fra_Sml_t *pSeq)
Definition: fraClaus.c:513
#define assert(ex)
Definition: util_old.h:213
ABC_INT64_T abctime
Definition: abc_global.h:278
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
#define Aig_ObjForEachCut(p, pObj, pCut, i)
Definition: aig.h:218
void Fra_SmlStop(Fra_Sml_t *p)
Definition: fraSim.c:839
int Fra_ClausProcessClausesCut ( Clu_Man_t p,
Fra_Sml_t pSimMan,
Dar_Cut_t pCut,
int *  pScores 
)

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

Synopsis [Return combinations appearing in the cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 202 of file fraClaus.c.

203 {
204  unsigned Matrix[32];
205  unsigned * pSims[16], uWord;
206  int nSeries, i, k, j;
207  int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
208  // compute parameters
209  assert( pCut->nLeaves > 1 && pCut->nLeaves < 5 );
210  assert( nWordsForSim % 8 == 0 );
211  // get parameters
212  for ( i = 0; i < (int)pCut->nLeaves; i++ )
213  pSims[i] = Fra_ObjSim( pSimMan, pCut->pLeaves[i] ) + p->nSimWordsPref;
214  // add combinational patterns
215  memset( pScores, 0, sizeof(int) * 16 );
216  nSeries = nWordsForSim / 8;
217  for ( i = 0; i < nSeries; i++ )
218  {
219  memset( Matrix, 0, sizeof(unsigned) * 32 );
220  for ( k = 0; k < 8; k++ )
221  for ( j = 0; j < (int)pCut->nLeaves; j++ )
222  Matrix[31-(k*4+j)] = pSims[j][i*8+k];
223  transpose32a( Matrix );
224  for ( k = 0; k < 32; k++ )
225  for ( j = 0, uWord = Matrix[k]; j < 8; j++, uWord >>= 4 )
226  pScores[uWord & 0xF]++;
227  }
228  // collect patterns
229  uWord = 0;
230  for ( i = 0; i < 16; i++ )
231  if ( pScores[i] )
232  uWord |= (1 << i);
233 // Extra_PrintBinary( stdout, &uWord, 16 ); printf( "\n" );
234  return (int)uWord;
235 }
char * memset()
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int nWordsTotal
Definition: fra.h:177
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
int pLeaves[4]
Definition: darInt.h:63
void transpose32a(unsigned a[32])
Definition: fraClaus.c:176
unsigned nLeaves
Definition: darInt.h:62
#define assert(ex)
Definition: util_old.h:213
int Fra_ClausProcessClausesCut2 ( Clu_Man_t p,
Fra_Sml_t pSimMan,
Dar_Cut_t pCut,
int *  pScores 
)

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

Synopsis [Return combinations appearing in the cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 248 of file fraClaus.c.

249 {
250  unsigned * pSims[16], uWord;
251  int iMint, i, k, b;
252  int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
253  // compute parameters
254  assert( pCut->nLeaves > 1 && pCut->nLeaves < 5 );
255  assert( nWordsForSim % 8 == 0 );
256  // get parameters
257  for ( i = 0; i < (int)pCut->nLeaves; i++ )
258  pSims[i] = Fra_ObjSim( pSimMan, pCut->pLeaves[i] ) + p->nSimWordsPref;
259  // add combinational patterns
260  memset( pScores, 0, sizeof(int) * 16 );
261  for ( i = 0; i < nWordsForSim; i++ )
262  for ( k = 0; k < 32; k++ )
263  {
264  iMint = 0;
265  for ( b = 0; b < (int)pCut->nLeaves; b++ )
266  if ( pSims[b][i] & (1 << k) )
267  iMint |= (1 << b);
268  pScores[iMint]++;
269  }
270  // collect patterns
271  uWord = 0;
272  for ( i = 0; i < 16; i++ )
273  if ( pScores[i] )
274  uWord |= (1 << i);
275 // Extra_PrintBinary( stdout, &uWord, 16 ); printf( "\n" );
276  return (int)uWord;
277 }
char * memset()
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int nWordsTotal
Definition: fra.h:177
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
int pLeaves[4]
Definition: darInt.h:63
unsigned nLeaves
Definition: darInt.h:62
#define assert(ex)
Definition: util_old.h:213
void Fra_ClausProcessClausesCut3 ( Clu_Man_t p,
Fra_Sml_t pSimMan,
Aig_Cut_t pCut,
int *  pScores 
)

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

Synopsis [Return the number of combinations appearing in the cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 290 of file fraClaus.c.

291 {
292  unsigned Matrix[32];
293  unsigned * pSims[16], uWord;
294  int iMint, i, j, k, b, nMints, nSeries;
295  int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
296 
297  // compute parameters
298  assert( pCut->nFanins > 1 && pCut->nFanins < 17 );
299  assert( nWordsForSim % 8 == 0 );
300  // get parameters
301  for ( i = 0; i < (int)pCut->nFanins; i++ )
302  pSims[i] = Fra_ObjSim( pSimMan, pCut->pFanins[i] ) + p->nSimWordsPref;
303  // add combinational patterns
304  nMints = (1 << pCut->nFanins);
305  memset( pScores, 0, sizeof(int) * nMints );
306 
307  if ( pCut->nLeafMax == 4 )
308  {
309  // convert the simulation patterns
310  nSeries = nWordsForSim / 8;
311  for ( i = 0; i < nSeries; i++ )
312  {
313  memset( Matrix, 0, sizeof(unsigned) * 32 );
314  for ( k = 0; k < 8; k++ )
315  for ( j = 0; j < (int)pCut->nFanins; j++ )
316  Matrix[31-(k*4+j)] = pSims[j][i*8+k];
317  transpose32a( Matrix );
318  for ( k = 0; k < 32; k++ )
319  for ( j = 0, uWord = Matrix[k]; j < 8; j++, uWord >>= 4 )
320  pScores[uWord & 0xF]++;
321  }
322  }
323  else
324  {
325  // go through the simulation patterns
326  for ( i = 0; i < nWordsForSim; i++ )
327  for ( k = 0; k < 32; k++ )
328  {
329  iMint = 0;
330  for ( b = 0; b < (int)pCut->nFanins; b++ )
331  if ( pSims[b][i] & (1 << k) )
332  iMint |= (1 << b);
333  pScores[iMint]++;
334  }
335  }
336 }
char * memset()
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int nWordsTotal
Definition: fra.h:177
char nLeafMax
Definition: aig.h:186
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
void transpose32a(unsigned a[32])
Definition: fraClaus.c:176
char nFanins
Definition: aig.h:187
int pFanins[0]
Definition: aig.h:188
#define assert(ex)
Definition: util_old.h:213
void Fra_ClausRecordClause ( Clu_Man_t p,
Dar_Cut_t pCut,
int  iMint,
int  Cost 
)

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

Synopsis [Processes the clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 405 of file fraClaus.c.

406 {
407  int i;
408  for ( i = 0; i < (int)pCut->nLeaves; i++ )
409  Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pCut->pLeaves[i]], (iMint&(1<<i)) ) );
410  Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
411  Vec_IntPush( p->vCosts, Cost );
412 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int pLeaves[4]
Definition: darInt.h:63
static lit toLitCond(int v, int c)
Definition: satVec.h:143
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
unsigned nLeaves
Definition: darInt.h:62
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
void Fra_ClausRecordClause2 ( Clu_Man_t p,
Aig_Cut_t pCut,
int  iMint,
int  Cost 
)

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

Synopsis [Processes the clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 425 of file fraClaus.c.

426 {
427  int i;
428  for ( i = 0; i < (int)pCut->nFanins; i++ )
429  Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pCut->pFanins[i]], (iMint&(1<<i)) ) );
430  Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
431  Vec_IntPush( p->vCosts, Cost );
432 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static lit toLitCond(int v, int c)
Definition: satVec.h:143
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
char nFanins
Definition: aig.h:187
int pFanins[0]
Definition: aig.h:188
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
int Fra_ClausRunBmc ( Clu_Man_t p)

FUNCTION DEFINITIONS ///.

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

Synopsis [Runs the SAT solver on the problem.]

Description []

SideEffects []

SeeAlso []

Definition at line 94 of file fraClaus.c.

95 {
96  Aig_Obj_t * pObj;
97  int Lits[2], nLitsTot, RetValue, i;
98  // set the output literals
99  nLitsTot = 2 * p->pCnf->nVars;
100  pObj = Aig_ManCo(p->pAig, 0);
101  for ( i = 0; i < p->nPref + p->nFrames; i++ )
102  {
103  Lits[0] = i * nLitsTot + toLitCond( p->pCnf->pVarNums[pObj->Id], 0 );
104  RetValue = sat_solver_solve( p->pSatBmc, Lits, Lits + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
105  if ( RetValue != l_False )
106  return 0;
107  }
108  return 1;
109 }
Aig_Man_t * pAig
Definition: llb3Image.c:49
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 lit toLitCond(int v, int c)
Definition: satVec.h:143
Definition: aig.h:69
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
#define l_False
Definition: SolverTypes.h:85
int Id
Definition: aig.h:85
int nVars
Definition: llb3Image.c:58
int Fra_ClausRunSat ( Clu_Man_t p)

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

Synopsis [Runs the SAT solver on the problem.]

Description []

SideEffects []

SeeAlso []

Definition at line 122 of file fraClaus.c.

123 {
124  Aig_Obj_t * pObj;
125  int * pLits;
126  int i, RetValue;
127  pLits = ABC_ALLOC( int, p->nFrames + 1 );
128  // set the output literals
129  pObj = Aig_ManCo(p->pAig, 0);
130  for ( i = 0; i <= p->nFrames; i++ )
131  pLits[i] = i * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObj->Id], i != p->nFrames );
132  // try to solve the problem
133  RetValue = sat_solver_solve( p->pSatMain, pLits, pLits + p->nFrames + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
134  ABC_FREE( pLits );
135  if ( RetValue == l_False )
136  return 1;
137  // get the counter-example
138  assert( RetValue == l_True );
139  return 0;
140 }
Aig_Man_t * pAig
Definition: llb3Image.c:49
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
#define l_True
Definition: SolverTypes.h:84
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
static lit toLitCond(int v, int c)
Definition: satVec.h:143
Definition: aig.h:69
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
#define ABC_FREE(obj)
Definition: abc_global.h:232
#define l_False
Definition: SolverTypes.h:85
#define assert(ex)
Definition: util_old.h:213
int Id
Definition: aig.h:85
int nVars
Definition: llb3Image.c:58
int Fra_ClausRunSat0 ( Clu_Man_t p)

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

Synopsis [Runs the SAT solver on the problem.]

Description []

SideEffects []

SeeAlso []

Definition at line 153 of file fraClaus.c.

154 {
155  Aig_Obj_t * pObj;
156  int Lits[2], RetValue;
157  pObj = Aig_ManCo(p->pAig, 0);
158  Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 0 );
159  RetValue = sat_solver_solve( p->pSatMain, Lits, Lits + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
160  if ( RetValue == l_False )
161  return 1;
162  return 0;
163 }
Aig_Man_t * pAig
Definition: llb3Image.c:49
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 lit toLitCond(int v, int c)
Definition: satVec.h:143
Definition: aig.h:69
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
#define l_False
Definition: SolverTypes.h:85
int Id
Definition: aig.h:85
int Fra_ClausSelectClauses ( Clu_Man_t p)

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

Synopsis [Returns the cut-off cost.]

Description []

SideEffects []

SeeAlso []

Definition at line 350 of file fraClaus.c.

351 {
352  int * pCostCount, nClauCount, Cost, CostMax, i, c;
353  assert( Vec_IntSize(p->vClauses) > p->nClausesMax );
354  // count how many implications have each cost
355  CostMax = p->nSimWords * 32 + 1;
356  pCostCount = ABC_ALLOC( int, CostMax );
357  memset( pCostCount, 0, sizeof(int) * CostMax );
358  Vec_IntForEachEntry( p->vCosts, Cost, i )
359  {
360  if ( Cost == -1 )
361  continue;
362  assert( Cost < CostMax );
363  pCostCount[ Cost ]++;
364  }
365  assert( pCostCount[0] == 0 );
366  // select the bound on the cost (above this bound, implication will be included)
367  nClauCount = 0;
368  for ( c = CostMax - 1; c > 0; c-- )
369  {
370  assert( pCostCount[c] >= 0 );
371  nClauCount += pCostCount[c];
372  if ( nClauCount >= p->nClausesMax )
373  break;
374  }
375  // collect implications with the given costs
376  nClauCount = 0;
377  Vec_IntForEachEntry( p->vCosts, Cost, i )
378  {
379  if ( Cost >= c && nClauCount < p->nClausesMax )
380  {
381  nClauCount++;
382  continue;
383  }
384  Vec_IntWriteEntry( p->vCosts, i, -1 );
385  }
386  ABC_FREE( pCostCount );
387  p->nClauses = nClauCount;
388 if ( p->fVerbose )
389 printf( "Selected %d clauses. Cost range: [%d < %d < %d]\n", nClauCount, 1, c, CostMax );
390  return c;
391 }
char * memset()
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define ABC_FREE(obj)
Definition: abc_global.h:232
#define assert(ex)
Definition: util_old.h:213
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
int Fra_ClausSimInfoCheck ( Clu_Man_t p,
int *  pLits,
int  nLits 
)

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

Synopsis [Uses the simulation info.]

Description [Returns 1 if the simulation info disproved the clause.]

SideEffects []

SeeAlso []

Definition at line 1056 of file fraClaus.c.

1057 {
1058  unsigned * pSims[16], uWord;
1059  int nWords, iVar, i, w;
1060  for ( i = 0; i < nLits; i++ )
1061  {
1062  iVar = lit_var(pLits[i]) - p->nFrames * p->pCnf->nVars;
1063  assert( iVar > 0 && iVar < p->pCnf->nVars );
1064  pSims[i] = (unsigned *)Vec_PtrEntry( p->vCexes, iVar );
1065  }
1066  nWords = p->nCexes / 32;
1067  for ( w = 0; w < nWords; w++ )
1068  {
1069  uWord = ~(unsigned)0;
1070  for ( i = 0; i < nLits; i++ )
1071  uWord &= (lit_sign(pLits[i])? pSims[i][w] : ~pSims[i][w]);
1072  if ( uWord )
1073  return 1;
1074  }
1075  if ( p->nCexes % 32 )
1076  {
1077  uWord = ~(unsigned)0;
1078  for ( i = 0; i < nLits; i++ )
1079  uWord &= (lit_sign(pLits[i])? pSims[i][w] : ~pSims[i][w]);
1080  if ( uWord & Abc_InfoMask( p->nCexes % 32 ) )
1081  return 1;
1082  }
1083  return 0;
1084 }
static unsigned Abc_InfoMask(int nVar)
Definition: abc_global.h:261
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int lit_var(lit l)
Definition: satVec.h:145
int nWords
Definition: abcNpn.c:127
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static int lit_sign(lit l)
Definition: satVec.h:146
#define assert(ex)
Definition: util_old.h:213
int nVars
Definition: llb3Image.c:58
void Fra_ClausSimInfoClean ( Clu_Man_t p)

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

Synopsis [Cleans simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 991 of file fraClaus.c.

992 {
993  assert( p->pCnf->nVars <= Vec_PtrSize(p->vCexes) );
994  Vec_PtrCleanSimInfo( p->vCexes, 0, p->nCexesAlloc/32 );
995  p->nCexes = 0;
996 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static void Vec_PtrCleanSimInfo(Vec_Ptr_t *vInfo, int iWord, int nWords)
Definition: vecPtr.h:968
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
#define assert(ex)
Definition: util_old.h:213
int nVars
Definition: llb3Image.c:58
void Fra_ClausSimInfoRealloc ( Clu_Man_t p)

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

Synopsis [Reallocs simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 1009 of file fraClaus.c.

1010 {
1011  assert( p->nCexes == p->nCexesAlloc );
1012  Vec_PtrReallocSimInfo( p->vCexes );
1013  Vec_PtrCleanSimInfo( p->vCexes, p->nCexesAlloc/32, 2 * p->nCexesAlloc/32 );
1014  p->nCexesAlloc *= 2;
1015 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static void Vec_PtrCleanSimInfo(Vec_Ptr_t *vInfo, int iWord, int nWords)
Definition: vecPtr.h:968
static void Vec_PtrReallocSimInfo(Vec_Ptr_t *vInfo)
Definition: vecPtr.h:1035
#define assert(ex)
Definition: util_old.h:213
void Fra_ClausSimInfoRecord ( Clu_Man_t p,
int *  pModel 
)

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

Synopsis [Records simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 1028 of file fraClaus.c.

1029 {
1030  int i;
1031  if ( p->nCexes == p->nCexesAlloc )
1033  assert( p->nCexes < p->nCexesAlloc );
1034  for ( i = 0; i < p->pCnf->nVars; i++ )
1035  {
1036  if ( pModel[i] == l_True )
1037  {
1038  assert( Abc_InfoHasBit( (unsigned *)Vec_PtrEntry(p->vCexes, i), p->nCexes ) == 0 );
1039  Abc_InfoSetBit( (unsigned *)Vec_PtrEntry(p->vCexes, i), p->nCexes );
1040  }
1041  }
1042  p->nCexes++;
1043 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
#define l_True
Definition: SolverTypes.h:84
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
#define assert(ex)
Definition: util_old.h:213
void Fra_ClausSimInfoRealloc(Clu_Man_t *p)
Definition: fraClaus.c:1009
int nVars
Definition: llb3Image.c:58
int Fra_ClausSmlNodeIsConst ( Fra_Sml_t pSeq,
Aig_Obj_t pObj 
)

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

Synopsis [Returns 1 if simulation info is composed of all zeros.]

Description []

SideEffects []

SeeAlso []

Definition at line 445 of file fraClaus.c.

446 {
447  unsigned * pSims;
448  int i;
449  pSims = Fra_ObjSim(pSeq, pObj->Id);
450  for ( i = pSeq->nWordsPref; i < pSeq->nWordsTotal; i++ )
451  if ( pSims[i] )
452  return 0;
453  return 1;
454 }
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
int nWordsPref
Definition: fra.h:178
int Id
Definition: aig.h:85
int Fra_ClausSmlNodesAreImp ( Fra_Sml_t pSeq,
Aig_Obj_t pObj1,
Aig_Obj_t pObj2 
)

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

Synopsis [Returns 1 if implications holds.]

Description []

SideEffects []

SeeAlso []

Definition at line 467 of file fraClaus.c.

468 {
469  unsigned * pSimL, * pSimR;
470  int k;
471  pSimL = Fra_ObjSim(pSeq, pObj1->Id);
472  pSimR = Fra_ObjSim(pSeq, pObj2->Id);
473  for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ )
474  if ( pSimL[k] & ~pSimR[k] ) // !(Obj1 -> Obj2)
475  return 0;
476  return 1;
477 }
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
int nWordsPref
Definition: fra.h:178
int Id
Definition: aig.h:85
int Fra_ClausSmlNodesAreImpC ( Fra_Sml_t pSeq,
Aig_Obj_t pObj1,
Aig_Obj_t pObj2 
)

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

Synopsis [Returns 1 if implications holds.]

Description []

SideEffects []

SeeAlso []

Definition at line 490 of file fraClaus.c.

491 {
492  unsigned * pSimL, * pSimR;
493  int k;
494  pSimL = Fra_ObjSim(pSeq, pObj1->Id);
495  pSimR = Fra_ObjSim(pSeq, pObj2->Id);
496  for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ )
497  if ( pSimL[k] & pSimR[k] )
498  return 0;
499  return 1;
500 }
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
int nWordsPref
Definition: fra.h:178
int Id
Definition: aig.h:85
void Fra_ClausWriteIndClauses ( Clu_Man_t p)

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

Synopsis [Writes the clauses into an AIGER file.]

Description []

SideEffects []

SeeAlso []

Definition at line 1540 of file fraClaus.c.

1541 {
1542  extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
1543  Aig_Man_t * pNew;
1544  Aig_Obj_t * pClause, * pLiteral;
1545  char * pName;
1546  int * pStart, * pVar2Id;
1547  int Beg, End, i, k;
1548  // create mapping from SAT vars to node IDs
1549  pVar2Id = ABC_ALLOC( int, p->pCnf->nVars );
1550  memset( pVar2Id, 0xFF, sizeof(int) * p->pCnf->nVars );
1551  for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
1552  if ( p->pCnf->pVarNums[i] >= 0 )
1553  {
1554  assert( p->pCnf->pVarNums[i] < p->pCnf->nVars );
1555  pVar2Id[ p->pCnf->pVarNums[i] ] = i;
1556  }
1557  // start the manager
1558  pNew = Aig_ManDupWithoutPos( p->pAig );
1559  // add the clauses
1560  Beg = 0;
1561  pStart = Vec_IntArray( p->vLitsProven );
1562  Vec_IntForEachEntry( p->vClausesProven, End, i )
1563  {
1564  pClause = Fra_ClausGetLiteral( p, pVar2Id, pStart[Beg] );
1565  for ( k = Beg + 1; k < End; k++ )
1566  {
1567  pLiteral = Fra_ClausGetLiteral( p, pVar2Id, pStart[k] );
1568  pClause = Aig_Or( pNew, pClause, pLiteral );
1569  }
1570  Aig_ObjCreateCo( pNew, pClause );
1571  Beg = End;
1572  }
1573  ABC_FREE( pVar2Id );
1574  Aig_ManCleanup( pNew );
1575  pName = Ioa_FileNameGenericAppend( p->pAig->pName, "_care.aig" );
1576  printf( "Care one-hotness clauses will be written into file \"%s\".\n", pName );
1577  Ioa_WriteAiger( pNew, pName, 0, 1 );
1578  Aig_ManStop( pNew );
1579 }
char * memset()
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Aig_Man_t * pAig
Definition: llb3Image.c:49
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
char * Ioa_FileNameGenericAppend(char *pBase, char *pSuffix)
Definition: ioaUtil.c:93
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:259
Definition: aig.h:69
void Ioa_WriteAiger(Aig_Man_t *pMan, char *pFileName, int fWriteSymbols, int fCompact)
Definition: ioaWriteAig.c:446
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Aig_Obj_t * Fra_ClausGetLiteral(Clu_Man_t *p, int *pVar2Id, int Lit)
Definition: fraClaus.c:1520
#define ABC_FREE(obj)
Definition: abc_global.h:232
#define assert(ex)
Definition: util_old.h:213
Aig_Man_t * Aig_ManDupWithoutPos(Aig_Man_t *p)
Definition: aigDup.c:835
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
int nVars
Definition: llb3Image.c:58
void transpose32a ( unsigned  a[32])

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

Synopsis [Return combinations appearing in the cut.]

Description [This procedure is taken from "Hacker's Delight" by H.S.Warren.]

SideEffects []

SeeAlso []

Definition at line 176 of file fraClaus.c.

177 {
178  int j, k;
179  unsigned long m, t;
180  for ( j = 16, m = 0x0000FFFF; j; j >>= 1, m ^= m << j )
181  {
182  for ( k = 0; k < 32; k = ((k | j) + 1) & ~j )
183  {
184  t = (a[k] ^ (a[k|j] >> j)) & m;
185  a[k] ^= t;
186  a[k|j] ^= (t << j);
187  }
188  }
189 }