Started SAT-based reparameterization.

2 files changed, 398 insertions, 0 deletions

diff --git a/src/aig/aig/aigRepar.c b/src/aig/aig/aigRepar.c
new file mode 100644
index 00000000..d10471d7
--- /dev/null
+++ b/src/aig/aig/aigRepar.c
@@ -0,0 +1,397 @@
+/**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
+
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index c291433f..aaf5bf6d 100644
--- a/src/aig/aig/module.make
+++ b/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 \