Skip to content

A
abc
Commit c30a0af7 by Alan Mishchenko
Options

Improvements to QBF solver; new quantification command &qvar.

parent 97751e43
Showing with 164 additions and 32 deletions
src/aig/gia/giaQbf.c
......@@ -330,31 +330,58 @@ void Gia_QbfFree( Qbf_Man_t * p )
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_QbfQuantify( Gia_Man_t * p, int nPars )
Gia_Man_t * Gia_QbfQuantifyOne( Gia_Man_t * p, int iVar, int fAndAll, int fOrAll )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, m, nMints = (1 << (Gia_ManPiNum(p) - nPars));
assert( Gia_ManPoNum(p) == 1 );
Vec_Int_t * vCofs;
int i, c;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
for ( i = 0; i < nPars; i++ )
Gia_ManAppendCi(pNew);
for ( m = 0; m < nMints; m++ )
Gia_ManForEachPi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
// compute cofactors
vCofs = Vec_IntAlloc( 2 * Gia_ManPoNum(p) );
for ( c = 0; c < 2; c++ )
{
Gia_ManForEachPi( p, pObj, i )
pObj->Value = (i < nPars) ? Gia_Obj2Lit(pNew, Gia_ManPi(pNew, i)) : ((m >> (i - nPars)) & 1);
Gia_ManPi(p, iVar)->Value = c;
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachCo( p, pObj, i )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManForEachPo( p, pObj, i )
Vec_IntPush( vCofs, Gia_ObjFanin0Copy(pObj) );
}
if ( fAndAll )
{
for ( i = 0; i < Gia_ManPoNum(p); i++ )
Gia_ManAppendCo( pNew, Gia_ManHashAnd(pNew, Vec_IntEntry(vCofs, i), Vec_IntEntry(vCofs, Gia_ManPoNum(p)+i)) );
}
else if ( fOrAll )
{
for ( i = 0; i < Gia_ManPoNum(p); i++ )
Gia_ManAppendCo( pNew, Gia_ManHashOr(pNew, Vec_IntEntry(vCofs, i), Vec_IntEntry(vCofs, Gia_ManPoNum(p)+i)) );
}
else
{
Vec_IntForEachEntry( vCofs, c, i )
Gia_ManAppendCo( pNew, c );
}
Vec_IntFree( vCofs );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
assert( Gia_ManPiNum(pNew) == nPars );
assert( Gia_ManPoNum(pNew) == nMints );
return pNew;
}
Gia_Man_t * Gia_QbfQuantifyAll( Gia_Man_t * p, int nPars, int fAndAll, int fOrAll )
{
Gia_Man_t * pNew, * pTemp; int v;
pNew = Gia_ManDup( p );
for ( v = Gia_ManPiNum(p) - 1; v >= nPars; v-- )
{
pNew = Gia_QbfQuantifyOne( pTemp = pNew, v, fAndAll, fOrAll );
Gia_ManStop( pTemp );
}
return pNew;
}
......@@ -396,6 +423,7 @@ Gia_Man_t * Gia_QbfCofactor( Gia_Man_t * p, int nPars, Vec_Int_t * vValues, Vec_
assert( Gia_ManPiNum(pNew) == nPars );
return pNew;
}
/*
int Gia_QbfAddCofactor( Qbf_Man_t * p, Gia_Man_t * pCof )
{
Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pCof, 8, 0, 1, 0 );
......@@ -415,6 +443,46 @@ int Gia_QbfAddCofactor( Qbf_Man_t * p, Gia_Man_t * pCof )
return 0;
return 1;
}
*/
void Cnf_SpecialDataLift( Cnf_Dat_t * p, int nVarsPlus, int firstPiVar, int lastPiVar)
{
int v, var;
for ( v = 0; v < p->nLiterals; v++ )
{
var = p->pClauses[0][v] / 2;
if (var < firstPiVar || var >= lastPiVar)
p->pClauses[0][v] += 2*nVarsPlus;
else
p->pClauses[0][v] -= 2*firstPiVar;
}
}
int Gia_QbfAddCofactor( Qbf_Man_t * p, Gia_Man_t * pCof )
{
Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pCof, 8, 0, 1, 0 );
int i, useold = 0;
int iFirstVar = useold ? sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof) : pCnf->nVars - Gia_ManPiNum(pCof); //-1
pCnf->pMan = NULL;
if (useold)
Cnf_DataLift( pCnf, sat_solver_nvars(p->pSatSyn) );
else
Cnf_SpecialDataLift( pCnf, sat_solver_nvars(p->pSatSyn), iFirstVar, iFirstVar + Gia_ManPiNum(p->pGia) );
for ( i = 0; i < pCnf->nClauses; i++ )
if ( !sat_solver_addclause( p->pSatSyn, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
{
Cnf_DataFree( pCnf );
return 0;
}
Cnf_DataFree( pCnf );
// add connection clauses
if (useold)
for ( i = 0; i < Gia_ManPiNum(p->pGia); i++ )
if ( !sat_solver_add_buffer( p->pSatSyn, i, iFirstVar+i, 0 ) )
return 0;
return 1;
}
/**Function*************************************************************
......
src/base/abci/abc.c
......@@ -444,6 +444,7 @@ static int Abc_CommandAbc9ICheck ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9SatTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9FFTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Qbf ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9QVar ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GenQbf ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SatFx ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SatClp ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -1060,6 +1061,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&sattest", Abc_CommandAbc9SatTest, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&fftest", Abc_CommandAbc9FFTest, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&qbf", Abc_CommandAbc9Qbf, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&qvar", Abc_CommandAbc9QVar, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&genqbf", Abc_CommandAbc9GenQbf, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&satfx", Abc_CommandAbc9SatFx, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&satclp", Abc_CommandAbc9SatClp, 0 );
......@@ -36911,7 +36913,6 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_QbfQuantify( Gia_Man_t * p, int nPars );
extern void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars );
extern int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int fVerbose );
int c, nPars = -1;
......@@ -36919,10 +36920,9 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv )
int nConfLimit = 0;
int nTimeOut = 0;
int fDumpCnf = 0;
int fQuantX = 0;
int fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PICTdqvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "PICTdvh" ) ) != EOF )
{
switch ( c )
{
......@@ -36973,9 +36973,6 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'd':
fDumpCnf ^= 1;
break;
case 'q':
fQuantX ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
......@@ -37005,18 +37002,6 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "The number of parameter variables is invalid (should be > 0 and < PI num).\n" );
return 1;
}
if ( fQuantX )
{
Gia_Man_t * pTemp;
if ( Gia_ManPiNum(pAbc->pGia) - nPars > 16 )
{
Abc_Print( -1, "Cannot quantify more than 16 variables.\n" );
return 1;
}
pTemp = Gia_QbfQuantify( pAbc->pGia, nPars );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
}
if ( fDumpCnf )
Gia_QbfDumpFile( pAbc->pGia, nPars );
else
......@@ -37024,14 +37009,93 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &qbf [-PICT num] [-dqvh]\n" );
Abc_Print( -2, "usage: &qbf [-PICT num] [-dvh]\n" );
Abc_Print( -2, "\t solves QBF problem EpVxM(p,x)\n" );
Abc_Print( -2, "\t-P num : number of parameters p (should be the first PIs) [default = %d]\n", nPars );
Abc_Print( -2, "\t-I num : quit after the given iteration even if unsolved [default = %d]\n", nIterLimit );
Abc_Print( -2, "\t-C num : conflict limit per problem [default = %d]\n", nConfLimit );
Abc_Print( -2, "\t-T num : global timeout [default = %d]\n", nTimeOut );
Abc_Print( -2, "\t-d : toggle dumping QDIMACS file instead of solving [default = %s]\n", fDumpCnf? "yes": "no" );
Abc_Print( -2, "\t-q : toggle quantifying functions variables [default = %s]\n", fQuantX? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9QVar( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_QbfQuantifyAll( Gia_Man_t * p, int nPars, int fAndAll, int fOrAll );
Gia_Man_t * pTemp;
int c, nPars = -1;
int fQuantU = 0;
int fQuantE = 0;
int fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Puevh" ) ) != EOF )
{
switch ( c )
{
case 'P':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
goto usage;
}
nPars = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nPars < 0 )
goto usage;
break;
case 'u':
fQuantU ^= 1;
break;
case 'e':
fQuantE ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "There is no current GIA.\n" );
return 1;
}
if ( Gia_ManRegNum(pAbc->pGia) )
{
Abc_Print( -1, "Works only for combinational networks.\n" );
return 1;
}
if ( !(nPars > 0 && nPars < Gia_ManPiNum(pAbc->pGia)) )
{
Abc_Print( -1, "The number of parameter variables is invalid (should be > 0 and < PI num).\n" );
return 1;
}
pTemp = Gia_QbfQuantifyAll( pAbc->pGia, nPars, fQuantU, fQuantE );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &qvar [-P num] [-uevh]\n" );
Abc_Print( -2, "\t derives cofactors w.r.t. the last NumPi-<num> variables\n" );
Abc_Print( -2, "\t-P num : number of parameters p (should be the first PIs) [default = %d]\n", nPars );
Abc_Print( -2, "\t-u : toggle ANDing cofactors (universal quantification) [default = %s]\n", fQuantU? "yes": "no" );
Abc_Print( -2, "\t-e : toggle ORing cofactors (existential quantification) [default = %s]\n", fQuantE? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment