ctl/wrapper_ctl.mli

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