luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Integrating Satoko into pdr.

This commit is contained in:
Alan Mishchenko 2017-08-16 12:08:55 +07:00
parent 6ff66ed49e
commit 29cb71f98b
9 changed files with 68 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
src/proof/pdr/pdrCnf.c
View File

@ -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 );

6
src/proof/pdr/pdrCore.c
View File

@ -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;
}

2
src/proof/pdr/pdrIncr.c
View File

@ -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 );

26
src/proof/pdr/pdrInt.h
View File

@ -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
////////////////////////////////////////////////////////////////////////

20
src/proof/pdr/pdrMan.c
View File

@ -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 );
}

22
src/proof/pdr/pdrSat.c
View File

@ -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 );

4
src/proof/pdr/pdrTsim.c
View File

@ -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 )

2
src/proof/pdr/pdrTsim3.c
View File

@ -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
{

6
src/proof/pdr/pdrUtil.c
View File

@ -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;