summaryrefslogtreecommitdiffstats
path: root/src/proof/int/intM114p.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/int/intM114p.c')
-rw-r--r--src/proof/int/intM114p.c442
1 files changed, 442 insertions, 0 deletions
diff --git a/src/proof/int/intM114p.c b/src/proof/int/intM114p.c
new file mode 100644
index 00000000..7c011426
--- /dev/null
+++ b/src/proof/int/intM114p.c
@@ -0,0 +1,442 @@
+/**CFile****************************************************************
+
+ FileName [intM114p.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Interpolation engine.]
+
+ Synopsis [Intepolation using interfaced to MiniSat-1.14p.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 24, 2008.]
+
+ Revision [$Id: intM114p.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "intInt.h"
+#include "src/sat/psat/m114p.h"
+
+#ifdef ABC_USE_LIBRARIES
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Returns the SAT solver for one interpolation run.]
+
+ Description [pInter is the previous interpolant. pAig is one time frame.
+ pFrames is the unrolled time frames.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+M114p_Solver_t Inter_ManDeriveSatSolverM114p(
+ Aig_Man_t * pInter, Cnf_Dat_t * pCnfInter,
+ Aig_Man_t * pAig, Cnf_Dat_t * pCnfAig,
+ Aig_Man_t * pFrames, Cnf_Dat_t * pCnfFrames,
+ Vec_Int_t ** pvMapRoots, Vec_Int_t ** pvMapVars )
+{
+ M114p_Solver_t pSat;
+ Aig_Obj_t * pObj, * pObj2;
+ int i, Lits[2];
+
+ // sanity checks
+ assert( Aig_ManRegNum(pInter) == 0 );
+ assert( Aig_ManRegNum(pAig) > 0 );
+ assert( Aig_ManRegNum(pFrames) == 0 );
+ assert( Aig_ManPoNum(pInter) == 1 );
+ assert( Aig_ManPoNum(pFrames) == 1 );
+ assert( Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) );
+// assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
+
+ // prepare CNFs
+ Cnf_DataLift( pCnfAig, pCnfFrames->nVars );
+ Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars );
+
+ *pvMapRoots = Vec_IntAlloc( 10000 );
+ *pvMapVars = Vec_IntAlloc( 0 );
+ Vec_IntFill( *pvMapVars, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars, -1 );
+ for ( i = 0; i < pCnfFrames->nVars; i++ )
+ Vec_IntWriteEntry( *pvMapVars, i, -2 );
+
+ // start the solver
+ pSat = M114p_SolverNew( 1 );
+ M114p_SolverSetVarNum( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars );
+
+ // add clauses of A
+ // interpolant
+ for ( i = 0; i < pCnfInter->nClauses; i++ )
+ {
+ Vec_IntPush( *pvMapRoots, 0 );
+ if ( !M114p_SolverAddClause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ) )
+ assert( 0 );
+ }
+ // connector clauses
+ Aig_ManForEachPi( pInter, pObj, i )
+ {
+ pObj2 = Saig_ManLo( pAig, i );
+ Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
+ Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
+ Vec_IntPush( *pvMapRoots, 0 );
+ if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
+ assert( 0 );
+ Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 );
+ Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
+ Vec_IntPush( *pvMapRoots, 0 );
+ if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
+ assert( 0 );
+ }
+ // one timeframe
+ for ( i = 0; i < pCnfAig->nClauses; i++ )
+ {
+ Vec_IntPush( *pvMapRoots, 0 );
+ if ( !M114p_SolverAddClause( pSat, pCnfAig->pClauses[i], pCnfAig->pClauses[i+1] ) )
+ assert( 0 );
+ }
+ // connector clauses
+ Aig_ManForEachPi( pFrames, pObj, i )
+ {
+ if ( i == Aig_ManRegNum(pAig) )
+ break;
+// Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
+ Vec_IntWriteEntry( *pvMapVars, pCnfFrames->pVarNums[pObj->Id], i );
+
+ pObj2 = Saig_ManLi( pAig, i );
+ Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 );
+ Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
+ Vec_IntPush( *pvMapRoots, 0 );
+ if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
+ assert( 0 );
+ Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 );
+ Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
+ Vec_IntPush( *pvMapRoots, 0 );
+ if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
+ assert( 0 );
+ }
+ // add clauses of B
+ for ( i = 0; i < pCnfFrames->nClauses; i++ )
+ {
+ Vec_IntPush( *pvMapRoots, 1 );
+ if ( !M114p_SolverAddClause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) )
+ {
+// assert( 0 );
+ break;
+ }
+ }
+ // return clauses to the original state
+ Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
+ Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );
+ return pSat;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs one resolution step.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Inter_ManResolveM114p( Vec_Int_t * vResolvent, int * pLits, int nLits, int iVar )
+{
+ int i, k, iLit = -1, fFound = 0;
+ // find the variable in the clause
+ for ( i = 0; i < vResolvent->nSize; i++ )
+ if ( lit_var(vResolvent->pArray[i]) == iVar )
+ {
+ iLit = vResolvent->pArray[i];
+ vResolvent->pArray[i] = vResolvent->pArray[--vResolvent->nSize];
+ break;
+ }
+ assert( iLit != -1 );
+ // add other variables
+ for ( i = 0; i < nLits; i++ )
+ {
+ if ( lit_var(pLits[i]) == iVar )
+ {
+ assert( iLit == lit_neg(pLits[i]) );
+ fFound = 1;
+ continue;
+ }
+ // check if this literal appears
+ for ( k = 0; k < vResolvent->nSize; k++ )
+ if ( vResolvent->pArray[k] == pLits[i] )
+ break;
+ if ( k < vResolvent->nSize )
+ continue;
+ // add this literal
+ Vec_IntPush( vResolvent, pLits[i] );
+ }
+ assert( fFound );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes interpolant using MiniSat-1.14p.]
+
+ Description [Assumes that the solver returned UNSAT and proof
+ logging was enabled. Array vMapRoots maps number of each root clause
+ into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT
+ solver variable into -1 (var of A), -2 (var of B), and <num> (var of C),
+ where <num> is the var's 0-based number in the ordering of C variables.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Inter_ManInterpolateM114pPudlak( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
+{
+ Aig_Man_t * p;
+ Aig_Obj_t * pInter, * pInter2, * pVar;
+ Vec_Ptr_t * vInters;
+ Vec_Int_t * vLiterals, * vClauses, * vResolvent;
+ int * pLitsNext, nLitsNext, nOffset, iLit;
+ int * pLits, * pClauses, * pVars;
+ int nLits, nVars, i, k, v, iVar;
+ assert( M114p_SolverProofIsReady(s) );
+ vInters = Vec_PtrAlloc( 1000 );
+
+ vLiterals = Vec_IntAlloc( 10000 );
+ vClauses = Vec_IntAlloc( 1000 );
+ vResolvent = Vec_IntAlloc( 100 );
+
+ // create elementary variables
+ p = Aig_ManStart( 10000 );
+ Vec_IntForEachEntry( vMapVars, iVar, i )
+ if ( iVar >= 0 )
+ Aig_IthVar(p, iVar);
+ // process root clauses
+ M114p_SolverForEachRoot( s, &pLits, nLits, i )
+ {
+ if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B
+ pInter = Aig_ManConst1(p);
+ else // clause of A
+ pInter = Aig_ManConst0(p);
+ Vec_PtrPush( vInters, pInter );
+
+ // save the root clause
+ Vec_IntPush( vClauses, Vec_IntSize(vLiterals) );
+ Vec_IntPush( vLiterals, nLits );
+ for ( v = 0; v < nLits; v++ )
+ Vec_IntPush( vLiterals, pLits[v] );
+ }
+ assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) );
+
+ // process learned clauses
+ M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
+ {
+ pInter = Vec_PtrEntry( vInters, pClauses[0] );
+
+ // initialize the resolvent
+ nOffset = Vec_IntEntry( vClauses, pClauses[0] );
+ nLitsNext = Vec_IntEntry( vLiterals, nOffset );
+ pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1;
+ Vec_IntClear( vResolvent );
+ for ( v = 0; v < nLitsNext; v++ )
+ Vec_IntPush( vResolvent, pLitsNext[v] );
+
+ for ( k = 0; k < nVars; k++ )
+ {
+ iVar = Vec_IntEntry( vMapVars, pVars[k] );
+ pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] );
+
+ // resolve it with the next clause
+ nOffset = Vec_IntEntry( vClauses, pClauses[k+1] );
+ nLitsNext = Vec_IntEntry( vLiterals, nOffset );
+ pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1;
+ Inter_ManResolveM114p( vResolvent, pLitsNext, nLitsNext, pVars[k] );
+
+ if ( iVar == -1 ) // var of A
+ pInter = Aig_Or( p, pInter, pInter2 );
+ else if ( iVar == -2 ) // var of B
+ pInter = Aig_And( p, pInter, pInter2 );
+ else // var of C
+ {
+ // check polarity of the pivot variable in the clause
+ for ( v = 0; v < nLitsNext; v++ )
+ if ( lit_var(pLitsNext[v]) == pVars[k] )
+ break;
+ assert( v < nLitsNext );
+ pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLitsNext[v]) );
+ pInter = Aig_Mux( p, pVar, pInter, pInter2 );
+ }
+ }
+ Vec_PtrPush( vInters, pInter );
+
+ // store the resulting clause
+ Vec_IntPush( vClauses, Vec_IntSize(vLiterals) );
+ Vec_IntPush( vLiterals, Vec_IntSize(vResolvent) );
+ Vec_IntForEachEntry( vResolvent, iLit, v )
+ Vec_IntPush( vLiterals, iLit );
+ }
+ assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) );
+ assert( Vec_IntSize(vResolvent) == 0 ); // the empty clause
+ Vec_PtrFree( vInters );
+ Vec_IntFree( vLiterals );
+ Vec_IntFree( vClauses );
+ Vec_IntFree( vResolvent );
+ Aig_ObjCreatePo( p, pInter );
+ Aig_ManCleanup( p );
+ return p;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Computes interpolant using MiniSat-1.14p.]
+
+ Description [Assumes that the solver returned UNSAT and proof
+ logging was enabled. Array vMapRoots maps number of each root clause
+ into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT
+ solver variable into -1 (var of A), -2 (var of B), and <num> (var of C),
+ where <num> is the var's 0-based number in the ordering of C variables.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Inter_ManpInterpolateM114( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
+{
+ Aig_Man_t * p;
+ Aig_Obj_t * pInter, * pInter2, * pVar;
+ Vec_Ptr_t * vInters;
+ int * pLits, * pClauses, * pVars;
+ int nLits, nVars, i, k, iVar;
+ int nClauses;
+
+ nClauses = M114p_SolverProofClauseNum(s);
+
+ assert( M114p_SolverProofIsReady(s) );
+
+ vInters = Vec_PtrAlloc( 1000 );
+ // process root clauses
+ p = Aig_ManStart( 10000 );
+ M114p_SolverForEachRoot( s, &pLits, nLits, i )
+ {
+ if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B
+ pInter = Aig_ManConst1(p);
+ else // clause of A
+ {
+ pInter = Aig_ManConst0(p);
+ for ( k = 0; k < nLits; k++ )
+ {
+ iVar = Vec_IntEntry( vMapVars, lit_var(pLits[k]) );
+ if ( iVar < 0 ) // var of A or B
+ continue;
+ // this is a variable of C
+ pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLits[k]) );
+ pInter = Aig_Or( p, pInter, pVar );
+ }
+ }
+ Vec_PtrPush( vInters, pInter );
+ }
+// assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) );
+
+ // process learned clauses
+ M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
+ {
+ pInter = Vec_PtrEntry( vInters, pClauses[0] );
+ for ( k = 0; k < nVars; k++ )
+ {
+ iVar = Vec_IntEntry( vMapVars, pVars[k] );
+ pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] );
+ if ( iVar == -1 ) // var of A
+ pInter = Aig_Or( p, pInter, pInter2 );
+ else // var of B or C
+ pInter = Aig_And( p, pInter, pInter2 );
+ }
+ Vec_PtrPush( vInters, pInter );
+ }
+
+ assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) );
+ Vec_PtrFree( vInters );
+ Aig_ObjCreatePo( p, pInter );
+ Aig_ManCleanup( p );
+ assert( Aig_ManCheck(p) );
+ return p;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs one SAT run with interpolation.]
+
+ Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Inter_ManPerformOneStepM114p( Inter_Man_t * p, int fUsePudlak, int fUseOther )
+{
+ M114p_Solver_t pSat;
+ Vec_Int_t * vMapRoots, * vMapVars;
+ int clk, status, RetValue;
+ assert( p->pInterNew == NULL );
+ // derive the SAT solver
+ pSat = Inter_ManDeriveSatSolverM114p( p->pInter, p->pCnfInter,
+ p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames,
+ &vMapRoots, &vMapVars );
+ // solve the problem
+clk = clock();
+ status = M114p_SolverSolve( pSat, NULL, NULL, 0 );
+ p->nConfCur = M114p_SolverGetConflictNum( pSat );
+p->timeSat += clock() - clk;
+ if ( status == 0 )
+ {
+ RetValue = 1;
+// Inter_ManpInterpolateM114Report( pSat, vMapRoots, vMapVars );
+
+clk = clock();
+ if ( fUsePudlak )
+ p->pInterNew = Inter_ManInterpolateM114pPudlak( pSat, vMapRoots, vMapVars );
+ else
+ p->pInterNew = Inter_ManpInterpolateM114( pSat, vMapRoots, vMapVars );
+p->timeInt += clock() - clk;
+ }
+ else if ( status == 1 )
+ {
+ RetValue = 0;
+ }
+ else
+ {
+ RetValue = -1;
+ }
+ M114p_SolverDelete( pSat );
+ Vec_IntFree( vMapRoots );
+ Vec_IntFree( vMapVars );
+ return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_IMPL_END
+
+#endif
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 19:02:47 +0000