NuSMV/code/nusmv/core/bmc/bmcUtils.h

Go to the documentation of this file.

/* ---------------------------------------------------------------------------


  This file is part of the ``bmc'' package of NuSMV version 2.
  Copyright (C) 2000-2001 by FBK-irst and University of Trento.

  NuSMV version 2 is free software; you can redistribute it and/or
  modify it under the terms of the GNU Lesser General Public
  License as published by the Free Software Foundation; either
  version 2 of the License, or (at your option) any later version.

  NuSMV version 2 is distributed in the hope that it will be useful,
  but WITHOUT ANY WARRANTY; without even the implied warranty of
  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
  Lesser General Public License for more details.

  You should have received a copy of the GNU Lesser General Public
  License along with this library; if not, write to the Free Software
  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307  USA.

  For more information on NuSMV see <http://nusmv.fbk.eu>
  or email to <nusmv-users@fbk.eu>.
  Please report bugs to <nusmv-users@fbk.eu>.

  To contact the NuSMV development board, email to <nusmv@fbk.eu>.

-----------------------------------------------------------------------------*/

#ifndef __NUSMV_CORE_BMC_BMC_UTILS_H__
#define __NUSMV_CORE_BMC_BMC_UTILS_H__

#include "nusmv/core/trace/Trace.h"
#include "nusmv/core/trace/TraceMgr.h"

#include "nusmv/core/utils/utils.h"
#include "nusmv/core/utils/ucmd.h"


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

#define UNKNOWN_OP      -1

#define CONSTANT_EXPR    0

#define LITERAL          1

#define PROP_CONNECTIVE  2

#define TIME_OPERATOR    3

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

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

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

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

#define isConstantExpr(op) ((op)==TRUEEXP)  || ((op)==FALSEEXP)

#define isVariable(op)     (((op)==DOT) || ((op) == BIT))

#define isPastOp(op)       ((op)==OP_PREC)  || ((op)==OP_NOTPRECNOT) ||    \
                           ((op)==OP_ONCE)  || ((op)==OP_HISTORICAL) ||    \
                           ((op)==SINCE)    || ((op)==TRIGGERED)

#define isBinaryOp(op)     ((op)==AND)      || ((op)==OR)            ||    \
                           ((op)==IFF)      || ((op)==UNTIL)         ||    \
                           ((op)==SINCE)    || ((op)==RELEASES)      ||    \
                           ((op)==TRIGGERED)

#define getOpClass(op) \
  ((op)==TRUEEXP)       || ((op)==FALSEEXP)      ? CONSTANT_EXPR           \
  :                                                                        \
  ((op)==DOT) || ((op) == BIT) || ((op)==NOT)    ? LITERAL                 \
  :                                                                        \
  ((op)==AND)           || ((op)==OR)        ||                            \
  ((op)==IFF)                                    ? PROP_CONNECTIVE         \
  :                                                                        \
  ((op)==OP_PREC)       || ((op)==OP_NEXT)   ||                            \
  ((op)==OP_NOTPRECNOT) ||                                                 \
  ((op)==OP_ONCE)       || ((op)==OP_FUTURE) ||                            \
  ((op)==OP_HISTORICAL) || ((op)==OP_GLOBAL) ||                            \
  ((op)==SINCE)         || ((op)==UNTIL)     ||                            \
  ((op)==TRIGGERED)     || ((op)==RELEASES)      ? TIME_OPERATOR           \
  :                                                                        \
                                                   UNKNOWN_OP

/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/

Trace_ptr
Bmc_Utils_generate_and_print_cntexample(BeEnc_ptr be_enc,
                                        TraceMgr_ptr tm,
                                        SatSolver_ptr solver,
                                        be_ptr be_prob,
                                        const int k,
                                        const char* trace_name,
                                        NodeList_ptr symbols);

Trace_ptr
Bmc_Utils_generate_cntexample(BeEnc_ptr be_enc,
                              SatSolver_ptr solver,
                              be_ptr be_prob,
                              const int k,
                              const char* trace_name,
                              NodeList_ptr symbols);

Trace_ptr
Bmc_Utils_fill_cntexample(BeEnc_ptr be_enc,
                          SatSolver_ptr solver,
                          const int k, Trace_ptr trace);

boolean Bmc_Utils_IsNoLoopback(const int l);

boolean Bmc_Utils_IsNoLoopbackString(const char* str);

boolean Bmc_Utils_IsSingleLoopback(const int l);

boolean Bmc_Utils_IsAllLoopbacks(const int l);

boolean Bmc_Utils_IsAllLoopbacksString(const char* str);

int Bmc_Utils_GetNoLoopback(void);

int Bmc_Utils_GetAllLoopbacks(void);

const char* Bmc_Utils_GetAllLoopbacksString(void);

int Bmc_Utils_RelLoop2AbsLoop(const int loop, const int k);

Outcome Bmc_Utils_Check_k_l(const int k, const int l);

int Bmc_Utils_GetSuccTime(const int time, const int k, const int l);

int Bmc_Utils_ConvertLoopFromString(const char* strValue, Outcome* result);

void Bmc_Utils_ConvertLoopFromInteger(const int iLoopback, char* szLoopback, const int _bufsize);

void
Bmc_Utils_ExpandMacrosInFilename(const char* filename_to_be_expanded,
      const SubstString* table_ptr,
      const size_t table_len,
      char* filename_expanded, size_t buf_len);

be_ptr
Bmc_Utils_apply_inlining(Be_Manager_ptr be_mgr, be_ptr f);

be_ptr
Bmc_Utils_apply_inlining4inc(Be_Manager_ptr be_mgr, be_ptr f);

be_ptr
Bmc_Utils_simple_costraint_from_string(BeEnc_ptr be_enc,
                                       BddEnc_ptr bdd_enc,
                                       const char* str,
                                       Expr_ptr* node_expr);

be_ptr
Bmc_Utils_next_costraint_from_string(BeEnc_ptr be_enc,
                                     BddEnc_ptr bdd_enc,
                                     const char* str,
                                     Expr_ptr* node_expr);

void
Bmc_Utils_add_be_into_inc_solver_positively(SatIncSolver_ptr solver,
                                            SatSolverGroup group,
                                            be_ptr prob,
                                            BeEnc_ptr be_enc,
                                            Be_CnfAlgorithm cnf_alg);

void
Bmc_Utils_add_be_into_non_inc_solver_positively(SatSolver_ptr solver,
                                                be_ptr prob,
                                                BeEnc_ptr be_enc,
                                                Be_CnfAlgorithm cnf_alg);

#endif /* __NUSMV_CORE_BMC_BMC_UTILS_H__ */

---