diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-05 21:08:55 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-05 21:08:55 -0700 |
| commit | 05f7cd9ed206b188b6cdcf5d06de732065f898fd (patch) | |
| tree | ef648c5dbcf45c17b5d8e365d5c4e1d9b2833cba /src/base/abci/abc.c | |
| parent | 98cf5698a1ab2cca09d7fbfec878d332b48e1a46 (diff) | |
| download | abc-05f7cd9ed206b188b6cdcf5d06de732065f898fd.tar.gz abc-05f7cd9ed206b188b6cdcf5d06de732065f898fd.tar.bz2 abc-05f7cd9ed206b188b6cdcf5d06de732065f898fd.zip | |
Integration of the liveness property prover developed by Sayak Ray.
Diffstat (limited to 'src/base/abci/abc.c')
| -rw-r--r-- | src/base/abci/abc.c | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f555bbf8..bef700d3 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -402,6 +402,8 @@ static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, cha extern int Abc_CommandAbcLivenessToSafety ( Abc_Frame_t * pAbc, int argc, char ** argv ); extern int Abc_CommandAbcLivenessToSafetySim ( Abc_Frame_t * pAbc, int argc, char ** argv ); extern int Abc_CommandAbcLivenessToSafetyWithLTL( Abc_Frame_t * pAbc, int argc, char ** argv ); +extern int Abc_CommandCS_kLiveness ( Abc_Frame_t * pAbc, int argc, char ** argv ); +extern int Abc_CommandNChooseK ( Abc_Frame_t * pAbc, int argc, char ** argv ); extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan ); @@ -894,9 +896,11 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Abstraction", "&fla_gla", Abc_CommandAbc9Fla2Gla, 0 ); Cmd_CommandAdd( pAbc, "Abstraction", "&gla_fla", Abc_CommandAbc9Gla2Fla, 0 ); - Cmd_CommandAdd( pAbc, "Liveness", "l2s", Abc_CommandAbcLivenessToSafety, 0 ); - Cmd_CommandAdd( pAbc, "Liveness", "l2ssim", Abc_CommandAbcLivenessToSafetySim, 0 ); - Cmd_CommandAdd( pAbc, "Liveness", "l3s", Abc_CommandAbcLivenessToSafetyWithLTL, 0 ); + Cmd_CommandAdd( pAbc, "Liveness", "l2s", Abc_CommandAbcLivenessToSafety, 0 ); + Cmd_CommandAdd( pAbc, "Liveness", "l2ssim", Abc_CommandAbcLivenessToSafetySim, 0 ); + Cmd_CommandAdd( pAbc, "Liveness", "l3s", Abc_CommandAbcLivenessToSafetyWithLTL, 0 ); + Cmd_CommandAdd( pAbc, "Liveness", "kcs", Abc_CommandCS_kLiveness, 0 ); + Cmd_CommandAdd( pAbc, "Liveness", "nck", Abc_CommandNChooseK, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); |