From 1067e6dec9007daf226b0d23de24cbad54ffa904 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 1 Aug 2013 19:02:08 -0700 Subject: SAT solver with dynamic CNF loading. --- src/sat/bmc/bmcLoad.c | 210 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 210 insertions(+) create mode 100644 src/sat/bmc/bmcLoad.c (limited to 'src') diff --git a/src/sat/bmc/bmcLoad.c b/src/sat/bmc/bmcLoad.c new file mode 100644 index 00000000..b3d56005 --- /dev/null +++ b/src/sat/bmc/bmcLoad.c @@ -0,0 +1,210 @@ +/**CFile**************************************************************** + + FileName [bmcLoad.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT-based bounded model checking.] + + Synopsis [Experiments with CNF loading.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: bmcLoad.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "bmc.h" +#include "sat/bsat/satStore.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Bmc_Lad_t_ Bmc_Lad_t; +struct Bmc_Lad_t_ +{ + Bmc_LadPar_t * pPars; // parameters + Gia_Man_t * pGia; // unrolled AIG + sat_solver * pSat; // SAT solvers + Vec_Int_t * vSat2Id; // maps SAT var into its node +// Vec_Int_t * vCut; // cut in terms of GIA IDs +// Vec_Int_t * vCnf; // CNF for the cut + int nCallBacks1; + int nCallBacks2; +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + + +/**Function************************************************************* + + Synopsis [Load CNF for the cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bmc_LadGetSatVar( Bmc_Lad_t * p, int Id ) +{ + Gia_Obj_t * pObj = Gia_ManObj( p->pGia, Id ); + if ( pObj->Value == 0 ) + { + pObj->Value = Vec_IntSize( p->vSat2Id ); + Vec_IntPush( p->vSat2Id, Id ); + sat_solver_setnvars( p->pSat, Vec_IntSize(p->vSat2Id) ); + } + return pObj->Value; +} +int Bmc_LadAddCnf( void * pMan, int iLit ) +{ + Bmc_Lad_t * p = (Bmc_Lad_t *)pMan; + int Lits[3], iVar = Abc_Lit2Var(iLit); + Gia_Obj_t * pObj = Gia_ManObj( p->pGia, Vec_IntEntry(p->vSat2Id, iVar) ); + p->nCallBacks1++; + if ( Gia_ObjIsCi(pObj) || Gia_ObjIsConst0(pObj) ) + return 0; + assert( Gia_ObjIsAnd(pObj) ); + if ( (Abc_LitIsCompl(iLit) ? pObj->fMark1 : pObj->fMark0) ) + return 0; + Lits[0] = Abc_LitNot(iLit); + if ( Abc_LitIsCompl(iLit) ) + { + Lits[1] = Abc_Var2Lit( Bmc_LadGetSatVar(p, Gia_ObjFaninId0p(p->pGia, pObj)), !Gia_ObjFaninC0(pObj) ); + Lits[2] = Abc_Var2Lit( Bmc_LadGetSatVar(p, Gia_ObjFaninId1p(p->pGia, pObj)), !Gia_ObjFaninC1(pObj) ); + sat_solver_clause_new( p->pSat, Lits, Lits + 3, 0 ); + pObj->fMark1 = 1; + } + else + { + Lits[1] = Abc_Var2Lit( Bmc_LadGetSatVar(p, Gia_ObjFaninId0p(p->pGia, pObj)), Gia_ObjFaninC0(pObj) ); + sat_solver_clause_new( p->pSat, Lits, Lits + 2, 0 ); + Lits[1] = Abc_Var2Lit( Bmc_LadGetSatVar(p, Gia_ObjFaninId1p(p->pGia, pObj)), Gia_ObjFaninC1(pObj) ); + sat_solver_clause_new( p->pSat, Lits, Lits + 2, 0 ); + pObj->fMark0 = 1; + } + p->nCallBacks2++; + return 1; +} +int Bmc_LadAddCnf_rec( Bmc_Lad_t * p, int Id ) +{ + int iVar = Bmc_LadGetSatVar( p, Id ); + Gia_Obj_t * pObj = Gia_ManObj( p->pGia, Id ); + if ( Gia_ObjIsAnd(pObj) && !(pObj->fMark0 && pObj->fMark1) ) + { + Bmc_LadAddCnf( p, Abc_Var2Lit(iVar, 0) ); + Bmc_LadAddCnf( p, Abc_Var2Lit(iVar, 1) ); + Bmc_LadAddCnf_rec( p, Gia_ObjFaninId0(pObj, Id) ); + Bmc_LadAddCnf_rec( p, Gia_ObjFaninId1(pObj, Id) ); + } + return iVar; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Bmc_Lad_t * Bmc_LadStart( Gia_Man_t * pGia, Bmc_LadPar_t * pPars ) +{ + Bmc_Lad_t * p; + int Lit; + Gia_ManSetPhase( pGia ); + Gia_ManCleanValue( pGia ); + Gia_ManCreateRefs( pGia ); + p = ABC_CALLOC( Bmc_Lad_t, 1 ); + p->pPars = pPars; + p->pGia = pGia; + p->pSat = sat_solver_new(); + p->vSat2Id = Vec_IntAlloc( 1000 ); + Vec_IntPush( p->vSat2Id, 0 ); + // create constant node + Lit = Abc_Var2Lit( Bmc_LadGetSatVar(p, 0), 1 ); + sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); + // add callback for CNF loading + if ( pPars->fLoadCnf ) + p->pSat->pCnfMan = p; + if ( pPars->fLoadCnf ) + p->pSat->pCnfFunc = Bmc_LadAddCnf; + return p; +} +void Bmc_LadStop( Bmc_Lad_t * p ) +{ + Vec_IntFree( p->vSat2Id ); + sat_solver_delete( p->pSat ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bmc_PerformBmc( Gia_Man_t * pGia, Bmc_LadPar_t * pPars ) +{ + int nConfLimit = 0; + Bmc_Lad_t * p; + Gia_Obj_t * pObj; + int i, status, Lit; + abctime clk = Abc_Clock(); + p = Bmc_LadStart( pGia, pPars ); + Gia_ManForEachPo( pGia, pObj, i ) + { + if ( pPars->fLoadCnf ) + Lit = Abc_Var2Lit( Bmc_LadGetSatVar(p, Gia_ObjFaninId0p(pGia, pObj)), Gia_ObjFaninC0(pObj) ); + else + Lit = Abc_Var2Lit( Bmc_LadAddCnf_rec(p, Gia_ObjFaninId0p(pGia, pObj)), Gia_ObjFaninC0(pObj) ); + if ( pPars->fVerbose ) + { + printf( "Frame%4d : ", i ); + printf( "Vars = %6d ", Vec_IntSize(p->vSat2Id) ); + printf( "Clas = %6d ", sat_solver_nclauses(p->pSat) ); + } + status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + if ( pPars->fVerbose ) + { + printf( "Conf = %6d ", sat_solver_nconflicts(p->pSat) ); + if ( status == l_False ) + printf( "UNSAT " ); + else if ( status == l_True ) + printf( "SAT " ); + else // if ( status == l_Undec ) + printf( "UNDEC " ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + } + } + printf( "Callbacks = %d. Loadings = %d.\n", p->nCallBacks1, p->nCallBacks2 ); + Bmc_LadStop( p ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + -- cgit v1.2.3