text: /**CFile****************************************************************
  
    FileName    [pdrSat.c]
  
    SystemName  [ABC: Logic synthesis and verification system.]
  
    PackageName [Property driven reachability.]
  
    Synopsis    [SAT solver procedures.]
  
    Author      [Alan Mishchenko]
    
    Affiliation [UC Berkeley]
  
    Date        [Ver. 1.0. Started - November 20, 2010.]
  
    Revision    [$Id: pdrSat.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
  
  ***********************************************************************/
  
  #include "pdrInt.h"
  
  ABC_NAMESPACE_IMPL_START
  
  
  ////////////////////////////////////////////////////////////////////////
  ///                        DECLARATIONS                              ///
  ////////////////////////////////////////////////////////////////////////
  
  ////////////////////////////////////////////////////////////////////////
  ///                     FUNCTION DEFINITIONS                         ///
  ////////////////////////////////////////////////////////////////////////
  
  /**Function*************************************************************
  
    Synopsis    [Creates new SAT solver.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k )
  {
      sat_solver * pSat;
      Aig_Obj_t * pObj;
      int i;
      assert( Vec_PtrSize(p->vSolvers) == k );
      assert( Vec_VecSize(p->vClauses) == k );
      assert( Vec_IntSize(p->vActVars) == k );
      // create new solver
  //    pSat = sat_solver_new();
      pSat = zsat_solver_new_seed(p->pPars->nRandomSeed);
      pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
      Vec_PtrPush( p->vSolvers, pSat );
      Vec_VecExpand( p->vClauses, k );
      Vec_IntPush( p->vActVars, 0 );
      // add property cone
      Saig_ManForEachPo( p->pAig, pObj, i )
          Pdr_ObjSatVar( p, k, 1, pObj );
      return pSat;
  }
  
  /**Function*************************************************************
  
    Synopsis    [Returns old or restarted solver.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k )
  {
      sat_solver * pSat;
      Vec_Ptr_t * vArrayK;
      Pdr_Set_t * pCube;
      int i, j;
      pSat = Pdr_ManSolver(p, k);
      if ( Vec_IntEntry(p->vActVars, k) < p->pPars->nRecycle )
          return pSat;
      assert( k < Vec_PtrSize(p->vSolvers) - 1 );
      p->nStarts++;
  //    sat_solver_delete( pSat );
  //    pSat = sat_solver_new();
  //    sat_solver_restart( pSat );
      zsat_solver_restart_seed( pSat, p->pPars->nRandomSeed );
      // create new SAT solver
      pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
      // write new SAT solver
      Vec_PtrWriteEntry( p->vSolvers, k, pSat );
      Vec_IntWriteEntry( p->vActVars, k, 0 );
      // set the property output
      Pdr_ManSetPropertyOutput( p, k );
      // add the clauses
      Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, k )
          Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j )
              Pdr_ManSolverAddClause( p, k, pCube );
      return pSat;
  }
  
  /**Function*************************************************************
  
    Synopsis    [Converts SAT variables into register IDs.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  Vec_Int_t * Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, int nArray )
  {
      int i, RegId;
      Vec_IntClear( p->vLits );
      for ( i = 0; i < nArray; i++ )
      {
          RegId = Pdr_ObjRegNum( p, k, Abc_Lit2Var(pArray[i]) );
          if ( RegId == -1 )
              continue;
          assert( RegId >= 0 && RegId < Aig_ManRegNum(p->pAig) );
          Vec_IntPush( p->vLits, Abc_Var2Lit(RegId, !Abc_LitIsCompl(pArray[i])) );
      }
      assert( Vec_IntSize(p->vLits) >= 0 && Vec_IntSize(p->vLits) <= nArray );
      return p->vLits;
  }
  
  /**Function*************************************************************
  
    Synopsis    [Converts the cube in terms of RO numbers into array of CNF literals.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCompl, int fNext )
  {
      Aig_Obj_t * pObj;
      int i, iVar, iVarMax = 0;
      abctime clk = Abc_Clock();
      Vec_IntClear( p->vLits );
  //    assert( !(fNext && fCompl) );
      for ( i = 0; i < pCube->nLits; i++ )
      {
          if ( pCube->Lits[i] == -1 )
              continue;
          if ( fNext )
              pObj = Saig_ManLi( p->pAig, Abc_Lit2Var(pCube->Lits[i]) );
          else
              pObj = Saig_ManLo( p->pAig, Abc_Lit2Var(pCube->Lits[i]) );
          iVar = Pdr_ObjSatVar( p, k, fNext ? 2 - Abc_LitIsCompl(pCube->Lits[i]) : 3, pObj ); assert( iVar >= 0 );
          iVarMax = Abc_MaxInt( iVarMax, iVar );
          Vec_IntPush( p->vLits, Abc_Var2Lit( iVar, fCompl ^ Abc_LitIsCompl(pCube->Lits[i]) ) );
      }
  //    sat_solver_setnvars( Pdr_ManSolver(p, k), iVarMax + 1 );
      p->tCnf += Abc_Clock() - clk;
      return p->vLits;
  }
  
  /**Function*************************************************************
  
    Synopsis    [Sets the property output to 0 (sat) forever.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k )
  {
      sat_solver * pSat;
      Aig_Obj_t * pObj;
      int Lit, RetValue, i;
      if ( !p->pPars->fUsePropOut )
          return;
      pSat = Pdr_ManSolver(p, k);
      Saig_ManForEachPo( p->pAig, pObj, i )
      {
          // skip solved outputs
          if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
              continue;
          // skip timedout outputs
          if ( p->pPars->vOutMap && Vec_IntEntry(p->pPars->vOutMap, i) == -1 )
              continue;
          Lit = Abc_Var2Lit( Pdr_ObjSatVar(p, k, 1, pObj), 1 ); // neg literal
          RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
          assert( RetValue == 1 );
      }
      sat_solver_compress( pSat );
  }
  
  /**Function*************************************************************
  
    Synopsis    [Adds one clause in terms of ROs to the k-th SAT solver.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Pdr_ManSolverAddClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
  {
      sat_solver * pSat;
      Vec_Int_t * vLits;
      int RetValue;
      pSat  = Pdr_ManSolver(p, k);
      vLits = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
      RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
      assert( RetValue == 1 );
      sat_solver_compress( pSat );
  }
  
  /**Function*************************************************************
  
    Synopsis    [Collects values of the RO/RI variables in k-th SAT solver.]
  
    Description []
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues )
  {
      sat_solver * pSat;
      Aig_Obj_t * pObj;
      int iVar, i;
      Vec_IntClear( vValues );
      pSat = Pdr_ManSolver(p, k);
      Aig_ManForEachObjVec( vObjIds, p->pAig, pObj, i )
      {
          iVar = Pdr_ObjSatVar( p, k, 3, pObj ); assert( iVar >= 0 );
          Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
      }
  }
  
  /**Function*************************************************************
  
    Synopsis    [Checks if the cube holds (UNSAT) in the given timeframe.]
   
    Description [Return 1/0 if cube or property are proved to hold/fail
    in k-th timeframe.  Returns the predecessor bad state in ppPred.]
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
  { 
      sat_solver * pSat;
      Vec_Int_t * vLits;
      abctime Limit;
      int RetValue;
      pSat = Pdr_ManFetchSolver( p, k );
      vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 0 );
      Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
      RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
      sat_solver_set_runtime_limit( pSat, Limit );
      if ( RetValue == l_Undef )
          return -1;
      return (RetValue == l_False);
  }
  
  /**Function*************************************************************
  
    Synopsis    [Checks if the cube holds (UNSAT) in the given timeframe.]
   
    Description [Return 1/0 if cube or property are proved to hold/fail
    in k-th timeframe.  Returns the predecessor bad state in ppPred.]
                 
    SideEffects []
  
    SeeAlso     []
  
  ***********************************************************************/
  int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit, int fTryConf, int fUseLit )
  { 
      //int fUseLit = 0;
      int fLitUsed = 0;
      sat_solver * pSat;
      Vec_Int_t * vLits;
      int Lit, RetValue;
      abctime clk, Limit;
      p->nCalls++;
      pSat = Pdr_ManFetchSolver( p, k );
      if ( pCube == NULL ) // solve the property
      {
          clk = Abc_Clock();
          Lit = Abc_Var2Lit( Pdr_ObjSatVar(p, k, 2, Aig_ManCo(p->pAig, p->iOutCur)), 0 ); // pos literal (property fails)
          Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
          RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 );
          sat_solver_set_runtime_limit( pSat, Limit );
          if ( RetValue == l_Undef )
              return -1;
      }
      else // check relative containment in terms of next states
      {
          if ( fUseLit )
          {
              fLitUsed = 1;
              Vec_IntAddToEntry( p->vActVars, k, 1 );
              // add the cube in terms of current state variables
              vLits = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
              // add activation literal
              Lit = Abc_Var2Lit( Pdr_ManFreeVar(p, k), 0 );
              // add activation literal
              Vec_IntPush( vLits, Lit );
              RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
              assert( RetValue == 1 );
              sat_solver_compress( pSat );
              // create assumptions
              vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
              // add activation literal
              Vec_IntPush( vLits, Abc_LitNot(Lit) );
          }
          else
              vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
  
          // solve 
          clk = Abc_Clock();
          Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
          RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), fTryConf ? p->pPars->nConfGenLimit : nConfLimit, 0, 0, 0 );
          sat_solver_set_runtime_limit( pSat, Limit );
          if ( RetValue == l_Undef )
          {
              if ( fTryConf && p->pPars->nConfGenLimit )
                  RetValue = l_True;
              else
                  return -1;
          }
      }
      clk = Abc_Clock() - clk;
      p->tSat += clk;
      assert( RetValue != l_Undef );
      if ( RetValue == l_False )
      {
          p->tSatUnsat += clk;
          p->nCallsU++;
          if ( ppPred )
              *ppPred = NULL;
          RetValue = 1;
      }
      else // if ( RetValue == l_True )
      {
          p->tSatSat += clk;
          p->nCallsS++;
          if ( ppPred )
          {
              abctime clk = Abc_Clock();
              if ( p->pPars->fNewXSim )
                  *ppPred = Txs3_ManTernarySim( p->pTxs3, k, pCube );
              else
                  *ppPred = Pdr_ManTernarySim( p, k, pCube );
              p->tTsim += Abc_Clock() - clk;
              p->nXsimLits += (*ppPred)->nLits;
              p->nXsimRuns++;
          }
          RetValue = 0;
      }
  
  /* // for some reason, it does not work...
      if ( fLitUsed )
      {
          int RetValue;
          Lit = Abc_LitNot(Lit);
          RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
          assert( RetValue == 1 );
          sat_solver_compress( pSat );
      }
  */
      return RetValue;
  }
  
  
  ////////////////////////////////////////////////////////////////////////
  ///                       END OF FILE                                ///
  ////////////////////////////////////////////////////////////////////////
  
  
  ABC_NAMESPACE_IMPL_END
  
  