mirror of https://github.com/YosysHQ/abc.git
465 lines
18 KiB
C
465 lines
18 KiB
C
/**CFile****************************************************************
|
|
|
|
FileName [sbd.c]
|
|
|
|
SystemName [ABC: Logic synthesis and verification system.]
|
|
|
|
PackageName [SAT-based optimization using internal don't-cares.]
|
|
|
|
Synopsis []
|
|
|
|
Author [Alan Mishchenko]
|
|
|
|
Affiliation [UC Berkeley]
|
|
|
|
Date [Ver. 1.0. Started - June 20, 2005.]
|
|
|
|
Revision [$Id: sbd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
|
|
|
***********************************************************************/
|
|
|
|
#include "sbdInt.h"
|
|
|
|
ABC_NAMESPACE_IMPL_START
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// DECLARATIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// FUNCTION DEFINITIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Constructs SAT solver for the window.]
|
|
|
|
Description [The window for the pivot node (Pivot) is represented as
|
|
a DFS ordered array of objects (vWinObjs) whose indexed in the array
|
|
(which will be used as SAT variables) are given in array vObj2Var.
|
|
The TFO nodes are listed as the last ones in vWinObjs. The root nodes
|
|
are labeled with Abc_LitIsCompl() in vTfo and also given in vRoots.
|
|
If fQbf is 1, returns the instance meant for QBF solving. It is using
|
|
the last variable (LastVar) as the placeholder for the second copy
|
|
of the pivot node.]
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors,
|
|
int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var,
|
|
Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf )
|
|
{
|
|
Gia_Obj_t * pObj;
|
|
int i, iLit = 1, iObj, Fan0, Fan1, Lit0m, Lit1m, Node, fCompl0, fCompl1, RetValue;
|
|
int TfoStart = Vec_IntSize(vWinObjs) - Vec_IntSize(vTfo);
|
|
int PivotVar = Vec_IntEntry(vObj2Var, Pivot);
|
|
int LastVar = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots);
|
|
//Vec_IntPrint( vWinObjs );
|
|
//Vec_IntPrint( vTfo );
|
|
//Vec_IntPrint( vRoots );
|
|
// create SAT solver
|
|
if ( pSat == NULL )
|
|
pSat = sat_solver_new();
|
|
else
|
|
sat_solver_restart( pSat );
|
|
sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + SBD_FVAR_MAX );
|
|
// create constant 0 clause
|
|
sat_solver_addclause( pSat, &iLit, &iLit + 1 );
|
|
// add clauses for all nodes
|
|
Vec_IntForEachEntryStart( vWinObjs, iObj, i, 1 )
|
|
{
|
|
pObj = Gia_ManObj( p, iObj );
|
|
if ( Gia_ObjIsCi(pObj) )
|
|
continue;
|
|
assert( Gia_ObjIsAnd(pObj) );
|
|
assert( Vec_IntEntry( vMirrors, iObj ) < 0 );
|
|
Node = Vec_IntEntry( vObj2Var, iObj );
|
|
Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, iObj) );
|
|
Lit1m = Vec_IntEntry( vMirrors, Gia_ObjFaninId1(pObj, iObj) );
|
|
Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
|
|
Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
|
|
Fan0 = Vec_IntEntry( vObj2Var, Fan0 );
|
|
Fan1 = Vec_IntEntry( vObj2Var, Fan1 );
|
|
fCompl0 = Gia_ObjFaninC0(pObj) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m));
|
|
fCompl1 = Gia_ObjFaninC1(pObj) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m));
|
|
if ( Gia_ObjIsXor(pObj) )
|
|
sat_solver_add_xor( pSat, Node, Fan0, Fan1, fCompl0 ^ fCompl1 );
|
|
else
|
|
sat_solver_add_and( pSat, Node, Fan0, Fan1, fCompl0, fCompl1, 0 );
|
|
}
|
|
// add second clauses for the TFO
|
|
Vec_IntForEachEntryStart( vWinObjs, iObj, i, TfoStart )
|
|
{
|
|
pObj = Gia_ManObj( p, iObj );
|
|
assert( Gia_ObjIsAnd(pObj) );
|
|
assert( Vec_IntEntry( vMirrors, iObj ) < 0 );
|
|
Node = Vec_IntEntry( vObj2Var, iObj ) + Vec_IntSize(vTfo);
|
|
Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, iObj) );
|
|
Lit1m = Vec_IntEntry( vMirrors, Gia_ObjFaninId1(pObj, iObj) );
|
|
Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
|
|
Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
|
|
Fan0 = Vec_IntEntry( vObj2Var, Fan0 );
|
|
Fan1 = Vec_IntEntry( vObj2Var, Fan1 );
|
|
Fan0 = Fan0 < TfoStart ? Fan0 : Fan0 + Vec_IntSize(vTfo);
|
|
Fan1 = Fan1 < TfoStart ? Fan1 : Fan1 + Vec_IntSize(vTfo);
|
|
if ( fQbf )
|
|
{
|
|
Fan0 = Fan0 == PivotVar ? LastVar : Fan0;
|
|
Fan1 = Fan1 == PivotVar ? LastVar : Fan1;
|
|
}
|
|
fCompl0 = Gia_ObjFaninC0(pObj) ^ (!fQbf && Fan0 == PivotVar) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m));
|
|
fCompl1 = Gia_ObjFaninC1(pObj) ^ (!fQbf && Fan1 == PivotVar) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m));
|
|
if ( Gia_ObjIsXor(pObj) )
|
|
sat_solver_add_xor( pSat, Node, Fan0, Fan1, fCompl0 ^ fCompl1 );
|
|
else
|
|
sat_solver_add_and( pSat, Node, Fan0, Fan1, fCompl0, fCompl1, 0 );
|
|
}
|
|
if ( Vec_IntSize(vRoots) > 0 )
|
|
{
|
|
// create XOR clauses for the roots
|
|
int nVars = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo);
|
|
Vec_Int_t * vFaninVars = Vec_IntAlloc( Vec_IntSize(vRoots) );
|
|
Vec_IntForEachEntry( vRoots, iObj, i )
|
|
{
|
|
assert( Vec_IntEntry( vMirrors, iObj ) < 0 );
|
|
Node = Vec_IntEntry( vObj2Var, iObj );
|
|
Vec_IntPush( vFaninVars, Abc_Var2Lit(nVars, 0) );
|
|
sat_solver_add_xor( pSat, Node, Node + Vec_IntSize(vTfo), nVars++, 0 );
|
|
}
|
|
// make OR clause for the last nRoots variables
|
|
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vFaninVars), Vec_IntLimit(vFaninVars) );
|
|
Vec_IntFree( vFaninVars );
|
|
if ( RetValue == 0 )
|
|
{
|
|
sat_solver_delete( pSat );
|
|
return NULL;
|
|
}
|
|
assert( sat_solver_nvars(pSat) == nVars + SBD_FVAR_MAX );
|
|
}
|
|
else if ( fQbf )
|
|
{
|
|
int n, pLits[2];
|
|
for ( n = 0; n < 2; n++ )
|
|
{
|
|
pLits[0] = Abc_Var2Lit( PivotVar, n );
|
|
pLits[1] = Abc_Var2Lit( LastVar, n );
|
|
RetValue = sat_solver_addclause( pSat, pLits, pLits + 2 );
|
|
assert( RetValue );
|
|
}
|
|
}
|
|
// finalize
|
|
RetValue = sat_solver_simplify( pSat );
|
|
if ( RetValue == 0 )
|
|
{
|
|
sat_solver_delete( pSat );
|
|
return NULL;
|
|
}
|
|
return pSat;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Solves one SAT problem.]
|
|
|
|
Description [Computes node function for PivotVar with fanins in vDivSet
|
|
using don't-care represented in the SAT solver. Uses array vValues to
|
|
return the values of the first Vec_IntSize(vValues) SAT variables in case
|
|
the implementation of the node with the given fanins does not exist.]
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivSet, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vTemp )
|
|
{
|
|
int nBTLimit = 0;
|
|
word uCube, uTruth = 0;
|
|
int status, i, iVar, nFinal, * pFinal, pLits[2], nIter = 0;
|
|
assert( FreeVar < sat_solver_nvars(pSat) );
|
|
assert( Vec_IntSize(vDivVars) == Vec_IntSize(vDivValues) );
|
|
pLits[0] = Abc_Var2Lit( PivotVar, 0 ); // F = 1
|
|
pLits[1] = Abc_Var2Lit( FreeVar, 0 ); // iNewLit
|
|
while ( 1 )
|
|
{
|
|
// find onset minterm
|
|
status = sat_solver_solve( pSat, pLits, pLits + 2, nBTLimit, 0, 0, 0 );
|
|
if ( status == l_Undef )
|
|
return SBD_SAT_UNDEC;
|
|
if ( status == l_False )
|
|
return uTruth;
|
|
assert( status == l_True );
|
|
// remember variable values
|
|
Vec_IntForEachEntry( vDivVars, iVar, i )
|
|
Vec_IntWriteEntry( vDivValues, i, 2*sat_solver_var_value(pSat, iVar) );
|
|
// collect divisor literals
|
|
Vec_IntClear( vTemp );
|
|
Vec_IntPush( vTemp, Abc_LitNot(pLits[0]) ); // F = 0
|
|
Vec_IntForEachEntry( vDivSet, iVar, i )
|
|
Vec_IntPush( vTemp, sat_solver_var_literal(pSat, iVar) );
|
|
// check against offset
|
|
status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp), nBTLimit, 0, 0, 0 );
|
|
if ( status == l_Undef )
|
|
return SBD_SAT_UNDEC;
|
|
if ( status == l_True )
|
|
break;
|
|
assert( status == l_False );
|
|
// compute cube and add clause
|
|
nFinal = sat_solver_final( pSat, &pFinal );
|
|
uCube = ~(word)0;
|
|
Vec_IntClear( vTemp );
|
|
Vec_IntPush( vTemp, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
|
|
for ( i = 0; i < nFinal; i++ )
|
|
{
|
|
if ( pFinal[i] == pLits[0] )
|
|
continue;
|
|
Vec_IntPush( vTemp, pFinal[i] );
|
|
iVar = Vec_IntFind( vDivSet, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 );
|
|
uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
|
|
}
|
|
uTruth |= uCube;
|
|
status = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp) );
|
|
assert( status );
|
|
nIter++;
|
|
}
|
|
assert( status == l_True );
|
|
// store the counter-example
|
|
Vec_IntForEachEntry( vDivVars, iVar, i )
|
|
Vec_IntAddToEntry( vDivValues, i, sat_solver_var_value(pSat, iVar) );
|
|
|
|
for ( i = 0; i < Vec_IntSize(vDivValues); i++ )
|
|
Vec_IntAddToEntry( vDivValues, i, 0xC );
|
|
/*
|
|
// reduce the counter example
|
|
for ( n = 0; n < 2; n++ )
|
|
{
|
|
Vec_IntClear( vTemp );
|
|
Vec_IntPush( vTemp, Abc_Var2Lit(PivotVar, n) ); // n = 0 => F = 1 (expanding offset against onset)
|
|
for ( i = 0; i < Vec_IntSize(vValues); i++ )
|
|
Vec_IntPush( vTemp, Abc_Var2Lit(i, !((Vec_IntEntry(vValues, i) >> n) & 1)) );
|
|
status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp), nBTLimit, 0, 0, 0 );
|
|
assert( status == l_False );
|
|
// compute cube and add clause
|
|
nFinal = sat_solver_final( pSat, &pFinal );
|
|
for ( i = 0; i < nFinal; i++ )
|
|
if ( Abc_Lit2Var(pFinal[i]) != PivotVar )
|
|
Vec_IntAddToEntry( vValues, Abc_Lit2Var(pFinal[i]), 1 << (n+2) );
|
|
}
|
|
*/
|
|
return SBD_SAT_SAT;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis []
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Sbd_ManSolve2( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vTemp, Vec_Int_t * vSop )
|
|
{
|
|
int nBTLimit = 0;
|
|
int status, i, iVar, nFinal, * pFinal, pLits[2], nIter = 0;
|
|
assert( FreeVar < sat_solver_nvars(pSat) );
|
|
assert( Vec_IntSize(vDivVars) == Vec_IntSize(vDivValues) );
|
|
pLits[0] = Abc_Var2Lit( PivotVar, 0 ); // F = 1
|
|
pLits[1] = Abc_Var2Lit( FreeVar, 0 ); // iNewLit
|
|
Vec_IntClear( vSop );
|
|
while ( 1 )
|
|
{
|
|
// find onset minterm
|
|
status = sat_solver_solve( pSat, pLits, pLits + 2, nBTLimit, 0, 0, 0 );
|
|
if ( status == l_Undef )
|
|
return 0;
|
|
if ( status == l_False )
|
|
return 1;
|
|
assert( status == l_True );
|
|
// remember variable values
|
|
//for ( i = 0; i < Vec_IntSize(vValues); i++ )
|
|
// Vec_IntWriteEntry( vValues, i, 2*sat_solver_var_value(pSat, i) );
|
|
// collect divisor literals
|
|
Vec_IntClear( vTemp );
|
|
Vec_IntPush( vTemp, Abc_LitNot(pLits[0]) ); // F = 0
|
|
//Vec_IntForEachEntry( vDivSet, iVar, i )
|
|
Vec_IntForEachEntry( vDivVars, iVar, i )
|
|
Vec_IntPush( vTemp, sat_solver_var_literal(pSat, iVar) );
|
|
// check against offset
|
|
status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp), nBTLimit, 0, 0, 0 );
|
|
if ( status == l_Undef )
|
|
return 0;
|
|
if ( status == l_True )
|
|
break;
|
|
assert( status == l_False );
|
|
// compute cube and add clause
|
|
nFinal = sat_solver_final( pSat, &pFinal );
|
|
Vec_IntClear( vTemp );
|
|
Vec_IntPush( vTemp, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
|
|
for ( i = 0; i < nFinal; i++ )
|
|
{
|
|
if ( pFinal[i] == pLits[0] )
|
|
continue;
|
|
Vec_IntPush( vTemp, pFinal[i] );
|
|
iVar = Vec_IntFind( vDivVars, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 );
|
|
//uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
|
|
Vec_IntPush( vSop, Abc_Var2Lit( iVar, !Abc_LitIsCompl(pFinal[i]) ) );
|
|
}
|
|
//uTruth |= uCube;
|
|
Vec_IntPush( vSop, -1 );
|
|
status = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp) );
|
|
assert( status );
|
|
nIter++;
|
|
}
|
|
assert( status == l_True );
|
|
// store the counter-example
|
|
//for ( i = 0; i < Vec_IntSize(vValues); i++ )
|
|
// Vec_IntAddToEntry( vValues, i, sat_solver_var_value(pSat, i) );
|
|
return 0;
|
|
}
|
|
|
|
word Sbd_ManSolverSupp( Vec_Int_t * vSop, int * pInds, int * pnVars )
|
|
{
|
|
word Supp = 0;
|
|
int i, Entry, nVars = 0;
|
|
Vec_IntForEachEntry( vSop, Entry, i )
|
|
{
|
|
if ( Entry == -1 )
|
|
continue;
|
|
assert( Abc_Lit2Var(Entry) < 64 );
|
|
if ( (Supp >> Abc_Lit2Var(Entry)) & 1 )
|
|
continue;
|
|
pInds[Abc_Lit2Var(Entry)] = nVars++;
|
|
Supp |= (word)1 << Abc_Lit2Var(Entry);
|
|
}
|
|
*pnVars = nVars;
|
|
return Supp;
|
|
}
|
|
void Sbd_ManSolverPrint( Vec_Int_t * vSop )
|
|
{
|
|
int v, i, Entry, nVars, pInds[64];
|
|
word Supp = Sbd_ManSolverSupp( vSop, pInds, &nVars );
|
|
char Cube[65] = {'\0'};
|
|
assert( Cube[nVars] == '\0' );
|
|
for ( v = 0; v < nVars; v++ )
|
|
Cube[v] = '-';
|
|
Vec_IntForEachEntry( vSop, Entry, i )
|
|
{
|
|
if ( Entry == -1 )
|
|
{
|
|
printf( "%s\n", Cube );
|
|
for ( v = 0; v < nVars; v++ )
|
|
Cube[v] = '-';
|
|
continue;
|
|
}
|
|
Cube[pInds[Abc_Lit2Var(Entry)]] = '1' - (char)Abc_LitIsCompl(Entry);
|
|
}
|
|
Supp = 0;
|
|
}
|
|
void Sbd_ManSolveSelect( Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots )
|
|
{
|
|
Vec_Int_t * vSop = Vec_IntAlloc( 100 );
|
|
Vec_Int_t * vTemp = Vec_IntAlloc( 100 );
|
|
sat_solver * pSat = Sbd_ManSatSolver( NULL, p, vMirrors, Pivot, vWinObjs, vObj2Var, vTfo, vRoots, 0 );
|
|
int PivotVar = Vec_IntEntry(vObj2Var, Pivot);
|
|
int FreeVar = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots);
|
|
int Status = Sbd_ManSolve2( pSat, PivotVar, FreeVar, vDivVars, vDivValues, vTemp, vSop );
|
|
printf( "Pivot = %4d. Divs = %4d. ", Pivot, Vec_IntSize(vDivVars) );
|
|
if ( Status == 0 )
|
|
printf( "UNSAT.\n" );
|
|
else
|
|
{
|
|
int nVars, pInds[64];
|
|
word Supp = Sbd_ManSolverSupp( vSop, pInds, &nVars );
|
|
//Sbd_ManSolverPrint( vSop );
|
|
printf( "SAT with %d vars and %d cubes.\n", nVars, Vec_IntCountEntry(vSop, -1) );
|
|
Supp = 0;
|
|
}
|
|
Vec_IntFree( vTemp );
|
|
Vec_IntFree( vSop );
|
|
sat_solver_delete( pSat );
|
|
}
|
|
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Returns a bunch of positive/negative random care minterms.]
|
|
|
|
Description [Returns 0/1 if the functions is const 0/1.]
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
static void sat_solver_random_polarity(sat_solver* s)
|
|
{
|
|
int i, k;
|
|
for ( i = 0; i < s->size; i += 64 )
|
|
{
|
|
word Polar = Gia_ManRandomW(0);
|
|
for ( k = 0; k < 64 && (i << 6) + k < s->size; k++ )
|
|
s->polarity[(i << 6) + k] = Abc_TtGetBit(&Polar, k);
|
|
}
|
|
}
|
|
int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds )
|
|
{
|
|
int nBTLimit = 0;
|
|
int i, Ind;
|
|
assert( Vec_IntSize(vInds) == nCareMints[0] + nCareMints[1] );
|
|
Vec_IntForEachEntry( vInds, Ind, i )
|
|
{
|
|
int fOffSet = (int)(i < nCareMints[0]);
|
|
int status, k, iLit = Abc_Var2Lit( PivotVar, fOffSet );
|
|
sat_solver_random_polarity( pSat );
|
|
status = sat_solver_solve( pSat, &iLit, &iLit + 1, nBTLimit, 0, 0, 0 );
|
|
if ( status == l_Undef )
|
|
return -2;
|
|
if ( status == l_False )
|
|
return fOffSet;
|
|
for ( k = 0; k <= PivotVar; k++ )
|
|
if ( Abc_TtGetBit(pVarSims[k], Ind) != sat_solver_var_value(pSat, k) )
|
|
Abc_TtXorBit(pVarSims[k], Ind);
|
|
}
|
|
return -1;
|
|
}
|
|
|
|
int Sbd_ManCollectConstantsNew( sat_solver * pSat, Vec_Int_t * vDivVars, int nConsts, int PivotVar, word * pOnset, word * pOffset )
|
|
{
|
|
int nBTLimit = 0;
|
|
int n, i, k, status, iLit, iVar;
|
|
word * pPats[2] = {pOnset, pOffset};
|
|
assert( Vec_IntSize(vDivVars) < 64 );
|
|
for ( n = 0; n < 2; n++ )
|
|
for ( i = 0; i < nConsts; i++ )
|
|
{
|
|
sat_solver_random_polarity( pSat );
|
|
iLit = Abc_Var2Lit( PivotVar, n );
|
|
status = sat_solver_solve( pSat, &iLit, &iLit + 1, nBTLimit, 0, 0, 0 );
|
|
if ( status == l_Undef )
|
|
return -2;
|
|
if ( status == l_False )
|
|
return n;
|
|
pPats[n][i] = ((word)!n) << Vec_IntSize(vDivVars);
|
|
Vec_IntForEachEntry( vDivVars, iVar, k )
|
|
if ( sat_solver_var_value(pSat, iVar) )
|
|
Abc_TtXorBit(&pPats[n][i], k);
|
|
}
|
|
return -1;
|
|
}
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// END OF FILE ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
ABC_NAMESPACE_IMPL_END
|
|
|