diff options
| -rw-r--r-- | src/aig/gia/giaQbf.c | 304 | ||||
| -rw-r--r-- | src/aig/gia/module.make | 1 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 127 | ||||
| -rw-r--r-- | src/misc/vec/vecInt.h | 6 |
4 files changed, 436 insertions, 2 deletions
diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c new file mode 100644 index 00000000..33216ce3 --- /dev/null +++ b/src/aig/gia/giaQbf.c @@ -0,0 +1,304 @@ +/**CFile**************************************************************** + + FileName [giaQbf.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [QBF solver.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - October 18, 2014.] + + Revision [$Id: giaQbf.c,v 1.00 2014/10/18 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "sat/cnf/cnf.h" +#include "sat/bsat/satStore.h" +#include "misc/extra/extra.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Qbf_Man_t_ Qbf_Man_t; +struct Qbf_Man_t_ +{ + Gia_Man_t * pGia; // original miter + int nPars; // parameter variables + int nVars; // functional variables + int fVerbose; // verbose flag + // internal variables + int iParVarBeg; // SAT var ID of the first par variable in the ver solver + sat_solver * pSatVer; // verification instance + sat_solver * pSatSyn; // synthesis instance + Vec_Int_t * vValues; // variable values + Vec_Int_t * vParMap; // parameter mapping + abctime clkStart; // global timeout +}; + +extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Dumps the original problem in QDIMACS format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars ) +{ + // original problem: \exists p \forall x \exists y. M(p,x,y) + // negated problem: \forall p \exists x \exists y. !M(p,x,y) + Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 0, 0 ); + Vec_Int_t * vVarMap, * vForAlls, * vExists; + Gia_Obj_t * pObj; + char * pFileName; + int i, Entry; + // create var map + vVarMap = Vec_IntStart( pCnf->nVars ); + Gia_ManForEachCi( pGia, pObj, i ) + if ( i < nPars ) + Vec_IntWriteEntry( vVarMap, pCnf->pVarNums[Gia_ManCiIdToId(pGia, i)], 1 ); + // create various maps + vForAlls = Vec_IntAlloc( nPars ); + vExists = Vec_IntAlloc( Gia_ManCiNum(pGia) - nPars ); + Vec_IntForEachEntry( vVarMap, Entry, i ) + if ( Entry ) + Vec_IntPush( vForAlls, i ); + else + Vec_IntPush( vExists, i ); + // generate CNF + pFileName = Extra_FileNameGenericAppend( pGia->pSpec, ".qdimacs" ); + Cnf_DataWriteIntoFile( pCnf, pFileName, 0, vForAlls, vExists ); + Cnf_DataFree( pCnf ); + Vec_IntFree( vForAlls ); + Vec_IntFree( vExists ); + Vec_IntFree( vVarMap ); + printf( "The 2QBF formula was written into file \"%s\".\n", pFileName ); +} + +/**Function************************************************************* + + Synopsis [Generate one SAT assignment of the problem.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fVerbose ) +{ + Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 0, 0 ); + Qbf_Man_t * p = ABC_CALLOC( Qbf_Man_t, 1 ); + p->clkStart = Abc_Clock(); + p->pGia = pGia; + p->nPars = nPars; + p->nVars = Gia_ManPiNum(pGia) - nPars; + p->fVerbose = fVerbose; + p->iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia) - 2; + p->pSatVer = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + p->pSatSyn = sat_solver_new(); + p->vValues = Vec_IntAlloc( Gia_ManPiNum(pGia) ); + p->vParMap = Vec_IntStartFull( nPars ); + sat_solver_setnvars( p->pSatSyn, nPars ); + Cnf_DataFree( pCnf ); + return p; +} +void Gia_QbfFree( Qbf_Man_t * p ) +{ + sat_solver_delete( p->pSatVer ); + sat_solver_delete( p->pSatSyn ); + Vec_IntFree( p->vValues ); + Vec_IntFree( p->vParMap ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Create and add one cofactor.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_QbfCofactor( Gia_Man_t * p, int nPars, Vec_Int_t * vValues, Vec_Int_t * vParMap ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; int i; + assert( Gia_ManPiNum(p) == nPars + Vec_IntSize(vValues) ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + Gia_ManHashAlloc( pNew ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachPi( p, pObj, i ) + pObj->Value = i < nPars ? Gia_ManAppendCi(pNew) : Vec_IntEntry(vValues, i - nPars); + 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) ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + 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, 0, 0 ); + int i, iFirstVar = sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof) - 2; + pCnf->pMan = NULL; + Cnf_DataLift( pCnf, sat_solver_nvars(p->pSatSyn) ); + 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 + 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************************************************************* + + Synopsis [Extract SAT assignment.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_QbfOnePattern( Qbf_Man_t * p, Vec_Int_t * vValues ) +{ + int i; + Vec_IntClear( vValues ); + for ( i = 0; i < p->nPars; i++ ) + Vec_IntPush( vValues, sat_solver_var_value(p->pSatSyn, i) ); +} +void Gia_QbfPrint( Qbf_Man_t * p, Vec_Int_t * vValues, int Iter ) +{ + printf( "%5d : ", Iter ); + assert( Vec_IntSize(p->vValues) == p->nVars ); + Vec_IntPrintBinary( p->vValues ); printf( " " ); + printf( "Var = %6d ", sat_solver_nvars(p->pSatSyn) ); + printf( "Cla = %6d ", sat_solver_nclauses(p->pSatSyn) ); + printf( "Conf = %6d ", sat_solver_nconflicts(p->pSatSyn) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart ); +} + +/**Function************************************************************* + + Synopsis [Generate one SAT assignment in terms of functional vars.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_QbfVerify( Qbf_Man_t * p, Vec_Int_t * vValues ) +{ + int i, Entry, RetValue; + assert( Vec_IntSize(vValues) == p->nPars ); + Vec_IntForEachEntry( vValues, Entry, i ) + Vec_IntWriteEntry( vValues, i, Abc_Var2Lit(p->iParVarBeg+i, !Entry) ); + RetValue = sat_solver_solve( p->pSatVer, Vec_IntArray(vValues), Vec_IntLimit(vValues), 0, 0, 0, 0 ); + if ( RetValue == l_True ) + { + Vec_IntClear( vValues ); + for ( i = 0; i < p->nVars; i++ ) + Vec_IntPush( vValues, sat_solver_var_value(p->pSatVer, p->iParVarBeg+p->nPars+i) ); + } + return RetValue == l_True ? 1 : 0; +} + +/**Function************************************************************* + + Synopsis [Performs QBF solving using an improved algorithm.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int fVerbose ) +{ + Qbf_Man_t * p = Gia_QbfAlloc( pGia, nPars, fVerbose ); + Gia_Man_t * pCof; + int i, status, RetValue = 0; + assert( Gia_ManRegNum(pGia) == 0 ); + Vec_IntFill( p->vValues, nPars, 0 ); + for ( i = 0; Gia_QbfVerify(p, p->vValues) && (!nIterLimit || i < nIterLimit); i++ ) + { + // generate next constraint + assert( Vec_IntSize(p->vValues) == p->nVars ); + pCof = Gia_QbfCofactor( pGia, nPars, p->vValues, p->vParMap ); + status = Gia_QbfAddCofactor( p, pCof ); + Gia_ManStop( pCof ); + if ( status == 0 ) { RetValue = 1; break; } + // synthesize next assignment + status = sat_solver_solve( p->pSatSyn, NULL, NULL, nConfLimit, 0, 0, 0 ); + if ( fVerbose ) + Gia_QbfPrint( p, p->vValues, i ); + if ( status == l_Undef ) { RetValue = -1; break; } + if ( status == l_False ) { RetValue = 1; break; } + // extract SAT assignment + Gia_QbfOnePattern( p, p->vValues ); + assert( Vec_IntSize(p->vValues) == p->nPars ); + } + if ( RetValue == -1 && nTimeOut ) + printf( "The solver timed out after %d sec. ", nTimeOut ); + else if ( RetValue == -1 && nConfLimit ) + printf( "The solver aborted after %d conflicts. ", nConfLimit ); + else if ( RetValue == 1 ) + printf( "The problem is UNSAT. " ); + else + printf( "The problem is SAT. " ); + Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart ); + if ( RetValue == 0 ) + { + assert( Vec_IntSize(p->vValues) == nPars ); + Vec_IntPrintBinary( p->vValues ); + printf( "\n" ); + } + Gia_QbfFree( p ); + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 2f6c5512..4e830971 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -46,6 +46,7 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaMuxes.c \ src/aig/gia/giaNf.c \ src/aig/gia/giaPat.c \ + src/aig/gia/giaQbf.c \ src/aig/gia/giaResub.c \ src/aig/gia/giaRetime.c \ src/aig/gia/giaScl.c \ diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 15015059..2086faa5 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -423,6 +423,7 @@ static int Abc_CommandAbc9BCore ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9ICheck ( Abc_Frame_t * pAbc, int argc, char ** argv ); 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_CommandAbc9Inse ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Maxi ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Bmci ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1015,6 +1016,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&icheck", Abc_CommandAbc9ICheck, 0 ); 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", "&inse", Abc_CommandAbc9Inse, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&maxi", Abc_CommandAbc9Maxi, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&bmci", Abc_CommandAbc9Bmci, 0 ); @@ -12934,7 +12936,7 @@ int Abc_CommandQbf( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( !(nPars > 0 && nPars < Abc_NtkPiNum(pNtk)) ) { - Abc_Print( -1, "The number of paramter variables is invalid (should be > 0 and < PI num).\n" ); + Abc_Print( -1, "The number of parameter variables is invalid (should be > 0 and < PI num).\n" ); return 1; } if ( Abc_NtkIsStrash(pNtk) ) @@ -26505,7 +26507,7 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv ) } else { - Abc_Print( -1, "One of the paramters, -V <num> or -L <num>, should be set on the command line.\n" ); + Abc_Print( -1, "One of the parameters, -V <num> or -L <num>, should be set on the command line.\n" ); goto usage; } return 0; @@ -35686,6 +35688,127 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + 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; + int nIterLimit = 0; + int nConfLimit = 0; + int nTimeOut = 0; + int fDumpCnf = 0; + int fVerbose = 1; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "PICTdvh" ) ) != 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 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nIterLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nIterLimit < 0 ) + goto usage; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConfLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfLimit < 0 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + nTimeOut = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nTimeOut < 0 ) + goto usage; + break; + case 'd': + fDumpCnf ^= 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 ( Gia_ManPoNum(pAbc->pGia) != 1 ) + { + Abc_Print( -1, "The miter should have one primary output.\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; + } + if ( fDumpCnf ) + Gia_QbfDumpFile( pAbc->pGia, nPars ); + else + Gia_QbfSolve( pAbc->pGia, nPars, nIterLimit, nConfLimit, nTimeOut, fVerbose ); + return 0; + +usage: + 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-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_CommandAbc9Inse( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern Vec_Int_t * Gia_ManInseTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose ); diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index 6d015bcc..b56d8661 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -1758,6 +1758,12 @@ static inline void Vec_IntPrint( Vec_Int_t * vVec ) printf( " %d", Entry ); printf( " }\n" ); } +static inline void Vec_IntPrintBinary( Vec_Int_t * vVec ) +{ + int i, Entry; + Vec_IntForEachEntry( vVec, Entry, i ) + printf( "%d", (int)(Entry != 0) ); +} /**Function************************************************************* |