/**CFile**************************************************************** FileName [mainMC.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [The main package.] Synopsis [The main file for the model checker.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: main.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "mainInt.h" #include "aig/aig/aig.h" #include "aig/saig/saig.h" #include "aig/fra/fra.h" #include "aig/ioa/ioa.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [The main() procedure.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int main( int argc, char * argv[] ) { int fEnableBmcOnly = 0; // enable to make it BMC-only int fEnableCounter = 1; // should be 1 in the final version int fEnableComment = 0; // should be 0 in the final version Fra_Sec_t SecPar, * pSecPar = &SecPar; FILE * pFile; Aig_Man_t * pAig; int RetValue = -1; int Depth = -1; // BMC parameters int nFrames = 50; int nSizeMax = 500000; int nBTLimit = 10000; int fRewrite = 0; int fNewAlgo = 1; int fVerbose = 0; clock_t clkTotal = clock(); if ( argc != 2 ) { printf( " Expecting one command-line argument (an input file in AIGER format).\n" ); printf( " usage: %s \n", argv[0] ); return 0; } pFile = fopen( argv[1], "r" ); if ( pFile == NULL ) { printf( " Cannot open input AIGER file \"%s\".\n", argv[1] ); printf( " usage: %s \n", argv[0] ); return 0; } fclose( pFile ); pAig = Ioa_ReadAiger( argv[1], 1 ); if ( pAig == NULL ) { printf( " Parsing the AIGER file \"%s\" has failed.\n", argv[1] ); printf( " usage: %s \n", argv[0] ); return 0; } Aig_ManSetRegNum( pAig, pAig->nRegs ); if ( !fEnableBmcOnly ) { // perform BMC if ( pAig->nRegs != 0 ) RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, NULL, 0 ); // perform full-blown SEC if ( RetValue != 0 ) { extern void Dar_LibStart(); extern void Dar_LibStop(); extern void Cnf_ManFree(); Fra_SecSetDefaultParams( pSecPar ); pSecPar->TimeLimit = 600; pSecPar->nFramesMax = 4; // the max number of frames used for induction pSecPar->fPhaseAbstract = 0; // disable phase-abstraction pSecPar->fSilent = 1; // disable phase-abstraction Dar_LibStart(); RetValue = Fra_FraigSec( pAig, pSecPar, NULL ); Dar_LibStop(); Cnf_ManFree(); } } // perform BMC again if ( RetValue == -1 && pAig->nRegs != 0 ) { int nFrames = 200; int nSizeMax = 500000; int nBTLimit = 10000000; int fRewrite = 0; RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &Depth, 0 ); if ( RetValue != 0 ) RetValue = -1; } // decide how to report the output pFile = stdout; // report the result if ( RetValue == 0 ) { // fprintf(stdout, "s SATIFIABLE\n"); fprintf( pFile, "1" ); if ( fEnableCounter ) { printf( "\n" ); if ( pAig->pSeqModel ) Fra_SmlWriteCounterExample( pFile, pAig, pAig->pSeqModel ); } if ( fEnableComment ) { printf( " # File %10s. ", argv[1] ); PRT( "Time", clock() - clkTotal ); } if ( pFile != stdout ) fclose(pFile); Aig_ManStop( pAig ); exit(10); } else if ( RetValue == 1 ) { // fprintf(stdout, "s UNSATISFIABLE\n"); fprintf( pFile, "0" ); if ( fEnableComment ) { printf( " # File %10s. ", argv[1] ); PRT( "Time", clock() - clkTotal ); } printf( "\n" ); if ( pFile != stdout ) fclose(pFile); Aig_ManStop( pAig ); exit(20); } else // if ( RetValue == -1 ) { // fprintf(stdout, "s UNKNOWN\n"); fprintf( pFile, "2" ); if ( fEnableComment ) { printf( " # File %10s. ", argv[1] ); PRT( "Time", clock() - clkTotal ); } printf( "\n" ); if ( pFile != stdout ) fclose(pFile); Aig_ManStop( pAig ); exit(0); } return 0; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END ric.Error */ .highlight .gh { color: #333333 } /* Generic.Heading */ .highlight .gi { color: #000000; background-color: #ddffdd } /* Generic.Inserted */ .highlight .go { color: #888888 } /* Generic.Output */ .highlight .gp { color: #555555 } /* Generic.Prompt */ .highlight .gs { font-weight: bold } /* Generic.Strong */ .highlight .gu { color: #666666 } /* Generic.Subheading */ .highlight .gt { color: #aa0000 } /* Generic.Traceback */ .highlight .kc { color: #008800; font-weight: bold } /* Keyword.Constant */ .highlight .kd { color: #008800; font-weight: bold } /* Keyword.Declaration */ .highlight .kn { color: #008800; font-weight: bold } /* Keyword.Namespace */ .highlight .kp { color: #008800 } /* Keyword.Pseudo */ .highlight .kr { color: #008800; font-weight: bold } /* Keyword.Reserved */ .highlight .kt { color: #888888; font-weight: bold } /* Keyword.Type */ .highlight .m { color: #0000DD; font-weight: bold } /* Literal.Number */ .highlight .s { color: #dd2200; background-color: #fff0f0 } /* Literal.String */ .highlight .na { color: #336699 } /* Name.Attribute */ .highlight .nb { color: #003388 } /* Name.Builtin */ .highlight .nc { color: #bb0066; font-weight: bold } /* Name.Class */ .highlight .no { color: #003366; font-weight: bold } /* Name.Constant */ .highlight .nd { color: #555555 } /* Name.Decorator */ .highlight .ne { color: #bb0066; font-weight: bold } /* Name.Exception */ .highlight .nf { color: #0066bb; font-weight: bold } /* Name.Function */ .highlight .nl { color: #336699; font-style: italic } /* Name.Label */ .highlight .nn { color: #bb0066; font-weight: bold } /* Name.Namespace */ .highlight .py { color: #336699; font-weight: bold } /* Name.Property */ .highlight .nt { color: #bb0066; font-weight: bold } /* Name.Tag */ .highlight .nv { color: #336699 } /* Name.Variable */ .highlight .ow { color: #008800 } /* Operator.Word */ .highlight .w { color: #bbbbbb } /* Text.Whitespace */ .highlight .mb { color: #0000DD; font-weight: bold } /* Literal.Number.Bin */ .highlight .mf { color: #0000DD; font-weight: bold } /* Literal.Number.Float */ .highlight .mh { color: #0000DD; font-weight: bold } /* Literal.Number.Hex */ .highlight .mi { color: #0000DD; font-weight: bold } /* Literal.Number.Integer */ .highlight .mo { color: #0000DD; font-weight: bold } /* Literal.Number.Oct */ .highlight .sa { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Affix */ .highlight .sb { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Backtick */ .highlight .sc { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Char */ .highlight .dl { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Delimiter */ .highlight .sd { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Doc */ .highlight .s2 { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Double */ .highlight .se { color: #0044dd; background-color: #fff0f0 } /* Literal.String.Escape */ .highlight .sh { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Heredoc */ .highlight .si { color: #3333bb; background-color: #fff0f0 } /* Literal.String.Interpol */ .highlight .sx { color: #22bb22; background-color: #f0fff0 } /* Literal.String.Other */ .highlight .sr { color: #008800; background-color: #fff0ff } /* Literal.String.Regex */ .highlight .s1 { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Single */ .highlight .ss { color: #aa6600; background-color: #fff0f0 } /* Literal.String.Symbol */ .highlight .bp { color: #003388 } /* Name.Builtin.Pseudo */ .highlight .fm { color: #0066bb; font-weight: bold } /* Name.Function.Magic */ .highlight .vc { color: #336699 } /* Name.Variable.Class */ .highlight .vg { color: #dd7700 } /* Name.Variable.Global */ .highlight .vi { color: #3333bb } /* Name.Variable.Instance */ .highlight .vm { color: #336699 } /* Name.Variable.Magic */ .highlight .il { color: #0000DD; font-weight: bold } /* Literal.Number.Integer.Long */
#!/usr/bin/env bash
IFS=$'\n'
[ -n "$1" -a -n "$2" ] || {
	echo "Usage: $0 <file> <directory>"
	exit 1
}
[ -f "$1" -a -d "$2" ] || {
	echo "File/directory not found"
	exit 1
}
cat "$1" | (
	cd "$2"
	while read entry; do
		[ -n "$entry" ] || break
		[ ! -d "$entry" ] || [ -L "$entry" ] && rm -f "$entry"
	done
)
sort -r "$1" | (
	cd "$2"
	while read entry; do
		[ -n "$entry" ] || break
		[ -d "$entry" ] && rmdir "$entry" > /dev/null 2>&1
	done
)
true