NuSMV/code/nusmv/core/rbc/clg/clg.h
Go to the documentation of this file.00001 /* --------------------------------------------------------------------------- 00002 00003 This file is part of the ``rbc.clg'' package 00004 of NuSMV version 2. Copyright (C) 2007 by FBK-irst. 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 USA. 00019 00020 For more information on NuSMV see <http://nusmv.fbk.eu> 00021 or email to <nusmv-users@fbk.eu>. 00022 Please report bugs to <nusmv-users@fbk.eu>. 00023 00024 To contact the NuSMV development board, email to <nusmv@fbk.eu>. 00025 00026 -----------------------------------------------------------------------------*/ 00027 00041 #ifndef __NUSMV_CORE_RBC_CLG_CLG_H__ 00042 #define __NUSMV_CORE_RBC_CLG_CLG_H__ 00043 00044 #include "nusmv/core/utils/utils.h" 00045 00046 /*---------------------------------------------------------------------------*/ 00047 /* Constant declarations */ 00048 /*---------------------------------------------------------------------------*/ 00049 00055 #define CLG_DIMACS 20 /* Create clauses suitable for a DIMACS file */ 00056 00062 #define CLG_ZCHAFF 21 /* Create clauses suitable for feeding to ZChaff directly */ 00063 00069 #define CLG_NUSMV 22 /* Create clauses suitable for feeding to NuMSV */ 00070 00071 /*---------------------------------------------------------------------------*/ 00072 /* Type declarations */ 00073 /*---------------------------------------------------------------------------*/ 00074 00081 typedef struct Clg_Vertex* clause_graph; 00082 00088 typedef void(*Clg_Commit)(void*, int*, int); 00089 00096 typedef struct ClgManager_TAG* ClgManager_ptr; 00097 00098 /*---------------------------------------------------------------------------*/ 00099 /* Structure declarations */ 00100 /*---------------------------------------------------------------------------*/ 00101 00102 /*---------------------------------------------------------------------------*/ 00103 /* Variable declarations */ 00104 /*---------------------------------------------------------------------------*/ 00105 00106 /*---------------------------------------------------------------------------*/ 00107 /* Macro declarations */ 00108 /*---------------------------------------------------------------------------*/ 00109 00110 00113 /*---------------------------------------------------------------------------*/ 00114 /* Function prototypes */ 00115 /*---------------------------------------------------------------------------*/ 00116 00123 ClgManager_ptr ClgManager_create(void); 00124 00130 void ClgManager_destroy(ClgManager_ptr clgManager); 00131 00137 clause_graph Clg_Lit(ClgManager_ptr clgmgr, int literal); 00138 00144 clause_graph Clg_Conj(ClgManager_ptr clgmgr, 00145 clause_graph left, clause_graph right); 00146 00152 clause_graph Clg_Disj(ClgManager_ptr clgmgr, 00153 clause_graph left, clause_graph right); 00154 00167 void Clg_Extract(const NuSMVEnv_ptr env, clause_graph head, 00168 int type, Clg_Commit commit, void *data); 00169 00175 int Clg_Size(clause_graph graph); 00176 00179 #endif /* __NUSMV_CORE_RBC_CLG_CLG_H__ */ 00180
