Version abc70930

1 files changed, 0 insertions, 452 deletions

diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c
deleted file mode 100644
index 11029b69..00000000
--- a/src/aig/fra/fraSat.c
+++ /dev/null
@@ -1,452 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraSat.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [New FRAIG package.]
-
-  Synopsis    []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 30, 2007.]
-
-  Revision    [$Id: fraSat.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include <math.h>
-#include "fra.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Runs equivalence test for the two nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
-{
-    int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock();
-    int status;
-
-    // make sure the nodes are not complemented
-    assert( !Aig_IsComplement(pNew) );
-    assert( !Aig_IsComplement(pOld) );
-    assert( pNew != pOld );
-
-    // if at least one of the nodes is a failed node, perform adjustments:
-    // if the backtrack limit is small, simply skip this node
-    // if the backtrack limit is > 10, take the quare root of the limit
-    nBTLimit = p->pPars->nBTLimitNode;
-    if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
-    {
-        p->nSatFails++;
-        // fail immediately
-//        return -1;
-        if ( nBTLimit <= 10 )
-            return -1;
-        nBTLimit = (int)pow(nBTLimit, 0.7);
-    }
-
-    p->nSatCalls++;
-    p->nSatCallsRecent++;
-
-    // make sure the solver is allocated and has enough variables
-    if ( p->pSat == NULL )
-    {
-        p->pSat = sat_solver_new();
-        p->nSatVars = 1;
-        sat_solver_setnvars( p->pSat, 1000 );
-        // var 0 is reserved for const1 node - add the clause
-        pLits[0] = toLit( 0 );
-        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
-    }
-
-    // if the nodes do not have SAT variables, allocate them
-    Fra_CnfNodeAddToSolver( p, pOld, pNew );
-
-    if ( p->pSat->qtail != p->pSat->qhead )
-    {
-        status = sat_solver_simplify(p->pSat);
-        assert( status != 0 );
-        assert( p->pSat->qtail == p->pSat->qhead );
-    }
-
-    // prepare variable activity
-    if ( p->pPars->fConeBias )
-        Fra_SetActivityFactors( p, pOld, pNew ); 
-
-    // solve under assumptions
-    // A = 1; B = 0     OR     A = 1; B = 1 
-clk = clock();
-    pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
-    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
-//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
-    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
-        (sint64)nBTLimit, (sint64)0, 
-        p->nBTLimitGlobal, p->nInsLimitGlobal );
-p->timeSat += clock() - clk;
-    if ( RetValue1 == l_False )
-    {
-p->timeSatUnsat += clock() - clk;
-        pLits[0] = lit_neg( pLits[0] );
-        pLits[1] = lit_neg( pLits[1] );
-        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
-        assert( RetValue );
-        // continue solving the other implication
-        p->nSatCallsUnsat++;
-    }
-    else if ( RetValue1 == l_True )
-    {
-p->timeSatSat += clock() - clk;
-        Fra_SmlSavePattern( p );
-        p->nSatCallsSat++;
-        return 0;
-    }
-    else // if ( RetValue1 == l_Undef )
-    {
-p->timeSatFail += clock() - clk;
-        // mark the node as the failed node
-        if ( pOld != p->pManFraig->pConst1 ) 
-            pOld->fMarkB = 1;
-        pNew->fMarkB = 1;
-        p->nSatFailsReal++;
-        return -1;
-    }
-
-    // if the old node was constant 0, we already know the answer
-    if ( pOld == p->pManFraig->pConst1 )
-    {
-        p->nSatProof++;
-        return 1;
-    }
-
-    // solve under assumptions
-    // A = 0; B = 1     OR     A = 0; B = 0 
-clk = clock();
-    pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 1 );
-    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase );
-    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
-        (sint64)nBTLimit, (sint64)0, 
-        p->nBTLimitGlobal, p->nInsLimitGlobal );
-p->timeSat += clock() - clk;
-    if ( RetValue1 == l_False )
-    {
-p->timeSatUnsat += clock() - clk;
-        pLits[0] = lit_neg( pLits[0] );
-        pLits[1] = lit_neg( pLits[1] );
-        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
-        assert( RetValue );
-        p->nSatCallsUnsat++;
-    }
-    else if ( RetValue1 == l_True )
-    {
-p->timeSatSat += clock() - clk;
-        Fra_SmlSavePattern( p );
-        p->nSatCallsSat++;
-        return 0;
-    }
-    else // if ( RetValue1 == l_Undef )
-    {
-p->timeSatFail += clock() - clk;
-        // mark the node as the failed node
-        pOld->fMarkB = 1;
-        pNew->fMarkB = 1;
-        p->nSatFailsReal++;
-        return -1;
-    }
-/*
-    // check BDD proof
-    {
-        int RetVal;
-        PRT( "Sat", clock() - clk2 );
-        clk2 = clock();
-        RetVal = Fra_NodesAreEquivBdd( pOld, pNew );
-//        printf( "%d ", RetVal );
-        assert( RetVal );
-        PRT( "Bdd", clock() - clk2 );
-        printf( "\n" );
-    }
-*/
-    // return SAT proof
-    p->nSatProof++;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Runs the result of test for pObj => pNew.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR )
-{
-    int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock();
-    int status;
-
-    // make sure the nodes are not complemented
-    assert( !Aig_IsComplement(pNew) );
-    assert( !Aig_IsComplement(pOld) );
-    assert( pNew != pOld );
-
-    // if at least one of the nodes is a failed node, perform adjustments:
-    // if the backtrack limit is small, simply skip this node
-    // if the backtrack limit is > 10, take the quare root of the limit
-    nBTLimit = p->pPars->nBTLimitNode;
-/*
-    if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
-    {
-        p->nSatFails++;
-        // fail immediately
-//        return -1;
-        if ( nBTLimit <= 10 )
-            return -1;
-        nBTLimit = (int)pow(nBTLimit, 0.7);
-    }
-*/
-    p->nSatCalls++;
-
-    // make sure the solver is allocated and has enough variables
-    if ( p->pSat == NULL )
-    {
-        p->pSat = sat_solver_new();
-        p->nSatVars = 1;
-        sat_solver_setnvars( p->pSat, 1000 );
-        // var 0 is reserved for const1 node - add the clause
-        pLits[0] = toLit( 0 );
-        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
-    }
-
-    // if the nodes do not have SAT variables, allocate them
-    Fra_CnfNodeAddToSolver( p, pOld, pNew );
-
-    if ( p->pSat->qtail != p->pSat->qhead )
-    {
-        status = sat_solver_simplify(p->pSat);
-        assert( status != 0 );
-        assert( p->pSat->qtail == p->pSat->qhead );
-    }
-
-    // prepare variable activity
-    if ( p->pPars->fConeBias )
-        Fra_SetActivityFactors( p, pOld, pNew ); 
-
-    // solve under assumptions
-    // A = 1; B = 0     OR     A = 1; B = 1 
-clk = clock();
-//    pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
-//    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
-    pLits[0] = toLitCond( Fra_ObjSatNum(pOld),  fComplL );
-    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), !fComplR );
-//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
-    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
-        (sint64)nBTLimit, (sint64)0, 
-        p->nBTLimitGlobal, p->nInsLimitGlobal );
-p->timeSat += clock() - clk;
-    if ( RetValue1 == l_False )
-    {
-p->timeSatUnsat += clock() - clk;
-        pLits[0] = lit_neg( pLits[0] );
-        pLits[1] = lit_neg( pLits[1] );
-        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
-        assert( RetValue );
-        // continue solving the other implication
-        p->nSatCallsUnsat++;
-    }
-    else if ( RetValue1 == l_True )
-    {
-p->timeSatSat += clock() - clk;
-        Fra_SmlSavePattern( p );
-        p->nSatCallsSat++;
-        return 0;
-    }
-    else // if ( RetValue1 == l_Undef )
-    {
-p->timeSatFail += clock() - clk;
-        // mark the node as the failed node
-        if ( pOld != p->pManFraig->pConst1 ) 
-            pOld->fMarkB = 1;
-        pNew->fMarkB = 1;
-        p->nSatFailsReal++;
-        return -1;
-    }
-    // return SAT proof
-    p->nSatProof++;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Runs equivalence test for one node.]
-
-  Description [Returns the fraiged node.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew )
-{
-    int pLits[2], RetValue1, RetValue, clk;
-
-    // make sure the nodes are not complemented
-    assert( !Aig_IsComplement(pNew) );
-    assert( pNew != p->pManFraig->pConst1 );
-    p->nSatCalls++;
-
-    // make sure the solver is allocated and has enough variables
-    if ( p->pSat == NULL )
-    {
-        p->pSat = sat_solver_new();
-        p->nSatVars = 1;
-        sat_solver_setnvars( p->pSat, 1000 );
-        // var 0 is reserved for const1 node - add the clause
-        pLits[0] = toLit( 0 );
-        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
-    }
-
-    // if the nodes do not have SAT variables, allocate them
-    Fra_CnfNodeAddToSolver( p, NULL, pNew );
-
-    // prepare variable activity
-    if ( p->pPars->fConeBias )
-        Fra_SetActivityFactors( p, NULL, pNew ); 
-
-    // solve under assumptions
-clk = clock();
-    pLits[0] = toLitCond( Fra_ObjSatNum(pNew), pNew->fPhase );
-    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1, 
-        (sint64)p->pPars->nBTLimitMiter, (sint64)0, 
-        p->nBTLimitGlobal, p->nInsLimitGlobal );
-p->timeSat += clock() - clk;
-    if ( RetValue1 == l_False )
-    {
-p->timeSatUnsat += clock() - clk;
-        pLits[0] = lit_neg( pLits[0] );
-        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
-        assert( RetValue );
-        // continue solving the other implication
-        p->nSatCallsUnsat++;
-    }
-    else if ( RetValue1 == l_True )
-    {
-p->timeSatSat += clock() - clk;
-        if ( p->pPatWords )
-            Fra_SmlSavePattern( p );
-        p->nSatCallsSat++;
-        return 0;
-    }
-    else // if ( RetValue1 == l_Undef )
-    {
-p->timeSatFail += clock() - clk;
-        // mark the node as the failed node
-        pNew->fMarkB = 1;
-        p->nSatFailsReal++;
-        return -1;
-    }
-
-    // return SAT proof
-    p->nSatProof++;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets variable activities in the cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_SetActivityFactors_rec( Fra_Man_t * p, Aig_Obj_t * pObj, int LevelMin, int LevelMax )
-{
-    Vec_Ptr_t * vFanins;
-    Aig_Obj_t * pFanin;
-    int i, Counter = 0;
-    assert( !Aig_IsComplement(pObj) );
-    assert( Fra_ObjSatNum(pObj) );
-    // skip visited variables
-    if ( Aig_ObjIsTravIdCurrent(p->pManFraig, pObj) )
-        return 0;
-    Aig_ObjSetTravIdCurrent(p->pManFraig, pObj);
-    // add the PI to the list
-    if ( pObj->Level <= (unsigned)LevelMin || Aig_ObjIsPi(pObj) )
-        return 0;
-    // set the factor of this variable
-    // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pPars->dActConeBumpMax / ThisBump
-    p->pSat->factors[Fra_ObjSatNum(pObj)] = p->pPars->dActConeBumpMax * (pObj->Level - LevelMin)/(LevelMax - LevelMin);
-    veci_push(&p->pSat->act_vars, Fra_ObjSatNum(pObj));
-    // explore the fanins
-    vFanins = Fra_ObjFaninVec( pObj );
-    Vec_PtrForEachEntry( vFanins, pFanin, i )
-        Counter += Fra_SetActivityFactors_rec( p, Aig_Regular(pFanin), LevelMin, LevelMax );
-    return 1 + Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets variable activities in the cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
-{
-    int clk, LevelMin, LevelMax;
-    assert( pOld || pNew );
-clk = clock(); 
-    // reset the active variables
-    veci_resize(&p->pSat->act_vars, 0);
-    // prepare for traversal
-    Aig_ManIncrementTravId( p->pManFraig );
-    // determine the min and max level to visit
-    assert( p->pPars->dActConeRatio > 0 && p->pPars->dActConeRatio < 1 );
-    LevelMax = AIG_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
-    LevelMin = (int)(LevelMax * (1.0 - p->pPars->dActConeRatio));
-    // traverse
-    if ( pOld && !Aig_ObjIsConst1(pOld) )
-        Fra_SetActivityFactors_rec( p, pOld, LevelMin, LevelMax );
-    if ( pNew && !Aig_ObjIsConst1(pNew) )
-        Fra_SetActivityFactors_rec( p, pNew, LevelMin, LevelMax );
-//Fra_PrintActivity( p );
-p->timeTrav += clock() - clk;
-    return 1;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-