summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/proof/pdr/pdrCnf.c22
-rw-r--r--src/proof/pdr/pdrCore.c6
-rw-r--r--src/proof/pdr/pdrIncr.c2
-rw-r--r--src/proof/pdr/pdrInt.h26
-rw-r--r--src/proof/pdr/pdrMan.c20
-rw-r--r--src/proof/pdr/pdrSat.c22
-rw-r--r--src/proof/pdr/pdrTsim.c4
-rw-r--r--src/proof/pdr/pdrTsim3.c2
-rw-r--r--src/proof/pdr/pdrUtil.c6
9 files changed, 68 insertions, 42 deletions
diff --git a/src/proof/pdr/pdrCnf.c b/src/proof/pdr/pdrCnf.c
index 016830c3..e0f1641c 100644
--- a/src/proof/pdr/pdrCnf.c
+++ b/src/proof/pdr/pdrCnf.c
@@ -86,7 +86,7 @@ static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pOb
sat_solver_setnvars( pSat, iVarNew + 1 );
if ( k == 0 && Saig_ObjIsLo(p->pAig, pObj) ) // initialize the register output
{
- int Lit = toLitCond( iVarNew, 1 );
+ int Lit = Abc_Var2Lit( iVarNew, 1 );
int RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
assert( RetValue == 1 );
(void) RetValue;
@@ -136,11 +136,11 @@ int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int Level, int Pol )
for ( i = iClaBeg; i < iClaEnd; i++ )
{
Vec_IntClear( vLits );
- Vec_IntPush( vLits, toLitCond( iVarThis, lit_sign(p->pCnf2->pClauses[i][0]) ) );
+ Vec_IntPush( vLits, Abc_Var2Lit( iVarThis, Abc_LitIsCompl(p->pCnf2->pClauses[i][0]) ) );
for ( pLit = p->pCnf2->pClauses[i]+1; pLit < p->pCnf2->pClauses[i+1]; pLit++ )
{
- iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)), Level+1, 3 );
- Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) );
+ iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, Abc_Lit2Var(*pLit)), Level+1, 3 );
+ Vec_IntPush( vLits, Abc_Var2Lit( iVar, Abc_LitIsCompl(*pLit) ) );
}
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
assert( RetValue );
@@ -154,11 +154,11 @@ int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int Level, int Pol )
if ( 2 - !Abc_LitIsCompl(p->pCnf2->pClauses[i][0]) == (Pol & ~PolPres) ) // taking opposite literal
{
Vec_IntClear( vLits );
- Vec_IntPush( vLits, toLitCond( iVarThis, Abc_LitIsCompl(p->pCnf2->pClauses[i][0]) ) );
+ Vec_IntPush( vLits, Abc_Var2Lit( iVarThis, Abc_LitIsCompl(p->pCnf2->pClauses[i][0]) ) );
for ( pLit = p->pCnf2->pClauses[i]+1; pLit < p->pCnf2->pClauses[i+1]; pLit++ )
{
- iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)), Level+1, ((unsigned)p->pCnf2->pClaPols[i] >> (2*(pLit-p->pCnf2->pClauses[i]-1))) & 3 );
- Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) );
+ iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, Abc_Lit2Var(*pLit)), Level+1, ((unsigned)p->pCnf2->pClaPols[i] >> (2*(pLit-p->pCnf2->pClauses[i]-1))) & 3 );
+ Vec_IntPush( vLits, Abc_Var2Lit( iVar, Abc_LitIsCompl(*pLit) ) );
}
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
assert( RetValue );
@@ -187,7 +187,7 @@ static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pOb
sat_solver_setnvars( pSat, iVarNew + 1 );
if ( k == 0 && Saig_ObjIsLo(p->pAig, pObj) ) // initialize the register output
{
- int Lit = toLitCond( iVarNew, 1 );
+ int Lit = Abc_Var2Lit( iVarNew, 1 );
int RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
assert( RetValue == 1 );
(void) RetValue;
@@ -213,11 +213,11 @@ int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int Level, int Pol )
for ( i = iClaBeg; i < iClaEnd; i++ )
{
Vec_IntClear( vLits );
- Vec_IntPush( vLits, toLitCond( iVarThis, lit_sign(p->pCnf2->pClauses[i][0]) ) );
+ Vec_IntPush( vLits, Abc_Var2Lit( iVarThis, Abc_LitIsCompl(p->pCnf2->pClauses[i][0]) ) );
for ( pLit = p->pCnf2->pClauses[i]+1; pLit < p->pCnf2->pClauses[i+1]; pLit++ )
{
- iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)), Level+1, Pol );
- Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) );
+ iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, Abc_Lit2Var(*pLit)), Level+1, Pol );
+ Vec_IntPush( vLits, Abc_Var2Lit( iVar, Abc_LitIsCompl(*pLit) ) );
}
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
assert( RetValue );
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 60454752..7e5218d0 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -107,13 +107,13 @@ Pdr_Set_t * Pdr_ManReduceClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
assert( Vec_IntSize(vLits) < pCube->nLits );
// if the cube overlaps with init, add any literal
Vec_IntForEachEntry( vLits, Entry, i )
- if ( lit_sign(Entry) == 0 ) // positive literal
+ if ( Abc_LitIsCompl(Entry) == 0 ) // positive literal
break;
if ( i == Vec_IntSize(vLits) ) // only negative literals
{
// add the first positive literal
for ( i = 0; i < pCube->nLits; i++ )
- if ( lit_sign(pCube->Lits[i]) == 0 ) // positive literal
+ if ( Abc_LitIsCompl(pCube->Lits[i]) == 0 ) // positive literal
{
Vec_IntPush( vLits, pCube->Lits[i] );
break;
@@ -524,6 +524,7 @@ static inline int Vec_IntSelectSortPrioReverseLit( int * pArray, int nSize, Vec_
***********************************************************************/
int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppCubeMin )
{
+#if 0
int fUseMinAss = 0;
sat_solver * pSat = Pdr_ManFetchSolver( p, k );
int Order = Vec_IntSelectSortPrioReverseLit( pCube->Lits, pCube->nLits, p->vPrio );
@@ -661,6 +662,7 @@ int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** pp
*ppCubeMin = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits1), Vec_IntSize(vLits1) );
assert( !Pdr_SetIsInit(*ppCubeMin, -1) );
Order = 0;
+#endif
return 0;
}
diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c
index 7bb3319d..186791b2 100644
--- a/src/proof/pdr/pdrIncr.c
+++ b/src/proof/pdr/pdrIncr.c
@@ -896,7 +896,7 @@ int IPdr_ManCheckCubeReduce( Pdr_Man_t * p, Vec_Ptr_t * vClauses, Pdr_Set_t * pC
if ( pCube == NULL ) // solve the property
{
- Lit = toLit( Pdr_ObjSatVar(p, 1, 2, Aig_ManCo(p->pAig, p->iOutCur)) ); // pos literal (property fails)
+ Lit = Abc_Var2Lit( Pdr_ObjSatVar(p, 1, 2, Aig_ManCo(p->pAig, p->iOutCur)), 0 ); // pos literal (property fails)
RetValue = sat_solver_addclause( pSat, &Lit, &Lit+1 );
assert( RetValue == 1 );
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index 2a8ab023..639276db 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -28,11 +28,35 @@
#include "aig/saig/saig.h"
#include "misc/vec/vecWec.h"
#include "sat/cnf/cnf.h"
-#include "sat/bsat/satSolver.h"
#include "pdr.h"
#include "misc/hash/hashInt.h"
#include "aig/gia/giaAig.h"
+//#define PDR_USE_SATOKO 1
+
+#ifndef PDR_USE_SATOKO
+ #include "sat/bsat/satSolver.h"
+#else
+ #include "sat/satoko/satoko.h"
+ #include "sat/satoko/solver.h"
+ #define l_Undef 0
+ #define l_True 1
+ #define l_False -1
+ #define sat_solver satoko_t
+ #define sat_solver_new satoko_create
+ #define sat_solver_delete satoko_destroy
+ #define zsat_solver_new_seed(s) satoko_create()
+ #define zsat_solver_restart_seed(s,a) satoko_reset(s)
+ #define sat_solver_nvars solver_varnum
+ #define sat_solver_setnvars satoko_setnvars
+ #define sat_solver_addclause(s,b,e) satoko_add_clause(s,b,e-b)
+ #define sat_solver_final satoko_final_conflict
+ #define sat_solver_solve(s,b,e,c,x,y,z) satoko_solve_assumptions_limit(s,b,e-b,(int)c)
+ #define sat_solver_var_value solver_read_cex_varvalue
+ #define sat_solver_set_runtime_limit solver_set_runtime_limit
+ #define sat_solver_compress(s)
+#endif
+
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index cb51e51e..7686ec03 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -421,12 +421,12 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
{
Lit = pObl->pState->Lits[i];
- if ( lit_sign(Lit) )
+ if ( Abc_LitIsCompl(Lit) )
continue;
- if ( lit_var(Lit) >= pCex->nPis ) // allows PPI literals to be thrown away
+ if ( Abc_Lit2Var(Lit) >= pCex->nPis ) // allows PPI literals to be thrown away
continue;
- assert( lit_var(Lit) < pCex->nPis );
- Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) );
+ assert( Abc_Lit2Var(Lit) < pCex->nPis );
+ Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Abc_Lit2Var(Lit) );
}
assert( f == nFrames );
if ( !Saig_ManVerifyCex(p->pAig, pCex) )
@@ -470,9 +470,9 @@ Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p )
for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
{
Lit = pObl->pState->Lits[i];
- if ( lit_var(Lit) < nPis ) // PI literal
+ if ( Abc_Lit2Var(Lit) < nPis ) // PI literal
continue;
- Flop = lit_var(Lit) - nPis;
+ Flop = Abc_Lit2Var(Lit) - nPis;
if ( Vec_IntEntry(p->vMapFf2Ppi, Flop) >= 0 ) // already used PPI literal
continue;
Vec_IntWriteEntry( p->vMapFf2Ppi, Flop, Vec_IntSize(p->vMapPpi2Ff) );
@@ -502,13 +502,13 @@ Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p )
for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
{
Lit = pObl->pState->Lits[i];
- if ( lit_sign(Lit) )
+ if ( Abc_LitIsCompl(Lit) )
continue;
- if ( lit_var(Lit) < nPis ) // PI literal
- Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) );
+ if ( Abc_Lit2Var(Lit) < nPis ) // PI literal
+ Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Abc_Lit2Var(Lit) );
else
{
- int iPPI = nPis + Vec_IntEntry(p->vMapFf2Ppi, lit_var(Lit) - nPis);
+ int iPPI = nPis + Vec_IntEntry(p->vMapFf2Ppi, Abc_Lit2Var(Lit) - nPis);
assert( iPPI < pCex->nPis );
Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + iPPI );
}
diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c
index 3c1bbad0..b1a5b66c 100644
--- a/src/proof/pdr/pdrSat.c
+++ b/src/proof/pdr/pdrSat.c
@@ -120,11 +120,11 @@ Vec_Int_t * Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, int nArray )
Vec_IntClear( p->vLits );
for ( i = 0; i < nArray; i++ )
{
- RegId = Pdr_ObjRegNum( p, k, lit_var(pArray[i]) );
+ RegId = Pdr_ObjRegNum( p, k, Abc_Lit2Var(pArray[i]) );
if ( RegId == -1 )
continue;
assert( RegId >= 0 && RegId < Aig_ManRegNum(p->pAig) );
- Vec_IntPush( p->vLits, toLitCond(RegId, !lit_sign(pArray[i])) );
+ Vec_IntPush( p->vLits, Abc_Var2Lit(RegId, !Abc_LitIsCompl(pArray[i])) );
}
assert( Vec_IntSize(p->vLits) >= 0 && Vec_IntSize(p->vLits) <= nArray );
return p->vLits;
@@ -153,12 +153,12 @@ Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCom
if ( pCube->Lits[i] == -1 )
continue;
if ( fNext )
- pObj = Saig_ManLi( p->pAig, lit_var(pCube->Lits[i]) );
+ pObj = Saig_ManLi( p->pAig, Abc_Lit2Var(pCube->Lits[i]) );
else
- pObj = Saig_ManLo( p->pAig, lit_var(pCube->Lits[i]) );
- iVar = Pdr_ObjSatVar( p, k, fNext ? 2 - lit_sign(pCube->Lits[i]) : 3, pObj ); assert( iVar >= 0 );
+ pObj = Saig_ManLo( p->pAig, Abc_Lit2Var(pCube->Lits[i]) );
+ iVar = Pdr_ObjSatVar( p, k, fNext ? 2 - Abc_LitIsCompl(pCube->Lits[i]) : 3, pObj ); assert( iVar >= 0 );
iVarMax = Abc_MaxInt( iVarMax, iVar );
- Vec_IntPush( p->vLits, toLitCond( iVar, fCompl ^ lit_sign(pCube->Lits[i]) ) );
+ Vec_IntPush( p->vLits, Abc_Var2Lit( iVar, fCompl ^ Abc_LitIsCompl(pCube->Lits[i]) ) );
}
// sat_solver_setnvars( Pdr_ManSolver(p, k), iVarMax + 1 );
p->tCnf += Abc_Clock() - clk;
@@ -192,7 +192,7 @@ void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k )
// skip timedout outputs
if ( p->pPars->vOutMap && Vec_IntEntry(p->pPars->vOutMap, i) == -1 )
continue;
- Lit = toLitCond( Pdr_ObjSatVar(p, k, 1, pObj), 1 ); // neg literal
+ Lit = Abc_Var2Lit( Pdr_ObjSatVar(p, k, 1, pObj), 1 ); // neg literal
RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
assert( RetValue == 1 );
}
@@ -300,7 +300,7 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
if ( pCube == NULL ) // solve the property
{
clk = Abc_Clock();
- Lit = toLit( Pdr_ObjSatVar(p, k, 2, Aig_ManCo(p->pAig, p->iOutCur)) ); // pos literal (property fails)
+ Lit = Abc_Var2Lit( Pdr_ObjSatVar(p, k, 2, Aig_ManCo(p->pAig, p->iOutCur)), 0 ); // pos literal (property fails)
Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 );
sat_solver_set_runtime_limit( pSat, Limit );
@@ -316,7 +316,7 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
// add the cube in terms of current state variables
vLits = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
// add activation literal
- Lit = toLit( Pdr_ManFreeVar(p, k) );
+ Lit = Abc_Var2Lit( Pdr_ManFreeVar(p, k), 0 );
// add activation literal
Vec_IntPush( vLits, Lit );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
@@ -325,7 +325,7 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
// create assumptions
vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
// add activation literal
- Vec_IntPush( vLits, lit_neg(Lit) );
+ Vec_IntPush( vLits, Abc_LitNot(Lit) );
}
else
vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
@@ -376,7 +376,7 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
if ( fLitUsed )
{
int RetValue;
- Lit = lit_neg(Lit);
+ Lit = Abc_LitNot(Lit);
RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
assert( RetValue == 1 );
sat_solver_compress( pSat );
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c
index acbf70f5..5bc0d3d6 100644
--- a/src/proof/pdr/pdrTsim.c
+++ b/src/proof/pdr/pdrTsim.c
@@ -289,14 +289,14 @@ void Pdr_ManDeriveResult( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCi
{
if ( Saig_ObjIsPi(pAig, pObj) )
{
- Lit = toLitCond( Aig_ObjCioId(pObj), (Vec_IntEntry(vCiVals, i) == 0) );
+ Lit = Abc_Var2Lit( Aig_ObjCioId(pObj), (Vec_IntEntry(vCiVals, i) == 0) );
Vec_IntPush( vPiLits, Lit );
continue;
}
assert( Saig_ObjIsLo(pAig, pObj) );
if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
continue;
- Lit = toLitCond( Aig_ObjCioId(pObj) - Saig_ManPiNum(pAig), (Vec_IntEntry(vCiVals, i) == 0) );
+ Lit = Abc_Var2Lit( Aig_ObjCioId(pObj) - Saig_ManPiNum(pAig), (Vec_IntEntry(vCiVals, i) == 0) );
Vec_IntPush( vRes, Lit );
}
if ( Vec_IntSize(vRes) == 0 )
diff --git a/src/proof/pdr/pdrTsim3.c b/src/proof/pdr/pdrTsim3.c
index ebd1a702..3e24a356 100644
--- a/src/proof/pdr/pdrTsim3.c
+++ b/src/proof/pdr/pdrTsim3.c
@@ -233,7 +233,7 @@ Abc_Print( 1, " in frame %d.\n", k );
// read solver
pSat = Pdr_ManFetchSolver( p->pMan, k );
- LitAux = toLit( Pdr_ManFreeVar(p->pMan, k) );
+ LitAux = Abc_Var2Lit( Pdr_ManFreeVar(p->pMan, k), 0 );
// add the clause (complemented cube) in terms of next state variables
if ( pCube == NULL ) // the target is the property output
{
diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c
index 986697ac..b2eaa2c7 100644
--- a/src/proof/pdr/pdrUtil.c
+++ b/src/proof/pdr/pdrUtil.c
@@ -234,7 +234,7 @@ void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCoun
{
if ( p->Lits[i] == -1 )
continue;
- pBuff[lit_var(p->Lits[i])] = (lit_sign(p->Lits[i])? '0':'1');
+ pBuff[Abc_Lit2Var(p->Lits[i])] = (Abc_LitIsCompl(p->Lits[i])? '0':'1');
}
if ( vFlopCounts )
{
@@ -351,7 +351,7 @@ void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vF
{
if ( p->Lits[i] == -1 )
continue;
- pBuff[lit_var(p->Lits[i])] = (lit_sign(p->Lits[i])? '0':'1');
+ pBuff[Abc_Lit2Var(p->Lits[i])] = (Abc_LitIsCompl(p->Lits[i])? '0':'1');
}
if ( vFlopCounts )
{
@@ -465,7 +465,7 @@ int Pdr_SetIsInit( Pdr_Set_t * pCube, int iRemove )
assert( pCube->Lits[i] != -1 );
if ( i == iRemove )
continue;
- if ( lit_sign( pCube->Lits[i] ) == 0 )
+ if ( Abc_LitIsCompl( pCube->Lits[i] ) == 0 )
return 0;
}
return 1;
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-29 02:55:04 +0000