NuSMV Developers Manual: NuSMV/code/nusmv/core/bmc/sbmc/sbmcBmcInc.h Source File

00001 /* ---------------------------------------------------------------------------
00002 
00003  This file is part of the ``bmc.sbmc'' package of NuSMV version 2.
00004   Copyright (C) 2006 Tommi Junttila.
00005 
00006   NuSMV version 2 is free software; you can redistribute it and/or
00007   modify it under the terms of the GNU Lesser General Public License
00008   as published by the Free Software Foundation; either version 2 of
00009   the License, or (at your option) any later version.
00010 
00011   NuSMV version 2 is distributed in the hope that it will be useful,
00012   but WITHOUT ANY WARRANTY; without even the implied warranty of
00013   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
00014   Lesser General Public License for more details.
00015 
00016   You should have received a copy of the GNU Lesser General Public
00017   License along with this library; if not, write to the Free Software
00018   Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
00019   USA.
00020 
00021   For more information of NuSMV see <http://nusmv.fbk.eu> or
00022   email to <nusmv-users@fbk.eu>.  Please report bugs to
00023   <nusmv-users@fbk.eu>.
00024 
00025   To contact the NuSMV development board, email to  <nusmv@fbk.eu>. 
00026 
00027 -----------------------------------------------------------------------------*/
00028 
00039 #ifndef __NUSMV_CORE_BMC_SBMC_SBMC_BMC_INC_H__
00040 #define __NUSMV_CORE_BMC_SBMC_SBMC_BMC_INC_H__
00041 
00042 #include "nusmv/core/utils/utils.h"
00043 #include "nusmv/core/prop/Prop.h"
00044 
00045 /*---------------------------------------------------------------------------*/
00046 /* Constant declarations                                                     */
00047 /*---------------------------------------------------------------------------*/
00048 
00049 
00050 /*---------------------------------------------------------------------------*/
00051 /* Type declarations                                                         */
00052 /*---------------------------------------------------------------------------*/
00053 
00054 
00055 /*---------------------------------------------------------------------------*/
00056 /* Structure declarations                                                    */
00057 /*---------------------------------------------------------------------------*/
00058 
00059 
00060 /*---------------------------------------------------------------------------*/
00061 /* Variable declarations                                                     */
00062 /*---------------------------------------------------------------------------*/
00063 
00064 
00065 /*---------------------------------------------------------------------------*/
00066 /* Macro declarations                                                        */
00067 /*---------------------------------------------------------------------------*/
00068 
00069 
00072 /*---------------------------------------------------------------------------*/
00073 /* Function prototypes                                                       */
00074 /*---------------------------------------------------------------------------*/
00075 
00085 int Sbmc_zigzag_incr(NuSMVEnv_ptr env,
00086                             Prop_ptr ltlprop,
00087                             const int max_k,
00088                             const int opt_do_virtual_unrolling,
00089                             const int opt_do_completeness_check);
00090 
00102 int Sbmc_zigzag_incr_assume(NuSMVEnv_ptr env,
00103                                    Prop_ptr ltlprop,
00104                                    const int max_k,
00105                                    const int opt_do_virtual_unrolling,
00106                                    const int opt_do_completeness_check,
00107                                    Slist_ptr assumptions,
00108                                    Slist_ptr* conflict);
00109 
00110 
00113 #endif /* __NUSMV_CORE_BMC_SBMC_SBMC_BMC_INC_H__ */