diff options
Diffstat (limited to 'src/aig/fra/fraIndVer.c')
| -rw-r--r-- | src/aig/fra/fraIndVer.c | 166 |
1 files changed, 0 insertions, 166 deletions
diff --git a/src/aig/fra/fraIndVer.c b/src/aig/fra/fraIndVer.c deleted file mode 100644 index 32069cfb..00000000 --- a/src/aig/fra/fraIndVer.c +++ /dev/null @@ -1,166 +0,0 @@ -/**CFile**************************************************************** - - FileName [fraIndVer.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [New FRAIG package.] - - Synopsis [Verification of the inductive invariant.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 30, 2007.] - - Revision [$Id: fraIndVer.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "fra.h" -#include "cnf.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Verifies the inductive invariant.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Fra_InvariantVerify( Aig_Man_t * pAig, int nFrames, Vec_Int_t * vClauses, Vec_Int_t * vLits ) -{ - Cnf_Dat_t * pCnf; - sat_solver * pSat; - int * pStart; - int RetValue, Beg, End, i, k; - int CounterBase = 0, CounterInd = 0; - int clk = clock(); - - if ( nFrames != 1 ) - { - printf( "Invariant verification: Can only verify for K = 1\n" ); - return 1; - } - - // derive CNF - pCnf = Cnf_DeriveSimple( pAig, Aig_ManPoNum(pAig) ); -/* - // add the property - { - Aig_Obj_t * pObj; - int Lits[1]; - - pObj = Aig_ManPo( pAig, 0 ); - Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 1 ); - - Vec_IntPush( vLits, Lits[0] ); - Vec_IntPush( vClauses, Vec_IntSize(vLits) ); - printf( "Added the target property to the set of clauses to be inductively checked.\n" ); - } -*/ - // derive initialized frames for the base case - pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames, 1 ); - // check clauses in the base case - Beg = 0; - pStart = Vec_IntArray( vLits ); - Vec_IntForEachEntry( vClauses, End, i ) - { - // complement the literals - for ( k = Beg; k < End; k++ ) - pStart[k] = lit_neg(pStart[k]); - RetValue = sat_solver_solve( pSat, pStart + Beg, pStart + End, 0, 0, 0, 0 ); - for ( k = Beg; k < End; k++ ) - pStart[k] = lit_neg(pStart[k]); - Beg = End; - if ( RetValue == l_False ) - continue; -// printf( "Clause %d failed the base case.\n", i ); - CounterBase++; - } - sat_solver_delete( pSat ); - - // derive initialized frames for the base case - pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames + 1, 0 ); - assert( pSat->size == 2 * pCnf->nVars ); - // add clauses to the first frame - Beg = 0; - pStart = Vec_IntArray( vLits ); - Vec_IntForEachEntry( vClauses, End, i ) - { - RetValue = sat_solver_addclause( pSat, pStart + Beg, pStart + End ); - Beg = End; - if ( RetValue == 0 ) - { - Cnf_DataFree( pCnf ); - sat_solver_delete( pSat ); - printf( "Invariant verification: SAT solver is unsat after adding a clause.\n" ); - return 0; - } - } - // simplify the solver - if ( pSat->qtail != pSat->qhead ) - { - RetValue = sat_solver_simplify(pSat); - assert( RetValue != 0 ); - assert( pSat->qtail == pSat->qhead ); - } - - // check clauses in the base case - Beg = 0; - pStart = Vec_IntArray( vLits ); - Vec_IntForEachEntry( vClauses, End, i ) - { - // complement the literals - for ( k = Beg; k < End; k++ ) - { - pStart[k] += 2 * pCnf->nVars; - pStart[k] = lit_neg(pStart[k]); - } - RetValue = sat_solver_solve( pSat, pStart + Beg, pStart + End, 0, 0, 0, 0 ); - for ( k = Beg; k < End; k++ ) - { - pStart[k] = lit_neg(pStart[k]); - pStart[k] -= 2 * pCnf->nVars; - } - Beg = End; - if ( RetValue == l_False ) - continue; -// printf( "Clause %d failed the inductive case.\n", i ); - CounterInd++; - } - sat_solver_delete( pSat ); - Cnf_DataFree( pCnf ); - if ( CounterBase ) - printf( "Invariant verification: %d clauses (out of %d) FAILED the base case.\n", CounterBase, Vec_IntSize(vClauses) ); - if ( CounterInd ) - printf( "Invariant verification: %d clauses (out of %d) FAILED the inductive case.\n", CounterInd, Vec_IntSize(vClauses) ); - if ( CounterBase || CounterInd ) - return 0; - printf( "Invariant verification: %d clauses verified correctly. ", Vec_IntSize(vClauses) ); - ABC_PRT( "Time", clock() - clk ); - return 1; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - |