Commit 9914c168 by Alan Mishchenko

Adding interpolant computation sat_solver2.

parent 57b9a9fe
...@@ -689,7 +689,7 @@ extern ABC_DLL Abc_Ntk_t * Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk ); ...@@ -689,7 +689,7 @@ extern ABC_DLL Abc_Ntk_t * Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk );
extern ABC_DLL int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter ); extern ABC_DLL int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter );
extern ABC_DLL void Abc_NtkMiterReport( Abc_Ntk_t * pMiter ); extern ABC_DLL void Abc_NtkMiterReport( Abc_Ntk_t * pMiter );
extern ABC_DLL Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial, int fVerbose ); extern ABC_DLL Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial, int fVerbose );
extern ABC_DLL int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd ); extern ABC_DLL int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd, int fXor );
/*=== abcNames.c ====================================================*/ /*=== abcNames.c ====================================================*/
extern ABC_DLL char * Abc_ObjName( Abc_Obj_t * pNode ); extern ABC_DLL char * Abc_ObjName( Abc_Obj_t * pNode );
extern ABC_DLL char * Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix ); extern ABC_DLL char * Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix );
......
...@@ -6560,18 +6560,22 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -6560,18 +6560,22 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);//, * pNtkRes; Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);//, * pNtkRes;
int fReverse = 0; int fReverse = 0;
int fComb = 0; int fComb = 0;
int fXor = 0;
int c; int c;
extern int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd ); extern int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd, int fXor );
// set defaults // set defaults
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "rh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "rxh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
case 'r': case 'r':
fReverse ^= 1; fReverse ^= 1;
break; break;
case 'x':
fXor ^= 1;
break;
case 'c': case 'c':
fComb ^= 1; fComb ^= 1;
break; break;
...@@ -6612,7 +6616,7 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -6612,7 +6616,7 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
else else
{ {
if ( !Abc_NtkCombinePos( pNtk, 0 ) ) if ( !Abc_NtkCombinePos( pNtk, 0, fXor ) )
{ {
Abc_Print( -1, "ORing the POs has failed.\n" ); Abc_Print( -1, "ORing the POs has failed.\n" );
return 1; return 1;
...@@ -6626,9 +6630,10 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -6626,9 +6630,10 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: orpos [-rh]\n" ); Abc_Print( -2, "usage: orpos [-rxh]\n" );
Abc_Print( -2, "\t creates single-output miter by ORing the POs of the current network\n" ); Abc_Print( -2, "\t creates single-output miter by ORing the POs of the current network\n" );
Abc_Print( -2, "\t-r : performs the reverse transform (OR decomposition) [default = %s]\n", fReverse? "yes": "no" ); Abc_Print( -2, "\t-r : performs the reverse transform (OR decomposition) [default = %s]\n", fReverse? "yes": "no" );
Abc_Print( -2, "\t-x : toggles combining the PO using XOR [default = %s]\n", fXor? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t-h : print the command usage\n");
return 1; return 1;
} }
...@@ -6689,7 +6694,7 @@ int Abc_CommandAndPos( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -6689,7 +6694,7 @@ int Abc_CommandAndPos( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
// get the new network // get the new network
if ( !Abc_NtkCombinePos( pNtk, 1 ) ) if ( !Abc_NtkCombinePos( pNtk, 1, 0 ) )
{ {
Abc_Print( -1, "ANDing the POs has failed.\n" ); Abc_Print( -1, "ANDing the POs has failed.\n" );
return 1; return 1;
...@@ -22100,7 +22105,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -22100,7 +22105,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
Abc_Ntk_t * pNtkNew = Abc_NtkDup( pNtk ); Abc_Ntk_t * pNtkNew = Abc_NtkDup( pNtk );
Abc_Print( 0, "All %d outputs will be ORed together.\n", Abc_NtkPoNum(pNtk) ); Abc_Print( 0, "All %d outputs will be ORed together.\n", Abc_NtkPoNum(pNtk) );
if ( !Abc_NtkCombinePos( pNtkNew, 0 ) ) if ( !Abc_NtkCombinePos( pNtkNew, 0, 0 ) )
{ {
Abc_NtkDelete( pNtkNew ); Abc_NtkDelete( pNtkNew );
Abc_Print( -1, "ORing outputs has failed.\n" ); Abc_Print( -1, "ORing outputs has failed.\n" );
...@@ -32953,7 +32958,7 @@ usage: ...@@ -32953,7 +32958,7 @@ usage:
***********************************************************************/ ***********************************************************************/
int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
// Gia_Man_t * pTemp = NULL; Gia_Man_t * pTemp = NULL;
int c, fVerbose = 0; int c, fVerbose = 0;
int nFrames = 3; int nFrames = 3;
int fSwitch = 0; int fSwitch = 0;
...@@ -32973,6 +32978,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -32973,6 +32978,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// extern Gia_Man_t * Bmc_CexTarget( Gia_Man_t * p, int nFrames ); // extern Gia_Man_t * Bmc_CexTarget( Gia_Man_t * p, int nFrames );
// extern void Gia_ManMuxProfiling( Gia_Man_t * p ); // extern void Gia_ManMuxProfiling( Gia_Man_t * p );
// extern Gia_Man_t * Mig_ManTest( Gia_Man_t * pGia ); // extern Gia_Man_t * Mig_ManTest( Gia_Man_t * pGia );
extern Gia_Man_t * Gia_ManInterTest( Gia_Man_t * p );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Fsvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "Fsvh" ) ) != EOF )
...@@ -33044,6 +33050,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -33044,6 +33050,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// Gia_ManMuxProfiling( pAbc->pGia ); // Gia_ManMuxProfiling( pAbc->pGia );
// pTemp = Mig_ManTest( pAbc->pGia ); // pTemp = Mig_ManTest( pAbc->pGia );
// Abc_FrameUpdateGia( pAbc, pTemp ); // Abc_FrameUpdateGia( pAbc, pTemp );
pTemp = Gia_ManInterTest( pAbc->pGia );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: &test [-F num] [-svh]\n" ); Abc_Print( -2, "usage: &test [-F num] [-svh]\n" );
...@@ -1148,7 +1148,7 @@ int Abc_NtkDemiter( Abc_Ntk_t * pNtk ) ...@@ -1148,7 +1148,7 @@ int Abc_NtkDemiter( Abc_Ntk_t * pNtk )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd ) int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd, int fXor )
{ {
Abc_Obj_t * pNode, * pMiter; Abc_Obj_t * pNode, * pMiter;
int i; int i;
...@@ -1165,6 +1165,8 @@ int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd ) ...@@ -1165,6 +1165,8 @@ int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd )
Abc_NtkForEachPo( pNtk, pNode, i ) Abc_NtkForEachPo( pNtk, pNode, i )
if ( fAnd ) if ( fAnd )
pMiter = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) ); pMiter = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) );
else if ( fXor )
pMiter = Abc_AigXor( (Abc_Aig_t *)pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) );
else else
pMiter = Abc_AigOr( (Abc_Aig_t *)pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) ); pMiter = Abc_AigOr( (Abc_Aig_t *)pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) );
// remove the POs and their names // remove the POs and their names
......
...@@ -362,7 +362,6 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in ...@@ -362,7 +362,6 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in
***********************************************************************/ ***********************************************************************/
void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose ) void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose )
{ {
extern int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd );
extern Vec_Ptr_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int nPartSizeLimit, int fVerbose ); extern Vec_Ptr_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int nPartSizeLimit, int fVerbose );
extern void Abc_NtkConvertCos( Abc_Ntk_t * pNtk, Vec_Int_t * vOuts, Vec_Ptr_t * vOnePtr ); extern void Abc_NtkConvertCos( Abc_Ntk_t * pNtk, Vec_Int_t * vOuts, Vec_Ptr_t * vOnePtr );
...@@ -416,7 +415,7 @@ void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds ...@@ -416,7 +415,7 @@ void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds
// get this part of the miter // get this part of the miter
Abc_NtkConvertCos( pMiter, vOne, vOnePtr ); Abc_NtkConvertCos( pMiter, vOne, vOnePtr );
pMiterPart = Abc_NtkCreateConeArray( pMiter, vOnePtr, 0 ); pMiterPart = Abc_NtkCreateConeArray( pMiter, vOnePtr, 0 );
Abc_NtkCombinePos( pMiterPart, 0 ); Abc_NtkCombinePos( pMiterPart, 0, 0 );
// check the miter for being constant // check the miter for being constant
RetValue = Abc_NtkMiterIsConstant( pMiterPart ); RetValue = Abc_NtkMiterIsConstant( pMiterPart );
if ( RetValue == 0 ) if ( RetValue == 0 )
......
...@@ -6,6 +6,7 @@ SRC += src/sat/bsat/satMem.c \ ...@@ -6,6 +6,7 @@ SRC += src/sat/bsat/satMem.c \
src/sat/bsat/satProof.c \ src/sat/bsat/satProof.c \
src/sat/bsat/satSolver.c \ src/sat/bsat/satSolver.c \
src/sat/bsat/satSolver2.c \ src/sat/bsat/satSolver2.c \
src/sat/bsat/satSolver2i.c \
src/sat/bsat/satStore.c \ src/sat/bsat/satStore.c \
src/sat/bsat/satTrace.c \ src/sat/bsat/satTrace.c \
src/sat/bsat/satTruth.c \ src/sat/bsat/satTruth.c \
......
...@@ -169,6 +169,8 @@ static inline void proof_chain_start( sat_solver2* s, clause* c ) ...@@ -169,6 +169,8 @@ static inline void proof_chain_start( sat_solver2* s, clause* c )
{ {
if ( !s->fProofLogging ) if ( !s->fProofLogging )
return; return;
if ( s->pInt2 )
s->tempInter = Int2_ManChainStart( s->pInt2, c );
if ( s->pPrf2 ) if ( s->pPrf2 )
Prf_ManChainStart( s->pPrf2, c ); Prf_ManChainStart( s->pPrf2, c );
if ( s->pPrf1 ) if ( s->pPrf1 )
...@@ -186,6 +188,11 @@ static inline void proof_chain_resolve( sat_solver2* s, clause* cls, int Var ) ...@@ -186,6 +188,11 @@ static inline void proof_chain_resolve( sat_solver2* s, clause* cls, int Var )
{ {
if ( !s->fProofLogging ) if ( !s->fProofLogging )
return; return;
if ( s->pInt2 )
{
clause* c = cls ? cls : var_unit_clause( s, Var );
s->tempInter = Int2_ManChainResolve( s->pInt2, c, s->tempInter, var_is_partA(s,Var) );
}
if ( s->pPrf2 ) if ( s->pPrf2 )
{ {
clause* c = cls ? cls : var_unit_clause( s, Var ); clause* c = cls ? cls : var_unit_clause( s, Var );
...@@ -204,6 +211,12 @@ static inline int proof_chain_stop( sat_solver2* s ) ...@@ -204,6 +211,12 @@ static inline int proof_chain_stop( sat_solver2* s )
{ {
if ( !s->fProofLogging ) if ( !s->fProofLogging )
return 0; return 0;
if ( s->pInt2 )
{
int h = s->tempInter;
s->tempInter = -1;
return h;
}
if ( s->pPrf2 ) if ( s->pPrf2 )
Prf_ManChainStop( s->pPrf2 ); Prf_ManChainStop( s->pPrf2 );
if ( s->pPrf1 ) if ( s->pPrf1 )
...@@ -410,7 +423,7 @@ static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, ...@@ -410,7 +423,7 @@ static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt,
assert( proof_id ); assert( proof_id );
c->lbd = sat_clause_compute_lbd( s, c ); c->lbd = sat_clause_compute_lbd( s, c );
assert( clause_id(c) == veci_size(&s->act_clas) ); assert( clause_id(c) == veci_size(&s->act_clas) );
if ( s->pPrf1 ) if ( s->pPrf1 || s->pInt2 )
veci_push(&s->claProofs, proof_id); veci_push(&s->claProofs, proof_id);
// veci_push(&s->act_clas, (1<<10)); // veci_push(&s->act_clas, (1<<10));
veci_push(&s->act_clas, 0); veci_push(&s->act_clas, 0);
...@@ -1141,6 +1154,7 @@ sat_solver2* sat_solver2_new(void) ...@@ -1141,6 +1154,7 @@ sat_solver2* sat_solver2_new(void)
// proof-logging // proof-logging
veci_new(&s->claProofs); veci_new(&s->claProofs);
// s->pPrf1 = Vec_SetAlloc( 20 ); // s->pPrf1 = Vec_SetAlloc( 20 );
s->tempInter = -1;
// initialize clause pointers // initialize clause pointers
s->hLearntLast = -1; // the last learnt clause s->hLearntLast = -1; // the last learnt clause
...@@ -1244,6 +1258,7 @@ void sat_solver2_delete(sat_solver2* s) ...@@ -1244,6 +1258,7 @@ void sat_solver2_delete(sat_solver2* s)
// veci_delete(&s->proofs); // veci_delete(&s->proofs);
Vec_SetFree( s->pPrf1 ); Vec_SetFree( s->pPrf1 );
Prf_ManStop( s->pPrf2 ); Prf_ManStop( s->pPrf2 );
Int2_ManStop( s->pInt2 );
// delete arrays // delete arrays
if (s->vi != 0){ if (s->vi != 0){
......
...@@ -42,6 +42,7 @@ ABC_NAMESPACE_HEADER_START ...@@ -42,6 +42,7 @@ ABC_NAMESPACE_HEADER_START
struct sat_solver2_t; struct sat_solver2_t;
typedef struct sat_solver2_t sat_solver2; typedef struct sat_solver2_t sat_solver2;
typedef struct Int2_Man_t_ Int2_Man_t;
extern sat_solver2* sat_solver2_new(void); extern sat_solver2* sat_solver2_new(void);
extern void sat_solver2_delete(sat_solver2* s); extern void sat_solver2_delete(sat_solver2* s);
...@@ -72,6 +73,14 @@ extern void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ); ...@@ -72,6 +73,14 @@ extern void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars );
extern word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars ); extern word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars );
extern void Sat_ProofCheck( sat_solver2 * s ); extern void Sat_ProofCheck( sat_solver2 * s );
// interpolation APIs
extern Int2_Man_t * Int2_ManStart( sat_solver2 * pSat, int * pGloVars, int nGloVars );
extern void Int2_ManStop( Int2_Man_t * p );
extern int Int2_ManChainStart( Int2_Man_t * p, clause * c );
extern int Int2_ManChainResolve( Int2_Man_t * p, clause * c, int iLit, int varA );
extern void * Int2_ManReadInterpolant( sat_solver2 * s );
//================================================================================================= //=================================================================================================
// Solver representation: // Solver representation:
...@@ -156,6 +165,8 @@ struct sat_solver2_t ...@@ -156,6 +165,8 @@ struct sat_solver2_t
int hProofLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) int hProofLast; // in proof-logging mode, the ID of the final conflict clause (conf_final)
Prf_Man_t * pPrf2; // another proof manager Prf_Man_t * pPrf2; // another proof manager
double dPrfMemory; // memory used by the proof-logger double dPrfMemory; // memory used by the proof-logger
Int2_Man_t * pInt2; // interpolation manager
int tempInter; // temporary storage for the interpolant
// statistics // statistics
stats_t stats; stats_t stats;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment