NuSMV/code/nusmv/core/sat/SatIncSolver_private.h
Go to the documentation of this file.00001 /* --------------------------------------------------------------------------- 00002 00003 00004 This file is part of the ``sat'' package of NuSMV version 2. 00005 Copyright (C) 2004 by FBK-irst. 00006 00007 NuSMV version 2 is free software; you can redistribute it and/or 00008 modify it under the terms of the GNU Lesser General Public 00009 License as published by the Free Software Foundation; either 00010 version 2 of the License, or (at your option) any later version. 00011 00012 NuSMV version 2 is distributed in the hope that it will be useful, 00013 but WITHOUT ANY WARRANTY; without even the implied warranty of 00014 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU 00015 Lesser General Public License for more details. 00016 00017 You should have received a copy of the GNU Lesser General Public 00018 License along with this library; if not, write to the Free Software 00019 Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA. 00020 00021 For more information on NuSMV see <http://nusmv.fbk.eu> 00022 or email to <nusmv-users@fbk.eu>. 00023 Please report bugs to <nusmv-users@fbk.eu>. 00024 00025 To contact the NuSMV development board, email to <nusmv@fbk.eu>. 00026 00027 -----------------------------------------------------------------------------*/ 00028 00037 #ifndef __NUSMV_CORE_SAT_SAT_INC_SOLVER_PRIVATE_H__ 00038 #define __NUSMV_CORE_SAT_SAT_INC_SOLVER_PRIVATE_H__ 00039 00040 #include "nusmv/core/sat/SatIncSolver.h" 00041 #include "nusmv/core/sat/SatSolver_private.h" 00042 00043 /*---------------------------------------------------------------------------*/ 00044 /* Macro declarations */ 00045 /*---------------------------------------------------------------------------*/ 00046 00047 /*---------------------------------------------------------------------------*/ 00048 /* Type declarations */ 00049 /*---------------------------------------------------------------------------*/ 00057 typedef struct SatIncSolver_TAG 00058 { 00059 INHERITS_FROM(SatSolver); 00060 00061 /* ---------------------------------------------------------------------- */ 00062 /* Virtual Methods */ 00063 /* ---------------------------------------------------------------------- */ 00064 00065 /* creates a new group */ 00066 VIRTUAL SatSolverGroup 00067 (*create_group) (const SatIncSolver_ptr self); 00068 00069 /* destroys existing group */ 00070 VIRTUAL void 00071 (*destroy_group) (const SatIncSolver_ptr self, SatSolverGroup group); 00072 /* moves formulas from 'group' into permanent one and destroys 'group' */ 00073 VIRTUAL void 00074 (*move_to_permanent_and_destroy_group) (const SatIncSolver_ptr self, 00075 SatSolverGroup group); 00076 00077 /* tries to solve formulas in the groups in the given list and the permanent 00078 group */ 00079 VIRTUAL SatSolverResult 00080 (*solve_groups) (const SatIncSolver_ptr self, const Olist_ptr groups); 00081 00082 /* tries to solve the formulas belonging to the solver except those 00083 in the group from the given list. Permanent group should not be 00084 in the list ever. */ 00085 VIRTUAL SatSolverResult 00086 (*solve_without_groups) (const SatIncSolver_ptr self, 00087 const Olist_ptr groups); 00088 } SatIncSolver; 00089 00092 /*---------------------------------------------------------------------------*/ 00093 /* Function prototypes */ 00094 /*---------------------------------------------------------------------------*/ 00099 void sat_inc_solver_init(SatIncSolver_ptr self, 00100 const NuSMVEnv_ptr env, 00101 const char* name); 00102 00107 void sat_inc_solver_deinit(SatIncSolver_ptr self); 00108 00109 /* pure virtual functions */ 00114 SatSolverGroup 00115 sat_inc_solver_create_group(const SatIncSolver_ptr self); 00116 00121 void 00122 sat_inc_solver_destroy_group(const SatIncSolver_ptr self, 00123 SatSolverGroup group); 00124 00129 void 00130 sat_inc_solver_move_to_permanent_and_destroy_group(const SatIncSolver_ptr self, 00131 SatSolverGroup group); 00136 SatSolverResult 00137 sat_inc_solver_solve_groups(const SatIncSolver_ptr self, 00138 const Olist_ptr groups); 00139 00144 SatSolverResult 00145 sat_inc_solver_solve_without_groups(const SatIncSolver_ptr self, 00146 const Olist_ptr groups); 00147 00150 #endif /* __NUSMV_CORE_SAT_SAT_INC_SOLVER_PRIVATE_H__ */
