ctl/wrapper_ctl.mli

   1 (*
   2  * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
   3  * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
   4  * This file is part of Coccinelle.
   5  *
   6  * Coccinelle is free software: you can redistribute it and/or modify
   7  * it under the terms of the GNU General Public License as published by
   8  * the Free Software Foundation, according to version 2 of the License.
   9  *
  10  * Coccinelle is distributed in the hope that it will be useful,
  11  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  12  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  13  * GNU General Public License for more details.
  14  *
  15  * You should have received a copy of the GNU General Public License
  16  * along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
  17  *
  18  * The authors reserve the right to distribute this or future versions of
  19  * Coccinelle under other licenses.
  20  *)
  21
  22
  23 type info = int
  24
  25 type ('pred, 'mvar) wrapped_ctl =
  26     ('pred * 'mvar Ast_ctl.modif,  'mvar, info) Ast_ctl.generic_ctl
  27
  28 type ('a, 'b) wrapped_binding =
  29     ClassicVal of 'a
  30   | PredVal of 'b Ast_ctl.modif
  31
  32 type ('pred,'state,'mvar,'value) labelfunc =
  33     'pred ->
  34       ('state * ('pred * ('mvar, 'value) Ast_ctl.generic_substitution))  list
  35
  36 module CTL_ENGINE_BIS :
  37   functor (SUB : Ctl_engine.SUBST) ->
  38     functor (G : Ctl_engine.GRAPH) ->
  39       functor(P : Ctl_engine.PREDICATE) ->
  40   sig
  41
  42     type predicate = P.t
  43     module WRAPPER_ENV :
  44         sig
  45           type mvar = SUB.mvar
  46           type value = (SUB.value, predicate) wrapped_binding
  47         end
  48     module WRAPPER_PRED :
  49         sig
  50           type t = P.t * SUB.mvar Ast_ctl.modif
  51         end
  52     module WRAPPER_ENGINE :
  53         sig
  54           type substitution =
  55               (WRAPPER_ENV.mvar, WRAPPER_ENV.value) Ast_ctl.generic_subst list
  56           type ('a, 'b) witness =
  57               (G.node, substitution,
  58                ('a, WRAPPER_ENV.mvar, 'b) Ast_ctl.generic_ctl list)
  59                 Ast_ctl.generic_witnesstree
  60           type ('a, 'b) triples =
  61               (G.node * substitution * ('a, 'b) witness list) list
  62         end
  63
  64
  65     val satbis_noclean :
  66         G.cfg *
  67         (predicate, G.node, WRAPPER_ENV.mvar, SUB.value) labelfunc *
  68         G.node list ->
  69           ((WRAPPER_PRED.t, WRAPPER_ENV.mvar, int) Ast_ctl.generic_ctl *
  70              (WRAPPER_PRED.t list list)) ->
  71                (WRAPPER_PRED.t, 'a) WRAPPER_ENGINE.triples
  72
  73     val satbis :
  74         G.cfg *
  75          (predicate,G.node,SUB.mvar,SUB.value) labelfunc *
  76          G.node list ->
  77            ((predicate,SUB.mvar) wrapped_ctl *
  78               (WRAPPER_PRED.t list list)) ->
  79                 (WRAPPER_ENV.mvar list * (SUB.mvar * SUB.value) list) ->
  80                   ((WRAPPER_PRED.t, 'a) WRAPPER_ENGINE.triples *
  81                      ((G.node * (SUB.mvar * SUB.value) list * predicate)
  82                         list list *
  83                         bool *
  84                         (WRAPPER_ENV.mvar * SUB.value) list list))
  85
  86     val print_bench : unit -> unit
  87 end