Skip to content

A
abc
Commit bc2f199b by Alan Mishchenko
Options

Started SAT-based reparameterization.

parent 8fdc5d22
Showing with 478 additions and 151 deletions
abclib.dsp
......@@ -3227,6 +3227,10 @@ SOURCE=.\src\aig\aig\aigPartSat.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigRepar.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigRepr.c
# End Source File
# Begin Source File
......
src/aig/aig/aigRepar.c 0 → 100644
/**CFile****************************************************************
FileName [aigRepar.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG package.]
Synopsis [Interpolation-based reparametrization.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: aigRepar.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "aig.h"
#include "cnf.h"
#include "satSolver2.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Adds buffer to the solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Aig_ManInterAddBuffer( sat_solver2 * pSat, int iVarA, int iVarB, int fCompl, int fMark )
{
lit Lits[2];
int Cid;
assert( iVarA >= 0 && iVarB >= 0 );
Lits[0] = toLitCond( iVarA, 0 );
Lits[1] = toLitCond( iVarB, !fCompl );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVarA, 1 );
Lits[1] = toLitCond( iVarB, fCompl );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
}
/**Function*************************************************************
Synopsis [Adds constraints for the two-input AND-gate.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Aig_ManInterAddXor( sat_solver2 * pSat, int iVarA, int iVarB, int iVarC, int fCompl, int fMark )
{
lit Lits[3];
int Cid;
assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
Lits[0] = toLitCond( iVarA, !fCompl );
Lits[1] = toLitCond( iVarB, 1 );
Lits[2] = toLitCond( iVarC, 1 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVarA, !fCompl );
Lits[1] = toLitCond( iVarB, 0 );
Lits[2] = toLitCond( iVarC, 0 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVarA, fCompl );
Lits[1] = toLitCond( iVarB, 1 );
Lits[2] = toLitCond( iVarC, 0 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
Lits[0] = toLitCond( iVarA, fCompl );
Lits[1] = toLitCond( iVarB, 0 );
Lits[2] = toLitCond( iVarC, 1 );
Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
if ( fMark )
clause_set_partA( pSat, Cid, 1 );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManInterTest( Aig_Man_t * pMan, int fVerbose )
{
sat_solver2 * pSat;
Aig_Man_t * pInter;
Vec_Int_t * vVars;
Cnf_Dat_t * pCnf;
Aig_Obj_t * pObj;
int Lit, Cid, Var, status, i;
int clk = clock();
assert( Aig_ManRegNum(pMan) == 0 );
assert( Aig_ManPoNum(pMan) == 1 );
// derive CNFs
pCnf = Cnf_Derive( pMan, 1 );
// start the solver
pSat = sat_solver2_new();
sat_solver2_setnvars( pSat, 2*pCnf->nVars+1 );
// set A-variables (all used except PI/PO)
Aig_ManForEachObj( pMan, pObj, i )
{
if ( pCnf->pVarNums[pObj->Id] < 0 )
continue;
if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsPo(pObj) )
var_set_partA( pSat, pCnf->pVarNums[pObj->Id], 1 );
}
// add clauses of A
for ( i = 0; i < pCnf->nClauses; i++ )
{
Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] );
clause_set_partA( pSat, Cid, 1 );
}
// add clauses of B
Cnf_DataLift( pCnf, pCnf->nVars );
for ( i = 0; i < pCnf->nClauses; i++ )
sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] );
Cnf_DataLift( pCnf, -pCnf->nVars );
// add PI equality clauses
vVars = Vec_IntAlloc( Aig_ManPoNum(pMan)+1 );
Aig_ManForEachPi( pMan, pObj, i )
{
if ( Aig_ObjRefs(pObj) == 0 )
continue;
Var = pCnf->pVarNums[pObj->Id];
Aig_ManInterAddBuffer( pSat, Var, pCnf->nVars + Var, 0, 0 );
Vec_IntPush( vVars, Var );
}
// add an XOR clause in the end
Var = pCnf->pVarNums[Aig_ManPo(pMan,0)->Id];
Aig_ManInterAddXor( pSat, Var, pCnf->nVars + Var, 2*pCnf->nVars, 0, 0 );
Vec_IntPush( vVars, Var );
// solve the problem
Lit = toLitCond( 2*pCnf->nVars, 0 );
status = sat_solver2_solve( pSat, &Lit, &Lit + 1, 0, 0, 0, 0 );
assert( status == l_False );
Sat_Solver2PrintStats( stdout, pSat );
// derive interpolant
pInter = Sat_ProofInterpolant( pSat, vVars );
Aig_ManPrintStats( pInter );
Aig_ManDumpBlif( pInter, "int.blif", NULL, NULL );
// clean up
Aig_ManStop( pInter );
Vec_IntFree( vVars );
Cnf_DataFree( pCnf );
sat_solver2_delete( pSat );
ABC_PRT( "Total interpolation time", clock() - clk );
}
/**Function*************************************************************
Synopsis [Duplicates AIG while mapping PIs into the given array.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManAppend( Aig_Man_t * pBase, Aig_Man_t * pNew )
{
Aig_Obj_t * pObj;
int i;
assert( Aig_ManPoNum(pNew) == 1 );
assert( Aig_ManPiNum(pNew) == Aig_ManPiNum(pBase) );
// create the PIs
Aig_ManCleanData( pNew );
Aig_ManConst1(pNew)->pData = Aig_ManConst1(pBase);
Aig_ManForEachPi( pNew, pObj, i )
pObj->pData = Aig_IthVar(pBase, i);
// duplicate internal nodes
Aig_ManForEachNode( pNew, pObj, i )
pObj->pData = Aig_And( pBase, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
// add one PO to base
pObj = Aig_ManPo( pNew, 0 );
Aig_ObjCreatePo( pBase, Aig_ObjChild0Copy(pObj) );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose )
{
Aig_Man_t * pAigTemp, * pInter, * pBase = NULL;
sat_solver2 * pSat;
Vec_Int_t * vVars;
Cnf_Dat_t * pCnf, * pCnfInter;
Aig_Obj_t * pObj;
int nOuts = Aig_ManPoNum(pMan);
int ShiftP[2], ShiftCnf[2], ShiftOr[2], ShiftAssume;
int Cid, Lit, status, i, k, c;
int clk = clock();
assert( Aig_ManRegNum(pMan) == 0 );
// derive CNFs
pCnf = Cnf_Derive( pMan, nOuts );
// start the solver
pSat = sat_solver2_new();
sat_solver2_setnvars( pSat, 4*pCnf->nVars + 6*nOuts );
// vars: pGlobal + (p0 + A1 + A2 + or0) + (p1 + B1 + B2 + or1) + pAssume;
ShiftP[0] = nOuts;
ShiftP[1] = 2*pCnf->nVars + 3*nOuts;
ShiftCnf[0] = ShiftP[0] + nOuts;
ShiftCnf[1] = ShiftP[1] + nOuts;
ShiftOr[0] = ShiftCnf[0] + 2*pCnf->nVars;
ShiftOr[1] = ShiftCnf[1] + 2*pCnf->nVars;
ShiftAssume = ShiftOr[1] + nOuts;
assert( ShiftAssume + nOuts == pSat->size );
// mark variables of A
for ( i = ShiftCnf[0]; i < ShiftP[1]; i++ )
var_set_partA( pSat, i, 1 );
// add clauses of A, then B
vVars = Vec_IntAlloc( 2*nOuts );
for ( k = 0; k < 2; k++ )
{
// copy A1
Cnf_DataLift( pCnf, ShiftCnf[k] );
for ( i = 0; i < pCnf->nClauses; i++ )
{
Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] );
clause_set_partA( pSat, Cid, k==0 );
}
// add equality p[k] == A1/B1
Aig_ManForEachPo( pMan, pObj, i )
Aig_ManInterAddBuffer( pSat, ShiftP[k] + i, pCnf->pVarNums[pObj->Id], k==1, k==0 );
// copy A2
Cnf_DataLift( pCnf, pCnf->nVars );
for ( i = 0; i < pCnf->nClauses; i++ )
{
Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] );
clause_set_partA( pSat, Cid, k==0 );
}
// add comparator (!p[k] ^ A2/B2) == or[k]
Vec_IntClear( vVars );
Aig_ManForEachPo( pMan, pObj, i )
{
Aig_ManInterAddXor( pSat, ShiftP[k] + i, pCnf->pVarNums[pObj->Id], ShiftOr[k] + i, k==1, k==0 );
Vec_IntPush( vVars, toLitCond(ShiftOr[k] + i, 1) );
}
Cid = sat_solver2_addclause( pSat, Vec_IntArray(vVars), Vec_IntArray(vVars) + Vec_IntSize(vVars) );
clause_set_partA( pSat, Cid, k==0 );
// return to normal
Cnf_DataLift( pCnf, -ShiftCnf[k]-pCnf->nVars );
}
// add clauses to constrain p[0] and p[1]
for ( k = 0; k < nOuts; k++ )
Aig_ManInterAddXor( pSat, ShiftP[0] + k, ShiftP[1] + k, ShiftAssume + k, 0, 0 );
// start the interpolant
pBase = Aig_ManStart( 1000 );
pBase->pName = Aig_UtilStrsav( "repar" );
for ( k = 0; k < 2*nOuts; k++ )
Aig_IthVar(pBase, i);
// start global variables (pGlobal and p[0])
Vec_IntClear( vVars );
for ( k = 0; k < 2*nOuts; k++ )
Vec_IntPush( vVars, k );
// perform iterative solving
// vars: pGlobal + (p0 + A1 + A2 + or0) + (p1 + B1 + B2 + or1) + pAssume;
for ( k = 0; k < nOuts; k++ )
{
// swap k-th variables
int Temp = Vec_IntEntry( vVars, k );
Vec_IntWriteEntry( vVars, k, Vec_IntEntry(vVars, nOuts+k) );
Vec_IntWriteEntry( vVars, nOuts+k, Temp );
// solve incrementally
Lit = toLitCond( ShiftAssume + k, 1 ); // XOR output is 0 ==> p1 == p2
status = sat_solver2_solve( pSat, &Lit, &Lit + 1, 0, 0, 0, 0 );
assert( status == l_False );
Sat_Solver2PrintStats( stdout, pSat );
// derive interpolant
pInter = Sat_ProofInterpolant( pSat, vVars );
Aig_ManPrintStats( pInter );
// make sure interpolant does not depend on useless vars
Aig_ManForEachPi( pInter, pObj, i )
assert( i <= k || Aig_ObjRefs(pObj) == 0 );
// simplify
pInter = Dar_ManRwsat( pAigTemp = pInter, 1, 0 );
Aig_ManStop( pAigTemp );
// add interpolant to the solver
pCnfInter = Cnf_Derive( pInter, 1 );
Cnf_DataLift( pCnfInter, pSat->size );
sat_solver2_setnvars( pSat, pSat->size + 2*pCnfInter->nVars );
for ( i = 0; i < pCnfInter->nVars; i++ )
var_set_partA( pSat, pSat->size-2*pCnfInter->nVars + i, 1 );
for ( c = 0; c < 2; c++ )
{
if ( c == 1 )
Cnf_DataLift( pCnfInter, pCnfInter->nVars );
// add to A
for ( i = 0; i < pCnfInter->nClauses; i++ )
{
Cid = sat_solver2_addclause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] );
clause_set_partA( pSat, Cid, c==0 );
}
// connect to the inputs
Aig_ManForEachPi( pInter, pObj, i )
if ( i <= k )
Aig_ManInterAddBuffer( pSat, i, pCnf->pVarNums[pObj->Id], 0, c==0 );
// connect to the outputs
pObj = Aig_ManPo(pInter, 0);
Aig_ManInterAddBuffer( pSat, ShiftP[c] + k, pCnf->pVarNums[pObj->Id], 0, c==0 );
if ( c == 1 )
Cnf_DataLift( pCnfInter, -pCnfInter->nVars );
}
Cnf_DataFree( pCnfInter );
// accumulate
Aig_ManAppend( pBase, pInter );
Aig_ManStop( pInter );
// update global variables
Temp = Vec_IntEntry( vVars, k );
Vec_IntWriteEntry( vVars, k, Vec_IntEntry(vVars, nOuts+k) );
Vec_IntWriteEntry( vVars, nOuts+k, Temp );
}
Vec_IntFree( vVars );
Cnf_DataFree( pCnf );
sat_solver2_delete( pSat );
ABC_PRT( "Reparameterization time", clock() - clk );
return pBase;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
src/aig/aig/module.make
......@@ -17,6 +17,7 @@ SRC += src/aig/aig/aigCheck.c \
src/aig/aig/aigPart.c \
src/aig/aig/aigPartReg.c \
src/aig/aig/aigPartSat.c \
src/aig/aig/aigRepar.c \
src/aig/aig/aigRepr.c \
src/aig/aig/aigRet.c \
src/aig/aig/aigRetF.c \
......
src/base/abci/abc.c
......@@ -8891,12 +8891,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
*/
{
extern void Abs_VfaManTest( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fVerbose );
// extern void Abs_VfaManTest( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fVerbose );
extern void Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose );
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
if ( pNtk )
{
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
Abs_VfaManTest( pAig, 32, 1000000, 1 );
Aig_ManInterRepar( pAig, 1 );
Aig_ManStop( pAig );
}
}
......
src/sat/bsat/satProof.c
......@@ -133,10 +133,10 @@ static inline satset* Proof_ResolveRead (Rec_Int_t* p, cla h ) { return (sats
// iterating through fanins of a proof node
#define Proof_NodeForeachFanin( p, pNode, pFanin, i ) \
for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = (pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(p, pNode->pEnts[i] >> 2)), 1); i++ )
#define Proof_NodeForeachLeaf( pLeaves, pNode, pLeaf, i ) \
for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pLeaves, pNode->pEnts[i] >> 2) : NULL), 1); i++ )
#define Proof_NodeForeachFaninLeaf( p, pLeaves, pNode, pFanin, i ) \
for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pLeaves, pNode->pEnts[i] >> 2) : Proof_NodeRead(p, pNode->pEnts[i] >> 2)); i++ )
#define Proof_NodeForeachLeaf( pClauses, pNode, pLeaf, i ) \
for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pClauses, pNode->pEnts[i] >> 2) : NULL), 1); i++ )
#define Proof_NodeForeachFaninLeaf( p, pClauses, pNode, pFanin, i ) \
for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pClauses, pNode->pEnts[i] >> 2) : Proof_NodeRead(p, pNode->pEnts[i] >> 2)); i++ )
////////////////////////////////////////////////////////////////////////
......@@ -420,135 +420,6 @@ void Sat_ProofReduce( sat_solver2 * s )
#if 0
/**Function*************************************************************
Synopsis [Performs one resultion step.]
Description [Returns ID of the resolvent if success, and -1 if failure.]
SideEffects []
SeeAlso []
***********************************************************************/
satset * Sat_ProofCheckResolveOne( Vec_Int_t * p, satset * c1, satset * c2, Vec_Int_t * vTemp )
{
satset * c;
int i, k, hNode, Var = -1, Count = 0;
// find resolution variable
for ( i = 0; i < (int)c1->nEnts; i++ )
for ( k = 0; k < (int)c2->nEnts; k++ )
if ( (c1->pEnts[i] ^ c2->pEnts[k]) == 1 )
{
Var = (c1->pEnts[i] >> 1);
Count++;
}
if ( Count == 0 )
{
printf( "Cannot find resolution variable\n" );
return NULL;
}
if ( Count > 1 )
{
printf( "Found more than 1 resolution variables\n" );
return NULL;
}
// perform resolution
Vec_IntClear( vTemp );
for ( i = 0; i < (int)c1->nEnts; i++ )
if ( (c1->pEnts[i] >> 1) != Var )
Vec_IntPush( vTemp, c1->pEnts[i] );
for ( i = 0; i < (int)c2->nEnts; i++ )
if ( (c2->pEnts[i] >> 1) != Var )
Vec_IntPushUnique( vTemp, c2->pEnts[i] );
// move to the new one
hNode = Vec_IntSize( p );
Vec_IntPush( p, 0 ); // placeholder
Vec_IntPush( p, 0 );
Vec_IntForEachEntry( vTemp, Var, i )
Vec_IntPush( p, Var );
c = Proof_NodeRead( p, hNode );
c->nEnts = Vec_IntSize(vTemp);
return c;
}
/**Function*************************************************************
Synopsis [Checks the proof for consitency.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
satset * Sat_ProofCheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vResolves, int iAnt )
{
satset * pAnt;
if ( iAnt & 1 )
return Proof_NodeRead( vClauses, iAnt >> 2 );
assert( iAnt > 0 );
pAnt = Proof_NodeRead( vProof, iAnt >> 2 );
assert( pAnt->Id > 0 );
return Proof_NodeRead( vResolves, pAnt->Id );
}
/**Function*************************************************************
Synopsis [Checks the proof for consitency.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sat_ProofCheck( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot )
{
Vec_Int_t * vUsed, * vResolves, * vTemp;
satset * pSet, * pSet0, * pSet1;
int i, k, Counter = 0, clk = clock();
// collect visited clauses
vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
Proof_CleanCollected( vProof, vUsed );
// perform resolution steps
vTemp = Vec_IntAlloc( 1000 );
vResolves = Vec_IntAlloc( 1000 );
Vec_IntPush( vResolves, -1 );
Proof_ForeachNodeVec( vUsed, vProof, pSet, i )
{
pSet0 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] );
for ( k = 1; k < (int)pSet->nEnts; k++ )
{
pSet1 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] );
pSet0 = Sat_ProofCheckResolveOne( vResolves, pSet0, pSet1, vTemp );
}
pSet->Id = Proof_NodeHandle( vResolves, pSet0 );
//printf( "Clause for proof %d: ", Vec_IntEntry(vUsed, i) );
//satset_print( pSet0 );
Counter++;
}
Vec_IntFree( vTemp );
// clean the proof
Proof_CleanCollected( vProof, vUsed );
// compare the final clause
printf( "Used %6.2f Mb for resolvents.\n", 4.0 * Vec_IntSize(vResolves) / (1<<20) );
if ( pSet0->nEnts > 0 )
printf( "Cound not derive the empty clause. " );
else
printf( "Proof verification successful. " );
Abc_PrintTime( 1, "Time", clock() - clk );
// cleanup
Vec_IntFree( vResolves );
Vec_IntFree( vUsed );
}
#endif
/**Function*************************************************************
Synopsis [Performs one resultion step.]
......@@ -669,7 +540,7 @@ void Sat_ProofCheck( sat_solver2 * s )
// compare the final clause
printf( "Used %6.2f Mb for resolvents.\n", 4.0 * Rec_IntSize(vResolves) / (1<<20) );
if ( pSet0->nEnts > 0 )
printf( "Cound not derive the empty clause. " );
printf( "Derived clause with %d lits instead of the empty clause. ", pSet0->nEnts );
else
printf( "Proof verification successful. " );
Abc_PrintTime( 1, "Time", clock() - clk );
......@@ -689,7 +560,7 @@ void Sat_ProofCheck( sat_solver2 * s )
SeeAlso []
***********************************************************************/
Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vUsed )
Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vUsed, int fUseIds )
{
Vec_Int_t * vCore;
satset * pNode, * pFanin;
......@@ -709,11 +580,59 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_
Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
{
pNode->mark = 0;
Vec_IntWriteEntry( vCore, i, pNode->Id - 1 );
if ( fUseIds )
Vec_IntWriteEntry( vCore, i, pNode->Id - 1 );
}
return vCore;
}
/**Function*************************************************************
Synopsis [Verifies that variables are labeled correctly.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sat_ProofInterpolantCheckVars( sat_solver2 * s, Vec_Int_t * vGloVars )
{
satset* c;
Vec_Int_t * vVarMap;
int i, k, Entry, * pMask;
int Counts[5] = {0};
// map variables into their type (A, B, or AB)
vVarMap = Vec_IntStart( s->size );
sat_solver_foreach_clause( s, c, i )
for ( k = 0; k < (int)c->nEnts; k++ )
*Vec_IntEntryP(vVarMap, lit_var(c->pEnts[k])) |= 2 - c->partA;
// analyze variables
Vec_IntForEachEntry( vGloVars, Entry, i )
{
pMask = Vec_IntEntryP(vVarMap, Entry);
assert( *pMask >= 0 && *pMask <= 3 );
Counts[(*pMask & 3)]++;
*pMask = 0;
}
// count the number of global variables not listed
Vec_IntForEachEntry( vVarMap, Entry, i )
if ( Entry == 3 )
Counts[4]++;
Vec_IntFree( vVarMap );
// report
if ( Counts[0] )
printf( "Warning: %6d variables listed as global do not appear in clauses (this is normal)\n", Counts[0] );
if ( Counts[1] )
printf( "Warning: %6d variables listed as global appear only in A-clauses (this is a BUG)\n", Counts[1] );
if ( Counts[2] )
printf( "Warning: %6d variables listed as global appear only in B-clauses (this is a BUG)\n", Counts[2] );
if ( Counts[3] )
printf( "Warning: %6d (out of %d) variables listed as global appear in both A- and B-clauses (this is normal)\n", Counts[3], Vec_IntSize(vGloVars) );
if ( Counts[4] )
printf( "Warning: %6d variables not listed as global appear in both A- and B-clauses (this is a BUG)\n", Counts[4] );
}
/**Function*************************************************************
......@@ -737,15 +656,17 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
satset * pNode, * pFanin;
Aig_Man_t * pAig;
Aig_Obj_t * pObj;
int i, k, iVar, Entry;
int i, k, iVar, Lit, Entry;
Sat_ProofInterpolantCheckVars( s, vGlobVars );
// collect visited nodes
vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
// collect core clauses (cleans vUsed and vCore)
vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed );
vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 0 );
// map variables into their global numbers
vVarMap = Vec_IntStartFull( Vec_IntFindMax(vGlobVars) + 1 );
vVarMap = Vec_IntStartFull( s->size );
Vec_IntForEachEntry( vGlobVars, Entry, i )
Vec_IntWriteEntry( vVarMap, Entry, i );
......@@ -762,9 +683,9 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
if ( pNode->partA )
{
pObj = Aig_ManConst0( pAig );
satset_foreach_var( pNode, iVar, k, 0 )
if ( iVar < Vec_IntSize(vVarMap) && Vec_IntEntry(vVarMap, iVar) >= 0 )
pObj = Aig_Or( pAig, pObj, Aig_IthVar(pAig, iVar) );
satset_foreach_lit( pNode, Lit, k, 0 )
if ( (iVar = Vec_IntEntry(vVarMap, lit_var(Lit))) >= 0 )
pObj = Aig_Or( pAig, pObj, Aig_NotCond(Aig_IthVar(pAig, iVar), lit_sign(Lit)) );
}
else
pObj = Aig_ManConst1( pAig );
......@@ -777,9 +698,11 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
// copy the numbers out and derive interpol for resolvents
Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
{
// satset_print( pNode );
assert( pNode->nEnts > 1 );
Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k )
{
assert( pFanin->Id < 2*Aig_ManObjNumMax(pAig) );
if ( k == 0 )
pObj = Aig_ObjFromLit( pAig, pFanin->Id );
else if ( pNode->pEnts[k] & 2 ) // variable of A
......@@ -828,7 +751,7 @@ void * Sat_ProofCore( sat_solver2 * s )
// collect visited clauses
vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
// collect core clauses
vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed );
vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 1 );
Vec_IntFree( vUsed );
return vCore;
}
......
src/sat/bsat/satSolver2.c
......@@ -144,11 +144,9 @@ static inline void solver2_clear_marks(sat_solver2* s) {
static inline satset* clause_read (sat_solver2* s, cla h) { return (h & 1) ? satset_read(&s->learnts, h>>1) : satset_read(&s->clauses, h>>1); }
static inline cla clause_handle (sat_solver2* s, satset* c) { return c->learnt ? (satset_handle(&s->learnts, c)<<1)|1: satset_handle(&s->clauses, c)<<1; }
static inline int clause_check (sat_solver2* s, satset* c) { return c->learnt ? satset_check(&s->learnts, c) : satset_check(&s->clauses, c); }
static inline int clause_proofid(sat_solver2* s, satset* c, int partA) { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (satset_handle(&s->clauses, c)<<2) | 1; }
static inline int clause_proofid(sat_solver2* s, satset* c, int partA) { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (satset_handle(&s->clauses, c)<<2) | (partA<<1) | 1; }
static inline int clause_is_used(sat_solver2* s, cla h) { return (h & 1) ? (h >> 1) < s->hLearntPivot : (h >> 1) < s->hClausePivot; }
//static inline int var_reason (sat_solver2* s, int v) { return (s->reasons[v]&1) ? 0 : s->reasons[v] >> 1; }
//static inline int lit_reason (sat_solver2* s, int l) { return (s->reasons[lit_var(l)&1]) ? 0 : s->reasons[lit_var(l)] >> 1; }
//static inline satset* var_unit_clause(sat_solver2* s, int v) { return (s->reasons[v]&1) ? clause_read(s, s->reasons[v] >> 1) : NULL; }
......@@ -163,9 +161,6 @@ int clause_is_partA (sat_solver2* s, int h) { return clause
void clause_set_partA(sat_solver2* s, int h, int partA) { clause_read(s, h)->partA = partA; }
int clause_id(sat_solver2* s, int h) { return clause_read(s, h)->Id; }
#define sat_solver_foreach_clause( s, c, h ) satset_foreach_entry( &s->clauses, c, h, 1 )
#define sat_solver_foreach_learnt( s, c, h ) satset_foreach_entry( &s->learnts, c, h, 1 )
//=================================================================================================
// Simple helpers:
......@@ -1452,6 +1447,7 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end)
if ( !solver2_enqueue(s,begin[0],0) )
assert( 0 );
}
//satset_print( clause_read(s, Cid) );
return Cid;
}
......
src/sat/bsat/satSolver2.h
......@@ -184,6 +184,11 @@ static inline void satset_print (satset * c) {
for ( i = 0; (i < veci_size(pVec)) && ((c) = satset_read(p, veci_begin(pVec)[i])); i++ )
#define satset_foreach_var( p, var, i, start ) \
for ( i = start; (i < (int)(p)->nEnts) && ((var) = lit_var((p)->pEnts[i])); i++ )
#define satset_foreach_lit( p, lit, i, start ) \
for ( i = start; (i < (int)(p)->nEnts) && ((lit) = (p)->pEnts[i]); i++ )
#define sat_solver_foreach_clause( s, c, h ) satset_foreach_entry( &s->clauses, c, h, 1 )
#define sat_solver_foreach_learnt( s, c, h ) satset_foreach_entry( &s->learnts, c, h, 1 )
//=================================================================================================
// Public APIs:
......
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