summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/abc/abc.h2
-rw-r--r--src/base/abci/abc.c22
-rw-r--r--src/base/abci/abcMiter.c4
-rw-r--r--src/base/abci/abcVerify.c3
-rw-r--r--src/sat/bsat/module.make1
-rw-r--r--src/sat/bsat/satSolver2.c17
-rw-r--r--src/sat/bsat/satSolver2.h11
7 files changed, 48 insertions, 12 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 2d3e7588..4b8a88eb 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -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 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 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 ====================================================*/
extern ABC_DLL char * Abc_ObjName( Abc_Obj_t * pNode );
extern ABC_DLL char * Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b45fde8f..74525e26 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -6560,18 +6560,22 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);//, * pNtkRes;
int fReverse = 0;
int fComb = 0;
+ int fXor = 0;
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
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "rh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "rxh" ) ) != EOF )
{
switch ( c )
{
case 'r':
fReverse ^= 1;
break;
+ case 'x':
+ fXor ^= 1;
+ break;
case 'c':
fComb ^= 1;
break;
@@ -6612,7 +6616,7 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv )
}
else
{
- if ( !Abc_NtkCombinePos( pNtk, 0 ) )
+ if ( !Abc_NtkCombinePos( pNtk, 0, fXor ) )
{
Abc_Print( -1, "ORing the POs has failed.\n" );
return 1;
@@ -6626,9 +6630,10 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
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-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");
return 1;
}
@@ -6689,7 +6694,7 @@ int Abc_CommandAndPos( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// get the new network
- if ( !Abc_NtkCombinePos( pNtk, 1 ) )
+ if ( !Abc_NtkCombinePos( pNtk, 1, 0 ) )
{
Abc_Print( -1, "ANDing the POs has failed.\n" );
return 1;
@@ -22100,7 +22105,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtkNew = Abc_NtkDup( 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_Print( -1, "ORing outputs has failed.\n" );
@@ -32953,7 +32958,7 @@ usage:
***********************************************************************/
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 nFrames = 3;
int fSwitch = 0;
@@ -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 void Gia_ManMuxProfiling( Gia_Man_t * p );
// extern Gia_Man_t * Mig_ManTest( Gia_Man_t * pGia );
+ extern Gia_Man_t * Gia_ManInterTest( Gia_Man_t * p );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Fsvh" ) ) != EOF )
@@ -33044,6 +33050,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// Gia_ManMuxProfiling( pAbc->pGia );
// pTemp = Mig_ManTest( pAbc->pGia );
// Abc_FrameUpdateGia( pAbc, pTemp );
+ pTemp = Gia_ManInterTest( pAbc->pGia );
+ Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &test [-F num] [-svh]\n" );
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 8c5a4a83..747fe263 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -1148,7 +1148,7 @@ int Abc_NtkDemiter( Abc_Ntk_t * pNtk )
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;
int i;
@@ -1165,6 +1165,8 @@ int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd )
Abc_NtkForEachPo( pNtk, pNode, i )
if ( fAnd )
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
pMiter = Abc_AigOr( (Abc_Aig_t *)pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) );
// remove the POs and their names
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 7d9973b1..25d1d113 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -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 )
{
- 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 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
// get this part of the miter
Abc_NtkConvertCos( pMiter, vOne, vOnePtr );
pMiterPart = Abc_NtkCreateConeArray( pMiter, vOnePtr, 0 );
- Abc_NtkCombinePos( pMiterPart, 0 );
+ Abc_NtkCombinePos( pMiterPart, 0, 0 );
// check the miter for being constant
RetValue = Abc_NtkMiterIsConstant( pMiterPart );
if ( RetValue == 0 )
diff --git a/src/sat/bsat/module.make b/src/sat/bsat/module.make
index e54dc891..4e85bece 100644
--- a/src/sat/bsat/module.make
+++ b/src/sat/bsat/module.make
@@ -6,6 +6,7 @@ SRC += src/sat/bsat/satMem.c \
src/sat/bsat/satProof.c \
src/sat/bsat/satSolver.c \
src/sat/bsat/satSolver2.c \
+ src/sat/bsat/satSolver2i.c \
src/sat/bsat/satStore.c \
src/sat/bsat/satTrace.c \
src/sat/bsat/satTruth.c \
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 84d59f62..96656b5b 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -169,6 +169,8 @@ static inline void proof_chain_start( sat_solver2* s, clause* c )
{
if ( !s->fProofLogging )
return;
+ if ( s->pInt2 )
+ s->tempInter = Int2_ManChainStart( s->pInt2, c );
if ( s->pPrf2 )
Prf_ManChainStart( s->pPrf2, c );
if ( s->pPrf1 )
@@ -186,6 +188,11 @@ static inline void proof_chain_resolve( sat_solver2* s, clause* cls, int Var )
{
if ( !s->fProofLogging )
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 )
{
clause* c = cls ? cls : var_unit_clause( s, Var );
@@ -204,6 +211,12 @@ static inline int proof_chain_stop( sat_solver2* s )
{
if ( !s->fProofLogging )
return 0;
+ if ( s->pInt2 )
+ {
+ int h = s->tempInter;
+ s->tempInter = -1;
+ return h;
+ }
if ( s->pPrf2 )
Prf_ManChainStop( s->pPrf2 );
if ( s->pPrf1 )
@@ -410,7 +423,7 @@ static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt,
assert( proof_id );
c->lbd = sat_clause_compute_lbd( s, c );
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->act_clas, (1<<10));
veci_push(&s->act_clas, 0);
@@ -1141,6 +1154,7 @@ sat_solver2* sat_solver2_new(void)
// proof-logging
veci_new(&s->claProofs);
// s->pPrf1 = Vec_SetAlloc( 20 );
+ s->tempInter = -1;
// initialize clause pointers
s->hLearntLast = -1; // the last learnt clause
@@ -1244,6 +1258,7 @@ void sat_solver2_delete(sat_solver2* s)
// veci_delete(&s->proofs);
Vec_SetFree( s->pPrf1 );
Prf_ManStop( s->pPrf2 );
+ Int2_ManStop( s->pInt2 );
// delete arrays
if (s->vi != 0){
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index d7d16d73..41dfc680 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -42,6 +42,7 @@ ABC_NAMESPACE_HEADER_START
struct sat_solver2_t;
typedef struct sat_solver2_t sat_solver2;
+typedef struct Int2_Man_t_ Int2_Man_t;
extern sat_solver2* sat_solver2_new(void);
extern void sat_solver2_delete(sat_solver2* s);
@@ -72,6 +73,14 @@ extern void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars );
extern word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars );
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:
@@ -156,6 +165,8 @@ struct sat_solver2_t
int hProofLast; // in proof-logging mode, the ID of the final conflict clause (conf_final)
Prf_Man_t * pPrf2; // another proof manager
double dPrfMemory; // memory used by the proof-logger
+ Int2_Man_t * pInt2; // interpolation manager
+ int tempInter; // temporary storage for the interpolant
// statistics
stats_t stats;
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 20:17:22 +0000