Adding interpolant computation sat_solver2.

src/sat/bsat/satSolver2i.c

+/**CFile****************************************************************
+
+  FileName    [satSolver2i.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT solver.]
+
+  Synopsis    [Records the trace of SAT solving in the CNF form.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 2, 2013.]
+
+  Revision    [$Id: satSolver2i.c,v 1.4 2013/09/02 00:00:00 casem Exp $]
+
+***********************************************************************/
+
+#include "satSolver2.h"
+#include "aig/gia/gia.h"
+#include "aig/gia/giaAig.h"
+#include "sat/cnf/cnf.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+struct Int2_Man_t_ 
+{
+    sat_solver2 *   pSat;      // user's SAT solver
+    Vec_Int_t *     vGloVars;  // IDs of global variables
+    Vec_Int_t *     vVar2Glo;  // mapping of SAT variables into their global IDs
+    Gia_Man_t *     pGia;      // AIG manager to store the interpolant
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Managing interpolation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Int2_Man_t * Int2_ManStart( sat_solver2 * pSat, int * pGloVars, int nGloVars )
+{
+    Int2_Man_t * p;
+    int i;
+    p = ABC_CALLOC( Int2_Man_t, 1 );
+    p->pSat     = pSat;
+    p->vGloVars = Vec_IntAllocArrayCopy( pGloVars, nGloVars );
+    p->vVar2Glo = Vec_IntInvert( p->vGloVars, -1 );
+    p->pGia     = Gia_ManStart( 10 * Vec_IntSize(p->vGloVars) );
+    p->pGia->pName = Abc_UtilStrsav( "interpolant" );
+    for ( i = 0; i < nGloVars; i++ )
+        Gia_ManAppendCi( p->pGia );
+    Gia_ManHashStart( p->pGia );
+    return p;
+}
+void Int2_ManStop( Int2_Man_t * p )
+{
+    if ( p == NULL )
+        return;
+    Gia_ManStopP( &p->pGia );
+    Vec_IntFree( p->vGloVars );
+    Vec_IntFree( p->vVar2Glo );
+    ABC_FREE( p );
+}
+void * Int2_ManReadInterpolant( sat_solver2 * pSat )
+{
+    Int2_Man_t * p = pSat->pInt2;
+    Gia_Man_t * pTemp, * pGia = p->pGia; p->pGia = NULL;
+    // return NULL, if the interpolant is not ready (for example, when the solver returned 'sat')
+    if ( pSat->hProofLast == -1 )
+        return NULL;
+    // create AIG with one primary output
+    assert( Gia_ManPoNum(pGia) == 0 );
+    Gia_ManAppendCo( pGia, pSat->hProofLast );  
+    pSat->hProofLast = -1;
+    // cleanup the resulting AIG
+    pGia = Gia_ManCleanup( pTemp = pGia );
+    Gia_ManStop( pTemp );
+    return (void *)pGia;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computing interpolant for a clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Int2_ManChainStart( Int2_Man_t * p, clause * c )
+{
+    if ( c->lrn )
+        return veci_begin(&p->pSat->claProofs)[clause_id(c)];
+    if ( !c->partA )
+        return 1;
+    if ( c->lits[c->size] < 0 )
+    {
+        int i, Var, CiId, Res = 0;
+        for ( i = 0; i < (int)c->size; i++ )
+        {
+            // get ID of the global variable
+            if ( Abc_Lit2Var(c->lits[i]) >= Vec_IntSize(p->vVar2Glo) )
+                continue;
+            Var = Vec_IntEntry( p->vVar2Glo, Abc_Lit2Var(c->lits[i]) );
+            if ( Var < 0 )
+                continue;
+            // get literal of the AIG node
+            CiId = Gia_ObjId( p->pGia, Gia_ManCi(p->pGia, Var) );
+            // compute interpolant of the clause
+            Res = Gia_ManHashOr( p->pGia, Res, Abc_Var2Lit(CiId, Abc_LitIsCompl(c->lits[i])) );
+        }
+        c->lits[c->size] = Res;
+    }
+    return c->lits[c->size];
+}
+int Int2_ManChainResolve( Int2_Man_t * p, clause * c, int iLit, int varA )
+{
+    int iLit2 = Int2_ManChainStart( p, c );
+    assert( iLit >= 0 );
+    if ( varA )
+        iLit = Gia_ManHashOr( p->pGia, iLit, iLit2 );
+    else
+        iLit = Gia_ManHashAnd( p->pGia, iLit, iLit2 );
+    return iLit;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Test for the interpolation procedure.]
+
+  Description [The input AIG can be any n-input comb circuit with one PO 
+  (not necessarily a comb miter).  The interpolant depends on n+1 variables
+  and equal to the relation f = F(x0,x1,...,xn).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManInterTest( Gia_Man_t * p )
+{
+    sat_solver2 * pSat;
+    Gia_Man_t * pInter;
+    Aig_Man_t * pMan;
+    Vec_Int_t * vGVars;
+    Cnf_Dat_t * pCnf;
+    Aig_Obj_t * pObj;
+    int Lit, Cid, Var, status, i;
+    abctime clk = Abc_Clock();
+    assert( Gia_ManRegNum(p) == 0 );
+    assert( Gia_ManCoNum(p) == 1 );
+
+    // derive CNFs
+    pMan = Gia_ManToAigSimple( p );
+    pCnf = Cnf_Derive( pMan, 1 );
+
+    // start the solver
+    pSat = sat_solver2_new();
+    pSat->fVerbose = 1;
+    sat_solver2_setnvars( pSat, 2*pCnf->nVars+1 );
+
+    // set A-variables (all used except PI/PO, which will be global variables)
+    Aig_ManForEachObj( pMan, pObj, i )
+        if ( pCnf->pVarNums[pObj->Id] >= 0 && !Aig_ObjIsCi(pObj) && !Aig_ObjIsCo(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], -1 );
+        clause2_set_partA( pSat, Cid, 1 ); // this API should be called for each clause of A
+    }
+
+    // add clauses of B (after shifting all CNF variables by pCnf->nVars)
+    Cnf_DataLift( pCnf, pCnf->nVars );
+    for ( i = 0; i < pCnf->nClauses; i++ )
+        sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1], -1 );
+    Cnf_DataLift( pCnf, -pCnf->nVars );
+
+    // add PI equality clauses
+    vGVars = Vec_IntAlloc( Aig_ManCoNum(pMan)+1 );
+    Aig_ManForEachCi( pMan, pObj, i )
+    {
+        Var = pCnf->pVarNums[pObj->Id];
+        sat_solver2_add_buffer( pSat, Var, pCnf->nVars + Var, 0, 0, -1 );
+        Vec_IntPush( vGVars, Var );
+    }
+
+    // add an XOR clause in the end
+    Var = pCnf->pVarNums[Aig_ManCo(pMan,0)->Id];
+    sat_solver2_add_xor( pSat, Var, pCnf->nVars + Var, 2*pCnf->nVars, 0, 0, -1 );
+    Vec_IntPush( vGVars, Var );
+
+    // start the interpolation manager
+    pSat->pInt2 = Int2_ManStart( pSat, Vec_IntArray(vGVars), Vec_IntSize(vGVars) );
+
+    // 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 = (Gia_Man_t *)Int2_ManReadInterpolant( pSat );
+    Gia_ManPrintStats( pInter, 0, 0, 0 );
+    Abc_PrintTime( 1, "Total interpolation time", Abc_Clock() - clk );
+
+    // clean up
+    Vec_IntFree( vGVars );
+    Cnf_DataFree( pCnf );
+    Aig_ManStop( pMan );
+    sat_solver2_delete( pSat );
+
+    // return interpolant
+    return pInter;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+