src/bmc/bmcAutSat.c

Go to the documentation of this file.

#include "bmc.h"
#include "bmcInt.h"

static char rcsid[] UNUSED = "$Id: bmcAutSat.c,v 1.10 2005/04/16 18:02:25 awedh Exp $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

int
BmcAutLtlCheckForTermination(
  Ntk_Network_t            *network,
  array_t                  *constraintArray,
  BmcCheckForTermination_t *terminationStatus,
  st_table                 *nodeToMvfAigTable,
  st_table                 *CoiTable,
  BmcOption_t              *options)
{
  
  BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
  FILE            *cnfFile;
  array_t         *result = NIL(array_t);
  array_t         *unitClause = array_alloc(int, 0);
  array_t         *orClause;

  long            startTime, endTime;
  int             k = terminationStatus->k;
  int             returnStatus = 0;
  Ltl_Automaton_t *automaton = terminationStatus->automaton;

  /*
    If checkLevel == 0 -->  check for beta' only and if UNSAT, m=k and chekLevel =1
    If checkLevel == 1 -->  check for beta  only and if UNSAT, checkLevel = 2.
    If checkLevel == 2 -->  check for alpha only and if UNSAT, n=k and checkLevel = 3.
    If gama is UNSAT up to (m+n-1) and checkLvel = 3, formula passes.
    checkLevel = 4 if (m+n-1) > maxK;
   */ 
  startTime = util_cpu_ctime();
 
  /* ===========================
     Early termination condition
     =========================== */
  if (options->earlyTermination) {
    if (options->verbosityLevel == BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout, "\nChecking the early termination at k= %d\n", k);
    }
    /*
      Create clauses database 
    */
    cnfClauses = BmcCnfClausesAlloc();

    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
    if (cnfFile == NIL(FILE)) {
      (void)fprintf(vis_stderr,
                    "** bmc error: Cannot create CNF output file %s\n",
                    options->satInFile);
      return -1;
    }
    BmcAutCnfGenerateClausesForSimpleCompositePath(network, automaton, 0, k, BMC_INITIAL_STATES,
                                                cnfClauses, nodeToMvfAigTable, CoiTable);
    BmcWriteClauses(NIL(mAig_Manager_t), cnfFile, cnfClauses, options);
    (void) fclose(cnfFile);
    BmcCnfClausesFree(cnfClauses);
          
    result = BmcCheckSAT(options);
    if(options->satSolverError){
      return -1;
    }
    if(result == NIL(array_t)) {
      (void) fprintf(vis_stdout, "# BMC: by early ermination\n");
      return 3;
    }
  } /* Early termination */
   if((!automaton->fairSets) &&
     (terminationStatus->checkLevel == 0)) {
    /*
      All the automaton states are fair states. So, beta' and beta are always UNSAT.
    */
    terminationStatus->m = 0;
     (void) fprintf(vis_stdout,"Value of m = %d\n", terminationStatus->m);
    terminationStatus->checkLevel = 2;
  }
  /*
    beta''(k) 
  */
  if(terminationStatus->checkLevel == 0){ 
    int i;
    /*
      Create clauses database 
    */
    cnfClauses = BmcCnfClausesAlloc();
    if (options->verbosityLevel == BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout, "# BMC: Check Beta'' \n");
    }
    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
    if (cnfFile == NIL(FILE)) {
      (void)fprintf(vis_stderr,
                    "** bmc error: Cannot create CNF output file %s\n",
                    options->satInFile);
      return -1;
    }
    BmcAutCnfGenerateClausesForSimpleCompositePath(network, automaton, 0, k+1, BMC_NO_INITIAL_STATES,
                                                cnfClauses, nodeToMvfAigTable, CoiTable);
    for(i=1; i<=k+1; i++){
      if(constraintArray != NIL(array_t)){
        Ctlsp_Formula_t *formula;
        int              j;
        
        arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
          array_insert(int, unitClause, 0,
                       - BmcGenerateCnfForLtl(network, formula, i, i, -1, cnfClauses)
                       );
          BmcCnfInsertClause(cnfClauses, unitClause);
        }
      }
      array_insert(int, unitClause, 0,
                   - BmcAutGenerateCnfForBddOffSet(automaton->fairSets, i, i, cnfClauses, NIL(st_table))
                   );
      BmcCnfInsertClause(cnfClauses, unitClause);
    }
       if(constraintArray != NIL(array_t)){
      Ctlsp_Formula_t *formula;
      int              j;

      orClause   = array_alloc(int, 0);
      
      arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
        array_insert_last(int, orClause,
                          BmcGenerateCnfForLtl(network, formula, k+1, k+1, -1, cnfClauses)
                          );
      }
      array_insert_last(int, orClause, 
                        BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k+1, k+1, cnfClauses, NIL(st_table))
                        );
      BmcCnfInsertClause(cnfClauses, orClause);
      array_free(orClause);
    } else {
      array_insert(int, unitClause, 0, 
                   BmcAutGenerateCnfForBddOffSet(automaton->fairSets, 0, 0, cnfClauses, NIL(st_table))
                   );
      BmcCnfInsertClause(cnfClauses, unitClause);
    }
    BmcWriteClauses(NIL(mAig_Manager_t), cnfFile, cnfClauses, options);
    (void) fclose(cnfFile);
    
    result = BmcCheckSAT(options);
    
    if(options->satSolverError){
      return -1;
    }
    if(result == NIL(array_t)) {
      terminationStatus->m = k;
      (void)fprintf(vis_stderr,"m = %d\n", terminationStatus->m);
      terminationStatus->checkLevel = 1;
    }
    BmcCnfClausesFree(cnfClauses);
  } /* Check for Beta' */
  
  /*
    beta'(k) 
  */
  if(terminationStatus->checkLevel == 0){
    int i;
    /*
      Create clauses database 
    */
    cnfClauses = BmcCnfClausesAlloc();
    if (options->verbosityLevel == BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout, "# BMC: Check Beta' \n");
    }
    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
    if (cnfFile == NIL(FILE)) {
      (void)fprintf(vis_stderr,
                    "** bmc error: Cannot create CNF output file %s\n",
                    options->satInFile);
      return -1;
    }
    BmcAutCnfGenerateClausesForSimpleCompositePath(network, automaton, 0, k+1, BMC_NO_INITIAL_STATES,
                                                cnfClauses, nodeToMvfAigTable, CoiTable);
    for(i=0; i<=k; i++){
      if(constraintArray != NIL(array_t)){
        Ctlsp_Formula_t *formula;
        int              j;
        
        arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
          array_insert(int, unitClause, 0,
                       - BmcGenerateCnfForLtl(network, formula, i, i, -1, cnfClauses)
                       );
          BmcCnfInsertClause(cnfClauses, unitClause);
        }
      }
      array_insert(int, unitClause, 0,
                   - BmcAutGenerateCnfForBddOffSet(automaton->fairSets, i, i, cnfClauses, NIL(st_table))
                   );
      BmcCnfInsertClause(cnfClauses, unitClause);
    }
    if(constraintArray != NIL(array_t)){
      Ctlsp_Formula_t *formula;
      int              j;

      orClause   = array_alloc(int, 0);
      
      arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
        array_insert_last(int, orClause,
                          BmcGenerateCnfForLtl(network, formula, k+1, k+1, -1, cnfClauses)
                          );
      }
      array_insert_last(int, orClause, 
                        BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k+1, k+1, cnfClauses, NIL(st_table))
                        );
      BmcCnfInsertClause(cnfClauses, orClause);
      array_free(orClause);
    } else {
      array_insert(int, unitClause, 0, 
                   BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k+1, k+1, cnfClauses, NIL(st_table))
                   );
      BmcCnfInsertClause(cnfClauses, unitClause);
    }
    
    BmcWriteClauses(NIL(mAig_Manager_t), cnfFile, cnfClauses, options);
    (void) fclose(cnfFile);
    
    result = BmcCheckSAT(options);
    
    if(options->satSolverError){
      return -1;
    }
    if(result == NIL(array_t)) {
      terminationStatus->m = k;
      (void)fprintf(vis_stdout,"Value of m = %d\n", terminationStatus->m);
      terminationStatus->checkLevel = 1;
    }
    BmcCnfClausesFree(cnfClauses);
  } /* Check for Beta' */
  
  /*
    Check for Beta.
  */
  if(terminationStatus->checkLevel == 1){
    cnfClauses = BmcCnfClausesAlloc();
    {/* To print a witness */
      /*  lsGen               lsGen;
      vertex_t            *vtx;
      Ltl_AutomatonNode_t *state;
      int i;
      
      foreach_vertex(automaton->G, lsGen, vtx) {
        state = (Ltl_AutomatonNode_t *) vtx->user_data;
        state->cnfIndex = ALLOC(int, k+2);
        for(i=0; i<=k+1; i++){
          state->cnfIndex[i] = BmcAutGenerateCnfForBddOffSet(state->Encode, i,
                                                             i, cnfClauses, NIL(st_table));
        }
        } */
    }/* To print a witness */
    if (options->verbosityLevel == BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout, "# BMC: Check Beta\n");
    }
    
    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
    if (cnfFile == NIL(FILE)) {
      (void)fprintf(vis_stderr,
                    "** bmc error: Cannot create CNF output file %s\n",
                    options->satInFile);
      return -1;
    }
    /*
      Generate a simple path of length k+1.
    */
    BmcAutCnfGenerateClausesForSimpleCompositePath(network, automaton, 0, k+1, BMC_NO_INITIAL_STATES,
                                                cnfClauses, nodeToMvfAigTable,
                                                   CoiTable);

    if(constraintArray != NIL(array_t)){
      Ctlsp_Formula_t *formula;
      int              j;
      
      arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
        array_insert(int, unitClause, 0,
                     - BmcGenerateCnfForLtl(network, formula, k, k, -1, cnfClauses)
                     );
        BmcCnfInsertClause(cnfClauses, unitClause);
      }
    }
    
    array_insert(int, unitClause, 0, 
                 - BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k, k, cnfClauses, NIL(st_table))
                 );
    BmcCnfInsertClause(cnfClauses, unitClause);

   if(constraintArray != NIL(array_t)){
      Ctlsp_Formula_t *formula;
      int              j;

      orClause   = array_alloc(int, 0);
      
      arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
        array_insert_last(int, orClause,
                          BmcGenerateCnfForLtl(network, formula, k+1, k+1, -1, cnfClauses)
                          );
      }
      array_insert_last(int, orClause, 
                        BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k+1, k+1, cnfClauses, NIL(st_table))
                        );
      BmcCnfInsertClause(cnfClauses, orClause);
      array_free(orClause);
    } else { 
      array_insert(int, unitClause, 0, 
                   BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k+1, k+1, cnfClauses, NIL(st_table))
                   );
      BmcCnfInsertClause(cnfClauses, unitClause);
    }
    
    BmcWriteClauses(NIL(mAig_Manager_t), cnfFile, cnfClauses, options);
    (void) fclose(cnfFile);
    
    result = BmcCheckSAT(options);
    
    if(options->satSolverError){
      return -1;
    }
    if(result == NIL(array_t)) {
      terminationStatus->checkLevel = 2;
    }
    BmcCnfClausesFree(cnfClauses);
  } /* Check Beta*/
  
  if(terminationStatus->checkLevel == 2){ /* we check Alpha if Beta is unsatisfiable */

    if (options->verbosityLevel == BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout, "# BMC: Check Alpha \n");
    }
    
    cnfClauses = BmcCnfClausesAlloc();
      
    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
    if (cnfFile == NIL(FILE)) {
      (void)fprintf(vis_stderr,
                    "** bmc error: Cannot create CNF output file %s\n",
                    options->satInFile);
      return -1;
    }
    
    BmcAutCnfGenerateClausesForSimpleCompositePath(network, automaton, 0, k, BMC_INITIAL_STATES,
                                                cnfClauses, nodeToMvfAigTable, CoiTable);
    if(automaton->fairSets){

      if(constraintArray != NIL(array_t)){
        Ctlsp_Formula_t *formula;
        int              j;
        
        orClause   = array_alloc(int, 0);
        
        arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
          array_insert_last(int, orClause,
                            BmcGenerateCnfForLtl(network, formula, k, k, -1, cnfClauses)
                            );
        }
        array_insert_last(int, orClause, 
                          BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k, k, cnfClauses, NIL(st_table))
                          );
        BmcCnfInsertClause(cnfClauses, orClause);
        array_free(orClause);
      } else {
        
        array_insert(int, unitClause, 0,  
                     BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k, k, cnfClauses, NIL(st_table))
                     );
        BmcCnfInsertClause(cnfClauses, unitClause);
      }
    }
    BmcWriteClauses(NIL(mAig_Manager_t), cnfFile, cnfClauses, options);
    (void) fclose(cnfFile);
    
    result = BmcCheckSAT(options);
    BmcCnfClausesFree(cnfClauses);
    if(options->satSolverError){
      return -1;
    }
    if(result == NIL(array_t)) {
      terminationStatus->n = k;
      terminationStatus->checkLevel = 3;
      (void)fprintf(vis_stderr,"m=%d  n=%d\n",terminationStatus->m,terminationStatus->n);
      if ((terminationStatus->m+terminationStatus->n-1) <= options->maxK){
        terminationStatus->k = terminationStatus->m+terminationStatus->n-1;
        if(k==0){
          /*
            By induction, the property passes.
          */
          terminationStatus->k = 0;
        }
        returnStatus = 1;
      } else {
        terminationStatus->checkLevel = 4;
        returnStatus = 2;
      }
    }
  }/* Chek for Alpha */
  
  array_free(unitClause);

  if (options->verbosityLevel != BmcVerbosityNone_c) {
    endTime = util_cpu_ctime();
    fprintf(vis_stdout, "-- Check for termination time time = %10g\n",
            (double)(endTime - startTime) / 1000.0);
  }

  return returnStatus;
 
} /* BmcAutLtlCheckForTermination */


