diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-09-18 05:05:22 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-09-18 05:05:22 -0700 |
commit | c30a0af71c219dcdd42322c411b805bb674d14b7 (patch) | |
tree | 8f6a5e2b004bfbc95cdbae7b6a2191bad286bdca /src/base/abci | |
parent | 97751e43b71792ded1947d98945e1e832325be6d (diff) | |
download | abc-c30a0af71c219dcdd42322c411b805bb674d14b7.tar.gz abc-c30a0af71c219dcdd42322c411b805bb674d14b7.tar.bz2 abc-c30a0af71c219dcdd42322c411b805bb674d14b7.zip |
Improvements to QBF solver; new quantification command &qvar.
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abc.c | 104 |
1 files changed, 84 insertions, 20 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 18427583..809995c4 100644 --- a/src/base/abci/abc.c +++ b/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; |