Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Revert recent PDR changes #320

Merged
merged 3 commits into from
Aug 13, 2024
Merged

Revert recent PDR changes #320

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
ec8419c
Revert "Improved anytime pdr"
povik Aug 12, 2024
39f6fbb
Revert "Fix pdr timing output"
povik Aug 12, 2024
de8620d
Revert "pdr -X to write CEXes immediately"
povik Aug 12, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 2 additions & 16 deletions src/base/abci/abc.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30247,7 +30247,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Pdr_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIXalxrmuyfqipdegjonctkvwzh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIaxrmuyfqipdegjonctkvwzh" ) ) != EOF )
{
switch ( c )
{
Expand Down Expand Up @@ -30368,21 +30368,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->pInvFileName = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'X':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-X\" should be followed by a directory name.\n" );
goto usage;
}
pPars->pCexFilePrefix = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'a':
pPars->fSolveAll ^= 1;
break;
case 'l':
pPars->fAnytime ^= 1;
break;
case 'x':
pPars->fStoreCex ^= 1;
break;
Expand Down Expand Up @@ -30487,7 +30475,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;

usage:
Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-LI <file>] [-X <prefix>] [-axrmuyfqipdegjonctkvwzh]\n" );
Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-LI <file>] [-axrmuyfqipdegjonctkvwzh]\n" );
Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" );
Abc_Print( -2, "\t pioneered by Aaron R. Bradley (http://theory.stanford.edu/~arbrad/)\n" );
Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" );
Expand All @@ -30502,9 +30490,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -2, "\t-S num : * value to seed the SAT solver with [default = %d]\n", pPars->nRandomSeed );
Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
Abc_Print( -2, "\t-I file: the invariant file name [default = %s]\n", pPars->pInvFileName ? pPars->pInvFileName : "default name" );
Abc_Print( -2, "\t-X pref: when solving all outputs, store CEXes immediately as <pref>*.aiw [default = %s]\n", pPars->pCexFilePrefix ? pPars->pCexFilePrefix : "disabled");
Abc_Print( -2, "\t-a : toggle solving all outputs even if one of them is SAT [default = %s]\n", pPars->fSolveAll? "yes": "no" );
Abc_Print( -2, "\t-l : toggle anytime schedule when solving all outputs [default = %s]\n", pPars->fAnytime? "yes": "no" );
Abc_Print( -2, "\t-x : toggle storing CEXes when solving all outputs [default = %s]\n", pPars->fStoreCex? "yes": "no" );
Abc_Print( -2, "\t-r : toggle using more effort in generalization [default = %s]\n", pPars->fTwoRounds? "yes": "no" );
Abc_Print( -2, "\t-m : toggle using monolythic CNF computation [default = %s]\n", pPars->fMonoCnf? "yes": "no" );
Expand Down
3 changes: 0 additions & 3 deletions src/proof/pdr/pdr.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,6 @@ struct Pdr_Par_t_
int fSilent; // totally silent execution
int fSolveAll; // do not stop when found a SAT output
int fStoreCex; // enable storing counter-examples in MO mode
int fAnytime; // enable anytime scheduling
int fUseBridge; // use bridge interface
int fUsePropOut; // use property output
int nFailOuts; // the number of failed outputs
Expand All @@ -85,7 +84,6 @@ struct Pdr_Par_t_
abctime timeLastSolved; // the time when the last output was solved
Vec_Int_t * vOutMap; // in the multi-output mode, contains status for each PO (0 = sat; 1 = unsat; negative = undecided)
char * pInvFileName; // invariable file name
char * pCexFilePrefix; // CEX output prefix
};

////////////////////////////////////////////////////////////////////////
Expand All @@ -97,7 +95,6 @@ struct Pdr_Par_t_
////////////////////////////////////////////////////////////////////////

/*=== pdrCore.c ==========================================================*/
extern void Pdr_OutputCexToDir( Pdr_Par_t * pPars, Abc_Cex_t * pCex );
extern void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars );
extern int Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars );

Expand Down
Loading
Loading