void
BmcAutCnfGenerateClausesForPath(
  Ltl_Automaton_t *automaton,
  int             fromState,
  int             toState,
  int             initialState,
  BmcCnfClauses_t *cnfClauses)
{
  int          k;
  array_t      *unitClause = array_alloc(int, 1);

  if(initialState){
    array_insert(int, unitClause, 0, 
                 BmcAutGenerateCnfForBddOffSet(automaton->initialStates, 0, 0, cnfClauses, automaton->nsPsTable)
                 );
    BmcCnfInsertClause(cnfClauses, unitClause);
  }
  for(k=fromState; k<toState; k++){
    array_insert(int, unitClause, 0,  
    BmcAutGenerateCnfForBddOffSet(automaton->transitionRelation, k, k+1, cnfClauses, automaton->nsPsTable)
                      );
    BmcCnfInsertClause(cnfClauses, unitClause);
  }
  array_free(unitClause);
  
} /* BmcAutCnfGenerateClausesForPath() */


void
BmcAutCnfGenerateClausesForSimpleCompositePath(
   Ntk_Network_t   *network,
   Ltl_Automaton_t *automaton,
   int             fromState,
   int             toState,
   int             initialState,
   BmcCnfClauses_t *cnfClauses,
   st_table        *nodeToMvfAigTable,
   st_table        *CoiTable)
{
  int state;
  
  /*
    Generate clauses for a path from fromState to toState in the original model.
  */
  BmcCnfGenerateClausesForPath(network, fromState, toState, initialState, cnfClauses, nodeToMvfAigTable, CoiTable);
  /*
    Generate clauses for a path from fromState to toState in the Automaton.
  */
  BmcAutCnfGenerateClausesForPath(automaton, fromState, toState, initialState, cnfClauses);
  
  /*
    Restrict the above path to be simpe path.
  */
  for(state= fromState + 1; state < toState; state++){
    BmcCnfNoLoopToAnyPreviouseCompositeStates(network, automaton, fromState, state,
                                              cnfClauses, nodeToMvfAigTable, CoiTable);
  }

  return;
} /* BmcAutCnfGenerateClausesForSimpleCompositePath */


void
BmcCnfNoLoopToAnyPreviouseCompositeStates(
   Ntk_Network_t   *network,
   Ltl_Automaton_t *automaton,
   int             fromState,
   int             toState,
   BmcCnfClauses_t *cnfClauses,
   st_table        *nodeToMvfAigTable,
   st_table        *CoiTable)
{
  mAig_Manager_t     *manager   = Ntk_NetworkReadMAigManager(network);
  bdd_manager        *bddManager = bdd_get_manager(automaton->transitionRelation);
  
  Ntk_Node_t         *latch;
  MvfAig_Function_t  *latchMvfAig;
  bAigEdge_t         *latchBAig;
  array_t            *orClause;
  int                currentIndex, nextIndex, andIndex1, andIndex2;  
  int                i, k, mvfSize, bddID;
    
  st_generator       *stGen;

  /*
    Generates CNF clauses to constrain that the toState is not equal
    to any previouse states starting from fromState.
    
    Assume there are two state varaibles a and b. To check if Si !=
    Sj, we must generate clauses for the formula ( ai != aj + bi !=
    bj).
  */
  for(k=fromState; k < toState; k++){
    orClause = array_alloc(int,0);
    st_foreach_item(CoiTable, stGen, &latch, NULL) {
      
  
      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
      if (latchMvfAig ==  NIL(MvfAig_Function_t)){
        latchMvfAig = Bmc_NodeBuildMVF(network, latch);
        array_free(latchMvfAig);
        latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
      } 
      mvfSize   = array_n(latchMvfAig);
      latchBAig = ALLOC(bAigEdge_t, mvfSize);   
      
      for(i=0; i< mvfSize; i++){
        latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i));
      }

      for (i=0; i< mvfSize; i++){
        currentIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], k       ,cnfClauses);
        nextIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], toState ,cnfClauses);     
        andIndex1 = cnfClauses->cnfGlobalIndex++;
        BmcCnfGenerateClausesForAND(currentIndex, -nextIndex, andIndex1, cnfClauses);
        andIndex2 = cnfClauses->cnfGlobalIndex++;
        BmcCnfGenerateClausesForAND(-currentIndex, nextIndex, andIndex2, cnfClauses);

        array_insert_last(int, orClause, andIndex1);
        array_insert_last(int, orClause, andIndex2);
      }
      FREE(latchBAig);
    }/* For each latch loop*/
    st_foreach_item(automaton->psNsTable, stGen, &bddID, NULL) {
      currentIndex = BmcGetCnfVarIndexForBddNode(bddManager, bdd_regular(bdd_bdd_ith_var(bddManager, bddID)),
                                                 k, cnfClauses);
      nextIndex    = BmcGetCnfVarIndexForBddNode(bddManager, bdd_regular(bdd_bdd_ith_var(bddManager, bddID)),
                                                 toState, cnfClauses);
                                                 
      andIndex1 = cnfClauses->cnfGlobalIndex++;
      BmcCnfGenerateClausesForAND(currentIndex, -nextIndex, andIndex1, cnfClauses);
      andIndex2 = cnfClauses->cnfGlobalIndex++;
      BmcCnfGenerateClausesForAND(-currentIndex, nextIndex, andIndex2, cnfClauses);
      
      array_insert_last(int, orClause, andIndex1);
      array_insert_last(int, orClause, andIndex2);
    }
    BmcCnfInsertClause(cnfClauses, orClause);
    array_free(orClause);
  } /* foreach k*/
  return;
} /* BmcCnfNoLoopToAnyPreviouseCompositeStates */